Certifier: add force-case-delay translation relation by ana-pantilie · Pull Request #7594 · IntersectMBO/plutus

ana-pantilie · 2026-02-16T11:41:27Z

Fixes https://github.com/IntersectMBO/plutus-private/issues/2053

zliu41

Looks reasonable - could you share benchmarking results from cabal bench plutus-benchmark:certifier-bench?

zliu41 · 2026-02-26T16:46:25Z

plutus-metatheory/src/VerifiedCompilation/UForceCaseDelay.lagda.md

+
+The Force-Case-Delay compiler optimization phase transforms terms of the form: `force (case scrut [\x1... -> delay term_1, ..., \x1... -> delay term_m])` into `case scrut [\x1... -> term_1, ..., \x1... -> term_m]`. Note that the delay must appear in all the branches of the case, under any number (including zero) of lambda abstractions.
+
+An important remark is that this transformation is not semantics-preserving in general, but it is semantics preserving when the program is "well-formed". We do not have a formal definition of well-formedness, this is left as future work. For more information about the intuitive notion of well-formedness, see `Note [Applying force to delays in case branches]` in the Untyped Plutus Core implementation of the Force-Case-Delay optimization phase.


well-formedness

Is that not the same as "the UPLC program is typeable in TPLC"? Or similarly (though not equivalently), "evaluating the UPLC program does not lead to MachineError"? If you are talking about formalizing it in Agda, I don't think that's possible - I think it is undecidable.

the UPLC program is typeable in TPLC

I think this is more restrictive than what we mean by "well-defined".

evaluating the UPLC program does not lead to MachineError

That's probably the best definition, and if I'm not mistaken it appears in the note.

If you are talking about formalizing it in Agda, I don't think that's possible - I think it is undecidable.

It might not be, but I'm not entirely convinced we can't find a formalization which, although not complete, is enough for our purposes.

If you are talking about formalizing it in Agda, I don't think that's possible - I think it is undecidable.

It is certainly possible to formalize such a property, it's just undecidable in general. However, it (or a weaker property that suffices) may follow from typeability in TPLC and if it is preserved by the translation relations, we could prove it for what Ana describes.

I imagine it's only possible to formalize it in very special cases, unless I'm missing something

It's terms like

force case (constr 0 [true, false]) [ \x y z -> delay x ]

that make it unsound in general (note the amount of parameters in the branch does not line up), because it's optimised to

case (constr 0 [true, false]) [ \x y z -> x ]

I don't expect you could ever obtain the first term from the optimiser when starting out with a TPLC-typable term. Or can we?

In any case, it's unclear what that property would be exactly.

zliu41 · 2026-02-26T16:47:01Z

plutus-metatheory/src/VerifiedCompilation/UForceCaseDelay.lagda.md

+
+variable
+  n : ℕ
+  M N : n ⊢


I think we use X ⊢ in most other places

I know, but I don't like that notation. It gives me the impression that X can be any type, when it's just a natural number.

X is a left-over from when terms used to be indexes by X : Set which was instantiated to nested Maybe. I'm in favor of n, and we should eventually change that in other places too.

Or Γ, which is commonly used for context?

That works too, although I'd associate it more with a typing context, rather than scoping.

zliu41 · 2026-02-26T16:48:52Z

plutus-metatheory/src/VerifiedCompilation/UForceCaseDelay.lagda.md

+
+isForceCaseDelay? : MatchOrCE (ForceCaseDelay {n})
+
+{-# TERMINATING #-}


Do you know which recursive call upsets the termination checker?

ana-pantilie · 2026-02-27T10:07:45Z

@zliu41 The benchmarking results:

benchmarking N Queens
time                 56.44 ms   (52.06 ms .. 59.90 ms)
                     0.985 R²   (0.965 R² .. 0.995 R²)
mean                 53.26 ms   (49.51 ms .. 56.85 ms)
std dev              7.223 ms   (5.064 ms .. 10.26 ms)
variance introduced by outliers: 52% (severely inflated)

benchmarking Cardano Open Oracle Protocol
time                 138.6 ms   (129.4 ms .. 145.4 ms)
                     0.997 R²   (0.992 R² .. 1.000 R²)
mean                 133.2 ms   (118.2 ms .. 139.3 ms)
std dev              13.93 ms   (3.785 ms .. 22.51 ms)
variance introduced by outliers: 35% (moderately inflated)

benchmarking Linear Vesting
time                 68.56 ms   (63.95 ms .. 72.28 ms)
                     0.990 R²   (0.975 R² .. 0.998 R²)
mean                 65.79 ms   (60.93 ms .. 70.00 ms)
std dev              7.765 ms   (5.032 ms .. 11.93 ms)
variance introduced by outliers: 43% (moderately inflated)

benchmarking Cardano Loans
time                 554.2 ms   (444.8 ms .. 654.2 ms)
                     0.995 R²   (0.982 R² .. 1.000 R²)
mean                 550.8 ms   (532.4 ms .. 563.1 ms)
std dev              18.72 ms   (8.999 ms .. 24.34 ms)
variance introduced by outliers: 19% (moderately inflated)

benchmarking Marlowe
time                 564.4 ms   (541.3 ms .. 610.2 ms)
                     0.999 R²   (0.999 R² .. 1.000 R²)
mean                 568.9 ms   (560.2 ms .. 580.9 ms)
std dev              11.63 ms   (3.984 ms .. 15.41 ms)
variance introduced by outliers: 19% (moderately inflated)

The numbers are quite similar to the ones from your PR which improved the certifier performance. Note that we're running them on different machines, so it's possible my machine is faster and that explains why the numbers are lower.

basetunnel · 2026-02-27T11:19:41Z

@zliu41 The benchmarking results:

benchmarking N Queens
time                 56.44 ms   (52.06 ms .. 59.90 ms)
                     0.985 R²   (0.965 R² .. 0.995 R²)
mean                 53.26 ms   (49.51 ms .. 56.85 ms)
std dev              7.223 ms   (5.064 ms .. 10.26 ms)
variance introduced by outliers: 52% (severely inflated)

benchmarking Cardano Open Oracle Protocol
time                 138.6 ms   (129.4 ms .. 145.4 ms)
                     0.997 R²   (0.992 R² .. 1.000 R²)
mean                 133.2 ms   (118.2 ms .. 139.3 ms)
std dev              13.93 ms   (3.785 ms .. 22.51 ms)
variance introduced by outliers: 35% (moderately inflated)

benchmarking Linear Vesting
time                 68.56 ms   (63.95 ms .. 72.28 ms)
                     0.990 R²   (0.975 R² .. 0.998 R²)
mean                 65.79 ms   (60.93 ms .. 70.00 ms)
std dev              7.765 ms   (5.032 ms .. 11.93 ms)
variance introduced by outliers: 43% (moderately inflated)

benchmarking Cardano Loans
time                 554.2 ms   (444.8 ms .. 654.2 ms)
                     0.995 R²   (0.982 R² .. 1.000 R²)
mean                 550.8 ms   (532.4 ms .. 563.1 ms)
std dev              18.72 ms   (8.999 ms .. 24.34 ms)
variance introduced by outliers: 19% (moderately inflated)

benchmarking Marlowe
time                 564.4 ms   (541.3 ms .. 610.2 ms)
                     0.999 R²   (0.999 R² .. 1.000 R²)
mean                 568.9 ms   (560.2 ms .. 580.9 ms)
std dev              11.63 ms   (3.984 ms .. 15.41 ms)
variance introduced by outliers: 19% (moderately inflated)

The numbers are quite similar to the ones from your PR which improved the certifier performance. Note that we're running them on different machines, so it's possible my machine is faster and that explains why the numbers are lower.

Could you comment out the other passes in VerifiedCompilation.lagda.md to see what the performance is of this single procedure?

ana-pantilie changed the title ~~Certifier: add force-case-delay transition relation~~ Certifier: add force-case-delay translation relation Feb 17, 2026

ana-pantilie force-pushed the ana/certifier-forcecasedelay branch from 88d9ba0 to 3d80c91 Compare February 18, 2026 18:36

ana-pantilie force-pushed the ana/certifier-forcecasedelay branch 2 times, most recently from 8238d2e to c795e79 Compare February 26, 2026 13:54

ana-pantilie added 2 commits February 26, 2026 15:57

Stub for force case delay

2744281

Force-Case-Delay final version

86ec713

ana-pantilie force-pushed the ana/certifier-forcecasedelay branch from c795e79 to 86ec713 Compare February 26, 2026 13:58

ana-pantilie marked this pull request as ready for review February 26, 2026 13:59

ana-pantilie requested review from basetunnel, ramsay-t and zliu41 February 26, 2026 13:59

zliu41 approved these changes Feb 26, 2026

View reviewed changes

basetunnel approved these changes Feb 27, 2026

View reviewed changes


		The Force-Case-Delay compiler optimization phase transforms terms of the form: `force (case scrut [\x1... -> delay term_1, ..., \x1... -> delay term_m])` into `case scrut [\x1... -> term_1, ..., \x1... -> term_m]`. Note that the delay must appear in all the branches of the case, under any number (including zero) of lambda abstractions.

		An important remark is that this transformation is not semantics-preserving in general, but it is semantics preserving when the program is "well-formed". We do not have a formal definition of well-formedness, this is left as future work. For more information about the intuitive notion of well-formedness, see `Note [Applying force to delays in case branches]` in the Untyped Plutus Core implementation of the Force-Case-Delay optimization phase.


		isForceCaseDelay? : MatchOrCE (ForceCaseDelay {n})

		{-# TERMINATING #-}

Conversation

ana-pantilie commented Feb 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

zliu41 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ana-pantilie commented Feb 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

basetunnel commented Feb 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ana-pantilie commented Feb 16, 2026 •

edited

Loading

ana-pantilie commented Feb 27, 2026 •

edited

Loading