Merge branch 'ana/flag-build-with-certifier' into certifier-update

Author: zeme-wana

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

@@ -50,6 +50,11 @@ common os-support
   if (impl(ghcjs) || os(windows))
     buildable: False
 
+flag certify
+  default:     False
+  manual:      True
+  description: Build with the Agda-based compiler certification tool.
+
 library
   import:          lang, ghc-version-support, os-support
   hs-source-dirs:  src
@@ -93,6 +98,13 @@ library
     , text
     , uniplate
 
+  if flag(certify)
+    build-depends:
+      , megaparsec
+      , plutus-metatheory  ^>=1.58
+
+    cpp-options:   -DCERTIFY
+
 executable gen-plugin-opts-doc
   import:           lang, ghc-version-support, os-support
   main-is:          GeneratePluginOptionsDoc.hs

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

@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 -- editorconfig-checker-disable-file
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -11,6 +12,7 @@
 
 module PlutusTx.Options where
 
+{- ORMOLU_DISABLE -}
 import PlutusCore.Error as PLC
 import PlutusCore.Parser as PLC
 import PlutusCore.Quote as PLC
@@ -44,6 +46,11 @@ import Prettyprinter
 import Text.Read (readMaybe)
 import Type.Reflection
 
+#ifdef CERTIFY
+import Text.Megaparsec.Char (alphaNumChar, char, upperChar)
+import Control.Applicative (many, optional, (<|>))
+#endif
+  
 data PluginOptions = PluginOptions
   { _posPlcTargetVersion :: PLC.Version
   , _posDoTypecheck :: Bool
@@ -82,6 +89,9 @@ data PluginOptions = PluginOptions
     -- Which effectively ignores the trace text.
     _posRemoveTrace :: Bool
   , _posDumpCompilationTrace :: Bool
+#ifdef CERTIFY
+  , _posCertify :: Maybe String
+#endif
   }
 
 makeLenses ''PluginOptions
@@ -314,6 +324,20 @@ pluginOptions =
     , let k = "dump-compilation-trace"
           desc = "Dump compilation trace for debugging"
        in (k, PluginOption typeRep (setTrue k) posDumpCompilationTrace desc [])
+#ifdef CERTIFY
+    , 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."
+          p =
+            optional $ do
+              firstC <- upperChar
+              rest <- many (alphaNumChar <|> char '_' <|> char '\\')
+              pure (firstC : rest)
+       in (k, PluginOption typeRep (plcParserOption p k) posCertify desc [])
+#endif
     ]
 
 flag :: (a -> a) -> OptionKey -> Maybe OptionValue -> Validation ParseError (a -> a)
@@ -387,6 +411,9 @@ defaultPluginOptions =
     , _posPreserveLogging = True
     , _posRemoveTrace = False
     , _posDumpCompilationTrace = False
+#ifdef CERTIFY
+    , _posCertify = Nothing
+#endif
     }
 
 processOne

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

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase #-}
@@ -12,6 +13,7 @@
 
 module PlutusTx.Plugin (plugin, plc) where
 
+{- ORMOLU_DISABLE -}
 import PlutusPrelude
 import PlutusTx.AsData.Internal qualified
 import PlutusTx.Bool ((&&), (||))
@@ -86,6 +88,11 @@ import Prettyprinter qualified as PP
 import System.IO (openBinaryTempFile)
 import System.IO.Unsafe (unsafePerformIO)
 
+#ifdef CERTIFY
+import Certifier (runCertifier, mkCertifier, prettyCertifierError, prettyCertifierSuccess)
+import System.IO (hPutStrLn, stderr)
+#endif
+
 data PluginCtx = PluginCtx
   { pcOpts :: PluginOptions
   , pcFamEnvs :: GHC.FamInstEnvs
@@ -637,7 +644,22 @@ runCompiler moduleName opts expr = do
       modifyError PLC.TypeErrorE $
         PLC.inferTypeOfProgram plcTcConfig (plcP $> annMayInline)
 
+#ifdef CERTIFY
+  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 ()
+#else
   (uplcP, _) <- flip runReaderT plcOpts $ PLC.compileProgramWithTrace plcP
+#endif
+
   dbP <- liftExcept $ modifyError PLC.FreeVariableErrorE $ traverseOf UPLC.progTerm UPLC.deBruijnTerm uplcP
   when (opts ^. posDumpUPlc) . liftIO $
     dumpFlat