From 6fa1bc9b019fc3eb765e55e07d3039b09e8adbf3 Mon Sep 17 00:00:00 2001 From: Ana Pantilie <45069775+ana-pantilie@users.noreply.github.com> Date: Tue, 5 Nov 2024 18:08:45 +0200 Subject: [PATCH] Use Agda Haskell lib instead of MAlonzo (#6562) Co-authored-by: zeme --- nix/agda-packages.nix | 49 ------ nix/agda-project.nix | 42 ----- nix/agda-with-stdlib.nix | 30 ---- nix/agda.nix | 147 ++++++++++++++++++ nix/build-latex-doc.nix | 2 +- nix/outputs.nix | 5 +- nix/plutus-metatheory-site.nix | 2 +- nix/project.nix | 30 +++- nix/shell.nix | 3 +- nix/unraveling-recursion-paper.nix | 2 +- plutus-executables/executables/uplc/Main.hs | 94 ++++++++--- plutus-executables/plutus-executables.cabal | 27 +++- plutus-executables/src/AgdaUnparse.hs | 135 ++++++++++++++++ plutus-metatheory/src/Certifier.agda | 17 ++ .../src/VerifiedCompilation.lagda.md | 48 ++---- 15 files changed, 445 insertions(+), 188 deletions(-) delete mode 100644 nix/agda-packages.nix delete mode 100644 nix/agda-project.nix delete mode 100644 nix/agda-with-stdlib.nix create mode 100644 nix/agda.nix create mode 100644 plutus-executables/src/AgdaUnparse.hs create mode 100644 plutus-metatheory/src/Certifier.agda diff --git a/nix/agda-packages.nix b/nix/agda-packages.nix deleted file mode 100644 index b31facd3c4b..00000000000 --- a/nix/agda-packages.nix +++ /dev/null @@ -1,49 +0,0 @@ -{ repoRoot, inputs, pkgs, system, lib }: - -# We want to keep control of which version of Agda we use, so we supply our own and override -# the one from nixpkgs. -# -# The Agda builder needs a derivation with: -# - The 'agda' executable -# - The 'agda-mode' executable -# - A 'version' attribute -# -# So we stitch one together here. -# -# Furthermore, the agda builder uses a `ghcWithPackages` that has to have ieee754 available. -# We'd like it to use the same GHC as we have, if nothing else just to avoid depending on -# another GHC from nixpkgs! Sadly, this one is harder to override, and we just hack -# it into pkgs.haskellPackages in a fragile way. Annoyingly, this also means we have to ensure -# we have a few extra packages that it uses in our Haskell package set. -let - Agda = repoRoot.nix.agda-project.hsPkgs.Agda; - - frankenAgdaBin = pkgs.symlinkJoin { - name = "agda"; - version = Agda.identifier.version; - paths = [ - Agda.components.exes.agda - Agda.components.exes.agda-mode - ]; - }; - - frankenAgda = frankenAgdaBin // { - # Newer Agda is built with enableSeparateBinOutput, hence this hacky workaround. - # https://github.com/NixOS/nixpkgs/commit/294245f7501e0a8e69b83346a4fa5afd4ed33ab3 - bin = frankenAgdaBin; - }; - - frankenPkgs = - pkgs // - { - haskellPackages = pkgs.haskellPackages // - { - inherit (repoRoot.nix.agda-project) ghcWithPackages; - }; - }; -in - -pkgs.agdaPackages.override { - Agda = frankenAgda; - pkgs = frankenPkgs; -} diff --git a/nix/agda-project.nix b/nix/agda-project.nix deleted file mode 100644 index e81e2b3e78c..00000000000 --- a/nix/agda-project.nix +++ /dev/null @@ -1,42 +0,0 @@ -{ repoRoot, inputs, pkgs, system, lib }: - -pkgs.haskell-nix.hackage-project { - name = "Agda"; - - version = "2.6.4"; - - compiler-nix-name = "ghc96"; - - cabalProjectLocal = '' - extra-packages: ieee754, filemanip - ''; - - modules = [{ - # Agda is a huge pain. They have a special custom setup that compiles the - # interface files for the Agda that ships with the compiler. These go in - # the data files for the *library*, but they require the *executable* to - # compile them, which depends on the library! They get away with it by - # using the old-style builds and building everything together, we can't - # do that. - # So we work around it: - # - turn off the custom setup - # - manually compile the executable (fortunately it has no extra - # dependencies!) and do the compilation at the end of the library derivation. - packages.Agda.package.buildType = lib.mkForce "Simple"; - packages.Agda.components.library.enableSeparateDataOutput = lib.mkForce true; - packages.Agda.components.library.postInstall = '' - # Compile the executable using the package DB we've just made, which contains - # the main Agda library - ghc src/main/Main.hs -package-db=$out/package.conf.d -o agda - - # Find all the files in $data - shopt -s globstar - files=($data/**/*.agda) - for f in "''${files[@]}" ; do - echo "Compiling $f" - # This is what the custom setup calls in the end - ./agda --no-libraries --local-interfaces $f - done - ''; - }]; -} diff --git a/nix/agda-with-stdlib.nix b/nix/agda-with-stdlib.nix deleted file mode 100644 index ee4c8918e65..00000000000 --- a/nix/agda-with-stdlib.nix +++ /dev/null @@ -1,30 +0,0 @@ -{ repoRoot, inputs, pkgs, system, lib }: - -let - # Need a newer version for 2.6.2 compatibility - stdlib = repoRoot.nix.agda-packages.standard-library.overrideAttrs (oldAtts: rec { - - version = "1.7.3"; - - src = pkgs.fetchFromGitHub { - repo = "agda-stdlib"; - owner = "agda"; - rev = "v${version}"; - sha256 = "sha256-vtL6VPvTXhl/mepulUm8SYyTjnGsqno4RHDmTIy22Xg="; - }; - # This is preConfigure is copied from more recent nixpkgs that also - # uses version 1.7 of standard-library. Old nixpkgs (that used 1.4) - # had a preConfigure step that worked with 1.7. Less old nixpkgs - # (that used 1.6) had a preConfigure step that attempts to `rm` - # files that are now in the .gitignore list for 1. - preConfigure = '' - runhaskell GenerateEverything.hs - # We will only build/consider Everything.agda, in particular we don't want Everything*.agda - # do be copied to the store. - rm EverythingSafe.agda - ''; - }); - -in - -repoRoot.nix.agda-packages.agda.withPackages [ stdlib ] diff --git a/nix/agda.nix b/nix/agda.nix new file mode 100644 index 00000000000..cfcb10aced7 --- /dev/null +++ b/nix/agda.nix @@ -0,0 +1,147 @@ +{ repoRoot, inputs, pkgs, system, lib }: + +rec { + + agda-stdlib = agda-packages.standard-library.overrideAttrs (oldAtts: rec { + + version = "1.7.3"; + + src = pkgs.fetchFromGitHub { + repo = "agda-stdlib"; + owner = "agda"; + rev = "v${version}"; + sha256 = "sha256-vtL6VPvTXhl/mepulUm8SYyTjnGsqno4RHDmTIy22Xg="; + }; + + # This is preConfigure is copied from more recent nixpkgs that also + # uses version 1.7 of standard-library. Old nixpkgs (that used 1.4) + # had a preConfigure step that worked with 1.7. Less old nixpkgs + # (that used 1.6) had a preConfigure step that attempts to `rm` + # files that are now in the .gitignore list for 1. + preConfigure = '' + runhaskell GenerateEverything.hs + # We will only build/consider Everything.agda, in particular we don't want Everything*.agda + # do be copied to the store. + rm EverythingSafe.agda + ''; + }); + + + # We want to keep control of which version of Agda we use, so we supply our own and override + # the one from nixpkgs. + # + # The Agda builder needs a derivation with: + # - The 'agda' executable + # - The 'agda-mode' executable + # - A 'version' attribute + # + # So we stitch one together here. + # + # Furthermore, the agda builder uses a `ghcWithPackages` that has to have ieee754 available. + # We'd like it to use the same GHC as we have, if nothing else just to avoid depending on + # another GHC from nixpkgs! Sadly, this one is harder to override, and we just hack + # it into pkgs.haskellPackages in a fragile way. Annoyingly, this also means we have to ensure + # we have a few extra packages that it uses in our Haskell package set. + agda-packages = + let + Agda = agda-project.hsPkgs.Agda; + + frankenAgdaBin = pkgs.symlinkJoin { + name = "agda"; + version = Agda.identifier.version; + paths = [ + Agda.components.exes.agda + Agda.components.exes.agda-mode + ]; + }; + + frankenAgda = frankenAgdaBin // { + # Newer Agda is built with enableSeparateBinOutput, hence this hacky workaround. + # https://github.com/NixOS/nixpkgs/commit/294245f7501e0a8e69b83346a4fa5afd4ed33ab3 + bin = frankenAgdaBin; + }; + + frankenPkgs = + pkgs // + { + haskellPackages = pkgs.haskellPackages // + { + inherit (agda-project) ghcWithPackages; + }; + }; + in + pkgs.agdaPackages.override { + Agda = frankenAgda; + pkgs = frankenPkgs; + }; + + + # Agda is a huge pain. They have a special custom setup that compiles the + # interface files for the Agda that ships with the compiler. These go in + # the data files for the *library*, but they require the *executable* to + # compile them, which depends on the library! They get away with it by + # using the old-style builds and building everything together, we can't + # do that. + # So we work around it: + # - turn off the custom setup + # - manually compile the executable (fortunately it has no extra dependencies!) + # and do the compilation at the end of the library derivation. + # In addition, depending on whether we are cross-compiling or not, the + # compiler-nix-name handed to us by haskell.nix will be different, so we need + # to pass it in. + agda-project-module-patch = { compiler-nix-name }: { + packages.Agda.doHaddock = lib.mkForce false; + packages.Agda.package.buildType = lib.mkForce "Simple"; + packages.Agda.components.library.enableSeparateDataOutput = lib.mkForce true; + packages.Agda.components.library.postInstall = '' + # Compile the executable using the package DB we've just made, which contains + # the main Agda library + ${compiler-nix-name} src/main/Main.hs -package-db=$out/package.conf.d -o agda + + # Find all the files in $data + shopt -s globstar + files=($data/**/*.agda) + for f in "''${files[@]}" ; do + echo "Compiling $f" + # This is what the custom setup calls in the end + ./agda --no-libraries --local-interfaces $f + done + ''; + }; + + + agda-project-module-patch-default = agda-project-module-patch { + compiler-nix-name = "ghc"; + }; + + + agda-project-module-patch-musl64 = agda-project-module-patch { + compiler-nix-name = "x86_64-unknown-linux-musl-ghc"; + }; + + + agda-with-stdlib = agda-packages.agda.withPackages [ agda-stdlib ]; + + + agda-project = pkgs.haskell-nix.hackage-project { + name = "Agda"; + version = "2.6.4.3"; + compiler-nix-name = "ghc96"; + 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/build-latex-doc.nix b/nix/build-latex-doc.nix index 7a82fdc2ee2..2204fbfd735 100644 --- a/nix/build-latex-doc.nix +++ b/nix/build-latex-doc.nix @@ -16,7 +16,7 @@ repoRoot.nix.build-latex { buildInputs = lib.optionals withAgda [ - repoRoot.nix.agda-with-stdlib + repoRoot.nix.agda.agda-with-stdlib ]; diff --git a/nix/outputs.nix b/nix/outputs.nix index c35bf6de619..bf7a2d36e74 100644 --- a/nix/outputs.nix +++ b/nix/outputs.nix @@ -35,7 +35,6 @@ in { packages.plutus-metatheory-site = repoRoot.nix.plutus-metatheory-site; packages.pre-commit-check = ghc96.pre-commit-check; - packages.agda-project = repoRoot.nix.agda-project.hsPkgs.Agda.components.exes.agda; } (lib.optionalAttrs (system == "x86_64-linux" || system == "x86_64-darwin") @@ -64,9 +63,7 @@ in (lib.optionalAttrs (system == "aarch64-darwin") { # Plausibly if things build on x86 darwin then they'll build on aarch darwin. - # Se we only build roots and devshells on aarch to avoid overloading the builders. - # Note: We can't build the 9.6 shell on aarch64-darwin - # because of https://github.com/well-typed/cborg/issues/311 + # Se we only build roots and dev sshells on aarch to avoid overloading the builders. hydraJobs.ghc810.devShell = ghc810.devShell; hydraJobs.ghc96.devShell = ghc96.devShell; hydraJobs.ghc98.devShell = ghc98.devShell; diff --git a/nix/plutus-metatheory-site.nix b/nix/plutus-metatheory-site.nix index 18cac84f7ba..43f0836ef73 100644 --- a/nix/plutus-metatheory-site.nix +++ b/nix/plutus-metatheory-site.nix @@ -21,7 +21,7 @@ let plutus-metatheory-agda-html = pkgs.stdenv.mkDerivation { name = "plutus-metatheory-doc"; src = lib.cleanSource (inputs.self + /plutus-metatheory); - buildInputs = [ repoRoot.nix.agda-with-stdlib ]; + buildInputs = [ repoRoot.nix.agda.agda-with-stdlib ]; dontInstall = true; # Jekyll requires the _layouts folder to be in the same directory as the diff --git a/nix/project.nix b/nix/project.nix index 993157e3c24..c3d5b5f20d5 100644 --- a/nix/project.nix +++ b/nix/project.nix @@ -4,7 +4,10 @@ let cabalProject = pkgs.haskell-nix.cabalProject' ({ config, pkgs, ... }: - let isCrossCompiling = pkgs.stdenv.hostPlatform != pkgs.stdenv.buildPlatform; in + 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"; @@ -41,19 +44,32 @@ let }; 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-with-stdlib ]; - plutus-metatheory.components.exes.plc-agda.build-tools = [ repoRoot.nix.agda-with-stdlib ]; - plutus-metatheory.components.tests.test-NEAT.build-tools = [ repoRoot.nix.agda-with-stdlib ]; + 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.exes.uplc.build-tools = [ repoRoot.nix.agda-with-stdlib ]; - plutus-executables.components.tests.test-simple.build-tools = [ repoRoot.nix.agda-with-stdlib ]; - plutus-executables.components.tests.test-detailed.build-tools = [ repoRoot.nix.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 ]; diff --git a/nix/shell.nix b/nix/shell.nix index 0350d47e84a..cf70014277f 100644 --- a/nix/shell.nix +++ b/nix/shell.nix @@ -29,7 +29,7 @@ in welcomeMessage = "🤟 \\033[1;34mWelcome to Plutus\\033[0m 🤟"; packages = [ - repoRoot.nix.agda-with-stdlib + repoRoot.nix.agda.agda-with-stdlib # R environment repoRoot.nix.r-with-packages @@ -92,6 +92,7 @@ in shellHook = '' ${builtins.readFile certEnv} + ${repoRoot.nix.agda.shell-hook-exports} ''; preCommit = { diff --git a/nix/unraveling-recursion-paper.nix b/nix/unraveling-recursion-paper.nix index e1c5bae4a7f..190583f8b1f 100644 --- a/nix/unraveling-recursion-paper.nix +++ b/nix/unraveling-recursion-paper.nix @@ -35,7 +35,7 @@ repoRoot.nix.build-latex { }; buildInputs = [ - repoRoot.nix.agda-with-stdlib + repoRoot.nix.agda.agda-with-stdlib pkgs.zip ]; diff --git a/plutus-executables/executables/uplc/Main.hs b/plutus-executables/executables/uplc/Main.hs index eb6ca71648c..9d16b884700 100644 --- a/plutus-executables/executables/uplc/Main.hs +++ b/plutus-executables/executables/uplc/Main.hs @@ -1,14 +1,7 @@ -- editorconfig-checker-disable -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} -{-# LANGUAGE NamedFieldPuns #-} + module Main (main) where import PlutusCore qualified as PLC @@ -24,7 +17,6 @@ import PlutusCore.Executable.Parsers import PlutusCore.MkPlc (mkConstant) import PlutusPrelude -import MAlonzo.Code.VerifiedCompilation qualified as Agda import Untyped qualified as AgdaFFI import UntypedPlutusCore.Evaluation.Machine.SteppableCek.DebugDriver qualified as D @@ -49,12 +41,29 @@ 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 Data.Text qualified as Text +import System.Environment (getEnv) + uplcHelpText :: String uplcHelpText = helpText "Untyped Plutus Core" @@ -272,16 +281,62 @@ runOptimisations (OptimiseOptions inp ifmt outp ofmt mode cert) = do UPLC.simplifyProgramWithTrace UPLC.defaultSimplifyOpts defaultBuiltinSemanticsVariant renamed writeProgram outp ofmt mode simplified runCertifier cert simplificationTrace - where - runCertifier (Just certName) (SimplifierTrace simplTrace) = do - let processAgdaAST Simplification {beforeAST, stage, afterAST} = - case (UPLC.deBruijnTerm beforeAST, UPLC.deBruijnTerm afterAST) of - (Right before', Right after') -> (stage, (AgdaFFI.conv (void before'), AgdaFFI.conv (void after'))) - (Left (err :: UPLC.FreeVariableError), _) -> error $ show err - (_, Left (err :: UPLC.FreeVariableError)) -> error $ show err - rawAgdaTrace = reverse $ processAgdaAST <$> simplTrace - Agda.runCertifier (T.pack certName) rawAgdaTrace - runCertifier Nothing _ = pure () + +---------------- Agda certifier ---------------- + +-- | Run the Agda certifier on the simplification trace, if requested +runCertifier + :: Maybe String + -- ^ Should we run the Agda certifier? If so, what should the certificate file be called? + -> SimplifierTrace UPLC.Name UPLC.DefaultUni UPLC.DefaultFun a + -- ^ The trace produced by the simplification process + -> IO () +runCertifier (Just certName) (SimplifierTrace simplTrace) = do + let processAgdaAST Simplification {beforeAST, stage, afterAST} = + case (UPLC.deBruijnTerm beforeAST, UPLC.deBruijnTerm afterAST) of + (Right before', Right after') -> + (stage, (AgdaFFI.conv (void before'), AgdaFFI.conv (void after'))) + (Left (err :: UPLC.FreeVariableError), _) -> error $ show err + (_, Left (err :: UPLC.FreeVariableError)) -> error $ show err + rawAgdaTrace = reverse $ processAgdaAST <$> simplTrace + runAgda 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" + let inputFile = HAgda.File.AbsolutePath (Text.pack $ 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) ---------------- Script application ---------------- @@ -399,7 +454,6 @@ runDbg (DbgOptions inp ifmt cekModel semvar) = do -- nilSlippage is important so as to get correct live up-to-date budget cekTrans <- fst <$> D.mkCekTrans cekparams Cek.restrictingEnormous Cek.noEmitter D.nilSlippage Repl.runInputT replSettings $ - -- MAYBE: use cutoff or partialIterT to prevent runaway D.iterTM (handleDbg cekTrans) $ D.runDriverT nterm -- TODO: this is just an example of an optional single breakpoint, decide diff --git a/plutus-executables/plutus-executables.cabal b/plutus-executables/plutus-executables.cabal index cb54f112862..a1ff152a0e4 100644 --- a/plutus-executables/plutus-executables.cabal +++ b/plutus-executables/plutus-executables.cabal @@ -23,6 +23,7 @@ source-repository head common lang default-language: Haskell2010 default-extensions: + BangPatterns DeriveFoldable DeriveFunctor DeriveGeneric @@ -30,12 +31,20 @@ common lang DeriveTraversable DerivingStrategies DerivingVia + ExistentialQuantification ExplicitForAll FlexibleContexts + GADTs GeneralizedNewtypeDeriving ImportQualifiedPost + LambdaCase + MultiParamTypeClasses + NamedFieldPuns + OverloadedStrings ScopedTypeVariables StandaloneDeriving + TypeApplications + TypeSynonymInstances ghc-options: -Wall -Wnoncanonical-monad-instances -Wincomplete-uni-patterns @@ -50,6 +59,17 @@ common os-support if (impl(ghcjs) || os(windows)) buildable: False +library lib + import: lang, os-support + hs-source-dirs: src + exposed-modules: AgdaUnparse + build-depends: + , base >=4.9 && <5 + , bytestring + , plutus-core ^>=1.36 + , plutus-metatheory + , text + executable pir import: lang main-is: pir/Main.hs @@ -85,21 +105,26 @@ executable uplc main-is: uplc/Main.hs hs-source-dirs: executables build-depends: - , base >=4.9 && <5 + , Agda ==2.6.4.3 + , base >=4.9 && <5 , bytestring , criterion , deepseq + , filepath , flat ^>=0.6 , haskeline , mtl , optparse-applicative , plutus-core ^>=1.36 , plutus-core:plutus-core-execlib + , plutus-executables:lib , plutus-metatheory , prettyprinter , split , text +-- build-tool-depends: Agda:agda + test-suite test-simple import: lang, os-support type: exitcode-stdio-1.0 diff --git a/plutus-executables/src/AgdaUnparse.hs b/plutus-executables/src/AgdaUnparse.hs new file mode 100644 index 00000000000..e36c9fc6528 --- /dev/null +++ b/plutus-executables/src/AgdaUnparse.hs @@ -0,0 +1,135 @@ +module AgdaUnparse where + +import Data.ByteString (ByteString) +import Data.Functor.Identity +import Data.Text (Text) +import Data.Text qualified as T +import PlutusCore qualified as PLC +import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1 +import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2 +import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing +import PlutusCore.Data (Data) +import PlutusCore.Data qualified as Data +import PlutusCore.Default (DSum (..)) +import PlutusPrelude +import Untyped qualified as AgdaFFI +import UntypedPlutusCore qualified as UPLC +import UntypedPlutusCore.Transform.Simplifier + +-- | A class for types that can be unparsed to Agda code. +class AgdaUnparse a where + agdaUnparse :: a -> String + +instance AgdaUnparse AgdaFFI.UTerm where + agdaUnparse = + \case + AgdaFFI.UVar n -> "(UVar " ++ agdaUnparse (fromInteger n :: Natural) ++ ")" + AgdaFFI.ULambda term -> "(ULambda " ++ agdaUnparse term ++ ")" + AgdaFFI.UApp t u -> "(UApp " ++ agdaUnparse t ++ " " ++ agdaUnparse u ++ ")" + AgdaFFI.UCon someValue -> "(UCon " ++ (agdaUnparseValue . mkValueDSum) someValue ++ ")" + AgdaFFI.UError -> "UError" + AgdaFFI.UBuiltin fun -> "(UBuiltin " ++ agdaUnparse fun ++ ")" + AgdaFFI.UDelay term -> "(UDelay " ++ agdaUnparse term ++ ")" + AgdaFFI.UForce term -> "(UForce " ++ agdaUnparse term ++ ")" + AgdaFFI.UConstr i terms -> "(UConstr " ++ agdaUnparse i ++ " " ++ agdaUnparse terms ++ ")" + AgdaFFI.UCase term cases -> "(UCase " ++ agdaUnparse term ++ " " ++ agdaUnparse cases ++ ")" + +instance AgdaUnparse UPLC.DefaultFun where + agdaUnparse = lowerInitialChar . show + +instance AgdaUnparse SimplifierStage where + agdaUnparse FloatDelay = "floatDelayT" + agdaUnparse ForceDelay = "forceDelayT" + agdaUnparse CaseOfCase = "caseOfCaseT" + agdaUnparse CaseReduce = "caseReduceT" + agdaUnparse Inline = "inlineT" + agdaUnparse CSE = "cseT" + +instance AgdaUnparse Natural where + agdaUnparse = show + +instance AgdaUnparse Integer where + agdaUnparse x = "(ℤ.pos " ++ show x ++ ")" + +instance AgdaUnparse Bool where + agdaUnparse True = "true" + agdaUnparse False = "false" + +instance AgdaUnparse Char where + agdaUnparse c = [c] +instance AgdaUnparse Text where + agdaUnparse = T.unpack + +instance AgdaUnparse ByteString where + agdaUnparse = show -- TODO: maybe this should be encoded some other way + +instance AgdaUnparse () where + agdaUnparse _ = "tt" + +instance AgdaUnparse a => AgdaUnparse [a] where + agdaUnparse l = "(" ++ foldr (\x xs -> agdaUnparse x ++ " ∷ " ++ xs) "[]" l ++ ")" + +instance (AgdaUnparse a, AgdaUnparse b) => AgdaUnparse (a, b) where + agdaUnparse (x, y) = "(" ++ agdaUnparse x ++ " , " ++ agdaUnparse y ++ ")" + +instance AgdaUnparse Data where + agdaUnparse (Data.Constr i args) = + "(ConstrDATA" ++ " " ++ agdaUnparse i ++ " " ++ agdaUnparse args ++ ")" + agdaUnparse (Data.Map assocList) = + "(MapDATA" ++ " " ++ agdaUnparse assocList ++ ")" + agdaUnparse (Data.List xs) = + "(ListDATA" ++ " " ++ agdaUnparse xs ++ ")" + agdaUnparse (Data.I i) = + "(iDATA" ++ " " ++ agdaUnparse i ++ ")" + agdaUnparse (Data.B b) = + "(bDATA" ++ " " ++ agdaUnparse b ++ ")" + +instance AgdaUnparse BLS12_381.G1.Element where + agdaUnparse = show + +instance AgdaUnparse BLS12_381.G2.Element where + agdaUnparse = show + +instance AgdaUnparse BLS12_381.Pairing.MlResult where + agdaUnparse = show + +agdaUnparseValue :: DSum (PLC.ValueOf UPLC.DefaultUni) Identity -> String +agdaUnparseValue dSum = + "(tagCon " ++ + case dSum of + PLC.ValueOf PLC.DefaultUniInteger _ :=> Identity val -> + "integer " ++ agdaUnparse val + PLC.ValueOf PLC.DefaultUniByteString _ :=> Identity val -> + "bytestring " ++ agdaUnparse val + PLC.ValueOf PLC.DefaultUniString _ :=> Identity val -> + "string " ++ agdaUnparse val + PLC.ValueOf PLC.DefaultUniBool _ :=> Identity val -> + "bool " ++ agdaUnparse val + PLC.ValueOf PLC.DefaultUniUnit _ :=> Identity _ -> + "unit " ++ agdaUnparse () + PLC.ValueOf PLC.DefaultUniData _ :=> Identity val -> + "pdata " ++ agdaUnparse val + PLC.ValueOf (PLC.DefaultUniList elemType) _ :=> Identity val -> + "list " ++ agdaUnparseDList elemType val + PLC.ValueOf (PLC.DefaultUniPair type1 type2) _ :=> Identity val -> + "pair " ++ agdaUnparseDPair type1 type2 val + PLC.ValueOf PLC.DefaultUniBLS12_381_G1_Element _ :=> Identity val -> + "bls12-381-g1-element " ++ agdaUnparse val + PLC.ValueOf PLC.DefaultUniBLS12_381_G2_Element _ :=> Identity val -> + "bls12-381-g2-element " ++ agdaUnparse val + PLC.ValueOf PLC.DefaultUniBLS12_381_MlResult _ :=> Identity val -> + "bls12-381-mlresult " ++ agdaUnparse val + _ -> error "agdaUnparseValue: unexpected value" + ++ ")" + where + agdaUnparseDList elemType xs = + let xs' :: [DSum (PLC.ValueOf PLC.DefaultUni) Identity] + xs' = mkValueDSum . PLC.Some . PLC.ValueOf elemType <$> xs + in agdaUnparse $ agdaUnparseValue <$> xs' + agdaUnparseDPair type1 type2 (x, y) = + let x' = mkValueDSum $ PLC.Some $ PLC.ValueOf type1 x + y' = mkValueDSum $ PLC.Some $ PLC.ValueOf type2 y + in agdaUnparse (agdaUnparseValue x', agdaUnparseValue y') + +mkValueDSum :: PLC.Some (PLC.ValueOf UPLC.DefaultUni) -> DSum (PLC.ValueOf UPLC.DefaultUni) Identity +mkValueDSum (PLC.Some valueOf@(PLC.ValueOf _ a)) = valueOf :=> Identity a diff --git a/plutus-metatheory/src/Certifier.agda b/plutus-metatheory/src/Certifier.agda new file mode 100644 index 00000000000..e4d5922985d --- /dev/null +++ b/plutus-metatheory/src/Certifier.agda @@ -0,0 +1,17 @@ +-- 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 9d8f3b1af6e..bfdc7c37124 100644 --- a/plutus-metatheory/src/VerifiedCompilation.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation.lagda.md @@ -58,8 +58,8 @@ import Relation.Binary as Binary using (Decidable) open import VerifiedCompilation.UntypedTranslation using (Translation; Relation; translation?) import Relation.Binary as Binary using (Decidable) import Relation.Unary as Unary using (Decidable) +import Agda.Builtin.Int import Relation.Nary as Nary using (Decidable) - ``` ## Compiler optimisation traces @@ -136,27 +136,11 @@ isTrace? ((tag , x₁ , x₂) ∷ xs) with isTrace? xs ``` -## Serialising the proofs - -The proof objects are converted to a textual representation which can be written to a file. - -**TODO**: This is currently not supported. The `showTrace` function is a placeholder for the actual serialisation function. - -``` -showTrace : {X : Set} {{_ : DecEq X}} {xs : List (SimplifierTag × (X ⊢) × (X ⊢))} → Trace xs → String -showTrace _ = "TODO" -serializeTraceProof : {X : Set} {{_ : DecEq X}} {xs : List (SimplifierTag × (X ⊢) × (X ⊢))} → Dec (Trace xs) → String -serializeTraceProof (no ¬p) = "no" -serializeTraceProof (yes p) = "yes " ++ showTrace p - -``` ## The certification function -The `runCertifier` function is the top-level function which can be called by the compiler through the foreign function interface. -It represents the "impure top layer" which receives the list of ASTs produced by the compiler and writes the certificate -generated by the `certifier` function to disk. +The `runCertifier` function is the top-level function which can be called by the compiler. ``` @@ -177,6 +161,11 @@ postulate {-# COMPILE GHC stderr = IO.stderr #-} {-# COMPILE GHC hPutStrLn = TextIO.hPutStr #-} +buildPairs : {X : Set} → List (Maybe X ⊢) -> List ((Maybe X ⊢) × (Maybe X ⊢)) +buildPairs [] = [] +buildPairs (x ∷ []) = (x , x) ∷ [] +buildPairs (x₁ ∷ (x₂ ∷ xs)) = (x₁ , x₂) ∷ buildPairs (x₂ ∷ xs) + traverseEitherList : {A B E : Set} → (A → Either E B) → List (SimplifierTag × A × A) → Either E (List (SimplifierTag × B × B)) traverseEitherList _ [] = inj₂ [] traverseEitherList f ((tag , before , after) ∷ xs) with f before @@ -187,16 +176,13 @@ traverseEitherList f ((tag , before , after) ∷ xs) with f before ... | inj₁ e = inj₁ e ... | inj₂ xs' = inj₂ (((tag , b , a)) ∷ xs') -certifier - : {X : Set} {{_ : DecEq X}} - → List (SimplifierTag × Untyped × Untyped) - → Either ScopeError String -certifier {X} rawInput with traverseEitherList (toWellScoped {X}) rawInput -... | inj₁ err = inj₁ err -... | inj₂ inputTrace = inj₂ (serializeTraceProof (isTrace? inputTrace)) - -runCertifier : String → List (SimplifierTag × Untyped × Untyped) → IO ⊤ -runCertifier fileName rawInput with certifier {⊥} rawInput -... | inj₁ err = hPutStrLn stderr "error" -- TODO: pretty print error -... | inj₂ result = writeFile (fileName ++ ".agda") result -{-# COMPILE GHC runCertifier as runCertifier #-} +data Proof : Set₁ where + proof + : {X : Set} {result : List (SimplifierTag × (X ⊢) × (X ⊢))} {{_ : DecEq X}} + → Dec (Trace {X} result) + → Proof + +runCertifier : List (SimplifierTag × Untyped × Untyped) → Maybe Proof +runCertifier rawInput with traverseEitherList (toWellScoped {⊥}) rawInput +... | inj₁ _ = nothing +... | inj₂ inputTrace = just (proof (isTrace? inputTrace))