Enable calling procedures in contracts by keyboardDrummer · Pull Request #1352 · strata-org/Strata

keyboardDrummer · 2026-06-10T08:24:12Z

Functional changes

[Debugging] Improve the printing of Laurel if-then-else expressions
EliminateReturnsInExpression now runs for procedures as well, which enables more types of transparent bodies for procedures. To make it work for both functions and procedures, it was also necessary for the body of functions to be immediately wrapped in a return statement during parsing.
Allow calling procedures from contracts. Combined with the previous change this makes procedures strictly more powerful than functions
Let the transparency pass rewrite the bodies of assume statements so they don't assert anything.
Improve diagnostics related to contracts, using the correct verbiage "precondition" and "postcondition" instead of "assertion"
Generalized the LaurelPass concept so it works for all transformation between Laurel source and Core, not just the Laurel->Laurel transformation. This helps make the documentation more complete.

Why let the transparency pass rewrite the bodies of assume statements so they don't assert anything?

After the contract pass, a call will look like assert <preconditions>; call(..); assume <postconditions>, where the body of the callee looks like assume <preconditions>; <body>; assert <postconditions>. If we now do either concrete execution, or we do inlining, then any assertions that occur inside the pre or postconditions will be asserted twice, because they occur once in an assert and once in an assume. By ignoring the assertions inside the assume, we prevent the duplication.

Whether you also want this behavior for assumptions that were created by users is something I'm not sure about. However, if we want we can let those behave differently. Right now I think we don't have enough data to decide what we want for user created assumptions, and they are AFAIK not yet used, so I think it's OK to change their behavior.

Implementation

Add these passes:

[New] EliminateReturnStatements: rewrite return to exit statements, needed for the next pass.
[New] ContractPass: translate away pre and postconditions entirely by introducing assertion and assumptions at call sites and at procedure starts and ends
[Updated] Lift assertions, assumptions and procedure calls when they occur in expressions. Note: the changes in this pass could have been extracted to a different PR to reduce the scope of this one, but I think that keeping them in this PR is most efficient from a developer time perspective.

Follow-up work

Remove the now obsolete functions from Laurel
Create WF proofs for quantifier bodies
Lift assumptions in expressions to axioms.
In the transparency phase, if something has no asserts and only calls functions, only create a function and no procedure

…y pass

…y-pass-only

…trata into transparency-pass-only

ContractPass (strata-org#1352, Remy Willems) was correct for every program expressible on its base: the base has no `<T>` grammar binder and nothing constructs a `.TVar` parameter type, so a polymorphic procedure could not exist and the pass only ever saw monomorphic procedures. This extends it to the new input class strata-org#1394 introduces — procedures with type parameters — which is an integration requirement of the polymorphism work, not a defect in strata-org#1352. Two changes, both gated on the presence of a type variable (no-op, byte-identical for monomorphic callees): - Call-site arg temps: the pass emits `var $cp : <paramType> := arg` typed at the callee's DECLARED param type. For a polymorphic callee (`idp<T>(x: T)`) that is the type variable `T`, which resolution treats as authoritative and never replaces with the argument's type — so `T` reaches Core unbound, and a multi-instantiation body (`idp(5)` + `idp(true)`) forces one `T` to be both `int` and `bool`. When a param type mentions a `.TVar`, type the temp from the ARGUMENT instead (`computeExprType`), giving each call site its own instantiation. - Contract helper functions: `$pre`/`$post` helpers mention `T` in their parameter types, so they must bind the procedure's `typeArgs`. Threads the SemanticModel into the pass (it was discarded) to type arguments. Surfaced by rebasing strata-org#1394 onto a base that had since added ContractPass; pins poly_proc_sound / poly_proc_multi / generic_map_param.

The post-covariance checker asserted Parent.post after assuming Child.post, but with `preconditions := []` — it never assumed Parent.pre. Behavioral post-covariance is `Parent.pre ⇒ (Child.post ⇒ Parent.post)`: a caller invoking the parent contract has already established Parent.pre, so a sound covariant override whose post implies the parent's only UNDER the parent precondition (e.g. parent `requires a >= 0 ensures r >= 0`, child `ensures r == a`) was spuriously OVER-REJECTED. Fix: the post-checker now assumes Parent.pre (renamed into the child's parameter names). Parent.pre — NOT Child.pre: Child.pre is contravariantly weaker and assuming it would be unsound; Parent.pre ⇒ Child.pre is enforced separately by the pre-checker. Completeness fix (was over-rejection, never wrong-accept); the genuine-violation twin still fails even with Parent.pre assumed. Surfaced by rebasing onto a base that added ContractPass (strata-org#1352), which made `requires` clauses meaningful end-to-end and exposed this latent gap. 2 new corpus cases (liskov_post_covariance_under_parent_pre + its must-fail violation twin). Full lake test green (only pre-existing ion-java).

…ring Merging the base brought in #1352, whose ContractPass desugars every procedure contract into helper functions and strips the procedure's preconditions. Core's `mkContractWFProc` checks a postcondition's partial-op well-formedness assuming the procedure's preconditions (and earlier postconditions) in declaration order; with the preconditions stripped, that context is gone, so a postcondition that is well-formed only under those conditions becomes unprovable. This broke the Seq/Array contract tests (T24 `contractSeq`, T25 `setFirst`), where `Sequence.select` / `a[0]` carry bounds preconditions. Fix (no Core change): - ContractPass keeps a procedure's non-procedure-calling preconditions as *free* instead of stripping them. Call-site checking is unchanged (the `$pre` helpers still assert them), but `mkContractWFProc` and the body VC again assume them, restoring the context for native (opaque-path) postcondition WF. Procedure-calling preconditions are dropped from the spec (illegal as a contract expression) and enforced only via their `$pre` helper. - The `$postN` helper body is guarded as `context ==> condition` (context = preconditions ++ earlier postconditions). Core's WF-obligation collector assumes an implication's LHS when checking the RHS, so the helper's own partial-op WF sees that context — this reaches the sibling-postcondition case (e.g. `ensures Array.length(a) > 0; ensures a[0] == v`) that a precondition alone cannot supply. - TransparencyPass strips preconditions from the `$asFunction` twin: now that ContractPass retains them on the procedure, the twin would otherwise inherit them and fire a duplicate WF obligation at every application. - SubscriptElim: adapt `subscriptElimPass` to the renamed `LoweringPass` and 3-argument `run` signature introduced by the base. Verified: full StrataTest suite (566 jobs) green; adversarial soundness probes pass (false pre/postconditions still rejected, call-site precondition violations still caught), differential-identical to the base. See #1418.

…ring Merging the base brought in #1352, whose ContractPass desugars every procedure contract into helper functions and strips the procedure's preconditions. Core's `mkContractWFProc` checks a postcondition's partial-op well-formedness assuming the procedure's preconditions (and earlier postconditions) in declaration order; with the preconditions stripped, that context is gone, so a postcondition that is well-formed only under those conditions becomes unprovable. This broke the Seq/Array contract tests (T24 `contractSeq`, T25 `setFirst`), where `Sequence.select` / `a[0]` carry bounds preconditions. Fix (no Core change): - The `$postN` postcondition helper carries the procedure's preconditions plus the earlier postconditions as *free* preconditions of the helper. Core's function-WF generation assumes a function's preconditions in order before checking the WF of its body, so a partial op in the postcondition is checked with that context in scope. Carrying them on the helper (rather than guarding the body as `assumed ==> condition`) means a call site that applies the helper learns the postcondition directly; `free` keeps them assumption-only, so they are never re-asserted there. - ContractPass keeps a procedure's non-procedure-calling preconditions as *free* instead of stripping them. The opaque path retains the postcondition natively on the procedure (it is the impl-satisfaction check, run by Core's `ProcedureEval`/`mkContractWFProc` over `spec.postconditions` — distinct from the `$post` helper, which only handles call sites). Without the preconditions in scope, that native postcondition's partial-op WF is unprovable. Call-site checking is unchanged (the `$pre` helpers still assert them). Procedure-calling preconditions are dropped from the spec (illegal as a contract expression) and enforced only via their `$pre` helper. - TransparencyPass strips preconditions from the `$asFunction` twin: now that ContractPass retains them on the procedure, the twin would otherwise inherit them and fire a duplicate WF obligation at every application. - SubscriptElim: adapt `subscriptElimPass` to the renamed `LoweringPass` and 3-argument `run` signature introduced by the base. Verified: full StrataTest suite (566 jobs) green; adversarial soundness probes pass (false pre/postconditions rejected, call-site precondition violations caught), differential-identical to base. See #1418.

The post-covariance checker asserted Parent.post after assuming Child.post, but with `preconditions := []` — it never assumed Parent.pre. Behavioral post-covariance is `Parent.pre ⇒ (Child.post ⇒ Parent.post)`: a caller invoking the parent contract has already established Parent.pre, so a sound covariant override whose post implies the parent's only UNDER the parent precondition (e.g. parent `requires a >= 0 ensures r >= 0`, child `ensures r == a`) was spuriously OVER-REJECTED. Fix: the post-checker now assumes Parent.pre (renamed into the child's parameter names). Parent.pre — NOT Child.pre: Child.pre is contravariantly weaker and assuming it would be unsound; Parent.pre ⇒ Child.pre is enforced separately by the pre-checker. Completeness fix (was over-rejection, never wrong-accept); the genuine-violation twin still fails even with Parent.pre assumed. Surfaced by rebasing onto a base that added ContractPass (strata-org#1352), which made `requires` clauses meaningful end-to-end and exposed this latent gap. 2 new corpus cases (liskov_post_covariance_under_parent_pre + its must-fail violation twin). Full lake test green (only pre-existing ion-java).

ContractPass (strata-org#1352, Remy Willems) was correct for every program expressible on its base: the base has no `<T>` grammar binder and nothing constructs a `.TVar` parameter type, so a polymorphic procedure could not exist and the pass only ever saw monomorphic procedures. This extends it to the new input class strata-org#1394 introduces — procedures with type parameters — which is an integration requirement of the polymorphism work, not a defect in strata-org#1352. Two changes, both gated on the presence of a type variable (no-op, byte-identical for monomorphic callees): - Call-site arg temps: the pass emits `var $cp : <paramType> := arg` typed at the callee's DECLARED param type. For a polymorphic callee (`idp<T>(x: T)`) that is the type variable `T`, which resolution treats as authoritative and never replaces with the argument's type — so `T` reaches Core unbound, and a multi-instantiation body (`idp(5)` + `idp(true)`) forces one `T` to be both `int` and `bool`. When a param type mentions a `.TVar`, type the temp from the ARGUMENT instead (`computeExprType`), giving each call site its own instantiation. - Contract helper functions: `$pre`/`$post` helpers mention `T` in their parameter types, so they must bind the procedure's `typeArgs`. Threads the SemanticModel into the pass (it was discarded) to type arguments. Surfaced by rebasing strata-org#1394 onto a base that had since added ContractPass; pins poly_proc_sound / poly_proc_multi / generic_map_param.

The post-covariance checker asserted Parent.post after assuming Child.post, but with `preconditions := []` — it never assumed Parent.pre. Behavioral post-covariance is `Parent.pre ⇒ (Child.post ⇒ Parent.post)`: a caller invoking the parent contract has already established Parent.pre, so a sound covariant override whose post implies the parent's only UNDER the parent precondition (e.g. parent `requires a >= 0 ensures r >= 0`, child `ensures r == a`) was spuriously OVER-REJECTED. Fix: the post-checker now assumes Parent.pre (renamed into the child's parameter names). Parent.pre — NOT Child.pre: Child.pre is contravariantly weaker and assuming it would be unsound; Parent.pre ⇒ Child.pre is enforced separately by the pre-checker. Completeness fix (was over-rejection, never wrong-accept); the genuine-violation twin still fails even with Parent.pre assumed. Surfaced by rebasing onto a base that added ContractPass (strata-org#1352), which made `requires` clauses meaningful end-to-end and exposed this latent gap. 2 new corpus cases (liskov_post_covariance_under_parent_pre + its must-fail violation twin). Full lake test green (only pre-existing ion-java).

## Functional changes 1. [Debugging] Improve the printing of Laurel if-then-else expressions 1. `EliminateReturnsInExpression` now runs for procedures as well, which enables more types of transparent bodies for procedures. To make it work for both functions and procedures, it was also necessary for the body of functions to be immediately wrapped in a return statement during parsing. 1. Allow calling procedures from contracts. Combined with the previous change this makes procedures strictly more powerful than functions 1. Let the transparency pass rewrite the bodies of assume statements so they don't assert anything. 1. Improve diagnostics related to contracts, using the correct verbiage "precondition" and "postcondition" instead of "assertion" 1. Generalized the `LaurelPass` concept so it works for all transformation between Laurel source and Core, not just the Laurel->Laurel transformation. This helps make the documentation more complete. ### Why let the transparency pass rewrite the bodies of assume statements so they don't assert anything? After the contract pass, a call will look like `assert <preconditions>; call(..); assume <postconditions>`, where the body of the callee looks like `assume <preconditions>; <body>; assert <postconditions>`. If we now do either concrete execution, or we do inlining, then any assertions that occur inside the pre or postconditions will be asserted twice, because they occur once in an assert and once in an assume. By ignoring the assertions inside the assume, we prevent the duplication. Whether you also want this behavior for assumptions that were created by users is something I'm not sure about. However, if we want we can let those behave differently. Right now I think we don't have enough data to decide what we want for user created assumptions, and they are AFAIK not yet used, so I think it's OK to change their behavior. ## Implementation Add these passes: - [New] EliminateReturnStatements: rewrite `return` to `exit` statements, needed for the next pass. - [New] ContractPass: translate away pre and postconditions entirely by introducing assertion and assumptions at call sites and at procedure starts and ends - [Updated] Lift assertions, assumptions and procedure calls when they occur in expressions. Note: the changes in this pass could have been extracted to a different PR to reduce the scope of this one, but I think that keeping them in this PR is most efficient from a developer time perspective. ## Follow-up work - Remove the now obsolete functions from Laurel - Create WF proofs for quantifier bodies - Lift assumptions in expressions to axioms. - In the transparency phase, if something has no asserts and only calls functions, only create a function and no procedure --------- Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com> Co-authored-by: Fabio Madge <fabio@madge.me>

The post-covariance checker asserted Parent.post after assuming Child.post, but with `preconditions := []` — it never assumed Parent.pre. Behavioral post-covariance is `Parent.pre ⇒ (Child.post ⇒ Parent.post)`: a caller invoking the parent contract has already established Parent.pre, so a sound covariant override whose post implies the parent's only UNDER the parent precondition (e.g. parent `requires a >= 0 ensures r >= 0`, child `ensures r == a`) was spuriously OVER-REJECTED. Fix: the post-checker now assumes Parent.pre (renamed into the child's parameter names). Parent.pre — NOT Child.pre: Child.pre is contravariantly weaker and assuming it would be unsound; Parent.pre ⇒ Child.pre is enforced separately by the pre-checker. Completeness fix (was over-rejection, never wrong-accept); the genuine-violation twin still fails even with Parent.pre assumed. Surfaced by rebasing onto a base that added ContractPass (strata-org#1352), which made `requires` clauses meaningful end-to-end and exposed this latent gap. 2 new corpus cases (liskov_post_covariance_under_parent_pre + its must-fail violation twin). Full lake test green (only pre-existing ion-java).

keyboardDrummer added 30 commits May 26, 2026 09:55

Improve Laurel printer

7e34b04

Introduce transparency pass

f246686

Fixes

b11e042

Refactoring

9e4ee85

Remove pack multiple outputs pass

7408103

Add error file

4e8fa8b

Update tests

2d19629

Add sources to lift phase

c9fd151

Update tests and improve errors

19987e8

Update comment

24c3983

Trigger CI

3c23531

Trigger CI

6046381

Trigger CI

86962e4

Replace panic with safe access

d192346

Move proof skipping logic from LaurelToCore translator to transparenc…

7a04e66

…y pass

Small refactoring

a45f8f0

Merge branch 'formatting-and-debugging-improvements' into transparenc…

96b2686

…y-pass-only

Cleanup

d0fdd35

Merge branch 'transparency-pass-only' of github.com:keyboardDrummer/S…

2e0d7e1

…trata into transparency-pass-only

Add contract pass

c62cfb4

Cleanup

a95da10

Fixes

49255b4

Fixes

10640f7

Do not run the contract pass for functions yet

8c15c16

Reduce id changes

573a36b

Fixes

74ec111

Test fixes

800f6c4

Fix test

e56cb20

Fix test

a352b47

Fix test

65c92f4

Merged via the queue into strata-org:reviewed-kbd-will-merge-to-main with commit 49c3e1a Jun 23, 2026
15 checks passed

fabiomadge mentioned this pull request Jun 26, 2026

ContractPass desugaring makes well-formed partial-op postconditions unprovable #1418

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Enable calling procedures in contracts#1352

Enable calling procedures in contracts#1352
keyboardDrummer merged 146 commits into
strata-org:reviewed-kbd-will-merge-to-mainfrom
keyboardDrummer:issue-924-contract-and-proof-pass

keyboardDrummer commented Jun 10, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Uh oh!

Conversation

keyboardDrummer commented Jun 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Functional changes

Why let the transparency pass rewrite the bodies of assume statements so they don't assert anything?

Implementation

Follow-up work

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

keyboardDrummer commented Jun 10, 2026 •

edited

Loading