feat(laurel): Seq<T> and Array<T> with bounds-checked subscript and diagnostics

[fabiomadge]

Adds Seq<T> (immutable value sequences) and Array<T> (mutable heap-backed arrays) to Laurel: type-aware desugaring to Core's polymorphic Sequence, bounds-checked subscript, type-checked index/element operands, validator diagnostics for common misuses, and a Sequence.fromArray snapshot operation.

Targets reviewed-kbd-will-merge-to-main. Rebased onto that branch after it advanced past the original branch point — most notably the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), and the HeapParameterization datatype-== fix (#1349). The earlier draft caveat about carrying a standalone copy of #1349 is obsolete: #1349 is already in the base, so the duplicate has collapsed.

Scope

Seq<T> (immutable values): Seq<T> types, [a, b, c] literals, s[i] read, s[i := v] functional update. Nine Sequence.* primitives (empty, build, select, update, length, append, contains, take, drop), declared in the Laurel prelude and backed by Core's polymorphic Sequence.

Array<T> (mutable, heap-backed; T = int only for now): Array<T> types, a[i] read, a[i] := v destructive write, Array.length(a), Sequence.fromArray(a) snapshot. Modeled by a synthetic $Array composite with a $data: Seq<int> field, injected only into programs that actually use Array<T>. Participates in modifies clauses.

Type checking

Because the feature was originally written against the pre-#1121 single-pass resolver, subscript typing is re-expressed in the new bidirectional Synth/Check architecture:

• Subscript rules (Synth.subscript, Check.subscriptWrite) check the index against TInt and the written/update value against the collection's element type, so a[0] := true on an Array<int> is rejected at the Laurel layer with a clear message. A concrete non-collection target (5[0]) is rejected (expected a sequence or array); a gradual Unknown/TCore target flows silently, mirroring how Fresh/ReferenceEquals treat non-reference targets.
• Polymorphic primitives. The Sequence.*/Array.* ops carry placeholder int signatures the strict checker would reject, so they ride the same structural-inference escape hatch as the existing select/update/const map primitives in Synth.staticCall: the result type is inferred from the arguments (e.g. Sequence.build(s, v) : Seq<typeof v>, so [1, 2, 3] : Seq<int>) rather than checked against the placeholders.
• Surface-vs-lowered consistency. Array<T> is a surface type whose declaration is never rewritten, while its value lowers to $Array (after SubscriptElim) then Composite (after TypeHierarchy). A narrow carve-out in isConsistent/isConsistentSubtype (LaurelAST.lean) keeps the surface and lowered forms interchangeable, plus an element-checked Seq<U> → Array<T> initialization rule (var a: Array<int> := [1, 2, 3]).

Bounds checking

Out-of-bounds access is a proof obligation, not a desugaring error. Sequence.select/update carry 0 ≤ i < length and take/drop carry 0 ≤ n ≤ length preconditions; the subscript sugar inherits them. Core's PrecondElim generates a VC at every call site — imperative code and pure positions (requires/ensures, quantifier/function bodies) alike — classified outOfBoundsAccess for SARIF, the same treatment as division by zero.

Validator diagnostics

ValidateSubscriptUsage flags misuses that are not expressible as a type error, before verification:

1. a[i := v] on Array<T> (functional update on a mutable array).
2. s[i] := v on Seq<T> (destructive write on an immutable sequence).
3. Array.length(x) on a non-Array<T>, plus wrong arity for Array.length/Sequence.fromArray.
4. Array<T> with T ≠ int (a Laurel-layer limitation, not SMT).
5. Sequence.fromArray(x) on a non-Array<T>.

The pipeline collects these alongside resolution errors; when a program already failed subscript validation, the post-pass StrataBug guard drops the expected downstream re-resolution noise rather than mislabeling it as a compiler bug.

Array<T> in datatypes

Supported. An array is a heap reference, so a datatype storing one compares by reference on that field (two values built from the same array are equal; from distinct arrays, not — even with equal contents). For value semantics, store a Seq<T> via Sequence.fromArray. (The HeapParameterization ==/!= fix this once carried standalone is now provided by #1349 in the base.)

Design notes

SubscriptWrite vs Subscript. Destructive write a[i] := v and functional update s[i := v] are distinct AST nodes (StmtExpr.SubscriptWrite vs StmtExpr.Subscript … (some v)), set by the grammar translator. An earlier revision shared one node disambiguated by syntactic position; that coupled SubscriptElim and ValidateSubscriptUsage and misclassified a functional update used directly as an if/while-branch value. The node split removes both the coupling and the bug.

BoxSeq per-element-type names. A composite with Seq fields of different element types collided under a single shared BoxSeq constructor. Fixed with a per-element-type tag (BoxSeq_int, BoxSeq_bool, …), matching the existing per-primitive BoxInt/BoxBool approach.

Out of scope

Array<T> for T ≠ int (diagnostic 4) — would need per-element-type $Array injection at the Laurel layer.

Tests & docs

Examples/Fundamentals/T24_Sequences, T25_Arrays, T26_MixedSeqFields, T27_ArrayInDatatype cover positive use (all operations, contracts, quantifiers, aliasing, loops, modifies, snapshot semantics, array/seq in datatypes with reference/value-equality contrast), one negative case per validator diagnostic (substring-pinned), negative cases for the new index/element type checks and non-collection-target rejection, and end-to-end out-of-bounds verification failures. SubscriptElimConstantsTest pins the constants-walk. docs/verso/LaurelDoc.lean documents the feature, the subscript typing rules, equality/aliasing semantics, and common mistakes.

[MikaelMayer]

🤖 Well-structured PR. The separation between ValidateSubscriptUsage (pure diagnostics) and SubscriptElim (rewriting) is clean, and the centralized SeqOp.* / arrayCompositeName constants prevent name drift between passes. The highTypeTag approach for per-element-type Box constructors is a good solution to the deduplication collision. The bounds-precondition infrastructure (mkSeqBoundsPrecond + classifyPrecondition) integrates naturally with the existing PrecondElim pattern.

A few items below.

[MikaelMayer]

🔍 LGTM — all comments addressed.

[MikaelMayer]

🔍 LGTM — all comments addressed. subscriptElim now maps elimExpr model over program.constants initializers, closing the gap I flagged. The subsequent refactoring and documentation commits look clean.

[MikaelMayer]

🔍 LGTM — all comments addressed. The new structural-recursion commit cleanly resolves the partial TODO by adding sizeOf lemmas and inlining the mutual helpers. Previous feedback (constants handling, _model docstring, arrayDataField separation) remains intact.

[MikaelMayer]

🔍 LGTM — all previous comments remain addressed. The new commit makes containsTArray, stmtExprUsesTArray, and validateHighType structurally recursive with proper termination_by/decreasing_by blocks, consistent with the prior commit's approach for the SubscriptElim walkers. The HighType.sizeOf_* lemmas in Laurel.lean follow the established pattern.

[MikaelMayer]

🔍 LGTM — all comments addressed. The new commit is a minor cleanup (anonymous have bindings in decreasing_by). All three original inline comments (constants handling, _model docstring, arrayDataField separation) remain properly addressed.

[MikaelMayer]

🤖🔍 LGTM — all comments addressed. The new commits add good deduplication (mkArrayUpdateStmt/mkArrayInitSplit helpers), exhaustive pattern matching in containsTArray/validateHighType, arity diagnostics, datatype-Array rejection, and comprehensive tests including the constants-walk coverage I originally flagged.

[MikaelMayer]

🤖🔍 LGTM — all comments addressed. The new elimStmtAt refactor cleanly centralises the four duplicated statement-position dispatch arms into a single mutual helper with proper lex termination. Original inline comments (constants handling, _model docstring, arrayDataField separation) remain intact.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[keyboardDrummer]

In this PR, arrays are translated using a translation to sequences. Have you considered defining Arrays using a library Laurel file?

[keyboardDrummer]

I think passes shouldn't refer to AST node types that don't relate to them. Instead, they use generic traversal code like what's in MapStmtExpr.lean

[fabiomadge]

Partly done.

Validator — done. The ~35-arm validateStmtExpr walker is gone, replaced by two generic collects over MapStmtExpr (mapProgramHighTypesM for types, mapStmtExpr for exprs); only Subscript/SubscriptWrite/StaticCall are named, so a new unrelated constructor needs no change.

elimExpr — proposing as a follow-up, because it's not a mechanical port:

1. It expands one statement into two (var a: Array<T> := … → alloc + $data store), spliced at Block/If/While. The 1→1 combinators can't express that; the new mapStmtExprFlattenM (1→N) does solve this splice part.
2. But mapStmtExprFlattenM is bottom-up, and elimExpr's Subscript arm must read computeExprType on the original target — a bottom-up port reads the already-rewritten child (a Sequence.select typed int) and diverges for nested array-of-array access (latent today only because Array<T> is int-only). So the port needs a top-down pre hook with manual child recursion, not a plain bottom-up map — tractable, but not a drop-in.

Happy to file elimExpr as a follow-up issue with these points.

[fabiomadge]

Have you considered defining Arrays using a library Laurel file?

Not seriously yet — and there's a real design space rather than one shape, so I'd like your read on which you mean:

• Composite over Seq — composite $Array<T> { $data: Seq<T> }, subscript still lowering to Sequence.*. This is essentially what's here already ($Array is exactly this with int hardcoded); a library version just moves the declaration out of Lean and lifts int→T. Reuses the Sequence axioms, bounds for free.
• Composite over a different backing — Map<int,T>, native SMT array — different element store, different solver characteristics.
• Axiomatize Array directly — declare its ops external with their own Core axioms (the way Sequence is defined in Factory.lean), no Seq indirection. The most first-class version, and the only one that meaningfully shrinks the current lowering.

Two constraints regardless: (1) int-only is a generics gap — the composite grammar takes a bare name, so lifting it is gated on something like #1394; (2) the subscript surface ops are type-directed, so some resolution-time lowering stays Lean-side even with a library type.

Since composite-over-Seq is ~the status quo, I suspect the real question is whether to axiomatize Array as its own thing. Fold into this PR, or follow-up?

[keyboardDrummer]

Is the addition of StrataTest/DDM/Integration/Java/testdata/ion-java-1.11.11.jar and the other one intentional? What about lsp.json ?

[keyboardDrummer]

Is this still useful? I would think the filter in let newErrors := result.errors.filter fun e => !resolutionErrors.contains e already achieves a similar thing. Does it not?

[fabiomadge]

Not redundant. The filter drops post-pass errors identical to existing ones; this flag handles new but expected errors, when a pass desugars already-invalid input into something that re-resolves differently. Tested both removals: deleting it → T25 breaks (Array<bool> desugars to a new error the filter lets through, mislabeled StrataBug); early-return on initial resolve error → T9 breaks (skips LiftInstanceProcedures). Its job — run the full pipeline on invalid input without relabeling the fallout as a bug — isn't covered by either.

[keyboardDrummer]

when a pass desugars already-invalid input into something that re-resolves differently.

How come the error changes? Isn't that a bug?

[fabiomadge]

Not a bug — expected when a pass desugars already-invalid input. Array<bool> is caught at the initial resolve; the passes still run, and SubscriptElim desugars the rejected program into a different re-resolve error (expected 'Seq<int>', got 'Seq<bool>'). The flag fires only when resolution already errored, labeling that as expected fallout rather than StrataBug.

We can't early-return on the resolve error, because the passes still need to run — e.g. LiftInstanceProcedures moves composite methods into staticProcedures; Core ignores anything left on the composite, so skipping it silently drops methods from verification (the "not lifted" check guards that). So the flag is what keeps invalid input from mislabeling the fallout.

[keyboardDrummer]

I would prefer a separate files for supporting Arrays and Sequences, since sequences don't depend on arrays and both are not insignificant features.

I think I'd be OK for now if Arrays don't support the dedicates subscript syntax, but rather require calls to static procedures. I know that will make the tests a little ugly but it means that Arrays can be defined fully as a library.

[fabiomadge]

On separate files: I prototyped two ways to split it, both passing the suite, both leaving the Seq module with no Array code references:

• (a) hook-seam — one elimExpr stays in SubscriptElim; array logic moves to a new ArrayElim.lean, called as hooks. One pass, one resolve.
• (b) two passes — ArrayElim becomes a separate pass running before SubscriptElim. Fully independent, but the two traversals are ~95% duplicated and array programs pay an extra resolve.

I lean (a). Which would you prefer? Happy to split it into its own PR.

[keyboardDrummer]

With (b), if we don't support the subscript syntax for Array, then we wouldn't need the extra pass right?

[fabiomadge]

Right in spirit — without a[i] sugar, arrays stop touching the shared .Subscript nodes, so there's no overlap to separate (they'd still need $Array injection + Array.length lowering, independently). I'd keep the syntax for now though. Of the two shapes I prototyped I lean (a) hook-seam — same separation, no duplicated traversal or extra resolve. Do it as a follow-up PR?

[keyboardDrummer]

okay, I get this now. I think this will be made obsolete by https://code.amazon.com/reviews/CR-285805099/revisions/1#/details, and that will probably land in GF before this lands there, so I suggest defer looking at this until then.

[fabiomadge]

Agreed it's interim — read CR-285805099, it supersedes this cleanly (clears the opaque ensures, asserts in-body via $post with input snapshotting for old), so it falls away once that lands. Leaving as-is to keep the Seq/Array tests green. That's on GF and this is the mirror, so they reconcile on sync — I'd still like your approval here so the branch isn't blocked on a stale review.