Enable calling procedures in contracts#1352
Merged
keyboardDrummer merged 146 commits intoJun 23, 2026
Merged
Conversation
…trata into transparency-pass-only
Contributor
|
Re-checked at Note: PR is |
fabiomadge
previously approved these changes
Jun 22, 2026
keyboardDrummer
commented
Jun 23, 2026
… into issue-924-contract-and-proof-pass
joscoh
approved these changes
Jun 23, 2026
robin-aws
approved these changes
Jun 23, 2026
Merged
via the queue into
strata-org:reviewed-kbd-will-merge-to-main
with commit Jun 23, 2026
49c3e1a
15 checks passed
fabiomadge
added a commit
to fabiomadge/Strata
that referenced
this pull request
Jun 26, 2026
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.
fabiomadge
added a commit
to fabiomadge/Strata
that referenced
this pull request
Jun 26, 2026
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).
fabiomadge
added a commit
that referenced
this pull request
Jun 26, 2026
…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.
fabiomadge
added a commit
that referenced
this pull request
Jun 30, 2026
…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.
fabiomadge
added a commit
that referenced
this pull request
Jun 30, 2026
…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.
fabiomadge
added a commit
that referenced
this pull request
Jun 30, 2026
…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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Functional changes
EliminateReturnsInExpressionnow 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.LaurelPassconcept 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 likeassume <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:
returntoexitstatements, needed for the next pass.Follow-up work