diff --git a/nix/agda.nix b/nix/agda.nix index 4ee53d92953..ba8c07676c1 100644 --- a/nix/agda.nix +++ b/nix/agda.nix @@ -115,16 +115,4 @@ rec { cabalProjectLocal = "extra-packages: ieee754, filemanip"; modules = [ agda-project-module-patch-default ]; }; - - # TODO this is a bit of a hack, but it's the only way to get the uplc - # executable to find the metatheory and the stdandard library. - shell-hook-exports = '' - export AGDA_STDLIB_SRC="${agda-stdlib}/src" - export PLUTUS_METHATHEORY_SRC="./plutus-metatheory/src" - ''; - - wrap-program-args = '' - --set AGDA_STDLIB_SRC "${agda-stdlib}/src" \ - --set PLUTUS_METHATHEORY_SRC "./plutus-metatheory/src" - ''; } diff --git a/nix/project.nix b/nix/project.nix index 85aeadc7498..da1d6eac031 100644 --- a/nix/project.nix +++ b/nix/project.nix @@ -3,151 +3,133 @@ { repoRoot, inputs, pkgs, system, lib }: let - cabalProject = pkgs.haskell-nix.cabalProject' ({ config, pkgs, ... }: - let - isCompilingMingwW64 = pkgs.stdenv.hostPlatform.system == "x86_64-windows" - && pkgs.stdenv.hostPlatform.libc == "msvcrt"; - isCompilingMusl64 = pkgs.stdenv.hostPlatform.system == "x86_64-linux" - && pkgs.stdenv.hostPlatform.libc == "musl"; - in { - name = "plutus"; - - # We need the mkDefault here since compiler-nix-name will be overridden - # in the flake variants. - compiler-nix-name = lib.mkDefault "ghc96"; - - src = ../.; - - shell = { - withHoogle = true; - # We would expect R to be pulled in automatically as it's a dependency of - # plutus-core, but it appears it is not, so we need to be explicit about - # the dependency on R here. Adding it as a buildInput will ensure it's - # added to the pkg-config env var. - buildInputs = [ pkgs.R ]; - }; - - flake.variants = { - ghc96 = { }; # Alias for the default project - ghc96-profiled.modules = [{ - enableProfiling = true; - enableLibraryProfiling = true; - }]; - ghc810.compiler-nix-name = "ghc810"; - ghc98.compiler-nix-name = "ghc98"; - ghc910.compiler-nix-name = "ghc910"; - }; - - inputMap = { - "https://chap.intersectmbo.org/" = inputs.iogx.inputs.CHaP; - }; - - sha256map = { - "https://github.com/jaccokrijnen/plutus-cert"."e814b9171398cbdfecdc6823067156a7e9fc76a3" = - "0srqvx0b819b5crrbsa9hz2fnr50ahqizvvm0wdmyq2bbpk2rka7"; - }; - - modules = [ - - (lib.mkIf (!isCompilingMingwW64 && !isCompilingMusl64) - repoRoot.nix.agda.agda-project-module-patch-default) - - (lib.mkIf isCompilingMusl64 - repoRoot.nix.agda.agda-project-module-patch-musl64) - - # Common - { - packages = { - # plutus-metatheory needs agda with the stdlib around for the custom setup - # I can't figure out a way to apply this as a blanket change for all the - # components in the package, oh well - plutus-metatheory.components.library.build-tools = - [ repoRoot.nix.agda.agda-with-stdlib ]; - plutus-metatheory.components.exes.plc-agda.build-tools = - [ repoRoot.nix.agda.agda-with-stdlib ]; - plutus-metatheory.components.tests.test-NEAT.build-tools = - [ repoRoot.nix.agda.agda-with-stdlib ]; - - plutus-executables.components.exes.uplc.build-tools = - [ repoRoot.nix.agda.agda-with-stdlib ]; - # plutus-executables.components.exes.uplc.postInstall = '' - # wrapProgram $out/bin/uplc ${repoRoot.nix.agda.wrap-program-args} - # ''; - - plutus-executables.components.tests.test-simple.build-tools = - [ repoRoot.nix.agda.agda-with-stdlib ]; - plutus-executables.components.tests.test-detailed.build-tools = - [ repoRoot.nix.agda.agda-with-stdlib ]; - - plutus-core.components.benchmarks.update-cost-model = { - build-tools = [ repoRoot.nix.r-with-packages ]; - }; - - plutus-core.components.benchmarks.cost-model-test = { - build-tools = [ repoRoot.nix.r-with-packages ]; - }; - - plutus-cert.components.library.build-tools = - # Needs to build both itself and its bundled deps. - # This needs both coq and ocaml packages, and only - # works with particular versions. Fortunately - # they're in nixpkgs. - let - ocamlPkgs = pkgs.ocaml-ng.ocamlPackages_4_10; - coqPkgs = pkgs.coqPackages_8_13; - in with ocamlPkgs; - with coqPkgs; [ - pkgs.perl - ocaml - ocamlbuild - findlib - coq - mathcomp - coq-ext-lib - ssreflect - equations - ]; - - plutus-core.components.tests.plutus-core-test.postInstall = '' - wrapProgram $out/bin/plutus-core-test --set PATH ${ - lib.makeBinPath [ pkgs.diffutils ] - } - ''; - - plutus-core.components.tests.plutus-ir-test.postInstall = '' - wrapProgram $out/bin/plutus-ir-test --set PATH ${ - lib.makeBinPath [ pkgs.diffutils ] - } - ''; - - # We want to build it but not run the tests in CI. - cardano-constitution.doCheck = false; + cabalProject = pkgs.haskell-nix.cabalProject' ({ config, pkgs, ... }: { + name = "plutus"; + + # We need the mkDefault here since compiler-nix-name will be overridden + # in the flake variants. + compiler-nix-name = lib.mkDefault "ghc96"; + + src = ../.; + + shell = { + withHoogle = true; + # We would expect R to be pulled in automatically as it's a dependency of + # plutus-core, but it appears it is not, so we need to be explicit about + # the dependency on R here. Adding it as a buildInput will ensure it's + # added to the pkg-config env var. + buildInputs = [ pkgs.R ]; + }; + + flake.variants = { + ghc96 = { }; # Alias for the default project + ghc96-profiled.modules = [{ + enableProfiling = true; + enableLibraryProfiling = true; + }]; + ghc810.compiler-nix-name = "ghc810"; + ghc98.compiler-nix-name = "ghc98"; + ghc910.compiler-nix-name = "ghc910"; + }; + + inputMap = { "https://chap.intersectmbo.org/" = inputs.iogx.inputs.CHaP; }; + + sha256map = { + "https://github.com/jaccokrijnen/plutus-cert"."e814b9171398cbdfecdc6823067156a7e9fc76a3" = + "0srqvx0b819b5crrbsa9hz2fnr50ahqizvvm0wdmyq2bbpk2rka7"; + }; + + modules = [ + # Common + { + packages = { + # plutus-metatheory needs agda with the stdlib around for the custom setup + # I can't figure out a way to apply this as a blanket change for all the + # components in the package, oh well + plutus-metatheory.components.library.build-tools = + [ repoRoot.nix.agda.agda-with-stdlib ]; + plutus-metatheory.components.exes.plc-agda.build-tools = + [ repoRoot.nix.agda.agda-with-stdlib ]; + plutus-metatheory.components.tests.test-NEAT.build-tools = + [ repoRoot.nix.agda.agda-with-stdlib ]; + + plutus-executables.components.exes.uplc.build-tools = + [ repoRoot.nix.agda.agda-with-stdlib ]; + + plutus-executables.components.tests.test-simple.build-tools = + [ repoRoot.nix.agda.agda-with-stdlib ]; + plutus-executables.components.tests.test-detailed.build-tools = + [ repoRoot.nix.agda.agda-with-stdlib ]; + + plutus-core.components.benchmarks.update-cost-model = { + build-tools = [ repoRoot.nix.r-with-packages ]; }; - } - - # -Werror for CI - # Only enable on the newer compilers. We don't care about warnings on the old ones, - # and sometimes it's hard to be warning free on all compilers, e.g. the unused - # packages warning is bad in 8.10.7 - # (https://gitlab.haskellib.org/ghc/ghc/-/merge_requests/6130) - (lib.mkIf (config.compiler-nix-name != "ghc8107") { - packages = { - - # Werror everything. - # This is a pain, see https://github.com/input-output-hk/haskell.nix/issues/519 - plutus-benchmark.ghcOptions = [ "-Werror" ]; - plutus-executables.ghcOptions = [ "-Werror" ]; - plutus-conformance.ghcOptions = [ "-Werror" ]; - plutus-core.ghcOptions = [ "-Werror" ]; - plutus-ledger-api.ghcOptions = [ "-Werror" ]; - # FIXME: has warnings in generated code - #plutus-metatheory.package.ghcOptions = "-Werror"; - plutus-tx.ghcOptions = [ "-Werror" ]; - plutus-tx-plugin.ghcOptions = [ "-Werror" ]; + + plutus-core.components.benchmarks.cost-model-test = { + build-tools = [ repoRoot.nix.r-with-packages ]; }; - }) - ]; - }); + + plutus-cert.components.library.build-tools = + # Needs to build both itself and its bundled deps. + # This needs both coq and ocaml packages, and only + # works with particular versions. Fortunately + # they're in nixpkgs. + let + ocamlPkgs = pkgs.ocaml-ng.ocamlPackages_4_10; + coqPkgs = pkgs.coqPackages_8_13; + in with ocamlPkgs; + with coqPkgs; [ + pkgs.perl + ocaml + ocamlbuild + findlib + coq + mathcomp + coq-ext-lib + ssreflect + equations + ]; + + plutus-core.components.tests.plutus-core-test.postInstall = '' + wrapProgram $out/bin/plutus-core-test --set PATH ${ + lib.makeBinPath [ pkgs.diffutils ] + } + ''; + + plutus-core.components.tests.plutus-ir-test.postInstall = '' + wrapProgram $out/bin/plutus-ir-test --set PATH ${ + lib.makeBinPath [ pkgs.diffutils ] + } + ''; + + # We want to build it but not run the tests in CI. + cardano-constitution.doCheck = false; + }; + } + + # -Werror for CI + # Only enable on the newer compilers. We don't care about warnings on the old ones, + # and sometimes it's hard to be warning free on all compilers, e.g. the unused + # packages warning is bad in 8.10.7 + # (https://gitlab.haskellib.org/ghc/ghc/-/merge_requests/6130) + (lib.mkIf (config.compiler-nix-name != "ghc8107") { + packages = { + + # Werror everything. + # This is a pain, see https://github.com/input-output-hk/haskell.nix/issues/519 + plutus-benchmark.ghcOptions = [ "-Werror" ]; + plutus-executables.ghcOptions = [ "-Werror" ]; + plutus-conformance.ghcOptions = [ "-Werror" ]; + plutus-core.ghcOptions = [ "-Werror" ]; + plutus-ledger-api.ghcOptions = [ "-Werror" ]; + # FIXME: has warnings in generated code + #plutus-metatheory.package.ghcOptions = "-Werror"; + plutus-tx.ghcOptions = [ "-Werror" ]; + plutus-tx-plugin.ghcOptions = [ "-Werror" ]; + }; + }) + ]; + }); project = lib.iogx.mkHaskellProject { inherit cabalProject; diff --git a/nix/shell.nix b/nix/shell.nix index d689c2e0d82..32787c4638b 100644 --- a/nix/shell.nix +++ b/nix/shell.nix @@ -98,7 +98,6 @@ in { shellHook = '' ${builtins.readFile certEnv} - ${repoRoot.nix.agda.shell-hook-exports} ''; preCommit = { diff --git a/plutus-executables/executables/uplc/Main.hs b/plutus-executables/executables/uplc/Main.hs index fbb24673d01..1ee7441b868 100644 --- a/plutus-executables/executables/uplc/Main.hs +++ b/plutus-executables/executables/uplc/Main.hs @@ -41,27 +41,15 @@ import Flat (unflat) import Options.Applicative import Prettyprinter ((<+>)) import System.Exit (exitFailure) -import System.FilePath (()) import System.IO (hPrint, stderr) import Text.Read (readMaybe) import Control.Monad.ST (RealWorld) import System.Console.Haskeline qualified as Repl -import Agda.Interaction.Base (ComputeMode (DefaultCompute)) -import Agda.Interaction.FindFile qualified as HAgda.File -import Agda.Interaction.Imports qualified as HAgda.Imp -import Agda.Interaction.Options (CommandLineOptions (optIncludePaths), defaultOptions) -import Agda.Syntax.Parser qualified as HAgda.Parser - -import Agda.Compiler.Backend (crInterface, iInsideScope, setCommandLineOptions, setScope) -import Agda.Interaction.BasicOps (evalInCurrent) -import Agda.Main (runTCMPrettyErrors) -import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract)) -import Agda.TypeChecking.Pretty (PrettyTCM (..)) -import Agda.Utils.FileName qualified as HAgda.File import AgdaUnparse (agdaUnparse) -import System.Environment (getEnv) + +import MAlonzo.Code.VerifiedCompilation (runCertifierMain) uplcHelpText :: String uplcHelpText = helpText "Untyped Plutus Core" @@ -298,44 +286,36 @@ runCertifier (Just certName) (SimplifierTrace simplTrace) = do (Left (err :: UPLC.FreeVariableError), _) -> error $ show err (_, Left (err :: UPLC.FreeVariableError)) -> error $ show err rawAgdaTrace = reverse $ processAgdaAST <$> simplTrace - runAgda certName rawAgdaTrace + runCertifierMain rawAgdaTrace + writeFile (certName ++ ".agda") (rawCertificate certName rawAgdaTrace) runCertifier Nothing _ = pure () --- | Run the Agda compiler on the metatheory and evaluate the 'runCertifier' function --- on the given trace. -runAgda - :: String - -- ^ The name of the certificate file to write - -> [(SimplifierStage, (AgdaFFI.UTerm, AgdaFFI.UTerm))] - -- ^ The trace produced by the simplification process - -> IO () -runAgda certName rawTrace = do - let program = "runCertifier (" ++ agdaUnparse rawTrace ++ ")" - (parseTraceResult, _) <- HAgda.Parser.runPMIO $ HAgda.Parser.parse HAgda.Parser.exprParser program - let parsedTrace = - case parseTraceResult of - Right (res, _) -> res - Left err -> error $ show err - stdlibPath <- getEnv "AGDA_STDLIB_SRC" - metatheoryPath <- getEnv "PLUTUS_METHATHEORY_SRC" - inputFile <- HAgda.File.absolute (metatheoryPath "Certifier.agda") - runTCMPrettyErrors $ do - let opts = - defaultOptions - { optIncludePaths = - [ metatheoryPath - , stdlibPath - ] - } - setCommandLineOptions opts - result <- HAgda.Imp.typeCheckMain HAgda.Imp.TypeCheck =<< HAgda.Imp.parseSource (HAgda.File.SourceFile inputFile) - let interface = crInterface result - insideScope = iInsideScope interface - setScope insideScope - internalisedTrace <- toAbstract parsedTrace - decisionProcedureResult <- evalInCurrent DefaultCompute internalisedTrace - final <- prettyTCM decisionProcedureResult - liftIO $ writeFile (certName ++ ".agda") (show final) +rawCertificate :: String -> [(SimplifierStage, (AgdaFFI.UTerm, AgdaFFI.UTerm))] -> String +rawCertificate certName rawTrace = + "module " <> certName <> " where\ + \\n\ + \\nopen import VerifiedCompilation\ + \\nopen import Untyped\ + \\nopen import RawU\ + \\nopen import Builtin\ + \\nopen import Data.Unit\ + \\nopen import Data.Nat\ + \\nopen import Data.Integer\ + \\nopen import Utils\ + \\nimport Agda.Builtin.Bool\ + \\nimport Relation.Nullary\ + \\nimport VerifiedCompilation.UntypedTranslation\ + \\nopen import Agda.Builtin.Maybe\ + \\nopen import Data.Empty using (⊥)\ + \\nopen import Data.Bool.Base using (Bool; false; true)\ + \\nopen import Agda.Builtin.Equality using (_≡_; refl)\ + \\n\ + \\nasts : List (SimplifierTag × Untyped × Untyped)\ + \\nasts = " <> agdaUnparse rawTrace <> + "\n\ + \\ncertificate : passed? (runCertifier asts) ≡ true\ + \\ncertificate = refl\ + \\n" ---------------- Script application ---------------- diff --git a/plutus-executables/plutus-executables.cabal b/plutus-executables/plutus-executables.cabal index 77de79f15a7..b9910189e21 100644 --- a/plutus-executables/plutus-executables.cabal +++ b/plutus-executables/plutus-executables.cabal @@ -103,12 +103,10 @@ executable uplc main-is: uplc/Main.hs hs-source-dirs: executables build-depends: - , Agda ==2.7.0 , base >=4.9 && <5 , bytestring , criterion , deepseq - , filepath , flat ^>=0.6 , haskeline , mtl diff --git a/plutus-metatheory/src/Certifier.agda b/plutus-metatheory/src/Certifier.agda deleted file mode 100644 index e4d5922985d..00000000000 --- a/plutus-metatheory/src/Certifier.agda +++ /dev/null @@ -1,17 +0,0 @@ --- Do not edit without also changing AgdaUnparse in plutus-executables. - -module Certifier where - -open import VerifiedCompilation -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) diff --git a/plutus-metatheory/src/VerifiedCompilation.lagda.md b/plutus-metatheory/src/VerifiedCompilation.lagda.md index 970a81e02fa..dcd58c4699c 100644 --- a/plutus-metatheory/src/VerifiedCompilation.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation.lagda.md @@ -156,10 +156,12 @@ postulate writeFile : String → String → IO ⊤ stderr : FileHandle hPutStrLn : FileHandle → String → IO ⊤ + putStrLn : String → IO ⊤ {-# COMPILE GHC writeFile = \f -> TextIO.writeFile (Text.unpack f) #-} {-# COMPILE GHC stderr = IO.stderr #-} {-# COMPILE GHC hPutStrLn = TextIO.hPutStr #-} +{-# COMPILE GHC putStrLn = TextIO.putStrLn #-} buildPairs : {X : Set} → List (Maybe X ⊢) -> List ((Maybe X ⊢) × (Maybe X ⊢)) buildPairs [] = [] @@ -186,3 +188,21 @@ runCertifier : List (SimplifierTag × Untyped × Untyped) → Maybe Proof runCertifier rawInput with traverseEitherList (toWellScoped {⊥}) rawInput ... | inj₁ _ = nothing ... | inj₂ inputTrace = just (proof (isTrace? inputTrace)) + +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) + +passed? : Maybe Proof → Bool +passed? (just (proof (no ¬a))) = false +passed? (just (proof (yes a))) = true +passed? nothing = false + +runCertifierMain : List (SimplifierTag × Untyped × Untyped) → IO ⊤ +runCertifierMain asts with runCertifier asts +... | just (proof (yes a)) = + putStrLn "The compilation was successfully certified." +... | just (proof (no ¬a)) = + putStrLn "The compilation was not successfully certified. Please open a bug report at https://www.github.com/IntersectMBO/plutus and attach the faulty certificate." +... | nothing = + putStrLn "The certifier was unable to check the compilation. Please open a bug report at https://www.github.com/IntersectMBO/plutus." +{-# COMPILE GHC runCertifierMain as runCertifierMain #-}