[DON'T MERGE] UPLC 2025 certifier demo

plutus-metatheory/src/Certifier.hs

@@ -21,13 +21,16 @@ import System.FilePath ((</>))
 
 import FFI.AgdaUnparse (AgdaUnparse (..))
 import FFI.SimplifierTrace (mkFfiSimplifierTrace)
-import FFI.Untyped (UTerm)
+import FFI.Untyped (UTerm, uconv)
 
+import PlutusCore.Pretty (prettyPlcReadableSimple)
 import UntypedPlutusCore qualified as UPLC
 import UntypedPlutusCore.Transform.Simplifier
 
 import MAlonzo.Code.VerifiedCompilation (runCertifierMain)
 
+import Debug.Trace (trace)
+
 type CertName = String
 type CertDir = String
 
@@ -100,11 +103,13 @@ data TermWithId = TermWithId
   { termId :: Int
   , term   :: UTerm
   }
+  deriving stock Show
 
 data Ast = Ast
   { equivClass    :: EquivClass
   , astTermWithId :: TermWithId
   }
+  deriving stock Show
 
 getTermId :: Ast -> Int
 getTermId Ast {astTermWithId = TermWithId {termId} } = termId
@@ -194,11 +199,12 @@ mkAgdaAstFile ast =
       agdaIdStr = "ast" <> show agdaId
       agdaAstTy = agdaIdStr <> " : Untyped"
       agdaAstDef = agdaIdStr <> " = " <> agdaAst
+      uplcAst = show . prettyPlcReadableSimple . uconv 0 . term . astTermWithId $ ast
       agdaAstFile = agdaModuleName <> ".agda"
-   in (agdaAstFile, mkAstModule agdaModuleName agdaAstTy agdaAstDef)
+   in (agdaAstFile, mkAstModule agdaModuleName agdaAstTy agdaAstDef uplcAst)
 
-mkAstModule :: String -> String -> String -> String
-mkAstModule agdaIdStr agdaAstTy agdaAstDef =
+mkAstModule :: String -> String -> String -> String -> String
+mkAstModule agdaIdStr agdaAstTy agdaAstDef uplcAst =
   "module " <> agdaIdStr <> " where\
   \\n\
   \\nopen import VerifiedCompilation\
@@ -218,6 +224,8 @@ mkAstModule agdaIdStr agdaAstTy agdaAstDef =
   \\nopen import Data.Bool.Base using (Bool; false; true)\
   \\nopen import Agda.Builtin.Equality using (_≡_; refl)\
   \\n\
+  \\n{-\n" <> uplcAst <> "\n-}\n\
+  \\n\
   \\n" <> agdaAstTy <> "\n\
   \\n" <> agdaAstDef <> "\n"
 

plutus-metatheory/src/FFI/Untyped.hs

@@ -10,6 +10,8 @@ import UntypedPlutusCore
 import Data.Text as T hiding (map)
 import GHC.Exts (IsList (..))
 
+import Debug.Trace (trace)
+
 -- Untyped (Raw) syntax
 
 data UTerm = UVar Integer
@@ -42,18 +44,18 @@ conv (Force _ t)     = UForce (conv t)
 conv (Constr _ i es) = UConstr (toInteger i) (toList (fmap conv es))
 conv (Case _ arg cs) = UCase (conv arg) (toList (fmap conv cs))
 
-tmnames :: String
-tmnames = ['a' .. 'z']
+tmnames :: [String]
+tmnames = fmap (\n -> 'x' : show n) [0..] -- ['a' .. 'z']
 
 uconv ::  Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
 uconv i (UVar x)     = Var
   ()
-  (NamedDeBruijn (T.pack [tmnames !! (i - 1 - fromInteger x)])
+  (NamedDeBruijn (T.pack (tmnames !! (i - 1 - fromInteger x)))
                 -- PLC's debruijn starts counting from 1, while in the metatheory it starts from 0.
                  (Index (fromInteger x + 1)))
 uconv i (ULambda t)  = LamAbs
   ()
-  (NamedDeBruijn (T.pack [tmnames !! i]) deBruijnInitIndex)
+  (NamedDeBruijn (T.pack (tmnames !! i)) deBruijnInitIndex)
   (uconv (i+1) t)
 uconv i (UApp t u)     = Apply () (uconv i t) (uconv i u)
 uconv _ (UCon c)       = Constant () c

plutus-metatheory/src/VerifiedCompilation.lagda.md

@@ -76,7 +76,8 @@ which produces a `Trace` always produces a correct one, although it might be use
 ```
 
 data Transformation : SimplifierTag → Relation where
-  isCoC : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UCC.CaseOfCase ast ast' → Transformation SimplifierTag.caseOfCaseT ast ast'
+  -- FIXME: CaseOfCase has suffered some changes and the certifier has not been updated yet
+  cocNotImplemented : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → Transformation SimplifierTag.caseOfCaseT ast ast'
   isFD : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UFD.ForceDelay ast ast' → Transformation SimplifierTag.forceDelayT ast ast'
   isFlD : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UFlD.FloatDelay ast ast' → Transformation SimplifierTag.floatDelayT ast ast'
   isCSE : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UCSE.UntypedCSE ast ast' → Transformation SimplifierTag.cseT ast ast'
@@ -104,9 +105,7 @@ isTransformation? tag ast ast' | SimplifierTag.forceDelayT with UFD.isForceDelay
 ... | ce ¬p t b a = ce (λ { (isFD x) → ¬p x}) t b a
 ... | proof p = proof (isFD p)
 isTransformation? tag ast ast' | SimplifierTag.forceCaseDelayT = proof forceCaseDelayNotImplemented
-isTransformation? tag ast ast' | SimplifierTag.caseOfCaseT with UCC.isCaseOfCase? ast ast'
-... | ce ¬p t b a = ce (λ { (isCoC x) → ¬p x}) t b a
-... | proof p = proof (isCoC p)
+isTransformation? tag ast ast' | SimplifierTag.caseOfCaseT = proof cocNotImplemented
 isTransformation? tag ast ast' | SimplifierTag.caseReduceT with UCR.isCaseReduce? ast ast'
 ... | ce ¬p t b a = ce (λ { (isCaseReduce x) → ¬p x}) t b a
 ... | proof p = proof (isCaseReduce p)
@@ -186,8 +185,11 @@ getCE (just (cert (ce _ {X} {X'} t b a))) = just (X , X' , t , b , a)
 open import Data.Bool.Base using (Bool; false; true)
 open import Agda.Builtin.Equality using (_≡_; refl)
 
+postulate
+  tr : {X X' : Set} → SimplifierTag → X → X' → Bool → Bool
+
 passed? : Maybe Cert → Bool
-passed? (just (cert (ce _ _ _ _))) = false
+passed? (just (cert (ce p t x1 x2))) = false
 passed? (just (cert (proof _))) = true
 passed? nothing = false
 

plutus-tx-plugin/plutus-tx-plugin.cabal

@@ -82,10 +82,12 @@ library
     , extra
     , ghc
     , lens
+    , megaparsec
     , mtl
     , plutus-core            ^>=1.54
     , plutus-core:flat
     , plutus-core:plutus-ir
+    , plutus-metatheory      ^>=1.54
     , plutus-tx              ^>=1.54
     , prettyprinter
     , template-haskell

plutus-tx-plugin/src/PlutusTx/Options.hs

@@ -19,6 +19,7 @@ import PlutusIR.Compiler.Types qualified as PIR
 import PlutusTx.Compiler.Types
 import UntypedPlutusCore qualified as UPLC
 
+import Control.Applicative (many, optional, (<|>))
 import Control.Exception
 import Control.Lens
 import Data.Bifunctor (first)
@@ -35,6 +36,7 @@ import Data.Text qualified as Text
 import Data.Type.Equality
 import GHC.Plugins qualified as GHC
 import Prettyprinter
+import Text.Megaparsec.Char (alphaNumChar, char, upperChar)
 
 import Text.Read (readMaybe)
 import Type.Reflection
@@ -76,6 +78,7 @@ data PluginOptions = PluginOptions
     -- Which effectively ignores the trace text.
     _posRemoveTrace                    :: Bool
   , _posDumpCompilationTrace           :: Bool
+  , _posCertify                        :: Maybe String
   }
 
 makeLenses ''PluginOptions
@@ -307,6 +310,18 @@ pluginOptions =
     , let k = "dump-compilation-trace"
           desc = "Dump compilation trace for debugging"
        in (k, PluginOption typeRep (setTrue k) posDumpCompilationTrace desc [])
+    , let k = "certify"
+          desc =
+            "Produce a certificate for the compiled program, with the given name. "
+              <> "This certificate provides evidence that the compiler optimizations have "
+              <> "preserved the functional behavior of the original program. "
+              <> "Currently, this is only supported for the UPLC compilation pipeline. "
+              <> "Warning: this is an experimental feature and may not work as expected."
+          p = optional $ do
+            firstC <- upperChar
+            rest <- many (alphaNumChar <|> char '_' <|> char '\\')
+            pure (firstC : rest)
+       in (k, PluginOption typeRep (plcParserOption p k) posCertify desc [])
     ]
 
 flag :: (a -> a) -> OptionKey -> Maybe OptionValue -> Validation ParseError (a -> a)
@@ -379,6 +394,7 @@ defaultPluginOptions =
     , _posPreserveLogging = True
     , _posRemoveTrace = False
     , _posDumpCompilationTrace = False
+    , _posCertify = Nothing
     }
 
 processOne

plutus-tx-plugin/src/PlutusTx/Plugin.hs

@@ -83,9 +83,11 @@ import PlutusIR.Compiler.Types qualified as PIR
 import PlutusIR.Transform.RewriteRules
 import PlutusIR.Transform.RewriteRules.RemoveTrace (rewriteRuleRemoveTrace)
 import Prettyprinter qualified as PP
-import System.IO (openBinaryTempFile)
+import System.IO (hPutStrLn, openBinaryTempFile, stderr)
 import System.IO.Unsafe (unsafePerformIO)
 
+import Certifier
+
 data PluginCtx = PluginCtx
   { pcOpts            :: PluginOptions
   , pcFamEnvs         :: GHC.FamInstEnvs
@@ -636,7 +638,17 @@ runCompiler moduleName opts expr = do
         modifyError PLC.TypeErrorE $
           PLC.inferTypeOfProgram plcTcConfig (plcP $> annMayInline)
 
-  (uplcP, _) <- flip runReaderT plcOpts $ PLC.compileProgramWithTrace plcP
+  let optCertify = opts ^. posCertify
+  (uplcP, simplTrace) <- flip runReaderT plcOpts $ PLC.compileProgramWithTrace plcP
+  liftIO $ case optCertify of
+      Just certName -> do
+          result <- runCertifier $ mkCertifier simplTrace certName
+          case result of
+              Right certSuccess ->
+                  hPutStrLn stderr $ prettyCertifierSuccess certSuccess
+              Left err ->
+                 hPutStrLn stderr $ prettyCertifierError err
+      Nothing -> pure ()
   dbP <- liftExcept $ modifyError PLC.FreeVariableErrorE $ traverseOf UPLC.progTerm UPLC.deBruijnTerm uplcP
   when (opts ^. posDumpUPlc) . liftIO $
       dumpFlat