Move CSE to the unimplemented-in-the-certifier category (#7734)

* Move CSE to the unimplemented-in-the-certifier category

* Remove dead code

* Fix order of constructors in Agda <-> Haskell FFI

Author: ana-pantilie

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

@@ -15,20 +15,25 @@ certified.
 
 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. -}
+the pass will be also certified in the same PR.
+
+IMPORTANT: 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
+of their counterparts in 'VerifiedCompilation.Trace'.
+
 IMPORTANT: if you add a new pass, or modify an existing pass, without
 also modifying the certifier in the same PR, you must add/move its
 corresponding constructor to this type. Please also open an issue
@@ -37,6 +42,7 @@ data UncertifiedOptStage
   = CaseOfCase
   | LetFloatOut
   | CaseReduce
+  | CSE
   deriving stock (Show, Generic)
   deriving anyclass (NFData)
 
@@ -58,7 +64,7 @@ pattern InlineStage :: OptStage
 pattern InlineStage = Right Inline
 
 pattern CseStage :: OptStage
-pattern CseStage = Right CSE
+pattern CseStage = Left CSE
 
 pattern ApplyToCaseStage :: OptStage
 pattern ApplyToCaseStage = Right ApplyToCase

plutus-metatheory/changelog.d/20260422_153424_ana.pantilie95_move_cse_to_unimplementedcert.md

@@ -0,0 +1,3 @@
+### Removed
+
+- Temporarily disabled the CSE certifier pass due to the discovery of bugs in the specification.

plutus-metatheory/plutus-metatheory.cabal

@@ -377,8 +377,6 @@ 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,7 +116,6 @@ 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_12)
+        MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_14)
      (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_12)
+          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_14)
        (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_12)
+        MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_14)
      (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_284 (coe v2) (coe v1)))
+                             MAlonzo.Code.CertifierReport.d_makeReport_282 (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_284 (coe v2) (coe v1)))
+                             MAlonzo.Code.CertifierReport.d_makeReport_282 (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_284 (coe v2) (coe v1))))
+                         MAlonzo.Code.CertifierReport.d_makeReport_282 (coe v2) (coe v1))))
          _ -> MAlonzo.RTE.mazUnreachableError)