From d8d411af212ca1ca97983369163d3fd997cbc3e4 Mon Sep 17 00:00:00 2001 From: Ana Pantilie Date: Tue, 29 Oct 2024 14:41:59 +0200 Subject: [PATCH] Clean-up --- plutus-executables/executables/uplc/Main.hs | 211 +++--------------- plutus-executables/plutus-executables.cabal | 22 +- plutus-executables/src/AgdaUnparse.hs | 135 +++++++++++ .../src/{Test.agda => Certifier.agda} | 4 +- .../src/VerifiedCompilation.lagda.md | 4 +- 5 files changed, 197 insertions(+), 179 deletions(-) create mode 100644 plutus-executables/src/AgdaUnparse.hs rename plutus-metatheory/src/{Test.agda => Certifier.agda} (77%) diff --git a/plutus-executables/executables/uplc/Main.hs b/plutus-executables/executables/uplc/Main.hs index 5b18ceabaa8..3d3a5f19b1e 100644 --- a/plutus-executables/executables/uplc/Main.hs +++ b/plutus-executables/executables/uplc/Main.hs @@ -1,21 +1,13 @@ -- editorconfig-checker-disable -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE GADTs #-} -{-# 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 import PlutusCore.Annotation (SrcSpan) import PlutusCore.Data (Data) -import PlutusCore.Default (BuiltinSemanticsVariant (..), DSum (..)) +import PlutusCore.Default (BuiltinSemanticsVariant (..)) import PlutusCore.Evaluation.Machine.ExBudget (ExBudget (..), ExRestrictingBudget (..)) import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as PLC import PlutusCore.Evaluation.Machine.ExMemory (ExCPU (..), ExMemory (..)) @@ -25,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 @@ -44,7 +35,6 @@ import Criterion.Main (defaultConfig) import Criterion.Types (Config (..)) import Data.ByteString.Lazy as BSL (readFile) import Data.Foldable -import Data.Functor.Identity import Data.List.Split (splitOn) import Data.Text qualified as T import Flat (unflat) @@ -61,39 +51,17 @@ 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, optLibraries, optLocalInterfaces), - defaultOptions) -import Agda.Syntax.Abstract qualified as HAgda.Abstract -import Agda.Syntax.Abstract qualified as HAgda.Concrete -import Agda.Syntax.Common.Pretty qualified as HAgda.Pretty +import Agda.Interaction.Options (CommandLineOptions (optIncludePaths), defaultOptions) import Agda.Syntax.Parser qualified as HAgda.Parser -import Agda.TypeChecking.Monad.Base (Interface (iModuleName), TCM) -import Agda.Compiler.Backend (Interface (iImportedModules, iModuleName), crInterface, getScope, - getTCState, iInsideScope, iScope, setCommandLineOptions, setScope, - stScope) +import Agda.Compiler.Backend (crInterface, iInsideScope, setCommandLineOptions, setScope) import Agda.Interaction.BasicOps (evalInCurrent) import Agda.Main (runTCMPrettyErrors) -import Agda.Syntax.Concrete.Pretty qualified as Concrete -import Agda.Syntax.Scope.Base (AbstractModule, AbstractName, ThingsInScope, allNamesInScope) -import Agda.Syntax.Scope.Monad (getCurrentScope, setCurrentModule) -import Agda.Syntax.Translation.AbstractToConcrete (ToConcrete (toConcrete)) import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract)) import Agda.TypeChecking.Pretty (PrettyTCM (..)) import Agda.Utils.FileName qualified as HAgda.File -import Agda.Utils.Maybe (fromJust) -import Data.ByteString (ByteString) -import Data.List (isInfixOf, isSuffixOf) -import Data.Map.Strict qualified as Map -import Data.Text (Text) +import AgdaUnparse (agdaUnparse) import Data.Text qualified as Text -import Data.Traversable (forM) -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 qualified as Data -import PlutusCore.Default qualified as PLC -import PlutusPrelude qualified as UPLC import System.Environment (getEnv) uplcHelpText :: String @@ -313,18 +281,35 @@ 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 - runAgda certName rawAgdaTrace - runCertifier Nothing _ = pure () - -runAgda :: String -> [(SimplifierStage, (AgdaFFI.UTerm, AgdaFFI.UTerm))] -> IO () + +---------------- 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 @@ -334,15 +319,13 @@ runAgda certName rawTrace = do Left err -> error $ show err stdlibPath <- getEnv "AGDA_STDLIB_SRC" metatheoryPath <- getEnv "PLUTUS_METHATHEORY_SRC" - print stdlibPath - print metatheoryPath - let inputFile = HAgda.File.AbsolutePath (Text.pack $ metatheoryPath "Test.agda") -- "/home/ana/Workspace/IOG/plutus/plutus-metatheory/src/Test.agda" + let inputFile = HAgda.File.AbsolutePath (Text.pack $ metatheoryPath "Certifier.agda") runTCMPrettyErrors $ do let opts = defaultOptions { optIncludePaths = - [ metatheoryPath -- "/home/ana/Workspace/IOG/plutus/plutus-metatheory/src" - , stdlibPath -- "/nix/store/g9vi7hzrp1cqgm21355549yyqcpkjnxx-standard-library-1.7.3/src" + [ metatheoryPath + , stdlibPath ] } setCommandLineOptions opts @@ -351,130 +334,10 @@ runAgda certName rawTrace = do insideScope = iInsideScope interface setScope insideScope internalisedTrace <- toAbstract parsedTrace - intermediate <- prettyTCM internalisedTrace - -- liftIO $ writeFile (certName ++ ".agda") (show intermediate) decisionProcedureResult <- evalInCurrent DefaultCompute internalisedTrace final <- prettyTCM decisionProcedureResult liftIO $ writeFile (certName ++ ".agda") (show final) -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 - -class AgdaUnparse a where - agdaUnparse :: a -> String - -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 -- 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 "BUG: 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 - ---------------- Script application ---------------- -- | Apply one script to a list of others and output the result. All of the diff --git a/plutus-executables/plutus-executables.cabal b/plutus-executables/plutus-executables.cabal index 71e64564ea2..f43b99ba852 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 @@ -88,7 +108,6 @@ executable uplc , Agda ==2.6.4 , base >=4.9 && <5 , bytestring - , containers , criterion , deepseq , filepath @@ -98,6 +117,7 @@ executable uplc , optparse-applicative , plutus-core ^>=1.36 , plutus-core:plutus-core-execlib + , plutus-executables:lib , plutus-metatheory , prettyprinter , split 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/Test.agda b/plutus-metatheory/src/Certifier.agda similarity index 77% rename from plutus-metatheory/src/Test.agda rename to plutus-metatheory/src/Certifier.agda index 41ba5f5f26d..e4d5922985d 100644 --- a/plutus-metatheory/src/Test.agda +++ b/plutus-metatheory/src/Certifier.agda @@ -1,4 +1,6 @@ -module Test where +-- Do not edit without also changing AgdaUnparse in plutus-executables. + +module Certifier where open import VerifiedCompilation open import Untyped diff --git a/plutus-metatheory/src/VerifiedCompilation.lagda.md b/plutus-metatheory/src/VerifiedCompilation.lagda.md index 04dbc85c08a..bfdc7c37124 100644 --- a/plutus-metatheory/src/VerifiedCompilation.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation.lagda.md @@ -140,9 +140,7 @@ isTrace? ((tag , x₁ , x₂) ∷ xs) with isTrace? xs ## 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. ```