Add certifier golden testing framework

plutus-executables/executables/uplc/Main.hs

@@ -61,7 +61,6 @@ 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
@@ -319,7 +318,7 @@ runAgda certName rawTrace = do
           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")
+  inputFile <- HAgda.File.absolute (metatheoryPath </> "Certifier.agda")
   runTCMPrettyErrors $ do
     let opts =
           defaultOptions
@@ -336,7 +335,7 @@ runAgda certName rawTrace = do
     internalisedTrace <- toAbstract parsedTrace
     decisionProcedureResult <- evalInCurrent DefaultCompute internalisedTrace
     final <- prettyTCM decisionProcedureResult
-    liftIO $ writeFile (certName ++ ".agda") (show final)
+    liftIO $ writeFile certName (show final)
 
 ---------------- Script application ----------------
 

plutus-executables/plutus-executables.cabal

@@ -157,3 +157,18 @@ test-suite test-detailed
   build-tool-depends:
     , plutus-executables:plc
     , plutus-executables:uplc
+
+test-suite test-certifier
+  import:             lang, os-support
+  type:               exitcode-stdio-1.0
+  main-is:            Spec.hs
+  hs-source-dirs:     test/certifier
+  build-depends:
+    , base
+    , directory
+    , filepath
+    , process
+    , tasty
+    , tasty-golden
+
+  build-tool-depends: plutus-executables:uplc

plutus-executables/test/certifier/Spec.hs

@@ -0,0 +1,45 @@
+module Main (main) where
+
+import Control.Monad (void)
+import System.Directory (withCurrentDirectory)
+import System.FilePath (dropExtensions, (<.>), (</>))
+import System.Process (readProcess)
+import Test.Tasty (TestTree, defaultMain, testGroup)
+import Test.Tasty.Golden (findByExtension, goldenVsFile)
+
+path :: String
+path = "test/certifier"
+
+package :: String
+package = "plutus-executables"
+
+mkTestCase :: FilePath -> TestTree
+mkTestCase input =
+    let expectedCert = dropExtensions input <.> "out" <.> "golden"
+        actualCert = dropExtensions input <.> "out"
+    in goldenVsFile input expectedCert actualCert (mkTest input actualCert)
+
+mkTest :: FilePath -> FilePath -> IO ()
+mkTest input testName = do
+    -- This is a hack which is necessary because we rely on the
+    -- PLUTUS_METHATHEORY_SRC environment variable
+    withCurrentDirectory ".."
+        $ void
+        $ readProcess
+            "uplc"
+            [ "optimise"
+            , "-i"
+            , package </> input
+            , "--certify"
+            , package </> testName
+            ]
+            ""
+
+main :: IO ()
+main = do
+    uplcFiles <- findByExtension [".uplc"] path
+    defaultMain
+        $ testGroup "certifier"
+        $ mkTestCase
+        <$> uplcFiles
+