Certifier: fix the CSE translation relation and re-enable it

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

@@ -17,21 +17,22 @@ This means that these passes are formalized as part of the certifier,
 and adding a new pass constructor to this type means that it is expected
 the pass will be also certified in the same PR.
 
-IMPORTANT: the order of the constructors MUST be the same as the order
+WARNING: the order of the constructors MUST be the same as the order
 of their counterparts in 'VerifiedCompilation.Trace'. -}
 data CertifiedOptStage
   = FloatDelay
   | ForceDelay
   | ForceCaseDelay
   | Inline
+  | CSE
   | ApplyToCase
   deriving stock (Show, Generic)
   deriving anyclass (NFData)
 
 {-| Datatype which represents optimization passes which are not yet
 certified.
 
-IMPORTANT: the order of the constructors MUST be the same as the order
+WARNING: the order of the constructors MUST be the same as the order
 of their counterparts in 'VerifiedCompilation.Trace'.
 
 IMPORTANT: if you add a new pass, or modify an existing pass, without
@@ -42,7 +43,6 @@ data UncertifiedOptStage
   = CaseOfCase
   | LetFloatOut
   | CaseReduce
-  | CSE
   deriving stock (Show, Generic)
   deriving anyclass (NFData)
 
@@ -64,7 +64,7 @@ pattern InlineStage :: OptStage
 pattern InlineStage = Right Inline
 
 pattern CseStage :: OptStage
-pattern CseStage = Left CSE
+pattern CseStage = Right CSE
 
 pattern ApplyToCaseStage :: OptStage
 pattern ApplyToCaseStage = Right ApplyToCase

plutus-metatheory/changelog.d/20260427_230550_ana.pantilie95_fix_cse_certifier.md

@@ -0,0 +1,3 @@
+### Fixed
+
+- Fixed the CSE translation relation in the certifier and re-enabled it.

plutus-metatheory/plutus-metatheory.cabal

@@ -367,6 +367,7 @@ library
     MAlonzo.Code.Untyped.Purity
     MAlonzo.Code.Untyped.Reduction
     MAlonzo.Code.Untyped.RenamingSubstitution
+    MAlonzo.Code.Untyped.Strictness
     MAlonzo.Code.Utils
     MAlonzo.Code.Utils.Decidable
     MAlonzo.Code.Utils.List
@@ -377,6 +378,8 @@ library
     MAlonzo.Code.VerifiedCompilation.Trace
     MAlonzo.Code.VerifiedCompilation.UApplyToCase
     MAlonzo.Code.VerifiedCompilation.UCaseOfCase
+    MAlonzo.Code.VerifiedCompilation.UCaseReduce
+    MAlonzo.Code.VerifiedCompilation.UCSE
     MAlonzo.Code.VerifiedCompilation.UFloatDelay
     MAlonzo.Code.VerifiedCompilation.UForceCaseDelay
     MAlonzo.Code.VerifiedCompilation.UForceDelay

plutus-metatheory/src/CertifierReport.lagda.md

@@ -40,13 +40,13 @@ showCertifiedOptTag floatDelayT = "Float Delay"
 showCertifiedOptTag forceDelayT = "Force-Delay Cancellation"
 showCertifiedOptTag forceCaseDelayT = "Float Force into Case Branches"
 showCertifiedOptTag inlineT = "Inlining"
+showCertifiedOptTag cseT = "Common Subexpression Elimination"
 showCertifiedOptTag applyToCaseT = "Transform multi-argument applications into case-constr form"
 
 showUncertifiedOptTag : UncertifiedOptTag → String
 showUncertifiedOptTag caseOfCaseT = "Case-of-Case"
 showUncertifiedOptTag letFloatOutT = "Float bindings outwards"
 showUncertifiedOptTag caseReduceT = "Case-Constr and Case-Constant Cancellation"
-showUncertifiedOptTag cseT = "Common Subexpression Elimination"
 
 showTag : OptTag → String
 showTag (inj₁ tag) = showUncertifiedOptTag tag ++ "  ⚠ (certifier unavailable)"
@@ -116,6 +116,7 @@ numSitesInlineᵖʷ (x Pointwise.∷ xs) = numSitesInline x + numSitesInlineᵖ
 numSites : {M N : 0 ⊢} (tag : CertifiedOptTag) → RelationOf (inj₂ tag) M N → ℕ
 numSites forceDelayT p = numSites′ p
 numSites floatDelayT p = numSites′ p
+numSites cseT p = numSites′ p
 numSites inlineT p = numSitesInline p
 numSites forceCaseDelayT p = numSites′ p
 numSites applyToCaseT p = numSites′ p

plutus-metatheory/src/FFI/AgdaUnparse.hs

@@ -55,13 +55,13 @@ instance AgdaUnparse CertifiedOptStage where
   agdaUnparse ForceDelay = "forceDelayT"
   agdaUnparse ForceCaseDelay = "forceCaseDelayT"
   agdaUnparse Inline = "inlineT"
+  agdaUnparse CSE = "cseT"
   agdaUnparse ApplyToCase = "applyToCaseT"
 
 instance AgdaUnparse UncertifiedOptStage where
   agdaUnparse CaseOfCase = "caseOfCaseT"
   agdaUnparse LetFloatOut = "letFloatOutT"
   agdaUnparse CaseReduce = "caseReduceT"
-  agdaUnparse CSE = "cseT"
 
 instance AgdaUnparse Hints.Hints where
   agdaUnparse = \case

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

@@ -33,7 +33,7 @@ d_runCertifier_2 ::
   [MAlonzo.Code.Utils.T__'215'__428
      (MAlonzo.Code.Utils.T_Either_6
         MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
-        MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_14)
+        MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
      (MAlonzo.Code.Utils.T__'215'__428
         MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_72
         (MAlonzo.Code.Utils.T__'215'__428
@@ -77,7 +77,7 @@ runCertifierMain ::
     (MAlonzo.Code.Utils.T__'215'__428
        (MAlonzo.Code.Utils.T_Either_6
           MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
-          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_14)
+          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_72
           (MAlonzo.Code.Utils.T__'215'__428
@@ -94,7 +94,7 @@ d_runCertifierMain_12 ::
   [MAlonzo.Code.Utils.T__'215'__428
      (MAlonzo.Code.Utils.T_Either_6
         MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
-        MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_14)
+        MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
      (MAlonzo.Code.Utils.T__'215'__428
         MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_72
         (MAlonzo.Code.Utils.T__'215'__428
@@ -121,15 +121,15 @@ d_runCertifierMain_12 v0 v1
                           MAlonzo.Code.Utils.C__'44'__442
                           (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                           (coe
-                             MAlonzo.Code.CertifierReport.d_makeReport_282 (coe v2) (coe v1)))
+                             MAlonzo.Code.CertifierReport.d_makeReport_284 (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'__442
                           (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                           (coe
-                             MAlonzo.Code.CertifierReport.d_makeReport_282 (coe v2) (coe v1)))
+                             MAlonzo.Code.CertifierReport.d_makeReport_284 (coe v2) (coe v1)))
                 _ -> MAlonzo.RTE.mazUnreachableError
          MAlonzo.Code.Utils.C_inj'8322'_14 v3
            -> coe
@@ -140,5 +140,5 @@ d_runCertifierMain_12 v0 v1
                       MAlonzo.Code.Utils.C__'44'__442
                       (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                       (coe
-                         MAlonzo.Code.CertifierReport.d_makeReport_282 (coe v2) (coe v1))))
+                         MAlonzo.Code.CertifierReport.d_makeReport_284 (coe v2) (coe v1))))
          _ -> MAlonzo.RTE.mazUnreachableError)