Skip to content

Enable calling procedures in contracts#28

Open
keyboardDrummer wants to merge 112 commits into
transparency-pass-onlyfrom
issue-924-contract-and-proof-pass
Open

Enable calling procedures in contracts#28
keyboardDrummer wants to merge 112 commits into
transparency-pass-onlyfrom
issue-924-contract-and-proof-pass

Conversation

@keyboardDrummer

@keyboardDrummer keyboardDrummer commented Apr 23, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

Builds on:

Functional changes

  1. [Debugging] Improvement the printing of Laurel if-then-else expressions
  2. EliminateReturnsInExpression now runs for procedures as well
  3. Refactoring of how Laurel function bodies are handled. The body is now immediately wrapped in a return statement during parsing.
  4. Allow calling procedures from contracts - making them strictly more powerful than functions
  5. Let the transparency pass rewrite the bodies of assume statements so they don't assert anything.
  6. Improve diagnostics related to contracts, using the correct verbiage "precondition" and "postcondition" instead of "assertion"

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.

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

@keyboardDrummer keyboardDrummer changed the title Issue 924 contract and proof pass Add contract and transparency pass Apr 23, 2026
@github-actions github-actions Bot added Git conflicts PR has merge conflicts with the base branch SMT GOTO dependencies github_actions and removed Git conflicts PR has merge conflicts with the base branch labels Apr 23, 2026
@keyboardDrummer keyboardDrummer mentioned this pull request Apr 23, 2026
Closed
@keyboardDrummer-bot keyboardDrummer-bot force-pushed the disallow-transparent-statement-bodies branch from 3a0f094 to df6ccdc Compare April 23, 2026 14:37
@keyboardDrummer keyboardDrummer mentioned this pull request Apr 27, 2026
Merged
@keyboardDrummer keyboardDrummer force-pushed the disallow-transparent-statement-bodies branch from 2e860cf to e3fe027 Compare April 29, 2026 08:44
keyboardDrummer-bot added a commit that referenced this pull request May 1, 2026
@keyboardDrummer-bot
Merge branch 'merge-1076-1077' into issue-924-contract-and-proof-pass
a549f5f 
Merges PR #31 (strata-org PRs strata-org#1076 and strata-org#1077) into this branch.

Key conflict resolution decisions:
- Removed AstNode.md field (from PR #28) in favor of PR #31's source-only approach
- Adapted ContractPass, TransparencyPass, EliminateReturnStatements to use 2-field AstNode
- Used diagnosticFromSource/identifierToCoreMd helpers from PR #31
- Kept PR #28's contract pass pipeline (transparencyPass, orderFunctionsAndProofs)
- Kept PR #28's translateMethod for Python class methods
- Kept PR #28's wildcard modifies filtering in HeapParameterization
- Took PR #31's modifiesClausesToArgs (handles multiple wildcards correctly)
- Took PR #31's buildSpecBody (adds postcondition support)
- Took PR #31's instance procedure diagnostics
- Kept PR #28's test expectations (contract pass changes error messages)
@github-actions github-actions Bot added GOTO and removed Java Git conflicts PR has merge conflicts with the base branch labels May 1, 2026
@keyboardDrummer keyboardDrummer force-pushed the disallow-transparent-statement-bodies branch from fd2988e to 5fb8577 Compare May 1, 2026 12:22
@keyboardDrummer keyboardDrummer changed the base branch from disallow-transparent-statement-bodies to merge-1076-1077 May 1, 2026 12:23
@github-actions github-actions Bot added Git conflicts PR has merge conflicts with the base branch and removed github_actions labels May 1, 2026
@keyboardDrummer keyboardDrummer changed the base branch from merge-1076-1077 to issue-21-assign-variable-type May 4, 2026 13:11
kadirayk and others added 30 commits June 16, 2026 10:23
@kadirayk
Per-invariant source ranges for loop-invariant diagnostics (strata-or…
24b8f04 
…g#1361)

## Summary

Loop-invariant verification diagnostics (a failing `invariant(...)` in a
`while`/`for` loop) previously pointed at the **whole loop** instead of
the specific invariant that failed. This change threads each invariant's
source range through the loop's metadata so loop elimination can
attribute each invariant's verification condition to that invariant's
own source location.

This support is required for
[JVerify#437](strata-org/jverify#437)

## Problem

In Strata, loop-invariant proof obligations are synthesized by
`LoopElim` and were tagged with the loop-wide metadata `md`. The
per-invariant source range was lost earlier in the pipeline: Core loop
invariants are bare `(label, expr)` pairs and Core expressions are
`Unit`-annotated, so they carry no source range.

A front-end-only change does not help: the diagnostic location is driven
by the synthesized assert's metadata, not by anything attached to the
invariant expression. The fix therefore has to live in Strata.

## Solution

Thread each invariant's source range through the loop's existing
`MetaData` array and use it per-invariant in `LoopElim`. When a
per-invariant provenance is present, each invariant's generated
assert/assume is attributed to that invariant's own source location;
otherwise we fall back to the loop metadata `md`, so loops not
originating from Laurel (Core `.st`, C_Simp) are unchanged.


## Testing

`StrataTest/.../Fundamentals/T13_WhileLoopsError.lean` adds two
caret-annotated regression tests using the existing diagnostic harness
(`TestDiagnostics`, `matchesDiagnostic`), which checks the exact
start/end line and column of each diagnostic:

1. **`badInitialInvariant`** — a single `invariant i >= 0` that fails on
entry. The caret asserts the diagnostic lands on the invariant
expression, not the `while` loop.
2. **`secondInvariantFails`** — two invariants where the first holds on
entry but the second (`invariant j >= 0`) does not. The caret asserts
the diagnostic points specifically at the failing second invariant. This
is the case that distinguishes per-invariant attribution from loop-wide
attribution: before the fix the range would resolve to the loop, so the
carets would not match.

Verification:

- `lake build Strata` — compiles, no proof breakage.
- `lake build StrataTest` — all `#guard_msgs` tests pass, including the
new ones.
- The fallback to the loop `md` keeps existing Core `.st` and C_Simp
loop diagnostics unchanged.
@keyboardDrummer
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main'…
d1f9d6c 
… into issue-924-contract-and-proof-pass
@keyboardDrummer
Fix test
0322796
@keyboardDrummer
Code review
878f325
@keyboardDrummer
Fix early return
e0c8b68
@keyboardDrummer
Fix lifting bug
a63384a
@keyboardDrummer
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main'…
02ad82c 
… into issue-924-contract-and-proof-pass
@AD1024 @olivier-aws
feat(laurel): Adding surface syntax for calling instance procedures &…
4d3cbac 
… lowering to Core (strata-org#1328)

## Summary

This PR addresses the problem that Laurel composite types could
*declare* instance procedures inside `composite { ... }` blocks, but
they couldn't be compiled or called. The Laurel→Core translator
unconditionally rejected every instance procedure with a
`NotYetImplemented` diagnostic, and even without that block they would
have been silently dropped: the SCC ordering in
[`CoreGroupingAndOrdering.lean`](Strata/Languages/Laurel/CoreGroupingAndOrdering.lean)
only enumerates `program.staticProcedures`, so anything on
`CompositeType.instanceProcedures` never reached Strata Core.

### 1. Surface syntax of instance procedure calls: `obj#method(args)`

- **Parser**
([`ConcreteToAbstractTreeTranslator.lean`](Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean)):
when the callee of `call(...)` is a `fieldAccess` node, emit
`InstanceCall target method args` instead of dropping the receiver into
an empty-string static call.
- **Grammar**
([`LaurelGrammar.st`](Strata/Languages/Laurel/Grammar/LaurelGrammar.st)):
adjust `call`'s precedence so `c#m(args)` parses as `call(fieldAccess(c,
m), args)`.
- **Resolution**
([`Resolution.lean`](Strata/Languages/Laurel/Resolution.lean)):
pre-register instance procedures in the global scope under their lifted
key (`<CompositeName>$<methodName>`). Two composites can now share a
method name without colliding (Note: this change seems to resolve strata-org#1321
but the the issue of the Resolver still exists - variable scope should
be carefully refactored for the resolution pass). `InstanceCall`
resolution looks up the receiver's composite type, builds the lifted
key, and stamps the resolved `uniqueId` on the original callee
identifier.

### 2. Laurel-to-Laurel pass: `LiftInstanceProcedures`

A new pass under
[`Strata/Languages/Laurel/LiftInstanceProcedures.lean`](Strata/Languages/Laurel/LiftInstanceProcedures.lean),
wired into
[`LaurelCompilationPipeline.lean`](Strata/Languages/Laurel/LaurelCompilationPipeline.lean)
with `needsResolves := true` between `EliminateValueReturns` and
`HeapParameterization`. The pass:

- Walks every `.Composite ct` in `program.types` and clones each `proc ∈
ct.instanceProcedures` into a fresh top-level static procedure named
`<CompositeName>$<methodName>`. Body, parameters, contracts, and
`invokeOn` are copied verbatim.
- Walks the entire program and rewrites every `InstanceCall` whose
callee so it points at the lifted name (with the receiver prepended as
the first argument to match the lifted procedure's `self :
<CompositeName>` parameter).
- Clears `ct.instanceProcedures := []` on every composite and appends
the lifted procedures to `program.staticProcedures`.

Downstream simplifications:
[`HeapParameterization.lean`](Strata/Languages/Laurel/HeapParameterization.lean)
drops its secondary traversal of `instanceProcedures` (now always
empty), and the `NotYetImplemented` block in
[`LaurelToCoreTranslator.lean`](Strata/Languages/Laurel/LaurelToCoreTranslator.lean)
is replaced by a defensive `StrataBug` assertion that fires only on a
pass-ordering regression (all instance procedures should already be
lifted and rewritten at this point).

---------

Co-authored-by: olivier-aws <obouisso@amazon.com>
@keyboardDrummer
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main'…
799f167 
… into issue-924-contract-and-proof-pass
@fabiomadge @ssomayyajula
fix(laurel): datatype ==/!= mis-lowered to reference comparison i…
0c99354 
…n heap-writing procedures (strata-org#1349)

## Summary

`HeapParameterization` rewrites `==`/`!=` on heap references into a
`Composite..ref!` reference comparison, gated on the operand type being
`.UserDefined _`. That pattern matches **both** composites (heap
references, where `ref!` is correct) **and** datatypes (values, where
`ref!` is wrong — it unifies a datatype value against `Composite`, which
is an `int` synonym).

## Symptom

The bug only surfaces inside a procedure that **writes the heap**,
because only then does the heap-rewriting pass descend into the body and
reach the equality arm. A datatype comparison sitting next to any heap
write (e.g. a `new C` allocation) fails Core type checking with:

```
Impossible to unify (arrow Composite int) with (arrow <Datatype> ...)
```

This is a latent, general correctness bug — it affects **any** datatype
`==`/`!=` in a heap-writing procedure, including a plain `datatype Pair
{ MkPair(a: int, b: int) }`. It is independent of any particular field
type.

## Fix

Guard the `ref!` rewrite on `!isDatatype` (using the existing
`isDatatype` helper) in both the `.Eq` and `.Neq` arms, so datatype
equality falls through to structural comparison. Composite
reference-equality semantics are unchanged.

## Tests

`StrataTest/Languages/Laurel/DatatypeEqHeapProcTest.lean` covers both
`==` and `!=` on a datatype inside a heap-writing procedure. Verified
both arms **fail Core type checking without the guard** and **verify
cleanly with it** (non-vacuous regression guard). Full `Strata` +
`StrataTest` build passes (554 jobs), no other regressions.

## Notes

Found while investigating `Array<T>` in datatype constructor arguments
(the Seq/Array PR strata-org#1073): allocating an `Array<T>` forces `writesHeap`,
which made this pre-existing bug reachable. This PR fixes the root cause
independently; the array-facing follow-up (lifting the validator gate,
flipping that test to positive) is left to strata-org#1073.

Co-authored-by: Siva Somayyajula <somayyas@amazon.com>
@keyboardDrummer
Port fixes to lifting pass
83e793b
@keyboardDrummer
Merge branch 'reviewed-kbd-will-merge-to-main' into issue-924-contrac…
6e0ce93 
…t-and-proof-pass
@keyboardDrummer-bot @leo-leesco
@claude @shigoel @atomb @tautschnig @kiro-agent @aqjune-aws @MikaelMayer @thanhnguyen-aws @fabiomadge @joehendrix @PROgram52bc @keyboardDrummer @sagjoshi
Add type checking to Laurel resolution pass (strata-org#1121)
9c40e44 
## Summary

Adds type checking to Laurel's `Resolution.lean` as requested in strata-org#1120.

## Changes

- **`resolveStmtExpr` now returns `ResolveM (StmtExprMd × HighTypeMd)`**
— both the resolved expression and its synthesized type.

- **Type checks added:**
  - Boolean conditions in `if`/`while`/`assert`/`assume` must be `TBool`
- Arithmetic/comparison operands must be numeric (`TInt`, `TReal`,
`TFloat64`)
- Logical operands (`And`, `Or`, `Not`, `Implies`, etc.) must be `TBool`
  - Static call argument types must match parameter types
- Instance call argument types must match parameter types (skipping
`self`)
  - Assignment value type must match target type (single-target only)
- Functional procedure body type must match declared output type
(transparent bodies only)

- **Diagnostics, not hard failures** — type mismatches are reported via
`ResolveState.errors` and compilation continues.

- **Cascading error prevention:**
  - `Unknown` types are compatible with everything
- `UserDefined` types skip strict assignability checks
(subtype/inheritance relationships are not tracked during resolution)
- `TVoid` types skip assignment/output checks (statements like
`return`/`while` don't produce values in the expression sense)
- `MultiValuedExpr` types skip assignability checks (arity mismatch
already reported separately)
- Kind-mismatched type references (e.g., using a variable name as a
type) produce `Unknown` to avoid cascading

- **`computeExprType` in `LaurelTypes.lean` is unchanged** — it
continues to work alongside the new type checking.

- **Callers updated** to use the returned type from `resolveStmtExpr`
(e.g., `resolveBody`, `resolveProcedure`, `resolveInstanceProcedure`,
`resolveConstant`, `resolveTypeDefinition`).

## Testing

All existing tests pass (`lake build StrataTest` — 592 jobs successful).

Closes strata-org#1120"

---------

Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Co-authored-by: Léo LEESCO <leo.leesco@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Léo Leesco <109468520+leo-leesco@users.noreply.github.com>
Co-authored-by: Shilpi Goel <shigoel@gmail.com>
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
Co-authored-by: Michael Tautschnig <mt@debian.org>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
Co-authored-by: thanhnguyen-aws <ntson@amazon.com>
Co-authored-by: Fabio Madge <fmadge@amazon.com>
Co-authored-by: Joe Hendrix <joehx@amazon.com>
Co-authored-by: June Lee <lebjuney@amazon.com>
Co-authored-by: David Deng <daviddenghaotian@gmail.com>
Co-authored-by: David Deng <htd@amazon.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Mikael Mayer <mimayere@amazon.com>
Co-authored-by: Remy Willems <rwillems@amazon.com>
Co-authored-by: Sagar Joshi <72283186+sagjoshi@users.noreply.github.com>
@keyboardDrummer
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main'…
e1fc044 
… into issue-924-contract-and-proof-pass
@keyboardDrummer
Some fixes for resolution during phases
dcfb0e9
@keyboardDrummer
Fixes to resolution so it throws fewer errors during passes
a0ec015
@keyboardDrummer
Emit resolution errors during passes
25f1d5d
@keyboardDrummer
Source fix
fa7f844
@keyboardDrummer
Improve well-formedness of the 3 heap passes
441ec1e
@keyboardDrummer
Fix for type hierarchy
cf706b2
@keyboardDrummer
Refactoring
66589c5
@keyboardDrummer
Allow dangling addition in blocks
903f89e
@keyboardDrummer
Fix diagnostic and test
1a0e8ae
@keyboardDrummer
Remove function return type expectation check
018939b
@keyboardDrummer
Update resolver check to use procedure instead of function
8d34b32
@keyboardDrummer
Small improvements
d9b39ac
@keyboardDrummer
Merge branch 'issue-924-contract-and-proof-pass' of github.com:keyboa…
a24cc86 
…rdDrummer/Strata into issue-924-contract-and-proof-pass
@keyboardDrummer
Merge branch 'fixResolutionErrorsDuringPhases' into issue-924-contrac…
c438d8c 
…t-and-proof-pass
@keyboardDrummer
Fix merge
fcb3903
@keyboardDrummer
Remove obsolete test
4efaebd
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@keyboardDrummer-bot keyboardDrummer-bot keyboardDrummer-bot left review comments

Assignees

No one assigned

Labels

Core github_actions GOTO Laurel Python SMT

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.