[Laurel] Support constrained types as composite fields

[olivier-aws]

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 Document Laurel passes and their dependencies, and other documentation updates #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.

[keyboardDrummer]

Nice!

[fabiomadge]

Already approved, but flagging a verified correctness bug — requesting changes. The feature is sound and deferring the read-side gap is fine (verified: genuine incompleteness, not unsoundness).

Field-write constraint check double-evaluates the RHS. The .Field arm at :222 asserts the constraint on value — the whole RHS expression — which has already been emitted as the field-write statement just above (:197), so any side effect in the RHS runs twice. Verified on this head, with count : nat and x starting at 0: c#count := (x := x + 1) + 1 leaves x == 2, not 1; the ConstrainedTypeElim output is literally c#count := (x:=x+1)+1; assert nat$constraint((x:=x+1)+1) — x:=x+1 appears twice, so x is incremented 0→2 instead of 0→1. A legal program gets the wrong state. Fix inline at :222: assert on a read-back of the field, not on value. With it, x == 1 holds (non-vacuous) and suite + proofs stay green once T11's two does not hold carets become could not be proved (the read-back reasons through a heap read). This is in the hand-written elimStmt traversal you flagged at :180 — though it's a double-emission rather than the catch-all incompleteness you mentioned. Notably the pass already has a constrainedTargetReadback helper (:133) that builds exactly this field read-back for expression-position assignments; the statement-level arm just doesn't use it.

Non-blocking — a smaller alternative. The bug, the new wrapExprAssigns, and the edit to the shared LiftImperativeExpressions all stem from moving ConstrainedTypeElim ahead of lifting. Keeping it last (as on main2) and instead resolving constrained field types to base inside HeapParameterization (box selection + Eq/Neq) reaches the same goal: I prototyped it at −79 lines, no shared-pass change, cleaner "does not hold" diagnostic, double-eval can't arise. I know #1356 argued heap-param shouldn't know about constrained types — resurfacing it only because that was decided before this bug and before I'd verified the alternative end-to-end. Your call, not a blocker.

Minor aside (no action). Eq/Neq ref-compares any .UserDefined _ operand without resolving constrained types. The reorder makes that safe here (verified: c#count == d#count lowers to an int compare), so it's an ordering invariant, not a live bug — but a one-line resolveBoxType there would make it order-independent.

[olivier-aws]

@keyboardDrummer-bot please fix conflicts