From c4ce2d0c965e80ad037ea8c090f839148a0700fd Mon Sep 17 00:00:00 2001 From: zeme Date: Wed, 11 Mar 2026 08:53:29 +0100 Subject: [PATCH 1/6] wio --- .github/workflows/plinth-certifier-tests.yml | 46 ++ .gitignore | 1 + plutus-executables/executables/uplc/Main.hs | 2 +- plutus-metatheory/src/Certifier.hs | 27 +- plutus-tx-plugin/plutus-tx-plugin.cabal | 2 + .../src/PlutusTx/Compiler/Expr.hs | 1 + plutus-tx-plugin/src/PlutusTx/Options.hs | 28 +- .../src/PlutusTx/Plugin/Common.hs | 228 ++++++-- plutus-tx/src/PlutusTx/TH.hs | 16 +- scripts/plinth-certifier-tests.py | 527 ++++++++++++++++++ 10 files changed, 793 insertions(+), 85 deletions(-) create mode 100644 .github/workflows/plinth-certifier-tests.yml create mode 100755 scripts/plinth-certifier-tests.py 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/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/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..73fbc1ea85a 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 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..1908ad13a08 100644 --- a/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs +++ b/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs @@ -68,6 +68,7 @@ import GHC.Tc.Types qualified as GHC import GHC.Tc.Types.Evidence qualified as GHC import GHC.Tc.Utils.Env qualified as GHC import GHC.Tc.Utils.Monad qualified as GHC +import GHC.Types.Tickish qualified as GHC import GHC.Types.TyThing qualified as GHC import GHC.Unit.Finder qualified as GHC @@ -82,6 +83,7 @@ import Data.ByteString qualified as BS import Data.ByteString.Unsafe qualified as BSUnsafe import Data.Either.Validation import Data.Generics.Uniplate.Data +import Data.List (intercalate) import Data.Map qualified as Map import Data.Maybe (mapMaybe, maybeToList) import Data.Monoid.Extra (mwhen) @@ -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 (doesFileExist, getCurrentDirectory, makeAbsolute) +import System.FilePath (isRelative, 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] @@ -336,14 +341,17 @@ mkPluginPass markerTHName opts = GHC.CoreDoPluginPass "Core to PLC" $ \guts -> d case (maybeMarkerName, maybeanchorGhcName) of -- See Note [Marker resolution] (Just markerName, Just anchorGhcName) -> - let pctx = + let thisModule = GHC.mg_module guts + pkgName = stripUnitVersion (GHC.unitString (GHC.moduleUnit 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 @@ -474,54 +482,67 @@ resulting 'CompiledCode' because that's impredicative polymorphism. {-| Compiles all the core-expressions surrounded by the marker in the given expression into PLC literals. -} compileMarkedExprs :: GHC.CoreExpr -> PluginM PLC.DefaultUni PLC.DefaultFun GHC.CoreExpr -compileMarkedExprs expr = do - markerName <- asks pcMarkerName - anchorGhcName <- asks pcAnchorName - case expr of - -- This clause is for the `plc` marker. It can be removed when we remove `plc`. - GHC.App - ( GHC.App +compileMarkedExprs = go "" + where + go lastLoc expr = do + markerName <- asks pcMarkerName + anchorGhcName <- asks pcAnchorName + case expr of + -- This clause is for the `plc` marker. It can be removed when we remove `plc`. + GHC.App ( GHC.App ( GHC.App - -- function id - -- sometimes GHCi sticks ticks around this for some reason - (stripTicks -> (GHC.Var fid)) - -- first type argument, must be a string literal type - (GHC.Type (GHC.isStrLitTy -> Just fs_locStr)) + ( GHC.App + -- function id + -- sometimes GHCi sticks ticks around this for some reason + (stripTicks -> (GHC.Var fid)) + -- first type argument, must be a string literal type + (GHC.Type (GHC.isStrLitTy -> Just fs_locStr)) + ) + -- second type argument + (GHC.Type codeTy) ) - -- second type argument - (GHC.Type codeTy) + _ ) - _ - ) - -- value argument - inner - | markerName == GHC.idName fid -> compileMarkedExprOrDefer (show fs_locStr) codeTy inner - GHC.App - ( GHC.App - (stripAnchors anchorGhcName -> (GHC.Var fid)) - (stripAnchors anchorGhcName -> GHC.Type codeTy) - ) - -- code to be compiled - inner - | markerName == GHC.idName fid -> compileMarkedExprOrDefer "" codeTy inner - e@(GHC.Var fid) - | markerName == GHC.idName fid -> - throwError . NoContext . InvalidMarkerError . GHC.showSDocUnsafe $ GHC.ppr e - GHC.App e a -> GHC.App <$> compileMarkedExprs e <*> compileMarkedExprs a - GHC.Lam b e -> GHC.Lam b <$> compileMarkedExprs e - GHC.Let bnd e -> GHC.Let <$> compileBind bnd <*> compileMarkedExprs e - GHC.Case e b t alts -> do - e' <- compileMarkedExprs e - let expAlt (GHC.Alt a bs rhs) = GHC.Alt a bs <$> compileMarkedExprs rhs - 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 - e@(GHC.Coercion _) -> pure e - e@(GHC.Lit _) -> pure e - e@(GHC.Var _) -> pure e - e@(GHC.Type _) -> pure e + -- value argument + inner + | markerName == GHC.idName fid -> compileMarkedExprOrDefer (GHC.unpackFS fs_locStr) codeTy inner + GHC.App + ( GHC.App + (stripAnchorsKeepLoc anchorGhcName -> (ancLocStr, GHC.Var fid)) + (stripAnchors anchorGhcName -> GHC.Type codeTy) + ) + -- code to be compiled + inner + | markerName == GHC.idName fid -> + -- Use anchor location if available, otherwise fall back to the + -- nearest enclosing source tick. + let locStr = if null ancLocStr then lastLoc else ancLocStr + in compileMarkedExprOrDefer locStr codeTy inner + e@(GHC.Var fid) + | markerName == GHC.idName fid -> + throwError . NoContext . InvalidMarkerError . GHC.showSDocUnsafe $ GHC.ppr e + GHC.App e a -> GHC.App <$> go lastLoc e <*> go lastLoc a + GHC.Lam b e -> GHC.Lam b <$> go lastLoc e + GHC.Let bnd e -> GHC.Let <$> compileBind' bnd <*> go lastLoc e + GHC.Case e b t alts -> do + e' <- go lastLoc e + let expAlt (GHC.Alt a bs rhs) = GHC.Alt a bs <$> go lastLoc rhs + alts' <- mapM expAlt alts + pure $ GHC.Case e' b t alts' + GHC.Cast e c -> flip GHC.Cast c <$> go lastLoc e + GHC.Tick tick e -> + let loc' = case tick of + GHC.SourceNote {GHC.sourceSpan = sp} -> encodeSrcSpan sp + _ -> lastLoc + in GHC.Tick tick <$> go loc' e + e@(GHC.Coercion _) -> pure e + e@(GHC.Lit _) -> pure e + e@(GHC.Var _) -> pure e + e@(GHC.Type _) -> pure e + + compileBind' (GHC.NonRec b rhs) = GHC.NonRec b <$> go "" rhs + compileBind' (GHC.Rec binds) = GHC.Rec <$> mapM (\(b, rhs) -> fmap (\r -> (b, r)) (go "" rhs)) binds {-| Behaves the same as 'compileMarkedExpr', unless a compilation error occurs ; if a compilation error happens and the 'defer-errors' option is turned on, @@ -555,11 +576,12 @@ and return a core expression which evaluates to the compiled plc AST as a serial 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 +compileMarkedExpr locStr 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 @@ -623,7 +645,7 @@ compileMarkedExpr _locStr codeTy origE = do ((pirP, uplcP), covIdx) <- runWriterT . runQuoteT . flip runReaderT ctx . flip evalStateT st $ - runCompiler moduleNameStr opts origE' + runCompiler packageName moduleNameStr locStr opts origE' -- serialize the PIR, PLC, and coverageindex outputs into a bytestring. bsPir <- makeByteStringLiteral $ flat pirP @@ -654,10 +676,12 @@ runCompiler , MonadIO m ) => String + -> String + -> String -> PluginOptions -> GHC.CoreExpr -> m (PIRProgram uni fun, UPLCProgram uni fun) -runCompiler moduleName opts expr = do +runCompiler packageName moduleName locStr opts expr = do GHC.DynFlags {GHC.extensions = extensions} <- asks ccFlags let enabledExtensions = @@ -812,17 +836,10 @@ 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 -> liftIO $ generateCertificate simplTrace certifyPath dbP <- liftExcept $ modifyError PLC.FreeVariableErrorE $ traverseOf UPLC.progTerm UPLC.deBruijnTerm uplcP when (opts ^. posDumpUPlc) . liftIO $ @@ -848,6 +865,86 @@ runCompiler moduleName opts expr = do getSrcSpans :: PIR.Provenance Ann -> SrcSpans getSrcSpans = SrcSpans . Set.unions . fmap (unSrcSpans . annSrcSpans) . toList + generateCertificate simplTrace certifyPath = do + -- Absolutize the path relative to the project root (not CWD, which + -- cabal sets per-package), so all certificates land in one place. + absCertifyPath <- + if null certifyPath + then pure "" + else + if isRelative certifyPath + then do + root <- findProjectRoot + pure (root certifyPath) + else pure certifyPath + let sanitise c = if c == '.' Prelude.|| c == '-' then '_' else c + certName = map sanitise packageName ++ "_" ++ map sanitise moduleName + locTag = case decodeSrcSpan locStr 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 decodeSrcSpan locStr 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 + +{-| Strip version and hash suffixes from a GHC unit ID string. +E.g. @"plutus-tx-plugin-1.59.0.0-inplace"@ becomes @"plutus-tx-plugin"@, +@"plutus-tx-plugin-1.59.0.0"@ becomes @"plutus-tx-plugin"@. +If the string has no version suffix (e.g. @"main"@), it is returned as-is. -} +stripUnitVersion :: String -> String +stripUnitVersion = go [] + where + -- Split on '-' and collect segments. The package name is everything + -- before the first segment that looks like a version (starts with a digit). + go acc [] = intercalate "-" (reverse acc) + go acc s = + let (seg, rest) = break (== '-') s + rest' = drop 1 rest -- skip the '-' + in case seg of + (c : _) + | c >= '0' Prelude.&& c <= '9' -> + if null acc then s else intercalate "-" (reverse acc) + _ -> go (seg : acc) rest' + +{-| Walk up from the current directory looking for @cabal.project@ to find the +project root. Falls back to 'makeAbsolute' of @"."@ if none is found. -} +findProjectRoot :: IO FilePath +findProjectRoot = getCurrentDirectory >>= go + where + go dir = do + exists <- doesFileExist (dir "cabal.project") + if exists + then pure dir + else + let parent = takeDirectory dir + in if parent == dir + then makeAbsolute "." -- fallback: no cabal.project found + else go parent + -- | 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 @@ -900,6 +997,21 @@ stripAnchors marker = \case | GHC.getName f == marker -> stripAnchors marker code other -> other +-- | Like 'stripAnchors' but also extracts the first anchor location string. +stripAnchorsKeepLoc :: GHC.Name -> GHC.CoreExpr -> (String, GHC.CoreExpr) +stripAnchorsKeepLoc marker = go "" + where + go loc = \case + GHC.Tick _ e -> go loc e + GHC.App (GHC.App (GHC.App (GHC.Var f) locArg) _codeTy) code + | GHC.getName f == marker -> + let loc' = case locArg of + GHC.Type (GHC.LitTy (GHC.StrTyLit locFs)) -> + if null loc then GHC.unpackFS locFs else loc + _ -> loc + in go loc' code + other -> (loc, other) + -- | Helper to avoid doing too much construction of Core ourselves mkCompiledCode :: forall a. BS.ByteString -> BS.ByteString -> BS.ByteString -> CompiledCode a mkCompiledCode plcBS pirBS ci = SerializedCode plcBS (Just pirBS) (fold . unflat $ ci) 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..f1e12dc7bac --- /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=8, + help="Parallel Agda processes (default: 8)") + 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() From f8115f97935509c33bfb92eeb3b6529a65865c38 Mon Sep 17 00:00:00 2001 From: zeme Date: Wed, 11 Mar 2026 08:52:46 +0100 Subject: [PATCH 2/6] Done --- .../src/PlutusTx/Compiler/Expr.hs | 81 +++++++------- .../src/PlutusTx/Compiler/Expr.hs-boot | 2 +- .../src/PlutusTx/Compiler/Types.hs | 1 + .../src/PlutusTx/Plugin/Common.hs | 104 ++++++++++-------- scripts/plinth-certifier-tests.py | 4 +- 5 files changed, 103 insertions(+), 89 deletions(-) diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs index 73fbc1ea85a..da5f411f865 100644 --- a/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs +++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs @@ -327,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 @@ -655,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' @@ -871,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. @@ -886,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 @@ -894,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 @@ -975,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 @@ -991,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 -> @@ -1001,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. @@ -1010,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 -> @@ -1027,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 @@ -1115,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 @@ -1135,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` _ -> @@ -1165,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 $ @@ -1228,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. @@ -1244,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 @@ -1257,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 -> @@ -1297,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" @@ -1347,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' @@ -1386,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 @@ -1407,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" @@ -1577,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 @@ -1706,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..dd5fa0b3d82 100644 --- a/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs +++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs @@ -68,6 +68,7 @@ data CompileContext uni fun = CompileContext , ccDebugTraceOn :: Bool , ccRewriteRules :: PIR.RewriteRules uni fun , ccSafeToInline :: Bool + , ccCurrentLoc :: Maybe GHC.RealSrcSpan } data CompileState = CompileState diff --git a/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs b/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs index 1908ad13a08..89f78d7425d 100644 --- a/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs +++ b/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs @@ -48,6 +48,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 @@ -638,6 +639,7 @@ compileMarkedExpr locStr codeTy origE = do , ccDebugTraceOn = _posDumpCompilationTrace opts , ccRewriteRules = makeRewriteRules opts , ccSafeToInline = False + , ccCurrentLoc = Nothing } st = CompileState 0 mempty -- See Note [Occurrence analysis] @@ -839,7 +841,9 @@ runCompiler packageName moduleName locStr opts expr = do (uplcP, simplTrace) <- flip runReaderT plcOpts $ PLC.compileProgramWithTrace plcP case opts ^. posCertify of Nothing -> pure () - Just certifyPath -> liftIO $ generateCertificate simplTrace certifyPath + Just certifyPath -> + liftIO $ + generateCertificate packageName moduleName locStr opts simplTrace certifyPath dbP <- liftExcept $ modifyError PLC.FreeVariableErrorE $ traverseOf UPLC.progTerm UPLC.deBruijnTerm uplcP when (opts ^. posDumpUPlc) . liftIO $ @@ -865,51 +869,59 @@ runCompiler packageName moduleName locStr opts expr = do getSrcSpans :: PIR.Provenance Ann -> SrcSpans getSrcSpans = SrcSpans . Set.unions . fmap (unSrcSpans . annSrcSpans) . toList - generateCertificate simplTrace certifyPath = do - -- Absolutize the path relative to the project root (not CWD, which - -- cabal sets per-package), so all certificates land in one place. - absCertifyPath <- - if null certifyPath - then pure "" - else - if isRelative certifyPath - then do - root <- findProjectRoot - pure (root certifyPath) - else pure certifyPath - let sanitise c = if c == '.' Prelude.|| c == '-' then '_' else c - certName = map sanitise packageName ++ "_" ++ map sanitise moduleName - locTag = case decodeSrcSpan locStr 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 decodeSrcSpan locStr 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 +generateCertificate + :: String + -> String + -> String + -> PluginOptions + -> SimplifierTrace PLC.Name PLC.DefaultUni PLC.DefaultFun a + -> String + -> IO () +generateCertificate packageName moduleName locStr opts simplTrace certifyPath = do + -- Absolutize the path relative to the project root (not CWD, which + -- cabal sets per-package), so all certificates land in one place. + absCertifyPath <- + if null certifyPath + then pure "" + else + if isRelative certifyPath + then do + root <- findProjectRoot + pure (root certifyPath) + else pure certifyPath + let sanitise c = if c == '.' Prelude.|| c == '-' then '_' else c + certName = map sanitise packageName ++ "_" ++ map sanitise moduleName + locTag = case decodeSrcSpan locStr 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 decodeSrcSpan locStr 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 {-| Strip version and hash suffixes from a GHC unit ID string. E.g. @"plutus-tx-plugin-1.59.0.0-inplace"@ becomes @"plutus-tx-plugin"@, diff --git a/scripts/plinth-certifier-tests.py b/scripts/plinth-certifier-tests.py index f1e12dc7bac..2442911e4f2 100755 --- a/scripts/plinth-certifier-tests.py +++ b/scripts/plinth-certifier-tests.py @@ -464,8 +464,8 @@ def make_parser() -> argparse.ArgumentParser: # -- check -- p_check = sub.add_parser("check", help="Run Agda type-checking on certificates") - p_check.add_argument("-j", "--jobs", type=int, default=8, - help="Parallel Agda processes (default: 8)") + 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.") From f1f1c5bc43554ed5791c7413a8d95b8d1b48562f Mon Sep 17 00:00:00 2001 From: zeme Date: Wed, 11 Mar 2026 09:39:21 +0100 Subject: [PATCH 3/6] wiop --- .../src/PlutusTx/Plugin/Common.hs | 138 +++++++----------- 1 file changed, 56 insertions(+), 82 deletions(-) diff --git a/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs b/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs index 89f78d7425d..24278335e6e 100644 --- a/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs +++ b/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs @@ -69,7 +69,6 @@ import GHC.Tc.Types qualified as GHC import GHC.Tc.Types.Evidence qualified as GHC import GHC.Tc.Utils.Env qualified as GHC import GHC.Tc.Utils.Monad qualified as GHC -import GHC.Types.Tickish qualified as GHC import GHC.Types.TyThing qualified as GHC import GHC.Unit.Finder qualified as GHC @@ -84,7 +83,6 @@ import Data.ByteString qualified as BS import Data.ByteString.Unsafe qualified as BSUnsafe import Data.Either.Validation import Data.Generics.Uniplate.Data -import Data.List (intercalate) import Data.Map qualified as Map import Data.Maybe (mapMaybe, maybeToList) import Data.Monoid.Extra (mwhen) @@ -341,9 +339,13 @@ 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) -> + (Just markerName, Just anchorGhcName) -> do + hscEnv <- GHC.getHscEnv let thisModule = GHC.mg_module guts - pkgName = stripUnitVersion (GHC.unitString (GHC.moduleUnit thisModule)) + unitState = GHC.hsc_units hscEnv + pkgName = case GHC.lookupUnit unitState (GHC.moduleUnit thisModule) of + Just unitInfo -> GHC.unitPackageNameString unitInfo + Nothing -> GHC.unitString (GHC.moduleUnit thisModule) pctx = PluginCtx { pcOpts = opts @@ -354,8 +356,8 @@ mkPluginPass markerTHName opts = GHC.CoreDoPluginPass "Core to PLC" $ \guts -> d , 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. @@ -483,67 +485,58 @@ resulting 'CompiledCode' because that's impredicative polymorphism. {-| Compiles all the core-expressions surrounded by the marker in the given expression into PLC literals. -} compileMarkedExprs :: GHC.CoreExpr -> PluginM PLC.DefaultUni PLC.DefaultFun GHC.CoreExpr -compileMarkedExprs = go "" - where - go lastLoc expr = do - markerName <- asks pcMarkerName - anchorGhcName <- asks pcAnchorName - case expr of - -- This clause is for the `plc` marker. It can be removed when we remove `plc`. - GHC.App +compileMarkedExprs expr = do + markerName <- asks pcMarkerName + anchorGhcName <- asks pcAnchorName + case expr of + -- This clause is for the `plc` marker. It can be removed when we remove `plc`. + GHC.App + ( GHC.App ( GHC.App ( GHC.App - ( GHC.App - -- function id - -- sometimes GHCi sticks ticks around this for some reason - (stripTicks -> (GHC.Var fid)) - -- first type argument, must be a string literal type - (GHC.Type (GHC.isStrLitTy -> Just fs_locStr)) - ) - -- second type argument - (GHC.Type codeTy) + -- function id + -- sometimes GHCi sticks ticks around this for some reason + (stripTicks -> (GHC.Var fid)) + -- first type argument, must be a string literal type + (GHC.Type (GHC.isStrLitTy -> Just fs_locStr)) ) - _ - ) - -- value argument - inner - | markerName == GHC.idName fid -> compileMarkedExprOrDefer (GHC.unpackFS fs_locStr) codeTy inner - GHC.App - ( GHC.App - (stripAnchorsKeepLoc anchorGhcName -> (ancLocStr, GHC.Var fid)) - (stripAnchors anchorGhcName -> GHC.Type codeTy) + -- second type argument + (GHC.Type codeTy) ) - -- code to be compiled - inner - | markerName == GHC.idName fid -> - -- Use anchor location if available, otherwise fall back to the - -- nearest enclosing source tick. - let locStr = if null ancLocStr then lastLoc else ancLocStr - in compileMarkedExprOrDefer locStr codeTy inner - e@(GHC.Var fid) - | markerName == GHC.idName fid -> - throwError . NoContext . InvalidMarkerError . GHC.showSDocUnsafe $ GHC.ppr e - GHC.App e a -> GHC.App <$> go lastLoc e <*> go lastLoc a - GHC.Lam b e -> GHC.Lam b <$> go lastLoc e - GHC.Let bnd e -> GHC.Let <$> compileBind' bnd <*> go lastLoc e - GHC.Case e b t alts -> do - e' <- go lastLoc e - let expAlt (GHC.Alt a bs rhs) = GHC.Alt a bs <$> go lastLoc rhs - alts' <- mapM expAlt alts - pure $ GHC.Case e' b t alts' - GHC.Cast e c -> flip GHC.Cast c <$> go lastLoc e - GHC.Tick tick e -> - let loc' = case tick of - GHC.SourceNote {GHC.sourceSpan = sp} -> encodeSrcSpan sp - _ -> lastLoc - in GHC.Tick tick <$> go loc' e - e@(GHC.Coercion _) -> pure e - e@(GHC.Lit _) -> pure e - e@(GHC.Var _) -> pure e - e@(GHC.Type _) -> pure e - - compileBind' (GHC.NonRec b rhs) = GHC.NonRec b <$> go "" rhs - compileBind' (GHC.Rec binds) = GHC.Rec <$> mapM (\(b, rhs) -> fmap (\r -> (b, r)) (go "" rhs)) binds + _ + ) + -- value argument + inner + | markerName == GHC.idName fid -> compileMarkedExprOrDefer (GHC.unpackFS fs_locStr) codeTy inner + GHC.App + ( GHC.App + (stripAnchorsKeepLoc anchorGhcName -> (ancLocStr, GHC.Var fid)) + (stripAnchors anchorGhcName -> GHC.Type codeTy) + ) + -- code to be compiled + inner + | markerName == GHC.idName fid -> + compileMarkedExprOrDefer ancLocStr codeTy inner + e@(GHC.Var fid) + | markerName == GHC.idName fid -> + throwError . NoContext . InvalidMarkerError . GHC.showSDocUnsafe $ GHC.ppr e + GHC.App e a -> GHC.App <$> compileMarkedExprs e <*> compileMarkedExprs a + GHC.Lam b e -> GHC.Lam b <$> compileMarkedExprs e + GHC.Let bnd e -> GHC.Let <$> compileBind' bnd <*> compileMarkedExprs e + GHC.Case e b t alts -> do + e' <- compileMarkedExprs e + let expAlt (GHC.Alt a bs rhs) = GHC.Alt a bs <$> compileMarkedExprs rhs + alts' <- mapM expAlt alts + pure $ GHC.Case e' b t alts' + GHC.Cast e c -> flip GHC.Cast c <$> 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 + e@(GHC.Type _) -> pure e + where + compileBind' (GHC.NonRec b rhs) = GHC.NonRec b <$> compileMarkedExprs rhs + compileBind' (GHC.Rec binds) = GHC.Rec <$> mapM (\(b, rhs) -> fmap (\r -> (b, r)) (compileMarkedExprs rhs)) binds {-| Behaves the same as 'compileMarkedExpr', unless a compilation error occurs ; if a compilation error happens and the 'defer-errors' option is turned on, @@ -923,25 +916,6 @@ generateCertificate packageName moduleName locStr opts simplTrace certifyPath = writeFile (certDir "plinth-certifier-FAIL.txt") (errMsg ++ "\n") hPutStrLn stderr $ "Certifier result: FAIL — " ++ certDir ++ "\n" ++ errMsg -{-| Strip version and hash suffixes from a GHC unit ID string. -E.g. @"plutus-tx-plugin-1.59.0.0-inplace"@ becomes @"plutus-tx-plugin"@, -@"plutus-tx-plugin-1.59.0.0"@ becomes @"plutus-tx-plugin"@. -If the string has no version suffix (e.g. @"main"@), it is returned as-is. -} -stripUnitVersion :: String -> String -stripUnitVersion = go [] - where - -- Split on '-' and collect segments. The package name is everything - -- before the first segment that looks like a version (starts with a digit). - go acc [] = intercalate "-" (reverse acc) - go acc s = - let (seg, rest) = break (== '-') s - rest' = drop 1 rest -- skip the '-' - in case seg of - (c : _) - | c >= '0' Prelude.&& c <= '9' -> - if null acc then s else intercalate "-" (reverse acc) - _ -> go (seg : acc) rest' - {-| Walk up from the current directory looking for @cabal.project@ to find the project root. Falls back to 'makeAbsolute' of @"."@ if none is found. -} findProjectRoot :: IO FilePath From 4dab3ec74ad07253faaa42d3b8f3800371dfba79 Mon Sep 17 00:00:00 2001 From: zeme Date: Wed, 11 Mar 2026 12:35:23 +0100 Subject: [PATCH 4/6] done --- plutus-executables/inc-168982000/inc.agda-lib | 5 + .../inc-168982000/src/Ast0.agda | 22 ++++ .../inc-168982000/src/Ast1.agda | 22 ++++ .../inc-168982000/src/Ast2.agda | 22 ++++ .../inc-168982000/src/Ast3.agda | 22 ++++ .../inc-168982000/src/Ast4.agda | 22 ++++ .../inc-168982000/src/Ast5.agda | 22 ++++ .../inc-168982000/src/Ast6.agda | 22 ++++ plutus-executables/inc-168982000/src/inc.agda | 35 ++++++ .../src/PlutusTx/Compiler/Types.hs | 3 + .../src/PlutusTx/Compiler/Utils.hs | 22 ++++ .../src/PlutusTx/Plugin/Common.hs | 110 ++++++------------ 12 files changed, 256 insertions(+), 73 deletions(-) create mode 100644 plutus-executables/inc-168982000/inc.agda-lib create mode 100644 plutus-executables/inc-168982000/src/Ast0.agda create mode 100644 plutus-executables/inc-168982000/src/Ast1.agda create mode 100644 plutus-executables/inc-168982000/src/Ast2.agda create mode 100644 plutus-executables/inc-168982000/src/Ast3.agda create mode 100644 plutus-executables/inc-168982000/src/Ast4.agda create mode 100644 plutus-executables/inc-168982000/src/Ast5.agda create mode 100644 plutus-executables/inc-168982000/src/Ast6.agda create mode 100644 plutus-executables/inc-168982000/src/inc.agda diff --git a/plutus-executables/inc-168982000/inc.agda-lib b/plutus-executables/inc-168982000/inc.agda-lib new file mode 100644 index 00000000000..bc5f355ca1c --- /dev/null +++ b/plutus-executables/inc-168982000/inc.agda-lib @@ -0,0 +1,5 @@ +name: inc +depend: + standard-library-2.1.1 + plutus-metatheory +include: src \ No newline at end of file diff --git a/plutus-executables/inc-168982000/src/Ast0.agda b/plutus-executables/inc-168982000/src/Ast0.agda new file mode 100644 index 00000000000..6e4d67dc566 --- /dev/null +++ b/plutus-executables/inc-168982000/src/Ast0.agda @@ -0,0 +1,22 @@ +module Ast0 where + +open import VerifiedCompilation +open import VerifiedCompilation.Certificate +open import Untyped +open import RawU +open import Builtin +open import Data.Unit +open import Data.Nat +open import Data.Integer +open import Utils +import Agda.Builtin.Bool +import Relation.Nullary +import VerifiedCompilation.UntypedTranslation +open import Agda.Builtin.Maybe +open import Data.Empty using (⊥) +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) + +ast0 : Untyped + +ast0 = (UApp (ULambda (UForce (UVar 0))) (UDelay (ULambda (UApp (ULambda (UApp (UApp (UApp (UForce (UApp (ULambda (UForce (UVar 0))) (UDelay (UDelay (ULambda (UVar 0)))))) (UApp (ULambda (UApp (ULambda (UApp (ULambda (UForce (UVar 0))) (UDelay (UForce (UVar 0))))) (UDelay (ULambda (UApp (ULambda (ULambda (UApp (ULambda (UApp (UApp (UVar 4) (UVar 2)) (UVar 0))) (UVar 0)))) (UVar 0)))))) (UBuiltin addInteger))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) (UVar 0))))) diff --git a/plutus-executables/inc-168982000/src/Ast1.agda b/plutus-executables/inc-168982000/src/Ast1.agda new file mode 100644 index 00000000000..d50bfa9cfff --- /dev/null +++ b/plutus-executables/inc-168982000/src/Ast1.agda @@ -0,0 +1,22 @@ +module Ast1 where + +open import VerifiedCompilation +open import VerifiedCompilation.Certificate +open import Untyped +open import RawU +open import Builtin +open import Data.Unit +open import Data.Nat +open import Data.Integer +open import Utils +import Agda.Builtin.Bool +import Relation.Nullary +import VerifiedCompilation.UntypedTranslation +open import Agda.Builtin.Maybe +open import Data.Empty using (⊥) +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) + +ast1 : Untyped + +ast1 = (UApp (ULambda (UForce (UDelay (UVar 0)))) (ULambda (UApp (ULambda (UApp (UApp (UApp (UForce (UApp (ULambda (UForce (UDelay (UVar 0)))) (UDelay (ULambda (UVar 0))))) (UApp (ULambda (UApp (ULambda (UApp (ULambda (UForce (UVar 0))) (UDelay (UForce (UDelay (UVar 0)))))) (ULambda (UApp (ULambda (ULambda (UApp (ULambda (UApp (UApp (UVar 4) (UVar 2)) (UVar 0))) (UVar 0)))) (UVar 0))))) (UBuiltin addInteger))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) (UVar 0)))) diff --git a/plutus-executables/inc-168982000/src/Ast2.agda b/plutus-executables/inc-168982000/src/Ast2.agda new file mode 100644 index 00000000000..4842983c985 --- /dev/null +++ b/plutus-executables/inc-168982000/src/Ast2.agda @@ -0,0 +1,22 @@ +module Ast2 where + +open import VerifiedCompilation +open import VerifiedCompilation.Certificate +open import Untyped +open import RawU +open import Builtin +open import Data.Unit +open import Data.Nat +open import Data.Integer +open import Utils +import Agda.Builtin.Bool +import Relation.Nullary +import VerifiedCompilation.UntypedTranslation +open import Agda.Builtin.Maybe +open import Data.Empty using (⊥) +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) + +ast2 : Untyped + +ast2 = (UApp (ULambda (UVar 0)) (ULambda (UApp (ULambda (UApp (UApp (UApp (UForce (UApp (ULambda (UVar 0)) (UDelay (ULambda (UVar 0))))) (UApp (ULambda (UApp (ULambda (UApp (ULambda (UForce (UVar 0))) (UDelay (UVar 0)))) (ULambda (UApp (ULambda (ULambda (UApp (ULambda (UApp (UApp (UVar 4) (UVar 2)) (UVar 0))) (UVar 0)))) (UVar 0))))) (UBuiltin addInteger))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) (UVar 0)))) diff --git a/plutus-executables/inc-168982000/src/Ast3.agda b/plutus-executables/inc-168982000/src/Ast3.agda new file mode 100644 index 00000000000..e43c8ec9aad --- /dev/null +++ b/plutus-executables/inc-168982000/src/Ast3.agda @@ -0,0 +1,22 @@ +module Ast3 where + +open import VerifiedCompilation +open import VerifiedCompilation.Certificate +open import Untyped +open import RawU +open import Builtin +open import Data.Unit +open import Data.Nat +open import Data.Integer +open import Utils +import Agda.Builtin.Bool +import Relation.Nullary +import VerifiedCompilation.UntypedTranslation +open import Agda.Builtin.Maybe +open import Data.Empty using (⊥) +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) + +ast3 : Untyped + +ast3 = (ULambda (UApp (UApp (UApp (UForce (UDelay (ULambda (UVar 0)))) (UForce (UDelay (ULambda (ULambda (UApp (UApp (UBuiltin addInteger) (UVar 1)) (UVar 0))))))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) diff --git a/plutus-executables/inc-168982000/src/Ast4.agda b/plutus-executables/inc-168982000/src/Ast4.agda new file mode 100644 index 00000000000..9b158f9a1c4 --- /dev/null +++ b/plutus-executables/inc-168982000/src/Ast4.agda @@ -0,0 +1,22 @@ +module Ast4 where + +open import VerifiedCompilation +open import VerifiedCompilation.Certificate +open import Untyped +open import RawU +open import Builtin +open import Data.Unit +open import Data.Nat +open import Data.Integer +open import Utils +import Agda.Builtin.Bool +import Relation.Nullary +import VerifiedCompilation.UntypedTranslation +open import Agda.Builtin.Maybe +open import Data.Empty using (⊥) +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) + +ast4 : Untyped + +ast4 = (ULambda (UApp (UApp (UApp (ULambda (UVar 0)) (ULambda (ULambda (UApp (UApp (UBuiltin addInteger) (UVar 1)) (UVar 0))))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) diff --git a/plutus-executables/inc-168982000/src/Ast5.agda b/plutus-executables/inc-168982000/src/Ast5.agda new file mode 100644 index 00000000000..a49f6680097 --- /dev/null +++ b/plutus-executables/inc-168982000/src/Ast5.agda @@ -0,0 +1,22 @@ +module Ast5 where + +open import VerifiedCompilation +open import VerifiedCompilation.Certificate +open import Untyped +open import RawU +open import Builtin +open import Data.Unit +open import Data.Nat +open import Data.Integer +open import Utils +import Agda.Builtin.Bool +import Relation.Nullary +import VerifiedCompilation.UntypedTranslation +open import Agda.Builtin.Maybe +open import Data.Empty using (⊥) +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) + +ast5 : Untyped + +ast5 = (ULambda (UApp (UApp (ULambda (ULambda (UApp (UApp (UBuiltin addInteger) (UVar 1)) (UVar 0)))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) diff --git a/plutus-executables/inc-168982000/src/Ast6.agda b/plutus-executables/inc-168982000/src/Ast6.agda new file mode 100644 index 00000000000..0373e2190df --- /dev/null +++ b/plutus-executables/inc-168982000/src/Ast6.agda @@ -0,0 +1,22 @@ +module Ast6 where + +open import VerifiedCompilation +open import VerifiedCompilation.Certificate +open import Untyped +open import RawU +open import Builtin +open import Data.Unit +open import Data.Nat +open import Data.Integer +open import Utils +import Agda.Builtin.Bool +import Relation.Nullary +import VerifiedCompilation.UntypedTranslation +open import Agda.Builtin.Maybe +open import Data.Empty using (⊥) +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) + +ast6 : Untyped + +ast6 = (ULambda (UApp (UApp (UBuiltin addInteger) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) diff --git a/plutus-executables/inc-168982000/src/inc.agda b/plutus-executables/inc-168982000/src/inc.agda new file mode 100644 index 00000000000..be0addf1c30 --- /dev/null +++ b/plutus-executables/inc-168982000/src/inc.agda @@ -0,0 +1,35 @@ +module inc where + +open import Certifier +open import VerifiedCompilation +open import VerifiedCompilation.Certificate +open import Untyped +open import RawU +open import Builtin +open import Data.Unit +open import Data.Nat +open import Data.Integer +open import Utils +import Agda.Builtin.Bool +import Relation.Nullary +import VerifiedCompilation.UntypedTranslation +open import Agda.Builtin.List using (_∷_; []) +open import Agda.Builtin.Maybe +open import Data.Empty using (⊥) +open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Ast0 +open import Ast1 +open import Ast2 +open import Ast3 +open import Ast4 +open import Ast5 +open import Ast6 + + + +asts : List (SimplifierTag × Hints × Untyped × Untyped) +asts = ((floatDelayT , (none , (ast0 , ast1))) ∷ (forceCaseDelayT , (none , (ast1 , ast1))) ∷ (forceDelayT , (none , (ast1 , ast2))) ∷ (caseOfCaseT , (none , (ast2 , ast2))) ∷ (caseReduceT , (none , (ast2 , ast2))) ∷ (inlineT , (inline (((ƛ↓ (expand (ƛ ((ƛ↓ ((((force ((ƛ↓ (expand (delay (ƛ var)))) ·↓)) · ((ƛ↓ ((ƛ↓ ((ƛ↓ (force (expand (delay (expand (ƛ ((ƛ↓ (ƛ ((ƛ↓ (((expand builtin) · (expand var)) · (expand var))) ·↓))) ·↓))))))) ·↓)) ·↓)) ·↓)) · con) · (expand var))) ·↓)))) ·↓)) , (ast2 , ast3))) ∷ (floatDelayT , (none , (ast3 , ast3))) ∷ (forceCaseDelayT , (none , (ast3 , ast3))) ∷ (forceDelayT , (none , (ast3 , ast4))) ∷ (caseOfCaseT , (none , (ast4 , ast4))) ∷ (caseReduceT , (none , (ast4 , ast4))) ∷ (inlineT , (inline ((ƛ ((((ƛ↓ (expand (ƛ (ƛ ((builtin · var) · var))))) ·↓) · con) · var))) , (ast4 , ast5))) ∷ (floatDelayT , (none , (ast5 , ast5))) ∷ (forceCaseDelayT , (none , (ast5 , ast5))) ∷ (forceDelayT , (none , (ast5 , ast5))) ∷ (caseOfCaseT , (none , (ast5 , ast5))) ∷ (caseReduceT , (none , (ast5 , ast5))) ∷ (inlineT , (inline ((ƛ (((ƛ↓ (ƛ↓ ((builtin · (expand con)) · (expand var)))) ·↓) ·↓))) , (ast5 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (cseT , (none , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (cseT , (none , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (cseT , (none , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (cseT , (none , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (applyToCaseT , (none , (ast6 , ast6))) ∷ []) + +certificate : passed? (runCertifier asts) ≡ true +certificate = refl diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs index dd5fa0b3d82..c4c8a2d037f 100644 --- a/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs +++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs @@ -69,6 +69,9 @@ data CompileContext uni fun = CompileContext , 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/Plugin/Common.hs b/plutus-tx-plugin/src/PlutusTx/Plugin/Common.hs index 24278335e6e..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 @@ -92,8 +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 (doesFileExist, getCurrentDirectory, makeAbsolute) -import System.FilePath (isRelative, takeDirectory, ()) +import System.Directory (makeAbsolute) +import System.FilePath (takeDirectory, ()) import System.IO (hPutStrLn, openBinaryTempFile, stderr) import System.IO.Unsafe (unsafePerformIO) @@ -342,10 +343,7 @@ mkPluginPass markerTHName opts = GHC.CoreDoPluginPass "Core to PLC" $ \guts -> d (Just markerName, Just anchorGhcName) -> do hscEnv <- GHC.getHscEnv let thisModule = GHC.mg_module guts - unitState = GHC.hsc_units hscEnv - pkgName = case GHC.lookupUnit unitState (GHC.moduleUnit thisModule) of - Just unitInfo -> GHC.unitPackageNameString unitInfo - Nothing -> GHC.unitString (GHC.moduleUnit thisModule) + pkgName = getPackageName hscEnv thisModule pctx = PluginCtx { pcOpts = opts @@ -507,22 +505,23 @@ compileMarkedExprs expr = do ) -- value argument inner - | markerName == GHC.idName fid -> compileMarkedExprOrDefer (GHC.unpackFS fs_locStr) codeTy inner + | markerName == GHC.idName fid -> + compileMarkedExprOrDefer (decodeSrcSpan (GHC.unpackFS fs_locStr)) codeTy inner GHC.App ( GHC.App - (stripAnchorsKeepLoc anchorGhcName -> (ancLocStr, 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 ancLocStr codeTy inner + compileMarkedExprOrDefer mLoc codeTy inner e@(GHC.Var fid) | markerName == GHC.idName fid -> throwError . NoContext . InvalidMarkerError . GHC.showSDocUnsafe $ GHC.ppr e GHC.App e a -> GHC.App <$> compileMarkedExprs e <*> compileMarkedExprs a GHC.Lam b e -> GHC.Lam b <$> compileMarkedExprs e - GHC.Let bnd e -> GHC.Let <$> compileBind' bnd <*> compileMarkedExprs e + GHC.Let bnd e -> GHC.Let <$> compileBind bnd <*> compileMarkedExprs e GHC.Case e b t alts -> do e' <- compileMarkedExprs e let expAlt (GHC.Alt a bs rhs) = GHC.Alt a bs <$> compileMarkedExprs rhs @@ -534,19 +533,16 @@ compileMarkedExprs expr = do e@(GHC.Lit _) -> pure e e@(GHC.Var _) -> pure e e@(GHC.Type _) -> pure e - where - compileBind' (GHC.NonRec b rhs) = GHC.NonRec b <$> compileMarkedExprs rhs - compileBind' (GHC.Rec binds) = GHC.Rec <$> mapM (\(b, rhs) -> fmap (\r -> (b, r)) (compileMarkedExprs rhs)) binds {-| Behaves the same as 'compileMarkedExpr', unless a compilation error occurs ; 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 @@ -569,8 +565,8 @@ 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 @@ -633,6 +629,9 @@ compileMarkedExpr locStr codeTy origE = do , ccRewriteRules = makeRewriteRules opts , ccSafeToInline = False , ccCurrentLoc = Nothing + , ccPackageName = packageName + , ccModuleName = moduleNameStr + , ccSourceLoc = mLoc } st = CompileState 0 mempty -- See Note [Occurrence analysis] @@ -640,7 +639,7 @@ compileMarkedExpr locStr codeTy origE = do ((pirP, uplcP), covIdx) <- runWriterT . runQuoteT . flip runReaderT ctx . flip evalStateT st $ - runCompiler packageName moduleNameStr locStr opts origE' + runCompiler opts origE' -- serialize the PIR, PLC, and coverageindex outputs into a bytestring. bsPir <- makeByteStringLiteral $ flat pirP @@ -670,13 +669,11 @@ runCompiler , MonadError (CompileError uni fun Ann) m , MonadIO m ) - => String - -> String - -> String - -> PluginOptions + => PluginOptions -> GHC.CoreExpr -> m (PIRProgram uni fun, UPLCProgram uni fun) -runCompiler packageName moduleName locStr opts expr = do +runCompiler opts expr = do + moduleName <- asks ccModuleName GHC.DynFlags {GHC.extensions = extensions} <- asks ccFlags let enabledExtensions = @@ -834,9 +831,11 @@ runCompiler packageName moduleName locStr opts expr = do (uplcP, simplTrace) <- flip runReaderT plcOpts $ PLC.compileProgramWithTrace plcP case opts ^. posCertify of Nothing -> pure () - Just certifyPath -> + Just certifyPath -> do + packageName <- asks ccPackageName + mLoc <- asks ccSourceLoc liftIO $ - generateCertificate packageName moduleName locStr opts simplTrace certifyPath + generateCertificate packageName moduleName mLoc opts simplTrace certifyPath dbP <- liftExcept $ modifyError PLC.FreeVariableErrorE $ traverseOf UPLC.progTerm UPLC.deBruijnTerm uplcP when (opts ^. posDumpUPlc) . liftIO $ @@ -865,26 +864,19 @@ runCompiler packageName moduleName locStr opts expr = do generateCertificate :: String -> String - -> String + -> Maybe GHC.RealSrcSpan -> PluginOptions -> SimplifierTrace PLC.Name PLC.DefaultUni PLC.DefaultFun a -> String -> IO () -generateCertificate packageName moduleName locStr opts simplTrace certifyPath = do - -- Absolutize the path relative to the project root (not CWD, which - -- cabal sets per-package), so all certificates land in one place. +generateCertificate packageName moduleName mLoc opts simplTrace certifyPath = do absCertifyPath <- if null certifyPath then pure "" - else - if isRelative certifyPath - then do - root <- findProjectRoot - pure (root certifyPath) - else pure certifyPath + else makeAbsolute certifyPath let sanitise c = if c == '.' Prelude.|| c == '-' then '_' else c certName = map sanitise packageName ++ "_" ++ map sanitise moduleName - locTag = case decodeSrcSpan locStr of + locTag = case mLoc of Just sp -> let line = show (GHC.srcSpanStartLine sp) col = show (GHC.srcSpanStartCol sp) @@ -895,7 +887,7 @@ generateCertificate packageName moduleName locStr opts simplTrace certifyPath = certDir | null absCertifyPath = -- No path given: place next to the source file - case decodeSrcSpan locStr of + case mLoc of Just sp -> let sourceFile = GHC.unpackFS (GHC.srcSpanFile sp) in takeDirectory sourceFile certDirName @@ -916,21 +908,6 @@ generateCertificate packageName moduleName locStr opts simplTrace certifyPath = writeFile (certDir "plinth-certifier-FAIL.txt") (errMsg ++ "\n") hPutStrLn stderr $ "Certifier result: FAIL — " ++ certDir ++ "\n" ++ errMsg -{-| Walk up from the current directory looking for @cabal.project@ to find the -project root. Falls back to 'makeAbsolute' of @"."@ if none is found. -} -findProjectRoot :: IO FilePath -findProjectRoot = getCurrentDirectory >>= go - where - go dir = do - exists <- doesFileExist (dir "cabal.project") - if exists - then pure dir - else - let parent = takeDirectory dir - in if parent == dir - then makeAbsolute "." -- fallback: no cabal.project found - else go parent - -- | 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 @@ -976,27 +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 - --- | Like 'stripAnchors' but also extracts the first anchor location string. -stripAnchorsKeepLoc :: GHC.Name -> GHC.CoreExpr -> (String, GHC.CoreExpr) -stripAnchorsKeepLoc marker = go "" - where - go loc = \case - GHC.Tick _ e -> go loc e - GHC.App (GHC.App (GHC.App (GHC.Var f) locArg) _codeTy) code - | GHC.getName f == marker -> - let loc' = case locArg of - GHC.Type (GHC.LitTy (GHC.StrTyLit locFs)) -> - if null loc then GHC.unpackFS locFs else loc - _ -> loc - in go loc' code - other -> (loc, 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 From 6388626ebc6fb8a4aaefef4f144b283c7daf7938 Mon Sep 17 00:00:00 2001 From: zeme Date: Wed, 11 Mar 2026 12:51:51 +0100 Subject: [PATCH 5/6] wip --- plutus-executables/inc-168982000/inc.agda-lib | 5 --- .../inc-168982000/src/Ast0.agda | 22 ------------ .../inc-168982000/src/Ast1.agda | 22 ------------ .../inc-168982000/src/Ast2.agda | 22 ------------ .../inc-168982000/src/Ast3.agda | 22 ------------ .../inc-168982000/src/Ast4.agda | 22 ------------ .../inc-168982000/src/Ast5.agda | 22 ------------ .../inc-168982000/src/Ast6.agda | 22 ------------ plutus-executables/inc-168982000/src/inc.agda | 35 ------------------- ...0311_120000_agda_certifier_improvements.md | 7 ++++ ...agda_certifier_source_location_tracking.md | 25 +++++++++++++ ...311_120000_agda_certifier_encode_th_loc.md | 6 ++++ 12 files changed, 38 insertions(+), 194 deletions(-) delete mode 100644 plutus-executables/inc-168982000/inc.agda-lib delete mode 100644 plutus-executables/inc-168982000/src/Ast0.agda delete mode 100644 plutus-executables/inc-168982000/src/Ast1.agda delete mode 100644 plutus-executables/inc-168982000/src/Ast2.agda delete mode 100644 plutus-executables/inc-168982000/src/Ast3.agda delete mode 100644 plutus-executables/inc-168982000/src/Ast4.agda delete mode 100644 plutus-executables/inc-168982000/src/Ast5.agda delete mode 100644 plutus-executables/inc-168982000/src/Ast6.agda delete mode 100644 plutus-executables/inc-168982000/src/inc.agda create mode 100644 plutus-metatheory/changelog.d/20260311_120000_agda_certifier_improvements.md create mode 100644 plutus-tx-plugin/changelog.d/20260311_120000_agda_certifier_source_location_tracking.md create mode 100644 plutus-tx/changelog.d/20260311_120000_agda_certifier_encode_th_loc.md diff --git a/plutus-executables/inc-168982000/inc.agda-lib b/plutus-executables/inc-168982000/inc.agda-lib deleted file mode 100644 index bc5f355ca1c..00000000000 --- a/plutus-executables/inc-168982000/inc.agda-lib +++ /dev/null @@ -1,5 +0,0 @@ -name: inc -depend: - standard-library-2.1.1 - plutus-metatheory -include: src \ No newline at end of file diff --git a/plutus-executables/inc-168982000/src/Ast0.agda b/plutus-executables/inc-168982000/src/Ast0.agda deleted file mode 100644 index 6e4d67dc566..00000000000 --- a/plutus-executables/inc-168982000/src/Ast0.agda +++ /dev/null @@ -1,22 +0,0 @@ -module Ast0 where - -open import VerifiedCompilation -open import VerifiedCompilation.Certificate -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) -open import Data.Bool.Base using (Bool; false; true) -open import Agda.Builtin.Equality using (_≡_; refl) - -ast0 : Untyped - -ast0 = (UApp (ULambda (UForce (UVar 0))) (UDelay (ULambda (UApp (ULambda (UApp (UApp (UApp (UForce (UApp (ULambda (UForce (UVar 0))) (UDelay (UDelay (ULambda (UVar 0)))))) (UApp (ULambda (UApp (ULambda (UApp (ULambda (UForce (UVar 0))) (UDelay (UForce (UVar 0))))) (UDelay (ULambda (UApp (ULambda (ULambda (UApp (ULambda (UApp (UApp (UVar 4) (UVar 2)) (UVar 0))) (UVar 0)))) (UVar 0)))))) (UBuiltin addInteger))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) (UVar 0))))) diff --git a/plutus-executables/inc-168982000/src/Ast1.agda b/plutus-executables/inc-168982000/src/Ast1.agda deleted file mode 100644 index d50bfa9cfff..00000000000 --- a/plutus-executables/inc-168982000/src/Ast1.agda +++ /dev/null @@ -1,22 +0,0 @@ -module Ast1 where - -open import VerifiedCompilation -open import VerifiedCompilation.Certificate -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) -open import Data.Bool.Base using (Bool; false; true) -open import Agda.Builtin.Equality using (_≡_; refl) - -ast1 : Untyped - -ast1 = (UApp (ULambda (UForce (UDelay (UVar 0)))) (ULambda (UApp (ULambda (UApp (UApp (UApp (UForce (UApp (ULambda (UForce (UDelay (UVar 0)))) (UDelay (ULambda (UVar 0))))) (UApp (ULambda (UApp (ULambda (UApp (ULambda (UForce (UVar 0))) (UDelay (UForce (UDelay (UVar 0)))))) (ULambda (UApp (ULambda (ULambda (UApp (ULambda (UApp (UApp (UVar 4) (UVar 2)) (UVar 0))) (UVar 0)))) (UVar 0))))) (UBuiltin addInteger))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) (UVar 0)))) diff --git a/plutus-executables/inc-168982000/src/Ast2.agda b/plutus-executables/inc-168982000/src/Ast2.agda deleted file mode 100644 index 4842983c985..00000000000 --- a/plutus-executables/inc-168982000/src/Ast2.agda +++ /dev/null @@ -1,22 +0,0 @@ -module Ast2 where - -open import VerifiedCompilation -open import VerifiedCompilation.Certificate -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) -open import Data.Bool.Base using (Bool; false; true) -open import Agda.Builtin.Equality using (_≡_; refl) - -ast2 : Untyped - -ast2 = (UApp (ULambda (UVar 0)) (ULambda (UApp (ULambda (UApp (UApp (UApp (UForce (UApp (ULambda (UVar 0)) (UDelay (ULambda (UVar 0))))) (UApp (ULambda (UApp (ULambda (UApp (ULambda (UForce (UVar 0))) (UDelay (UVar 0)))) (ULambda (UApp (ULambda (ULambda (UApp (ULambda (UApp (UApp (UVar 4) (UVar 2)) (UVar 0))) (UVar 0)))) (UVar 0))))) (UBuiltin addInteger))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) (UVar 0)))) diff --git a/plutus-executables/inc-168982000/src/Ast3.agda b/plutus-executables/inc-168982000/src/Ast3.agda deleted file mode 100644 index e43c8ec9aad..00000000000 --- a/plutus-executables/inc-168982000/src/Ast3.agda +++ /dev/null @@ -1,22 +0,0 @@ -module Ast3 where - -open import VerifiedCompilation -open import VerifiedCompilation.Certificate -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) -open import Data.Bool.Base using (Bool; false; true) -open import Agda.Builtin.Equality using (_≡_; refl) - -ast3 : Untyped - -ast3 = (ULambda (UApp (UApp (UApp (UForce (UDelay (ULambda (UVar 0)))) (UForce (UDelay (ULambda (ULambda (UApp (UApp (UBuiltin addInteger) (UVar 1)) (UVar 0))))))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) diff --git a/plutus-executables/inc-168982000/src/Ast4.agda b/plutus-executables/inc-168982000/src/Ast4.agda deleted file mode 100644 index 9b158f9a1c4..00000000000 --- a/plutus-executables/inc-168982000/src/Ast4.agda +++ /dev/null @@ -1,22 +0,0 @@ -module Ast4 where - -open import VerifiedCompilation -open import VerifiedCompilation.Certificate -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) -open import Data.Bool.Base using (Bool; false; true) -open import Agda.Builtin.Equality using (_≡_; refl) - -ast4 : Untyped - -ast4 = (ULambda (UApp (UApp (UApp (ULambda (UVar 0)) (ULambda (ULambda (UApp (UApp (UBuiltin addInteger) (UVar 1)) (UVar 0))))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) diff --git a/plutus-executables/inc-168982000/src/Ast5.agda b/plutus-executables/inc-168982000/src/Ast5.agda deleted file mode 100644 index a49f6680097..00000000000 --- a/plutus-executables/inc-168982000/src/Ast5.agda +++ /dev/null @@ -1,22 +0,0 @@ -module Ast5 where - -open import VerifiedCompilation -open import VerifiedCompilation.Certificate -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) -open import Data.Bool.Base using (Bool; false; true) -open import Agda.Builtin.Equality using (_≡_; refl) - -ast5 : Untyped - -ast5 = (ULambda (UApp (UApp (ULambda (ULambda (UApp (UApp (UBuiltin addInteger) (UVar 1)) (UVar 0)))) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) diff --git a/plutus-executables/inc-168982000/src/Ast6.agda b/plutus-executables/inc-168982000/src/Ast6.agda deleted file mode 100644 index 0373e2190df..00000000000 --- a/plutus-executables/inc-168982000/src/Ast6.agda +++ /dev/null @@ -1,22 +0,0 @@ -module Ast6 where - -open import VerifiedCompilation -open import VerifiedCompilation.Certificate -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) -open import Data.Bool.Base using (Bool; false; true) -open import Agda.Builtin.Equality using (_≡_; refl) - -ast6 : Untyped - -ast6 = (ULambda (UApp (UApp (UBuiltin addInteger) (UCon (tagCon integer (ℤ.pos 1)))) (UVar 0))) diff --git a/plutus-executables/inc-168982000/src/inc.agda b/plutus-executables/inc-168982000/src/inc.agda deleted file mode 100644 index be0addf1c30..00000000000 --- a/plutus-executables/inc-168982000/src/inc.agda +++ /dev/null @@ -1,35 +0,0 @@ -module inc where - -open import Certifier -open import VerifiedCompilation -open import VerifiedCompilation.Certificate -open import Untyped -open import RawU -open import Builtin -open import Data.Unit -open import Data.Nat -open import Data.Integer -open import Utils -import Agda.Builtin.Bool -import Relation.Nullary -import VerifiedCompilation.UntypedTranslation -open import Agda.Builtin.List using (_∷_; []) -open import Agda.Builtin.Maybe -open import Data.Empty using (⊥) -open import Data.Bool.Base using (Bool; false; true) -open import Agda.Builtin.Equality using (_≡_; refl) -open import Ast0 -open import Ast1 -open import Ast2 -open import Ast3 -open import Ast4 -open import Ast5 -open import Ast6 - - - -asts : List (SimplifierTag × Hints × Untyped × Untyped) -asts = ((floatDelayT , (none , (ast0 , ast1))) ∷ (forceCaseDelayT , (none , (ast1 , ast1))) ∷ (forceDelayT , (none , (ast1 , ast2))) ∷ (caseOfCaseT , (none , (ast2 , ast2))) ∷ (caseReduceT , (none , (ast2 , ast2))) ∷ (inlineT , (inline (((ƛ↓ (expand (ƛ ((ƛ↓ ((((force ((ƛ↓ (expand (delay (ƛ var)))) ·↓)) · ((ƛ↓ ((ƛ↓ ((ƛ↓ (force (expand (delay (expand (ƛ ((ƛ↓ (ƛ ((ƛ↓ (((expand builtin) · (expand var)) · (expand var))) ·↓))) ·↓))))))) ·↓)) ·↓)) ·↓)) · con) · (expand var))) ·↓)))) ·↓)) , (ast2 , ast3))) ∷ (floatDelayT , (none , (ast3 , ast3))) ∷ (forceCaseDelayT , (none , (ast3 , ast3))) ∷ (forceDelayT , (none , (ast3 , ast4))) ∷ (caseOfCaseT , (none , (ast4 , ast4))) ∷ (caseReduceT , (none , (ast4 , ast4))) ∷ (inlineT , (inline ((ƛ ((((ƛ↓ (expand (ƛ (ƛ ((builtin · var) · var))))) ·↓) · con) · var))) , (ast4 , ast5))) ∷ (floatDelayT , (none , (ast5 , ast5))) ∷ (forceCaseDelayT , (none , (ast5 , ast5))) ∷ (forceDelayT , (none , (ast5 , ast5))) ∷ (caseOfCaseT , (none , (ast5 , ast5))) ∷ (caseReduceT , (none , (ast5 , ast5))) ∷ (inlineT , (inline ((ƛ (((ƛ↓ (ƛ↓ ((builtin · (expand con)) · (expand var)))) ·↓) ·↓))) , (ast5 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (cseT , (none , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (cseT , (none , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (cseT , (none , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (cseT , (none , (ast6 , ast6))) ∷ (floatDelayT , (none , (ast6 , ast6))) ∷ (forceCaseDelayT , (none , (ast6 , ast6))) ∷ (forceDelayT , (none , (ast6 , ast6))) ∷ (caseOfCaseT , (none , (ast6 , ast6))) ∷ (caseReduceT , (none , (ast6 , ast6))) ∷ (inlineT , (inline ((ƛ ((builtin · con) · var))) , (ast6 , ast6))) ∷ (applyToCaseT , (none , (ast6 , ast6))) ∷ []) - -certificate : passed? (runCertifier asts) ≡ true -certificate = refl 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-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..026e1a80cf3 --- /dev/null +++ b/plutus-tx-plugin/changelog.d/20260311_120000_agda_certifier_source_location_tracking.md @@ -0,0 +1,25 @@ +### 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. + +### Changed + +- `compileExpr` no longer takes a `Maybe GHC.RealSrcSpan` parameter; source + location now flows through `ccCurrentLoc` in `CompileContext` via + `asks`/`local`. +- `compileMarkedExprs` simplified from a stateful `go lastLoc` loop to direct + recursion. +- `stripAnchors` simplified to a single pattern match (no recursive `go` loop). +- Package name resolution uses `GHC.lookupUnit`, `GHC.thisPackageName`, and + `stripVersionFromUnitId` as a fallback chain. + +### Removed + +- `findProjectRoot` — replaced by `System.Directory.makeAbsolute`. diff --git a/plutus-tx/changelog.d/20260311_120000_agda_certifier_encode_th_loc.md b/plutus-tx/changelog.d/20260311_120000_agda_certifier_encode_th_loc.md new file mode 100644 index 00000000000..72f25d4481e --- /dev/null +++ b/plutus-tx/changelog.d/20260311_120000_agda_certifier_encode_th_loc.md @@ -0,0 +1,6 @@ +### Changed + +- `compileUntyped` now encodes source locations in a structured null-separated + format (matching `encodeSrcSpan` / `decodeSrcSpan`) instead of using + `TH.pprint`, enabling the plugin to recover a `RealSrcSpan` from the + type-level string. From d3787b5fb53802095f3dad4a6e1814fb00f4e167 Mon Sep 17 00:00:00 2001 From: zeme Date: Wed, 11 Mar 2026 13:01:47 +0100 Subject: [PATCH 6/6] wip --- ...0_agda_certifier_source_location_tracking.md | 17 +---------------- ...60311_120000_agda_certifier_encode_th_loc.md | 6 ------ 2 files changed, 1 insertion(+), 22 deletions(-) delete mode 100644 plutus-tx/changelog.d/20260311_120000_agda_certifier_encode_th_loc.md 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 index 026e1a80cf3..1839f8274b7 100644 --- 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 @@ -4,22 +4,7 @@ `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 +- `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. - -### Changed - -- `compileExpr` no longer takes a `Maybe GHC.RealSrcSpan` parameter; source - location now flows through `ccCurrentLoc` in `CompileContext` via - `asks`/`local`. -- `compileMarkedExprs` simplified from a stateful `go lastLoc` loop to direct - recursion. -- `stripAnchors` simplified to a single pattern match (no recursive `go` loop). -- Package name resolution uses `GHC.lookupUnit`, `GHC.thisPackageName`, and - `stripVersionFromUnitId` as a fallback chain. - -### Removed - -- `findProjectRoot` — replaced by `System.Directory.makeAbsolute`. diff --git a/plutus-tx/changelog.d/20260311_120000_agda_certifier_encode_th_loc.md b/plutus-tx/changelog.d/20260311_120000_agda_certifier_encode_th_loc.md deleted file mode 100644 index 72f25d4481e..00000000000 --- a/plutus-tx/changelog.d/20260311_120000_agda_certifier_encode_th_loc.md +++ /dev/null @@ -1,6 +0,0 @@ -### Changed - -- `compileUntyped` now encodes source locations in a structured null-separated - format (matching `encodeSrcSpan` / `decodeSrcSpan`) instead of using - `TH.pprint`, enabling the plugin to recover a `RealSrcSpan` from the - type-level string.