Add Agda certifier integration with source location tracking

.github/workflows/plinth-certifier-tests.yml

@@ -0,0 +1,46 @@
+# This workflow builds all packages with Agda certification enabled,
+# then type-checks each generated certificate to verify that compiler
+# optimizations preserve program semantics.
+#
+# Runs daily at 02:00 UTC and can be triggered manually.
+
+name: "Plinth Certifier Tests"
+
+on:
+  schedule:
+    - cron: "0 2 * * *"
+
+  workflow_dispatch:
+
+jobs:
+  certify:
+    name: Build and verify Agda certificates
+    runs-on: [self-hosted, plutus-runner]
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v6.0.1
+
+      - name: Run certifier tests
+        run: |
+          nix develop --no-warn-dirty --accept-flake-config --command \
+            python3 scripts/plinth-certifier-tests.py run -o agda-certificates
+
+      - name: Upload results
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: certifier-results
+          path: agda-certificates/__results__.txt
+          if-no-files-found: warn
+
+      - name: Upload certificate logs
+        if: failure()
+        uses: actions/upload-artifact@v4
+        with:
+          name: certifier-logs
+          path: |
+            agda-certificates/**/plinth-certifier-FAIL.txt
+            agda-certificates/**/agda-check-FAIL.log
+          if-no-files-found: warn

.gitignore

@@ -83,6 +83,7 @@ act-event.json
 .history/
 .virtualenv
 .vscode/
+.claude/
 .hsenv
 TAGS
 .DS_Store

plutus-executables/executables/uplc/Main.hs

@@ -358,7 +358,7 @@ runOptimisations (OptimiseOptions inp ifmt outp ofmt mode mcert certifierOutput)
         Left err -> do
           putStrLn $ prettyCertifierError err
           case err of
-            InvalidCertificate _ -> exitWith $ ExitFailure 1
+            InvalidCertificate _ _ -> exitWith $ ExitFailure 1
             InvalidCompilerOutput -> exitWith $ ExitFailure 2
             ValidationError _ -> exitWith $ ExitFailure 3
         -- TODO: Only Right True is success

plutus-metatheory/changelog.d/20260311_120000_agda_certifier_improvements.md

@@ -0,0 +1,7 @@
+### Changed
+
+- `InvalidCertificate` error now includes the certifier report text for better
+  diagnostics.
+- Use `createDirectoryIfMissing` instead of `createDirectory` to avoid failures
+  when certificate directories already exist.
+- Removed noisy console output from `runCertifier` (result and path messages).

plutus-metatheory/src/Certifier.hs

@@ -15,8 +15,9 @@ import Data.Foldable
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.List.NonEmpty qualified as NE
 import Data.Maybe (fromMaybe)
+import Data.Text qualified as Text
 import Data.Text.IO qualified as T
-import System.Directory (createDirectory)
+import System.Directory (createDirectoryIfMissing)
 import System.FilePath ((</>))
 
 import FFI.AgdaUnparse (AgdaUnparse (..))
@@ -32,7 +33,8 @@ type CertName = String
 type CertDir = FilePath
 
 data CertifierError
-  = InvalidCertificate CertDir
+  = -- | Certificate dir + certifier report
+    InvalidCertificate CertDir String
   | InvalidCompilerOutput
   | ValidationError CertName
 
@@ -45,12 +47,15 @@ data CertifierOutput
     ProjectOutput CertDir
 
 prettyCertifierError :: CertifierError -> String
-prettyCertifierError (InvalidCertificate certDir) =
+prettyCertifierError (InvalidCertificate certDir report) =
   "\n\nInvalid certificate: "
     <> certDir
     <> "\nThe compilation was not successfully certified. \
        \Please open a bug report at https://www.github.com/IntersectMBO/plutus \
-       \and attach the faulty certificate.\n"
+       \and attach the faulty certificate.\n\
+       \Certifier report:\n"
+    <> report
+    <> "\n"
 prettyCertifierError InvalidCompilerOutput =
   "\n\nInvalid compiler output: \
   \\nThe certifier was not able to process the trace produced by the compiler. \
@@ -81,19 +86,13 @@ mkCertifier simplTrace certName certOutput = do
   let rawAgdaTrace = mkFfiSimplifierTrace simplTrace
   case runCertifierMain rawAgdaTrace of
     Just (passed, report) -> do
-      liftIO . putStrLn $
-        "Certifier result: "
-          <> if passed then "PASS" else "FAIL"
       case certOutput of
         BasicOutput -> pure ()
-        ReportOutput file -> liftIO $ do
-          T.writeFile file report
-          putStrLn $ "Report written to " <> file
+        ReportOutput file -> liftIO $ T.writeFile file report
         ProjectOutput certDir -> do
           let cert = mkAgdaCertificateProject $ mkCertificate certName rawAgdaTrace
           writeCertificateProject certDir cert
-          liftIO . putStrLn $ "Certificate produced in " <> certDir
-          unless passed . throwError $ InvalidCertificate certDir
+          unless passed . throwError $ InvalidCertificate certDir (Text.unpack report)
       pure passed
     Nothing -> throwError InvalidCompilerOutput
 
@@ -336,8 +335,8 @@ writeCertificateProject
     liftIO $ do
       let (mainModulePath, mainModuleContents) = mainModule
           (agdalibPath, agdalibContents) = agdalib
-      createDirectory certDir
-      createDirectory (certDir </> "src")
+      createDirectoryIfMissing True certDir
+      createDirectoryIfMissing True (certDir </> "src")
       writeFile (certDir </> "src" </> mainModulePath) mainModuleContents
       writeFile (certDir </> agdalibPath) agdalibContents
       traverse_

plutus-tx-plugin/changelog.d/20260311_120000_agda_certifier_source_location_tracking.md

@@ -0,0 +1,10 @@
+### Added
+
+- Source location tracking for the Agda certifier: the plugin now embeds
+  `RealSrcSpan` information in `CompileContext` (`ccCurrentLoc`, `ccSourceLoc`)
+  and passes it through to certificate generation via `ReaderT` instead of
+  invasive function parameters.
+- `certify` plugin option to trigger Agda certificate generation for compiled
+  Plutus scripts.
+- `generateCertificate` top-level function that invokes the certifier with
+  package name, module name, and source location metadata.

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

@@ -82,8 +82,10 @@ library
     , base16-bytestring
     , bytestring
     , containers
+    , directory
     , either
     , extra
+    , filepath
     , ghc
     , lens
     , megaparsec