diff --git a/plutus-core/changelog.d/20260504_235314_ana.pantilie95_constant_folding_uplc_2.md b/plutus-core/changelog.d/20260504_235314_ana.pantilie95_constant_folding_uplc_2.md new file mode 100644 index 00000000000..b138ef87450 --- /dev/null +++ b/plutus-core/changelog.d/20260504_235314_ana.pantilie95_constant_folding_uplc_2.md @@ -0,0 +1,3 @@ +### Added + +- The UPLC optimizer now also simplifies terms by evaluating builtins. diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal index 66ea03bff36..a510e488621 100644 --- a/plutus-core/plutus-core.cabal +++ b/plutus-core/plutus-core.cabal @@ -235,6 +235,7 @@ library UntypedPlutusCore.Transform.Certify.Hints UntypedPlutusCore.Transform.Certify.Trace UntypedPlutusCore.Transform.Cse + UntypedPlutusCore.Transform.EvaluateBuiltins UntypedPlutusCore.Transform.FloatDelay UntypedPlutusCore.Transform.ForceCaseDelay UntypedPlutusCore.Transform.ForceDelay @@ -282,6 +283,7 @@ library PlutusCore.Pretty.Readable PlutusCore.Pretty.Utils Universe.Core + UntypedPlutusCore.Analysis.Builtins UntypedPlutusCore.Analysis.Definitions UntypedPlutusCore.Analysis.Usages UntypedPlutusCore.Core.Instance @@ -485,6 +487,7 @@ library untyped-plutus-core-testlib Generators.Spec Scoping.Spec Transform.CaseOfCase.Spec + Transform.EvaluateBuiltins.Spec Transform.Inline.Spec Transform.Simplify.Lib Transform.Simplify.Spec diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Analysis/Builtins.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Analysis/Builtins.hs new file mode 100644 index 00000000000..d59e3365bfe --- /dev/null +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Analysis/Builtins.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} + +module UntypedPlutusCore.Analysis.Builtins + ( BuiltinsInfo (..) + , biSemanticsVariant + , biUnserializableConstants + , builtinArityInfo + , constantIsSerializable + , termIsSerializable + , defaultUniUnserializableConstants + ) where + +import Control.Lens hiding (parts) +import Data.Kind +import Data.Proxy +import PlutusCore.Arity +import PlutusCore.Builtin +import PlutusCore.Builtin qualified as PLC +import PlutusCore.Default +import PlutusPrelude (Default (..)) +import UntypedPlutusCore.Core (Term) +import UntypedPlutusCore.Core.Plated (termSubtermsDeep, _Constant) + +-- | All non-static information about builtins that the compiler might want. +data BuiltinsInfo (uni :: Type -> Type) fun = BuiltinsInfo + { _biSemanticsVariant :: PLC.BuiltinSemanticsVariant fun + , -- See Note [Unserializable constants] + _biUnserializableConstants :: Some (ValueOf uni) -> Bool + } + +makeLenses ''BuiltinsInfo + +instance Default (BuiltinsInfo DefaultUni DefaultFun) where + def = + BuiltinsInfo + { _biSemanticsVariant = def + , _biUnserializableConstants = defaultUniUnserializableConstants + } + +-- | Get the arity of a builtin function from the 'PLC.BuiltinInfo'. +builtinArityInfo + :: forall uni fun + . ToBuiltinMeaning uni fun + => BuiltinsInfo uni fun + -> fun + -> Arity +builtinArityInfo binfo = builtinArity (Proxy @uni) (binfo ^. biSemanticsVariant) + +constantIsSerializable + :: forall uni fun + . BuiltinsInfo uni fun + -> Some (ValueOf uni) + -> Bool +constantIsSerializable bi v = not $ _biUnserializableConstants bi v + +termIsSerializable :: BuiltinsInfo uni fun -> Term name uni fun a -> Bool +termIsSerializable binfo = + allOf + (termSubtermsDeep . _Constant) + (constantIsSerializable binfo . snd) + +-- See Note [Unserializable constants] +defaultUniUnserializableConstants :: Some (ValueOf DefaultUni) -> Bool +defaultUniUnserializableConstants = \case + Some (ValueOf DefaultUniBLS12_381_G1_Element _) -> True + Some (ValueOf DefaultUniBLS12_381_G2_Element _) -> True + Some (ValueOf DefaultUniBLS12_381_MlResult _) -> True + _ -> False + +{- See Note [Unserializable constants] in PlutusIR.Analysis.Builtins. +-} diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Contexts.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Contexts.hs index e476fe9d2da..8ce7b4b8164 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Contexts.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Contexts.hs @@ -1,7 +1,9 @@ {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} module UntypedPlutusCore.Contexts where +import PlutusCore.Arity import UntypedPlutusCore.Core (Term (..)) import UntypedPlutusCore.Core.Instance.Eq () @@ -23,7 +25,7 @@ splitAppCtx :: Term nam uni fun a -> (Term nam uni fun a, AppCtx nam uni fun a) splitAppCtx = go AppCtxEnd where go appCtx = \case - Apply ann function argument -> go (AppCtxTerm ann argument appCtx) function + Apply ann function arg -> go (AppCtxTerm ann arg appCtx) function Force ann forcedTerm -> go (AppCtxType ann appCtx) forcedTerm term -> (term, appCtx) @@ -36,3 +38,22 @@ fillAppCtx term = \case AppCtxEnd -> term AppCtxTerm ann arg ctx -> fillAppCtx (Apply ann term arg) ctx AppCtxType ann ctx -> fillAppCtx (Force ann term) ctx + +data Saturation = Oversaturated | Undersaturated | Saturated + +-- | Do the given arguments saturate the given arity? +saturates :: AppCtx name uni fun a -> Arity -> Maybe Saturation +-- Exactly right +saturates AppCtxEnd [] = Just Saturated +-- Parameters left - undersaturated +saturates AppCtxEnd _ = Just Undersaturated +-- Match a term parameter to a term arg +saturates (AppCtxTerm _ _ ctx) (TermParam : arities) = saturates ctx arities +-- Match a type parameter to a type arg +saturates (AppCtxType _ ctx) (TypeParam : arities) = saturates ctx arities +-- Param/arg mismatch +saturates (AppCtxTerm {}) (TypeParam : _) = Nothing +saturates (AppCtxType {}) (TermParam : _) = Nothing +-- Arguments left - undersaturated +saturates (AppCtxTerm {}) [] = Just Oversaturated +saturates (AppCtxType {}) [] = Just Oversaturated diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs index f205119fe83..83a1be8eff7 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs @@ -10,8 +10,10 @@ module UntypedPlutusCore.Core.Plated , termConstantsDeep , termSubtermsDeep , termUniquesDeep + , _Constant ) where +import PlutusCore qualified as PLC import PlutusCore.Core (HasUniques) import PlutusCore.Name.Unique import UntypedPlutusCore.Core.Type @@ -78,3 +80,7 @@ termSubtermsDeep = cosmosOf termSubterms -- | Get all the transitive child 'Unique's of the given 'Term'. termUniquesDeep :: HasUniques (Term name uni fun ann) => Fold (Term name uni fun ann) Unique termUniquesDeep = termSubtermsDeep . termUniques + +-- | View a term as a constant. +_Constant :: Prism' (Term name uni fun a) (a, PLC.Some (PLC.ValueOf uni)) +_Constant = prism' (uncurry Constant) (\case Constant a v -> Just (a, v); _ -> Nothing) diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs index c98bcbaf4aa..79b7f81d40b 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs @@ -32,6 +32,7 @@ import PlutusPrelude import Data.Vector import PlutusCore.Builtin qualified as TPLC import PlutusCore.Core qualified as TPLC +import PlutusCore.Evaluation.Machine.ExMemoryUsage import PlutusCore.MkPlc import PlutusCore.Name.Unique qualified as TPLC import Universe @@ -110,6 +111,11 @@ deriving anyclass instance (NFData name, NFData fun, NFData ann, Everywhere uni NFData, Closed uni) => NFData (Term name uni fun ann) +-- See Note [ExMemoryUsage instances for non-constants]. +instance ExMemoryUsage (Term name uni fun ann) where + memoryUsage = + Prelude.error "Internal error: 'memoryUsage' for UPLC 'Term' is not supposed to be forced" + -- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language. data Program name uni fun ann = Program { _progAnn :: ann @@ -165,25 +171,25 @@ makeLenses ''UVarDecl -- | Return the outermost annotation of a 'Term'. instance HasAnn (Term name uni fun) where getAnn (Constant ann _) = ann - getAnn (Builtin ann _) = ann - getAnn (Var ann _) = ann + getAnn (Builtin ann _) = ann + getAnn (Var ann _) = ann getAnn (LamAbs ann _ _) = ann - getAnn (Apply ann _ _) = ann - getAnn (Delay ann _) = ann - getAnn (Force ann _) = ann - getAnn (Error ann) = ann + getAnn (Apply ann _ _) = ann + getAnn (Delay ann _) = ann + getAnn (Force ann _) = ann + getAnn (Error ann) = ann getAnn (Constr ann _ _) = ann - getAnn (Case ann _ _) = ann + getAnn (Case ann _ _) = ann modifyAnn f = \case - Constant ann c -> Constant (f ann) c - Builtin ann b -> Builtin (f ann) b - Var ann v -> Var (f ann) v - LamAbs ann x body -> LamAbs (f ann) x body - Apply ann fun arg -> Apply (f ann) fun arg - Delay ann body -> Delay (f ann) body - Force ann body -> Force (f ann) body - Error ann -> Error (f ann) - Constr ann i args -> Constr (f ann) i args + Constant ann c -> Constant (f ann) c + Builtin ann b -> Builtin (f ann) b + Var ann v -> Var (f ann) v + LamAbs ann x body -> LamAbs (f ann) x body + Apply ann fun arg -> Apply (f ann) fun arg + Delay ann body -> Delay (f ann) body + Force ann body -> Force (f ann) body + Error ann -> Error (f ann) + Constr ann i args -> Constr (f ann) i args Case ann scrut alts -> Case (f ann) scrut alts bindFunM diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Optimize.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Optimize.hs index 5b89d87ed74..ce63fea4776 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Optimize.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Optimize.hs @@ -13,16 +13,19 @@ module UntypedPlutusCore.Optimize , module UntypedPlutusCore.Transform.Optimizer ) where +import PlutusCore.Builtin (CostingPart) import PlutusCore.Compiler.Types import PlutusCore.Default qualified as PLC import PlutusCore.Default.Builtins import PlutusCore.Name.Unique +import UntypedPlutusCore.Analysis.Builtins (BuiltinsInfo, biSemanticsVariant) import UntypedPlutusCore.Core.Type import UntypedPlutusCore.Optimize.Opts as Opts import UntypedPlutusCore.Transform.ApplyToCase (applyToCase) import UntypedPlutusCore.Transform.CaseOfCase import UntypedPlutusCore.Transform.CaseReduce import UntypedPlutusCore.Transform.Cse +import UntypedPlutusCore.Transform.EvaluateBuiltins (evaluateBuiltinsPass) import UntypedPlutusCore.Transform.FloatDelay (floatDelay) import UntypedPlutusCore.Transform.ForceCaseDelay (forceCaseDelay) import UntypedPlutusCore.Transform.ForceDelay (forceDelay) @@ -30,7 +33,9 @@ import UntypedPlutusCore.Transform.Inline (InlineHints (..), inline) import UntypedPlutusCore.Transform.LetFloatOut (letFloatOut) import UntypedPlutusCore.Transform.Optimizer +import Control.Lens ((&), (.~)) import Control.Monad +import Data.Default.Class (def) import Data.Either (isRight) import Data.List as List (foldl') import Data.Typeable @@ -109,6 +114,7 @@ termOptimizer opts builtinSemanticsVariant = >=> runStage CaseOfCaseStage >=> runStage CaseReduceStage >=> runStage InlineStage + >=> runStage ConstantFoldingStage certifiedOnly = _ooCertifiedOptsOnly opts @@ -144,6 +150,14 @@ termOptimizer opts builtinSemanticsVariant = if _ooApplyToCase opts then applyToCase else pure LetFloatOutStage -> letFloatOut + ConstantFoldingStage -> + case (eqT @uni @PLC.DefaultUni, eqT @fun @DefaultFun) of + (Just Refl, Just Refl) -> + evaluateBuiltinsPass + (_ooPreserveLogging opts) + ((def :: BuiltinsInfo PLC.DefaultUni DefaultFun) & biSemanticsVariant .~ builtinSemanticsVariant) + (def :: CostingPart PLC.DefaultUni DefaultFun) + _ -> pure caseOfCase' :: Term name uni fun a diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs index f66c7abb104..f7a9e250ed6 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs @@ -43,6 +43,7 @@ corresponding constructor to this type. Please also open an issue at https://github.com/IntersectMBO/plutus/issues. -} data UncertifiedOptStage = CaseOfCase + | ConstantFolding deriving stock (Show, Generic) deriving anyclass (NFData) @@ -75,6 +76,9 @@ pattern CaseOfCaseStage = Left CaseOfCase pattern LetFloatOutStage :: OptStage pattern LetFloatOutStage = Right LetFloatOut +pattern ConstantFoldingStage :: OptStage +pattern ConstantFoldingStage = Left ConstantFolding + {-# COMPLETE FloatDelayStage , ForceDelayStage @@ -85,6 +89,7 @@ pattern LetFloatOutStage = Right LetFloatOut , ApplyToCaseStage , CaseOfCaseStage , LetFloatOutStage + , ConstantFoldingStage #-} data Optimization name uni fun a diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/EvaluateBuiltins.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/EvaluateBuiltins.hs new file mode 100644 index 00000000000..ab6e9b66634 --- /dev/null +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/EvaluateBuiltins.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} + +{-| This module mirrors 'PlutusIR.Transform.EvaluateBuiltins', adapted for UPLC's +untyped 'Term' and 'AppCtx'. See that module for detailed commentary. -} +module UntypedPlutusCore.Transform.EvaluateBuiltins + ( evaluateBuiltinsPass + ) where + +import PlutusCore.Builtin +import UntypedPlutusCore.Analysis.Builtins +import UntypedPlutusCore.Contexts +import UntypedPlutusCore.Core +import UntypedPlutusCore.Transform.Certify.Trace +import UntypedPlutusCore.Transform.Optimizer + +import Control.Lens (transformOf, (^.)) +import Data.Functor (void) + +evaluateBuiltinsPass + :: (Monad m, ToBuiltinMeaning uni fun, Typeable name) + => Bool + -- ^ Whether to be conservative and try to retain logging behaviour. + -> BuiltinsInfo uni fun + -> CostingPart uni fun + -> Term name uni fun a + -> OptimizerT name uni fun a m (Term name uni fun a) +evaluateBuiltinsPass preserveLogging binfo costModel term = do + result <- evaluateBuiltins preserveLogging binfo costModel term + recordOptimization term ConstantFoldingStage result + return result + +evaluateBuiltins + :: forall m name uni fun a + . ( Monad m + , ToBuiltinMeaning uni fun + , Typeable name + ) + => Bool + -- ^ Whether to be conservative and try to retain logging behaviour. + -> BuiltinsInfo uni fun + -> CostingPart uni fun + -> Term name uni fun a + -> OptimizerT name uni fun a m (Term name uni fun a) +evaluateBuiltins preserveLogging binfo costModel = + pure . transformOf termSubterms processTerm + where + eval + :: BuiltinRuntime (Term name uni fun ()) + -> AppCtx name uni fun a + -> Maybe (Term name uni fun ()) + eval (BuiltinCostedResult _ getFXs) AppCtxEnd = + case getFXs of + BuiltinSuccess y -> Just y + BuiltinSuccessWithLogs _ y -> if preserveLogging then Nothing else Just y + BuiltinFailure {} -> Nothing + eval (BuiltinExpectArgument toRuntime) (AppCtxTerm _ arg ctx) = + eval (toRuntime $ void arg) ctx + eval (BuiltinExpectForce runtime) (AppCtxType _ ctx) = + eval runtime ctx + eval _ _ = Nothing + + processTerm :: Term name uni fun a -> Term name uni fun a + -- See Note [Context splitting in a recursive pass] + processTerm t@(splitAppCtx -> (Builtin x bn, argCtx)) = + let runtime = toBuiltinRuntime costModel (toBuiltinMeaning (binfo ^. biSemanticsVariant) bn) + in case eval runtime argCtx of + -- See Note [Unserializable constants] in PlutusIR.Analysis.Builtins + Just t' | termIsSerializable binfo t' -> x <$ t' + _ -> t + processTerm t = t diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Optimizer.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Optimizer.hs index ddd01a503b6..b404da5d0b7 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Optimizer.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Optimizer.hs @@ -12,6 +12,7 @@ module UntypedPlutusCore.Transform.Optimizer , pattern Trace.ApplyToCaseStage , pattern Trace.CaseOfCaseStage , pattern Trace.LetFloatOutStage + , pattern Trace.ConstantFoldingStage , Trace.OptimizerTrace (..) , Trace.Optimization (..) , runOptimizerT diff --git a/plutus-core/untyped-plutus-core/test/Spec.hs b/plutus-core/untyped-plutus-core/test/Spec.hs index 0accb0b0c75..5fb2951d184 100644 --- a/plutus-core/untyped-plutus-core/test/Spec.hs +++ b/plutus-core/untyped-plutus-core/test/Spec.hs @@ -17,6 +17,7 @@ import Flat.Spec (test_flat) import Generators.Spec (test_parsing) import Scoping.Spec (test_names) import Transform.CaseOfCase.Spec (test_caseOfCase) +import Transform.EvaluateBuiltins.Spec (test_evaluateBuiltins) import Transform.Inline.Spec (test_inline) import Transform.Simplify.Spec (test_simplify) @@ -32,6 +33,7 @@ main = do , test_builtins , test_budget , test_caseOfCase + , test_evaluateBuiltins , test_inline , test_golden , test_tallying diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/addInteger.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/addInteger.golden.uplc new file mode 100644 index 00000000000..e440e5c8425 --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/addInteger.golden.uplc @@ -0,0 +1 @@ +3 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/failingBuiltin.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/failingBuiltin.golden.uplc new file mode 100644 index 00000000000..1f11dc4236f --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/failingBuiltin.golden.uplc @@ -0,0 +1 @@ +divideInteger 1 0 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/ifThenElse.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/ifThenElse.golden.uplc new file mode 100644 index 00000000000..56a6051ca2b --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/ifThenElse.golden.uplc @@ -0,0 +1 @@ +1 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/nonConstantArg.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/nonConstantArg.golden.uplc new file mode 100644 index 00000000000..2aa86a5982a --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/nonConstantArg.golden.uplc @@ -0,0 +1 @@ +addInteger x 2 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/overApplication.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/overApplication.golden.uplc new file mode 100644 index 00000000000..8f4361822ea --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/overApplication.golden.uplc @@ -0,0 +1 @@ +(\x -> 1) 3 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/traceConservative.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/traceConservative.golden.uplc new file mode 100644 index 00000000000..50101bfeaa0 --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/traceConservative.golden.uplc @@ -0,0 +1 @@ +force trace "hello" 1 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/traceNonConservative.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/traceNonConservative.golden.uplc new file mode 100644 index 00000000000..56a6051ca2b --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/traceNonConservative.golden.uplc @@ -0,0 +1 @@ +1 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressAndEqualBlsNonConservative.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressAndEqualBlsNonConservative.golden.uplc new file mode 100644 index 00000000000..f742d389cdb --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressAndEqualBlsNonConservative.golden.uplc @@ -0,0 +1,5 @@ +bls12_381_G1_equal + (bls12_381_G1_uncompress + #97f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb) + (bls12_381_G1_uncompress + #97f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb) \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressBlsConservative.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressBlsConservative.golden.uplc new file mode 100644 index 00000000000..6b006da298a --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressBlsConservative.golden.uplc @@ -0,0 +1,2 @@ +bls12_381_G2_uncompress + #c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressBlsNonConservative.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressBlsNonConservative.golden.uplc new file mode 100644 index 00000000000..6b006da298a --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/uncompressBlsNonConservative.golden.uplc @@ -0,0 +1,2 @@ +bls12_381_G2_uncompress + #c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/underApplication.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/underApplication.golden.uplc new file mode 100644 index 00000000000..51e72e82dd1 --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Transform/EvaluateBuiltins/underApplication.golden.uplc @@ -0,0 +1 @@ +addInteger 1 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/basic.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/basic.golden.certifier-hints index 90784ba2fe8..19e35b323c0 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/basic.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/basic.golden.certifier-hints @@ -20,6 +20,9 @@ NoHints InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/basicInline.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/basicInline.golden.certifier-hints index 493a09280eb..223be4d95c3 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/basicInline.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/basicInline.golden.certifier-hints @@ -22,6 +22,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/callsiteInline.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/callsiteInline.golden.certifier-hints index ff2ee10d4b0..13d9e8ca088 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/callsiteInline.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/callsiteInline.golden.certifier-hints @@ -46,6 +46,9 @@ InlLam InlVar --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/cse2.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/cse2.golden.uplc index 6922068a035..ac8c8049ae7 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/cse2.golden.uplc +++ b/plutus-core/untyped-plutus-core/test/Transform/cse2.golden.uplc @@ -1,8 +1,5 @@ force (force (case - (constr 0 - [ (lessThanInteger 0 0) - , (delay ((\cse -> addInteger cse cse) (addInteger 1 2))) - , (delay (addInteger 1 2)) ]) + (constr 0 [False, (delay ((\cse -> addInteger cse cse) 3)), (delay 3)]) [ifThenElse])) \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/cseExpensive.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/cseExpensive.golden.uplc index 4fd3257b083..58db072cc29 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/cseExpensive.golden.uplc +++ b/plutus-core/untyped-plutus-core/test/Transform/cseExpensive.golden.uplc @@ -1,767 +1 @@ -(\cse -> - addInteger cse cse) - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - (addInteger - 0 - 1) - (addInteger - 2 - 3)) - (addInteger - 4 - 5)) - (addInteger - 6 - 7)) - (addInteger - 8 - 9)) - (addInteger - 10 - 11)) - (addInteger - 12 - 13)) - (addInteger - 14 - 15)) - (addInteger - 16 - 17)) - (addInteger - 18 - 19)) - (addInteger - 20 - 21)) - (addInteger - 22 - 23)) - (addInteger - 24 - 25)) - (addInteger - 26 - 27)) - (addInteger - 28 - 29)) - (addInteger - 30 - 31)) - (addInteger - 32 - 33)) - (addInteger - 34 - 35)) - (addInteger - 36 - 37)) - (addInteger - 38 - 39)) - (addInteger - 40 - 41)) - (addInteger - 42 - 43)) - (addInteger - 44 - 45)) - (addInteger - 46 - 47)) - (addInteger - 48 - 49)) - (addInteger - 50 - 51)) - (addInteger - 52 - 53)) - (addInteger - 54 - 55)) - (addInteger - 56 - 57)) - (addInteger - 58 - 59)) - (addInteger - 60 - 61)) - (addInteger - 62 - 63)) - (addInteger - 64 - 65)) - (addInteger - 66 - 67)) - (addInteger - 68 - 69)) - (addInteger - 70 - 71)) - (addInteger - 72 - 73)) - (addInteger - 74 - 75)) - (addInteger - 76 - 77)) - (addInteger - 78 - 79)) - (addInteger - 80 - 81)) - (addInteger - 82 - 83)) - (addInteger - 84 - 85)) - (addInteger - 86 - 87)) - (addInteger - 88 - 89)) - (addInteger - 90 - 91)) - (addInteger - 92 - 93)) - (addInteger - 94 - 95)) - (addInteger - 96 - 97)) - (addInteger - 98 - 99)) - (addInteger - 100 - 101)) - (addInteger - 102 - 103)) - (addInteger - 104 - 105)) - (addInteger - 106 - 107)) - (addInteger - 108 - 109)) - (addInteger - 110 - 111)) - (addInteger - 112 - 113)) - (addInteger - 114 - 115)) - (addInteger - 116 - 117)) - (addInteger - 118 - 119)) - (addInteger - 120 - 121)) - (addInteger - 122 - 123)) - (addInteger - 124 - 125)) - (addInteger - 126 - 127)) - (addInteger - 128 - 129)) - (addInteger - 130 - 131)) - (addInteger - 132 - 133)) - (addInteger - 134 - 135)) - (addInteger - 136 - 137)) - (addInteger - 138 - 139)) - (addInteger - 140 - 141)) - (addInteger - 142 - 143)) - (addInteger - 144 - 145)) - (addInteger - 146 - 147)) - (addInteger - 148 - 149)) - (addInteger - 150 - 151)) - (addInteger - 152 - 153)) - (addInteger - 154 - 155)) - (addInteger - 156 - 157)) - (addInteger - 158 - 159)) - (addInteger - 160 - 161)) - (addInteger - 162 - 163)) - (addInteger - 164 - 165)) - (addInteger - 166 - 167)) - (addInteger - 168 - 169)) - (addInteger - 170 - 171)) - (addInteger - 172 - 173)) - (addInteger - 174 - 175)) - (addInteger - 176 - 177)) - (addInteger - 178 - 179)) - (addInteger - 180 - 181)) - (addInteger - 182 - 183)) - (addInteger - 184 - 185)) - (addInteger - 186 - 187)) - (addInteger - 188 - 189)) - (addInteger - 190 - 191)) - (addInteger - 192 - 193)) - (addInteger - 194 - 195)) - (addInteger - 196 - 197)) - (addInteger - 198 - 199)) - (addInteger - 200 - 201)) - (addInteger - 202 - 203)) - (addInteger - 204 - 205)) - (addInteger - 206 - 207)) - (addInteger - 208 - 209)) - (addInteger - 210 - 211)) - (addInteger - 212 - 213)) - (addInteger - 214 - 215)) - (addInteger - 216 - 217)) - (addInteger - 218 - 219)) - (addInteger - 220 - 221)) - (addInteger - 222 - 223)) - (addInteger - 224 - 225)) - (addInteger - 226 - 227)) - (addInteger - 228 - 229)) - (addInteger - 230 - 231)) - (addInteger - 232 - 233)) - (addInteger - 234 - 235)) - (addInteger - 236 - 237)) - (addInteger - 238 - 239)) - (addInteger - 240 - 241)) - (addInteger - 242 - 243)) - (addInteger - 244 - 245)) - (addInteger - 246 - 247)) - (addInteger - 248 - 249)) - (addInteger - 250 - 251)) - (addInteger - 252 - 253)) - (addInteger - 254 - 255)) - (addInteger - 256 - 257)) - (addInteger - 258 - 259)) - (addInteger - 260 - 261)) - (addInteger - 262 - 263)) - (addInteger - 264 - 265)) - (addInteger - 266 - 267)) - (addInteger - 268 - 269)) - (addInteger - 270 - 271)) - (addInteger - 272 - 273)) - (addInteger - 274 - 275)) - (addInteger - 276 - 277)) - (addInteger - 278 - 279)) - (addInteger - 280 - 281)) - (addInteger - 282 - 283)) - (addInteger - 284 - 285)) - (addInteger - 286 - 287)) - (addInteger - 288 - 289)) - (addInteger - 290 - 291)) - (addInteger - 292 - 293)) - (addInteger - 294 - 295)) - (addInteger - 296 - 297)) - (addInteger - 298 - 299)) - (addInteger - 300 - 301)) - (addInteger - 302 - 303)) - (addInteger - 304 - 305)) - (addInteger - 306 - 307)) - (addInteger - 308 - 309)) - (addInteger - 310 - 311)) - (addInteger - 312 - 313)) - (addInteger - 314 - 315)) - (addInteger - 316 - 317)) - (addInteger - 318 - 319)) - (addInteger - 320 - 321)) - (addInteger - 322 - 323)) - (addInteger - 324 - 325)) - (addInteger - 326 - 327)) - (addInteger - 328 - 329)) - (addInteger - 330 - 331)) - (addInteger - 332 - 333)) - (addInteger - 334 - 335)) - (addInteger - 336 - 337)) - (addInteger - 338 - 339)) - (addInteger - 340 - 341)) - (addInteger - 342 - 343)) - (addInteger - 344 - 345)) - (addInteger - 346 - 347)) - (addInteger - 348 - 349)) - (addInteger - 350 - 351)) - (addInteger - 352 - 353)) - (addInteger - 354 - 355)) - (addInteger - 356 - 357)) - (addInteger - 358 - 359)) - (addInteger - 360 - 361)) - (addInteger - 362 - 363)) - (addInteger 364 365)) - (addInteger 366 367)) - (addInteger 368 369)) - (addInteger 370 371)) - (addInteger 372 373)) - (addInteger 374 375)) - (addInteger 376 377)) - (addInteger 378 379)) - (addInteger 380 381)) - (addInteger 382 383)) - (addInteger 384 385)) - (addInteger 386 387)) - (addInteger 388 389)) - (addInteger 390 391)) - (addInteger 392 393)) - (addInteger 394 395)) - (addInteger 396 397)) - (addInteger 398 399)) - (addInteger 400 401)) \ No newline at end of file +(\cse -> addInteger cse cse) 80601 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/csePlusTree.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/csePlusTree.golden.uplc index ff1ca1eaa2a..409a8992921 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/csePlusTree.golden.uplc +++ b/plutus-core/untyped-plutus-core/test/Transform/csePlusTree.golden.uplc @@ -1,4 +1,3 @@ (\cse -> addInteger cse cse) ((\cse -> addInteger cse cse) - ((\cse -> addInteger cse cse) - ((\cse -> addInteger cse cse) (addInteger 1 1)))) \ No newline at end of file + ((\cse -> addInteger cse cse) ((\cse -> addInteger cse cse) 2))) \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/extraDelays.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/extraDelays.golden.certifier-hints index 495467a34c0..7068e974f39 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/extraDelays.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/extraDelays.golden.certifier-hints @@ -21,6 +21,9 @@ InlDelay InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.certifier-hints index 3d8e6b0d5ff..470659bfd2c 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.certifier-hints @@ -27,6 +27,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.uplc index b7b8ae1aa74..d8263ee9860 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.uplc +++ b/plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.uplc @@ -1 +1 @@ -addInteger 1 1 \ No newline at end of file +2 \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/floatDelay2.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/floatDelay2.golden.certifier-hints index 8f4476117bd..fd0c254cc7d 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/floatDelay2.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/floatDelay2.golden.certifier-hints @@ -34,6 +34,9 @@ InlApply InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/floatDelay2.golden.uplc b/plutus-core/untyped-plutus-core/test/Transform/floatDelay2.golden.uplc index 87366c81f72..98b96f2992a 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/floatDelay2.golden.uplc +++ b/plutus-core/untyped-plutus-core/test/Transform/floatDelay2.golden.uplc @@ -1 +1 @@ -(\a -> addInteger (force a) (force a)) (delay (addInteger 1 2)) \ No newline at end of file +(\a -> addInteger (force a) (force a)) (delay 3) \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/floatDelay3.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/floatDelay3.golden.certifier-hints index 5c167390ab8..4c83101e022 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/floatDelay3.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/floatDelay3.golden.certifier-hints @@ -33,6 +33,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps1.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps1.golden.certifier-hints index 7ef17c3aa23..cfd19e4902f 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps1.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps1.golden.certifier-hints @@ -23,6 +23,9 @@ InlLam InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps2.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps2.golden.certifier-hints index 8369d7a335c..82087a258ff 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps2.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps2.golden.certifier-hints @@ -24,6 +24,9 @@ InlLam InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps2Fail.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps2Fail.golden.certifier-hints index f0e39f7a4b0..2fd40583a19 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps2Fail.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayNoApps2Fail.golden.certifier-hints @@ -26,6 +26,9 @@ InlLam InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps1.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps1.golden.certifier-hints index eb22e165732..29e1948f8a6 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps1.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps1.golden.certifier-hints @@ -24,6 +24,9 @@ InlLam InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps2.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps2.golden.certifier-hints index b0cab22e102..b7c480f86b9 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps2.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps2.golden.certifier-hints @@ -25,6 +25,9 @@ InlLam InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps2Fail.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps2Fail.golden.certifier-hints index 35a49a5f1ba..b8a06436af1 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps2Fail.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceCaseDelayWithApps2Fail.golden.certifier-hints @@ -29,6 +29,9 @@ InlLam InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceDelayComplex.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceDelayComplex.golden.certifier-hints index 615fbb0e306..6354915df6a 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceDelayComplex.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceDelayComplex.golden.certifier-hints @@ -47,6 +47,9 @@ InlLam InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiApply.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiApply.golden.certifier-hints index 088faf8fee1..82389d83365 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiApply.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiApply.golden.certifier-hints @@ -35,6 +35,9 @@ InlLam InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiForce.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiForce.golden.certifier-hints index 493a09280eb..223be4d95c3 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiForce.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiForce.golden.certifier-hints @@ -22,6 +22,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceDelayNoApps.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceDelayNoApps.golden.certifier-hints index 90784ba2fe8..19e35b323c0 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceDelayNoApps.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceDelayNoApps.golden.certifier-hints @@ -20,6 +20,9 @@ NoHints InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceDelayNoAppsLayered.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceDelayNoAppsLayered.golden.certifier-hints index 90784ba2fe8..19e35b323c0 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceDelayNoAppsLayered.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceDelayNoAppsLayered.golden.certifier-hints @@ -20,6 +20,9 @@ NoHints InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/forceDelaySimple.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/forceDelaySimple.golden.certifier-hints index b3a1f86ca4a..a5948093d45 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/forceDelaySimple.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/forceDelaySimple.golden.certifier-hints @@ -24,6 +24,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/inlineImpure1.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/inlineImpure1.golden.certifier-hints index ae881203cc3..c60fcdbbc66 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/inlineImpure1.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/inlineImpure1.golden.certifier-hints @@ -24,6 +24,9 @@ InlApply InlError --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/inlineImpure2.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/inlineImpure2.golden.certifier-hints index ae881203cc3..c60fcdbbc66 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/inlineImpure2.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/inlineImpure2.golden.certifier-hints @@ -24,6 +24,9 @@ InlApply InlError --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/inlineImpure3.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/inlineImpure3.golden.certifier-hints index ae881203cc3..c60fcdbbc66 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/inlineImpure3.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/inlineImpure3.golden.certifier-hints @@ -24,6 +24,9 @@ InlApply InlError --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/inlineImpure4.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/inlineImpure4.golden.certifier-hints index 3680e2cf256..bba104fbabc 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/inlineImpure4.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/inlineImpure4.golden.certifier-hints @@ -26,6 +26,9 @@ InlLam InlVar --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/inlinePure1.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/inlinePure1.golden.certifier-hints index a17d9fce47a..2095279a87d 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/inlinePure1.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/inlinePure1.golden.certifier-hints @@ -24,6 +24,9 @@ InlLam InlVar --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/inlinePure2.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/inlinePure2.golden.certifier-hints index a17d9fce47a..2095279a87d 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/inlinePure2.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/inlinePure2.golden.certifier-hints @@ -24,6 +24,9 @@ InlLam InlVar --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/inlinePure3.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/inlinePure3.golden.certifier-hints index 10f47f1ad58..74e3d62f8f8 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/inlinePure3.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/inlinePure3.golden.certifier-hints @@ -29,6 +29,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/inlinePure4.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/inlinePure4.golden.certifier-hints index 40c1dc7aea8..b116e05f906 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/inlinePure4.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/inlinePure4.golden.certifier-hints @@ -32,6 +32,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/interveningLambda.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/interveningLambda.golden.certifier-hints index f1a98cb50f9..8744a8f2922 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/interveningLambda.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/interveningLambda.golden.certifier-hints @@ -25,6 +25,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/letFloatOutCase1.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/letFloatOutCase1.golden.certifier-hints index c26c6d6c2ec..fa97f87b88e 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/letFloatOutCase1.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/letFloatOutCase1.golden.certifier-hints @@ -21,6 +21,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/letFloatOutCase2.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/letFloatOutCase2.golden.certifier-hints index cdaa9e79fa7..f454a74cc83 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/letFloatOutCase2.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/letFloatOutCase2.golden.certifier-hints @@ -28,6 +28,9 @@ InlLam InlVar --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/letFloatOutForce.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/letFloatOutForce.golden.certifier-hints index 02e3c1b005c..591ef2b5395 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/letFloatOutForce.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/letFloatOutForce.golden.certifier-hints @@ -23,6 +23,9 @@ InlLam InlVar --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/multiApp.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/multiApp.golden.certifier-hints index c4146dcd212..042dfb3b9d0 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/multiApp.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/multiApp.golden.certifier-hints @@ -30,6 +30,9 @@ InlDrop InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/test/Transform/nested.golden.certifier-hints b/plutus-core/untyped-plutus-core/test/Transform/nested.golden.certifier-hints index 90784ba2fe8..19e35b323c0 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/nested.golden.certifier-hints +++ b/plutus-core/untyped-plutus-core/test/Transform/nested.golden.certifier-hints @@ -20,6 +20,9 @@ NoHints InlCon --- Certifier hints #8 (Right ApplyToCase) -- +-- Certifier hints #8 (Left ConstantFolding) -- +NoHints + +-- Certifier hints #9 (Right ApplyToCase) -- NoHints diff --git a/plutus-core/untyped-plutus-core/testlib/Transform/EvaluateBuiltins/Spec.hs b/plutus-core/untyped-plutus-core/testlib/Transform/EvaluateBuiltins/Spec.hs new file mode 100644 index 00000000000..edc7434877e --- /dev/null +++ b/plutus-core/untyped-plutus-core/testlib/Transform/EvaluateBuiltins/Spec.hs @@ -0,0 +1,148 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} + +module Transform.EvaluateBuiltins.Spec where + +import Data.ByteString qualified as BS +import Data.ByteString.Base16 qualified as Base16 +import Data.ByteString.Char8 qualified as BS8 +import Data.Text (Text) +import PlutusCore qualified as PLC +import PlutusCore.MkPlc (mkConstant, mkIterApp) +import PlutusCore.Quote (freshName, runQuote) +import PlutusPrelude (Default (def)) +import Test.Tasty (TestTree, testGroup) +import Transform.Simplify.Lib (goldenVsPretty) +import UntypedPlutusCore (DefaultFun, DefaultUni, Name, Term (..)) +import UntypedPlutusCore.Transform.EvaluateBuiltins (evaluateBuiltinsPass) +import UntypedPlutusCore.Transform.Optimizer (evalOptimizer) + +test_evaluateBuiltins :: TestTree +test_evaluateBuiltins = + testGroup "EvaluateBuiltins" $ + map + (uncurry $ goldenVsEvaluated True) + [ ("addInteger", addIntegerTerm) + , ("ifThenElse", ifThenElseTerm) + , ("traceConservative", traceTerm) + , ("failingBuiltin", failingBuiltinTerm) + , ("nonConstantArg", nonConstantArgTerm) + , ("overApplication", overApplicationTerm) + , ("underApplication", underApplicationTerm) + , ("uncompressBlsConservative", uncompressBlsG2Term) + ] + ++ map + (uncurry $ goldenVsEvaluated False) + [ ("traceNonConservative", traceTerm) + , ("uncompressBlsNonConservative", uncompressBlsG2Term) + , ("uncompressAndEqualBlsNonConservative", uncompressAndEqualBlsTerm) + ] + +goldenVsEvaluated :: Bool -> String -> Term Name DefaultUni DefaultFun () -> TestTree +goldenVsEvaluated conservative name = + goldenVsPretty ".golden.uplc" ("EvaluateBuiltins/" ++ name) + . runEvaluateBuiltins conservative + +runEvaluateBuiltins + :: Bool + -> Term Name DefaultUni DefaultFun () + -> Term Name DefaultUni DefaultFun () +runEvaluateBuiltins conservative = evalOptimizer . evaluateBuiltinsPass conservative def def + +addIntegerTerm :: Term Name DefaultUni DefaultFun () +addIntegerTerm = + Apply + () + (Apply () (Builtin () PLC.AddInteger) (mkConstant @Integer () 1)) + (mkConstant @Integer () 2) + +ifThenElseTerm :: Term Name DefaultUni DefaultFun () +ifThenElseTerm = + mkIterApp + (Force () (Builtin () PLC.IfThenElse)) + [ ((), mkConstant @Bool () True) + , ((), mkConstant @Integer () 1) + , ((), mkConstant @Integer () 2) + ] + +-- Used for both traceConservative (unchanged) and traceNonConservative (reduced to 1) +traceTerm :: Term Name DefaultUni DefaultFun () +traceTerm = + Apply + () + (Apply () (Force () (Builtin () PLC.Trace)) (mkConstant @Text () "hello")) + (mkConstant @Integer () 1) + +-- Division by zero; evaluates to error so should be left in place +failingBuiltinTerm :: Term Name DefaultUni DefaultFun () +failingBuiltinTerm = + Apply + () + (Apply () (Builtin () PLC.DivideInteger) (mkConstant @Integer () 1)) + (mkConstant @Integer () 0) + +-- The variable argument prevents evaluation +nonConstantArgTerm :: Term Name DefaultUni DefaultFun () +nonConstantArgTerm = runQuote $ do + x <- freshName "x" + pure $ + Apply + () + (Apply () (Builtin () PLC.AddInteger) (Var () x)) + (mkConstant @Integer () 2) + +-- ifThenElse returns a function (lambda), then applied to an extra argument +overApplicationTerm :: Term Name DefaultUni DefaultFun () +overApplicationTerm = runQuote $ do + x <- freshName "x" + pure $ + Apply + () + ( mkIterApp + (Force () (Builtin () PLC.IfThenElse)) + [ ((), mkConstant @Bool () True) + , ((), LamAbs () x (mkConstant @Integer () 1)) + , ((), LamAbs () x (mkConstant @Integer () 2)) + ] + ) + (mkConstant @Integer () 3) + +-- Missing an argument, should be left unchanged +underApplicationTerm :: Term Name DefaultUni DefaultFun () +underApplicationTerm = + Apply () (Builtin () PLC.AddInteger) (mkConstant @Integer () 1) + +-- In both conservative and non-conservative mode: left unchanged because the +-- result (a G2 element) is an unserializable constant +uncompressBlsG2Term :: Term Name DefaultUni DefaultFun () +uncompressBlsG2Term = + Apply () (Builtin () PLC.Bls12_381_G2_uncompress) (mkConstant @BS.ByteString () blsG2Bytes) + where + blsG2Bytes = + decodeHex + ( "c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + ++ "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + ) + +-- In non-conservative mode: left unchanged because intermediate results +-- (G1 elements) are unserializable, so we can't evaluate through them +uncompressAndEqualBlsTerm :: Term Name DefaultUni DefaultFun () +uncompressAndEqualBlsTerm = + Apply + () + ( Apply + () + (Builtin () PLC.Bls12_381_G1_equal) + (Apply () (Builtin () PLC.Bls12_381_G1_uncompress) blsG1BytesTerm) + ) + (Apply () (Builtin () PLC.Bls12_381_G1_uncompress) blsG1BytesTerm) + where + blsG1BytesTerm = + mkConstant @BS.ByteString () $ + decodeHex + "97f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb" + +decodeHex :: String -> BS.ByteString +decodeHex hex = case Base16.decode (BS8.pack hex) of + Right bs -> bs + Left err -> error $ "Transform.EvaluateBuiltins.Spec: invalid hex: " <> err diff --git a/plutus-metatheory/src/CertifierReport.lagda.md b/plutus-metatheory/src/CertifierReport.lagda.md index 4a8752ef9d8..a9aa670a8e2 100644 --- a/plutus-metatheory/src/CertifierReport.lagda.md +++ b/plutus-metatheory/src/CertifierReport.lagda.md @@ -50,6 +50,7 @@ showCertifiedOptTag letFloatOutT = "Float bindings outwards" showUncertifiedOptTag : UncertifiedOptTag → String showUncertifiedOptTag caseOfCaseT = "Case-of-Case" +showUncertifiedOptTag constantFoldingT = "Constant Folding" showTag : OptTag → String showTag (inj₁ tag) = showUncertifiedOptTag tag ++ " ⚠ (certifier unavailable)" diff --git a/plutus-metatheory/src/FFI/AgdaUnparse.hs b/plutus-metatheory/src/FFI/AgdaUnparse.hs index f8538cb52ab..21d3231a8fb 100644 --- a/plutus-metatheory/src/FFI/AgdaUnparse.hs +++ b/plutus-metatheory/src/FFI/AgdaUnparse.hs @@ -65,6 +65,7 @@ instance AgdaUnparse CertifiedOptStage where instance AgdaUnparse UncertifiedOptStage where agdaUnparse CaseOfCase = "caseOfCaseT" + agdaUnparse ConstantFolding = "constantFoldingT" instance AgdaUnparse Hints.Hints where agdaUnparse = \case diff --git a/plutus-metatheory/src/MAlonzo/Code/Certifier.hs b/plutus-metatheory/src/MAlonzo/Code/Certifier.hs index 8e71614caa1..9f397525666 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Certifier.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Certifier.hs @@ -33,9 +33,9 @@ d_runCertifier_2 :: [MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_72 + MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208))] -> @@ -47,7 +47,7 @@ d_runCertifier_2 v0 MAlonzo.Code.Utils.du_eitherBind_54 (coe MAlonzo.Code.Utils.du_try_102 - (coe MAlonzo.Code.VerifiedCompilation.Trace.d_toTrace_98 (coe v0)) + (coe MAlonzo.Code.VerifiedCompilation.Trace.d_toTrace_102 (coe v0)) (coe MAlonzo.Code.VerifiedCompilation.C_emptyDump_4)) (coe (\ v1 -> @@ -77,14 +77,14 @@ runCertifierMain :: (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_72 + MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208))) -> MAlonzo.Code.Agda.Builtin.List.T_List_10 - () MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_134 -> + () MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_138 -> MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () (MAlonzo.Code.Utils.T__'215'__436 @@ -94,13 +94,13 @@ d_runCertifierMain_12 :: [MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_72 + MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208))] -> - [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_134] -> + [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_138] -> Maybe (MAlonzo.Code.Utils.T__'215'__436 Bool MAlonzo.Code.Agda.Builtin.String.T_String_6) diff --git a/plutus-metatheory/src/MAlonzo/Code/CertifierReport.hs b/plutus-metatheory/src/MAlonzo/Code/CertifierReport.hs index efba1670141..9bbeaf7ae3d 100644 --- a/plutus-metatheory/src/MAlonzo/Code/CertifierReport.hs +++ b/plutus-metatheory/src/MAlonzo/Code/CertifierReport.hs @@ -54,29 +54,29 @@ d_hl_8 Data.Text.Text) -- CertifierReport.showCertifiedOptTag d_showCertifiedOptTag_10 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_showCertifiedOptTag_10 v0 = case coe v0 of - MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_10 + MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_12 -> coe ("Float Delay" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_12 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_14 -> coe ("Force-Delay Cancellation" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_14 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_16 -> coe ("Float Force into Case Branches" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_16 + MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_18 -> coe ("Inlining" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_18 + MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_20 -> coe ("Common Subexpression Elimination" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_20 + MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_22 -> coe ("Transform multi-argument applications into case-constr form" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_22 + MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_24 -> coe ("Case-Constr and Case-Constant Cancellation" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_24 + MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_26 -> coe ("Float bindings outwards" :: Data.Text.Text) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showUncertifiedOptTag @@ -84,12 +84,17 @@ d_showUncertifiedOptTag_12 :: MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_showUncertifiedOptTag_12 v0 - = coe seq (coe v0) (coe ("Case-of-Case" :: Data.Text.Text)) + = case coe v0 of + MAlonzo.Code.VerifiedCompilation.Trace.C_caseOfCaseT_6 + -> coe ("Case-of-Case" :: Data.Text.Text) + MAlonzo.Code.VerifiedCompilation.Trace.C_constantFoldingT_8 + -> coe ("Constant Folding" :: Data.Text.Text) + _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showTag d_showTag_14 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_showTag_14 v0 = case coe v0 of @@ -800,34 +805,34 @@ d_numSitesCaseReduce'42'_186 v0 v1 v2 v3 d_numSites_222 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> Integer d_numSites_222 v0 v1 v2 v3 = case coe v2 of - MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_10 + MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_12 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_12 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_14 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_14 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_16 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_16 + MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_18 -> coe d_numSitesInline_140 (coe (0 :: Integer)) erased (coe MAlonzo.Code.VerifiedCompilation.UInline.C_'9633'_32) (coe MAlonzo.Code.VerifiedCompilation.UInline.C_'9633'_32) (coe MAlonzo.Code.VerifiedCompilation.UInline.C_'9633'_106) (coe v0) (coe v1) (coe v3) - MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_18 + MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_20 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_20 + MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_22 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_22 + MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_24 -> coe d_numSitesCaseReduce_178 (coe (0 :: Integer)) (coe v0) (coe v1) (coe MAlonzo.Code.VerifiedCompilation.UCaseReduce.du_sound_568 (coe (0 :: Integer)) (coe v0)) - MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_24 + MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_26 -> coe (0 :: Integer) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showSites @@ -836,7 +841,7 @@ d_showSites_248 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_showSites_248 v0 v1 v2 v3 = case coe v2 of @@ -902,11 +907,11 @@ d_termSize'7510''695'_260 v0 v1 _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showEvalResult d_showEvalResult_282 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_134 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_138 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_showEvalResult_282 v0 = case coe v0 of - MAlonzo.Code.VerifiedCompilation.Trace.C_success_136 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.C_success_140 v1 v2 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 (d_'8649'__2 (coe ("Execution Cost: CPU = " :: Data.Text.Text))) @@ -917,7 +922,7 @@ d_showEvalResult_282 v0 MAlonzo.Code.Data.String.Base.d__'43''43'__20 (", MEM = " :: Data.Text.Text) (coe MAlonzo.Code.Data.Nat.Show.d_show_56 v2))) - MAlonzo.Code.VerifiedCompilation.Trace.C_failure_138 v1 v2 v3 + MAlonzo.Code.VerifiedCompilation.Trace.C_failure_142 v1 v2 v3 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 (d_'8649'__2 (coe ("Evaluation FAILED: " :: Data.Text.Text))) @@ -938,7 +943,7 @@ d_showEvalResult_282 v0 _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showCostPair d_showCostPair_294 :: - [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_134] -> + [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_138] -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_showCostPair_294 v0 = let v1 = "" :: Data.Text.Text in @@ -972,13 +977,13 @@ du_tail_302 v0 -- CertifierReport.reportPasses d_reportPasses_312 :: Integer -> - MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_80 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_84 -> AgdaAny -> - [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_134] -> + [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_138] -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_reportPasses_312 v0 v1 v2 v3 = case coe v1 of - MAlonzo.Code.VerifiedCompilation.Trace.C_step_84 v4 v5 v6 v7 + MAlonzo.Code.VerifiedCompilation.Trace.C_step_88 v4 v5 v6 v7 -> case coe v2 of MAlonzo.Code.Utils.C__'44'__450 v8 v9 -> coe @@ -1021,7 +1026,7 @@ d_reportPasses_312 v0 v1 v2 v3 (d_termSize_256 (coe (0 :: Integer)) (coe - MAlonzo.Code.VerifiedCompilation.Trace.d_head_90 + MAlonzo.Code.VerifiedCompilation.Trace.d_head_94 (coe v7)))) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 @@ -1040,7 +1045,7 @@ d_reportPasses_312 v0 v1 v2 v3 (d_showSites_248 (coe v6) (coe - MAlonzo.Code.VerifiedCompilation.Trace.d_head_90 + MAlonzo.Code.VerifiedCompilation.Trace.d_head_94 (coe v7)) (coe v4) (coe v8)) (coe @@ -1057,7 +1062,7 @@ d_reportPasses_312 v0 v1 v2 v3 (coe v3)))))))))))))))))))) _ -> MAlonzo.RTE.mazUnreachableError - MAlonzo.Code.VerifiedCompilation.Trace.C_done_86 v4 + MAlonzo.Code.VerifiedCompilation.Trace.C_done_90 v4 -> coe ("" :: Data.Text.Text) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.reportFailure @@ -1112,7 +1117,7 @@ d_makeReport_334 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.T_Error_2 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> - [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_134] -> + [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_138] -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_makeReport_334 v0 v1 = coe diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs index e17a56886c8..b4562fe42ad 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs @@ -41,13 +41,13 @@ data T_Error_2 = C_emptyDump_4 | C_illScoped_6 | C_counterExample_8 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) | + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) | C_abort_10 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) -- VerifiedCompilation.tagToRelation d_tagToRelation_12 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> () d_tagToRelation_12 = erased @@ -55,7 +55,7 @@ d_tagToRelation_12 = erased d_RelationOf_14 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> () d_RelationOf_14 = erased @@ -63,15 +63,15 @@ d_RelationOf_14 = erased d_hasRelation_18 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> Bool d_hasRelation_18 = coe MAlonzo.Code.Utils.du_is'45'inj'8322'_46 -- VerifiedCompilation.certifyPass d_certifyPass_26 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_72 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_76 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.VerifiedCompilation.Certificate.T_CertResult_12 @@ -84,56 +84,56 @@ d_certifyPass_26 v0 v1 MAlonzo.Code.VerifiedCompilation.NotImplemented.du_certNotImplemented_22) MAlonzo.Code.Utils.C_inj'8322'_14 v2 -> case coe v2 of - MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_10 + MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_12 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192 (coe MAlonzo.Code.VerifiedCompilation.UFloatDelay.d_isFloatDelay'63'_488 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_12 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_14 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192 (coe MAlonzo.Code.VerifiedCompilation.UForceDelay.d_isForceDelay'63'_178 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_14 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_16 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192 (coe MAlonzo.Code.VerifiedCompilation.UForceCaseDelay.d_isForceCaseDelay'63'_94 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_16 + MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_18 -> case coe v1 of - MAlonzo.Code.VerifiedCompilation.Trace.C_inline_74 v3 + MAlonzo.Code.VerifiedCompilation.Trace.C_inline_78 v3 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_checker_156 (coe MAlonzo.Code.VerifiedCompilation.UInline.d_top'45'check_718 (coe v3)) - MAlonzo.Code.VerifiedCompilation.Trace.C_none_76 + MAlonzo.Code.VerifiedCompilation.Trace.C_none_80 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_32 - (coe MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34) + (coe MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36) _ -> MAlonzo.RTE.mazUnreachableError - MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_18 + MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_20 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192 (coe MAlonzo.Code.VerifiedCompilation.UCSE.d_isUntypedCSE'63'_22 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_20 + MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_22 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192 (coe MAlonzo.Code.VerifiedCompilation.UApplyToCase.d_a2c'63''7580''7580'_24 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_22 + MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_24 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192 (coe MAlonzo.Code.VerifiedCompilation.UCaseReduce.d_decide_526 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_24 + MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_26 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192 (coe @@ -143,19 +143,19 @@ d_certifyPass_26 v0 v1 _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.Certificate d_Certificate_34 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_80 -> () + MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_84 -> () d_Certificate_34 = erased -- VerifiedCompilation.certify d_certify_46 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_80 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_84 -> MAlonzo.Code.Utils.T_Either_6 T_Error_2 AgdaAny d_certify_46 v0 = case coe v0 of - MAlonzo.Code.VerifiedCompilation.Trace.C_step_84 v1 v2 v3 v4 + MAlonzo.Code.VerifiedCompilation.Trace.C_step_88 v1 v2 v3 v4 -> let v5 = coe d_certifyPass_26 v1 v2 v3 - (MAlonzo.Code.VerifiedCompilation.Trace.d_head_90 (coe v4)) in + (MAlonzo.Code.VerifiedCompilation.Trace.d_head_94 (coe v4)) in coe (case coe v5 of MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_18 v6 @@ -172,14 +172,14 @@ d_certify_46 v0 MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_32 v8 v9 v10 -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_abort_10 (coe v8)) _ -> MAlonzo.RTE.mazUnreachableError) - MAlonzo.Code.VerifiedCompilation.Trace.C_done_86 v1 + MAlonzo.Code.VerifiedCompilation.Trace.C_done_90 v1 -> coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8) _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.cert d_cert_96 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_80 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_84 -> MAlonzo.Code.Utils.T_Either_6 T_Error_2 AgdaAny -> AgdaAny -> AgdaAny d_cert_96 ~v0 v1 v2 = du_cert_96 v1 v2 @@ -200,11 +200,11 @@ d_checkScope_100 v0 (coe MAlonzo.Code.Untyped.d_scopeCheckU0_288 (coe v0)) -- VerifiedCompilation.checkScopeᵗ d_checkScope'7511'_102 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_80 -> - Maybe MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_80 + MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_84 -> + Maybe MAlonzo.Code.VerifiedCompilation.Trace.T_Trace_84 d_checkScope'7511'_102 v0 = case coe v0 of - MAlonzo.Code.VerifiedCompilation.Trace.C_step_84 v1 v2 v3 v4 + MAlonzo.Code.VerifiedCompilation.Trace.C_step_88 v1 v2 v3 v4 -> coe MAlonzo.Code.Data.Maybe.Base.du__'62''62''61'__72 (coe d_checkScope_100 (coe v3)) @@ -218,9 +218,9 @@ d_checkScope'7511'_102 v0 coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C_step_84 (coe v1) (coe v2) + MAlonzo.Code.VerifiedCompilation.Trace.C_step_88 (coe v1) (coe v2) (coe v5) (coe v6)))))) - MAlonzo.Code.VerifiedCompilation.Trace.C_done_86 v1 + MAlonzo.Code.VerifiedCompilation.Trace.C_done_90 v1 -> coe MAlonzo.Code.Data.Maybe.Base.du__'62''62''61'__72 (coe d_checkScope_100 (coe v1)) @@ -228,5 +228,5 @@ d_checkScope'7511'_102 v0 (\ v2 -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 - (coe MAlonzo.Code.VerifiedCompilation.Trace.C_done_86 (coe v2)))) + (coe MAlonzo.Code.VerifiedCompilation.Trace.C_done_90 (coe v2)))) _ -> MAlonzo.RTE.mazUnreachableError diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs index 2779b21e7f6..74b444bfe0f 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs @@ -33,11 +33,11 @@ data T_CertResult_12 = C_proof_18 AgdaAny | C_ce_26 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) AgdaAny AgdaAny | C_abort_32 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) AgdaAny AgdaAny -- VerifiedCompilation.Certificate.ProofOrCE d_ProofOrCE_38 a0 a1 = () @@ -45,7 +45,7 @@ data T_ProofOrCE_38 = C_proof_44 AgdaAny | C_ce_52 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) AgdaAny AgdaAny -- VerifiedCompilation.Certificate.isProof? d_isProof'63'_56 :: @@ -74,7 +74,7 @@ data T_Proof'63'_66 = C_proof_72 AgdaAny | C_abort_78 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) AgdaAny AgdaAny -- VerifiedCompilation.Certificate._>>=_ d__'62''62''61'__88 :: @@ -145,14 +145,14 @@ d_decToPCE_234 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38 d_decToPCE_234 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_234 v2 v3 v4 v5 du_decToPCE_234 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38 du_decToPCE_234 v0 v1 v2 v3 @@ -195,7 +195,7 @@ d_matchOrCE_262 :: (AgdaAny -> AgdaAny -> ()) -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> @@ -205,7 +205,7 @@ d_matchOrCE_262 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 du_matchOrCE_262 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> @@ -230,7 +230,7 @@ d_pcePointwise_304 :: (AgdaAny -> AgdaAny -> ()) -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_38) -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38 d_pcePointwise_304 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 @@ -238,7 +238,7 @@ d_pcePointwise_304 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 du_pcePointwise_304 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_38) -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38 du_pcePointwise_304 v0 v1 v2 v3 diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Trace.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Trace.hs index ccdacc08c75..8469da9f5c5 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Trace.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Trace.hs @@ -30,41 +30,45 @@ import FFI.CostInfo d_UncertifiedOptTag_4 = () type T_UncertifiedOptTag_4 = UncertifiedOptStage pattern C_caseOfCaseT_6 = CaseOfCase +pattern C_constantFoldingT_8 = ConstantFolding check_caseOfCaseT_6 :: T_UncertifiedOptTag_4 check_caseOfCaseT_6 = CaseOfCase +check_constantFoldingT_8 :: T_UncertifiedOptTag_4 +check_constantFoldingT_8 = ConstantFolding cover_UncertifiedOptTag_4 :: UncertifiedOptStage -> () cover_UncertifiedOptTag_4 x = case x of CaseOfCase -> () + ConstantFolding -> () -- VerifiedCompilation.Trace.CertifiedOptTag -d_CertifiedOptTag_8 = () -type T_CertifiedOptTag_8 = CertifiedOptStage -pattern C_floatDelayT_10 = FloatDelay -pattern C_forceDelayT_12 = ForceDelay -pattern C_forceCaseDelayT_14 = ForceCaseDelay -pattern C_inlineT_16 = Inline -pattern C_cseT_18 = CSE -pattern C_applyToCaseT_20 = ApplyToCase -pattern C_caseReduceT_22 = CaseReduce -pattern C_letFloatOutT_24 = LetFloatOut -check_floatDelayT_10 :: T_CertifiedOptTag_8 -check_floatDelayT_10 = FloatDelay -check_forceDelayT_12 :: T_CertifiedOptTag_8 -check_forceDelayT_12 = ForceDelay -check_forceCaseDelayT_14 :: T_CertifiedOptTag_8 -check_forceCaseDelayT_14 = ForceCaseDelay -check_inlineT_16 :: T_CertifiedOptTag_8 -check_inlineT_16 = Inline -check_cseT_18 :: T_CertifiedOptTag_8 -check_cseT_18 = CSE -check_applyToCaseT_20 :: T_CertifiedOptTag_8 -check_applyToCaseT_20 = ApplyToCase -check_caseReduceT_22 :: T_CertifiedOptTag_8 -check_caseReduceT_22 = CaseReduce -check_letFloatOutT_24 :: T_CertifiedOptTag_8 -check_letFloatOutT_24 = LetFloatOut -cover_CertifiedOptTag_8 :: CertifiedOptStage -> () -cover_CertifiedOptTag_8 x +d_CertifiedOptTag_10 = () +type T_CertifiedOptTag_10 = CertifiedOptStage +pattern C_floatDelayT_12 = FloatDelay +pattern C_forceDelayT_14 = ForceDelay +pattern C_forceCaseDelayT_16 = ForceCaseDelay +pattern C_inlineT_18 = Inline +pattern C_cseT_20 = CSE +pattern C_applyToCaseT_22 = ApplyToCase +pattern C_caseReduceT_24 = CaseReduce +pattern C_letFloatOutT_26 = LetFloatOut +check_floatDelayT_12 :: T_CertifiedOptTag_10 +check_floatDelayT_12 = FloatDelay +check_forceDelayT_14 :: T_CertifiedOptTag_10 +check_forceDelayT_14 = ForceDelay +check_forceCaseDelayT_16 :: T_CertifiedOptTag_10 +check_forceCaseDelayT_16 = ForceCaseDelay +check_inlineT_18 :: T_CertifiedOptTag_10 +check_inlineT_18 = Inline +check_cseT_20 :: T_CertifiedOptTag_10 +check_cseT_20 = CSE +check_applyToCaseT_22 :: T_CertifiedOptTag_10 +check_applyToCaseT_22 = ApplyToCase +check_caseReduceT_24 :: T_CertifiedOptTag_10 +check_caseReduceT_24 = CaseReduce +check_letFloatOutT_26 :: T_CertifiedOptTag_10 +check_letFloatOutT_26 = LetFloatOut +cover_CertifiedOptTag_10 :: CertifiedOptStage -> () +cover_CertifiedOptTag_10 x = case x of FloatDelay -> () ForceDelay -> () @@ -75,108 +79,114 @@ cover_CertifiedOptTag_8 x CaseReduce -> () LetFloatOut -> () -- VerifiedCompilation.Trace.OptTag -d_OptTag_26 :: () -d_OptTag_26 = erased +d_OptTag_28 :: () +d_OptTag_28 = erased -- VerifiedCompilation.Trace.FloatDelayT -d_FloatDelayT_28 :: +d_FloatDelayT_30 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 -d_FloatDelayT_28 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_floatDelayT_10) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_FloatDelayT_30 + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_floatDelayT_12) -- VerifiedCompilation.Trace.ForceDelayT -d_ForceDelayT_30 :: +d_ForceDelayT_32 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 -d_ForceDelayT_30 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_forceDelayT_12) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_ForceDelayT_32 + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_forceDelayT_14) -- VerifiedCompilation.Trace.ForceCaseDelayT -d_ForceCaseDelayT_32 :: +d_ForceCaseDelayT_34 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 -d_ForceCaseDelayT_32 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_forceCaseDelayT_14) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_ForceCaseDelayT_34 + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_forceCaseDelayT_16) -- VerifiedCompilation.Trace.InlineT -d_InlineT_34 :: +d_InlineT_36 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 -d_InlineT_34 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_inlineT_16) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_InlineT_36 + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_inlineT_18) -- VerifiedCompilation.Trace.CseT -d_CseT_36 :: +d_CseT_38 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 -d_CseT_36 = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_cseT_18) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_CseT_38 = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_cseT_20) -- VerifiedCompilation.Trace.ApplyToCaseT -d_ApplyToCaseT_38 :: +d_ApplyToCaseT_40 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 -d_ApplyToCaseT_38 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_applyToCaseT_20) --- VerifiedCompilation.Trace.CaseOfCaseT -d_CaseOfCaseT_40 :: - MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 -d_CaseOfCaseT_40 - = coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_caseOfCaseT_6) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_ApplyToCaseT_40 + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_applyToCaseT_22) -- VerifiedCompilation.Trace.LetFloatOutT d_LetFloatOutT_42 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_LetFloatOutT_42 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_letFloatOutT_24) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_letFloatOutT_26) -- VerifiedCompilation.Trace.CaseReduceT d_CaseReduceT_44 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_CaseReduceT_44 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_caseReduceT_22) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_caseReduceT_24) +-- VerifiedCompilation.Trace.CaseOfCaseT +d_CaseOfCaseT_46 :: + MAlonzo.Code.Utils.T_Either_6 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_CaseOfCaseT_46 + = coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_caseOfCaseT_6) +-- VerifiedCompilation.Trace.ConstantFoldingT +d_ConstantFoldingT_48 :: + MAlonzo.Code.Utils.T_Either_6 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_ConstantFoldingT_48 + = coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_constantFoldingT_8) -- VerifiedCompilation.Trace.InlineHints -d_InlineHints_46 = () -type T_InlineHints_46 = Hints.Inline -pattern C_var_48 = Hints.InlVar -pattern C_expand_50 a0 = Hints.InlExpand a0 -pattern C_ƛ_52 a0 = Hints.InlLam a0 -pattern C__'183'__54 a0 a1 = Hints.InlApply a0 a1 -pattern C__'183''8595'_56 a0 = Hints.InlDrop a0 -pattern C_force_58 a0 = Hints.InlForce a0 -pattern C_delay_60 a0 = Hints.InlDelay a0 -pattern C_con_62 = Hints.InlCon -pattern C_builtin_64 = Hints.InlBuiltin -pattern C_error_66 = Hints.InlError -pattern C_constr_68 a0 = Hints.InlConstr a0 -pattern C_case_70 a0 a1 = Hints.InlCase a0 a1 -check_var_48 :: T_InlineHints_46 -check_var_48 = Hints.InlVar -check_expand_50 :: T_InlineHints_46 -> T_InlineHints_46 -check_expand_50 = Hints.InlExpand -check_ƛ_52 :: T_InlineHints_46 -> T_InlineHints_46 -check_ƛ_52 = Hints.InlLam -check__'183'__54 :: - T_InlineHints_46 -> T_InlineHints_46 -> T_InlineHints_46 -check__'183'__54 = Hints.InlApply -check__'183''8595'_56 :: T_InlineHints_46 -> T_InlineHints_46 -check__'183''8595'_56 = Hints.InlDrop -check_force_58 :: T_InlineHints_46 -> T_InlineHints_46 -check_force_58 = Hints.InlForce -check_delay_60 :: T_InlineHints_46 -> T_InlineHints_46 -check_delay_60 = Hints.InlDelay -check_con_62 :: T_InlineHints_46 -check_con_62 = Hints.InlCon -check_builtin_64 :: T_InlineHints_46 -check_builtin_64 = Hints.InlBuiltin -check_error_66 :: T_InlineHints_46 -check_error_66 = Hints.InlError -check_constr_68 :: - MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_46 -> - T_InlineHints_46 -check_constr_68 = Hints.InlConstr -check_case_70 :: - T_InlineHints_46 -> - MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_46 -> - T_InlineHints_46 -check_case_70 = Hints.InlCase -cover_InlineHints_46 :: Hints.Inline -> () -cover_InlineHints_46 x +d_InlineHints_50 = () +type T_InlineHints_50 = Hints.Inline +pattern C_var_52 = Hints.InlVar +pattern C_expand_54 a0 = Hints.InlExpand a0 +pattern C_ƛ_56 a0 = Hints.InlLam a0 +pattern C__'183'__58 a0 a1 = Hints.InlApply a0 a1 +pattern C__'183''8595'_60 a0 = Hints.InlDrop a0 +pattern C_force_62 a0 = Hints.InlForce a0 +pattern C_delay_64 a0 = Hints.InlDelay a0 +pattern C_con_66 = Hints.InlCon +pattern C_builtin_68 = Hints.InlBuiltin +pattern C_error_70 = Hints.InlError +pattern C_constr_72 a0 = Hints.InlConstr a0 +pattern C_case_74 a0 a1 = Hints.InlCase a0 a1 +check_var_52 :: T_InlineHints_50 +check_var_52 = Hints.InlVar +check_expand_54 :: T_InlineHints_50 -> T_InlineHints_50 +check_expand_54 = Hints.InlExpand +check_ƛ_56 :: T_InlineHints_50 -> T_InlineHints_50 +check_ƛ_56 = Hints.InlLam +check__'183'__58 :: + T_InlineHints_50 -> T_InlineHints_50 -> T_InlineHints_50 +check__'183'__58 = Hints.InlApply +check__'183''8595'_60 :: T_InlineHints_50 -> T_InlineHints_50 +check__'183''8595'_60 = Hints.InlDrop +check_force_62 :: T_InlineHints_50 -> T_InlineHints_50 +check_force_62 = Hints.InlForce +check_delay_64 :: T_InlineHints_50 -> T_InlineHints_50 +check_delay_64 = Hints.InlDelay +check_con_66 :: T_InlineHints_50 +check_con_66 = Hints.InlCon +check_builtin_68 :: T_InlineHints_50 +check_builtin_68 = Hints.InlBuiltin +check_error_70 :: T_InlineHints_50 +check_error_70 = Hints.InlError +check_constr_72 :: + MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_50 -> + T_InlineHints_50 +check_constr_72 = Hints.InlConstr +check_case_74 :: + T_InlineHints_50 -> + MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_50 -> + T_InlineHints_50 +check_case_74 = Hints.InlCase +cover_InlineHints_50 :: Hints.Inline -> () +cover_InlineHints_50 x = case x of Hints.InlVar -> () Hints.InlExpand _ -> () @@ -191,110 +201,110 @@ cover_InlineHints_46 x Hints.InlConstr _ -> () Hints.InlCase _ _ -> () -- VerifiedCompilation.Trace.Hints -d_Hints_72 = () -type T_Hints_72 = Hints.Hints -pattern C_inline_74 a0 = Hints.Inline a0 -pattern C_none_76 = Hints.NoHints -check_inline_74 :: T_InlineHints_46 -> T_Hints_72 -check_inline_74 = Hints.Inline -check_none_76 :: T_Hints_72 -check_none_76 = Hints.NoHints -cover_Hints_72 :: Hints.Hints -> () -cover_Hints_72 x +d_Hints_76 = () +type T_Hints_76 = Hints.Hints +pattern C_inline_78 a0 = Hints.Inline a0 +pattern C_none_80 = Hints.NoHints +check_inline_78 :: T_InlineHints_50 -> T_Hints_76 +check_inline_78 = Hints.Inline +check_none_80 :: T_Hints_76 +check_none_80 = Hints.NoHints +cover_Hints_76 :: Hints.Hints -> () +cover_Hints_76 x = case x of Hints.Inline _ -> () Hints.NoHints -> () -- VerifiedCompilation.Trace.Trace -d_Trace_80 a0 = () -data T_Trace_80 - = C_step_84 (MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8) - T_Hints_72 AgdaAny T_Trace_80 | - C_done_86 AgdaAny +d_Trace_84 a0 = () +data T_Trace_84 + = C_step_88 (MAlonzo.Code.Utils.T_Either_6 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10) + T_Hints_76 AgdaAny T_Trace_84 | + C_done_90 AgdaAny -- VerifiedCompilation.Trace.head -d_head_90 :: T_Trace_80 -> AgdaAny -d_head_90 v0 +d_head_94 :: T_Trace_84 -> AgdaAny +d_head_94 v0 = case coe v0 of - C_step_84 v1 v2 v3 v4 -> coe v3 - C_done_86 v1 -> coe v1 + C_step_88 v1 v2 v3 v4 -> coe v3 + C_done_90 v1 -> coe v1 _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.Trace.Dump -d_Dump_96 :: () -d_Dump_96 = erased +d_Dump_100 :: () +d_Dump_100 = erased -- VerifiedCompilation.Trace.toTrace -d_toTrace_98 :: +d_toTrace_102 :: [MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - T_Hints_72 + T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208))] -> - Maybe T_Trace_80 -d_toTrace_98 v0 + Maybe T_Trace_84 +d_toTrace_102 v0 = case coe v0 of [] -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 (:) v1 v2 -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 - (coe du_go_108 (coe v1) (coe v2)) + (coe du_go_112 (coe v1) (coe v2)) _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.Trace._.go -d_go_108 :: +d_go_112 :: MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - T_Hints_72 + T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208)) -> [MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - T_Hints_72 + T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208))] -> MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - T_Hints_72 + T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208)) -> [MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - T_Hints_72 + T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208))] -> - T_Trace_80 -d_go_108 ~v0 ~v1 v2 v3 = du_go_108 v2 v3 -du_go_108 :: + T_Trace_84 +d_go_112 ~v0 ~v1 v2 v3 = du_go_112 v2 v3 +du_go_112 :: MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - T_Hints_72 + T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208)) -> [MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_8) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10) (MAlonzo.Code.Utils.T__'215'__436 - T_Hints_72 + T_Hints_76 (MAlonzo.Code.Utils.T__'215'__436 MAlonzo.Code.RawU.T_Untyped_208 MAlonzo.Code.RawU.T_Untyped_208))] -> - T_Trace_80 -du_go_108 v0 v1 + T_Trace_84 +du_go_112 v0 v1 = case coe v0 of MAlonzo.Code.Utils.C__'44'__450 v2 v3 -> case coe v3 of @@ -304,7 +314,7 @@ du_go_108 v0 v1 -> case coe v1 of [] -> coe - C_step_84 (coe v2) (coe v4) (coe v6) (coe C_done_86 (coe v7)) + C_step_88 (coe v2) (coe v4) (coe v6) (coe C_done_90 (coe v7)) (:) v8 v9 -> case coe v8 of MAlonzo.Code.Utils.C__'44'__450 v10 v11 @@ -313,9 +323,9 @@ du_go_108 v0 v1 -> case coe v13 of MAlonzo.Code.Utils.C__'44'__450 v14 v15 -> coe - C_step_84 (coe v2) (coe v4) (coe v6) + C_step_88 (coe v2) (coe v4) (coe v6) (coe - du_go_108 + du_go_112 (coe MAlonzo.Code.Utils.C__'44'__450 (coe v10) @@ -334,18 +344,18 @@ du_go_108 v0 v1 _ -> MAlonzo.RTE.mazUnreachableError _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.Trace.EvalResult -d_EvalResult_134 = () -type T_EvalResult_134 = EvalResult -pattern C_success_136 a0 a1 = EvalSuccess a0 a1 -pattern C_failure_138 a0 a1 a2 = EvalFailure a0 a1 a2 -check_success_136 :: Integer -> Integer -> T_EvalResult_134 -check_success_136 = EvalSuccess -check_failure_138 :: +d_EvalResult_138 = () +type T_EvalResult_138 = EvalResult +pattern C_success_140 a0 a1 = EvalSuccess a0 a1 +pattern C_failure_142 a0 a1 a2 = EvalFailure a0 a1 a2 +check_success_140 :: Integer -> Integer -> T_EvalResult_138 +check_success_140 = EvalSuccess +check_failure_142 :: MAlonzo.Code.Agda.Builtin.String.T_String_6 -> - Integer -> Integer -> T_EvalResult_134 -check_failure_138 = EvalFailure -cover_EvalResult_134 :: EvalResult -> () -cover_EvalResult_134 x + Integer -> Integer -> T_EvalResult_138 +check_failure_142 = EvalFailure +cover_EvalResult_138 :: EvalResult -> () +cover_EvalResult_138 x = case x of EvalSuccess _ _ -> () EvalFailure _ _ _ -> () diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UApplyToCase.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UApplyToCase.hs index ce1e464715e..8cf849a9249 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UApplyToCase.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UApplyToCase.hs @@ -44,7 +44,7 @@ d_a2c'63''7580''7580'_24 v0 = coe MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_160 (coe v0) - (coe MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38) + (coe MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40) (coe d_a2c'63'_32) -- VerifiedCompilation.UApplyToCase.a2c? d_a2c'63'_32 :: @@ -75,31 +75,31 @@ d_a2c'63'_32 v0 v1 v2 MAlonzo.Code.Untyped.C_'96'_18 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 MAlonzo.Code.Untyped.C_ƛ_20 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 MAlonzo.Code.Untyped.C__'183'__22 v5 v6 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 MAlonzo.Code.Untyped.C_force_24 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 MAlonzo.Code.Untyped.C_delay_26 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 MAlonzo.Code.Untyped.C_con_28 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 MAlonzo.Code.Untyped.C_constr_34 v5 v6 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 MAlonzo.Code.Untyped.C_case_40 v5 v6 -> let v7 = coe @@ -241,18 +241,18 @@ d_a2c'63'_32 v0 v1 v2 seq (coe v12) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError) MAlonzo.Code.Untyped.C_builtin_44 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 MAlonzo.Code.Untyped.C_error_46 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_38 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_ApplyToCaseT_40 v1 v2 _ -> MAlonzo.RTE.mazUnreachableError)) -- VerifiedCompilation.UApplyToCase..extendedlambda0 d_'46'extendedlambda0_48 :: @@ -276,7 +276,7 @@ d_'46'extendedlambda1_94 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> T_ApplyToCase_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs index fa1445b10ac..dfdfd4db1af 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs @@ -54,7 +54,7 @@ d_isUntypedCSE'63'_22 :: d_isUntypedCSE'63'_22 v0 = coe MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_160 - (coe v0) (coe MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36) + (coe v0) (coe MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38) (coe d_isUCSE'63'_24) -- VerifiedCompilation.UCSE.isUCSE? d_isUCSE'63'_24 :: @@ -75,17 +75,17 @@ d_isUCSE'63'_24 v0 v1 v2 MAlonzo.Code.Untyped.C_'96'_18 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_ƛ_20 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C__'183'__22 v5 v6 -> case coe v5 of MAlonzo.Code.Untyped.C_'96'_18 v7 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_ƛ_20 v7 -> let v8 = coe @@ -199,7 +199,7 @@ d_isUCSE'63'_24 v0 v1 v2 v21) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -311,7 +311,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -372,7 +372,7 @@ d_isUCSE'63'_24 v0 v1 v2 v23) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -385,7 +385,7 @@ d_isUCSE'63'_24 v0 v1 v2 MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) MAlonzo.Code.Untyped.C__'183'__22 v14 v15 -> case coe v14 of @@ -592,7 +592,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -805,7 +805,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -866,7 +866,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -1025,7 +1025,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -1188,7 +1188,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -1253,7 +1253,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -1462,7 +1462,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -1675,7 +1675,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -1736,7 +1736,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -1945,7 +1945,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -2158,7 +2158,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -2219,7 +2219,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -2428,7 +2428,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -2641,7 +2641,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -2702,7 +2702,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -2911,7 +2911,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -3124,7 +3124,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -3185,7 +3185,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -3394,7 +3394,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -3607,7 +3607,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -3668,7 +3668,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -3877,7 +3877,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -4090,7 +4090,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -4151,7 +4151,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -4360,7 +4360,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -4573,7 +4573,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -4634,7 +4634,7 @@ d_isUCSE'63'_24 v0 v1 v2 v25) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -4843,7 +4843,7 @@ d_isUCSE'63'_24 v0 v1 v2 v24) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -5056,7 +5056,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -5117,7 +5117,7 @@ d_isUCSE'63'_24 v0 v1 v2 v24) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -5226,7 +5226,7 @@ d_isUCSE'63'_24 v0 v1 v2 v21) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -5345,7 +5345,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -5406,7 +5406,7 @@ d_isUCSE'63'_24 v0 v1 v2 v23) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -5419,7 +5419,7 @@ d_isUCSE'63'_24 v0 v1 v2 MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) MAlonzo.Code.Untyped.C_con_28 v14 -> coe @@ -5428,7 +5428,7 @@ d_isUCSE'63'_24 v0 v1 v2 MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) MAlonzo.Code.Untyped.C_constr_34 v14 v15 -> let v16 @@ -5539,7 +5539,7 @@ d_isUCSE'63'_24 v0 v1 v2 v24) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -5659,7 +5659,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -5720,7 +5720,7 @@ d_isUCSE'63'_24 v0 v1 v2 v24) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -5835,7 +5835,7 @@ d_isUCSE'63'_24 v0 v1 v2 v24) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -5955,7 +5955,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -6016,7 +6016,7 @@ d_isUCSE'63'_24 v0 v1 v2 v24) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -6029,7 +6029,7 @@ d_isUCSE'63'_24 v0 v1 v2 MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) MAlonzo.Code.Untyped.C_error_46 -> coe @@ -6038,7 +6038,7 @@ d_isUCSE'63'_24 v0 v1 v2 MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError @@ -6162,7 +6162,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -6274,7 +6274,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -6335,7 +6335,7 @@ d_isUCSE'63'_24 v0 v1 v2 v28) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -6346,7 +6346,7 @@ d_isUCSE'63'_24 v0 v1 v2 seq (coe v9) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) MAlonzo.Code.Untyped.C__'183'__22 v19 v20 -> case coe @@ -6556,7 +6556,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -6769,7 +6769,7 @@ d_isUCSE'63'_24 v0 v1 v2 v35) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -6830,7 +6830,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -6991,7 +6991,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -7154,7 +7154,7 @@ d_isUCSE'63'_24 v0 v1 v2 v35) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -7219,7 +7219,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -7430,7 +7430,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -7643,7 +7643,7 @@ d_isUCSE'63'_24 v0 v1 v2 v36) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -7704,7 +7704,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -7915,7 +7915,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -8128,7 +8128,7 @@ d_isUCSE'63'_24 v0 v1 v2 v35) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -8189,7 +8189,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -8400,7 +8400,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -8613,7 +8613,7 @@ d_isUCSE'63'_24 v0 v1 v2 v35) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -8674,7 +8674,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -8885,7 +8885,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -9098,7 +9098,7 @@ d_isUCSE'63'_24 v0 v1 v2 v35) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -9159,7 +9159,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -9370,7 +9370,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -9583,7 +9583,7 @@ d_isUCSE'63'_24 v0 v1 v2 v36) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -9644,7 +9644,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -9855,7 +9855,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -10068,7 +10068,7 @@ d_isUCSE'63'_24 v0 v1 v2 v36) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -10129,7 +10129,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -10340,7 +10340,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -10553,7 +10553,7 @@ d_isUCSE'63'_24 v0 v1 v2 v35) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -10614,7 +10614,7 @@ d_isUCSE'63'_24 v0 v1 v2 v30) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -10825,7 +10825,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -11038,7 +11038,7 @@ d_isUCSE'63'_24 v0 v1 v2 v34) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -11099,7 +11099,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -11211,7 +11211,7 @@ d_isUCSE'63'_24 v0 v1 v2 v26) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -11330,7 +11330,7 @@ d_isUCSE'63'_24 v0 v1 v2 v31) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -11391,7 +11391,7 @@ d_isUCSE'63'_24 v0 v1 v2 v28) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -11402,14 +11402,14 @@ d_isUCSE'63'_24 v0 v1 v2 seq (coe v9) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) MAlonzo.Code.Untyped.C_con_28 v19 -> coe seq (coe v9) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) MAlonzo.Code.Untyped.C_constr_34 v19 v20 -> let v21 @@ -11523,7 +11523,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -11643,7 +11643,7 @@ d_isUCSE'63'_24 v0 v1 v2 v34) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -11704,7 +11704,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -11822,7 +11822,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -11942,7 +11942,7 @@ d_isUCSE'63'_24 v0 v1 v2 v34) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -12003,7 +12003,7 @@ d_isUCSE'63'_24 v0 v1 v2 v29) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -12014,14 +12014,14 @@ d_isUCSE'63'_24 v0 v1 v2 seq (coe v9) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) MAlonzo.Code.Untyped.C_error_46 -> coe seq (coe v9) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError @@ -12030,71 +12030,71 @@ d_isUCSE'63'_24 v0 v1 v2 seq (coe v13) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError) MAlonzo.Code.Untyped.C__'183'__22 v7 v8 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_force_24 v7 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_delay_26 v7 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_con_28 v7 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_constr_34 v7 v8 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_case_40 v7 v8 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_builtin_44 v7 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_error_46 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 _ -> MAlonzo.RTE.mazUnreachableError MAlonzo.Code.Untyped.C_force_24 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_delay_26 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_con_28 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_constr_34 v5 v6 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_case_40 v5 v6 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_builtin_44 v5 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 MAlonzo.Code.Untyped.C_error_46 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_36 v1 v2 + MAlonzo.Code.VerifiedCompilation.Trace.d_CseT_38 v1 v2 _ -> MAlonzo.RTE.mazUnreachableError)) -- VerifiedCompilation.UCSE..extendedlambda0 d_'46'extendedlambda0_40 :: @@ -12127,7 +12127,7 @@ d_'46'extendedlambda2_106 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.Strictness.T__'8712''8595'__10 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs index 685682943f5..6ddd6cdeabf 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs @@ -560,7 +560,7 @@ d_isCaseOfCase'63'_256 v0 = coe MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_160 (coe v0) - (coe MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_40) + (coe MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_46) (coe d_isCoC'63'_264) -- VerifiedCompilation.UCaseOfCase.isCoC? d_isCoC'63'_264 :: @@ -671,7 +671,7 @@ d_isCoC'63'_264 v0 v1 v2 = coe MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_304 (coe - MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_40) + MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_46) (coe d_isCaseOfCase'63'_256 (coe @@ -688,7 +688,7 @@ d_isCoC'63'_264 v0 v1 v2 = coe MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_304 (coe - MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_40) + MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_46) (coe d_isCaseOfCase'63'_256 (coe @@ -705,7 +705,7 @@ d_isCoC'63'_264 v0 v1 v2 = coe MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_304 (coe - MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_40) + MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_46) (coe d_isCaseOfCase'63'_256 (coe @@ -754,7 +754,7 @@ d_isCoC'63'_264 v0 v1 v2 v40) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_40 + MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_46 (coe MAlonzo.Code.Untyped.C_case_40 (coe @@ -826,7 +826,7 @@ d_isCoC'63'_264 v0 v1 v2 seq (coe v5) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_40 v1 v2) + MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_46 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) -- VerifiedCompilation.UCaseOfCase..extendedlambda4 d_'46'extendedlambda4_280 :: @@ -867,7 +867,7 @@ d_'46'extendedlambda6_444 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -890,7 +890,7 @@ d_'46'extendedlambda7_524 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> [MAlonzo.Code.Untyped.T__'8866'_14] -> @@ -914,7 +914,7 @@ d_'46'extendedlambda8_608 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> [MAlonzo.Code.Untyped.T__'8866'_14] -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UFloatDelay.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UFloatDelay.hs index 7d089021985..30375befea6 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UFloatDelay.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UFloatDelay.hs @@ -541,7 +541,7 @@ d_isFloatDelay'63'_488 v0 = coe MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_160 (coe v0) - (coe MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_28) + (coe MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_30) (coe d_isFlD'63'_492) -- VerifiedCompilation.UFloatDelay.isFlD? d_isFlD'63'_492 :: @@ -697,7 +697,7 @@ d_isFlD'63'_492 v0 v1 v2 v38) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_28 + MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_30 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) @@ -726,7 +726,7 @@ d_isFlD'63'_492 v0 v1 v2 v21) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_28 + MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_30 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -741,7 +741,7 @@ d_isFlD'63'_492 v0 v1 v2 seq (coe v5) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_28 v1 v2) + MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_30 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) -- VerifiedCompilation.UFloatDelay..extendedlambda8 d_'46'extendedlambda8_508 :: @@ -773,7 +773,7 @@ d_'46'extendedlambda10_582 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -791,7 +791,7 @@ d_'46'extendedlambda11_630 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceCaseDelay.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceCaseDelay.hs index ea967ee8ca9..7fdd343f527 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceCaseDelay.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceCaseDelay.hs @@ -167,7 +167,7 @@ d_isForceCaseDelay'63'_94 v0 = coe MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_160 (coe v0) - (coe MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_32) + (coe MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_34) (coe d_isFCD'63'_96) -- VerifiedCompilation.UForceCaseDelay.isFCD? d_isFCD'63'_96 :: @@ -271,7 +271,7 @@ d_isFCD'63'_96 v0 v1 v2 = coe MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_304 (coe - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_32) + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_34) (coe d_isForceCaseDelay'63'_94 (coe @@ -298,14 +298,14 @@ d_isFCD'63'_96 v0 v1 v2 MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 v36 v37 v38 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_32 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_34 v1 v2 _ -> MAlonzo.RTE.mazUnreachableError) MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 v34 v35 v36 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_32 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_34 v1 v2 _ -> MAlonzo.RTE.mazUnreachableError) @@ -316,7 +316,7 @@ d_isFCD'63'_96 v0 v1 v2 v28) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_32 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_34 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError))) @@ -327,7 +327,7 @@ d_isFCD'63'_96 v0 v1 v2 seq (coe v18) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_32 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_34 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError))) _ -> MAlonzo.RTE.mazUnreachableError @@ -339,7 +339,7 @@ d_isFCD'63'_96 v0 v1 v2 seq (coe v5) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_32 v1 v2) + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_34 v1 v2) _ -> MAlonzo.RTE.mazUnreachableError) -- VerifiedCompilation.UForceCaseDelay..extendedlambda1 d_'46'extendedlambda1_112 :: @@ -382,7 +382,7 @@ d_'46'extendedlambda4_228 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> [MAlonzo.Code.Untyped.T__'8866'_14] -> @@ -401,7 +401,7 @@ d_'46'extendedlambda5_280 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs index 45778cf2700..ceddcb16d09 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs @@ -583,7 +583,7 @@ d_isForceDelay'63'_178 v0 = coe MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_160 (coe v0) - (coe MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30) + (coe MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32) (coe (\ v1 -> d_isFD'63'_184 (coe v1) (coe C_'9633'_82))) -- VerifiedCompilation.UForceDelay.isFD? d_isFD'63'_184 :: @@ -745,7 +745,7 @@ d_isFD'63'_184 v0 v1 v2 v3 seq (coe v9) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v2 v3) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError) @@ -1114,7 +1114,7 @@ d_isFD'63'_184 v0 v1 v2 v3 v87) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v2 v3) _ -> MAlonzo.RTE.mazUnreachableError) @@ -1146,7 +1146,7 @@ d_isFD'63'_184 v0 v1 v2 v3 v80) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v16 v22) _ -> MAlonzo.RTE.mazUnreachableError @@ -1157,7 +1157,7 @@ d_isFD'63'_184 v0 v1 v2 v3 v77) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v43 v59) _ -> MAlonzo.RTE.mazUnreachableError))))) @@ -1329,7 +1329,7 @@ d_isFD'63'_184 v0 v1 v2 v3 seq (coe v13) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v2 v3) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -1851,7 +1851,7 @@ d_isFD'63'_184 v0 v1 v2 v3 v98) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v15 v3) _ -> MAlonzo.RTE.mazUnreachableError) @@ -1883,7 +1883,7 @@ d_isFD'63'_184 v0 v1 v2 v3 v91) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v27 v33) _ -> MAlonzo.RTE.mazUnreachableError @@ -1894,7 +1894,7 @@ d_isFD'63'_184 v0 v1 v2 v3 v88) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v54 v70) _ -> MAlonzo.RTE.mazUnreachableError))))) @@ -2085,7 +2085,7 @@ d_isFD'63'_184 v0 v1 v2 v3 v24) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v15 v3) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -2228,7 +2228,7 @@ d_isFD'63'_184 v0 v1 v2 v3 seq (coe v14) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 - MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_30 + MAlonzo.Code.VerifiedCompilation.Trace.d_ForceDelayT_32 v2 v3) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError)) @@ -2255,7 +2255,7 @@ d_'46'extendedlambda2_246 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 d_'46'extendedlambda2_246 = erased @@ -2273,7 +2273,7 @@ d_'46'extendedlambda3_320 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_270 -> @@ -2292,7 +2292,7 @@ d_'46'extendedlambda4_348 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2322,7 +2322,7 @@ d_'46'extendedlambda6_476 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2334,7 +2334,7 @@ d_'46'extendedlambda6_476 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 d_'46'extendedlambda6_476 = erased @@ -2354,7 +2354,7 @@ d_'46'extendedlambda7_518 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 d_'46'extendedlambda7_518 = erased @@ -2381,7 +2381,7 @@ d_'46'extendedlambda8_634 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2410,7 +2410,7 @@ d_'46'extendedlambda9_688 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2434,7 +2434,7 @@ d_'46'extendedlambda10_750 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2446,7 +2446,7 @@ d_'46'extendedlambda10_750 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2470,7 +2470,7 @@ d_'46'extendedlambda11_814 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2481,7 +2481,7 @@ d_'46'extendedlambda11_814 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2506,7 +2506,7 @@ d_'46'extendedlambda12_880 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Builtin.T_Builtin_2 -> @@ -2516,7 +2516,7 @@ d_'46'extendedlambda12_880 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2546,7 +2546,7 @@ d_'46'extendedlambda13_1034 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2567,7 +2567,7 @@ d_'46'extendedlambda14_1074 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> @@ -2584,7 +2584,7 @@ d_'46'extendedlambda15_1190 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> @@ -2592,7 +2592,7 @@ d_'46'extendedlambda15_1190 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> @@ -2610,7 +2610,7 @@ d_'46'extendedlambda16_1214 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> @@ -2629,7 +2629,7 @@ d_'46'extendedlambda17_1238 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> @@ -2661,7 +2661,7 @@ d_'46'extendedlambda19_1340 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isDelay_356 -> @@ -2681,7 +2681,7 @@ d_'46'extendedlambda20_1454 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> @@ -2689,7 +2689,7 @@ d_'46'extendedlambda20_1454 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2706,7 +2706,7 @@ d_'46'extendedlambda21_1480 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2724,7 +2724,7 @@ d_'46'extendedlambda22_1506 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2742,7 +2742,7 @@ d_'46'extendedlambda23_1574 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> @@ -2780,7 +2780,7 @@ d_'46'extendedlambda25_1698 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_270 -> @@ -2803,7 +2803,7 @@ d_'46'extendedlambda26_1732 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UInline.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UInline.hs index c440a9ca48d..0849ffcea40 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UInline.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UInline.hs @@ -297,7 +297,7 @@ d_checkPointwise_304 :: Integer -> T__'8605'_28 -> T__'8605'_28 -> - [MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46] -> + [MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50] -> (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> MAlonzo.Code.Untyped.T__'8866'_14) -> T__'8829'__102 -> @@ -308,7 +308,7 @@ d_checkPointwise_304 v0 v1 v2 v3 v4 v5 v6 v7 = let v8 = coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_78 - MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34 v6 v7 in + MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36 v6 v7 in coe (case coe v3 of [] @@ -358,19 +358,19 @@ d_check_316 :: MAlonzo.Code.Untyped.T__'8866'_14) -> MAlonzo.Code.Untyped.T__'8866'_14 -> T__'8829'__102 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.VerifiedCompilation.Certificate.T_Proof'63'_66 d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 = let v8 = coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_78 - MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34 v4 v7 in + MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36 v4 v7 in coe (case coe v4 of MAlonzo.Code.Untyped.C_'96'_18 v9 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_var_48 + MAlonzo.Code.VerifiedCompilation.Trace.C_var_52 -> case coe v7 of MAlonzo.Code.Untyped.C_'96'_18 v10 -> let v11 @@ -385,7 +385,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 -> let v15 = coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_78 - MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34 + MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36 v4 v7 in coe (case coe v13 of @@ -418,7 +418,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_78 - MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34 + MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36 v4 v4 _ -> MAlonzo.RTE.mazUnreachableError) _ -> coe v15 @@ -428,7 +428,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 _ -> coe v15) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> coe v8 - MAlonzo.Code.VerifiedCompilation.Trace.C_expand_50 v10 + MAlonzo.Code.VerifiedCompilation.Trace.C_expand_54 v10 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du__'62''62''61'__88 (coe @@ -444,7 +444,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 -> case coe v5 of C_'9633'_106 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_ƛ_52 v10 + MAlonzo.Code.VerifiedCompilation.Trace.C_ƛ_56 v10 -> case coe v7 of MAlonzo.Code.Untyped.C_ƛ_20 v11 -> coe @@ -469,7 +469,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 -> case coe v2 of C__'183'__34 v16 v17 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_ƛ_52 v18 + MAlonzo.Code.VerifiedCompilation.Trace.C_ƛ_56 v18 -> case coe v7 of MAlonzo.Code.Untyped.C_ƛ_20 v19 -> coe @@ -537,7 +537,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 _ -> MAlonzo.RTE.mazUnreachableError MAlonzo.Code.Untyped.C__'183'__22 v9 v10 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C__'183'__54 v11 v12 + MAlonzo.Code.VerifiedCompilation.Trace.C__'183'__58 v11 v12 -> case coe v7 of MAlonzo.Code.Untyped.C__'183'__22 v13 v14 -> coe @@ -559,7 +559,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_72 (coe C__'183'__250 v15 v16))))) _ -> coe v8 - MAlonzo.Code.VerifiedCompilation.Trace.C__'183''8595'_56 v11 + MAlonzo.Code.VerifiedCompilation.Trace.C__'183''8595'_60 v11 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du__'62''62''61'__88 (coe @@ -574,7 +574,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 _ -> coe v8 MAlonzo.Code.Untyped.C_force_24 v9 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_force_58 v10 + MAlonzo.Code.VerifiedCompilation.Trace.C_force_62 v10 -> case coe v7 of MAlonzo.Code.Untyped.C_force_24 v11 -> coe @@ -591,7 +591,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 _ -> coe v8 MAlonzo.Code.Untyped.C_delay_26 v9 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_delay_60 v10 + MAlonzo.Code.VerifiedCompilation.Trace.C_delay_64 v10 -> case coe v7 of MAlonzo.Code.Untyped.C_delay_26 v11 -> coe @@ -608,7 +608,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 _ -> coe v8 MAlonzo.Code.Untyped.C_con_28 v9 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_con_62 + MAlonzo.Code.VerifiedCompilation.Trace.C_con_66 -> case coe v7 of MAlonzo.Code.Untyped.C_con_28 v10 -> let v11 @@ -627,14 +627,14 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 seq (coe v13) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_78 - MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34 + MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36 v4 v7) _ -> MAlonzo.RTE.mazUnreachableError) _ -> coe v8 _ -> coe v8 MAlonzo.Code.Untyped.C_constr_34 v9 v10 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_constr_68 v11 + MAlonzo.Code.VerifiedCompilation.Trace.C_constr_72 v11 -> case coe v7 of MAlonzo.Code.Untyped.C_constr_34 v12 v13 -> let v14 @@ -669,14 +669,14 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 seq (coe v16) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_78 - MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34 + MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36 v4 v7) _ -> MAlonzo.RTE.mazUnreachableError) _ -> coe v8 _ -> coe v8 MAlonzo.Code.Untyped.C_case_40 v9 v10 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_case_70 v11 v12 + MAlonzo.Code.VerifiedCompilation.Trace.C_case_74 v11 v12 -> case coe v7 of MAlonzo.Code.Untyped.C_case_40 v13 v14 -> coe @@ -701,7 +701,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 _ -> coe v8 MAlonzo.Code.Untyped.C_builtin_44 v9 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_builtin_64 + MAlonzo.Code.VerifiedCompilation.Trace.C_builtin_68 -> case coe v7 of MAlonzo.Code.Untyped.C_builtin_44 v10 -> let v11 @@ -752,7 +752,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 seq (coe v16) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_78 - MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34 + MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36 v4 v7) _ -> MAlonzo.RTE.mazUnreachableError) else (let v14 @@ -776,7 +776,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 seq (coe v16) (coe MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_78 - MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_34 + MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_36 v4 v7) _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError) @@ -784,7 +784,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 _ -> coe v8 MAlonzo.Code.Untyped.C_error_46 -> case coe v6 of - MAlonzo.Code.VerifiedCompilation.Trace.C_error_66 + MAlonzo.Code.VerifiedCompilation.Trace.C_error_70 -> case coe v7 of MAlonzo.Code.Untyped.C_error_46 -> coe @@ -795,7 +795,7 @@ d_check_316 v0 v1 v2 v3 v4 v5 v6 v7 _ -> MAlonzo.RTE.mazUnreachableError) -- VerifiedCompilation.UInline.top-check d_top'45'check_718 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.VerifiedCompilation.Certificate.T_Proof'63'_66 @@ -885,7 +885,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 C_'96'_230 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 - (coe MAlonzo.Code.VerifiedCompilation.Trace.C_var_48) erased + (coe MAlonzo.Code.VerifiedCompilation.Trace.C_var_52) erased C_'96''8595'_234 v14 -> case coe v5 of MAlonzo.Code.Untyped.C_'96'_18 v15 @@ -898,7 +898,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v17 v18 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 - (coe MAlonzo.Code.VerifiedCompilation.Trace.C_expand_50 (coe v17)) + (coe MAlonzo.Code.VerifiedCompilation.Trace.C_expand_54 (coe v17)) erased _ -> MAlonzo.RTE.mazUnreachableError) _ -> MAlonzo.RTE.mazUnreachableError @@ -923,7 +923,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C_ƛ_52 (coe v15)) + MAlonzo.Code.VerifiedCompilation.Trace.C_ƛ_56 (coe v15)) erased _ -> MAlonzo.RTE.mazUnreachableError)) _ -> MAlonzo.RTE.mazUnreachableError @@ -962,7 +962,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C_ƛ_52 + MAlonzo.Code.VerifiedCompilation.Trace.C_ƛ_56 (coe v27)) erased _ -> MAlonzo.RTE.mazUnreachableError) @@ -1027,7 +1027,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C__'183'__54 + MAlonzo.Code.VerifiedCompilation.Trace.C__'183'__58 (coe v24) (coe v26)) erased _ -> MAlonzo.RTE.mazUnreachableError @@ -1048,7 +1048,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C__'183''8595'_56 (coe v19)) + MAlonzo.Code.VerifiedCompilation.Trace.C__'183''8595'_60 (coe v19)) erased _ -> MAlonzo.RTE.mazUnreachableError) _ -> MAlonzo.RTE.mazUnreachableError @@ -1067,7 +1067,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C_force_58 (coe v18)) + MAlonzo.Code.VerifiedCompilation.Trace.C_force_62 (coe v18)) erased _ -> MAlonzo.RTE.mazUnreachableError) _ -> MAlonzo.RTE.mazUnreachableError @@ -1087,7 +1087,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C_delay_60 (coe v18)) + MAlonzo.Code.VerifiedCompilation.Trace.C_delay_64 (coe v18)) erased _ -> MAlonzo.RTE.mazUnreachableError) _ -> MAlonzo.RTE.mazUnreachableError @@ -1095,11 +1095,11 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 C_con_266 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 - (coe MAlonzo.Code.VerifiedCompilation.Trace.C_con_62) erased + (coe MAlonzo.Code.VerifiedCompilation.Trace.C_con_66) erased C_builtin_270 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 - (coe MAlonzo.Code.VerifiedCompilation.Trace.C_builtin_64) erased + (coe MAlonzo.Code.VerifiedCompilation.Trace.C_builtin_68) erased C_constr_280 v15 -> case coe v5 of MAlonzo.Code.Untyped.C_constr_34 v16 v17 @@ -1115,7 +1115,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C_constr_68 + MAlonzo.Code.VerifiedCompilation.Trace.C_constr_72 (coe v21)) erased _ -> MAlonzo.RTE.mazUnreachableError) @@ -1143,7 +1143,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe - MAlonzo.Code.VerifiedCompilation.Trace.C_case_70 + MAlonzo.Code.VerifiedCompilation.Trace.C_case_74 (coe v24) (coe v26)) erased _ -> MAlonzo.RTE.mazUnreachableError @@ -1157,7 +1157,7 @@ d_complete_806 v0 v1 v2 v3 v4 v5 v6 v7 seq (coe v6) (coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 - (coe MAlonzo.Code.VerifiedCompilation.Trace.C_error_66) erased)) + (coe MAlonzo.Code.VerifiedCompilation.Trace.C_error_70) erased)) _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.UInline._.e′ d_e'8242'_818 :: @@ -1179,7 +1179,7 @@ d_e'8242'_864 :: MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> MAlonzo.Code.Untyped.T__'8866'_14 -> T_Inline_224 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 d_e'8242'_864 = erased @@ -1191,7 +1191,7 @@ d_e'8242'_898 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> T_Inline_224 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 d_e'8242'_898 = erased @@ -1207,7 +1207,7 @@ d_e'8242'_940 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> T_Inline_224 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 d_e'8242'_940 = erased @@ -1223,7 +1223,7 @@ d_e'8242'_982 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> T_Inline_224 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 d_e'8242'_982 = erased @@ -1241,9 +1241,9 @@ d_e'8243'_1036 :: MAlonzo.Code.Untyped.T__'8866'_14 -> T_Inline_224 -> T_Inline_224 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 d_e'8243'_1036 = erased @@ -1259,7 +1259,7 @@ d_e'8242'_1082 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> T_Inline_224 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 d_e'8242'_1082 = erased @@ -1271,7 +1271,7 @@ d_e'8242'_1120 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> T_Inline_224 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> T__'8605'_28 -> T__'8605'_28 -> @@ -1285,7 +1285,7 @@ d_e'8242'_1158 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> T_Inline_224 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> T__'8605'_28 -> T__'8605'_28 -> @@ -1321,7 +1321,7 @@ d_e'8242'_1232 :: [MAlonzo.Code.Untyped.T__'8866'_14] -> [MAlonzo.Code.Untyped.T__'8866'_14] -> MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 -> - [MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46] -> + [MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> T__'8605'_28 -> T__'8605'_28 -> @@ -1339,9 +1339,9 @@ d_e'8243'_1290 :: [MAlonzo.Code.Untyped.T__'8866'_14] -> T_Inline_224 -> MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> - [MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46] -> + [MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> T__'8605'_28 -> T__'8605'_28 -> @@ -1361,9 +1361,9 @@ d_e'8243'_1356 :: [MAlonzo.Code.Untyped.T__'8866'_14] -> T_Inline_224 -> MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> - [MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_46] -> + [MAlonzo.Code.VerifiedCompilation.Trace.T_InlineHints_50] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 d_e'8243'_1356 = erased diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedTranslation.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedTranslation.hs index 5dba94f347e..fedeaa818c9 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedTranslation.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedTranslation.hs @@ -84,7 +84,7 @@ d_translation'63'_160 :: MAlonzo.Code.Untyped.T__'8866'_14 -> ()) -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -98,7 +98,7 @@ du_translation'63'_160 :: Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2924,7 +2924,7 @@ d_decPointwiseTranslation'63'_172 :: MAlonzo.Code.Untyped.T__'8866'_14 -> ()) -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2938,7 +2938,7 @@ du_decPointwiseTranslation'63'_172 :: Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_8 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> diff --git a/plutus-metatheory/src/VerifiedCompilation/Trace.lagda.md b/plutus-metatheory/src/VerifiedCompilation/Trace.lagda.md index ee791264791..9bc150a4cf9 100644 --- a/plutus-metatheory/src/VerifiedCompilation/Trace.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/Trace.lagda.md @@ -31,6 +31,7 @@ pragmas MUST be the same as the order of their counterparts in data UncertifiedOptTag : Set where caseOfCaseT : UncertifiedOptTag + constantFoldingT : UncertifiedOptTag data CertifiedOptTag : Set where floatDelayT : CertifiedOptTag @@ -56,14 +57,16 @@ CseT : OptTag CseT = Utils.inj₂ cseT ApplyToCaseT : OptTag ApplyToCaseT = Utils.inj₂ applyToCaseT - -CaseOfCaseT : OptTag -CaseOfCaseT = Utils.inj₁ caseOfCaseT LetFloatOutT : OptTag LetFloatOutT = Utils.inj₂ letFloatOutT CaseReduceT : OptTag CaseReduceT = Utils.inj₂ caseReduceT +CaseOfCaseT : OptTag +CaseOfCaseT = Utils.inj₁ caseOfCaseT +ConstantFoldingT : OptTag +ConstantFoldingT = Utils.inj₁ constantFoldingT + {-# COMPILE GHC CertifiedOptTag = data CertifiedOptStage @@ -81,6 +84,7 @@ CaseReduceT = Utils.inj₂ caseReduceT UncertifiedOptTag = data UncertifiedOptStage ( CaseOfCase + | ConstantFolding ) #-} ``` diff --git a/plutus-metatheory/test/certifier-report/golden/n-queens.golden.report b/plutus-metatheory/test/certifier-report/golden/n-queens.golden.report index 7f80510bc07..3c11573026e 100644 --- a/plutus-metatheory/test/certifier-report/golden/n-queens.golden.report +++ b/plutus-metatheory/test/certifier-report/golden/n-queens.golden.report @@ -64,7 +64,16 @@ Pass 7: Inlining ✅ Optimization sites: 216 ────────────────────────────────────────────────────── -Pass 8: Float Delay ✅ +Pass 8: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 3117 (before) + Program Size: 3117 (after) + Execution Cost: CPU = 264858581782, MEM = 1605309055 (before) + Execution Cost: CPU = 264858581782, MEM = 1605309055 (after) + + +────────────────────────────────────────────────────── +Pass 9: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 3117 (before) Program Size: 3170 (after) @@ -73,7 +82,7 @@ Pass 8: Float Delay ✅ Optimization sites: 1 ────────────────────────────────────────────────────── -Pass 9: Float Force into Case Branches ✅ +Pass 10: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 3170 (before) Program Size: 3170 (after) @@ -82,7 +91,7 @@ Pass 9: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 10: Float bindings outwards ✅ +Pass 11: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 3170 (before) Program Size: 3170 (after) @@ -91,7 +100,7 @@ Pass 10: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 11: Force-Delay Cancellation ✅ +Pass 12: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 3170 (before) Program Size: 2910 (after) @@ -100,7 +109,7 @@ Pass 11: Force-Delay Cancellation ✅ Optimization sites: 112 ────────────────────────────────────────────────────── -Pass 12: Case-of-Case ⚠ (certifier unavailable) +Pass 13: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 2910 (before) Program Size: 2910 (after) @@ -109,7 +118,7 @@ Pass 12: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 13: Case-Constr and Case-Constant Cancellation ✅ +Pass 14: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 2910 (before) Program Size: 2910 (after) @@ -118,7 +127,7 @@ Pass 13: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 14: Inlining ✅ +Pass 15: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 2910 (before) Program Size: 2474 (after) @@ -127,7 +136,16 @@ Pass 14: Inlining ✅ Optimization sites: 225 ────────────────────────────────────────────────────── -Pass 15: Float Delay ✅ +Pass 16: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 2474 (before) + Program Size: 2474 (after) + Execution Cost: CPU = 218067557782, MEM = 1312865155 (before) + Execution Cost: CPU = 218067557782, MEM = 1312865155 (after) + + +────────────────────────────────────────────────────── +Pass 17: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 2474 (before) Program Size: 2554 (after) @@ -136,7 +154,7 @@ Pass 15: Float Delay ✅ Optimization sites: 1 ────────────────────────────────────────────────────── -Pass 16: Float Force into Case Branches ✅ +Pass 18: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 2554 (before) Program Size: 2527 (after) @@ -145,7 +163,7 @@ Pass 16: Float Force into Case Branches ✅ Optimization sites: 5 ────────────────────────────────────────────────────── -Pass 17: Float bindings outwards ✅ +Pass 19: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 2527 (before) Program Size: 2527 (after) @@ -154,7 +172,7 @@ Pass 17: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 18: Force-Delay Cancellation ✅ +Pass 20: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 2527 (before) Program Size: 2357 (after) @@ -163,7 +181,7 @@ Pass 18: Force-Delay Cancellation ✅ Optimization sites: 85 ────────────────────────────────────────────────────── -Pass 19: Case-of-Case ⚠ (certifier unavailable) +Pass 21: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 2357 (before) Program Size: 2357 (after) @@ -172,7 +190,7 @@ Pass 19: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 20: Case-Constr and Case-Constant Cancellation ✅ +Pass 22: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 2357 (before) Program Size: 2357 (after) @@ -181,7 +199,7 @@ Pass 20: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 21: Inlining ✅ +Pass 23: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 2357 (before) Program Size: 2391 (after) @@ -190,7 +208,16 @@ Pass 21: Inlining ✅ Optimization sites: 196 ────────────────────────────────────────────────────── -Pass 22: Float Delay ✅ +Pass 24: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 2391 (before) + Program Size: 2391 (after) + Execution Cost: CPU = 173477157782, MEM = 1034175155 (before) + Execution Cost: CPU = 173477157782, MEM = 1034175155 (after) + + +────────────────────────────────────────────────────── +Pass 25: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 2391 (before) Program Size: 2402 (after) @@ -199,7 +226,7 @@ Pass 22: Float Delay ✅ Optimization sites: 1 ────────────────────────────────────────────────────── -Pass 23: Float Force into Case Branches ✅ +Pass 26: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 2402 (before) Program Size: 2402 (after) @@ -208,7 +235,7 @@ Pass 23: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 24: Float bindings outwards ✅ +Pass 27: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 2402 (before) Program Size: 2402 (after) @@ -217,7 +244,7 @@ Pass 24: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 25: Force-Delay Cancellation ✅ +Pass 28: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 2402 (before) Program Size: 2266 (after) @@ -226,7 +253,7 @@ Pass 25: Force-Delay Cancellation ✅ Optimization sites: 68 ────────────────────────────────────────────────────── -Pass 26: Case-of-Case ⚠ (certifier unavailable) +Pass 29: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 2266 (before) Program Size: 2266 (after) @@ -235,7 +262,7 @@ Pass 26: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 27: Case-Constr and Case-Constant Cancellation ✅ +Pass 30: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 2266 (before) Program Size: 2266 (after) @@ -244,7 +271,7 @@ Pass 27: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 28: Inlining ✅ +Pass 31: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 2266 (before) Program Size: 1948 (after) @@ -253,7 +280,16 @@ Pass 28: Inlining ✅ Optimization sites: 133 ────────────────────────────────────────────────────── -Pass 29: Float Delay ✅ +Pass 32: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1948 (before) + Program Size: 1948 (after) + Execution Cost: CPU = 125934997782, MEM = 737036655 (before) + Execution Cost: CPU = 125934997782, MEM = 737036655 (after) + + +────────────────────────────────────────────────────── +Pass 33: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1948 (before) Program Size: 1948 (after) @@ -262,7 +298,7 @@ Pass 29: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 30: Float Force into Case Branches ✅ +Pass 34: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1948 (before) Program Size: 1846 (after) @@ -271,7 +307,7 @@ Pass 30: Float Force into Case Branches ✅ Optimization sites: 28 ────────────────────────────────────────────────────── -Pass 31: Float bindings outwards ✅ +Pass 35: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1846 (before) Program Size: 1846 (after) @@ -280,7 +316,7 @@ Pass 31: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 32: Force-Delay Cancellation ✅ +Pass 36: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1846 (before) Program Size: 1820 (after) @@ -289,7 +325,7 @@ Pass 32: Force-Delay Cancellation ✅ Optimization sites: 13 ────────────────────────────────────────────────────── -Pass 33: Case-of-Case ⚠ (certifier unavailable) +Pass 37: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1820 (before) Program Size: 1820 (after) @@ -298,7 +334,7 @@ Pass 33: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 34: Case-Constr and Case-Constant Cancellation ✅ +Pass 38: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1820 (before) Program Size: 1820 (after) @@ -307,7 +343,7 @@ Pass 34: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 35: Inlining ✅ +Pass 39: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1820 (before) Program Size: 1770 (after) @@ -316,7 +352,16 @@ Pass 35: Inlining ✅ Optimization sites: 14 ────────────────────────────────────────────────────── -Pass 36: Float Delay ✅ +Pass 40: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1770 (before) + Program Size: 1770 (after) + Execution Cost: CPU = 117353973782, MEM = 683405255 (before) + Execution Cost: CPU = 117353973782, MEM = 683405255 (after) + + +────────────────────────────────────────────────────── +Pass 41: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1770 (before) Program Size: 1770 (after) @@ -325,7 +370,7 @@ Pass 36: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 37: Float Force into Case Branches ✅ +Pass 42: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1770 (before) Program Size: 1767 (after) @@ -334,7 +379,7 @@ Pass 37: Float Force into Case Branches ✅ Optimization sites: 1 ────────────────────────────────────────────────────── -Pass 38: Float bindings outwards ✅ +Pass 43: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1767 (before) Program Size: 1767 (after) @@ -343,7 +388,7 @@ Pass 38: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 39: Force-Delay Cancellation ✅ +Pass 44: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1767 (before) Program Size: 1767 (after) @@ -352,7 +397,7 @@ Pass 39: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 40: Case-of-Case ⚠ (certifier unavailable) +Pass 45: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1767 (before) Program Size: 1767 (after) @@ -361,7 +406,7 @@ Pass 40: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 41: Case-Constr and Case-Constant Cancellation ✅ +Pass 46: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1767 (before) Program Size: 1767 (after) @@ -370,7 +415,7 @@ Pass 41: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 42: Inlining ✅ +Pass 47: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1767 (before) Program Size: 1764 (after) @@ -379,7 +424,16 @@ Pass 42: Inlining ✅ Optimization sites: 1 ────────────────────────────────────────────────────── -Pass 43: Float Delay ✅ +Pass 48: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1764 (before) + Program Size: 1764 (after) + Execution Cost: CPU = 117353973782, MEM = 683405255 (before) + Execution Cost: CPU = 117353973782, MEM = 683405255 (after) + + +────────────────────────────────────────────────────── +Pass 49: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -388,7 +442,7 @@ Pass 43: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 44: Float Force into Case Branches ✅ +Pass 50: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -397,7 +451,7 @@ Pass 44: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 45: Float bindings outwards ✅ +Pass 51: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -406,7 +460,7 @@ Pass 45: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 46: Force-Delay Cancellation ✅ +Pass 52: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -415,7 +469,7 @@ Pass 46: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 47: Case-of-Case ⚠ (certifier unavailable) +Pass 53: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -424,7 +478,7 @@ Pass 47: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 48: Case-Constr and Case-Constant Cancellation ✅ +Pass 54: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -433,7 +487,7 @@ Pass 48: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 49: Inlining ✅ +Pass 55: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -442,7 +496,16 @@ Pass 49: Inlining ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 50: Float Delay ✅ +Pass 56: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1764 (before) + Program Size: 1764 (after) + Execution Cost: CPU = 117353973782, MEM = 683405255 (before) + Execution Cost: CPU = 117353973782, MEM = 683405255 (after) + + +────────────────────────────────────────────────────── +Pass 57: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -451,7 +514,7 @@ Pass 50: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 51: Float Force into Case Branches ✅ +Pass 58: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -460,7 +523,7 @@ Pass 51: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 52: Float bindings outwards ✅ +Pass 59: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -469,7 +532,7 @@ Pass 52: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 53: Force-Delay Cancellation ✅ +Pass 60: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -478,7 +541,7 @@ Pass 53: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 54: Case-of-Case ⚠ (certifier unavailable) +Pass 61: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -487,7 +550,7 @@ Pass 54: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 55: Case-Constr and Case-Constant Cancellation ✅ +Pass 62: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -496,7 +559,7 @@ Pass 55: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 56: Inlining ✅ +Pass 63: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -505,7 +568,16 @@ Pass 56: Inlining ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 57: Float Delay ✅ +Pass 64: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1764 (before) + Program Size: 1764 (after) + Execution Cost: CPU = 117353973782, MEM = 683405255 (before) + Execution Cost: CPU = 117353973782, MEM = 683405255 (after) + + +────────────────────────────────────────────────────── +Pass 65: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -514,7 +586,7 @@ Pass 57: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 58: Float Force into Case Branches ✅ +Pass 66: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -523,7 +595,7 @@ Pass 58: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 59: Float bindings outwards ✅ +Pass 67: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -532,7 +604,7 @@ Pass 59: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 60: Force-Delay Cancellation ✅ +Pass 68: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -541,7 +613,7 @@ Pass 60: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 61: Case-of-Case ⚠ (certifier unavailable) +Pass 69: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -550,7 +622,7 @@ Pass 61: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 62: Case-Constr and Case-Constant Cancellation ✅ +Pass 70: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -559,7 +631,7 @@ Pass 62: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 63: Inlining ✅ +Pass 71: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -568,7 +640,16 @@ Pass 63: Inlining ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 64: Float Delay ✅ +Pass 72: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1764 (before) + Program Size: 1764 (after) + Execution Cost: CPU = 117353973782, MEM = 683405255 (before) + Execution Cost: CPU = 117353973782, MEM = 683405255 (after) + + +────────────────────────────────────────────────────── +Pass 73: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -577,7 +658,7 @@ Pass 64: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 65: Float Force into Case Branches ✅ +Pass 74: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -586,7 +667,7 @@ Pass 65: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 66: Float bindings outwards ✅ +Pass 75: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -595,7 +676,7 @@ Pass 66: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 67: Force-Delay Cancellation ✅ +Pass 76: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -604,7 +685,7 @@ Pass 67: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 68: Case-of-Case ⚠ (certifier unavailable) +Pass 77: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -613,7 +694,7 @@ Pass 68: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 69: Case-Constr and Case-Constant Cancellation ✅ +Pass 78: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -622,7 +703,7 @@ Pass 69: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 70: Inlining ✅ +Pass 79: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -631,7 +712,16 @@ Pass 70: Inlining ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 71: Float Delay ✅ +Pass 80: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1764 (before) + Program Size: 1764 (after) + Execution Cost: CPU = 117353973782, MEM = 683405255 (before) + Execution Cost: CPU = 117353973782, MEM = 683405255 (after) + + +────────────────────────────────────────────────────── +Pass 81: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -640,7 +730,7 @@ Pass 71: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 72: Float Force into Case Branches ✅ +Pass 82: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -649,7 +739,7 @@ Pass 72: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 73: Float bindings outwards ✅ +Pass 83: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -658,7 +748,7 @@ Pass 73: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 74: Force-Delay Cancellation ✅ +Pass 84: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -667,7 +757,7 @@ Pass 74: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 75: Case-of-Case ⚠ (certifier unavailable) +Pass 85: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -676,7 +766,7 @@ Pass 75: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 76: Case-Constr and Case-Constant Cancellation ✅ +Pass 86: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -685,7 +775,7 @@ Pass 76: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 77: Inlining ✅ +Pass 87: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -694,7 +784,16 @@ Pass 77: Inlining ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 78: Float Delay ✅ +Pass 88: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1764 (before) + Program Size: 1764 (after) + Execution Cost: CPU = 117353973782, MEM = 683405255 (before) + Execution Cost: CPU = 117353973782, MEM = 683405255 (after) + + +────────────────────────────────────────────────────── +Pass 89: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -703,7 +802,7 @@ Pass 78: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 79: Float Force into Case Branches ✅ +Pass 90: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -712,7 +811,7 @@ Pass 79: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 80: Float bindings outwards ✅ +Pass 91: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -721,7 +820,7 @@ Pass 80: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 81: Force-Delay Cancellation ✅ +Pass 92: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -730,7 +829,7 @@ Pass 81: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 82: Case-of-Case ⚠ (certifier unavailable) +Pass 93: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -739,7 +838,7 @@ Pass 82: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 83: Case-Constr and Case-Constant Cancellation ✅ +Pass 94: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -748,7 +847,7 @@ Pass 83: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 84: Inlining ✅ +Pass 95: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1764 (after) @@ -757,7 +856,16 @@ Pass 84: Inlining ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 85: Common Subexpression Elimination ✅ +Pass 96: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1764 (before) + Program Size: 1764 (after) + Execution Cost: CPU = 117353973782, MEM = 683405255 (before) + Execution Cost: CPU = 117353973782, MEM = 683405255 (after) + + +────────────────────────────────────────────────────── +Pass 97: Common Subexpression Elimination ✅ ────────────────────────────────────────────────────── Program Size: 1764 (before) Program Size: 1773 (after) @@ -766,7 +874,7 @@ Pass 85: Common Subexpression Elimination ✅ Optimization sites: 4 ────────────────────────────────────────────────────── -Pass 86: Float Delay ✅ +Pass 98: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1773 (before) Program Size: 1773 (after) @@ -775,7 +883,7 @@ Pass 86: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 87: Float Force into Case Branches ✅ +Pass 99: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1773 (before) Program Size: 1773 (after) @@ -784,7 +892,7 @@ Pass 87: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 88: Float bindings outwards ✅ +Pass 100: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1773 (before) Program Size: 1773 (after) @@ -793,7 +901,7 @@ Pass 88: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 89: Force-Delay Cancellation ✅ +Pass 101: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1773 (before) Program Size: 1773 (after) @@ -802,7 +910,7 @@ Pass 89: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 90: Case-of-Case ⚠ (certifier unavailable) +Pass 102: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1773 (before) Program Size: 1773 (after) @@ -811,7 +919,7 @@ Pass 90: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 91: Case-Constr and Case-Constant Cancellation ✅ +Pass 103: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1773 (before) Program Size: 1773 (after) @@ -820,7 +928,7 @@ Pass 91: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 92: Inlining ✅ +Pass 104: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1773 (before) Program Size: 1774 (after) @@ -829,7 +937,16 @@ Pass 92: Inlining ✅ Optimization sites: 5 ────────────────────────────────────────────────────── -Pass 93: Common Subexpression Elimination ✅ +Pass 105: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1774 (before) + Program Size: 1774 (after) + Execution Cost: CPU = 117353829782, MEM = 683404355 (before) + Execution Cost: CPU = 117353829782, MEM = 683404355 (after) + + +────────────────────────────────────────────────────── +Pass 106: Common Subexpression Elimination ✅ ────────────────────────────────────────────────────── Program Size: 1774 (before) Program Size: 1774 (after) @@ -838,7 +955,7 @@ Pass 93: Common Subexpression Elimination ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 94: Float Delay ✅ +Pass 107: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1774 (before) Program Size: 1774 (after) @@ -847,7 +964,7 @@ Pass 94: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 95: Float Force into Case Branches ✅ +Pass 108: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1774 (before) Program Size: 1774 (after) @@ -856,7 +973,7 @@ Pass 95: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 96: Float bindings outwards ✅ +Pass 109: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1774 (before) Program Size: 1774 (after) @@ -865,7 +982,7 @@ Pass 96: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 97: Force-Delay Cancellation ✅ +Pass 110: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1774 (before) Program Size: 1770 (after) @@ -874,7 +991,7 @@ Pass 97: Force-Delay Cancellation ✅ Optimization sites: 2 ────────────────────────────────────────────────────── -Pass 98: Case-of-Case ⚠ (certifier unavailable) +Pass 111: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1770 (before) Program Size: 1770 (after) @@ -883,7 +1000,7 @@ Pass 98: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 99: Case-Constr and Case-Constant Cancellation ✅ +Pass 112: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1770 (before) Program Size: 1770 (after) @@ -892,7 +1009,7 @@ Pass 99: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 100: Inlining ✅ +Pass 113: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1770 (before) Program Size: 1756 (after) @@ -901,7 +1018,16 @@ Pass 100: Inlining ✅ Optimization sites: 2 ────────────────────────────────────────────────────── -Pass 101: Common Subexpression Elimination ✅ +Pass 114: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1756 (before) + Program Size: 1756 (after) + Execution Cost: CPU = 117353781782, MEM = 683404055 (before) + Execution Cost: CPU = 117353781782, MEM = 683404055 (after) + + +────────────────────────────────────────────────────── +Pass 115: Common Subexpression Elimination ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -910,7 +1036,7 @@ Pass 101: Common Subexpression Elimination ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 102: Float Delay ✅ +Pass 116: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -919,7 +1045,7 @@ Pass 102: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 103: Float Force into Case Branches ✅ +Pass 117: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -928,7 +1054,7 @@ Pass 103: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 104: Float bindings outwards ✅ +Pass 118: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -937,7 +1063,7 @@ Pass 104: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 105: Force-Delay Cancellation ✅ +Pass 119: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -946,7 +1072,7 @@ Pass 105: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 106: Case-of-Case ⚠ (certifier unavailable) +Pass 120: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -955,7 +1081,7 @@ Pass 106: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 107: Case-Constr and Case-Constant Cancellation ✅ +Pass 121: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -964,7 +1090,7 @@ Pass 107: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 108: Inlining ✅ +Pass 122: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -973,7 +1099,16 @@ Pass 108: Inlining ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 109: Common Subexpression Elimination ✅ +Pass 123: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1756 (before) + Program Size: 1756 (after) + Execution Cost: CPU = 117353781782, MEM = 683404055 (before) + Execution Cost: CPU = 117353781782, MEM = 683404055 (after) + + +────────────────────────────────────────────────────── +Pass 124: Common Subexpression Elimination ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -982,7 +1117,7 @@ Pass 109: Common Subexpression Elimination ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 110: Float Delay ✅ +Pass 125: Float Delay ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -991,7 +1126,7 @@ Pass 110: Float Delay ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 111: Float Force into Case Branches ✅ +Pass 126: Float Force into Case Branches ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -1000,7 +1135,7 @@ Pass 111: Float Force into Case Branches ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 112: Float bindings outwards ✅ +Pass 127: Float bindings outwards ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -1009,7 +1144,7 @@ Pass 112: Float bindings outwards ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 113: Force-Delay Cancellation ✅ +Pass 128: Force-Delay Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -1018,7 +1153,7 @@ Pass 113: Force-Delay Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 114: Case-of-Case ⚠ (certifier unavailable) +Pass 129: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -1027,7 +1162,7 @@ Pass 114: Case-of-Case ⚠ (certifier unavailable) ────────────────────────────────────────────────────── -Pass 115: Case-Constr and Case-Constant Cancellation ✅ +Pass 130: Case-Constr and Case-Constant Cancellation ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -1036,7 +1171,7 @@ Pass 115: Case-Constr and Case-Constant Cancellation ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 116: Inlining ✅ +Pass 131: Inlining ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1756 (after) @@ -1045,7 +1180,16 @@ Pass 116: Inlining ✅ Optimization sites: 0 ────────────────────────────────────────────────────── -Pass 117: Transform multi-argument applications into case-constr form ✅ +Pass 132: Constant Folding ⚠ (certifier unavailable) +────────────────────────────────────────────────────── + Program Size: 1756 (before) + Program Size: 1756 (after) + Execution Cost: CPU = 117353781782, MEM = 683404055 (before) + Execution Cost: CPU = 117353781782, MEM = 683404055 (after) + + +────────────────────────────────────────────────────── +Pass 133: Transform multi-argument applications into case-constr form ✅ ────────────────────────────────────────────────────── Program Size: 1756 (before) Program Size: 1738 (after) diff --git a/plutus-tx-plugin/test/Budget/9.6/applicative.golden.eval b/plutus-tx-plugin/test/Budget/9.6/applicative.golden.eval index 09f9aa88b5d..0cb4877735b 100644 --- a/plutus-tx-plugin/test/Budget/9.6/applicative.golden.eval +++ b/plutus-tx-plugin/test/Budget/9.6/applicative.golden.eval @@ -1,6 +1,6 @@ -CPU: 197_308 -Memory: 702 -AST Size: 6 -Flat Size: 13 +CPU: 32_100 +Memory: 300 +AST Size: 2 +Flat Size: 9 (constr 0 (con integer 3)) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/9.6/applicative.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/applicative.golden.uplc index 1efbfc301cc..2636cbd763d 100644 --- a/plutus-tx-plugin/test/Budget/9.6/applicative.golden.uplc +++ b/plutus-tx-plugin/test/Budget/9.6/applicative.golden.uplc @@ -1 +1 @@ -(program 1.1.0 (constr 0 [(addInteger 1 2)])) \ No newline at end of file +(program 1.1.0 (constr 0 [3])) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/9.6/monadicDo.golden.eval b/plutus-tx-plugin/test/Budget/9.6/monadicDo.golden.eval index 09f9aa88b5d..0cb4877735b 100644 --- a/plutus-tx-plugin/test/Budget/9.6/monadicDo.golden.eval +++ b/plutus-tx-plugin/test/Budget/9.6/monadicDo.golden.eval @@ -1,6 +1,6 @@ -CPU: 197_308 -Memory: 702 -AST Size: 6 -Flat Size: 13 +CPU: 32_100 +Memory: 300 +AST Size: 2 +Flat Size: 9 (constr 0 (con integer 3)) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/9.6/monadicDo.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/monadicDo.golden.uplc index 1efbfc301cc..2636cbd763d 100644 --- a/plutus-tx-plugin/test/Budget/9.6/monadicDo.golden.uplc +++ b/plutus-tx-plugin/test/Budget/9.6/monadicDo.golden.uplc @@ -1 +1 @@ -(program 1.1.0 (constr 0 [(addInteger 1 2)])) \ No newline at end of file +(program 1.1.0 (constr 0 [3])) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/9.6/toFromData.golden.eval b/plutus-tx-plugin/test/Budget/9.6/toFromData.golden.eval index 7a5f806f08e..5ae2964777a 100644 --- a/plutus-tx-plugin/test/Budget/9.6/toFromData.golden.eval +++ b/plutus-tx-plugin/test/Budget/9.6/toFromData.golden.eval @@ -1,7 +1,7 @@ -CPU: 3_182_422 -Memory: 13_404 -AST Size: 140 -Flat Size: 153 +CPU: 96_100 +Memory: 700 +AST Size: 6 +Flat Size: 15 (constr 1 (constr 0 (constr 0 (con bool True) (con integer 1) (con bool False))) diff --git a/plutus-tx-plugin/test/Budget/9.6/toFromData.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/toFromData.golden.uplc index 6365cded13b..908c3374348 100644 --- a/plutus-tx-plugin/test/Budget/9.6/toFromData.golden.uplc +++ b/plutus-tx-plugin/test/Budget/9.6/toFromData.golden.uplc @@ -1,82 +1 @@ -(program - 1.1.0 - (case - (unConstrData - (constrData - 1 - (force mkCons - (constrData - 0 - (force mkCons - (constrData - 0 - (force mkCons - (Constr 1 []) - (force mkCons - (iData 1) - (force mkCons (Constr 0 []) [])))) - [])) - []))) - [ (\index - args -> - case - index - [ (\ds -> constr 0 [(unIData (force headList ds))]) - , (\ds -> - constr 1 - [ (case - (unConstrData (force headList ds)) - [ (\index - args -> - case - index - [ (\ds -> - constr 0 - [ (case - (unConstrData (force headList ds)) - [ (\index - args -> - case - index - [ (\ds -> - (\l -> - constr 0 - [ (case - (unConstrData - (force - headList - ds)) - [ (\index - args -> - case - index - [ (\ds -> - False) - , (\ds -> - True) ] - args) ]) - , (unIData - (force - headList - l)) - , (case - (unConstrData - (force - headList - (force - tailList - l))) - [ (\index - args -> - case - index - [ (\ds -> - False) - , (\ds -> - True) ] - args) ]) ]) - (force tailList ds)) ] - args) ]) ]) - , (\ds -> constr 1 []) ] - args) ]) ]) ] - args) ])) \ No newline at end of file +(program 1.1.0 (constr 1 [(constr 0 [(constr 0 [True, 1, False])])])) \ No newline at end of file