Add decision procedure for hoist-builtins pass

Author: basetunnel

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs

@@ -28,6 +28,7 @@ data CertifiedOptStage
   | ApplyToCase
   | CaseReduce
   | LetFloatOut
+  | PolyBuiltin
   deriving stock (Show, Generic)
   deriving anyclass (NFData)
 
@@ -44,7 +45,6 @@ at https://github.com/IntersectMBO/plutus/issues. -}
 data UncertifiedOptStage
   = CaseOfCase
   | ConstantFolding
-  | PolyBuiltin
   deriving stock (Show, Generic)
   deriving anyclass (NFData)
 
@@ -81,7 +81,7 @@ pattern ConstantFoldingStage :: OptStage
 pattern ConstantFoldingStage = Left ConstantFolding
 
 pattern PolyBuiltinStage :: OptStage
-pattern PolyBuiltinStage = Left PolyBuiltin
+pattern PolyBuiltinStage = Right PolyBuiltin
 
 {-# COMPLETE
   FloatDelayStage

plutus-metatheory/src/CertifierReport.lagda.md

@@ -13,6 +13,7 @@ open import VerifiedCompilation.UntypedTranslation
 open import VerifiedCompilation.UInline
 open import VerifiedCompilation.UCaseReduce as CR
 import VerifiedCompilation.FloatOut as FloatOut
+open import VerifiedCompilation.UCSE as CSE
 open import Untyped.Relation.Binary.Modular
 open import Untyped.Relation.Binary.Core renaming (Pointwise to PW)
 open import Untyped
@@ -48,11 +49,11 @@ showCertifiedOptTag cseT = "Common Subexpression Elimination"
 showCertifiedOptTag applyToCaseT = "Transform multi-argument applications into case-constr form"
 showCertifiedOptTag caseReduceT = "Case-Constr and Case-Constant Cancellation"
 showCertifiedOptTag letFloatOutT = "Float bindings outwards"
+showCertifiedOptTag polyBuiltinT = "Hoist Polymorphic Builtins"
 
 showUncertifiedOptTag : UncertifiedOptTag → String
 showUncertifiedOptTag caseOfCaseT = "Case-of-Case"
 showUncertifiedOptTag constantFoldingT = "Constant Folding"
-showUncertifiedOptTag polyBuiltinT = "Hoist Polymorphic Builtins"
 
 showTag : OptTag → String
 showTag (inj₁ tag) = showUncertifiedOptTag tag ++ "  ⚠ (certifier unavailable)"
@@ -129,6 +130,7 @@ numSites forceCaseDelayT p = numSites′ p
 numSites applyToCaseT p = numSites′ p
 numSites {M = M} caseReduceT p = numSitesCaseReduce (CR.sound {M = M} p)
 numSites letFloatOutT p = FloatOut.numSites p
+numSites polyBuiltinT p = CSE.polyNumSites p
 
 showSites : {M N : 0 ⊢} → (tag : OptTag) → RelationOf tag M N → String
 showSites (inj₁ _) _ = ""

plutus-metatheory/src/FFI/AgdaUnparse.hs

@@ -72,11 +72,11 @@ instance AgdaUnparse CertifiedOptStage where
   agdaUnparse ApplyToCase = "applyToCaseT"
   agdaUnparse CaseReduce = "caseReduceT"
   agdaUnparse LetFloatOut = "letFloatOutT"
+  agdaUnparse PolyBuiltin = "polyBuiltinT"
 
 instance AgdaUnparse UncertifiedOptStage where
   agdaUnparse CaseOfCase = "caseOfCaseT"
   agdaUnparse ConstantFolding = "constantFoldingT"
-  agdaUnparse PolyBuiltin = "polyBuiltinT"
 
 instance AgdaUnparse Hints.Hints where
   agdaUnparse = \case

plutus-metatheory/src/MAlonzo/Code/Certifier.hs

@@ -34,7 +34,7 @@ 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_12)
+          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10)
        MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
     MAlonzo.Code.RawU.T_Untyped_208 ->
   MAlonzo.Code.Utils.T_Either_6
@@ -65,7 +65,7 @@ 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_12)
+          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10)
        MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
     MAlonzo.Code.RawU.T_Untyped_208 ->
   MAlonzo.Code.Agda.Builtin.List.T_List_10
@@ -80,7 +80,7 @@ d_runCertifierMain_10 ::
     (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_12)
+          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10)
        MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
     MAlonzo.Code.RawU.T_Untyped_208 ->
   [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122] ->
@@ -104,15 +104,15 @@ d_runCertifierMain_10 v0 v1
                           MAlonzo.Code.Utils.C__'44'__450
                           (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                           (coe
-                             MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1)))
+                             MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1)))
                 MAlonzo.Code.VerifiedCompilation.C_abort_10 v4
                   -> coe
                        MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                        (coe
                           MAlonzo.Code.Utils.C__'44'__450
                           (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                           (coe
-                             MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1)))
+                             MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1)))
                 _ -> MAlonzo.RTE.mazUnreachableError
          MAlonzo.Code.Utils.C_inj'8322'_14 v3
            -> coe
@@ -123,5 +123,5 @@ d_runCertifierMain_10 v0 v1
                       MAlonzo.Code.Utils.C__'44'__450
                       (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                       (coe
-                         MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1))))
+                         MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1))))
          _ -> MAlonzo.RTE.mazUnreachableError)