Skip to content

Certifier: add force-case-delay translation relation #7594

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ana-pantilie merged 4 commits into from
Mar 31, 2026
Merged

Certifier: add force-case-delay translation relation #7594

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a57abce
Stub for force case delay
ana-pantilie Feb 16, 2026
6363ed9
Force-Case-Delay final version
ana-pantilie Feb 17, 2026
38cc948
Add force-case-delay to list of implemented certifier passes, fix gol…
ana-pantilie Mar 30, 2026
8c63e10
Add changelog
ana-pantilie Mar 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions ...tatheory/changelog.d/20260331_023533_ana.pantilie95_certifier_forcecasedelay.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
### Added

- Added a compiler certification pass for the force-case-delay optimization.

1 change: 1 addition & 0 deletions plutus-metatheory/plutus-metatheory.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -377,6 +377,7 @@ library
MAlonzo.Code.VerifiedCompilation.UCaseReduce
MAlonzo.Code.VerifiedCompilation.UCSE
MAlonzo.Code.VerifiedCompilation.UFloatDelay
MAlonzo.Code.VerifiedCompilation.UForceCaseDelay
MAlonzo.Code.VerifiedCompilation.UForceDelay
MAlonzo.Code.VerifiedCompilation.UInline
MAlonzo.Code.VerifiedCompilation.UntypedTranslation
Expand Down
22 changes: 12 additions & 10 deletions plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ import qualified MAlonzo.Code.VerifiedCompilation.UApplyToCase
import qualified MAlonzo.Code.VerifiedCompilation.UCSE
import qualified MAlonzo.Code.VerifiedCompilation.UCaseReduce
import qualified MAlonzo.Code.VerifiedCompilation.UFloatDelay
import qualified MAlonzo.Code.VerifiedCompilation.UForceCaseDelay
import qualified MAlonzo.Code.VerifiedCompilation.UForceDelay
import qualified MAlonzo.Code.VerifiedCompilation.UInline

Expand All @@ -52,7 +53,7 @@ d_mRelationOf_12 v0
MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_8
-> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 erased
MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_10
-> coe MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 erased
MAlonzo.Code.VerifiedCompilation.Trace.C_caseOfCaseT_12
-> coe MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_14
Expand Down Expand Up @@ -90,37 +91,38 @@ d_certifyPass_24 v0 v1
= case coe v0 of
MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_6
-> coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_184
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_8
-> coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_184
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_10
-> coe
(\ v2 v3 ->
coe
MAlonzo.Code.VerifiedCompilation.NotImplemented.du_certNotImplemented_22)
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192
(coe
MAlonzo.Code.VerifiedCompilation.UForceCaseDelay.d_isForceCaseDelay'63'_94
(coe (0 :: Integer)))
MAlonzo.Code.VerifiedCompilation.Trace.C_caseOfCaseT_12
-> coe
(\ v2 v3 ->
coe
MAlonzo.Code.VerifiedCompilation.NotImplemented.du_certNotImplemented_22)
MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_14
-> coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_184
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192
(coe
MAlonzo.Code.VerifiedCompilation.UCaseReduce.d_isCaseReduce'63'_26
(coe (0 :: Integer)))
MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_16
-> case coe v1 of
MAlonzo.Code.VerifiedCompilation.Trace.C_inline_54 v2
-> coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_checker_148
MAlonzo.Code.VerifiedCompilation.Certificate.du_checker_156
(coe
MAlonzo.Code.VerifiedCompilation.UInline.d_top'45'check_718
(coe v2))
Expand All @@ -130,13 +132,13 @@ d_certifyPass_24 v0 v1
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_18
-> coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_184
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192
(coe
MAlonzo.Code.VerifiedCompilation.UCSE.d_isUntypedCSE'63'_26
(coe (0 :: Integer)))
MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_20
-> coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_184
MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_192
(coe
MAlonzo.Code.VerifiedCompilation.UApplyToCase.d_a2c'63''7580''7580'_24
(coe (0 :: Integer)))
Expand Down
122 changes: 72 additions & 50 deletions plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
Expand All @@ -39,88 +40,109 @@ data T_ProofOrCE_38
= C_proof_44 AgdaAny |
C_ce_52 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.isProof?
d_isProof'63'_56 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_ProofOrCE_38 -> Bool
d_isProof'63'_56 ~v0 ~v1 v2 = du_isProof'63'_56 v2
du_isProof'63'_56 :: T_ProofOrCE_38 -> Bool
du_isProof'63'_56 v0
= case coe v0 of
C_proof_44 v1 -> coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10
C_ce_52 v4 v5 v6 -> coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8
_ -> MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.isCE?
d_isCE'63'_60 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_ProofOrCE_38 -> Bool
d_isCE'63'_60 ~v0 ~v1 v2 = du_isCE'63'_60 v2
du_isCE'63'_60 :: T_ProofOrCE_38 -> Bool
du_isCE'63'_60 v0
= coe
MAlonzo.Code.Data.Bool.Base.d_not_22
(coe du_isProof'63'_56 (coe v0))
-- VerifiedCompilation.Certificate.Proof?
d_Proof'63'_58 a0 a1 = ()
data T_Proof'63'_58
= C_proof_64 AgdaAny |
C_abort_70 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
d_Proof'63'_66 a0 a1 = ()
data T_Proof'63'_66
= C_proof_72 AgdaAny |
C_abort_78 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
AgdaAny AgdaAny
-- VerifiedCompilation.Certificate._>>=_
d__'62''62''61'__80 ::
d__'62''62''61'__88 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
T_Proof'63'_58 -> (AgdaAny -> T_Proof'63'_58) -> T_Proof'63'_58
d__'62''62''61'__80 ~v0 ~v1 ~v2 ~v3 v4 v5
= du__'62''62''61'__80 v4 v5
du__'62''62''61'__80 ::
T_Proof'63'_58 -> (AgdaAny -> T_Proof'63'_58) -> T_Proof'63'_58
du__'62''62''61'__80 v0 v1
T_Proof'63'_66 -> (AgdaAny -> T_Proof'63'_66) -> T_Proof'63'_66
d__'62''62''61'__88 ~v0 ~v1 ~v2 ~v3 v4 v5
= du__'62''62''61'__88 v4 v5
du__'62''62''61'__88 ::
T_Proof'63'_66 -> (AgdaAny -> T_Proof'63'_66) -> T_Proof'63'_66
du__'62''62''61'__88 v0 v1
= case coe v0 of
C_proof_64 v2 -> coe v1 v2
C_abort_70 v4 v5 v6 -> coe C_abort_70 v4 v5 v6
C_proof_72 v2 -> coe v1 v2
C_abort_78 v4 v5 v6 -> coe C_abort_78 v4 v5 v6
_ -> MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.DecidableCE
d_DecidableCE_100 ::
d_DecidableCE_108 ::
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) -> ()
d_DecidableCE_100 = erased
d_DecidableCE_108 = erased
-- VerifiedCompilation.Certificate.Checkable
d_Checkable_118 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Checkable_118 = erased
d_Checkable_126 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Checkable_126 = erased
-- VerifiedCompilation.Certificate.Certifiable
d_Certifiable_134 :: () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Certifiable_134 = erased
d_Certifiable_142 :: () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Certifiable_142 = erased
-- VerifiedCompilation.Certificate.checker
d_checker_148 ::
d_checker_156 ::
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> T_Proof'63'_58) ->
(AgdaAny -> AgdaAny -> T_Proof'63'_66) ->
AgdaAny -> AgdaAny -> T_CertResult_12
d_checker_148 ~v0 ~v1 v2 v3 v4 = du_checker_148 v2 v3 v4
du_checker_148 ::
(AgdaAny -> AgdaAny -> T_Proof'63'_58) ->
d_checker_156 ~v0 ~v1 v2 v3 v4 = du_checker_156 v2 v3 v4
du_checker_156 ::
(AgdaAny -> AgdaAny -> T_Proof'63'_66) ->
AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_148 v0 v1 v2
du_checker_156 v0 v1 v2
= let v3 = coe v0 v1 v2 in
coe
(case coe v3 of
C_proof_64 v4 -> coe C_proof_18 (coe v4)
C_abort_70 v6 v7 v8 -> coe C_abort_32 v6 v7 v8
C_proof_72 v4 -> coe C_proof_18 (coe v4)
C_abort_78 v6 v7 v8 -> coe C_abort_32 v6 v7 v8
_ -> MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.decider
d_decider_184 ::
d_decider_192 ::
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
AgdaAny -> AgdaAny -> T_CertResult_12
d_decider_184 ~v0 ~v1 v2 v3 v4 = du_decider_184 v2 v3 v4
du_decider_184 ::
d_decider_192 ~v0 ~v1 v2 v3 v4 = du_decider_192 v2 v3 v4
du_decider_192 ::
(AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_184 v0 v1 v2
du_decider_192 v0 v1 v2
= let v3 = coe v0 v1 v2 in
coe
(case coe v3 of
C_proof_44 v4 -> coe C_proof_18 (coe v4)
C_ce_52 v7 v8 v9 -> coe C_ce_26 v7 v8 v9
_ -> MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.decToPCE
d_decToPCE_226 ::
d_decToPCE_234 ::
() ->
() ->
MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
AgdaAny -> AgdaAny -> T_ProofOrCE_38
d_decToPCE_226 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_226 v2 v3 v4 v5
du_decToPCE_226 ::
d_decToPCE_234 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_234 v2 v3 v4 v5
du_decToPCE_234 ::
MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_decToPCE_226 v0 v1 v2 v3
du_decToPCE_234 v0 v1 v2 v3
= case coe v1 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v4 v5
-> if coe v4
Expand All @@ -131,15 +153,15 @@ du_decToPCE_226 v0 v1 v2 v3
else coe seq (coe v5) (coe C_ce_52 v0 v2 v3)
_ -> MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.pceToDec
d_pceToDec_240 ::
d_pceToDec_248 ::
() ->
T_ProofOrCE_38 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_pceToDec_240 ~v0 v1 = du_pceToDec_240 v1
du_pceToDec_240 ::
d_pceToDec_248 ~v0 v1 = du_pceToDec_248 v1
du_pceToDec_248 ::
T_ProofOrCE_38 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_pceToDec_240 v0
du_pceToDec_248 v0
= case coe v0 of
C_proof_44 v1
-> coe
Expand All @@ -153,7 +175,7 @@ du_pceToDec_240 v0
(coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
_ -> MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.matchOrCE
d_matchOrCE_254 ::
d_matchOrCE_262 ::
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
Expand All @@ -163,15 +185,15 @@ d_matchOrCE_254 ::
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
AgdaAny -> AgdaAny -> T_ProofOrCE_38
d_matchOrCE_254 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
= du_matchOrCE_254 v4 v5 v6 v7
du_matchOrCE_254 ::
d_matchOrCE_262 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
= du_matchOrCE_262 v4 v5 v6 v7
du_matchOrCE_262 ::
MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_matchOrCE_254 v0 v1 v2 v3
du_matchOrCE_262 v0 v1 v2 v3
= let v4 = coe v1 v2 v3 in
coe
(case coe v4 of
Expand All @@ -184,21 +206,21 @@ du_matchOrCE_254 v0 v1 v2 v3
else coe seq (coe v6) (coe C_ce_52 v0 v2 v3)
_ -> MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.pcePointwise
d_pcePointwise_296 ::
d_pcePointwise_304 ::
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
(AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
[AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
d_pcePointwise_296 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
= du_pcePointwise_296 v4 v5 v6 v7
du_pcePointwise_296 ::
d_pcePointwise_304 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
= du_pcePointwise_304 v4 v5 v6 v7
du_pcePointwise_304 ::
MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
(AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
[AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
du_pcePointwise_296 v0 v1 v2 v3
du_pcePointwise_304 v0 v1 v2 v3
= case coe v2 of
[]
-> case coe v3 of
Expand All @@ -218,7 +240,7 @@ du_pcePointwise_296 v0 v1 v2 v3
(case coe v8 of
C_proof_44 v9
-> let v10
= coe du_pcePointwise_296 (coe v0) (coe v1) (coe v5) (coe v7) in
= coe du_pcePointwise_304 (coe v0) (coe v1) (coe v5) (coe v7) in
coe
(case coe v10 of
C_proof_44 v11
Expand Down
6 changes: 3 additions & 3 deletions plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -582,7 +582,7 @@ d_isCoC'63'_264 v0 v1 v2
v43)
(let v44
= coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_296
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_304
(coe
MAlonzo.Code.VerifiedCompilation.Trace.C_caseOfCaseT_12)
(coe
Expand All @@ -599,7 +599,7 @@ d_isCoC'63'_264 v0 v1 v2
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_44 v45
-> let v46
= coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_296
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_304
(coe
MAlonzo.Code.VerifiedCompilation.Trace.C_caseOfCaseT_12)
(coe
Expand All @@ -616,7 +616,7 @@ d_isCoC'63'_264 v0 v1 v2
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_44 v47
-> let v48
= coe
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_296
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_304
(coe
MAlonzo.Code.VerifiedCompilation.Trace.C_caseOfCaseT_12)
(coe
Expand Down
Loading
Loading