diff --git a/.github/workflows/plinth-certifier-tests.yml b/.github/workflows/plinth-certifier-tests.yml new file mode 100644 index 00000000000..587bfa06860 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index 50513c61b65..a2f3925041b 100644 --- a/.gitignore +++ b/.gitignore @@ -83,6 +83,7 @@ act-event.json .history/ .virtualenv .vscode/ +.claude/ .hsenv TAGS .DS_Store diff --git a/plutus-executables/executables/uplc/Main.hs b/plutus-executables/executables/uplc/Main.hs index c98a05b4815..0fdb259c2e8 100644 --- a/plutus-executables/executables/uplc/Main.hs +++ b/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 diff --git a/plutus-metatheory/changelog.d/20260311_120000_agda_certifier_improvements.md b/plutus-metatheory/changelog.d/20260311_120000_agda_certifier_improvements.md new file mode 100644 index 00000000000..39d92e671a3 --- /dev/null +++ b/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). diff --git a/plutus-metatheory/src/Certifier.hs b/plutus-metatheory/src/Certifier.hs index f772ba16462..f9e91839941 100644 --- a/plutus-metatheory/src/Certifier.hs +++ b/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_ diff --git a/plutus-tx-plugin/changelog.d/20260311_120000_agda_certifier_source_location_tracking.md b/plutus-tx-plugin/changelog.d/20260311_120000_agda_certifier_source_location_tracking.md new file mode 100644 index 00000000000..1839f8274b7 --- /dev/null +++ b/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. diff --git a/plutus-tx-plugin/plutus-tx-plugin.cabal b/plutus-tx-plugin/plutus-tx-plugin.cabal index 4f340f3dbe6..0885e0372d5 100644 --- a/plutus-tx-plugin/plutus-tx-plugin.cabal +++ b/plutus-tx-plugin/plutus-tx-plugin.cabal @@ -82,8 +82,10 @@ library , base16-bytestring , bytestring , containers + , directory , either , extra + , filepath , ghc , lens , megaparsec diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs index 78a8bf762b1..da5f411f865 100644 --- a/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs +++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs @@ -20,6 +20,7 @@ module PlutusTx.Compiler.Expr , compileExprWithDefs , compileDataConRef , encodeSrcSpan + , decodeSrcSpan ) where import GHC.Builtin.Names qualified as GHC @@ -326,7 +327,7 @@ compileAlt (GHC.Alt alt vars body) instArgTys defaultBody = -- See Note [Iterated abstraction and application] -- See Note [Case expressions and laziness] GHC.DataAlt _ -> withVarsScoped ((,Nothing) <$> vars) $ \vars' -> do - b <- compileExpr Nothing body + b <- compileExpr body delayed <- delay b return (PLC.mkIterLamAbs vars' b, PLC.mkIterLamAbs vars' delayed) GHC.DEFAULT -> do @@ -654,7 +655,7 @@ hoistExpr var t = do (PIR.Def var' (PIR.mkVar var', PIR.Strict)) mempty - t' <- maybeProfileRhs var var' =<< addSpan (compileExpr Nothing t) + t' <- maybeProfileRhs var var' =<< addSpan (compileExpr t) -- See Note [Non-strict let-bindings] PIR.modifyTermDef lexName (const $ PIR.Def var' (t', PIR.NonStrict)) pure $ PIR.mkVar var' @@ -870,7 +871,7 @@ compileHaskellList = buildList . strip -- This is when the list is a single element and GHC will specialize list builder directly. -- GHC will generate core that looks like below: -- (:) @resTy e ([] @resTy) - buildList (GHC.App (GHC.App (GHC.App (GHC.Var _con) _ty) e) _) = traverse (compileExpr Nothing) [e] + buildList (GHC.App (GHC.App (GHC.App (GHC.Var _con) _ty) e) _) = traverse (compileExpr) [e] -- This is when the list has more than one elements. GHC will generate core that looks like below: -- build @resTy (\con nil -> con e1 (con e2 (... nil))) -- 'build' is some special function that abstracts the list type. @@ -885,7 +886,7 @@ compileHaskellList = buildList . strip | otherwise = err consume _ = err in - consume li >>= traverse (compileExpr Nothing) + consume li >>= traverse (compileExpr) buildList _ = err traceExprMsg :: Maybe GHC.RealSrcSpan -> GHC.SDoc @@ -893,8 +894,8 @@ traceExprMsg = \case Nothing -> "Compiling code:" Just loc -> "Compiling code at" GHC.<+> GHC.ppr loc GHC.<> ":" -compileExpr :: CompilingDefault uni fun m ann => Maybe GHC.RealSrcSpan -> GHC.CoreExpr -> m (PIRTerm uni fun) -compileExpr mloc e = do +compileExpr :: CompilingDefault uni fun m ann => GHC.CoreExpr -> m (PIRTerm uni fun) +compileExpr e = do -- See Note [Scopes] CompileContext { ccScope = scope @@ -974,9 +975,10 @@ compileExpr mloc e = do pure $ PLC.constant annMayInline $ PLC.Some $ PLC.ValueOf (PLC.DefaultUniList ty') [] Nothing -> throwPlain $ CompilationError "'mkNil' applied to an unknown type" + mloc <- asks ccCurrentLoc case extractLoc anchorName maybeModBreaks e of (Just loc, e') -> do - res <- compileExpr (Just loc) e' + res <- local (\ctx -> ctx {ccCurrentLoc = Just loc}) $ compileExpr e' CompileContext {ccOpts = coverageOpts} <- ask -- See Note [Coverage annotations] let anns = Set.toList $ activeCoverageTypes coverageOpts @@ -990,7 +992,7 @@ compileExpr mloc e = do GHC.App (GHC.App (GHC.App (GHC.Var var) (GHC.Type resTy)) scrut) li | GHC.getName var == caseIntegerName && coDatatypeStyle opts == PIR.BuiltinCasing -> do resTy' <- compileTypeNorm resTy - scrut' <- compileExpr Nothing scrut + scrut' <- compileExpr scrut branches <- compileHaskellList li pure $ PIR.kase annAlwaysInline resTy' scrut' branches | GHC.getName var == caseIntegerName -> @@ -1000,7 +1002,7 @@ compileExpr mloc e = do -- list. Ideally, It is possible to have some custom PIR here that will generate -- chain of if-statements so that can skip the list construction work if we want -- to optimize more here. - compileExpr Nothing $ GHC.App (GHC.App (GHC.App (GHC.Var listIndexId) (GHC.Type resTy)) li) scrut + compileExpr $ GHC.App (GHC.App (GHC.App (GHC.Var listIndexId) (GHC.Type resTy)) li) scrut {- Note [Lazy boolean operators] (||) and (&&) have a special treatment: we want them lazy in the second argument, as this is the behavior in Haskell and other PLs. @@ -1009,11 +1011,11 @@ compileExpr mloc e = do -- Lazy || GHC.App (GHC.App (GHC.Var var) a) b | GHC.getName var == boolOperatorOr -> - compileExpr Nothing $ GHC.mkIfThenElse a (GHC.Var GHC.trueDataConId) b + compileExpr $ GHC.mkIfThenElse a (GHC.Var GHC.trueDataConId) b -- Lazy && GHC.App (GHC.App (GHC.Var var) a) b | GHC.getName var == boolOperatorAnd -> - compileExpr Nothing $ GHC.mkIfThenElse a b (GHC.Var GHC.falseDataConId) + compileExpr $ GHC.mkIfThenElse a b (GHC.Var GHC.falseDataConId) -- `inline f` or `inline (f x ... xn)` GHC.App (GHC.App (GHC.Var var) (GHC.Type _aTy)) e' | GHC.getName var == inlineName || GHC.getName var == GHC.inlineIdName -> @@ -1026,12 +1028,12 @@ compileExpr mloc e = do -- we use it directly. -- This only supports `inline f`, not `inline (f x1 ... xn)`. Just (_var, Just def) | null args -> pure def - _ -> compileExpr Nothing e' + _ -> compileExpr e' Just unfolding -- `f` is recursive. We do not inline recursive bindings. - | any (== f) (universeBi unfolding) -> compileExpr Nothing e' - | otherwise -> compileExpr Nothing (GHC.mkCoreApps unfolding args) - _ -> compileExpr Nothing e' + | any (== f) (universeBi unfolding) -> compileExpr e' + | otherwise -> compileExpr (GHC.mkCoreApps unfolding args) + _ -> compileExpr e' -- See Note [String literals] -- See Note [IsString instances and UTF-8 encoded string literals] -- IsString has only one method, so it's enough to know that it's an IsString method @@ -1114,16 +1116,16 @@ compileExpr mloc e = do GHC.Lit lit -> compileLiteral lit -- These are all wrappers around string and char literals, but keeping them allows us to give better errors -- unpackCString# is just a wrapper around a literal - GHC.Var n `GHC.App` expr | GHC.getName n == GHC.unpackCStringName -> compileExpr Nothing expr + GHC.Var n `GHC.App` expr | GHC.getName n == GHC.unpackCStringName -> compileExpr expr -- See Note [unpackFoldrCString#] GHC.Var build `GHC.App` _ `GHC.App` GHC.Lam _ (GHC.Var unpack `GHC.App` _ `GHC.App` expr) | GHC.getName build == GHC.buildName && GHC.getName unpack == GHC.unpackCStringFoldrName -> - compileExpr Nothing expr + compileExpr expr -- C# is just a wrapper around a literal - GHC.Var (GHC.idDetails -> GHC.DataConWorkId dc) `GHC.App` arg | dc == GHC.charDataCon -> compileExpr Nothing arg + GHC.Var (GHC.idDetails -> GHC.DataConWorkId dc) `GHC.App` arg | dc == GHC.charDataCon -> compileExpr arg -- Handle constructors of 'Integer' GHC.Var (GHC.idDetails -> GHC.DataConWorkId dc) `GHC.App` arg | GHC.dataConTyCon dc == GHC.integerTyCon -> do - i <- compileExpr Nothing arg + i <- compileExpr arg -- IN is a negative integer! if GHC.dataConName dc == GHC.integerINDataConName then do @@ -1134,7 +1136,7 @@ compileExpr mloc e = do GHC.Var (GHC.idDetails -> GHC.DataConWorkId dc) | dc == GHC.unboxedUnitDataCon -> pure (PIR.mkConstant annMayInline ()) -- Ignore the magic 'noinline' function, it's the identity but has no unfolding. -- See Note [GHC.Magic.noinline] - GHC.Var n `GHC.App` GHC.Type _ `GHC.App` arg | GHC.getName n == GHC.noinlineIdName -> compileExpr Nothing arg + GHC.Var n `GHC.App` GHC.Type _ `GHC.App` arg | GHC.getName n == GHC.noinlineIdName -> compileExpr arg -- See Note [GHC runtime errors] -- GHC.Var (isErrorId -> True) `GHC.App` _ `GHC.App` GHC.Type t `GHC.App` _ `GHC.App` _ -> @@ -1164,7 +1166,7 @@ compileExpr mloc e = do throwPlain $ UnsupportedError "Use of == from the Haskell Eq typeclass" GHC.Var n | isProbablyIntegerEq n -> do - lookupGhcId 'Builtins.equalsInteger >>= compileExpr Nothing . GHC.Var + lookupGhcId 'Builtins.equalsInteger >>= compileExpr . GHC.Var GHC.Var n | isProbablyBytestringEq n -> throwPlain $ @@ -1227,7 +1229,7 @@ compileExpr mloc e = do GHC.$+$ (GHC.ppr $ GHC.realIdUnfolding n) -- arg can be a type here, in which case it's a type instantiation l `GHC.App` GHC.Type t -> do - l' <- compileExpr Nothing l + l' <- compileExpr l fmap ( -- If the head of the application is an `AsData` matcher, propagate the -- `annIsAsDataMatcher` annotation to the whole application. @@ -1243,7 +1245,7 @@ compileExpr mloc e = do ) -- otherwise it's a normal application l `GHC.App` arg -> do - l' <- compileExpr Nothing l + l' <- compileExpr l let isAsDataMatcher = annIsAsDataMatcher (PIR.termAnn l') fmap ( -- If the head of the application is an `AsData` matcher, propagate the @@ -1256,21 +1258,21 @@ compileExpr mloc e = do ( -- If the head of the application is an `AsData` matcher, set `safeToInline` -- to True and continue. (if isAsDataMatcher then local (\c -> c {ccSafeToInline = True}) else id) - (PIR.Apply annMayInline <$> pure l' <*> compileExpr Nothing arg) + (PIR.Apply annMayInline <$> pure l' <*> compileExpr arg) ) -- if we're biding a type variable it's a type abstraction GHC.Lam b@(GHC.isTyVar -> True) body -> -- Ignore type binders for runtime rep variables, see Note [Runtime reps] if GHC.isRuntimeRepTy $ GHC.varType b - then compileExpr Nothing body - else mkTyAbsScoped b $ compileExpr Nothing body + then compileExpr body + else mkTyAbsScoped b $ compileExpr body -- otherwise it's a normal lambda GHC.Lam b body -> do let ann = if safeToInline then annSafeToInline else annMayInline - mkLamAbsScoped ann b $ compileExpr Nothing body + mkLamAbsScoped ann b $ compileExpr body GHC.Let (GHC.NonRec b rhs) body -> do -- the binding is in scope for the body, but not for the arg - rhs' <- compileExpr Nothing rhs + rhs' <- compileExpr rhs ty <- case rhs of GHC.Lit (GHC.LitNumber {}) | GHC.eqType (GHC.varType b) GHC.byteArrayPrimTy -> @@ -1296,24 +1298,24 @@ compileExpr mloc e = do withVarTyScoped b ty $ \v -> do rhs'' <- maybeProfileRhs b v rhs' let binds = pure $ PIR.TermBind annMayInline PIR.NonStrict v rhs'' - body' <- compileExpr Nothing body + body' <- compileExpr body pure $ PIR.Let annMayInline PIR.NonRec binds body' GHC.Let (GHC.Rec bs) body -> withVarsScoped (fmap (second (const Nothing)) bs) $ \vars -> do -- the bindings are scope in both the body and the args -- TODO: this is a bit inelegant matching the vars back up binds <- for (zip vars bs) $ \(v, (ghcVar, rhs)) -> do - rhs' <- maybeProfileRhs ghcVar v =<< compileExpr Nothing rhs + rhs' <- maybeProfileRhs ghcVar v =<< compileExpr rhs -- See Note [Non-strict let-bindings] pure $ PIR.TermBind annMayInline PIR.NonStrict v rhs' - body' <- compileExpr Nothing body + body' <- compileExpr body pure $ PIR.mkLet annMayInline PIR.Rec binds body' GHC.Case scrutinee b t alts -> compileCase (const . GHC.isDeadOcc . GHC.occInfo . GHC.idInfo) True binfo scrutinee b t alts -- ignore ticks - GHC.Tick _ body -> compileExpr Nothing body + GHC.Tick _ body -> compileExpr body -- See Note [Coercions and newtypes] - GHC.Cast body _ -> compileExpr Nothing body + GHC.Cast body _ -> compileExpr body GHC.Type _ -> throwPlain $ UnsupportedError "Types as standalone expressions" GHC.Coercion _ -> throwPlain $ UnsupportedError "Coercions as expressions" @@ -1346,9 +1348,9 @@ compileCase isDead rewriteConApps binfo scrutinee binder t alts = do -- See Note [Evaluation-only cases] | all (`isDead` body) bs -> do -- See Note [At patterns] - scrutinee' <- compileExpr Nothing scrutinee + scrutinee' <- compileExpr scrutinee withVarScoped binder binderAnn (Just scrutinee') $ \v -> do - body' <- compileExpr Nothing body + body' <- compileExpr body -- See Note [At patterns] let binds = [PIR.TermBind annMayInline PIR.Strict v scrutinee'] pure $ PIR.mkLet annMayInline PIR.NonRec binds body' @@ -1385,7 +1387,7 @@ compileCase isDead rewriteConApps binfo scrutinee binder t alts = do compileCase isDead' False binfo scrutinee binder t [GHC.Alt con bs (transform f body)] _ -> do -- See Note [At patterns] - scrutinee' <- compileExpr Nothing scrutinee + scrutinee' <- compileExpr scrutinee let scrutineeType = GHC.varType binder -- the variable for the scrutinee is bound inside the cases, but not in the scrutinee expression itself @@ -1406,11 +1408,11 @@ compileCase isDead rewriteConApps binfo scrutinee binder t alts = do -- 2. Compile the body of the DEFAULT alt ahead of time so it can be shared (See Note [Sharing DEFAULT bodies]) (alts', defCompiled) <- case mdef of Just d -> do - defCompiled <- compileExpr Nothing d + defCompiled <- compileExpr d pure (GHC.addDefault rest (Just d), defCompiled) Nothing -> do let d = GHC.mkImpossibleExpr t "unreachable alternative" - defCompiled <- compileExpr Nothing d + defCompiled <- compileExpr d pure (GHC.addDefault alts (Just d), defCompiled) defName <- PLC.freshName "defaultBody" @@ -1576,7 +1578,7 @@ coverageCompile originalExpr exprType src compiledTerm covT = -- ``` -- traceBool "" "" compiledTerm -- ``` - traceBoolCompiled <- compileExpr Nothing . GHC.Var =<< lookupGhcId 'traceBool + traceBoolCompiled <- compileExpr . GHC.Var =<< lookupGhcId 'traceBool let mkMetadata = CoverageMetadata . foldMap @@ -1705,7 +1707,7 @@ compileExprWithDefs e = do defineBuiltinTerms defineIntegerNegate defineFix - compileExpr Nothing e + compileExpr e {- Note [We always need DEFAULT] GHC can be clever and omit case alternatives sometimes, typically when the typechecker says a case diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs-boot b/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs-boot index a1064b7d220..01c296ae0ae 100644 --- a/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs-boot +++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs-boot @@ -11,7 +11,7 @@ import GHC.Plugins qualified as GHC compileDataConRef :: CompilingDefault uni fun m ann => GHC.DataCon -> m (PIRTerm uni fun) compileExpr :: CompilingDefault uni fun m ann - => Maybe GHC.RealSrcSpan -> GHC.CoreExpr -> m (PIRTerm uni fun) + => GHC.CoreExpr -> m (PIRTerm uni fun) compileExprWithDefs :: CompilingDefault uni fun m ann => GHC.CoreExpr -> m (PIRTerm uni fun) diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs index c2fa56573d3..c4c8a2d037f 100644 --- a/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs +++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs @@ -68,6 +68,10 @@ data CompileContext uni fun = CompileContext , ccDebugTraceOn :: Bool , ccRewriteRules :: PIR.RewriteRules uni fun , ccSafeToInline :: Bool + , ccCurrentLoc :: Maybe GHC.RealSrcSpan + , ccPackageName :: String + , ccModuleName :: String + , ccSourceLoc :: Maybe GHC.RealSrcSpan } data CompileState = CompileState diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Utils.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Utils.hs index 45b0c90477f..4880f6c5f80 100644 --- a/plutus-tx-plugin/src/PlutusTx/Compiler/Utils.hs +++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Utils.hs @@ -105,3 +105,25 @@ tyConsOfBind = \case tyConsOfAlt :: GHC.CoreAlt -> GHC.UniqSet GHC.TyCon tyConsOfAlt (GHC.Alt _ vars e) = foldMap tyConsOfBndr vars <> tyConsOfExpr e + +{-| Get the package name for the module being compiled. +Tries 'lookupUnit' first (works for installed packages), then +'thisPackageName' from DynFlags (works for home library units), +and finally falls back to stripping the version from the unit ID string. -} +getPackageName :: GHC.HscEnv -> GHC.Module -> String +getPackageName hscEnv thisModule = + let unitState = GHC.hsc_units hscEnv + unit = GHC.moduleUnit thisModule + in case GHC.lookupUnit unitState unit of + Just unitInfo -> GHC.unitPackageNameString unitInfo + Nothing -> case GHC.thisPackageName (GHC.hsc_dflags hscEnv) of + Just n -> n + Nothing -> stripVersion (GHC.unitString unit) + where + -- Extract "foo-bar" from "foo-bar-1.2.3-inplace-component" + stripVersion s = go [] s + go acc [] = reverse acc + go acc ('-' : rest@(c : _)) + | c >= '0', c <= '9' = reverse acc + | otherwise = go ('-' : acc) rest + go acc (c : rest) = go (c : acc) rest diff --git a/plutus-tx-plugin/src/PlutusTx/Options.hs b/plutus-tx-plugin/src/PlutusTx/Options.hs index b06cfd36189..01c04fde1f2 100644 --- a/plutus-tx-plugin/src/PlutusTx/Options.hs +++ b/plutus-tx-plugin/src/PlutusTx/Options.hs @@ -29,8 +29,7 @@ import Data.Either.Validation import Data.Foldable (toList) #else import Data.Foldable (foldl', toList) -#endif -import Control.Applicative (many, optional, (<|>)) +#endif import Data.List qualified as List import Data.List.NonEmpty (NonEmpty) import Data.Map (Map) @@ -41,7 +40,6 @@ 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 @@ -85,6 +83,9 @@ data PluginOptions = PluginOptions _posRemoveTrace :: Bool , _posDumpCompilationTrace :: Bool , _posCertify :: Maybe String + {-^ @Nothing@: certification disabled. + @Just ""@: certify, placing output next to source files. + @Just path@: certify, placing all output under the given directory. -} } makeLenses ''PluginOptions @@ -329,16 +330,13 @@ pluginOptions = in (k, PluginOption typeRep (setTrue k) posDumpCompilationTrace desc []) , let k = "certify" desc = - "Produce a certificate for the compiled program, with the given name. " + "Produce Agda certificate projects for compiled programs. " <> "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 []) + <> "Currently, this is only supported for the UPLC compilation pipeline. " + <> "When used without a value, certificates are placed next to source files. " + <> "When given a directory path (certify=DIR), all certificates are placed there." + in (k, PluginOption typeRep (optionalStringOption k) posCertify desc []) ] flag :: (a -> a) -> OptionKey -> Maybe OptionValue -> Validation ParseError (a -> a) @@ -347,6 +345,14 @@ flag f k = maybe (Success f) (Failure . UnexpectedValue k) setTrue :: OptionKey -> Maybe OptionValue -> Validation ParseError (Bool -> Bool) setTrue = flag (const True) +{-| An option that takes an optional string value. +Without a value: sets to @Just ""@. With a value: sets to @Just (Text.unpack v)@. -} +optionalStringOption + :: OptionKey -> Maybe OptionValue -> Validation ParseError (Maybe String -> Maybe String) +optionalStringOption _k = \case + Nothing -> Success $ const (Just "") + Just v -> Success $ const (Just (Text.unpack v)) + plcParserOption :: PLC.Parser a -> OptionKey -> Maybe OptionValue -> Validation ParseError (a -> a) plcParserOption p k = \case Just t -> case PLC.runQuoteT $ PLC.parse p "none" t of diff --git a/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs b/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs index 274f9a5d45a..96ebbee5259 100644 --- a/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs +++ b/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs @@ -38,6 +38,7 @@ import PlutusTx.Compiler.Compat qualified as Compat import PlutusTx.Compiler.Error import PlutusTx.Compiler.Expr import PlutusTx.Compiler.Types +import PlutusTx.Compiler.Utils (getPackageName) import PlutusTx.Coverage import PlutusTx.Function qualified import PlutusTx.List qualified @@ -48,6 +49,7 @@ import PlutusTx.PLCTypes import PlutusTx.Plugin.Utils qualified import PlutusTx.Trace import UntypedPlutusCore qualified as UPLC +import UntypedPlutusCore.Transform.Simplifier (SimplifierTrace) import GHC.ByteCode.Types qualified as GHC import GHC.Core.Coercion.Opt qualified as GHC @@ -91,6 +93,8 @@ import Data.Text qualified as Text import GHC.Num.Integer qualified import Language.Haskell.TH.Syntax as TH hiding (lift) import Prettyprinter qualified as PP +import System.Directory (makeAbsolute) +import System.FilePath (takeDirectory, ()) import System.IO (hPutStrLn, openBinaryTempFile, stderr) import System.IO.Unsafe (unsafePerformIO) @@ -101,6 +105,7 @@ data PluginCtx = PluginCtx , pcAnchorName :: GHC.Name , pcModuleName :: GHC.ModuleName , pcModuleModBreaks :: Maybe GHC.ModBreaks + , pcPackageName :: String } {- Note [Making sure unfoldings are present] @@ -335,18 +340,22 @@ mkPluginPass markerTHName opts = GHC.CoreDoPluginPass "Core to PLC" $ \guts -> d maybeanchorGhcName <- GHC.thNameToGhcName 'PlutusTx.Plugin.Utils.anchor case (maybeMarkerName, maybeanchorGhcName) of -- See Note [Marker resolution] - (Just markerName, Just anchorGhcName) -> - let pctx = + (Just markerName, Just anchorGhcName) -> do + hscEnv <- GHC.getHscEnv + let thisModule = GHC.mg_module guts + pkgName = getPackageName hscEnv thisModule + pctx = PluginCtx { pcOpts = opts , pcFamEnvs = (p_fam_env, GHC.mg_fam_inst_env guts) , pcMarkerName = markerName , pcAnchorName = anchorGhcName - , pcModuleName = GHC.moduleName $ GHC.mg_module guts + , pcModuleName = GHC.moduleName thisModule , pcModuleModBreaks = GHC.mg_modBreaks guts + , pcPackageName = pkgName } - in -- start looking for marker calls from the top-level binds - GHC.bindsOnlyPass (runPluginM pctx . traverse compileBind) guts + -- start looking for marker calls from the top-level binds + GHC.bindsOnlyPass (runPluginM pctx . traverse compileBind) guts _ -> pure guts {-| The monad where the plugin runs in for each module. @@ -496,15 +505,17 @@ compileMarkedExprs expr = do ) -- value argument inner - | markerName == GHC.idName fid -> compileMarkedExprOrDefer (show fs_locStr) codeTy inner + | markerName == GHC.idName fid -> + compileMarkedExprOrDefer (decodeSrcSpan (GHC.unpackFS fs_locStr)) codeTy inner GHC.App ( GHC.App - (stripAnchors anchorGhcName -> (GHC.Var fid)) - (stripAnchors anchorGhcName -> GHC.Type codeTy) + (stripAnchors anchorGhcName -> (mLoc, GHC.Var fid)) + (snd . stripAnchors anchorGhcName -> GHC.Type codeTy) ) -- code to be compiled inner - | markerName == GHC.idName fid -> compileMarkedExprOrDefer "" codeTy inner + | markerName == GHC.idName fid -> + compileMarkedExprOrDefer mLoc codeTy inner e@(GHC.Var fid) | markerName == GHC.idName fid -> throwError . NoContext . InvalidMarkerError . GHC.showSDocUnsafe $ GHC.ppr e @@ -517,7 +528,7 @@ compileMarkedExprs expr = do alts' <- mapM expAlt alts pure $ GHC.Case e' b t alts' GHC.Cast e c -> flip GHC.Cast c <$> compileMarkedExprs e - GHC.Tick t e -> GHC.Tick t <$> compileMarkedExprs e + GHC.Tick tick e -> GHC.Tick tick <$> compileMarkedExprs e e@(GHC.Coercion _) -> pure e e@(GHC.Lit _) -> pure e e@(GHC.Var _) -> pure e @@ -528,10 +539,10 @@ if a compilation error happens and the 'defer-errors' option is turned on, the compilation error is suppressed and the original hs expression is replaced with a haskell runtime-error expression. -} compileMarkedExprOrDefer - :: String -> GHC.Type -> GHC.CoreExpr -> PluginM PLC.DefaultUni PLC.DefaultFun GHC.CoreExpr -compileMarkedExprOrDefer locStr codeTy origE = do + :: Maybe GHC.RealSrcSpan -> GHC.Type -> GHC.CoreExpr -> PluginM PLC.DefaultUni PLC.DefaultFun GHC.CoreExpr +compileMarkedExprOrDefer mLoc codeTy origE = do opts <- asks pcOpts - let compileAct = compileMarkedExpr locStr codeTy origE + let compileAct = compileMarkedExpr mLoc codeTy origE if _posDeferErrors opts -- TODO: we could perhaps move this catchError to the "runExceptT" module-level, but -- it leads to uglier code and difficulty of handling other pure errors @@ -554,12 +565,13 @@ emitRuntimeError codeTy e = do and return a core expression which evaluates to the compiled plc AST as a serialized bytestring, to be injected back to the Haskell program. -} compileMarkedExpr - :: String -> GHC.Type -> GHC.CoreExpr -> PluginM PLC.DefaultUni PLC.DefaultFun GHC.CoreExpr -compileMarkedExpr _locStr codeTy origE = do + :: Maybe GHC.RealSrcSpan -> GHC.Type -> GHC.CoreExpr -> PluginM PLC.DefaultUni PLC.DefaultFun GHC.CoreExpr +compileMarkedExpr mLoc codeTy origE = do flags <- GHC.getDynFlags famEnvs <- asks pcFamEnvs opts <- asks pcOpts moduleName <- asks pcModuleName + packageName <- asks pcPackageName let moduleNameStr = GHC.showSDocForUser flags GHC.emptyUnitState GHC.alwaysQualify (GHC.ppr moduleName) -- We need to do this out here, since it has to run in CoreM @@ -616,6 +628,10 @@ compileMarkedExpr _locStr codeTy origE = do , ccDebugTraceOn = _posDumpCompilationTrace opts , ccRewriteRules = makeRewriteRules opts , ccSafeToInline = False + , ccCurrentLoc = Nothing + , ccPackageName = packageName + , ccModuleName = moduleNameStr + , ccSourceLoc = mLoc } st = CompileState 0 mempty -- See Note [Occurrence analysis] @@ -623,7 +639,7 @@ compileMarkedExpr _locStr codeTy origE = do ((pirP, uplcP), covIdx) <- runWriterT . runQuoteT . flip runReaderT ctx . flip evalStateT st $ - runCompiler moduleNameStr opts origE' + runCompiler opts origE' -- serialize the PIR, PLC, and coverageindex outputs into a bytestring. bsPir <- makeByteStringLiteral $ flat pirP @@ -653,11 +669,11 @@ runCompiler , MonadError (CompileError uni fun Ann) m , MonadIO m ) - => String - -> PluginOptions + => PluginOptions -> GHC.CoreExpr -> m (PIRProgram uni fun, UPLCProgram uni fun) -runCompiler moduleName opts expr = do +runCompiler opts expr = do + moduleName <- asks ccModuleName GHC.DynFlags {GHC.extensions = extensions} <- asks ccFlags let enabledExtensions = @@ -812,17 +828,14 @@ runCompiler moduleName opts expr = do modifyError PLC.TypeErrorE $ PLC.inferTypeOfProgram plcTcConfig (plcP $> annMayInline) - let optCertify = opts ^. posCertify (uplcP, simplTrace) <- flip runReaderT plcOpts $ PLC.compileProgramWithTrace plcP - liftIO $ case optCertify of - Just certName -> do - -- FIXME: add a plugin option to choose from BasicOutput vs. other options - result <- runCertifier $ mkCertifier simplTrace certName BasicOutput - case result of - Right _ -> pure () - Left err -> - hPutStrLn stderr $ prettyCertifierError err + case opts ^. posCertify of Nothing -> pure () + Just certifyPath -> do + packageName <- asks ccPackageName + mLoc <- asks ccSourceLoc + liftIO $ + generateCertificate packageName moduleName mLoc opts simplTrace certifyPath dbP <- liftExcept $ modifyError PLC.FreeVariableErrorE $ traverseOf UPLC.progTerm UPLC.deBruijnTerm uplcP when (opts ^. posDumpUPlc) . liftIO $ @@ -848,6 +861,53 @@ runCompiler moduleName opts expr = do getSrcSpans :: PIR.Provenance Ann -> SrcSpans getSrcSpans = SrcSpans . Set.unions . fmap (unSrcSpans . annSrcSpans) . toList +generateCertificate + :: String + -> String + -> Maybe GHC.RealSrcSpan + -> PluginOptions + -> SimplifierTrace PLC.Name PLC.DefaultUni PLC.DefaultFun a + -> String + -> IO () +generateCertificate packageName moduleName mLoc opts simplTrace certifyPath = do + absCertifyPath <- + if null certifyPath + then pure "" + else makeAbsolute certifyPath + let sanitise c = if c == '.' Prelude.|| c == '-' then '_' else c + certName = map sanitise packageName ++ "_" ++ map sanitise moduleName + locTag = case mLoc of + Just sp -> + let line = show (GHC.srcSpanStartLine sp) + col = show (GHC.srcSpanStartCol sp) + in ":" ++ line ++ ":" ++ col + Nothing -> ":unknown-location" + certDirName = + packageName ++ "_" ++ moduleName ++ locTag ++ ".agda-cert" + certDir + | null absCertifyPath = + -- No path given: place next to the source file + case mLoc of + Just sp -> + let sourceFile = GHC.unpackFS (GHC.srcSpanFile sp) + in takeDirectory sourceFile certDirName + Nothing -> certDirName + | otherwise = + -- Path given: place all certificates under that directory + absCertifyPath certDirName + let verbose = opts ^. posVerbosity Prelude./= Quiet + result <- runCertifier $ mkCertifier simplTrace certName (ProjectOutput certDir) + case result of + Right _ -> do + writeFile (certDir "plinth-certifier-PASS.txt") "" + when verbose $ + hPutStrLn stderr $ + "Certifier result: PASS — " ++ certDir + Left err -> do + let errMsg = prettyCertifierError err + writeFile (certDir "plinth-certifier-FAIL.txt") (errMsg ++ "\n") + hPutStrLn stderr $ "Certifier result: FAIL — " ++ certDir ++ "\n" ++ errMsg + -- | Get the 'GHC.Name' corresponding to the given 'TH.Name', or throw an error if we can't get it. thNameToGhcNameOrFail :: TH.Name -> PluginM uni fun GHC.Name thNameToGhcNameOrFail name = do @@ -893,12 +953,14 @@ stripTicks = \case GHC.Tick _ e -> stripTicks e e -> e -stripAnchors :: GHC.Name -> GHC.CoreExpr -> GHC.CoreExpr +{-| Strip a single @anchor@ application (and any surrounding ticks), +returning the decoded source span if present. -} +stripAnchors :: GHC.Name -> GHC.CoreExpr -> (Maybe GHC.RealSrcSpan, GHC.CoreExpr) stripAnchors marker = \case GHC.Tick _ e -> stripAnchors marker e - GHC.App (GHC.App (GHC.App (GHC.Var f) _locTy) _codeTy) code - | GHC.getName f == marker -> stripAnchors marker code - other -> other + GHC.App (GHC.App (GHC.App (GHC.Var f) (GHC.Type (GHC.LitTy (GHC.StrTyLit locFs)))) _codeTy) code + | GHC.getName f == marker -> (decodeSrcSpan (GHC.unpackFS locFs), code) + other -> (Nothing, other) -- | Helper to avoid doing too much construction of Core ourselves mkCompiledCode :: forall a. BS.ByteString -> BS.ByteString -> BS.ByteString -> CompiledCode a diff --git a/plutus-tx/src/PlutusTx/TH.hs b/plutus-tx/src/PlutusTx/TH.hs index ef264458f79..85c444140e0 100644 --- a/plutus-tx/src/PlutusTx/TH.hs +++ b/plutus-tx/src/PlutusTx/TH.hs @@ -8,6 +8,7 @@ module PlutusTx.TH , loadFromFile ) where +import Data.List (intercalate) import Data.Proxy import Language.Haskell.TH qualified as TH import Language.Haskell.TH.Syntax qualified as TH @@ -49,6 +50,19 @@ compileUntyped :: TH.Q TH.Exp -> TH.Q TH.Exp compileUntyped e = do TH.addCorePlugin "PlutusTx.Plugin" loc <- TH.location - let locStr = TH.pprint loc + let locStr = encodeTHLoc loc -- See Note [Typed TH] [|plc (Proxy :: Proxy $(TH.litT $ TH.strTyLit locStr)) $(e)|] + +{-| Encode a TH location in the same null-separated format as +'PlutusTx.Compiler.Expr.encodeSrcSpan', so that 'decodeSrcSpan' can parse it. -} +encodeTHLoc :: TH.Loc -> String +encodeTHLoc loc = + intercalate + "\0" + [ TH.loc_filename loc + , show (fst (TH.loc_start loc)) + , show (snd (TH.loc_start loc)) + , show (fst (TH.loc_end loc)) + , show (snd (TH.loc_end loc)) + ] diff --git a/scripts/plinth-certifier-tests.py b/scripts/plinth-certifier-tests.py new file mode 100755 index 00000000000..2442911e4f2 --- /dev/null +++ b/scripts/plinth-certifier-tests.py @@ -0,0 +1,527 @@ +#!/usr/bin/env python3 + +"""Plinth certifier test pipeline — subcommand-based interface. + +Certificate folders use stable names (__.agda-cert) so +rebuilding overwrites in-place rather than creating new timestamped folders. +The user controls what gets rebuilt via normal cabal incremental compilation +(or cabal clean + cabal build when a full rebuild is needed). + +Usage: plinth-certifier-tests.py [options] + +Commands: + build — Generate Agda certificates via cabal build with certify plugin option + check — Run Agda type-checking on generated certificates + status — Show summary of current certificate state (read-only) + clean — Remove certificate directories + run — Full pipeline: build then check +""" + +from __future__ import annotations + +import argparse +import fnmatch +import os +import re +import shutil +import subprocess +import sys +from concurrent.futures import ProcessPoolExecutor, as_completed +from dataclasses import dataclass, field +from datetime import datetime, timezone +from pathlib import Path + + +# --------------------------------------------------------------------------- +# Helpers +# --------------------------------------------------------------------------- + +def repo_root() -> Path: + result = subprocess.run( + ["git", "rev-parse", "--show-toplevel"], + capture_output=True, text=True, check=True, + ) + return Path(result.stdout.strip()) + + +REPO_ROOT = repo_root() +DEFAULT_CERT_DIR = REPO_ROOT / "agda-certificates" +DEFAULT_PATTERN = "*.agda-cert" + +AGDA_PASS_LOG = "agda-check-PASS.log" +AGDA_FAIL_LOG = "agda-check-FAIL.log" + + +def die(msg: str) -> None: + print(f"error: {msg}", file=sys.stderr) + sys.exit(1) + + +def agda_log_file(d: Path) -> Path | None: + """Return the agda check log if one exists (PASS or FAIL).""" + p = d / AGDA_PASS_LOG + if p.exists(): + return p + f = d / AGDA_FAIL_LOG + if f.exists(): + return f + return None + + +def remove_agda_logs(d: Path) -> None: + """Remove any existing agda check logs.""" + for name in (AGDA_PASS_LOG, AGDA_FAIL_LOG): + f = d / name + if f.exists(): + f.unlink() + + +# --------------------------------------------------------------------------- +# Certificate inspection +# --------------------------------------------------------------------------- + +@dataclass +class CertStatus: + """Status of a single certificate directory.""" + name: str + path: Path + certifier: str = "?" # PASS | FAIL | NO-RESULT + agda: str = "PENDING" # PASS | FAIL | SKIP | PENDING | STALE + fail_reason: str = "" + + +def inspect_cert(d: Path) -> CertStatus: + """Read the status files in a certificate directory.""" + s = CertStatus(name=d.name, path=d) + pass_file = d / "plinth-certifier-PASS.txt" + fail_file = d / "plinth-certifier-FAIL.txt" + + if pass_file.exists(): + s.certifier = "PASS" + elif fail_file.exists(): + s.certifier = "FAIL" + lines = fail_file.read_text().splitlines()[:5] + s.fail_reason = "\n".join(lines) + else: + s.certifier = "NO-RESULT" + + # Determine Agda status + if s.certifier != "PASS": + # Certifier didn't pass — Agda check is skipped + s.agda = "SKIP" + elif (d / AGDA_PASS_LOG).exists(): + log = d / AGDA_PASS_LOG + if pass_file.stat().st_mtime > log.stat().st_mtime: + s.agda = "STALE" + else: + s.agda = "PASS" + elif (d / AGDA_FAIL_LOG).exists(): + log = d / AGDA_FAIL_LOG + if pass_file.stat().st_mtime > log.stat().st_mtime: + s.agda = "STALE" + else: + s.agda = "FAIL" + else: + s.agda = "PENDING" + + return s + + +def is_uptodate(d: Path) -> bool: + """True if an agda check log exists and is at least as new as plinth-certifier-PASS.txt.""" + log = agda_log_file(d) + pass_f = d / "plinth-certifier-PASS.txt" + return ( + log is not None + and pass_f.exists() + and pass_f.stat().st_mtime <= log.stat().st_mtime + ) + + +def list_cert_dirs(cert_dir: Path, pattern: str) -> list[Path]: + """Return sorted list of certificate directories matching pattern.""" + if not cert_dir.is_dir(): + return [] + dirs = [] + for d in sorted(cert_dir.iterdir()): + if d.is_dir() and fnmatch.fnmatch(d.name, pattern): + dirs.append(d) + return dirs + + +# --------------------------------------------------------------------------- +# cmd_build +# --------------------------------------------------------------------------- + +def cmd_build(args: argparse.Namespace) -> int: + cert_dir = args.output.resolve() + targets = args.targets or ["all"] + + print("=== build ===") + print(f"Targets : {' '.join(targets)}") + print(f"Output : {cert_dir}") + print(f"Clean : {args.clean}") + print() + + if args.clean: + print("--- cabal clean ---") + subprocess.run(["cabal", "clean"]) + print() + + cert_dir.mkdir(parents=True, exist_ok=True) + + print(f"--- cabal build {' '.join(targets)} ---") + result = subprocess.run( + ["cabal", "build", *targets, + f"--ghc-options=-fplugin-opt PlutusTx.Plugin:certify={cert_dir}"], + ) + + if result.returncode != 0: + print(f"WARNING: cabal build exited with code {result.returncode}", file=sys.stderr) + print("Continuing to check any certificates that were produced...", file=sys.stderr) + print() + return result.returncode + + +# --------------------------------------------------------------------------- +# cmd_check +# --------------------------------------------------------------------------- + +def _check_one(cert_dir: Path) -> tuple[str, str, str]: + """Check a single certificate. Returns (status, name, detail). + + Runs in a subprocess worker so must be self-contained. + """ + name = cert_dir.name + pass_file = cert_dir / "plinth-certifier-PASS.txt" + fail_file = cert_dir / "plinth-certifier-FAIL.txt" + + # Check certifier result + if pass_file.exists(): + pass # proceed to Agda + elif fail_file.exists(): + return ("SKIP", name, "certifier failed") + else: + return ("SKIP", name, "no plinth-certifier result file") + + # Find .agda-lib + agda_libs = list(cert_dir.glob("*.agda-lib")) + if not agda_libs: + return ("SKIP", name, "no .agda-lib found") + + agda_lib = agda_libs[0] + cert_name = None + for line in agda_lib.read_text().splitlines(): + m = re.match(r"^name:\s*(.+)$", line) + if m: + cert_name = m.group(1).strip() + break + + if not cert_name: + return ("SKIP", name, "could not parse name from .agda-lib") + + main_agda = cert_dir / "src" / f"{cert_name}.agda" + if not main_agda.exists(): + return ("SKIP", name, f"main module not found: src/{cert_name}.agda") + + # Remove old logs before running + for old_log in ("agda-check-PASS.log", "agda-check-FAIL.log"): + f = cert_dir / old_log + if f.exists(): + f.unlink() + + # Run Agda + result = subprocess.run( + ["agda-with-stdlib-and-metatheory", f"src/{cert_name}.agda"], + cwd=cert_dir, + capture_output=True, text=True, + ) + output = result.stdout + result.stderr + + if result.returncode == 0: + (cert_dir / "agda-check-PASS.log").write_text(output) + return ("PASS", name, "") + else: + (cert_dir / "agda-check-FAIL.log").write_text(output) + return ("FAIL", name, f"exit code {result.returncode}") + + +def cmd_check(args: argparse.Namespace) -> int: + cert_dir = args.output.resolve() + pattern = args.pattern + jobs = args.jobs + force = args.force + + print("=== check ===") + print(f"Certificate dir : {cert_dir}") + print(f"Filter pattern : {pattern}") + print(f"Parallel jobs : {jobs}") + print(f"Force re-check : {force}") + print() + + if not cert_dir.is_dir(): + die(f"certificate directory does not exist: {cert_dir}") + + all_dirs = list_cert_dirs(cert_dir, pattern) + skipped_uptodate = 0 + dirs_to_check: list[Path] = [] + + for d in all_dirs: + if not force and is_uptodate(d): + skipped_uptodate += 1 + else: + if force: + build_dir = d / "_build" + if build_dir.is_dir(): + shutil.rmtree(build_dir) + dirs_to_check.append(d) + + if skipped_uptodate > 0: + print(f"Skipped {skipped_uptodate} already-checked certificates (use --force to re-check)") + print() + + if not dirs_to_check: + print("No certificate directories to check.") + print() + return 0 + + print(f"Certificates to check: {len(dirs_to_check)}") + print() + + # Run checks + results: list[tuple[str, str, str]] = [] + with ProcessPoolExecutor(max_workers=jobs) as executor: + futures = {executor.submit(_check_one, d): d for d in dirs_to_check} + for future in as_completed(futures): + status, name, detail = future.result() + results.append((status, name, detail)) + if detail: + print(f"{status}: {name} ({detail})", file=sys.stderr) + else: + print(f"{status}: {name}", file=sys.stderr) + + # Sort results by name for deterministic output + results.sort(key=lambda r: r[1]) + + # Tally + pass_list = [r[1] for r in results if r[0] == "PASS"] + fail_list = [r[1] for r in results if r[0] == "FAIL"] + skip_list = [r[1] for r in results if r[0] == "SKIP"] + total = len(results) + + # Write summary + results_file = cert_dir / "__results__.txt" + now = datetime.now(timezone.utc).strftime("%Y-%m-%d %H:%M:%S UTC") + lines = [ + "=== Plinth Certifier Test Results ===", + f"Date: {now}", + f"Certificate dir: {cert_dir}", + f"Filter pattern : {pattern}", + "", + f"Total : {total}", + f"Passed : {len(pass_list)}", + f"Failed : {len(fail_list)}", + f"Skipped: {len(skip_list)}", + ] + if skipped_uptodate > 0: + lines.append(f"Up-to-date (not re-checked): {skipped_uptodate}") + lines.append("") + + if pass_list: + lines.append("--- Passed ---") + lines.extend(f" PASS: {p}" for p in pass_list) + lines.append("") + + if fail_list: + lines.append("--- Failed ---") + lines.extend(f" FAIL: {f}" for f in fail_list) + lines.append("") + + if skip_list: + lines.append("--- Skipped ---") + lines.extend(f" SKIP: {s}" for s in skip_list) + lines.append("") + + summary = "\n".join(lines) + print() + print(summary) + results_file.write_text(summary + "\n") + print(f"Results written to: {results_file}") + print() + + return 1 if fail_list else 0 + + +# --------------------------------------------------------------------------- +# cmd_status +# --------------------------------------------------------------------------- + +def cmd_status(args: argparse.Namespace) -> int: + cert_dir = args.output.resolve() + pattern = args.pattern + + if not cert_dir.is_dir(): + print(f"No certificate directory found at: {cert_dir}") + return 0 + + dirs = list_cert_dirs(cert_dir, pattern) + counts: dict[str, int] = { + "cert_PASS": 0, "cert_FAIL": 0, "cert_NO-RESULT": 0, + "agda_PASS": 0, "agda_FAIL": 0, "agda_SKIP": 0, + "agda_PENDING": 0, "agda_STALE": 0, + } + + for d in dirs: + s = inspect_cert(d) + counts[f"cert_{s.certifier}"] += 1 + counts[f"agda_{s.agda}"] += 1 + # Skip fully-passing certificates (both certifier and agda PASS) + if s.certifier == "PASS" and s.agda == "PASS": + continue + print(f" {s.certifier:<12s} {s.agda:<10s} {s.name}") + + print() + print("=== Status Summary ===") + print(f"Total certificates : {len(dirs)}") + print() + print(f"Certifier PASS : {counts['cert_PASS']}") + print(f"Certifier FAIL : {counts['cert_FAIL']}") + print(f"No result file : {counts['cert_NO-RESULT']}") + print() + print(f"Agda PASS : {counts['agda_PASS']}") + print(f"Agda FAIL : {counts['agda_FAIL']}") + print(f"Agda SKIP : {counts['agda_SKIP']}") + print(f"Agda PENDING : {counts['agda_PENDING']}") + print(f"Agda STALE : {counts['agda_STALE']}") + return 0 + + +# --------------------------------------------------------------------------- +# cmd_clean +# --------------------------------------------------------------------------- + +def cmd_clean(args: argparse.Namespace) -> int: + cert_dir = args.output.resolve() + pattern = args.pattern + + if not cert_dir.is_dir(): + print(f"Nothing to clean: {cert_dir} does not exist.") + return 0 + + if pattern == DEFAULT_PATTERN: + print(f"Removing entire certificate directory: {cert_dir}") + shutil.rmtree(cert_dir) + else: + dirs = list_cert_dirs(cert_dir, pattern) + for d in dirs: + print(f"Removing: {d.name}") + shutil.rmtree(d) + print(f"Removed {len(dirs)} certificate directories.") + return 0 + + +# --------------------------------------------------------------------------- +# cmd_run +# --------------------------------------------------------------------------- + +def cmd_run(args: argparse.Namespace) -> int: + # Build phase + build_ns = argparse.Namespace( + output=args.output, + clean=args.clean, + targets=args.targets, + ) + build_rc = cmd_build(build_ns) + # Continue even if build had warnings + + # Check phase + check_ns = argparse.Namespace( + output=args.output, + pattern=DEFAULT_PATTERN, + jobs=args.jobs, + force=args.force, + ) + return cmd_check(check_ns) + + +# --------------------------------------------------------------------------- +# Argument parsing +# --------------------------------------------------------------------------- + +def make_parser() -> argparse.ArgumentParser: + parser = argparse.ArgumentParser( + prog="plinth-certifier-tests.py", + description="Plinth certifier test pipeline", + ) + sub = parser.add_subparsers(dest="command", required=True) + + # -- build -- + p_build = sub.add_parser("build", help="Generate Agda certificates (cabal build with certify)") + p_build.add_argument("--clean", action="store_true", help="Run cabal clean before building") + p_build.add_argument("-o", "--output", type=Path, default=DEFAULT_CERT_DIR, + help="Certificate output directory") + p_build.add_argument("targets", nargs="*", help="Cabal targets (default: all)") + + # -- check -- + p_check = sub.add_parser("check", help="Run Agda type-checking on certificates") + p_check.add_argument("-j", "--jobs", type=int, default=1, + help="Parallel Agda processes (default: 1)") + p_check.add_argument("--force", action="store_true", + help="Re-check all certificates, even those already checked. " + "Also deletes Agda _build directories to force a clean rebuild.") + p_check.add_argument("-o", "--output", type=Path, default=DEFAULT_CERT_DIR, + help="Certificate directory to scan") + p_check.add_argument("pattern", nargs="?", default=DEFAULT_PATTERN, + help="Glob pattern to filter certificate directories") + + # -- status -- + p_status = sub.add_parser("status", help="Show summary of current certificates (read-only)") + p_status.add_argument("-o", "--output", type=Path, default=DEFAULT_CERT_DIR, + help="Certificate directory to scan") + p_status.add_argument("pattern", nargs="?", default=DEFAULT_PATTERN, + help="Glob pattern to filter certificate directories") + + # -- clean -- + p_clean = sub.add_parser("clean", help="Remove certificate directories") + p_clean.add_argument("-o", "--output", type=Path, default=DEFAULT_CERT_DIR, + help="Certificate directory") + p_clean.add_argument("pattern", nargs="?", default=DEFAULT_PATTERN, + help="Glob pattern to filter which directories to remove") + + # -- run -- + p_run = sub.add_parser("run", help="Full pipeline (build + check)") + p_run.add_argument("--clean", action="store_true", help="Run cabal clean before building") + p_run.add_argument("-j", "--jobs", type=int, default=8, + help="Parallel Agda processes (default: 8)") + p_run.add_argument("--force", action="store_true", + help="Re-check all certificates, even those already checked. " + "Also deletes Agda _build directories to force a clean rebuild.") + p_run.add_argument("-o", "--output", type=Path, default=DEFAULT_CERT_DIR, + help="Certificate output directory") + p_run.add_argument("targets", nargs="*", help="Cabal targets (default: all)") + + return parser + + +# --------------------------------------------------------------------------- +# Main +# --------------------------------------------------------------------------- + +def main() -> None: + parser = make_parser() + args = parser.parse_args() + + dispatch = { + "build": cmd_build, + "check": cmd_check, + "status": cmd_status, + "clean": cmd_clean, + "run": cmd_run, + } + + rc = dispatch[args.command](args) + sys.exit(rc) + + +if __name__ == "__main__": + main()