pyspec: native contract decorator recognition surface#1427
Open
julesmt wants to merge 71 commits into
Open
Conversation
*Issue #, if available:* *Description of changes:* Test PR for `main2` branch By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. Co-authored-by: Josh Cohen <cohenjo@amazon.com>
*Issue #, if available:* *Description of changes:* - Support `decreases <int expr>` termination measures alongside structural ADT recursion - Int-recursive functions are pure UFs (no definitional axioms); termination obligations assert non-negativity and strict decrease at each call site - Compound measures supported (e.g., `decreases m + n`) - Mixed structural/int-valued mutual blocks are rejected - New `inlineIfAllCanonical` attribute enables concrete evaluation of int-recursive functions Core logic in `Strata/Transform/TerminationCheck.lean` — new `DecreasesKind` type classifies each function's measure, unified obligation generation via callback. Tests in `StrataTest/Languages/Core/Tests/IntRecursionTests.lean` and `StrataTest/Languages/Core/Tests/RecursiveFunctionErrorTests.lean`. CC @kondylidou By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com>
Keeps `main2` in sync with `main` By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- 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: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com> Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com> Co-authored-by: Josh Cohen <cohenjo@amazon.com>
…plentations (#1160) Add a one-time pad example using three different methods for the array data structure: a map of ints, a linked list, and the new sequence type. The map version is verified with `gen_smt_vcs` and the two others with `#eval verify`. --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com> Co-authored-by: Josh Cohen <36058610+joscoh@users.noreply.github.com>
## Problem When a Boole program had 4+ datatype declarations and the **first** datatype's testers or selectors (e.g. `color..iscolor_Red`, `color..color_Red_0`) were referenced in a later function, the verifier reported them as free variables during type-checking. Moving the referenced datatype to any position other than first worked around the bug. Closes #1142 ## Root cause `initFVarIsOp` built a symbol-class table by scanning program commands — one entry per command (one `false` per `datatype` command). But the `GlobalContext` registers many entries per datatype: the type itself plus every constructor, tester, and selector generated by templates. This made `fvarIsOp` too short and misaligned with the actual `fvar` indices. When the referenced datatype was declared first, its testers/selectors landed at low `fvar` indices that fell inside the misaligned table. Those indices returned `false` (treat as type symbol), so the testers were emitted as `.fvar` (variable references) instead of `.op` (function applications). The type-checker then rejected them as undeclared free variables. When the datatype was not first, the tester indices fell past the end of the table and hit the fallback path in `getFVarIsOp`, which correctly reads `GlobalContext.vars[i]` — the same source of truth the DDM elaborator uses for all symbols. ## Fix Removed `fvarIsOp`, `initFVarIsOp`, and `registerCommandSymbols` entirely. `getFVarIsOp` now reads directly from `GlobalContext.vars[i]`: - `GlobalKind.type` → emit as `.fvar` (type symbol, not a callable) - `GlobalKind.expr` → emit as `.op`, **except** for `command_var` global variables, which become procedure parameters in Core and must remain `.fvar` The `command_var` carve-out uses the existing `globalVarTypes` map (already collected in the pre-pass), so no new state is needed. ## Test Added `StrataTest/Languages/Boole/datatype_tester_freevar.lean` — a direct regression for the issue's failing case: `color` declared first among four datatypes, with `get_val` referencing `color..iscolor_Red` and `color..color_Red_0`. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- 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: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com> Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
## Summary
Extends the Boole language pipeline with new language features, curated
benchmark
targets anchored to dalek-lite (Curve25519/Ed25519), and a testing
infrastructure
upgrade across all Boole seeds.
## Language features
**`Sequence T` type and slicing ops**
- `toCoreMonoType` handles `.Sequence _ elem → .tcons "Sequence" [elem]`
- All 8 Core inherited ops wired up in `Verify.lean`
- Three Boole-specific wrappers: `Sequence.skip`, `Sequence.dropFirst`,
`Sequence.subrange`
- Typed empty-sequence constants:
`Sequence.empty_bv8/bv16/bv32/bv64/int` — each
needs a distinct token since 0-ary polymorphic `Sequence.empty` has no
arguments
to infer the type from
**Bitvector loop variables** (`for i : bvN := init to limit`)
- `for_to_by` and `for_downto_by` dispatch guard/step/increment to
`Bv{N}.ULe/Add/Sub` when the loop variable is a bitvector type
**`decreases` annotations**
- `for v := init to/downto limit` accepts an optional `decreases e`
clause;
forwarded to the Core while-loop measure field and actively verified by
cvc5
- Functions and procedures accept an optional `decreases e` clause using
Core's
existing `Measure` category — no new grammar category introduced
- All three forms reuse Core's single `measure_mk` op; no duplicate
constructs
- Function termination is verified by #1092; procedure-level `decreases`
is
silently dropped with a `dbg_trace` warning pending int-based
termination support
**Lambda abstraction and application**
- `fun x : T => body` lowers to nested Core `.abs` nodes
- `(f)(x)` lowers to `.app () f x`
**Inline `let`-block postconditions**
- `let v := e in body` in spec/ensures positions lowers via
`withBVarExprs`
**`choose` assignment**
- `w := choose z : T :: pred(z)` lowers to `havoc w; assume pred[z/w]`
**Bitvector comparisons**
- Unsigned (`<`, `<=`, `>`, `>=`) default to `Bv{N}.ULt/ULe/UGt/UGe` via
`toBvCmpOp`
- Signed (`<s`, `<=s`, `>s`, `>=s`) lower to `Bv{N}.SLt/SLe/SGt/SGe`
## New seeds
- `embedded_postcondition.lean` — inline let-block in `ensures`
- `montgomery_loop_invariant.lean` — relational while-loop invariant;
linear
arithmetic case verifies via cvc5 and `smtVCsCorrect`
- `scalar_reduce.lean` — B2 `reduce()` axiom with abstract types
- `sha256_compact_indexed.lean` — SHA-256 compact port (indexed
`Sequence`
encoding); all 19 VCs pass; loop counters use `int` (faithful to Rust's
`usize`
semantics, avoids uninterpreted cast to `Sequence` index); remaining
gaps:
iterator protocol (#27), fixed-size array syntax (#25), slice types
(#26)
Fully implemented seeds graduated from `FeatureRequests/` to the main
Boole test
folder: `early_return.lean`, `choose_operator.lean`,
`bitvector_ops.lean`,
`embedded_postcondition.lean`.
## Seed test infrastructure
Replaced `#guard_msgs (drop info) in` with explicit `/-- info: ... -/` +
`#guard_msgs in` across all Boole seeds. Added `(options := .quiet)`
uniformly.
## Documentation
- New `docs/BooleBenchmarks.md`: five real-world benchmark targets from
dalek-lite
- Updated `docs/BooleFeatureRequests.md`: all new seeds in inventory
table,
implemented features extended
By submitting this pull request, I confirm that you can use, modify,
copy, and
redistribute this contribution, under the terms of your choice.
---------
Co-authored-by: Michael Tautschnig <mt@debian.org>
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
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: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Instead of running all the commands to build the verso docs, which quickly become repetitive on quick iterations of documentation building, I propose to chain the commands : 1. build the docs 2. serve via a python server (localhost) 3. open automatically
Regular merge of `main` into `main2`. --------- 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: keyboardDrummer-bot <keyboardDrummer-bot@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: Claude Opus 4.6 <noreply@anthropic.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: keyboardDrummer-bot <keyboarddrummer.bot@gmail.com> Co-authored-by: Josh Cohen <36058610+joscoh@users.noreply.github.com> Co-authored-by: Josh Cohen <cohenjo@amazon.com>
…#1220) Previously, the RHS of an `init` statement could involve uninitialized variables, which were implicitly nondetermistic and which were used to implement default expressions for `init`. Since #432 added an explicit `.nondet` initialization method, this workaround is no longer needed, and this PR removes that capability. The Boole -> Core translation used a similar method; this PR also changes it to use `.nondet`. Co-authored-by: Josh Cohen <cohenjo@amazon.com>
Fixes #1236 `translateFromDDMTermToUntyped` was missing a case for `sc_decimal_neg`, causing negative real-valued counter-examples (e.g. `-2.0`) to fall through to the catch-all error and be silently dropped from the parsed model. Added the missing case that negates the mantissa, mirroring the existing `sc_numeral_neg` pattern. Since all `SpecConstant` constructors are now exhaustively matched, the catch-all was removed and a comment documents the deliberate exhaustiveness so future reviewers don't re-add a defensive catch-all. Tested: all library and test modules compile successfully.
…1271) Fixes #1231 `translateFromTerm` threw on `Term.none` and `Term.some`, which caused `termToSMTString` to produce an error (or previously, via `panic!`, an empty body that solvers reject). This PR adds proper SMT-LIB encoding: - `Term.none ty` → `(as none (Option T))` - `Term.some inner` → `(some <inner>)` Tested: existing tests pass, new `#guard_msgs` tests added for both cases at the `termToString` and `termToSMTString` levels.
…#1217) Adds three cross-sort conversion operators to Core, as proposed in #1191. Split from the original PR per reviewer request — Core layer only. Boole surface syntax follows in a separate PR. ## Operators | Core name | SMT-LIB 2.7 | Lean | Direction | |-----------------|-------------------|-------------------|-----------------| | `Bv{n}.ToUInt` | `ubv_to_int` | `BitVec.toNat` | bv → int (unsigned) | | `Bv{n}.ToInt` | `sbv_to_int` | `BitVec.toInt` | bv → int (signed, two's complement) | | `Int.ToBv{n}` | `(_ int_to_bv n)` | `BitVec.ofInt n` | int → bv (mod 2^n) | Supported widths: 1, 8, 16, 32, 64, 128. All three are total — no preconditions, no Safe variants, no axioms. ## Changes - **CoreOp**: `BvOpKind.ToUInt`, `BvOpKind.ToInt` (unary, cross-sort); `CoreOp.intToBv n` - **Factory**: `bvToUIntFunc`, `bvToIntFunc`, `intToBvFunc` + per-width instances for all 6 widths; registered in `WFFactory` (factoryOps: 286 → 304) - **SMTEncoder**: maps `.bv ⟨_, .ToUInt⟩` → `ubv_to_int`, `.bv ⟨_, .ToInt⟩` → `sbv_to_int`, `.intToBv n` → `(_ int_to_bv n)` - **DL/SMT/Op**: `Op.BV.ubv_to_int`, `Op.BV.sbv_to_int`, `Op.BV.int_to_bv n` \+ `mkName` entries - **DL/SMT/Denote + Translate**: handle `ubv_to_int` / `sbv_to_int` / `int_to_bv` - **Core DDMTransform/Grammar + Translate**: `bv128` type + literal; `bv128 → .bitvec 128` - **Boole/Verify** (minimal): `bv128` cases in `typeRange`, `toCoreMonoType`, `bvWidth` — required because `bv128` enters `BooleDDM.BooleType` via the grammar change above - **Tests**: `ProgramEvalTests` (18 new func entries for all 3 ops × 6 widths), `StatisticsTest` (count bump) --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
…ns (indices discarded) (#1270) Fixes #1232 `resolveQI` was discarding the indices from `iden_indexed` identifiers, so solver-returned bitvec literals like `(_ bv5 32)` were decoded as UF applications (`mkUFApp "bv5" []`) instead of proper bitvec values. This extends `resolveQI` to preserve indices, then detects the `bv{N}` pattern with a numeral width index in `translateFromDDMTermToUntyped` to reconstruct the correct `.prim (.bitvec (BitVec.ofNat width value))`. Tested: existing tests pass, new round-trip decode tests added for bitvec literals.
Lower a `Sequence.of_<ty>[v0, ..., vn]` literal to a left-fold of `seq_build` over a typed `seq_empty`. The element type is required on the seed so that empty literals retain their type and the bounds-precondition pass does not emit polymorphic obligations. --------- Co-authored-by: David Deng <htd@amazon.com>
…mts` (#1265) Remove the dead `var_map.find?` lookup in `outputSetStmts`. The lookup always returned `.none` because `out_vars` already contains renamed identifiers (from `renameAllLocalNames`), while `var_map`'s keys are the original pre-rename identifiers. Also simplifies `renameAllLocalNames` to return `CoreTransformM Procedure` instead of a tuple, since `var_map` has no remaining consumers. No behaviour change. Existing tests pass. Fixes #1234
…e callers to `Maps.remove` (#1261) Fixes #1240 ## Summary `Maps.remove` was functionally identical to `Maps.erase` (both erase from every scope) despite its docstring claiming first-occurrence semantics. This PR deletes the duplicate and keeps `Maps.remove` as the canonical name, migrating all callers accordingly. ## Changes - Deleted the old `Maps.remove` (which had incorrect docstring) and its four supporting theorems - Renamed `Maps.erase` → `Maps.remove` (keeping the correct implementation) - Renamed all related theorems to use `remove` instead of `erase` (e.g. `Maps.keys_erase_subset` → `Maps.keys_remove_subset`) - Migrated all call sites ## Testing Full build passes, all existing tests pass.
… `findUnique` registry (#1250) Fixes #1230 ## Problem The SMT encoder emitted identifiers from multiple sites without a unified disambiguation registry. A user-defined UF named `f.N` could collide with the Nth `encodeFunction` output, and sort/datatype/constructor names flowed directly to the solver without being tracked, creating potential duplicate-declaration errors. ## Solution Every SMT-LIB identifier emitted by the encoder now routes through a unified `usedNames` registry in `EncoderState`: - **`Encoder.uniquify` helper** (batch path): Encapsulates the find-unique-and-register pattern (checks `usedNames` + SMT reserved keywords, disambiguates via `@N` suffix, registers the result). - **`AbstractEncoder.uniquify` helper** (incremental path): Same pattern lifted into the `AbstractEncoderState` monad, used by both `encodeUF` and `encodeFunction`. - **`smtReservedKeywordsSet`**: Pre-computed `HashSet` lifted to top-level, avoiding recomputation on every `uniquify` call. - **Sort/datatype/constructor/selector names**: Pre-populated into `EncoderState` via `SMT.Context.preDeclaredNames` (shared helper used by both `encodeCore` and `encodeDeclarationsAbstract`). Includes constructor names (`c.name.name`) and selector names (`d.name ++ ".." ++ fieldName.name`) for all seen datatypes, plus built-in Option names (`none`, `some`, `val`). - **Constructor names in `declareType`**: `declareType` uniquifies constructor names in addition to the type name. - **Quantifier-bound names**: `toSMTTerm` now includes sort and datatype names in its disambiguation set. - **`encode` standalone function**: Pre-populated with the `Option` datatype names. - **No `$__` prefix**: Generated base names are now plain `f.0`, `f.1`, ... for readability; uniqueness is enforced by the registry, not by naming conventions. ## Testing - All existing tests pass - New `#guard_msgs` unit tests verify collision avoidance for: - UF-vs-function name collisions - UF-vs-sort/datatype name collisions - Constructor disambiguation in `declareType` - Built-in `Option`/`none`/`some`/`val` collision - AbstractEncoder paths (`encodeUF`/`encodeFunction`) via mock solver
…1260) Fixes #1242 Fix typo in `SourceRange.fromIon`: the `asSexp` call used `"Source rang"` instead of `"Source range"`, producing a truncated error message on malformed input. The repeated `"Source range"` prefix is now hoisted into a local `let tag` binding to prevent the same class of typo from recurring. Tests added: - Error-path test asserting the error message starts with `"Source range"` - Success-path round-trip tests for both the null case and a valid sexp with start/stop values
…ter and produce duplicate labels (#1267) Fixes #1235 Unlabeled `cover` statements were reading the `assert_def` counter instead of `cover_def` for their default label generation. This caused consecutive unlabeled `cover` statements to produce duplicate `cover_0` labels when no asserts intervened. The fix uses the correct counter for each statement kind. The duplicated assert/cover translation pattern is extracted into a `translateLabeledCheck` helper. Tested: existing tests pass, new regression tests verify distinct labels for consecutive covers and independent counters across assert/cover combinations.
…ization (#1286) Fixes #1228 When deserializing Ion binary structs, NOP pads (type code 0 with length != 15) between fields caused subsequent field-key symbol indices to shift, because the field-key symbol ID was unconditionally pushed to the symbol stack even for NOP pads. The fix introduces a `TypeDesc.isNopPad` helper and uses it to skip pushing the field-key symbol for NOP pads, so subsequent fields retain their correct symbol indices. Tested with `#guard` tests covering NOP pad between fields and NOP pad at start of struct. Existing tests pass.
…ed input (#1263) Fixes #1238 Adds a `checkArgMin` bounds check before accessing `args[1]` in the `"indent"` case of `SyntaxDefAtom.fromIon`. Previously, a malformed sexp like `(indent)` with no second argument would crash with a panic. Now it returns a graceful error message. Also cleans up the neighbouring `"ident"` case by dropping panicking `!` indexing (the proof from `checkArgCount` already provides bounds), renames unused proof variables to `_`, and renames a shadowed `have p` to `have _h` for clarity. Tested: existing tests pass, `#guard_msgs` regression tests added covering the malformed indent path, successful empty tail, successful with inner atoms, and wrong-type-at-args[1] error path.
Fixes #1243 `elabDialectImportCommand` was pushing the import name into `dialect.imports` before attempting to load the dialect. When the load failed, the early `return` left the name in imports, causing downstream `addDialect!` panics with "Unknown dialect". The fix extracts a `getOrLoadDialect` helper that encapsulates the lookup-or-load logic (including error reporting and `missingImport` flag). `elabDialectImportCommand` is now a linear sequence: resolve the dialect, push to imports, open it — making the invariant that `dialect.imports` only contains successfully resolved dialects locally evident. Tested: existing tests pass, new test added that elaborates a dialect with a non-existent import, asserts the failed name is absent from `dialect.imports`, and exercises `openLoadedDialect!` on the result to confirm the previously-panicking path succeeds. --------- Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
…t" (#1296) Fixes #1295 Replaces the "path unreachable" outcome label with "unreachable in this context" in all user-facing verification output (outcome labels, diagnostic messages, and SARIF messages). The SARIF message no longer includes "path condition is contradictory" since unreachability can stem from reasons beyond the path condition. This is a wording-only change with no impact on proof obligations or SMT encoding. Tested: all existing tests pass with updated expected output.
…ctor name (#1264) Fixes #1237 The `checkArgCount` call in the `"decimal"` case of `ArgF.fromIon` was copy-pasted from the `"num"` case and still passed `"num"` as the constructor name. A malformed `decimal` sexp would produce an error saying "num expects 3 arguments" instead of "decimal expects 3 arguments". Fixed by passing `"decimal"` to `checkArgCount`. Added a test in `StrataTest/DDM/Ion.lean` that constructs a 4-element `decimal` sexp and verifies the error message starts with `"decimal"`. Filed #1294 to track a broader refactoring that would eliminate this class of copy-paste bug.
## Summary Extracts the formatting and debugging improvements from #34 into a standalone PR. ### Formatting improvements - **Block formatting**: Changes block output from single-line `{ stmt1; stmt2 }` to vertical layout with `indent(2)`: ``` { stmt1; stmt2 } ``` - **Semicolon separator**: Uses newlines instead of spaces between semicolon-separated items in the formatter. ### Debugging improvements - **Better diagnostic reporting**: Replaces the boolean `coreProgramHasSuperfluousErrors` with a `coreDiagnostics : List DiagnosticModel` that records *why* the Core program was suppressed. When no other diagnostics explain the suppression, these are surfaced to the user. - **Informative `invalidCoreType`**: Adds `source` and `reason` parameters so each suppression site provides context about what went wrong. - **Intermediate file output**: Adds `processLaurelFileKeepIntermediates` test helper that writes pipeline intermediate files to `Build/` for debugging. - **`.gitignore`**: Adds `Build/` directory. ### Test updates - All expected outputs updated to match the new block formatting. - Minor `#guard_msgs` whitespace fixes. - Some test inputs updated to use `opaque` keyword where needed for the new formatting to apply correctly. --------- Co-authored-by: Remy Willems <rwillems@amazon.com> Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
…amFromDialect (#1285) Fixes #1244 `parseStrataProgramFromDialect` in `Strata/DDM/Elab.lean` threw `IO.userError "Internal {dialect} missing from loaded dialects."` as a plain string literal, missing the `s!` prefix. The user saw the literal text `{dialect}` in the error message instead of the actual dialect name. This PR: - Adds the missing `s!` prefix to the original error message - Fixes 5 additional instances of the same bug across the codebase (in `panic!`, `throw`, and `dbg_trace` calls) - Adds a CI lint check (`.github/scripts/checkMissingInterpolation.sh`) that detects this class of bug going forward Tested with a new `#guard_msgs` test that triggers the error and asserts the interpolated value appears. Existing tests pass. The new CI lint check passes on the fixed codebase.
… loadDialectRec) (#1253) Fixes #1227 `loadDialectRec` accepted a `stk : Array DialectName` parameter for cycle detection but never checked it. Two dialect files with mutual imports (A imports B, B imports A) caused unbounded recursion / stack overflow. Now checks whether the dialect name is already on the stack before attempting to load, returning a clear "Circular import detected" error that renders the full cycle path (e.g. `A -> B -> C -> A`), making the offending edge obvious. Tested with integration tests covering: - 2-cycle (A ↔ B) - Self-import (A imports A) — caught by the existing `openDialectSet` check - 3-cycle (X → Y → Z → X) All existing tests pass.
…Map` iteration order (#1269) Fixes #1233 `DeclState.ofDialects` folds over `LoadedDialects.dialects.toList` to open all dialects. Since `DialectMap` wraps a `HashMap`, iteration order is non-deterministic. If a child dialect is visited before its parent, `addDialect!` opens the parent transitively, and then when the parent is visited directly, `openLoadedDialect!` panics because it's already open. The fix replaces `openLoadedDialect!` with `ensureLoaded!` in the fold. `ensureLoaded!` is idempotent — it returns immediately if the dialect is already open. Tested: existing tests pass, new regression test added that directly exercises `DeclState.ofDialects` and deterministically tests the idempotency of `ensureLoaded!` by simulating the problematic child-before-parent iteration order.
…pe for ≥3 distinct-type args (#1280) Fix local function declaration building wrong arrow type for ≥3 distinct-type args. The `funcDecl_statement` case in the Core translator used `mkArrow` with reversed inputs, producing incorrect type ordering (e.g. `int → real → bool → int` instead of `int → bool → real → int`) for local functions with 3+ parameters of distinct types. Replaced with `mkArrow'` which takes the input list in order, conforming to the Denote-layer pattern used in Assumptions.lean, CallOfLFuncDenote.lean, and Semantics.lean. Tested with a regression test that declares a local function `f(x:int, b:bool, r:real):int` and calls it, plus a `#guard` that directly verifies the `mkArrow'`/`destructArrow` roundtrip invariant. Existing tests pass. Fixes #1226
…peArgs (#1284) Fixes #1229 ## Problem `TEnv.addTypeAlias` had two defects: 1. **No chain resolution** — the RHS was stored without de-aliasing, so chained aliases (e.g., `BarAlias a := FooAlias a` where `FooAlias` is itself an alias) were never fully resolved. 2. **Internal type argument names** — stored `typeArgs` used `lhs.freeVars` (which produces internal `$__ty0`, `$__ty1` names) instead of the user-supplied names. ## Fix Replace the `instantiateEnv` + pattern-match logic with a direct call to `LMonoTy.resolveAliases` on the RHS before storing, and use `alias.typeArgs` directly. This maintains the invariant that stored alias types are never themselves aliases, and preserves user-supplied type argument names. ## Invariant theorems Two theorems in `LExprTypeSpec.lean` lock the invariants this PR establishes: - `TEnv.addTypeAlias_preserves_typeArgs` — fully proved; the stored alias retains the user-supplied `typeArgs` and `name`. - `TEnv.addTypeAlias_stored_dealiased` — states that the stored type is a fixpoint of `resolveAliases`. Proof reduced to idempotence of `resolveAliases` (remaining `sorry` to be completed in a follow-up). A helper `LMonoTy.resolveAliases_env` / `LMonoTys.resolveAliases_env` proves that `resolveAliases` preserves the full `TEnv` (stronger than context-only preservation). ## Testing - New `#guard_msgs` tests verify chained alias resolution and preserved `typeArgs`. - All existing tests pass. ## Related issues (separate PRs) - #1239 (reopened): arity mismatch error reporting - #1297 (new): typed `seqEmptyOp` in Boole sequence literals
Previously, we were using raw strings and manually routed them to be translated to `Strata.Program` Now, we use the DDM mechanism that creates a `Strata.Program` out of the box. This comes with several advantages : - we don't have to calculate character offsets manually anymore (for error reporting) - we get to leverage Lean's LSP integration for DSLs For formatting and other purposes, you can use `Strata.SourcedProgram` which is essentially `Strata.Program` with added metadata (line/col number, filename…). An automatic coercion is in place to strip metadata back into a `Strata.Program`. --------- Co-authored-by: Michael Tautschnig <mt@debian.org> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>
## Summary Split out of #1356, this PR contains **only the bitvector-related changes**. The constrained-types work from #1356 is being handled separately. Adds support for bitvector-typed fields in composite types, plus bitvector literal syntax in the Laurel grammar. ### Changes - **HeapParameterization**: add `.TBv n` cases to `boxConstructorName`, `boxDestructorName`, and `boxConstructorDef` so composite types can have bv-typed fields (boxed as `BoxBv{n}`, generated per width). - **Grammar**: add `bvLiteral(value, width)` operation with syntax `<value> bv <width>` (e.g. `100 bv 16`). - **AST**: add `LiteralBv (value width : Nat)` variant to `StmtExpr`. - **Parsing/formatting/translation/typing**: handle bv literals in `ConcreteToAbstractTreeTranslator`, `AbstractToConcreteTreeTranslator`, `LaurelToCoreTranslator` (-> Lambda `bitvecConst`), and type inference (`LiteralBv` has type `TBv width`). ### Tests - `T10_CompositeBvField`: covers writing/reading bv fields, bv literals, and an error case (postcondition violation when a bv field is not written / wrong literal value). - Verified with `lake build` of the affected Laurel modules and the T10 test (`#guard_msgs` passes).
Adds prefix and postfix increment/decrement operators to the Laurel
dialect, usable both as statements (`x++;`) and inside expressions (`int
y := (x++) + (x++);`).
Surface tokens `++` and `--` are reserved for the new operators by
renaming Laurel's string-concatenation operator from `++` to `^`
(OCaml-style). Existing tests using the old token are migrated.
Implementation:
* New `.IncrDecr` constructor on `StmtExpr` carrying mode (Pre/Post), op
(Incr/Decr) and an lvalue target (Local or Field).
* New `EliminateIncrDecr` pass, run first in the Laurel pipeline, lowers
IncrDecr to existing constructs:
Pre -> (target := target ± 1) (yields new value)
Post -> ((target := target ± 1) ∓ 1) (yields old value)
Statement-position IncrDecr lowers to a clean assignment without a
dead snapshot.
* Lift fix: `transformStmt` now lifts side effects out of expression-
statements (only when they contain an assignment / imperative call),
so postfix-as-statement reaches Core correctly.
* All exhaustive StmtExpr matches updated: MapStmtExpr, computeExprType,
Resolution.resolveStmtExpr / collectStmtExpr, FilterPrelude, lift
helpers, and both grammar tree translators.
Tests:
* StrataTest/Languages/Laurel/IncrDecrLiftTest.lean — exact lowering of
stmt form, prefix, and postfix.
* StrataTest/Languages/Laurel/Examples/Fundamentals/T23_IncrDecr.lean —
10 verification procedures covering Java semantics: prefix yields new,
postfix yields old, (x++)+(x++), (++x)+(++x), mixed pre/post, pre/post
decrement, postfix in for-loop step, intentional failing assert.
A design plan accompanying this change is at
docs/LaurelIncrDecrPlan.md.
**Warning:** This repository will shortly undergo a split into several
separate repositories. If you're creating a PR that crosses the
boundaries between these repositories, you may want to hold off until
the split is complete or be prepared to rework your PR into multiple PRs
once the split is complete.
The code that will be moved includes:
- Strata/DDM/*
- Strata/Languages/Boole/*
- Strata/Languages/Python/* along with Tools/Python/*
- Tools/BoogieToStrata
## 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.
… lowering to Core (#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 #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>
…n heap-writing procedures (#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 #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 #1073. Co-authored-by: Siva Somayyajula <somayyas@amazon.com>
## Summary Adds type checking to Laurel's `Resolution.lean` as requested in #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 #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>
…#1381) EliminateValueInReturns only folded over program.staticProcedures, so a value-returning instance method with a body (using `return expr`) was never rewritten into `outParam := expr; return`. Updated the order of passes to run the `LiftInstanceProcedure` pass before `EliminateValueInReturns`. Add T9_ValueReturningInstanceMethods.lean: 9 positive cases (field/ computed/parameterized returns, conditional/early returns, modifies + return, bool return, shared method names, chained receiver, local var) and 2 negative cases pinning the no-output and multiple-output valued return diagnostics, proving the pass now reaches instance procedures. **Warning:** This repository will shortly undergo a split into several separate repositories. If you're creating a PR that crosses the boundaries between these repositories, you may want to hold off until the split is complete or be prepared to rework your PR into multiple PRs once the split is complete. The code that will be moved includes: - Strata/DDM/* - Strata/Languages/Boole/* - Strata/Languages/Python/* along with Tools/Python/* - Tools/BoogieToStrata
The last testing framework update regressed the error reporting to be tested-snippet-relative, but that is inconvenient. So whenever we flag an error now, it is relative to the entire file (easier to jump to) --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
### Changes - Report resolution errors that occur after transformation passes during the compilation of Laurel to Core. This change triggers errors in existing tests that lead to the remainder of the changes in this PR. - Remove `.THeap` and `.TTypedField`. The usages have been replaced by `.UserDefinedType "Heap"` and `.UserDefinedType "Field"`, so that all references to the heap type use that form, preventing type equality errors. - Only re-resolve after HeapParam, TypeInference and ModifiesClauses passes all complete, since they are part of the same logical pass. In the future, we should refactor so they're actually one pass, but still three components, since TypeHierarchy and ModifiesClauses are features that built on top of Composite types. - Replace all reference types with `Composite` during the TypeInference pass. This also enables a slight simplification of LaurelToCoreTranslator. - Correct a source location usage in the lifting pass. Without this change, the reported location for an error would change, and this is detected during re-resolution. - In `Resolution.lean`, synth instead of void-check non-last block elements. This is required because some passes create non-void non-last block elements. In particular the `EliminateIncrDecr` pass creates them. This change also means that `Resolution.lean` no longer needs to special-case checking `| .StaticCall .. | .InstanceCall .. | .IncrDecr `. - Because of the previous change, `Resolution.lean` needs to support synthing for any StmtExpr, which it now does. - In the resolver, add special casing for calls to select/update/const. These are polymorphic procedures which we can't type check without special casing yet, since we don't support polymorphism yet. - Remove expecting the body of a function to correspond to its result type. This check failed for more complicated functions from `T3_ControlFlow` after they were lowered by some passes. Note that function will be removed entirely. In the test related to this removed check, I have changed the function into a procedure and the same diagnostic is reported then, although through a different mechanism. - Refactor TypeAliasElim so it uses a generic traversal to update types. This generic traversal was added a part of changes to TypeHierarchy ### Testing Added one test, but mostly this PR relies on the existing tests. --------- Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
laurel: wire old() to Core two-state semantics Modifies-clause frame conditions now flow through Core's `old`-prefixed identifiers via Core's native two-state semantics, replacing the previous synthetic `$heap_in` parameter. 1. HeapParameterization: heap-writing procedures take `$heap` as a true inout parameter (same name in inputs and outputs) rather than a `$heap_in` / `$heap` pair with a synthesized assignment prelude. 2. ModifiesClauses: frame condition references `old($heap)` via `StmtExpr.Old` instead of a separate `$heap_in` variable. 3. New PushOldInward Laurel-to-Laurel pass: distributes `StmtExpr.Old` through its sub-expressions until each `Old` immediately wraps a Local Var. Warns if `old(...)` does not mention any inout parameter. 4. LaurelToCoreTranslator: `Old (Var (Local n))` translates directly to `fvar (mkOld n)`. Inout parameters at call sites are detected and emit `.inoutArg` rather than paired `.inArg` + `.outArg`. Call-arg construction is shared between the two StaticCall sites via a new buildCallArgs helper. Tests: T9_OldHeapTwoState drives the feature end-to-end — `old` of heap field reads, arithmetic/unary/comparison sub-expressions, `old(old(...))`, `old` inside quantifiers and if-then-else, multiple modifies/ensures, modifies-wildcard, wrong-body negative cases, the no-inout warning, and a caller asserting the post-state. PushOldInward's normalization shape (every `Old` wraps an inout Local Var) is enforced at translate time in LaurelToCoreTranslator: the `.Old` arm emits a `StrataBug` diagnostic if the invariant is ever violated. --------- Co-authored-by: Jules <julesmt@amazon.com> Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@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: Claude Opus 4.6 <noreply@anthropic.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: keyboardDrummer-bot <keyboarddrummer.bot@gmail.com> Co-authored-by: Sagar Joshi <72283186+sagjoshi@users.noreply.github.com>
…1401) With the new testing framework, we were correctly locating file-wide any uncaught diagnostic, but if an annotation was not matched (when we were over-expecting errors, or the error has changed), the annotation was located snippet-relative instead of file-relative. --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Fixes #1390. **Problem:** `Program.eval` threads one `Env` through all procedures. A structured `exit` out of a labeled block doesn't pop its path-condition frames (`.block` exit pops `exprEnv.state`, not `pathConditions`; the exiting path bypasses `Env.merge`), so a procedure's preconditions/assumptions leak into later procedures. A contradictory leaked set then makes the next procedure prove false obligations vacuously — silent unsound pass. Laurel lowers non-final `return` to `exit "$body"`, so ordinary early-return code hits it. **Fix:** reset `pathConditions` to the pre-procedure state in the `.proc` fold (deferred obligations and fresh names carry forward). A `.block`-level reset was rejected — breaks fall-through. **Test:** `ProcedurePathConditionIsolation` — unsatisfiable-precondition `first` + structured `exit`, `second`'s `assert false` must fail. Red without the fix, green with it; full `StrataTest` green (539). Control matrix + scope in #1390.
Laurel had only a pre-test `while`. This adds a `doWhile` grammar op and
a body-tested `do … while` loop. Rather than a separate AST node, a
do-while is represented as a post-test `While` — the existing `While`
constructor gains a `postTest : Bool := false` field — and is lowered in
a new `EliminateDoWhile` Laurel-to-Laurel pass into the existing
pre-test loop:
```
do S while(G) invariant I
```
becomes
```
{ while(true) invariant I { S; if (!G) { exit L } } } L
```
`L` is a fresh, collision-free label (`$dowhile_exit_{n}`, `$`-prefixed
so it can't collide with user identifiers), so nested do-whiles and user
`break`/`continue` don't capture each other's exits. The body runs once
per iteration with the guard re-checked after it, and the real guard
reaches post-loop code via the structured `exit` — so the encoding is
sound, complete, and linear (single body in the IR, no
peeling/duplication).
Invariant placement is head-tested (checked before each body), matching
`while`. **Gotcha (documented in T23):** because the guard is re-tested
only after the body, the invariant must hold of the *pre-body* state, so
`do { x:=x+1 } while(x<3)` needs the bound `x <= 2`, not `x <= 3`.
**Why a flag + a pass:** `postTest` captures the while/do-while
distinction at the type level (per review feedback) rather than
duplicating the loop as a second constructor — so most passes match
`While` once and carry the flag through, with no `.DoWhile` arms.
`postTest := false` (pre-test) is the default, so every existing
`.While` construction is unchanged. The desugaring lives in
`EliminateDoWhile` rather than in `ConcreteToAbstractTreeTranslator`, so
it runs for every program reaching the pipeline — including one supplied
directly as abstract AST, bypassing the concrete translator. The parser
builds a post-test `While`; the serializer emits `while`/`doWhile` by
the flag; the pass (modeled on `EliminateIncrDecr`, with its own
fresh-label counter) does the desugar and runs first, so no later pass
observes `postTest = true`. No new Core construct or `LoopElim` change —
the desugar reuses the existing verified pre-test loop machinery.
Resolution handles `postTest` in `Check.while` directly (it runs before
the passes, the same arrangement as `IncrDecr`).
The per-program traversal over static and composite-instance procedures,
which both `EliminateDoWhile` and `EliminateIncrDecr` had hand-rolled,
is now `mapProgramProceduresM` in `MapStmtExpr` (per review feedback) —
so neither pass refers to unrelated features like instance procedures.
Tests in `T23_DoWhile` (end-to-end): basic, runs-at-least-once (guard
false at entry), nested, break-out via labelled block, no-invariant
(zero `invariant` clauses — asserts the negated guard, the only fact
provable without an invariant), and `falsePostRejected` (a false
postcondition is rejected, confirming the `while(true)` desugar isn't
vacuous). Plus `EliminateDoWhileTest` (pass-output shape, incl. distinct
fresh labels for nested loops) and a round-trip case in
`AbstractToConcreteTreeTranslatorTest` (serialization arg order).
**Earlier label-clash warning, now resolved.** Multi-procedure `T23`
used to surface a latent label clash (`⚠️ [addPathCondition] Label clash
detected for assume_invariant_0_0, …`) — `do-while` was just the first
construct to trip it, because path-condition labels weren't reset
between procedures. This branch has merged the base fix #1391
(path-condition isolation at the procedure boundary), so the warning is
gone (verified: zero clashes on the T23 build). Not caused by this PR.
**Strata half only.** To use do-while end-to-end, the jverify front-end
must emit the new op (regenerate the `laurel/` bindings and add a
`JCDoWhileLoop` case to `JavaToLaurelCompiler`, which currently rejects
do-while) — a separate follow-up. Implements the front-end desugar from
#1350.
…overage (#1382) Two field-access improvements on the single `fieldAccess` grammar op, plus test coverage that closes out #1371. Note: the chained-field-access *capability* (`a#b#c` parsing, resolution, and heap elimination) already landed via #1328. This PR adds the one missing ergonomic piece, hardens the chained-access machinery with the tests it was missing, and a small refactor. **Grammar — paren-free field `++`/`--`.** `fieldAccess` precedence is raised 90 → 95. At 90 it tied with the postfix `++`/`--` ops (also 90), forcing `(c#n)++`; at 95 it binds tighter, so `c#n++` parses paren-free as `(c#n)++`. (`leftassoc`, already present from #1328, is unchanged.) Note the new precedence is shared with `call` (also 95, via its `callee:89`) — the two must stay equal or `a#b(x)` parsing shifts; documented at the op. **Resolution — refactor only.** The duplicated type-scope field lookup in `targetTypeName` and `incrDecrTargetType` is factored into a shared `fieldTypeInScope` helper. No behavior change. (This helper is also a dependency of the stacked compound-assignment PR.) **Tests — fill the chained-access coverage gap.** #1328 shipped chained access with only a read-side smoke test (no assertions). This adds: - `T9_ChainedFieldAccess`: chained **write** (`o#inner#count := …`), read-after-inner-assign, must-alias, depth-3 (`a#mid#inner#count`), chained reads on both sides of `==`, and paren-free chained `o#inner#count++` (the one test that exercises this PR's grammar change), plus three **negative** tests (unconstrained read, two-object may-alias, write isolation) that pin the encoding as non-vacuous and frame-sound. - `T23b_IncrDecrField`: paren-free single-level field `++`/`--`. Full `lake build` and `lake test` pass.
## Summary
Adds support for **constrained types as composite fields** in Laurel —
e.g. a composite with a field of a refinement type:
```
constrained nat = x: int where x >= 0 witness 0
composite Counter { var count: nat }
```
Field writes now check the constraint (`c#count := -1` fails), and the
field is boxed as its base type on the heap.
## ConstrainedTypeElim changes made along the way
Supporting this cleanly required running `ConstrainedTypeElim`
**earlier** in the Laurel pipeline (right after `typeAliasElim`, before
`HeapParameterization`) so that constrained field types are lowered to
their base types before the heap-boxing pass needs them. Moving the pass
forward exposed a few places where it had implicitly relied on running
last, which this PR fixes:
1. **Composite field types** — `ConstrainedTypeElim` removed the
constrained type definitions but left `UserDefined "nat"` references
inside composite fields, which then failed to resolve in Core
translation. `elimCompositeType` now resolves constrained field types to
their base types (and runs elimination on instance procedures) before
the definitions are removed. The field-write constraint check
(previously enabled by `HeapParameterization` via a `Declare` temporary)
is now emitted directly from the `.Field` assignment target.
2. **Constrained-typed assignments in expression position** — `elimStmt`
only checked assignments that appear as statements, so `y := (x := -1) +
1` with `x : nat` was unchecked. `wrapExprAssigns` now traverses
expression positions and wraps such assignments as `{ x := v; assert
T$constraint(x); x }`, asserting on a read-back so the RHS is evaluated
exactly once (semantics-preserving).
3. **`LiftExpressionAssignments` assert ordering** — for the read-back
form to work, the assert must stay *after* the assignment through
lowering. `transformExpr` was prepending `.Assert`/`.Assume` in
expression-position blocks only after the assignment had already been
prepended, moving them ahead of it (so they checked the stale value).
`transformExpr` now lifts `.Assert`/`.Assume` during its traversal so
they keep their position relative to assignments lifted from the same
block. This is a general correctness fix for the lifting pass.
4. **Cleanup** — once `ConstrainedTypeElim` runs first,
`HeapParameterization` no longer needs its own constrained-type
resolution (the field types reaching it are already base types), so the
dead `resolveConstrainedType` helper and the shared
`resolveConstrainedTypeWith` helper in `LaurelAST` were removed. Also
included the offending type name in the `LaurelToCoreTranslator` "could
not be resolved" diagnostic.
## Pipeline placement
`constrainedTypeElimPass` is moved to the second position (after
`typeAliasElimPass`). It has no `comesBefore` ordering constraints and
nothing depends on it running late, so the load-time
`comesBeforeRespected` check still holds.
## Notes
- Bitvector-as-composite-field changes that previously sat on this
branch have been removed; they live in a separate branch/PR. This PR is
scoped to constrained types.
- Rebased onto the latest `main2` (which includes the #1222
pipeline-framework refactor).
## Testing
- Full `lake build` passes (495 jobs, including all `#guard_msgs`
elaboration-time tests and the load-time pipeline-ordering check).
- `T11_ConstrainedField` covers constrained composite fields
(valid/invalid writes + a documented read-side completeness gap).
- `T10_ConstrainedTypes` gains a `sideEffect` case exercising an
assignment-in-expression to a constrained local.
---------
Co-authored-by: Remy Willems <rwillems@amazon.com>
Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
## 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>
Under `--use-array-theory`, a `modifies` clause naming only individual object references is now encoded as a single **quantifier-free heap equation** instead of a `∀`-quantified frame, so the solver discharges it by array rewriting instead of instantiating a quantifier per object/field. ∀ obj, fld. obj ≠ c ⇒ readField(old,obj,fld) == readField(new,obj,fld) -- before data(new) == store(data(old), c, select(data(new), c)) -- now The `∀` frame is unchanged for set-valued/empty `modifies` and when array theory is off, so default behavior is untouched. --------- 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: keyboardDrummer-bot <keyboardDrummer-bot@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: Claude Opus 4.6 <noreply@anthropic.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: keyboardDrummer-bot <keyboarddrummer.bot@gmail.com> Co-authored-by: Sagar Joshi <72283186+sagjoshi@users.noreply.github.com> Co-authored-by: Jules <julesmt@amazon.com>
Extract PySpecMClass into Specs/Diagnostics.lean to break the import cycle, then add Specs/Decorators.lean: a reusable decorator-recognition framework (DecoratorForm/ofExpr? normalizing the 4 surface shapes, lambda/kwarg helpers, and the decline-is-noop DecoratorScheme). Pure library gearing with no pipeline wiring yet; consumed later by the recognition layer.
Stacked on the decorator-framework branch. Recognizes PySpec's native, unqualified contract decorators on stub declarations, translates their lambda bodies into the spec data model, and round-trips them through DDM. Recognition + round-trip only; enforcement/lowering to Laurel/Core is deferred. Decorators: @requires, @ensures, @Modifies, @snapshot, @ghost (per-method) and @invariant (per-class). Bodies are translated to SpecExpr via the same transExpr path used by `assert`, stored on new FunctionDecl/ClassDef fields, and round-tripped via the DDM serializer. - Specs/Native.lean: DecoratorScheme-based recognizers (method + class) built on the framework; RawGhost/RawSnapshot bundles; uniform specError diagnostics - Specs/Decls.lean: Snapshot/Ghost structs; new FunctionDecl/ClassDef fields; SpecExpr.containsPlaceholder - Specs/DDM.lean: snapshot/ghost/modifies/invariant categories + toDDM/fromDDM - Specs.lean: transExpr .Attribute case scoped via allowFieldAccess (on for the not-yet-lowered targets, off for @requires/@ensures and asserts); contract-body translation helpers (runNoWarn + a deep containsPlaceholder drop); class-invariant translation - Specs/Decorators.lean: extends the framework with functionParamNames, exprKeyword?, hasKeyword, and an extra-positional-arg warning in expectLambda? Tests (StrataPythonTestExtra): content assertions over the recognized SpecExprs, negative/error tests, a DDM serde round-trip, and field-access boundary tests across 18 native_cases fixtures. Verified: lake build StrataPython (228 jobs), StrataPythonTestExtra (245), StrataPythonTest (239); all with zero warnings.
github-actions
Bot
added
Waiting-For-Review
Git conflicts
Laurel
Core
GOTO
dependencies
julesmt
changed the title
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
18 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.
Stacked on
pyspec/decorator-framework(review/merge that first).Recognizes PySpec's native contract decorators on stub declarations and
translates their lambda bodies into the spec data model, with a full DDM
round-trip. Recognition + round-trip only — enforcement/lowering to Laurel/Core
is deferred.
Decorators:
@requires,@ensures,@modifies,@snapshot,@ghost(per-method) and
@invariant(per-class). Bodies are translated toSpecExprvia the same
transExprpath used byassert, stored on newFunctionDecl/ClassDeffields, and round-tripped through the DDM serializer.