Add getIonDeserializer% and getIonSerializer% elaborators for generic Ion serialization - #1095
Closed
keyboardDrummer-bot wants to merge 86 commits into
Closed
Add getIonDeserializer% and getIonSerializer% elaborators for generic Ion serialization#1095keyboardDrummer-bot wants to merge 86 commits into
getIonDeserializer% and getIonSerializer% elaborators for generic Ion serialization#1095keyboardDrummer-bot wants to merge 86 commits into
Conversation
Implements a term-level elaborator that inspects Lean inductive and structure types at compile time and generates a ByteArray → Except Std.Format α deserializer. Encoding conventions: - Structures → Ion structs with field names as keys - Single-constructor inductives → Ion structs with _0, _1, … keys - Multi-constructor inductives → Ion sexps (CtorName arg1 arg2 …) - Supported leaf types: Nat, Int, String, Bool Closes #5
- Add readFloat runtime helper (accepts Ion float and int values) - Add Float as a supported leaf type in mkFieldRead and mkIndexRead - Support nested types: fields that are structures/inductives generate readers via let rec bindings in dependency order - Support recursive types: self-referencing types work when the enclosing definition is marked partial - Add tests for Float (Measurement), nested (Line with Point fields), and recursive (Tree) types
- Rewrite Strata/DDM/Integration/Java/Gen.lean to generate Java source
files from Lean types instead of DDM Dialect values
- New getIonSerializer% term elaborator inspects Lean inductive/structure
types at compile time and generates:
- Sealed interfaces for multi-constructor inductives
- Records for structures and single-constructor inductives
- Ion serialization matching getIonDeserializer% format:
- Structures → Ion struct with field name keys
- Single-ctor inductives → Ion struct with _0, _1, ... keys
- Multi-ctor inductives → Ion sexp (CtorName arg1 arg2 ...)
- Supported leaf types: Nat, Int, Float, String, Bool
- Nested and recursive types supported automatically
- Remove old javaGen CLI command from StrataMain.lean
- Rewrite tests to use Lean types (Point, Color, Shape, Person, Line, Tree)
- Add Java compilation test and Ion roundtrip test
(Java serializes → Lean deserializes → verify match)
# Conflicts: # StrataMain.lean # StrataTestExtra/DDM/Integration/Java/TestGen.lean # StrataTestExtra/DDM/Integration/Java/regenerate-testdata.sh
…rializer - Add readDecimal, readList, readOption runtime helpers to IonDeserializer - Extend getIonDeserializer% to handle List α, Option α, and Strata.Decimal - Extend getIonSerializer% to generate Java code for List (java.util.List), Option (nullable), and Decimal (java.math.BigDecimal) - Move old DDM-based Java generator to GenDDM.lean to preserve javaGen CLI - Remove support for MetaData, MetaDataElem, Core.Expression, and Array (no longer in Laurel AST) - Add tests for new types in StrataTest/Util/IonDeserializer.lean
The javac invocation was inside the HashMap iteration loop, causing it to compile partial sets of files. With non-deterministic HashMap ordering, this could fail when a file referencing another type was compiled before that type's source file was written. Also added the output directory to -cp so javac can find compiled classes from other files in the same package, and added cleanup at the end.
The CheckImports linter requires all modules under Strata/ to be transitively imported by Strata.lean. The new IonDeserializer module was missing from the import list, causing the lint step to fail in CI.
*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.
…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>
GenDDM.lean and the DDM-based Java code generator are no longer needed now that getIonSerializer% generates Java directly from Lean types. Removed: - Strata/DDM/Integration/Java/GenDDM.lean - Strata/DDM/Integration/Java/templates/ (IonSerializer.java, Node.java, SourceRange.java) - StrataTestExtra/DDM/Integration/Java/testdata/GenerateTestData.java - StrataTestExtra/DDM/Integration/Java/testdata/comprehensive.ion - StrataTestExtra/DDM/Integration/Java/testdata/comprehensive-files.ion - StrataTestExtra/DDM/Integration/Java/testdata/Simple.dialect.st - StrataTestExtra/DDM/Integration/Java/regenerate-testdata.sh - The javaGen CLI command (used GenDDM) - The 'Verify Java testdata is up to date' CI step
# Conflicts: # .github/workflows/ci.yml # StrataDDM/StrataDDM/Integration/Java/Gen.lean # StrataDDM/StrataDDM/Integration/Java/templates/IonSerializer.java # StrataDDM/StrataDDM/Integration/Java/templates/Node.java # StrataDDM/StrataDDM/Integration/Java/templates/SourceRange.java # StrataMain.lean # StrataTestExtra/Languages/Java/TestGen.lean # StrataTestExtra/Languages/Java/regenerate-testdata.sh # StrataTestExtra/Languages/Java/testdata/GenerateTestData.java # StrataTestExtra/Languages/Java/testdata/Simple.dialect.st # StrataTestExtra/Languages/Java/testdata/comprehensive-files.ion # StrataTestExtra/Languages/Java/testdata/comprehensive.ion
Adds a new executable 'laurelJavaGen' that uses getIonSerializer% on Strata.Laurel.Program to generate Java source files for the Laurel AST. Usage: lake exe laurelJavaGen <package> <output-dir> This replaces the old 'strata javaGen' CLI command which generated Java from the DDM grammar. The new approach generates from the Lean types directly, producing the getIonSerializer% format (records with toIon methods) instead of the old DDM format (Node interface, IonSerializer class, builder methods). Needed by: strata-org/jverify#405
- LaurelJavaGen.lean: use string literal for package arg (syntax requires str, not ident) - Gen.lean/extractCtorFields: use instantiate1 instead of manually stripping binders, fixing 'loose bvar' panic when processing parametric types like AstNode - Gen.lean/collectNestedTypes: same fix for nested type discovery - Gen.lean/extractCompoundNamesFromExpr: recurse into type arguments to discover compound types nested in parametric wrappers (e.g., StmtExpr inside AstNode StmtExpr)
- Type parameters (e.g., the 't' in AstNode(t : Type)) now generate a ToIon interface type instead of Object, with proper toIon serialization. - Fields with default values (optParam/autoParam wrappers like postTest : Bool := false) are now correctly recognized by stripping the optParam wrapper before type classification. - All generated types implement a new ToIon interface, enabling type-erased serialization of parametric fields. Fixes: AstNode.val becoming Object/newNull, While.postTest, PrimitiveOp.skipProof, and Hole.deterministic becoming Object/newNull.
…endent tests gracefully
AstNode(t : Type) now generates: public record AstNode<T extends ToIon>(T val, FileRange source) Use sites like AstNode HighType generate AstNode<HighType>. Implementation: - Track type params via tagged level markers in Sort exprs - extractCtorFields returns param names alongside fields - classifyFieldType detects tagged sorts and returns .typeParam with name - javaTypeForInfo renders compound types with generic args - TypeShape carries typeParams for generating <T extends ToIon> decls
…ermination - Rename local FieldInfo to JavaFieldInfo to avoid conflict with Lean.Elab.FieldInfo from opened namespaces - Remove default values from FieldTypeInfo inductive constructors (kernel rejects optParam on nested Array occurrences) - Fix String.drop returning String.Slice by adding .toString - Replace mapM closure with for loop to allow let-mut mutation - Add partial to javaTypeForInfo for mutual recursion termination
…izer - Fix getCtorFieldTypes to use instantiate1 when stripping type params, preventing loose bvar PANICs in whnf - Fix extractCompoundExprs to recurse into type arguments of compound types (e.g., AstNode StmtExpr → discovers both AstNode and StmtExpr) - Fix collectNestedTypeExprs to properly substitute type params when traversing constructor fields - Switch from nested let-rec to a single mutual let-rec block, fixing mutual recursion between parametric and non-parametric types - Use canonical string-based type keys for reliable expression hashing - Use whnf exclusively for type classification (fixes abbrev types like HighTypeMd) - Add exprToTypeSyntax helper for rendering applied types in annotations - Add deserializeLaurelProgram using getIonDeserializer% Laurel.Program - Update readLaurelIonProgram to try new struct format first with DDM fallback
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
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.
Closes #5
Summary
Adds two term-level elaborators for generic Ion serialization/deserialization of Lean types:
getIonDeserializer%— generates a functionByteArray → Except Std.Format αthat deserializes Ion binary data into values of a given Lean type at compile time.getIonSerializer%— generates Java source files (records, sealed interfaces) withtoIonmethods that serialize to the same Ion format.Design
Since
Typeis erased at runtime in Lean, both elaborators inspect the type's constructors and fields in the Lean environment at elaboration time and produce syntax that is then type-checked normally.Ion encoding conventions
_0,_1, …(ConstructorName arg₁ arg₂ …)Supported leaf types
Nat,Int,Float,String,Bool,DecimalContainer types
List α→ Ion list /java.util.List<T>,Option α→ Ion null for none / nullableTNested and recursive types
Fields whose types are themselves structures or inductives are handled recursively. For recursive types (e.g.,
Tree), the generated code useslet recbindings — the enclosing definition must be markedpartial.Usage
Files
Strata/Util/IonDeserializer.lean— Runtime helpers and thegetIonDeserializer%elaboratorStrata/DDM/Integration/Java/Gen.lean— Rewritten to providegetIonSerializer%for Lean typesStrata/DDM/Integration/Java/GenDDM.lean— Original DDM-based Java generator (preserved forjavaGenCLI)StrataTest/Util/IonDeserializer.lean— Tests for the deserializerStrataTestExtra/DDM/Integration/Java/TestGen.lean— Rewritten tests for the serializerTesting
javacand produces Ion data thatgetIonDeserializer%can read back correctly.