Add verified compilation certification component

cabal.project

@@ -22,6 +22,7 @@ packages: cardano-constitution
           plutus-benchmark
           plutus-conformance
           plutus-core
+          plutus-executables
           plutus-ledger-api
           plutus-metatheory
           plutus-tx

plutus-core/executables/plutus/AnyProgram/Compile.hs

@@ -31,8 +31,10 @@ import Control.Lens hiding ((%~))
 import Control.Monad.Error.Lens
 import Control.Monad.Except
 import Control.Monad.Reader
+import Control.Monad.State (StateT (runStateT))
 import Data.Singletons.Decide
 import Data.Text
+import PlutusCore.Compiler.Types (initUPLCSimplifierTrace)
 import PlutusPrelude hiding ((%~))
 
 -- Note that we use for erroring the original term's annotation
@@ -111,7 +113,7 @@ compileProgram = curry $ \case
             -- first self-"compile" to plc (just for reusing code)
             compileProgram sng1 (SPlc n2 a2)
         -- PLC.compileProgram subsumes uplcOptimise
-        >=> (PLC.runQuoteT . flip runReaderT PLC.defaultCompilationOpts .
+        >=> (PLC.runQuoteT . PLC.evalCompile PLC.defaultCompilationOpts .
                 plcToUplcViaName n2 PLC.compileProgram)
         >=> pure . UPLC.UnrestrictedProgram
 
@@ -213,7 +215,10 @@ plcTypecheck sngN sngA p = PLC.runQuoteT $ do
     tcConfig <- withA @Monoid sngA $ PLC.getDefTypeCheckConfig mempty
     void $ plcToName sngN (PLC.inferTypeOfProgram tcConfig) p
 
-uplcOptimise :: (?opts :: Opts, PLC.AsFreeVariableError e, MonadError e m)
+uplcOptimise :: (?opts :: Opts
+                , PLC.AsFreeVariableError e
+                , MonadError e m
+                )
              => SNaming n1
              -> UPLC.UnrestrictedProgram (FromName n1) DefaultUni DefaultFun a
              -> m (UPLC.UnrestrictedProgram (FromName n1) DefaultUni DefaultFun a)
@@ -225,7 +230,8 @@ uplcOptimise =
                                 case safeOrUnsafe of
                                   SafeOptimise   -> set UPLC.soConservativeOpts True
                                   UnsafeOptimise -> id
-                in fmap PLC.runQuoteT
+                in (fmap . fmap) fst
+                   . fmap (PLC.runQuoteT . flip runStateT initUPLCSimplifierTrace)
                    . _Wrapped
                    . uplcViaName (UPLC.simplifyProgram sOpts def)
 

plutus-core/executables/src/PlutusCore/Executable/Parsers.hs

@@ -114,14 +114,28 @@ nameformat =
    <> short 'j'
    <> help "Output evaluation result with de Bruijn indices (default: show textual names)")
 
+certifier :: Parser Certifier
+certifier =
+  optional
+  $ strOption
+    (long "certify"
+    <> help
+        ("[EXPERIMENTAL] Produce a certificate ARG.agda proving that the program"
+        <> " transformaton is correct; the certificate is an Agda proof object, which"
+        <> " can be checked using the Agda proof assistant"
+        )
+    )
+
 printOpts :: Parser PrintOptions
 printOpts = PrintOptions <$> input <*> output <*> printmode
 
 convertOpts :: Parser ConvertOptions
 convertOpts = ConvertOptions <$> input <*> inputformat <*> output <*> outputformat <*> printmode
 
 optimiseOpts :: Parser OptimiseOptions
-optimiseOpts = OptimiseOptions <$> input <*> inputformat <*> output <*> outputformat <*> printmode
+optimiseOpts =
+  OptimiseOptions
+  <$> input <*> inputformat <*> output <*> outputformat <*> printmode <*> certifier
 
 exampleMode :: Parser ExampleMode
 exampleMode = exampleAvailable <|> exampleSingle

plutus-core/executables/src/PlutusCore/Executable/Types.hs

@@ -72,8 +72,10 @@ instance Show Format where
     show (Flat DeBruijn)      = "flat-deBruijn"
     show (Flat NamedDeBruijn) = "flat-namedDeBruijn"
 
+type Certifier = Maybe String
+
 data ConvertOptions = ConvertOptions Input Format Output Format PrintMode
-data OptimiseOptions = OptimiseOptions Input Format Output Format PrintMode
+data OptimiseOptions = OptimiseOptions Input Format Output Format PrintMode Certifier
 data PrintOptions = PrintOptions Input Output PrintMode
 newtype ExampleOptions = ExampleOptions ExampleMode
 data ApplyOptions = ApplyOptions Files Format Output Format PrintMode

plutus-core/plutus-core.cabal

@@ -463,35 +463,6 @@ test-suite untyped-plutus-core-test
     , text
     , vector
 
-executable plc
-  import:         lang
-  main-is:        plc/Main.hs
-  hs-source-dirs: executables
-  build-depends:
-    , base                                            >=4.9   && <5
-    , bytestring
-    , flat                                            ^>=0.6
-    , optparse-applicative
-    , plutus-core:{plutus-core, plutus-core-execlib}  ^>=1.32
-
-executable uplc
-  import:         lang
-  main-is:        uplc/Main.hs
-  hs-source-dirs: executables
-  build-depends:
-    , base                                            >=4.9   && <5
-    , bytestring
-    , criterion
-    , deepseq
-    , flat                                            ^>=0.6
-    , haskeline
-    , mtl
-    , optparse-applicative
-    , plutus-core:{plutus-core, plutus-core-execlib}  ^>=1.32
-    , prettyprinter
-    , split
-    , text
-
 ----------------------------------------------
 -- plutus-ir
 ----------------------------------------------
@@ -663,22 +634,6 @@ test-suite plutus-ir-test
     , text
     , unordered-containers
 
-executable pir
-  import:         lang
-  main-is:        pir/Main.hs
-  hs-source-dirs: executables
-  build-depends:
-    , base                                                       >=4.9   && <5
-    , bytestring
-    , cassava
-    , containers
-    , lens
-    , megaparsec
-    , optparse-applicative
-    , plutus-core:{plutus-core, plutus-core-execlib, plutus-ir}  ^>=1.32
-    , text
-    , transformers
-
 executable plutus
   import:             lang
   main-is:            Main.hs

plutus-core/plutus-core/src/PlutusCore/Compiler.hs

@@ -2,9 +2,12 @@ module PlutusCore.Compiler
   ( module Opts
   , compileTerm
   , compileProgram
+  , runCompile
+  , evalCompile
   ) where
 
 import PlutusCore.Compiler.Erase
+import PlutusCore.Compiler.Opts as Opts
 import PlutusCore.Compiler.Types
 import PlutusCore.Core
 import PlutusCore.Name.Unique
@@ -13,12 +16,15 @@ import UntypedPlutusCore.Core.Type qualified as UPLC
 import UntypedPlutusCore.Simplify qualified as UPLC
 
 import Control.Lens (view)
-import Control.Monad.Reader (MonadReader)
-import PlutusCore.Compiler.Opts as Opts
+import Control.Monad.Reader (MonadReader, ReaderT (runReaderT))
+import Control.Monad.State (MonadState (..), StateT (runStateT))
 
 -- | Compile a PLC term to UPLC, and optimize it.
 compileTerm
-  :: (Compiling m uni fun name a, MonadReader (CompilationOpts name fun a) m)
+  :: (Compiling m uni fun name a
+  , MonadReader (CompilationOpts name fun a) m
+  , MonadState (UPLCSimplifierTrace name uni fun a) m
+  )
   => Term tyname name uni fun a
   -> m (UPLC.Term name uni fun a)
 compileTerm t = do
@@ -30,7 +36,33 @@ compileTerm t = do
 
 -- | Compile a PLC program to UPLC, and optimize it.
 compileProgram
-  :: (Compiling m uni fun name a, MonadReader (CompilationOpts name fun a) m)
+  :: (Compiling m uni fun name a
+  , MonadReader (CompilationOpts name fun a) m
+  , MonadState (UPLCSimplifierTrace name uni fun a) m
+  )
   => Program tyname name uni fun a
   -> m (UPLC.Program name uni fun a)
 compileProgram (Program a v t) = UPLC.Program a v <$> compileTerm t
+
+type Compile m name uni fun a =
+  ReaderT
+    (CompilationOpts name fun a)
+    (StateT
+       (UPLCSimplifierTrace name uni fun a)
+       m
+    )
+
+runCompile
+  :: CompilationOpts name fun a
+  -> Compile m name uni fun a b
+  -> m (b, UPLCSimplifierTrace name uni fun a)
+runCompile opts =
+  flip runStateT initUPLCSimplifierTrace
+  . flip runReaderT opts
+
+evalCompile
+  :: Functor m
+  => CompilationOpts name fun a
+  -> Compile m name uni fun a b
+  -> m b
+evalCompile opts = fmap fst . runCompile opts

plutus-core/plutus-core/src/PlutusCore/Compiler/Types.hs

@@ -2,11 +2,24 @@
 
 module PlutusCore.Compiler.Types where
 
+import Data.Hashable
 import PlutusCore.Builtin
+import PlutusCore.Default qualified as PLC
 import PlutusCore.Name.Unique
 import PlutusCore.Quote
+import UntypedPlutusCore.Core.Type qualified as UPLC
 
-import Data.Hashable
+-- TODO1: move somewhere more appropriate?
+-- TODO2: we probably don't want this in memory so after MVP
+-- we should consider serializing this to disk
+newtype UPLCSimplifierTrace name uni fun a =
+  UPLCSimplifierTrace
+    { uplcSimplifierTrace
+      :: [UPLC.Term name uni PLC.DefaultFun a]
+    }
+
+initUPLCSimplifierTrace :: UPLCSimplifierTrace name uni fun a
+initUPLCSimplifierTrace = UPLCSimplifierTrace []
 
 type Compiling m uni fun name a =
   ( ToBuiltinMeaning uni fun

plutus-core/plutus-ir/test/PlutusIR/Transform/StrictLetRec/Tests/Lib.hs

@@ -75,7 +75,7 @@ compileTplcProgramOrFail
 compileTplcProgramOrFail plcProgram =
   handlePirErrorByFailing @SrcSpan =<< do
     TPLC.compileProgram plcProgram
-      & flip runReaderT TPLC.defaultCompilationOpts
+      & TPLC.evalCompile TPLC.defaultCompilationOpts
       & runQuoteT
       & runExceptT
 

plutus-core/testlib/PlutusCore/Test.hs

@@ -193,7 +193,7 @@ instance
   toUPlc =
     pure
       . TPLC.runQuote
-      . flip runReaderT TPLC.defaultCompilationOpts
+      . TPLC.evalCompile TPLC.defaultCompilationOpts
       . TPLC.compileProgram
 
 instance ToUPlc (UPLC.Program UPLC.NamedDeBruijn uni fun ()) uni fun where

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Simplify.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE GADTs            #-}
+{-# LANGUAGE RankNTypes       #-}
 {-# LANGUAGE TypeApplications #-}
 
 module UntypedPlutusCore.Simplify (
@@ -22,12 +23,16 @@ import UntypedPlutusCore.Transform.ForceDelay (forceDelay)
 import UntypedPlutusCore.Transform.Inline (InlineHints (..), inline)
 
 import Control.Monad
+import Control.Monad.State.Class (MonadState)
+import Control.Monad.State.Class qualified as State
 import Data.List as List (foldl')
 import Data.Typeable
 
 simplifyProgram ::
     forall name uni fun m a.
-    (Compiling m uni fun name a) =>
+    (Compiling m uni fun name a
+    , MonadState (UPLCSimplifierTrace name uni fun a) m
+    ) =>
     SimplifyOpts name a ->
     BuiltinSemanticsVariant fun ->
     Program name uni fun a ->
@@ -37,7 +42,9 @@ simplifyProgram opts builtinSemanticsVariant (Program a v t) =
 
 simplifyTerm ::
     forall name uni fun m a.
-    (Compiling m uni fun name a) =>
+    ( Compiling m uni fun name a
+    , MonadState (UPLCSimplifierTrace name uni fun a) m
+    ) =>
     SimplifyOpts name a ->
     BuiltinSemanticsVariant fun ->
     Term name uni fun a ->
@@ -57,11 +64,17 @@ simplifyTerm opts builtinSemanticsVariant =
     -- generate simplification step
     simplifyStep :: Int -> Term name uni fun a -> m (Term name uni fun a)
     simplifyStep _ =
-      floatDelay
+      traceAST
+        >=> floatDelay
+        >=> traceAST
         >=> pure . forceDelay
+        >=> traceAST
         >=> pure . caseOfCase'
+        >=> traceAST
         >=> pure . caseReduce
+        >=> traceAST
         >=> inline (_soInlineConstants opts) (_soInlineHints opts) builtinSemanticsVariant
+        >=> traceAST
 
     caseOfCase' :: Term name uni fun a -> Term name uni fun a
     caseOfCase' = case eqT @fun @DefaultFun of
@@ -74,4 +87,11 @@ simplifyTerm opts builtinSemanticsVariant =
         (Just Refl, Just Refl) -> cse builtinSemanticsVariant
         _                      -> pure
 
+    traceAST ast =
+      case eqT @fun @DefaultFun of
+        Just Refl -> do
+          State.modify' (\st -> st { uplcSimplifierTrace = uplcSimplifierTrace st ++ [ast] })
+          return ast
+        Nothing -> return ast
+
     cseTimes = if _soConservativeOpts opts then 0 else _soMaxCseIterations opts

plutus-core/untyped-plutus-core/test/Transform/Simplify/Lib.hs

@@ -3,10 +3,12 @@
 module Transform.Simplify.Lib where
 
 import Control.Lens ((&), (.~))
+import Control.Monad.State (evalStateT)
 import Data.ByteString.Lazy qualified as BSL
 import Data.Text.Encoding (encodeUtf8)
 import PlutusCore qualified as PLC
 import PlutusCore.Builtin (BuiltinSemanticsVariant)
+import PlutusCore.Compiler.Types (initUPLCSimplifierTrace)
 import PlutusCore.Pretty (PrettyPlc, Render (render), prettyPlcReadableSimple)
 import PlutusPrelude (Default (def))
 import Test.Tasty (TestTree)
@@ -25,6 +27,7 @@ goldenVsSimplified :: String -> Term Name PLC.DefaultUni PLC.DefaultFun () -> Te
 goldenVsSimplified name =
   goldenVsPretty ".uplc.golden" name
     . PLC.runQuote
+    . flip evalStateT initUPLCSimplifierTrace
     . simplifyTerm
       ( defaultSimplifyOpts
           -- Just run one iteration, to see what that does
@@ -37,6 +40,7 @@ goldenVsCse :: String -> Term Name PLC.DefaultUni PLC.DefaultFun () -> TestTree
 goldenVsCse name =
   goldenVsPretty ".uplc.golden" name
     . PLC.runQuote
+    . flip evalStateT initUPLCSimplifierTrace
     . simplifyTerm
       ( defaultSimplifyOpts
           -- Just run one iteration, to see what that does

plutus-executables/CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for plutus-executables
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.