From 11230b01194e00faa5cc9c3d48c3ecc195e37173 Mon Sep 17 00:00:00 2001
From: Massart <julesmt@amazon.com>
Date: Fri, 12 Jun 2026 10:50:32 -0700
Subject: [PATCH 1/8] Factor native operator typing out of Synth.primitiveOp

Synth.primitiveOp inlined two match arms -- one for the arithmetic operators,
one for the boolean / comparison / equality / concatenation families. Extract
them into standalone nativeArith and nativeOther helpers (with an isArithmeticOp
predicate and a joinAll LUB fold), and have Synth.primitiveOp resolve its
operands once and dispatch to them.

Pure refactor, no behavior change. Gives the native typing rules a single home
so a later commit can reuse them as the fallback for gradual elaboration.
---
 Strata/Languages/Laurel/Resolution.lean | 201 ++++++++++++------------
 1 file changed, 101 insertions(+), 100 deletions(-)

diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index a3e3e5090d..6a6a62bc66 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -560,6 +560,101 @@ private def checkIncrDecrTargetType (op : IncrDecrOp) (target : VariableMd)
            Use an explicit assignment instead, e.g. 'x := x + 1'."
       modify fun s => { s with errors := s.errors.push diag }
 
+/-- Test whether `op` is in the arithmetic family. -/
+private def isArithmeticOp : Operation → Bool
+  | .Neg | .Add | .Sub | .Mul | .Div | .Mod | .DivT | .ModT => true
+  | _ => false
+
+/-- LUB of the operand types, or `none` if inconsistent. -/
+private def joinAll (ctx : TypeLattice) (argTypes : List HighTypeMd)
+    (source : Option FileRange) : Option HighTypeMd :=
+  argTypes.foldl
+    (fun acc t => match acc with | some l => join ctx l t | none => none)
+    (some { val := .Unknown, source := source })
+
+/-- A `MultiValuedExpr` operand is a multi-output call (`multi(x)` declared
+    `returns (a, b)`) used in value position. It is an internal pseudo-type with
+    no Core lowering, so it must never reach an operator slot — letting it
+    through crashes a later pass as a `StrataBug`. Emit the position-oriented
+    diagnostic for the offending operand and return `true` so the caller
+    short-circuits to the operator's natural result type, suppressing the
+    per-family check (and its cascading error) on that operand. -/
+private def reportMultiValued (a : StmtExprMd) (aTy : HighTypeMd) : ResolveM Bool := do
+  match aTy.val with
+  | .MultiValuedExpr _ =>
+    let diag := diagnosticFromSource a.source
+      "multi-output call cannot be used as a value here; it returns multiple values. Unpack it into separate variables first"
+    modify fun s => { s with errors := s.errors.push diag }
+    pure true
+  | _ => pure false
+
+/-- Native arithmetic typing: every operand must be numeric, and the result is
+    the LUB of the operand types under the consistency relation. A multi-valued
+    operand short-circuits to `Unknown` (arithmetic's natural
+    cascade-suppression type). -/
+private def nativeArith (op : Operation) (expr : StmtExpr) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (skipProof : Bool) (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let unknownTy : HighTypeMd := { val := .Unknown, source := source }
+  let mut hasMulti := false
+  for (a, aTy) in args'.zip argTypes do
+    if (← reportMultiValued a aTy) then hasMulti := true
+  if hasMulti then
+    return (.PrimitiveOp op args' skipProof, unknownTy)
+  let ctx := (← get).typeLattice
+  for (a, aTy) in args'.zip argTypes do
+    unless isNumeric ctx aTy do
+      typeMismatch a.source (some expr) "expected a numeric type" aTy
+  match joinAll ctx argTypes source with
+  | some ty => pure (.PrimitiveOp op args' skipProof, ty)
+  | none =>
+    let formatted := ", ".intercalate (argTypes.map (fun t => s!"'{formatType t}'"))
+    let diag := diagnosticFromSource source s!"cannot apply '{op}' to operands of types {formatted}"
+    modify fun s => { s with errors := s.errors.push diag }
+    pure (.PrimitiveOp op args' skipProof, unknownTy)
+
+/-- Native typing for the boolean / comparison / equality / string-concat
+    families: a fixed result type (`TBool` / `TString`) with the family's operand
+    constraint (booleans subtype `TBool`, comparisons are numeric, equality is
+    consistent, concat operands subtype `TString`). A multi-valued operand
+    short-circuits to the family's natural result type. -/
+private def nativeOther (op : Operation) (expr : StmtExpr) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (skipProof : Bool) (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let resultTy := match op with
+    | .Eq | .Neq | .And | .Or | .AndThen | .OrElse | .Not | .Implies
+    | .Lt | .Leq | .Gt | .Geq => HighType.TBool
+    | .StrConcat => HighType.TString
+    | _ => HighType.Unknown
+  let mut hasMulti := false
+  for (a, aTy) in args'.zip argTypes do
+    if (← reportMultiValued a aTy) then hasMulti := true
+  if hasMulti then
+    return (.PrimitiveOp op args' skipProof, { val := resultTy, source := source })
+  match op with
+  | .And | .Or | .AndThen | .OrElse | .Not | .Implies =>
+    for (a, aTy) in args'.zip argTypes do
+      checkSubtype a.source { val := .TBool, source := a.source } aTy
+  | .Lt | .Leq | .Gt | .Geq =>
+    let ctx := (← get).typeLattice
+    for (a, aTy) in args'.zip argTypes do
+      unless isNumeric ctx aTy do
+        typeMismatch a.source (some expr) "expected a numeric type" aTy
+  | .Eq | .Neq =>
+    match argTypes with
+    | [lhsTy, rhsTy] =>
+      let ctx := (← get).typeLattice
+      unless isConsistent ctx lhsTy rhsTy do
+        let diag := diagnosticFromSource source
+          s!"cannot compare '{formatType lhsTy}' with '{formatType rhsTy}' using '{op}'"
+        modify fun s => { s with errors := s.errors.push diag }
+    | _ => pure ()
+  | .StrConcat =>
+    for (a, aTy) in args'.zip argTypes do
+      checkSubtype a.source { val := .TString, source := a.source } aTy
+  | _ => pure ()
+  pure (.PrimitiveOp op args' skipProof, { val := resultTy, source := source })
+
 /-! ## Typing rules
 
 The judgment is bidirectional:
@@ -1850,106 +1945,12 @@ def Synth.primitiveOp (exprMd : StmtExprMd) (expr : StmtExpr)
     (h : exprMd.val = .PrimitiveOp op args skipProof) :
     ResolveM (StmtExpr × HighTypeMd) := do
   let _ := h_expr  -- carries the constructor identity for `expr` in diagnostics
-  -- Guard (all operator families): a `MultiValuedExpr` operand is a
-  -- multi-output call (`multi(x)` declared `returns (a, b)`) used in value
-  -- position. It is an internal pseudo-type with no Core lowering, so it must
-  -- never reach an operator slot — letting it through crashes a later pass as
-  -- a `StrataBug`. Emit the position-oriented diagnostic per offending operand
-  -- and return `true` so the caller short-circuits to the operator's natural
-  -- result type, suppressing the per-family check (and its cascading error)
-  -- on that operand.
-  let reportMultiValued (a : StmtExprMd) (aTy : HighTypeMd) : ResolveM Bool := do
-    match aTy.val with
-    | .MultiValuedExpr _ =>
-      let diag := diagnosticFromSource a.source
-        "multi-output call cannot be used as a value here; it returns multiple values. Unpack it into separate variables first"
-      modify fun s => { s with errors := s.errors.push diag }
-      pure true
-    | _ => pure false
-  match op with
-  -- Arithmetic: synth each operand's type, then take the join under
-  -- the consistency relation. This is the same discipline as
-  -- `Op-Eq`: operands must be pairwise consistent (with `Unknown`
-  -- promoting to whichever side is more informative). Each operand
-  -- is also required to be numeric.
-  | .Neg | .Add | .Sub | .Mul | .Div | .Mod | .DivT | .ModT =>
-    let results ← args.attach.mapM (fun a => have := a.property; do
-      Synth.resolveStmtExpr a.val)
-    let args' := results.map (·.1)
-    let argTypes := results.map (·.2)
-    let unknownTy : HighTypeMd := { val := .Unknown, source := source }
-    -- Multi-output operand guard: short-circuit to `Unknown` (arithmetic's
-    -- natural cascade-suppression type) once any operand is multi-valued.
-    let mut hasMulti := false
-    for (a, aTy) in args'.zip argTypes do
-      if (← reportMultiValued a aTy) then hasMulti := true
-    if hasMulti then
-      return (.PrimitiveOp op args' skipProof, unknownTy)
-    let ctx := (← get).typeLattice
-    -- Per-operand numeric check: surface the bad operand directly.
-    for (a, aTy) in args'.zip argTypes do
-      unless isNumeric ctx aTy do
-        typeMismatch a.source (some expr) "expected a numeric type" aTy
-    -- Fold operands by join, starting from `Unknown` so the
-    -- empty list (impossible for these ops, but kept for totality)
-    -- yields `Unknown` and a single-operand fold (`Neg`) yields the
-    -- operand's type.
-    let resultTy := argTypes.foldl
-      (fun acc aTy =>
-        match acc with
-        | some acc => join ctx acc aTy
-        | none => none)
-      (some unknownTy)
-    match resultTy with
-    | some ty => pure (.PrimitiveOp op args' skipProof, ty)
-    | none =>
-      let formatted := ", ".intercalate (argTypes.map (fun t => s!"'{formatType t}'"))
-      let diag := diagnosticFromSource source
-        s!"cannot apply '{op}' to operands of types {formatted}"
-      modify fun s => { s with errors := s.errors.push diag }
-      pure (.PrimitiveOp op args' skipProof, unknownTy)
-  | _ =>
-    let results ← args.attach.mapM (fun a => have := a.property; do
-      Synth.resolveStmtExpr a.val)
-    let args' := results.map (·.1)
-    let argTypes := results.map (·.2)
-    let resultTy := match op with
-      | .Eq | .Neq | .And | .Or | .AndThen | .OrElse | .Not | .Implies
-      | .Lt | .Leq | .Gt | .Geq => HighType.TBool
-      | .StrConcat => HighType.TString
-      -- Unreachable: filtered above.
-      | _ => HighType.Unknown
-    -- Multi-output operand guard: short-circuit to the operator's natural
-    -- result type (`TBool` for bool/cmp/eq, `TString` for concat) once any
-    -- operand is multi-valued, suppressing the per-family check below.
-    let mut hasMulti := false
-    for (a, aTy) in args'.zip argTypes do
-      if (← reportMultiValued a aTy) then hasMulti := true
-    if hasMulti then
-      return (.PrimitiveOp op args' skipProof, { val := resultTy, source := source })
-    match op with
-    | .And | .Or | .AndThen | .OrElse | .Not | .Implies =>
-      for (a, aTy) in args'.zip argTypes do
-        checkSubtype a.source { val := .TBool, source := a.source } aTy
-    | .Lt | .Leq | .Gt | .Geq =>
-      let ctx := (← get).typeLattice
-      for (a, aTy) in args'.zip argTypes do
-        unless isNumeric ctx aTy do
-          typeMismatch a.source (some expr) "expected a numeric type" aTy
-    | .Eq | .Neq =>
-      match argTypes with
-      | [lhsTy, rhsTy] =>
-        let ctx := (← get).typeLattice
-        unless isConsistent ctx lhsTy rhsTy do
-          let diag := diagnosticFromSource source
-            s!"cannot compare '{formatType lhsTy}' with '{formatType rhsTy}' using '{op}'"
-          modify fun s => { s with errors := s.errors.push diag }
-      | _ => pure ()
-    | .StrConcat =>
-      for (a, aTy) in args'.zip argTypes do
-        checkSubtype a.source { val := .TString, source := a.source } aTy
-    | _ => pure ()  -- unreachable
-    pure (.PrimitiveOp op args' skipProof, { val := resultTy, source := source })
+  let results ← args.attach.mapM (fun a => have := a.property; do
+    Synth.resolveStmtExpr a.val)
+  let args' := results.map (·.1)
+  let argTypes := results.map (·.2)
+  if isArithmeticOp op then nativeArith op expr args' argTypes skipProof source
+  else nativeOther op expr args' argTypes skipProof source
   termination_by (exprMd, 1)
   decreasing_by
     all_goals

From 9cbb15be8521b1f326c47eb0dbbf5f7c1882802b Mon Sep 17 00:00:00 2001
From: Massart <julesmt@amazon.com>
Date: Fri, 12 Jun 2026 10:52:56 -0700
Subject: [PATCH 2/8] Report datatype-constructor parameter types from
 getCallInfo

For datatype constructors, getCallInfo returned an empty parameter-type list, so
constructor arguments were never checked against their declared types. Return
ctor.args.map (.type) so a constructor call is type-checked like any other call.

No behavior change for existing programs (their arguments already matched); this
lets a later commit coerce constructor arguments under gradual typing.
---
 Strata/Languages/Laurel/Resolution.lean       |  6 +++--
 .../Laurel/ResolutionTypeCheckTests.lean      | 27 +++++++++++++++++++
 2 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 6a6a62bc66..14dc13ffee 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -468,12 +468,14 @@ private def getCallInfo (callee : Identifier) : ResolveM (HighTypeMd × List Hig
       | [singleOutput] => singleOutput.type
       | outputs => { val := .MultiValuedExpr (outputs.map (·.type)), source := none }
     pure (retTy, proc.inputs.map (·.type))
-  | some (_, .datatypeConstructor t _) =>
+  | some (_, .datatypeConstructor t ctor) =>
     -- Testers (e.g. "Color..isRed") return Bool; constructors return the type
+    -- and carry their declared argument types so call-site checking (and
+    -- gradual boxing) applies to constructor arguments.
     if (callee.text.splitOn "..is").length > 1 then
       pure ({ val := .TBool, source := callee.source }, [])
     else
-      pure ({ val := .UserDefined t, source := callee.source }, [])
+      pure ({ val := .UserDefined t, source := callee.source }, ctor.args.map (·.type))
   | some (_, .parameter p) => pure (p.type, [])
   | some (_, .constant c) => pure (c.type, [])
   | _ => pure ({ val := .Unknown, source := callee.source }, [])
diff --git a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
index e3888db451..df658dbbbc 100644
--- a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
+++ b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
@@ -389,3 +389,30 @@ procedure useUndef() opaque {
   var y: int := x + 2
 };
 #end
+
+/-! ## Datatype-constructor argument type checks
+
+Constructor arguments are now type-checked against the declared parameter types,
+so `Wrap(true)` for `Wrap(v: int)` is rejected (it was silently accepted before). -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+datatype Box { Wrap(v: int) }
+function foo(): Box {
+  Wrap(true)
+//     ^^^^ error: expected 'int', got 'bool'
+};
+#end
+
+/-! A correctly-typed constructor call still resolves cleanly (no
+over-rejection): `Wrap(1)` matches the declared `int` field. -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+datatype Box { Wrap(v: int) }
+function foo(): Box {
+  Wrap(1)
+};
+#end

From 32c4d7c47d9d47c36b5788214f5211ee9f18cb81 Mon Sep 17 00:00:00 2001
From: Massart <julesmt@amazon.com>
Date: Sat, 13 Jun 2026 18:46:21 -0700
Subject: [PATCH 3/8] Add gradual-typing elaboration to resolution

Add an optional GradualConfig (a frontend's dynamic type, its boxing
constructors, checked downcast accessors, per-operator prelude functions, and
which procedures to elaborate). A gradualActive flag, set only inside a
frontend's own procedures, gates a single dispatch in Synth.primitiveOp: when
active, route operands through synthArith / synthOther, which keep a native
operator when the operands are native and switch to the Any-prelude operator
(inserting box / unbox / Any_to_bool coercions at boundaries), falling back to
the native nativeArith / nativeOther rules; when inactive the native rules apply
unchanged. Inert until a frontend supplies a config.
---
 Strata/Languages/Laurel/Resolution.lean       | 428 ++++++++++++++----
 .../Laurel/GradualResolutionTests.lean        | 263 +++++++++++
 2 files changed, 595 insertions(+), 96 deletions(-)
 create mode 100644 StrataTest/Languages/Laurel/GradualResolutionTests.lean

diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 14dc13ffee..e5e358e778 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -136,8 +136,34 @@ abbrev Scope := Std.HashMap String ScopeEntry
 /-- Per-composite-type scope mapping field names to their scope entries. -/
 abbrev TypeScopes := Std.HashMap String Scope
 
+/-- Frontend-supplied gradual-typing prelude. When present, resolution rewrites
+    operations on `dynamic` operands to the named prelude operators and
+    materializes the implicit box/unbox/`toBool` casts at boundaries. All names
+    must already be in scope; `none` ⇒ no elaboration. -/
+structure GradualConfig where
+  /-- The dynamic type whose values are boxed (`TCore "Any"` for Python). -/
+  dynamic : HighType
+  /-- Whether a type is the dynamic type (may have several spellings). -/
+  isDynamic : HighType → Bool
+  /-- Box constructor name for a primitive type (e.g. `TInt ↦ "from_int"`). -/
+  box : HighType → Option String
+  /-- Unbox destructor name for a primitive type (e.g. `TInt ↦ "Any..as_int!"`). -/
+  unbox : HighType → Option String
+  /-- Coercion of a dynamic value to `bool` for condition positions. -/
+  toBool : String
+  /-- Dynamic prelude operator backing a native `Operation` (e.g. `Add ↦ "PAdd"`). -/
+  opPrelude : Operation → Option String
+  /-- Whether a procedure (by name) should be elaborated. Restricts elaboration
+      to frontend (user) code, leaving hand-written prelude bodies untouched. -/
+  shouldElaborate : String → Bool
+
 /-- State threaded through the resolution pass. -/
 structure ResolveState where
+  /-- Gradual-typing elaboration config, if the frontend requested it. -/
+  gradual : Option GradualConfig := none
+  /-- Whether gradual elaboration is active for the procedure being resolved.
+      Set per-procedure by `resolveProcedure` so only user code is elaborated. -/
+  gradualActive : Bool := false
   /-- Next fresh ID to allocate. -/
   nextId : Nat := 1
   /-- Current lexical scope (name → definition ID). -/
@@ -562,10 +588,172 @@ private def checkIncrDecrTargetType (op : IncrDecrOp) (target : VariableMd)
            Use an explicit assignment instead, e.g. 'x := x + 1'."
       modify fun s => { s with errors := s.errors.push diag }
 
-/-- Test whether `op` is in the arithmetic family. -/
-private def isArithmeticOp : Operation → Bool
-  | .Neg | .Add | .Sub | .Mul | .Div | .Mod | .DivT | .ModT => true
-  | _ => false
+/-! ## Typing rules
+
+The judgment is bidirectional:
+
+```
+Γ ⊢ e ⇒ A          (Synth.resolveStmtExpr)
+Γ ⊢ e ⇐ A          (Check.resolveStmtExpr)
+```
+
+- `Γ` — lexical scope (variables, fields). Block labels live in a
+  separate namespace `Γ_lbl` (`ResolveState.labelScope`), consulted
+  only by `Check.exit`.
+- `A` — *value type* of the term.
+
+The `Return` rules additionally depend on the enclosing procedure's
+declared output-type list, written `T_o-bar` in the rule statements.
+That list is bound on entry to a procedure body (by
+`resolveProcedure` / `resolveInstanceProcedure`, stored on
+`ResolveState.answerType`) and consulted only by `Check.return`;
+every other rule is independent of it.
+
+Several constructs are *statements*: their job is to have an effect,
+not to produce a value. They are handled by `Synth.resolveStmtExpr`
+and synthesize `TVoid`:
+
+- **Control-flow terminators** (`Exit`, `Return`): they jump somewhere
+  else and never hand a value back.
+- **Effect-only forms** (`Assert`, `Assume`, `While`, `Var-Declare`):
+  they run and fall through without producing a value.
+
+In either case, `Check.statement` (the `⋄` judgment) simply
+synthesizes and discards the type, so any expression — including
+value-producing ones like calls — is admitted in statement position.
+
+`Assign` is the one statement that *does* produce a value: it
+synthesizes the type of its right-hand side (so `x := e` can be used
+where that type is expected), and its check rule skips the \[⇐\] Sub
+boundary check only when the expected type is `TVoid` — i.e. when the
+assignment is used purely for effect. `Block` routes the surrounding
+expected type to its last statement (the block's value); non-last
+statements are in effect position (synthesized and discarded via
+`Check.statement`).
+
+Each typing rule is implemented as its own helper inside the mutual
+block below. Helpers are grouped by section to mirror the *Typing
+rules* index in `LaurelDoc.lean`:
+
+- Literals — `Synth.litInt`, `Synth.litBool`, `Synth.litString`, `Synth.litDecimal`
+- Variables — `Synth.varLocal`, `Synth.varField`, `Check.varDeclare`
+- Control flow — `Check.while`, `Check.exit`, `Check.return`,
+  `Check.block`, `Check.ifThenElse`
+- Verification statements — `Check.assert`, `Check.assume`
+- Assignment — `Synth.assign`, `Check.assign`
+- Calls — `Synth.staticCall`, `Synth.instanceCall`
+- Primitive operations — `Synth.primitiveOp`, `Check.primitiveOp`
+- Object forms — `Synth.new`, `Synth.asType`, `Synth.isType`, `Synth.refEq`,
+  `Synth.pureFieldUpdate`
+- Verification expressions — `Synth.quantifier`, `Synth.assigned`,
+  `Synth.fresh`, `Synth.old`/`Check.old`, `Synth.proveBy`/`Check.proveBy`
+- Self reference — `Synth.this`
+- Untyped forms — `Synth.abstract`, `Synth.all`
+- ContractOf — `Synth.contractOf`
+- Holes — `Check.holeSome`, `Check.holeNone`
+
+The dispatch functions `Synth.resolveStmtExpr` and `Check.resolveStmtExpr`
+pattern-match on the constructor and delegate to the corresponding helper. -/
+
+namespace Resolution
+
+/-! ## Gradual-typing elaboration helpers
+
+These build nodes from already-resolved pieces and resolve inserted callees via
+`resolveRef`; they never recurse into the `Synth`/`Check` mutual block, so its
+termination measure is unaffected. No-ops unless a `GradualConfig` is active. -/
+
+/-- The active config — `some` only inside a user procedure being elaborated. -/
+private def activeGradual : ResolveM (Option GradualConfig) := do
+  let s ← get
+  return if s.gradualActive then s.gradual else none
+
+/-- A `name(args)` call with its callee resolved in-pass, so phase 2 sees its id. -/
+private def mkPreludeCall (name : String) (args : List StmtExprMd)
+    (source : Option FileRange) : ResolveM StmtExprMd := do
+  let callee ← resolveRef { text := name } source
+  return { val := .StaticCall callee args, source := source }
+
+/-- Materialize an implicit `Any`↔primitive cast (box / unbox / `Any_to_bool`),
+    or `none` if none applies. Assumes elaboration is active (caller holds `g`). -/
+private def tryCoerce (g : GradualConfig) (expected actual : HighType) (e : StmtExprMd)
+    (source : Option FileRange) : ResolveM (Option StmtExprMd) := do
+  if g.isDynamic expected && !g.isDynamic actual then
+    match g.box actual with
+    | some b => return some (← mkPreludeCall b [e] source)
+    | none => return none
+  else if !g.isDynamic expected && g.isDynamic actual then
+    match expected, g.unbox expected with
+    | .TBool, _ => return some (← mkPreludeCall g.toBool [e] source)
+    | _, some u => return some (← mkPreludeCall u [e] source)
+    | _, none => return none
+  else return none
+
+/-- `tryCoerce` gated by the active config — a no-op when elaboration is off.
+    The single entry point for coercion insertion outside the `synthArith` /
+    `synthOther` dispatch, which already holds the config. -/
+private def tryCoerceActive (expected actual : HighType) (e : StmtExprMd)
+    (source : Option FileRange) : ResolveM (Option StmtExprMd) := do
+  match ← activeGradual with
+  | some g => tryCoerce g expected actual e source
+  | none => pure none
+
+/-- Insert a gradual coercion for `e` from `actual` to `expected`, falling back
+    to a subtyping check — the single boundary handler for non-operator check
+    sites. In gradual mode a native-expected / dynamic-actual boundary that no
+    coercion covers is fail-loud rather than deferring to `checkSubtype` (whose
+    consistency relation would silently accept an un-coerced dynamic value into a
+    native slot). Inert when gradual is off. -/
+private def coerceOrCheck (expected actual : HighTypeMd) (e : StmtExprMd)
+    (source : Option FileRange) : ResolveM StmtExprMd := do
+  match ← tryCoerceActive expected.val actual.val e source with
+  | some c => return c
+  | none =>
+    match ← activeGradual with
+    | some g =>
+      -- Fail loud only at a *concrete native scalar* boundary
+      -- {int,bool,str,real,float64,bv} that no coercion covered: a dynamic value
+      -- reaching one with no box/unbox and no VC is the genuinely-unsound case.
+      -- `Unknown` (the gradual top) and nominal types are consistent with
+      -- everything, so they fall through to `checkSubtype` and must not be
+      -- rejected here.
+      let expectedNativeScalar := match expected.val with
+        | .TInt | .TBool | .TString | .TReal | .TFloat64 | .TBv _ => true
+        | _ => false
+      if expectedNativeScalar && g.isDynamic actual.val then
+        let diag := diagnosticFromSource source
+          s!"no coercion from dynamic '{formatType actual}' into native '{formatType expected}' at this boundary; an explicit cast is required"
+        modify fun s => { s with errors := s.errors.push diag }
+        return e
+      else
+        checkSubtype source expected actual
+        return e
+    | none =>
+      checkSubtype source expected actual
+      return e
+
+/-- Coerce every operand to `target`. -/
+private def coerceEach (g : GradualConfig) (target : HighType) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (source : Option FileRange) :
+    ResolveM (List StmtExprMd) :=
+  (args'.zip argTypes).mapM fun (a, t) => return (← tryCoerce g target t.val a source).getD a
+
+/-- Rewrite `op` to its dynamic prelude operator, boxing all operands; `none` if
+    `op` has no prelude operator. -/
+private def forcePrelude (g : GradualConfig) (op : Operation) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (source : Option FileRange) :
+    ResolveM (Option (StmtExpr × HighTypeMd)) := do
+  let some name := g.opPrelude op | return none
+  let boxed ← coerceEach g g.dynamic args' argTypes source
+  let call ← mkPreludeCall name boxed source
+  return some (call.val, { val := g.dynamic, source := source })
+
+/-- `forcePrelude` only when some operand is already dynamic. -/
+private def elaborateDynamicOp (g : GradualConfig) (op : Operation) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (source : Option FileRange) :
+    ResolveM (Option (StmtExpr × HighTypeMd)) := do
+  unless argTypes.any (fun t => g.isDynamic t.val) do return none
+  forcePrelude g op args' argTypes source
 
 /-- LUB of the operand types, or `none` if inconsistent. -/
 private def joinAll (ctx : TypeLattice) (argTypes : List HighTypeMd)
@@ -574,13 +762,26 @@ private def joinAll (ctx : TypeLattice) (argTypes : List HighTypeMd)
     (fun acc t => match acc with | some l => join ctx l t | none => none)
     (some { val := .Unknown, source := source })
 
-/-- A `MultiValuedExpr` operand is a multi-output call (`multi(x)` declared
-    `returns (a, b)`) used in value position. It is an internal pseudo-type with
-    no Core lowering, so it must never reach an operator slot — letting it
-    through crashes a later pass as a `StrataBug`. Emit the position-oriented
-    diagnostic for the offending operand and return `true` so the caller
-    short-circuits to the operator's natural result type, suppressing the
-    per-family check (and its cascading error) on that operand. -/
+/-- Whether the operands join to a single numeric type. -/
+private def joinsToNumeric (ctx : TypeLattice) (argTypes : List HighTypeMd)
+    (source : Option FileRange) : Bool :=
+  match joinAll ctx argTypes source with
+  | some jt => isNumeric ctx jt
+  | none => false
+
+private def isComparisonOp : Operation → Bool
+  | .Lt | .Leq | .Gt | .Geq => true
+  | _ => false
+
+private def isArithmeticOp : Operation → Bool
+  | .Neg | .Add | .Sub | .Mul | .Div | .Mod | .DivT | .ModT => true
+  | _ => false
+
+/-- A `MultiValuedExpr` operand (a multi-output call used in value position) is
+    an internal pseudo-type with no Core lowering, so it must never reach an
+    operator slot — letting it through crashes a later pass as a `StrataBug`.
+    Emit the position-oriented diagnostic and return `true` so the caller
+    short-circuits to the operator's result type, suppressing cascades. -/
 private def reportMultiValued (a : StmtExprMd) (aTy : HighTypeMd) : ResolveM Bool := do
   match aTy.val with
   | .MultiValuedExpr _ =>
@@ -590,10 +791,35 @@ private def reportMultiValued (a : StmtExprMd) (aTy : HighTypeMd) : ResolveM Boo
     pure true
   | _ => pure false
 
-/-- Native arithmetic typing: every operand must be numeric, and the result is
-    the LUB of the operand types under the consistency relation. A multi-valued
-    operand short-circuits to `Unknown` (arithmetic's natural
-    cascade-suppression type). -/
+/-- A candidate lowering: `some` if it applies, else `none`. -/
+private abbrev OpAlt := ResolveM (Option (StmtExpr × HighTypeMd))
+
+/-- The first applicable candidate lowering, else the native `dflt`. -/
+private def firstElab (alts : List OpAlt) (dflt : ResolveM (StmtExpr × HighTypeMd)) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  for alt in alts do
+    if let some r ← alt then return r
+  dflt
+
+/-- The dynamic prelude operator for `op` when `cond` holds, else decline. -/
+private def preludeWhen (g : GradualConfig) (cond : Bool) (op : Operation) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (source : Option FileRange) : OpAlt :=
+  if cond then forcePrelude g op args' argTypes source else pure none
+
+/-- String concatenation, whether it arrives as `+` on all-string operands or as
+    an explicit `StrConcat`: emit `StrConcat`, coercing each operand to string
+    across the `Any` boundary (a no-op for operands already typed string). -/
+private def strConcatAlt (g : GradualConfig) (op : Operation) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (skipProof : Bool) (source : Option FileRange) : OpAlt := do
+  let isConcat := (op matches .StrConcat) ||
+    ((op matches .Add) && !argTypes.isEmpty && argTypes.all (fun t => t.val matches .TString))
+  unless isConcat do return none
+  let coerced ← coerceEach g (.TString) args' argTypes source
+  return some (.PrimitiveOp .StrConcat coerced skipProof, { val := .TString, source := source })
+
+/-- Native arithmetic typing: all operands must be numeric; the result is their
+    LUB under the consistency relation. A multi-valued operand short-circuits to
+    `Unknown` (arithmetic's natural cascade-suppression type). -/
 private def nativeArith (op : Operation) (expr : StmtExpr) (args' : List StmtExprMd)
     (argTypes : List HighTypeMd) (skipProof : Bool) (source : Option FileRange) :
     ResolveM (StmtExpr × HighTypeMd) := do
@@ -616,10 +842,8 @@ private def nativeArith (op : Operation) (expr : StmtExpr) (args' : List StmtExp
     pure (.PrimitiveOp op args' skipProof, unknownTy)
 
 /-- Native typing for the boolean / comparison / equality / string-concat
-    families: a fixed result type (`TBool` / `TString`) with the family's operand
-    constraint (booleans subtype `TBool`, comparisons are numeric, equality is
-    consistent, concat operands subtype `TString`). A multi-valued operand
-    short-circuits to the family's natural result type. -/
+    families: a fixed result type with each family's operand constraint. A
+    multi-valued operand short-circuits to the family's natural result type. -/
 private def nativeOther (op : Operation) (expr : StmtExpr) (args' : List StmtExprMd)
     (argTypes : List HighTypeMd) (skipProof : Bool) (source : Option FileRange) :
     ResolveM (StmtExpr × HighTypeMd) := do
@@ -657,74 +881,65 @@ private def nativeOther (op : Operation) (expr : StmtExpr) (args' : List StmtExp
   | _ => pure ()
   pure (.PrimitiveOp op args' skipProof, { val := resultTy, source := source })
 
-/-! ## Typing rules
-
-The judgment is bidirectional:
-
-```
-Γ ⊢ e ⇒ A          (Synth.resolveStmtExpr)
-Γ ⊢ e ⇐ A          (Check.resolveStmtExpr)
-```
-
-- `Γ` — lexical scope (variables, fields). Block labels live in a
-  separate namespace `Γ_lbl` (`ResolveState.labelScope`), consulted
-  only by `Check.exit`.
-- `A` — *value type* of the term.
-
-The `Return` rules additionally depend on the enclosing procedure's
-declared output-type list, written `T_o-bar` in the rule statements.
-That list is bound on entry to a procedure body (by
-`resolveProcedure` / `resolveInstanceProcedure`, stored on
-`ResolveState.answerType`) and consulted only by `Check.return`;
-every other rule is independent of it.
-
-Several constructs are *statements*: their job is to have an effect,
-not to produce a value. They are handled by `Synth.resolveStmtExpr`
-and synthesize `TVoid`:
-
-- **Control-flow terminators** (`Exit`, `Return`): they jump somewhere
-  else and never hand a value back.
-- **Effect-only forms** (`Assert`, `Assume`, `While`, `Var-Declare`):
-  they run and fall through without producing a value.
-
-In either case, `Check.statement` (the `⋄` judgment) simply
-synthesizes and discards the type, so any expression — including
-value-producing ones like calls — is admitted in statement position.
-
-`Assign` is the one statement that *does* produce a value: it
-synthesizes the type of its right-hand side (so `x := e` can be used
-where that type is expected), and its check rule skips the \[⇐\] Sub
-boundary check only when the expected type is `TVoid` — i.e. when the
-assignment is used purely for effect. `Block` routes the surrounding
-expected type to its last statement (the block's value); non-last
-statements are in effect position (synthesized and discarded via
-`Check.statement`).
-
-Each typing rule is implemented as its own helper inside the mutual
-block below. Helpers are grouped by section to mirror the *Typing
-rules* index in `LaurelDoc.lean`:
-
-- Literals — `Synth.litInt`, `Synth.litBool`, `Synth.litString`, `Synth.litDecimal`
-- Variables — `Synth.varLocal`, `Synth.varField`, `Check.varDeclare`
-- Control flow — `Check.while`, `Check.exit`, `Check.return`,
-  `Check.block`, `Check.ifThenElse`
-- Verification statements — `Check.assert`, `Check.assume`
-- Assignment — `Synth.assign`, `Check.assign`
-- Calls — `Synth.staticCall`, `Synth.instanceCall`
-- Primitive operations — `Synth.primitiveOp`, `Check.primitiveOp`
-- Object forms — `Synth.new`, `Synth.asType`, `Synth.isType`, `Synth.refEq`,
-  `Synth.pureFieldUpdate`
-- Verification expressions — `Synth.quantifier`, `Synth.assigned`,
-  `Synth.fresh`, `Synth.old`/`Check.old`, `Synth.proveBy`/`Check.proveBy`
-- Self reference — `Synth.this`
-- Untyped forms — `Synth.abstract`, `Synth.all`
-- ContractOf — `Synth.contractOf`
-- Holes — `Check.holeSome`, `Check.holeNone`
-
-The dispatch functions `Synth.resolveStmtExpr` and `Check.resolveStmtExpr`
-pattern-match on the constructor and delegate to the corresponding helper. -/
+/-- Lower an arithmetic-family `PrimitiveOp` over already-synthesized operands. -/
+private def synthArith (g : GradualConfig) (op : Operation) (expr : StmtExpr) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (skipProof : Bool) (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let ctx := (← get).typeLattice
+  firstElab
+    [ elaborateDynamicOp g op args' argTypes source,
+      strConcatAlt g op args' argTypes skipProof source,
+      preludeWhen g (!joinsToNumeric ctx argTypes source) op args' argTypes source ]
+    (nativeArith op expr args' argTypes skipProof source)
+
+/-- Lower the boolean / comparison / equality / string-concat `PrimitiveOp`
+    family over already-synthesized operands. -/
+private def synthOther (g : GradualConfig) (op : Operation) (expr : StmtExpr) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (skipProof : Bool) (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let ctx := (← get).typeLattice
+  firstElab
+    [ elaborateDynamicOp g op args' argTypes source,
+      preludeWhen g (isComparisonOp op && !joinsToNumeric ctx argTypes source)
+        op args' argTypes source,
+      strConcatAlt g op args' argTypes skipProof source ]
+    (nativeOther op expr args' argTypes skipProof source)
+
+/-- Strict native typing, dispatched by operator family. Used in non-user code
+    (the hand-written `Any` prelude, library bodies): a type mismatch is a hard
+    error, never a coercion. -/
+private def nativeOp (op : Operation) (expr : StmtExpr) (args' : List StmtExprMd)
+    (argTypes : List HighTypeMd) (skipProof : Bool) (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) :=
+  if isArithmeticOp op then nativeArith op expr args' argTypes skipProof source
+  else nativeOther op expr args' argTypes skipProof source
 
-namespace Resolution
+/-- Gradual typing, dispatched by operator family. Used inside frontend
+    procedures: pick a native or `Any`-prelude operator and insert coercions,
+    with `nativeOp`'s strict rule as the fallback. -/
+private def gradualOp (g : GradualConfig) (op : Operation) (expr : StmtExpr)
+    (args' : List StmtExprMd) (argTypes : List HighTypeMd) (skipProof : Bool)
+    (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  -- Hoisted multi-valued guard: a `MultiValuedExpr` operand has no Core lowering
+  -- and must never reach an operator slot (a later pass crashes as a `StrataBug`).
+  -- The gradual dispatch can route it into a prelude operator before the native
+  -- fallback catches it, so check here, before dispatch, to give the same clean
+  -- diagnostic in gradual mode as in strict mode.
+  let mut hasMulti := false
+  for (a, aTy) in args'.zip argTypes do
+    if (← reportMultiValued a aTy) then hasMulti := true
+  if hasMulti then
+    let resultTy : HighType :=
+      if isArithmeticOp op then .Unknown
+      else match op with
+        | .Eq | .Neq | .And | .Or | .AndThen | .OrElse | .Not | .Implies
+        | .Lt | .Leq | .Gt | .Geq => .TBool
+        | .StrConcat => .TString
+        | _ => .Unknown
+    return (.PrimitiveOp op args' skipProof, { val := resultTy, source := source })
+  if isArithmeticOp op then synthArith g op expr args' argTypes skipProof source
+  else synthOther g op expr args' argTypes skipProof source
 
 -- The `h : exprMd.val = .Foo args ...` parameters on the recursive helpers
 -- look unused to the linter, but each one is referenced by that helper's
@@ -866,6 +1081,10 @@ def Synth.resolveStmtExpr (exprMd : StmtExprMd) : ResolveM (StmtExprMd × HighTy
     synthesized type, used at sites where typing is not enforced —
     verification annotations, modifies/reads clauses). -/
 def Check.resolveStmtExpr (exprMd : StmtExprMd) (expected : HighTypeMd) : ResolveM StmtExprMd := do
+  -- In user code, lower primitive ops via synthesis then coerce to `expected`.
+  if (← get).gradualActive && (exprMd.val matches .PrimitiveOp _ _ _) then
+    let (e', actual) ← Synth.resolveStmtExpr exprMd
+    return ← coerceOrCheck expected actual e' exprMd.source
   match h_node: exprMd with
   | AstNode.mk expr source =>
   match h_expr: expr with
@@ -925,10 +1144,10 @@ def Check.resolveStmtExpr (exprMd : StmtExprMd) (expected : HighTypeMd) : Resolv
   | .PrimitiveOp .Implies args skipProof =>
     Check.primitiveOp exprMd .Implies args skipProof expected source (by rw [h_node])
   | _ =>
-    -- Subsumption fallback: synth then check `actual <: expected`.
+    -- Subsumption fallback: synth, then either materialize an implicit gradual
+    -- cast (box/unbox/toBool) or check `actual <: expected` as usual.
     let (e', actual) ← Synth.resolveStmtExpr exprMd
-    checkSubtype source expected actual
-    pure e'
+    coerceOrCheck expected actual e' source
   termination_by (exprMd, 3)
   decreasing_by all_goals first
     | (apply Prod.Lex.left; term_by_mem)
@@ -1418,8 +1637,14 @@ def Synth.ifThenElse (exprMd : StmtExprMd)
   | some e =>
     let (e', elseTy) ← Synth.resolveStmtExpr e
     let ctx := (← get).typeLattice
+    -- A `TVoid` branch marks a statement-position `if` whose value is discarded
+    -- (e.g. `if c: pass else: x = e`). Its synthesized "type" isn't a value type,
+    -- so don't require branch consistency; only when *both* branches produce real
+    -- values is consistency required.
     let ty ←
-      if isConsistent ctx thenTy elseTy then
+      if thenTy.val matches .TVoid || elseTy.val matches .TVoid then
+        pure { val := .TVoid, source := source }
+      else if isConsistent ctx thenTy elseTy then
         pure ((join ctx thenTy elseTy).getD thenTy)
       else
         let diag := diagnosticFromSource source
@@ -1951,8 +2176,12 @@ def Synth.primitiveOp (exprMd : StmtExprMd) (expr : StmtExpr)
     Synth.resolveStmtExpr a.val)
   let args' := results.map (·.1)
   let argTypes := results.map (·.2)
-  if isArithmeticOp op then nativeArith op expr args' argTypes skipProof source
-  else nativeOther op expr args' argTypes skipProof source
+  -- Gradual typing only inside user procedures; strict native typing elsewhere.
+  -- Kept apart on purpose: the `Any` prelude and library bodies must stay
+  -- verified under the strict rules, so don't unify these two arms.
+  match ← activeGradual with
+  | some g => gradualOp g op expr args' argTypes skipProof source
+  | none   => nativeOp op expr args' argTypes skipProof source
   termination_by (exprMd, 1)
   decreasing_by
     all_goals
@@ -2627,8 +2856,11 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
     -- translator wraps every body in (`Core.Statement.block bodyLabel …`),
     -- so that frontends emitting `Exit bodyLabel` for early-return lowering
     -- (e.g. PythonToLaurel) don't trip Check.exit's label-scope check.
+    let savedGradual := (← get).gradualActive
+    modify fun s => { s with gradualActive :=
+      (s.gradual.elim false fun g => g.shouldElaborate proc.name.text) }
     let body' ← withLabel (some bodyLabel) <| resolveBody proc.body
-    modify fun s => { s with answerType := savedAnswer }
+    modify fun s => { s with answerType := savedAnswer, gradualActive := savedGradual }
     -- Transparent (static) procedure bodies are supported (#1215): the
     -- TransparencyPass derives a functional `$asFunction` copy, and the
     -- LaurelToCore translator rejects the genuinely-unsupported constructs
@@ -2670,8 +2902,11 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     let savedAnswer := (← get).answerType
     modify fun s => { s with answerType := some (outputs'.map (·.type)) }
     -- See `resolveProcedure` for the rationale on `bodyLabel`.
+    let savedGradual := (← get).gradualActive
+    modify fun s => { s with gradualActive :=
+      (s.gradual.elim false fun g => g.shouldElaborate proc.name.text) }
     let body' ← withLabel (some bodyLabel) <| resolveBody proc.body
-    modify fun s => { s with answerType := savedAnswer }
+    modify fun s => { s with answerType := savedAnswer, gradualActive := savedGradual }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     modify fun s => { s with instanceTypeName := savedInstType }
     let axioms' ← proc.axioms.mapM resolveStmtExpr
@@ -3119,7 +3354,8 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do
 /-! ## Entry point -/
 
 /-- Run the full resolution pass on a Laurel program. -/
-public def resolve (program : Program) (existingModel: Option SemanticModel := none) : ResolutionResult :=
+public def resolve (program : Program) (existingModel: Option SemanticModel := none)
+    (gradual : Option GradualConfig := none) : ResolutionResult :=
   -- Phase 1: pre-register all top-level names, then assign IDs and resolve references
   let phase1 : ResolveM Program := do
     preRegisterTopLevel program
@@ -3131,7 +3367,7 @@ public def resolve (program : Program) (existingModel: Option SemanticModel := n
              types := types', constants := constants' }
   let nextId := existingModel.elim 1 (fun m => m.nextId)
   let typeLattice := TypeLattice.ofTypes program.types
-  let (program', finalState) := phase1.run { nextId := nextId, typeLattice }
+  let (program', finalState) := phase1.run { nextId := nextId, typeLattice, gradual }
   -- Phase 2: build refToDef from the resolved program (all definitions now have UUIDs)
   let refToDef := buildRefToDef program'
   let semanticModel := {
diff --git a/StrataTest/Languages/Laurel/GradualResolutionTests.lean b/StrataTest/Languages/Laurel/GradualResolutionTests.lean
new file mode 100644
index 0000000000..edab9b3224
--- /dev/null
+++ b/StrataTest/Languages/Laurel/GradualResolutionTests.lean
@@ -0,0 +1,263 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Tests that exercise the GRADUAL-TYPING path of resolution (`Laurel.resolve`
+called with a `GradualConfig`). The rest of the Laurel resolution suite runs in
+strict mode (no config), so these are the only tests that drive gradual
+elaboration: coercion insertion across the `Any` boundary, and the fail-loud
+diagnostic for an un-coerced dynamic-into-native boundary.
+
+The dynamic type here is `Core Any` (i.e. `HighType.TCore "Any"`), which the
+consistency relation treats as gradual (consistent with everything). A minimal
+`GradualConfig` is constructed per-test; the only knobs that matter are whether
+an unbox coercion exists for the native target.
+-/
+
+import StrataTest.Util.TestLaurel
+
+open Strata
+open StrataTest.Util
+
+namespace Strata.Laurel
+
+/-- Substring containment. -/
+private def containsSubstr (haystack needle : String) : Bool :=
+  (haystack.splitOn needle).length > 1
+
+/-- A minimal gradual config for tests. The dynamic type is `Core Any`.
+    `unboxName` controls whether an `Any → native` unbox coercion exists:
+    `some n` materializes a call to `n`; `none` leaves the boundary uncovered
+    (so the fail-loud path fires).
+    `boxName` controls whether a `native → Any` box coercion exists (the other
+    coercion direction); `none` (the default) leaves boxing off.
+    `elaborate` is wired into `shouldElaborate`: when `false`, gradual
+    elaboration is gated off for every procedure, so no coercion is inserted and
+    the boundary falls back to the permissive consistency check.
+    Prelude operators are unused here. -/
+private def testGradualConfig (unboxName : Option String)
+    (boxName : Option String := none) (elaborate : Bool := true) : GradualConfig where
+  dynamic := .TCore "Any"
+  isDynamic := fun t => match t with | .TCore "Any" => true | _ => false
+  box := fun _ => boxName
+  unbox := fun _ => unboxName
+  toBool := "Any_to_bool"
+  opPrelude := fun _ => none
+  shouldElaborate := fun _ => elaborate
+
+/-- Resolve with a gradual config, printing each diagnostic message on its own
+    line (or `no errors`), then whether the resolved program contains a call to
+    the named coercion function (evidence that a coercion was inserted). -/
+private def resolveGradual (unboxName : Option String) (coercionProbe : String)
+    (program : StrataDDM.Program)
+    (boxName : Option String := none) (elaborate : Bool := true) : IO Unit := do
+  let laurelProgram ← translateLaurel program
+  let result := resolve laurelProgram
+    (gradual := some (testGradualConfig unboxName boxName elaborate))
+  if result.errors.isEmpty then
+    IO.println "no errors"
+  else
+    for e in result.errors do
+      IO.println e.message
+  let formatted := toString (Std.Format.pretty (Std.ToFormat.format result.program))
+  IO.println s!"coercion '{coercionProbe}' inserted: {containsSubstr formatted coercionProbe}"
+
+/-! ## Coercion insertion (gradual path is live)
+
+With an unbox mapping available, an `Any`-typed value flowing into a native
+`int` slot is rewritten to an explicit unbox call. This confirms the gradual
+elaboration actually runs (strict resolution would never insert a call). -/
+
+/--
+info: no errors
+coercion 'unbox_to_int' inserted: true
+-/
+#guard_msgs in
+#eval! resolveGradual (some "unbox_to_int") "unbox_to_int"
+#strata
+program Laurel;
+function unbox_to_int(x: Core Any): int;
+procedure useAny(a: Core Any)
+  returns (r: int)
+{
+  r := a;
+  return
+};
+#end
+
+/-! ## Fail-loud at an un-coerced dynamic → native boundary (L3/L8/P4)
+
+With NO unbox mapping, the same `Any`-into-`int` position is no longer silently
+accepted (the consistency relation would treat `Core Any` as consistent with
+`int`). It now raises a resolution error demanding an explicit cast, and inserts
+no coercion. -/
+
+/--
+info: no coercion from dynamic 'Core Any' into native 'int' at this boundary; an explicit cast is required
+coercion 'unbox_to_int' inserted: false
+-/
+#guard_msgs in
+#eval! resolveGradual none "unbox_to_int"
+#strata
+program Laurel;
+procedure useAnyBad(a: Core Any)
+  returns (r: int)
+{
+  r := a;
+  return
+};
+#end
+
+/-! ## Multi-valued operand under gradual config (L1 gradual-path coverage)
+
+A multi-output call (`returns (a, b)`) used in operator-operand position is an
+internal `MultiValuedExpr` pseudo-type with no Core lowering. The gradual
+elaboration path must report the clean position-oriented diagnostic for it
+rather than letting it slip through to a later pass that crashes as a
+`StrataBug`. This exercises the gradual operator path specifically (the strict
+counterpart lives in `ResolutionTypeCheckTests`), confirming the multi-valued
+guard fires even when a `GradualConfig` is threaded through. -/
+
+/--
+info: multi-output call cannot be used as a value here; it returns multiple values. Unpack it into separate variables first
+coercion 'unused' inserted: false
+-/
+#guard_msgs in
+#eval! resolveGradual (some "unbox_to_int") "unused"
+#strata
+program Laurel;
+procedure multi(x: int) returns (a: int, b: int) opaque;
+procedure test() opaque {
+  assert multi(1) == 1
+};
+#end
+
+/-! ## A. Gradual gating / inertness (`shouldElaborate := false`)
+
+Even with a perfectly good unbox mapping available (`unbox ↦ "unbox_to_int"`),
+gating elaboration off (the config's `shouldElaborate` returns `false` for every
+procedure) must leave the `Any → int` position untouched: no coercion is
+inserted, and the boundary falls back to the permissive consistency check (which
+treats `Core Any` as consistent with `int`, so no error). This pins that gradual
+elaboration is genuinely gated by `shouldElaborate` — the same `r := a` position
+that gets an `unbox_to_int` coercion in the first test above gets none here. The
+prelude function is intentionally *not* declared, so the probe matches only an
+actually-inserted coercion call (gating off ⇒ no call ⇒ `false`). -/
+
+/--
+info: no errors
+coercion 'unbox_to_int' inserted: false
+-/
+#guard_msgs in
+#eval! resolveGradual (some "unbox_to_int") "unbox_to_int" (elaborate := false)
+#strata
+program Laurel;
+procedure useAny(a: Core Any)
+  returns (r: int)
+{
+  r := a;
+  return
+};
+#end
+
+/-! ## B. Truthiness coercion (`toBool`) at a condition position
+
+An `Any`-typed value used in a boolean-guard position (here a `while`
+condition, checked against `bool`) is rewritten to the config's `toBool`
+coercion (`Any_to_bool`). This holds independently of whether an unbox mapping
+exists (`unboxName` is `none` here), since the `.TBool` arm of `tryCoerce` is
+served by `toBool`, not `unbox`. -/
+
+/--
+info: no errors
+coercion 'Any_to_bool' inserted: true
+-/
+#guard_msgs in
+#eval! resolveGradual none "Any_to_bool"
+#strata
+program Laurel;
+function Any_to_bool(x: Core Any): bool;
+procedure loopAny(a: Core Any)
+{
+  while (a) { }
+};
+#end
+
+/-! ## C. Box coercion (native → dynamic)
+
+The other coercion direction: a native `int` flowing into a `Core Any` slot is
+rewritten to an explicit box call (`box_int`) supplied via the config's `box`
+mapping. Confirms the dynamic-expected / native-actual arm of `tryCoerce`. -/
+
+/--
+info: no errors
+coercion 'box_int' inserted: true
+-/
+#guard_msgs in
+#eval! resolveGradual none "box_int" (boxName := some "box_int")
+#strata
+program Laurel;
+function box_int(x: int): Core Any;
+procedure useInt(i: int)
+  returns (r: Core Any)
+{
+  r := i;
+  return
+};
+#end
+
+/-! ## D. Native operator over native operands (no coercion)
+
+A native operator (`+`) over native (`int`) operands resolves to the native
+operator with no coercion inserted: the gradual path only rewrites operators
+when some operand is already dynamic, so an all-native operation is left exactly
+as strict resolution would leave it (no unbox call, no error). -/
+
+/--
+info: no errors
+coercion 'unbox_to_int' inserted: false
+-/
+#guard_msgs in
+#eval! resolveGradual (some "unbox_to_int") "unbox_to_int"
+#strata
+program Laurel;
+procedure addInts(x: int, y: int)
+  returns (r: int)
+{
+  r := x + y;
+  return
+};
+#end
+
+/-! ## D (cont.). Fail-loud restricted to native scalar targets
+
+The dynamic → native fail-loud only fires for a *native scalar* target
+(`int/bool/str/real/float64/bv`). A dynamic value flowing into a non-scalar
+*nominal* target (here a `datatype`) is the gradual-top case: it falls through
+to the permissive consistency check WITHOUT the fail-loud diagnostic, exactly as
+before gradual elaboration existed. There is no unbox mapping (`unboxName` is
+`none`) and no coercion is inserted; the absence of the
+`no coercion from dynamic ... into native ...` error confirms the diagnostic is
+correctly scoped to native sorts and does not over-fire on nominal slots. -/
+
+/--
+info: no errors
+coercion 'unbox_to_color' inserted: false
+-/
+#guard_msgs in
+#eval! resolveGradual none "unbox_to_color"
+#strata
+program Laurel;
+datatype Color { Red, Green, Blue }
+procedure useAnyNominal(a: Core Any)
+  returns (r: Color)
+{
+  r := a;
+  return
+};
+#end
+
+end Strata.Laurel

From 5cee1ec9973e46f48a4df7a27d618cf558f050aa Mon Sep 17 00:00:00 2001
From: Massart <julesmt@amazon.com>
Date: Sat, 13 Jun 2026 18:46:21 -0700
Subject: [PATCH 4/8] Thread the gradual config through the Laurel pipeline

Add gradualConfig to LaurelTranslateOptions and pass it from
LaurelCompilationPipeline into resolve by named argument. Defaults to none, so
pipelines that supply no config are unaffected.
---
 Strata/Languages/Laurel/LaurelCompilationPipeline.lean | 4 ++--
 Strata/Languages/Laurel/LaurelPass.lean                | 4 ++++
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index 4e048572c5..66aefdbda0 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -138,7 +138,7 @@ private def runLaurelPasses
   emit "Initial" "laurel.st" program
 
   -- Initial resolution
-  let result := resolve program
+  let result := resolve program (gradual := options.gradualConfig)
   let resolutionErrors : Std.HashSet DiagnosticModel := Std.HashSet.ofArray result.errors
   let (program, model) := (result.program, result.model)
 
@@ -154,7 +154,7 @@ private def runLaurelPasses
     allStats := allStats.merge stats
     -- Run resolve after the pass if needed
     if pass.needsResolves then
-      let result := resolve program (some model)
+      let result := resolve program (existingModel := some model) (gradual := options.gradualConfig)
       let newErrors := result.errors.filter fun e => !resolutionErrors.contains e
       if !newErrors.isEmpty then
         let newDiags := newErrors.toList.map fun d =>
diff --git a/Strata/Languages/Laurel/LaurelPass.lean b/Strata/Languages/Laurel/LaurelPass.lean
index 7a61739a16..d7ce1eb61c 100644
--- a/Strata/Languages/Laurel/LaurelPass.lean
+++ b/Strata/Languages/Laurel/LaurelPass.lean
@@ -6,6 +6,7 @@
 module
 
 public import Strata.Languages.Laurel.SemanticModel
+public import Strata.Languages.Laurel.Resolution
 public import Strata.Util.Statistics
 public import Strata.Languages.Core.Options
 
@@ -21,6 +22,9 @@ structure LaurelTranslateOptions where
       this option has no effect. Use with the verifier's `useArrayTheory`. -/
   enumeratedModifiesClauses : Bool := false
   keepAllFilesPrefix : Option String := none
+  /-- Gradual-typing elaboration config; when set, resolution lowers generic
+      ops/coercions to the frontend's dynamic-typing prelude. -/
+  gradualConfig : Option GradualConfig := none
 
 instance : Inhabited LaurelTranslateOptions where
   default := {}

From e6653f38b461e438ba4e473fa81974e57e5acc03 Mon Sep 17 00:00:00 2001
From: Massart <julesmt@amazon.com>
Date: Sat, 13 Jun 2026 18:46:21 -0700
Subject: [PATCH 5/8] Retain elaboration-inserted prelude functions when
 filtering

filterPrelude runs before elaboration, so the prelude calls it may insert are
not yet referenced by the user program. Add extraSeeds (retained unconditionally)
and a generic opSeed (Operation -> Option String) so an operator's prelude
function is retained only when that operator appears. Inert without seeds.
---
 Strata/Languages/Laurel/FilterPrelude.lean    | 20 +++-
 .../Languages/Laurel/FilterPreludeTest.lean   | 94 +++++++++++++++++++
 2 files changed, 109 insertions(+), 5 deletions(-)
 create mode 100644 StrataTest/Languages/Laurel/FilterPreludeTest.lean

diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean
index 52fd25fcbc..2c89845e80 100644
--- a/Strata/Languages/Laurel/FilterPrelude.lean
+++ b/Strata/Languages/Laurel/FilterPrelude.lean
@@ -57,6 +57,11 @@ structure CollectState where
   procNames : Std.HashSet String := {}
   /-- Names from UserDefined types, New, extending. -/
   typeNames : Std.HashSet String := {}
+  /-- For a primitive operator present in the program, the prelude name a
+      frontend's elaboration would insert for it; that name is then retained as
+      if referenced. `fun _ => none` (the default) disables on-demand operator
+      seeding. -/
+  opSeed : Operation → Option String := fun _ => none
 
 abbrev CollectM := StateM CollectState
 
@@ -112,7 +117,9 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
   | .Var (.Declare param) => collectHighTypeNames param.type
   | .PureFieldUpdate target _ newVal =>
     collectExprNames target; collectExprNames newVal
-  | .PrimitiveOp _ args _ => args.forM collectExprNames
+  | .PrimitiveOp op args _ =>
+    if let some n := (← get).opSeed op then addProcName n
+    args.forM collectExprNames
   | .AsType target ty => collectExprNames target; collectHighTypeNames ty
   | .IsType target ty => collectExprNames target; collectHighTypeNames ty
   | .Quantifier _ param trigger body =>
@@ -257,14 +264,17 @@ private partial def reachableNamesAux
       | none => reachableNamesAux depMap rest visited
 
 /-- Collect all names referenced by a user Laurel program. -/
-private def collectProgramRefs (prog : Laurel.Program) : CollectState :=
+private def collectProgramRefs (prog : Laurel.Program)
+    (opSeed : Operation → Option String := fun _ => none) : CollectState :=
   runCollect do
+    modify fun s => { s with opSeed := opSeed }
     prog.staticProcedures.forM collectProcDeps
     prog.types.forM collectTypeDefDeps
 
 /-- Filter a prelude Laurel program to only include declarations
     transitively needed by the user program. -/
-public def filterPrelude (prelude user : Laurel.Program)
+public def filterPrelude (prelude user : Laurel.Program) (extraSeeds : List String := [])
+    (opSeed : Operation → Option String := fun _ => none)
     : Except String Laurel.Program := do
   -- Guard: filterPrelude does not yet track dependencies through static fields
   -- or constants.  Error early if either program contains them so a silent
@@ -277,9 +287,9 @@ public def filterPrelude (prelude user : Laurel.Program)
     throw "FilterPrelude: user program contains static fields, which are not yet supported"
   unless user.constants.isEmpty do
     throw "FilterPrelude: user program contains constants, which are not yet supported"
-  let refs := collectProgramRefs user
+  let refs := collectProgramRefs user opSeed
   let depMap ← buildDependencyMap prelude
-  let seeds := refs.allNames.fold (init := []) fun acc s => s :: acc
+  let seeds := refs.allNames.fold (init := extraSeeds) fun acc s => s :: acc
   let needed := reachableNamesAux depMap seeds {}
   return { prelude with
     staticProcedures := prelude.staticProcedures.filter fun p => p.name.text ∈ needed
diff --git a/StrataTest/Languages/Laurel/FilterPreludeTest.lean b/StrataTest/Languages/Laurel/FilterPreludeTest.lean
new file mode 100644
index 0000000000..0bdecb6c0b
--- /dev/null
+++ b/StrataTest/Languages/Laurel/FilterPreludeTest.lean
@@ -0,0 +1,94 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Unit tests for `filterPrelude`'s seed handling (`extraSeeds` + `opSeed`).
+
+`filterPrelude` restricts a prelude `Program` to only the declarations
+transitively reachable from the names a user program references. Two seeding
+knobs widen that reachable set:
+
+- `opSeed : Operation → Option String` — for a primitive operator present in
+  the user program, names the prelude function a frontend's elaboration would
+  insert for it. That name is then retained as if the user had called it.
+- `extraSeeds : List String` — names retained unconditionally, regardless of
+  whether the user program references them.
+
+These tests drive `filterPrelude` directly: a small prelude with three
+functions, and user programs that do / do not contain an operator, confirming
+exactly which prelude functions survive filtering.
+-/
+
+import StrataTest.Util.TestLaurel
+import Strata.Languages.Laurel.FilterPrelude
+
+open Strata
+open Strata.Laurel
+open StrataTest.Util
+
+namespace StrataTest.Util.FilterPreludeTest
+
+/-- A prelude with three static procedures:
+    - `op_add`   : the function an `Add` operator would elaborate to (opSeed target)
+    - `unused_fn`: referenced by nothing (must be dropped unless seeded)
+    - `always_kept`: the unconditional `extraSeeds` target -/
+def preludeProgram : IO Laurel.Program := translateLaurel <|
+#strata
+program Laurel;
+function op_add(x: int, y: int): int { x };
+function unused_fn(x: int): int { x };
+function always_kept(x: int): int { x };
+#end
+
+/-- `opSeed` mapping `Add ↦ "op_add"`; every other operator is unseeded. -/
+def addOpSeed : Operation → Option String
+  | .Add => some "op_add"
+  | _ => none
+
+/-- Run `filterPrelude` and report the sorted names of the retained prelude
+    static procedures (or the error). -/
+def retainedNames (user : Laurel.Program) : IO Unit := do
+  let prelude ← preludeProgram
+  match filterPrelude prelude user (extraSeeds := ["always_kept"]) (opSeed := addOpSeed) with
+  | .error e => IO.println s!"error: {e}"
+  | .ok filtered =>
+    let names := filtered.staticProcedures.map (·.name.text)
+    IO.println (toString (names.mergeSort (· ≤ ·)))
+
+/-! ## (a) opSeed path: operator present ⇒ its prelude function is retained
+
+The user program uses `+` (a `PrimitiveOp Add`). `opSeed` maps `Add` to
+`op_add`, so `op_add` is seeded and survives filtering. `always_kept` survives
+via `extraSeeds`. `unused_fn` is referenced by nothing and is dropped. -/
+
+/-- info: [always_kept, op_add] -/
+#guard_msgs in
+#eval! do
+  let user ← translateLaurel <|
+#strata
+program Laurel;
+function useAdd(x: int, y: int): int { x + y };
+#end
+  retainedNames user
+
+/-! ## (b) no operator ⇒ opSeed function dropped; extraSeeds still retained
+
+The user program contains no `Add` operator, so `op_add` is not seeded and is
+dropped. `always_kept` is retained unconditionally via `extraSeeds`, and
+`unused_fn` is dropped. This pins that `extraSeeds` retention is unconditional
+while `opSeed` retention is gated on the operator actually appearing. -/
+
+/-- info: [always_kept] -/
+#guard_msgs in
+#eval! do
+  let user ← translateLaurel <|
+#strata
+program Laurel;
+function noOp(x: int): int { x };
+#end
+  retainedNames user
+
+end StrataTest.Util.FilterPreludeTest

From 5350774db1d27dc727ce489fdd4c4bdc6df1814a Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Fri, 26 Jun 2026 14:54:36 -0700
Subject: [PATCH 6/8] Derive gradual elaboration activeness instead of caching
 a flag

Addresses PR #1422 review (comment on gradualActive vs gradual.isSome).

The reviewer's instinct was right that storing a derived boolean is a
smell, but gradualActive cannot simply be gradual.isSome: it must also
account for GradualConfig.shouldElaborate, which keeps elaboration out of
hand-written prelude bodies and out of top-level (non-procedure) contexts.

Replace the manually save/restored gradualActive : Bool with a meaningful
currentProc : Option String (none = not inside a procedure body, mirroring
answerType/instanceTypeName), and derive activeGradual as
  gradual.filter (currentProc.elim false shouldElaborate).
Centralize the per-procedure save/restore in a withProc combinator, used by
resolveProcedure and resolveInstanceProcedure. Behavior is unchanged.
---
 Strata/Languages/Laurel/Resolution.lean | 34 ++++++++++++++-----------
 1 file changed, 19 insertions(+), 15 deletions(-)

diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index e5e358e778..121addb5fb 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -161,9 +161,10 @@ structure GradualConfig where
 structure ResolveState where
   /-- Gradual-typing elaboration config, if the frontend requested it. -/
   gradual : Option GradualConfig := none
-  /-- Whether gradual elaboration is active for the procedure being resolved.
-      Set per-procedure by `resolveProcedure` so only user code is elaborated. -/
-  gradualActive : Bool := false
+  /-- Procedure whose body is being resolved (`none` outside one); with
+      `GradualConfig.shouldElaborate` it gates gradual elaboration to user code.
+      Set/restored by `withProc`. -/
+  currentProc : Option String := none
   /-- Next fresh ID to allocate. -/
   nextId : Nat := 1
   /-- Current lexical scope (name → definition ID). -/
@@ -349,6 +350,15 @@ def withLabel (label : Option String) (action : ResolveM α) : ResolveM α := do
   modify fun s => { s with labelScope := savedLabels }
   return result
 
+/-- Run `action` as procedure `name`'s body, tracking it as the current
+    procedure (restored on exit) so `activeGradual` applies correctly. -/
+def withProc (name : String) (action : ResolveM α) : ResolveM α := do
+  let savedProc := (← get).currentProc
+  modify fun s => { s with currentProc := some name }
+  let result ← action
+  modify fun s => { s with currentProc := savedProc }
+  return result
+
 /-! ## AST traversal (Phase 1) -/
 
 
@@ -666,7 +676,7 @@ termination measure is unaffected. No-ops unless a `GradualConfig` is active. -/
 /-- The active config — `some` only inside a user procedure being elaborated. -/
 private def activeGradual : ResolveM (Option GradualConfig) := do
   let s ← get
-  return if s.gradualActive then s.gradual else none
+  return s.gradual.filter fun g => s.currentProc.elim false g.shouldElaborate
 
 /-- A `name(args)` call with its callee resolved in-pass, so phase 2 sees its id. -/
 private def mkPreludeCall (name : String) (args : List StmtExprMd)
@@ -1082,7 +1092,7 @@ def Synth.resolveStmtExpr (exprMd : StmtExprMd) : ResolveM (StmtExprMd × HighTy
     verification annotations, modifies/reads clauses). -/
 def Check.resolveStmtExpr (exprMd : StmtExprMd) (expected : HighTypeMd) : ResolveM StmtExprMd := do
   -- In user code, lower primitive ops via synthesis then coerce to `expected`.
-  if (← get).gradualActive && (exprMd.val matches .PrimitiveOp _ _ _) then
+  if (← activeGradual).isSome && (exprMd.val matches .PrimitiveOp _ _ _) then
     let (e', actual) ← Synth.resolveStmtExpr exprMd
     return ← coerceOrCheck expected actual e' exprMd.source
   match h_node: exprMd with
@@ -2856,11 +2866,8 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
     -- translator wraps every body in (`Core.Statement.block bodyLabel …`),
     -- so that frontends emitting `Exit bodyLabel` for early-return lowering
     -- (e.g. PythonToLaurel) don't trip Check.exit's label-scope check.
-    let savedGradual := (← get).gradualActive
-    modify fun s => { s with gradualActive :=
-      (s.gradual.elim false fun g => g.shouldElaborate proc.name.text) }
-    let body' ← withLabel (some bodyLabel) <| resolveBody proc.body
-    modify fun s => { s with answerType := savedAnswer, gradualActive := savedGradual }
+    let body' ← withProc proc.name.text <| withLabel (some bodyLabel) <| resolveBody proc.body
+    modify fun s => { s with answerType := savedAnswer }
     -- Transparent (static) procedure bodies are supported (#1215): the
     -- TransparencyPass derives a functional `$asFunction` copy, and the
     -- LaurelToCore translator rejects the genuinely-unsupported constructs
@@ -2902,11 +2909,8 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     let savedAnswer := (← get).answerType
     modify fun s => { s with answerType := some (outputs'.map (·.type)) }
     -- See `resolveProcedure` for the rationale on `bodyLabel`.
-    let savedGradual := (← get).gradualActive
-    modify fun s => { s with gradualActive :=
-      (s.gradual.elim false fun g => g.shouldElaborate proc.name.text) }
-    let body' ← withLabel (some bodyLabel) <| resolveBody proc.body
-    modify fun s => { s with answerType := savedAnswer, gradualActive := savedGradual }
+    let body' ← withProc proc.name.text <| withLabel (some bodyLabel) <| resolveBody proc.body
+    modify fun s => { s with answerType := savedAnswer }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     modify fun s => { s with instanceTypeName := savedInstType }
     let axioms' ← proc.axioms.mapM resolveStmtExpr

From 706a25e575bfbd2bbd875675d2fade0571a92779 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Fri, 26 Jun 2026 14:56:16 -0700
Subject: [PATCH 7/8] Fix join on the dynamic type, and clarify it is not a
 true LUB.

Addresses PR #1422 review (join, line ~763).

- Doc: join/joinAll are consistency merges, not a least upper bound (they do
  not walk the inheritance tree), so a none result means "cannot merge
  structurally", not "inconsistent".
- Fix: join only erased .Unknown, but the dynamic type is .TCore (e.g. Any),
  which isConsistent treats as top while join did not. At the if-branch merge
  this made the inferred type order-dependent: 'if c then (e:Any) else (e:int)'
  inferred Any, but the swapped branches inferred int. Add .TCore absorbing
  arms so join agrees with isConsistent (dynamic wins), plus a symmetric-branch
  regression test. The operator path is unaffected (elaborateDynamicOp
  intercepts dynamic operands before join; nativeArith gates on isNumeric).
---
 Strata/Languages/Laurel/Resolution.lean       | 27 +++++++++--------
 .../Laurel/ResolutionTypeCheckTests.lean      | 29 +++++++++++++++++++
 2 files changed, 44 insertions(+), 12 deletions(-)

diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 121addb5fb..91160822e2 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -449,16 +449,14 @@ private def isNumeric (ctx : TypeLattice) (ty : HighTypeMd) : Bool :=
   | .TInt | .TReal | .TFloat64 | .TBv _ | .Unknown => true
   | _ => false
 
-/-- Least upper bound of two types under the consistency relation
-    (Siek–Taha). On Laurel's flat lattice the join collapses to the
-    "more informative" side: `Unknown` and `T` yields `T`; equal
-    types (after unfolding) yield themselves; everything else is
-    inconsistent and yields `none`.
-
-    Used by [⇒] Op-Arith to fold operand types into a single result
-    type: a homogeneous arithmetic expression `1 + 2` yields `TInt`,
-    `1 + <?>` yields `TInt` (Unknown promotes), `<?> + <?>` yields
-    `Unknown`, and `1 + 2.0` is rejected. -/
+/-- Consistency merge of two types, keeping the more-informative side:
+    `Unknown` with `T` ⇒ `T`; the dynamic `.TCore` (e.g. `Any`) absorbs ⇒ the
+    dynamic side; equal types (after unfolding) ⇒ themselves; else `none`. Not a
+    true LUB: it doesn't walk the inheritance tree, so `none` means "cannot
+    merge structurally", not "inconsistent".
+
+    Op-Arith examples: `1 + 2` ⇒ `TInt`, `1 + <?>` ⇒ `TInt`,
+    `<?> + <?>` ⇒ `Unknown`, `1 + 2.0` rejected. -/
 private def join (ctx : TypeLattice)
     (a b : HighTypeMd) : Option HighTypeMd :=
   let a' := ctx.unfold a
@@ -466,6 +464,10 @@ private def join (ctx : TypeLattice)
   match a'.val, b'.val with
   | .Unknown, _ => some b
   | _, .Unknown => some a
+  -- Dynamic `.TCore` (e.g. `Any`) absorbs: consistent with anything, so the
+  -- merge is the dynamic side, aligning `join` with `isConsistent` on `.TCore`.
+  | .TCore _, _ => some a
+  | _, .TCore _ => some b
   | _, _ => if highEq a' b' then some a else none
 
 /-- Test whether a type is a user-defined reference type. `Unknown` is accepted
@@ -765,7 +767,8 @@ private def elaborateDynamicOp (g : GradualConfig) (op : Operation) (args' : Lis
   unless argTypes.any (fun t => g.isDynamic t.val) do return none
   forcePrelude g op args' argTypes source
 
-/-- LUB of the operand types, or `none` if inconsistent. -/
+/-- Folds `join` over the operands (consistency merge, not a true LUB), or
+    `none` if they cannot be merged. -/
 private def joinAll (ctx : TypeLattice) (argTypes : List HighTypeMd)
     (source : Option FileRange) : Option HighTypeMd :=
   argTypes.foldl
@@ -1624,7 +1627,7 @@ def Check.ifThenElse (exprMd : StmtExprMd)
     `join` (`Unknown ⊔ T = T`), so a hole branch promotes to the other
     branch's concrete type and the synthesized type is independent of
     branch order. (`isConsistent` stays the accept/reject gate: it admits
-    a lone `TCore` corner where `join` is `none`, for which the result
+    a rare multi-valued corner where `join` is `none`, for which the result
     falls back to the then-branch type, leaving that boundary unchanged.)
     Inconsistent branches (e.g. `if c then 1 else "x"`) emit a diagnostic
     and synthesize `Unknown` to suppress cascading errors. Without an
diff --git a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
index df658dbbbc..fcadb9db98 100644
--- a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
+++ b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
@@ -284,6 +284,35 @@ function foo(c: bool): bool {
 };
 #end
 
+/-! ## `if` branch join with a dynamic `Core Any` branch is symmetric
+
+`Core Any` (the gradual dynamic type, `TCore "Any"`) is consistent with every
+type, so an `if` with one `Core Any` branch and one `int` branch must
+synthesize the *same* type regardless of branch order — the dynamic type
+absorbs (`Any ⊔ int = Any`), just as a hole promotes to the concrete type.
+Both orders therefore feed a non-numeric `Core Any` into `<` and report the
+*same* diagnostic. (Before `join` handled `.TCore`, the then-first order
+returned `Any` and errored while the else-first order returned `int` and was
+silently accepted — an order-dependent type.) -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+function foo(c: bool, a: Core Any): bool {
+  (if c then a else 1) < 1
+// ^^^^^^^^^^^^^^^^^^ error: '<' expected a numeric type, got 'Core Any'
+};
+#end
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+function foo(c: bool, a: Core Any): bool {
+  (if c then 1 else a) < 1
+// ^^^^^^^^^^^^^^^^^^ error: '<' expected a numeric type, got 'Core Any'
+};
+#end
+
 /-! ## `if` branch join recovers precision from a hole
 
 When one branch is a hole (`Unknown`) and the other is a concrete numeric

From 03dda8366b96a77cf91b9ead6e29170861e84977 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Fri, 26 Jun 2026 14:57:46 -0700
Subject: [PATCH 8/8] Expand OpAlt docstring with a worked a + b example

Addresses PR #1422 review (comment on the OpAlt docstring).

Explain that an OpAlt is one candidate in the priority list firstElab walks
(none = try next, some = commit), and add a concrete a + b walkthrough under
synthArith: Any + Int commits via elaborateDynamicOp, String + String falls
to strConcatAlt, and Int + Int falls through to the native Add. Doc-only.
---
 Strata/Languages/Laurel/Resolution.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 91160822e2..77a431b507 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -804,7 +804,11 @@ private def reportMultiValued (a : StmtExprMd) (aTy : HighTypeMd) : ResolveM Boo
     pure true
   | _ => pure false
 
-/-- A candidate lowering: `some` if it applies, else `none`. -/
+/-- A candidate `PrimitiveOp` lowering, one entry in the list `firstElab` walks:
+    `none` declines (try the next), `some (expr, ty)` commits; all `none` falls
+    back to the native default. E.g. lowering `a + b`: `Any + TInt` commits via
+    `elaborateDynamicOp`, `TString + TString` via `strConcatAlt`, `TInt + TInt`
+    falls back to `nativeArith`. -/
 private abbrev OpAlt := ResolveM (Option (StmtExpr × HighTypeMd))
 
 /-- The first applicable candidate lowering, else the native `dflt`. -/