diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index 86ae83d022..658cbada38 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -100,6 +100,20 @@ inductive Operation : Type where
   | StrConcat
   deriving Repr
 
+instance : ToString Operation where
+  toString
+    | .Eq => "=="          | .Neq => "!="
+    | .And => "&&"         | .Or => "||"
+    | .Not => "!"          | .Implies => "==>"
+    | .AndThen => "&&!"    | .OrElse => "||!"
+    | .Neg => "-"          | .Add => "+"
+    | .Sub => "-"          | .Mul => "*"
+    | .Div => "/"          | .Mod => "%"
+    | .DivT => "/t"        | .ModT => "%t"
+    | .Lt => "<"           | .Leq => "<="
+    | .Gt => ">"           | .Geq => ">="
+    | .StrConcat => "++"
+
 /--
 A wrapper that pairs a value with source-level metadata such as source
 locations and annotations. All Laurel AST nodes are wrapped in
@@ -334,6 +348,40 @@ inductive ContractType where
   | Reads | Modifies | Precondition | PostCondition
 end
 
+/-- A short user-facing name for the construct, used in diagnostic messages. -/
+def StmtExpr.constrName : StmtExpr → String
+  | .IfThenElse ..       => "if"
+  | .Block ..            => "block"
+  | .While ..            => "while"
+  | .Exit ..             => "exit"
+  | .Return ..           => "return"
+  | .LiteralInt ..       => "integer literal"
+  | .LiteralBool ..      => "boolean literal"
+  | .LiteralString ..    => "string literal"
+  | .LiteralDecimal ..   => "decimal literal"
+  | .Var ..              => "variable"
+  | .Assign ..           => ":="
+  | .PureFieldUpdate ..  => "field update"
+  | .StaticCall ..       => "call"
+  | .PrimitiveOp op _    => toString op
+  | .New ..              => "new"
+  | .This                => "this"
+  | .ReferenceEquals ..  => "reference equality"
+  | .AsType ..           => "as"
+  | .IsType ..           => "is"
+  | .InstanceCall ..     => "method call"
+  | .Quantifier ..       => "quantifier"
+  | .Assigned ..         => "assigned"
+  | .Old ..              => "old"
+  | .Fresh ..            => "fresh"
+  | .Assert ..           => "assert"
+  | .Assume ..           => "assume"
+  | .ProveBy ..          => "by"
+  | .ContractOf ..       => "contractOf"
+  | .Abstract            => "abstract"
+  | .All                 => "all"
+  | .Hole ..             => "hole"
+
 @[expose] abbrev HighTypeMd := AstNode HighType
 @[expose] abbrev StmtExprMd := AstNode StmtExpr
 @[expose] abbrev VariableMd := AstNode Variable
@@ -420,6 +468,7 @@ def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.va
   | HighType.TSet t1, HighType.TSet t2 => highEq t1 t2
   | HighType.TMap k1 v1, HighType.TMap k2 v2 => highEq k1 k2 && highEq v1 v2
   | HighType.UserDefined r1, HighType.UserDefined r2 => r1.text == r2.text
+  | HighType.TCore s1, HighType.TCore s2 => s1 == s2
   | HighType.Applied b1 args1, HighType.Applied b2 args2 =>
       highEq b1 b2 && args1.length == args2.length && (args1.attach.zip args2 |>.all (fun (a1, a2) => highEq a1.1 a2))
   | HighType.Pure b1, HighType.Pure b2 => highEq b1 b2
@@ -441,6 +490,99 @@ instance : BEq HighTypeMd where
 
 deriving instance BEq for HighType
 
+/-- Lookup tables threaded through subtyping/consistency checks. Built from
+    the program's `TypeDefinition`s by the resolution pass:
+    - `unfoldMap` maps an alias or constrained type's name to the type it
+      unwraps to (alias target / constrained base). Followed transitively to
+      reach a non-alias, non-constrained type.
+    - `extendingMap` maps a composite type's name to the *direct* parents in
+      its `extending` list. Walked transitively for the subtype check. -/
+structure TypeContext where
+  unfoldMap : Std.HashMap String HighTypeMd := {}
+  extendingMap : Std.HashMap String (List String) := {}
+  deriving Inhabited
+
+/-- Unfold aliases and constrained types to their underlying type.
+    Composites and primitives are returned unchanged. A `visited` set guards
+    against cycles in the alias/constrained graph (already cycle-checked
+    elsewhere, but keeps `unfold` safe to call independently). -/
+partial def TypeContext.unfold (ctx : TypeContext) (ty : HighTypeMd)
+    (visited : Std.HashSet String := {}) : HighTypeMd :=
+  match ty.val with
+  | .UserDefined name =>
+    if visited.contains name.text then ty
+    else match ctx.unfoldMap.get? name.text with
+      | some target => ctx.unfold target (visited.insert name.text)
+      | none => ty
+  | _ => ty
+
+/-- All ancestors of a composite type (including itself), reachable via
+    repeated `extending` lookups. The `fuel` cap is the number of distinct
+    type names ever registered, bounding the BFS even with malformed input. -/
+partial def TypeContext.ancestors (ctx : TypeContext) (name : String) : Std.HashSet String :=
+  let rec go (acc : Std.HashSet String) (frontier : List String) : Std.HashSet String :=
+    match frontier with
+    | [] => acc
+    | n :: rest =>
+      if acc.contains n then go acc rest
+      else
+        let acc' := acc.insert n
+        let parents := (ctx.extendingMap.get? n).getD []
+        go acc' (parents ++ rest)
+  go {} [name]
+
+/-- Pure subtyping `<:`. Walks the `extending` chain for `CompositeType`
+    (via `TypeContext.ancestors`), unfolds `TypeAlias` to its target, and
+    unwraps `ConstrainedType` to its base (both via `TypeContext.unfold`),
+    then falls back to structural equality via `highEq`.
+
+    Used together with `isConsistent` to form `isConsistentSubtype`, which
+    is what the bidirectional checker invokes at every check-mode boundary
+    (rule `[⇐] Sub`). -/
+def isSubtype (ctx : TypeContext) (sub sup : HighTypeMd) : Bool :=
+  let sub' := ctx.unfold sub
+  let sup' := ctx.unfold sup
+  match sub'.val, sup'.val with
+  | .UserDefined subName, .UserDefined supName =>
+    -- After unfolding, both sides are composites (or unresolved). A composite
+    -- is a subtype of any type in its extending chain.
+    (ctx.ancestors subName.text).contains supName.text || highEq sub' sup'
+  | _, _ => highEq sub' sup'
+
+/-- Consistency `~` (Siek–Taha): the symmetric gradual relation. `Unknown`
+    is the dynamic type and is consistent with everything; otherwise
+    structural equality after unfolding aliases / constrained types.
+
+    Used directly by `[⇒] Op-Eq`, where the operand types must be mutually
+    consistent (no subtype direction is privileged), and as one half of
+    `isConsistentSubtype`. -/
+def isConsistent (ctx : TypeContext) (a b : HighTypeMd) : Bool :=
+  let a' := ctx.unfold a
+  let b' := ctx.unfold b
+  match a'.val, b'.val with
+  | .Unknown, _ | _, .Unknown => true
+  | _, _ => highEq a' b'
+
+/-- Consistent subtyping: `∃ R. sub ~ R ∧ R <: sup`. For our flat lattice
+    this collapses to `sub ~ sup ∨ sub <: sup` — the standard collapse.
+
+    Used by rule `[⇐] Sub` (and every bespoke check rule). That single
+    choice is what makes the system *gradual*: an expression of type
+    `Unknown` (a hole, an unresolved name, a `Hole _ none`) flows freely
+    into any typed slot, and any expression flows freely into a slot of
+    type `Unknown`. Strict checking is applied between fully-known types
+    only.
+
+    A previous iteration was synth-only with two *bivariantly-compatible*
+    wildcards: `Unknown` and `UserDefined`. The `UserDefined` carve-out was
+    load-bearing: no assignment, call argument, or comparison involving a
+    user type was ever rejected. The bidirectional design retires that
+    carve-out — user-defined types are now a regular participant in `<:`,
+    with `isSubtype` walking inheritance chains and unwrapping aliases
+    and constrained types to deliver real checking on user-defined code. -/
+def isConsistentSubtype (ctx : TypeContext) (sub sup : HighTypeMd) : Bool :=
+  isConsistent ctx sub sup || isSubtype ctx sub sup
+
 def HighType.isBool : HighType → Bool
   | TBool => true
   | _ => false
@@ -578,6 +720,19 @@ def TypeDefinition.name : TypeDefinition → Identifier
   | .Datatype ty => ty.name
   | .Alias ty => ty.name
 
+/-- Build a `TypeContext` from a list of `TypeDefinition`s.
+    Aliases populate `unfoldMap` with their target; constrained types populate
+    it with their base; composites populate `extendingMap` with their direct
+    parents. Datatypes contribute nothing — they're nominal and irreducible. -/
+def TypeContext.ofTypes (types : List TypeDefinition) : TypeContext :=
+  types.foldl (init := {}) fun ctx td =>
+    match td with
+    | .Alias ta => { ctx with unfoldMap := ctx.unfoldMap.insert ta.name.text ta.target }
+    | .Constrained ct => { ctx with unfoldMap := ctx.unfoldMap.insert ct.name.text ct.base }
+    | .Composite c =>
+      { ctx with extendingMap := ctx.extendingMap.insert c.name.text (c.extending.map (·.text)) }
+    | .Datatype _ => ctx
+
 structure Constant where
   name : Identifier
   type : HighTypeMd
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 16bcf1333f..0e002ec048 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -13,24 +13,73 @@ import Strata.Languages.Python.PythonLaurelCorePrelude
 /-!
 # Name Resolution Pass
 
-Assigns a unique numeric ID to every definition and reference node in a
-Laurel program, then resolves references to their definitions.
+Turns a freshly parsed Laurel `Program` (where every `Identifier` has
+`uniqueId := none`) into a program where every definition has a fresh numeric
+ID and every reference points to the ID of the definition it names. The pass
+also synthesizes a `HighType` for every `StmtExpr` and emits diagnostics for
+unresolved names, duplicate definitions, kind mismatches (e.g. using a
+constant where a type is expected), and type mismatches.
+
+The entry point is `resolve`. It returns a `ResolutionResult` containing the
+resolved program, a `SemanticModel` (the `refToDef` map and ID counters), and
+the accumulated diagnostics.
 
 ## Design
 
-The resolution pass operates in two phases:
+The resolution pass operates in two phases.
 
 ### Phase 1: ID Assignment and Reference Resolution
-Walks the AST, assigning fresh unique IDs to all definition nodes and
-resolving references by looking up names in the current lexical scope.
-After this phase, every definition and reference node has its `id` field
-filled in.
+
+Walks the AST under `ResolveM`, a state monad over `ResolveState`. Phase 1:
+- assigns fresh unique IDs to all definition nodes via `defineNameCheckDup`,
+- resolves references by looking up names in the current lexical scope via
+  `resolveRef` (and `resolveFieldRef` for fields, which uses the target's
+  declared type to build a qualified lookup key),
+- opens fresh nested scopes via `withScope` for blocks, quantifiers,
+  procedure bodies, and constrained-type constraint/witness expressions,
+- synthesizes a `HighType` for every `StmtExpr` and checks it (via
+  `Check.resolveStmtExpr` for fresh subexpressions, or `checkSubtype` when a type is
+  already in hand) on assignments, call arguments, condition positions,
+  functional bodies, and constant initializers.
+
+Before any bodies are walked, `preRegisterTopLevel` registers every top-level
+name (types and their constructors / testers / destructors / instance
+procedures / fields, constants, static procedures) into scope with a
+placeholder `ResolvedNode`. The placeholders are overwritten with real nodes
+as each definition is fully resolved. This is what allows declaration order to
+not matter inside a Laurel program.
+
+When a reference fails to resolve, or a `UserDefined` type reference resolves
+to the wrong kind, Phase 1 records the name as `ResolvedNode.unresolved` (or
+the type as `HighType.Unknown`) and continues. Both are treated as wildcards
+by the type checker, so subsequent uses do not produce cascading errors.
+
+After this phase, every definition and reference node has its `uniqueId`
+field filled in.
 
 ### Phase 2: Build refToDef Map
+
 Walks the *resolved* AST (where all definitions already have their UUIDs)
-and builds a map from each definition's ID to its `ResolvedNode`. Because this
-happens after Phase 1, the `ResolvedNode` values in the map contain the fully
-resolved sub-trees (e.g. a procedure's parameters already have their IDs).
+and builds a map from each definition's ID to its `ResolvedNode`. Because
+this happens after Phase 1, the `ResolvedNode` values in the map contain the
+fully resolved sub-trees (e.g. a procedure's parameters already have their
+IDs).
+
+### Scopes
+
+Three forms of scope are maintained on `ResolveState`:
+- `scope` — the current lexical scope, mapping name → `(uniqueId, ResolvedNode)`,
+  saved and restored by `withScope`.
+- `currentScopeNames` — names defined at the current nesting level only, used
+  by `defineNameCheckDup` to detect duplicates.
+- `typeScopes` — per-composite-type scopes mapping field names to scope
+  entries. Built by `resolveTypeDefinition` *before* descending into instance
+  procedures (and inheriting from `extending` parents), so that field
+  references inside method bodies can be resolved.
+- `instanceTypeName` — when resolving inside an instance procedure, the
+  owning composite type's name. Used by `resolveFieldRef` as a fallback so
+  that a bare `self.field` reference resolves through the type scope when
+  `self` has type `Any`.
 
 ### Definition nodes (introduce a name into scope)
 - `Variable.Declare` — local variable declaration (in `Assign` targets or `Var`)
@@ -51,10 +100,10 @@ resolved sub-trees (e.g. a procedure's parameters already have their IDs).
 - `StmtExpr.Exit` — exit a labelled block
 - `HighType.UserDefined` — type reference
 
-Each of these nodes carries an `id : Nat` field (defaulting to `0`).
-The ID assignment pass fills in unique values. The resolution pass then
-builds a map from reference IDs to `ResolvedNode` values describing the
-definition each reference resolves to.
+Each of these nodes carries a `uniqueId : Option Nat` field (defaulting to
+`none`). Phase 1 fills in unique values; Phase 2 then builds a map from
+reference IDs to `ResolvedNode` values describing the definition each
+reference resolves to.
 -/
 
 namespace Strata.Laurel
@@ -204,6 +253,12 @@ structure ResolveState where
   nextId : Nat := 1
   /-- Current lexical scope (name → definition ID). -/
   scope : Scope := {}
+  /-- Map from definition uniqueId to its ResolvedNode. Populated alongside
+      `scope` whenever a definition is registered. Unlike `scope`, this map is
+      *not* saved/restored by `withScope` — uniqueIds are global. Used by
+      `getVarType` to look up types for references whose `text` doesn't match
+      a scope key (notably fields, which are scoped under qualified keys). -/
+  idToNode : Std.HashMap Nat ResolvedNode := {}
   /-- Names defined at the current scope level (for duplicate detection). -/
   currentScopeNames : Std.HashSet String := {}
   /-- Per-composite-type field scopes (type name → field name → scope entry). -/
@@ -213,6 +268,14 @@ structure ResolveState where
   /-- When resolving inside an instance procedure, the owning composite type name.
       Used by `resolveFieldRef` to resolve `self.field` when `self` has type `Any`. -/
   instanceTypeName : Option String := none
+  /-- When resolving inside a procedure body, the declared output types (in
+      declaration order). `none` means no enclosing procedure. Used by `Return`
+      to type-check the optional return value and to flag arity/shape mismatches. -/
+  expectedReturnTypes : Option (List HighTypeMd) := none
+  /-- Type-relation tables (alias/constrained unfolding + composite extending
+      chains) used by the subtyping/consistency checks. Built once from
+      `program.types` at the start of `resolve`. -/
+  typeContext : TypeContext := {}
 
 @[expose] abbrev ResolveM := StateM ResolveState
 
@@ -243,8 +306,10 @@ def defineNameCheckDup (iden : Identifier) (node : ResolvedNode) (overrideResolu
         let id ← freshId
         pure ({ iden with uniqueId := some (id) }, id)
 
-    modify fun s => { s with scope := s.scope.insert resolutionName (uniqueId, node),
-                             currentScopeNames := s.currentScopeNames.insert resolutionName }
+    modify fun s => { s with
+      scope := s.scope.insert resolutionName (uniqueId, node),
+      idToNode := s.idToNode.insert uniqueId node,
+      currentScopeNames := s.currentScopeNames.insert resolutionName }
     return name'
 
 /-- Resolve a reference: look up the name in scope and assign the definition's ID.
@@ -326,7 +391,14 @@ def resolveHighType (ty : HighTypeMd) : ResolveM HighTypeMd := do
   | .UserDefined ref =>
     let ref' ← resolveRef ref ty.source
       (expected := #[.compositeType, .constrainedType, .datatypeDefinition, .typeAlias])
-    pure (.UserDefined ref')
+    -- If the reference resolved to the wrong kind, treat the type as Unknown to avoid cascading errors
+    let s ← get
+    let kindOk : Bool := match s.scope.get? ref.text with
+      | some (_, node) => node.kind == .unresolved ||
+          (#[ResolvedNodeKind.compositeType, .constrainedType, .datatypeDefinition, .typeAlias].contains node.kind)
+      | none => true  -- unresolved references already reported
+    if kindOk then pure (HighType.UserDefined ref')
+    else pure HighType.Unknown
   | .TTypedField vt =>
     let vt' ← resolveHighType vt
     pure (.TTypedField vt')
@@ -353,157 +425,1109 @@ def resolveHighType (ty : HighTypeMd) : ResolveM HighTypeMd := do
   | other => pure other
   return { val := val', source := ty.source }
 
-def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do
-  match _: exprMd with
+/-- Format a type for use in diagnostics. -/
+private def formatType (ty : HighTypeMd) : String :=
+  match ty.val with
+  | .MultiValuedExpr tys =>
+    let parts := tys.map (fun t => toString (formatHighTypeVal t.val))
+    "(" ++ ", ".intercalate parts ++ ")"
+  | other => toString (formatHighTypeVal other)
+
+/-- Emit a type mismatch diagnostic. With a `construct`, the message is
+    "'<construct.constrName>' <problem>, got '<actual>'"; without,
+    "<problem>, got '<actual>'". When `actual` is `Unknown` the trailing
+    `got '…'` is dropped — "we couldn't synthesize a type" is the
+    statement, not "the type we got was Unknown". -/
+private def typeMismatch (source : Option FileRange) (construct : Option StmtExpr)
+    (problem : String) (actual : HighTypeMd) : ResolveM Unit := do
+  let constructor := match construct with
+    | some c => s!"'{c.constrName}' "
+    | none   => ""
+  let suffix := match actual.val with
+    | .Unknown => ""
+    | _        => s!", got '{formatType actual}'"
+  let diag := diagnosticFromSource source s!"{constructor}{problem}{suffix}"
+  modify fun s => { s with errors := s.errors.push diag }
+
+/-- Type-level subtype check: emits the standard "expected/got" diagnostic when
+    `actual` is not a consistent subtype of `expected`. Used at sites where the
+    actual type is already in hand (assignment, call args, body vs declared
+    output) — equivalent to `Check.resolveStmtExpr e expected` but without re-synthesizing. -/
+private def checkSubtype (source : Option FileRange) (expected : HighTypeMd) (actual : HighTypeMd) : ResolveM Unit := do
+  let ctx := (← get).typeContext
+  unless isConsistentSubtype ctx actual expected do
+    typeMismatch source none s!"expected '{formatType expected}'" actual
+
+/-- Test whether a type is in the set of numeric primitives. `Unknown` is
+    accepted as a gradual escape hatch. Aliases and constrained types are
+    unfolded first so e.g. `nat` (constrained over `int`) counts as numeric.
+    Used by Op-Cmp / Op-Arith. -/
+private def isNumeric (ctx : TypeContext) (ty : HighTypeMd) : Bool :=
+  match (ctx.unfold ty).val with
+  | .TInt | .TReal | .TFloat64 | .Unknown => true
+  | _ => false
+
+/-- Test whether a type is a user-defined reference type. `Unknown` is accepted
+    as a gradual escape hatch. Used by Fresh and ReferenceEquals, which only
+    make sense on composite/datatype references. -/
+private def isReference (ctx : TypeContext) (ty : HighTypeMd) : Bool :=
+  match (ctx.unfold ty).val with
+  | .UserDefined _ | .Unknown => true
+  | _ => false
+
+/-- Get the type of a resolved reference. Tries the lexical scope by name
+    first; if that misses (notably for fields, which are scoped under
+    qualified keys like "Container.intValue"), falls back to a uniqueId
+    lookup populated as definitions are registered. -/
+private def getVarType (ref : Identifier) : ResolveM HighTypeMd := do
+  let s ← get
+  match s.scope.get? ref.text with
+  | some (_, node) => pure node.getType
+  | none =>
+    match ref.uniqueId.bind s.idToNode.get? with
+    | some node => pure node.getType
+    | none => pure { val := .Unknown, source := ref.source }
+
+/-- Get the call return type and parameter types for a callee from scope. -/
+private def getCallInfo (callee : Identifier) : ResolveM (HighTypeMd × List HighTypeMd) := do
+  let s ← get
+  match s.scope.get? callee.text with
+  | some (_, .staticProcedure proc) =>
+    let retTy := match proc.outputs with
+      | [singleOutput] => singleOutput.type
+      | outputs => { val := .MultiValuedExpr (outputs.map (·.type)), source := none }
+    pure (retTy, proc.inputs.map (·.type))
+  | some (_, .instanceProcedure _ proc) =>
+    let retTy := match proc.outputs with
+      | [singleOutput] => singleOutput.type
+      | outputs => { val := .MultiValuedExpr (outputs.map (·.type)), source := none }
+    pure (retTy, proc.inputs.map (·.type))
+  | some (_, .datatypeConstructor t _) =>
+    -- Testers (e.g. "Color..isRed") return Bool; constructors return the type
+    if (callee.text.splitOn "..is").length > 1 then
+      pure ({ val := .TBool, source := callee.source }, [])
+    else
+      pure ({ val := .UserDefined t, source := callee.source }, [])
+  | some (_, .parameter p) => pure (p.type, [])
+  | some (_, .constant c) => pure (c.type, [])
+  | _ => pure ({ val := .Unknown, source := callee.source }, [])
+
+/-! ## Typing rules
+
+Each typing rule from the Laurel manual 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 — `Check.assign`
+- Calls — `Synth.staticCall`, `Synth.instanceCall`
+- Primitive operations — `Synth.primitiveOp`
+- Object forms — `Synth.new`, `Synth.asType`, `Synth.isType`, `Synth.refEq`,
+  `Synth.pureFieldUpdate`
+- Verification expressions — `Synth.quantifier`, `Synth.assigned`,
+  `Synth.fresh`, `Check.old`, `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.
+`Synth.resolveStmtExpr` is non-total: constructors without a synthesis rule
+hit a wildcard arm that emits a diagnostic and returns `Unknown`. -/
+
+namespace Resolution
+
+-- 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
+-- `decreasing_by` tactic to relate `sizeOf args` to `sizeOf exprMd`.
+set_option linter.unusedVariables false in
+mutual
+
+-- ### Dispatch
+
+/-- Synth-mode resolution: resolve `e` and synthesize its `HighType`,
+    written `Γ ⊢ e ⇒ T`. Each constructor with a synthesis rule delegates
+    to its rule's helper; constructors without one (statement-shaped
+    constructs like `IfThenElse`, `Block`, `While`, `Return`, `Assign`,
+    …) hit a wildcard arm that emits a `typeMismatch` diagnostic and
+    returns `Unknown` to suppress cascading errors.
+
+    Synthesis returns a type inferred from the expression itself;
+    checking (`Check.resolveStmtExpr`) verifies that the expression has
+    a given expected type. The two functions are mutually recursive,
+    with termination on a lexicographic measure `(exprMd, tag)` — tag
+    `2` for synth, `3` for check, helpers smaller — so that subsumption
+    (which calls synth on the *same* expression) can decrease via
+    `Prod.Lex.right`. -/
+def Synth.resolveStmtExpr (exprMd : StmtExprMd) : ResolveM (StmtExprMd × HighTypeMd) := do
+  match h_node: exprMd with
   | AstNode.mk expr source =>
-  let val' ← match _: expr with
-  | .IfThenElse cond thenBr elseBr =>
-    let cond' ← resolveStmtExpr cond
-    let thenBr' ← resolveStmtExpr thenBr
-    let elseBr' ← elseBr.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val)
-    pure (.IfThenElse cond' thenBr' elseBr')
-  | .Block stmts label =>
-    withScope do
-      let stmts' ← stmts.mapM resolveStmtExpr
-      pure (.Block stmts' label)
-  | .While cond invs dec body =>
-    let cond' ← resolveStmtExpr cond
-    let invs' ← invs.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val)
-    let dec' ← dec.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val)
-    let body' ← resolveStmtExpr body
-    pure (.While cond' invs' dec' body')
-  | .Exit target => pure (.Exit target)
-  | .Return val => do
-    let val' ← val.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val)
-    pure (.Return val')
-  | .LiteralInt v => pure (.LiteralInt v)
-  | .LiteralBool v => pure (.LiteralBool v)
-  | .LiteralString v => pure (.LiteralString v)
-  | .LiteralDecimal v => pure (.LiteralDecimal v)
-  | .Var (.Local ref) =>
-    let ref' ← resolveRef ref source
-    pure (.Var (.Local ref'))
-  | .Var (.Declare param) =>
-    let ty' ← resolveHighType param.type
-    let name' ← defineNameCheckDup param.name (.var param.name ty')
-    pure (.Var (.Declare ⟨name', ty'⟩))
-  | .Assign targets value =>
-    let targets' ← targets.attach.mapM fun ⟨v, _⟩ => do
-      let ⟨vv, vs⟩ := v
-      match vv with
-      | .Local ref =>
-        let ref' ← resolveRef ref source
-        pure (⟨.Local ref', vs⟩ : VariableMd)
-      | .Field target fieldName =>
-        let target' ← resolveStmtExpr target
-        let fieldName' ← resolveFieldRef target' fieldName source
-        pure (⟨.Field target' fieldName', vs⟩ : VariableMd)
-      | .Declare param =>
-        let ty' ← resolveHighType param.type
-        let name' ← defineNameCheckDup param.name (.var param.name ty')
-        pure (⟨.Declare ⟨name', ty'⟩, vs⟩ : VariableMd)
-    let value' ← resolveStmtExpr value
-    -- Check that LHS target count matches the number of outputs from the RHS.
-    -- This fires for procedure calls (which can have multiple outputs).
-    -- Functions always have exactly 1 output in the model, so single-target function calls pass trivially.
-    let expectedOutputCount ← match value'.val with
-      | .StaticCall callee _ => do
-        let s ← get
-        match s.scope.get? callee.text with
-        | some (_, .staticProcedure proc) => pure proc.outputs.length
-        | some (_, .instanceProcedure _ proc) => pure proc.outputs.length
-        | _ => pure 1
-      | .InstanceCall _ callee _ => do
-        let s ← get
-        match s.scope.get? callee.text with
-        | some (_, .instanceProcedure _ proc) => pure proc.outputs.length
-        | some (_, .staticProcedure proc) => pure proc.outputs.length
-        | _ => pure 1
-      | _ => pure 1
-    if targets'.length != expectedOutputCount then
-      let diag := diagnosticFromSource source
-        s!"Assignment target count mismatch: {targets'.length} targets but right-hand side produces {expectedOutputCount} values"
-      modify fun s => { s with errors := s.errors.push diag }
-    pure (.Assign targets' value')
+  let (val', ty) ← match h_expr: expr with
+  | .LiteralInt v => pure (Synth.litInt v source)
+  | .LiteralBool v => pure (Synth.litBool v source)
+  | .LiteralString v => pure (Synth.litString v source)
+  | .LiteralDecimal v => pure (Synth.litDecimal v source)
+  | .Var (.Local ref) => Synth.varLocal ref source
   | .Var (.Field target fieldName) =>
-    let target' ← resolveStmtExpr target
-    let fieldName' ← resolveFieldRef target' fieldName source
-    pure (.Var (.Field target' fieldName'))
+    Synth.varField exprMd target fieldName source (by rw [h_node])
   | .PureFieldUpdate target fieldName newVal =>
-    let target' ← resolveStmtExpr target
-    let fieldName' ← resolveFieldRef target' fieldName source
-    let newVal' ← resolveStmtExpr newVal
-    pure (.PureFieldUpdate target' fieldName' newVal')
+    Synth.pureFieldUpdate exprMd target fieldName newVal (by rw [h_node])
   | .StaticCall callee args =>
-    let callee' ← resolveRef callee source
-      (expected := #[.parameter, .staticProcedure, .datatypeConstructor, .constant])
-    let args' ← args.mapM resolveStmtExpr
-    pure (.StaticCall callee' args')
+    Synth.staticCall exprMd callee args source (by rw [h_node])
   | .PrimitiveOp op args =>
-    let args' ← args.mapM resolveStmtExpr
-    pure (.PrimitiveOp op args')
-  | .New ref =>
-    let ref' ← resolveRef ref source
-      (expected := #[.compositeType, .datatypeDefinition])
-    pure (.New ref')
-  | .This => pure .This
+    Synth.primitiveOp exprMd expr op args source h_expr (by rw [h_node])
+  | .New ref => Synth.new ref source
+  | .This => Synth.this source
   | .ReferenceEquals lhs rhs =>
-    let lhs' ← resolveStmtExpr lhs
-    let rhs' ← resolveStmtExpr rhs
-    pure (.ReferenceEquals lhs' rhs')
+    Synth.refEq exprMd expr lhs rhs source h_expr (by rw [h_node])
   | .AsType target ty =>
-    let target' ← resolveStmtExpr target
-    let ty' ← resolveHighType ty
-    pure (.AsType target' ty')
+    Synth.asType exprMd target ty (by rw [h_node])
   | .IsType target ty =>
-    let target' ← resolveStmtExpr target
-    let ty' ← resolveHighType ty
-    pure (.IsType target' ty')
+    Synth.isType exprMd target ty source (by rw [h_node])
   | .InstanceCall target callee args =>
-    let target' ← resolveStmtExpr target
-    let callee' ← resolveRef callee source
-      (expected := #[.instanceProcedure, .staticProcedure])
-    let args' ← args.mapM resolveStmtExpr
-    pure (.InstanceCall target' callee' args')
+    Synth.instanceCall exprMd target callee args source (by rw [h_node])
   | .Quantifier mode param trigger body =>
-    withScope do
-      let paramTy' ← resolveHighType param.type
-      let paramName' ← defineNameCheckDup param.name (.quantifierVar param.name paramTy')
-      let trigger' ← trigger.attach.mapM (fun pv => have := pv.property; resolveStmtExpr pv.val)
-      let body' ← resolveStmtExpr body
-      pure (.Quantifier mode ⟨paramName', paramTy'⟩ trigger' body')
+    Synth.quantifier exprMd mode param trigger body source (by rw [h_node])
   | .Assigned name =>
-    let name' ← resolveStmtExpr name
-    pure (.Assigned name')
-  | .Old val =>
-    let val' ← resolveStmtExpr val
-    pure (.Old val')
+    Synth.assigned exprMd name source (by rw [h_node])
   | .Fresh val =>
-    let val' ← resolveStmtExpr val
-    pure (.Fresh val')
+    Synth.fresh exprMd expr val source h_expr (by rw [h_node])
+  | .ContractOf ty fn =>
+    Synth.contractOf exprMd ty fn source (by rw [h_node])
+  | .Abstract => pure (Synth.abstract source)
+  | .All => pure (Synth.all source)
+  | _ =>
+    let unknown : HighTypeMd := { val := .Unknown, source := source }
+    typeMismatch source (some expr)
+      "has no synthesis rule; use it in a position with a known expected type"
+      unknown
+    pure (expr, unknown)
+  return ({ val := val', source := source }, ty)
+  termination_by (exprMd, 2)
+  decreasing_by all_goals first
+    | (apply Prod.Lex.left; term_by_mem)
+    | (try subst h_node; apply Prod.Lex.right; decide)
+    | (apply Prod.Lex.right; decide)
+
+/-- Check-mode resolution (rule **Sub** at the boundary): resolve `e` and
+    verify its type is a consistent subtype of `expected`, written
+    `Γ ⊢ e ⇐ T`. Bidirectional rules for individual constructs push
+    `expected` into subexpressions rather than bouncing through
+    synthesis, which keeps error messages localized and lets the
+    expected type propagate through nested control flow. Constructs
+    with a dedicated `Check.<construct>` rule:
+
+    - bindings — `Var (.Declare …)`, `Assign`
+    - control flow — `Block`, `IfThenElse`, `While`, `Exit`, `Return`
+    - verification — `Assert`, `Assume`, `Old`, `ProveBy`
+    - holes — `Hole` (typed and untyped)
+
+    Everything else falls back to subsumption — synthesize, then verify
+    `isConsistentSubtype actual expected`.
+
+    The right principle for new call sites is: when the position has a
+    known expected type (`TBool` for conditions, numeric for `decreases`,
+    the declared output for a constant initializer or a functional body),
+    use `Check.resolveStmtExpr`. When it doesn't, use `resolveStmtExpr`
+    (a thin wrapper that calls `Synth.resolveStmtExpr` and discards the
+    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
+  match h_node: exprMd with
+  | AstNode.mk expr source =>
+  match h_expr: expr with
+  | .Block stmts label =>
+    Check.block exprMd stmts label expected source (by rw [h_node])
+  | .IfThenElse cond thenBr elseBr =>
+    Check.ifThenElse exprMd cond thenBr elseBr expected source (by rw [h_node])
+  | .Assign targets value =>
+    Check.assign exprMd targets value expected source (by rw [h_node])
+  | .Hole det none => pure (Check.holeNone det expected source)
+  | .Hole det (some ty) => Check.holeSome det ty expected source
+  | .Var (.Declare param) => Check.varDeclare param expected source
+  | .While cond invs dec body =>
+    Check.while exprMd cond invs dec body expected source (by rw [h_node])
+  | .Exit target => Check.exit target expected source
+  | .Return val =>
+    Check.return exprMd val expected source (by rw [h_node])
   | .Assert ⟨condExpr, summary⟩ =>
-    let cond' ← resolveStmtExpr condExpr
-    pure (.Assert { condition := cond', summary })
+    Check.assert exprMd condExpr summary expected source (by rw [h_node])
   | .Assume cond =>
-    let cond' ← resolveStmtExpr cond
-    pure (.Assume cond')
+    Check.assume exprMd cond expected source (by rw [h_node])
+  | .Old val =>
+    Check.old exprMd val expected source (by rw [h_node])
   | .ProveBy val proof =>
-    let val' ← resolveStmtExpr val
-    let proof' ← resolveStmtExpr proof
-    pure (.ProveBy val' proof')
-  | .ContractOf ty fn =>
-    let fn' ← resolveStmtExpr fn
-    pure (.ContractOf ty fn')
-  | .Abstract => pure .Abstract
-  | .All => pure .All
-  | .Hole det type => match type with
-    | some ty =>
-      let ty' ← resolveHighType ty
-      pure (.Hole det ty')
-    | none => pure (.Hole det none)
-  return { val := val', source := source }
-  termination_by exprMd
-  decreasing_by all_goals term_by_mem
+    Check.proveBy exprMd val proof expected source (by rw [h_node])
+  | _ =>
+    -- Subsumption fallback: synth then check `actual <: expected`.
+    let (e', actual) ← Synth.resolveStmtExpr exprMd
+    checkSubtype source expected actual
+    pure e'
+  termination_by (exprMd, 3)
+  decreasing_by all_goals first
+    | (apply Prod.Lex.left; term_by_mem)
+    | (try subst_eqs; apply Prod.Lex.right; decide)
+    | (try subst h_node; apply Prod.Lex.right; decide)
+    | (apply Prod.Lex.right; decide)
+
+-- ### Literals
+
+/-- `Γ ⊢ LiteralInt n ⇒ TInt` -/
+def Synth.litInt (v : Int) (source : Option FileRange) : StmtExpr × HighTypeMd :=
+  (.LiteralInt v, { val := .TInt, source := source })
+
+/-- `Γ ⊢ LiteralBool b ⇒ TBool` -/
+def Synth.litBool (v : Bool) (source : Option FileRange) : StmtExpr × HighTypeMd :=
+  (.LiteralBool v, { val := .TBool, source := source })
+
+/-- `Γ ⊢ LiteralString s ⇒ TString` -/
+def Synth.litString (v : String) (source : Option FileRange) : StmtExpr × HighTypeMd :=
+  (.LiteralString v, { val := .TString, source := source })
+
+/-- `Γ ⊢ LiteralDecimal d ⇒ TReal` -/
+def Synth.litDecimal (v : Decimal) (source : Option FileRange) : StmtExpr × HighTypeMd :=
+  (.LiteralDecimal v, { val := .TReal, source := source })
+
+-- ### Variables
+
+/-- `Γ(x) = T  ∴  Γ ⊢ Var (.Local x) ⇒ T`
+
+    Resolves `ref` against the lexical scope and reads its declared type. -/
+def Synth.varLocal (ref : Identifier) (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let ref' ← resolveRef ref source
+  let ty ← getVarType ref
+  pure (.Var (.Local ref'), ty)
+
+/-- `Γ ⊢ e ⇒ _,  Γ(f) = T_f  ∴  Γ ⊢ Var (.Field e f) ⇒ T_f`
+
+    `f` is looked up against the type of `e` (or the enclosing instance type
+    for `self.f`); the typing rule itself is path-agnostic. -/
+def Synth.varField (exprMd : StmtExprMd)
+    (target : StmtExprMd) (fieldName : Identifier) (source : Option FileRange)
+    (h : exprMd.val = .Var (.Field target fieldName)) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let (target', _) ← Synth.resolveStmtExpr target
+  let fieldName' ← resolveFieldRef target' fieldName source
+  let ty ← getVarType fieldName'
+  pure (.Var (.Field target' fieldName'), ty)
+  termination_by (exprMd, 1)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    try simp_all
+    omega
+
+/-- `x ∉ dom(Γ),  TVoid <: T  ∴  Γ ⊢ Var (.Declare ⟨x, T_x⟩) ⇐ T ⊣ Γ, x : T_x`
+
+    `⊣ Γ, x : T_x` records that the surrounding scope is extended with the
+    new binding for the remainder of the enclosing scope. The declaration
+    itself produces no value, so `expected` must admit `TVoid`. -/
+def Check.varDeclare (param : Parameter)
+    (expected : HighTypeMd) (source : Option FileRange) :
+    ResolveM StmtExprMd := do
+  let ty' ← resolveHighType param.type
+  let name' ← defineNameCheckDup param.name (.var param.name ty')
+  checkSubtype source expected { val := .TVoid, source := source }
+  pure { val := .Var (.Declare ⟨name', ty'⟩), source := source }
+
+-- ### Control flow
+
+/-- `Γ ⊢ cond ⇐ TBool,  Γ ⊢ invs_i ⇐ TBool,  Γ ⊢ dec ⇐ ?,  Γ ⊢ body ⇐ T,  TVoid <: T  ∴  Γ ⊢ While cond invs dec body ⇐ T`
+
+    `cond` is checked against `TBool`, each invariant against `TBool`,
+    optional `decreases` is currently resolved without a type check (the
+    intended target is a numeric type), and the body is checked against
+    the surrounding `expected` type. The construct itself produces no
+    value, so `expected` must admit `TVoid`. -/
+def Check.while (exprMd : StmtExprMd)
+    (cond : StmtExprMd) (invs : List StmtExprMd)
+    (dec : Option StmtExprMd) (body : StmtExprMd)
+    (expected : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .While cond invs dec body) :
+    ResolveM StmtExprMd := do
+  let cond' ← Check.resolveStmtExpr cond { val := .TBool, source := cond.source }
+  let invs' ← invs.attach.mapM (fun a => have := a.property; do
+    Check.resolveStmtExpr a.val { val := .TBool, source := a.val.source })
+  let dec' ← dec.attach.mapM (fun a => have := a.property; do
+    let (e', _) ← Synth.resolveStmtExpr a.val; pure e')
+  let body' ← Check.resolveStmtExpr body expected
+  checkSubtype source expected { val := .TVoid, source := source }
+  pure { val := .While cond' invs' dec' body', source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      try (have := List.sizeOf_lt_of_mem ‹_ ∈ invs›)
+      try simp_all
+      omega
+
+/-- `Γ ⊢ Exit target ⇐ T`
+
+    `exit` is a control-flow jump out of a labeled block; it doesn't
+    deliver a value to the enclosing block, so no subsumption against
+    `expected` is required. -/
+def Check.exit (target : String) (_expected : HighTypeMd)
+    (source : Option FileRange) : ResolveM StmtExprMd := do
+  pure { val := .Exit target, source := source }
+
+/-- Cases on whether the return value is `none` or `some e`, and on the
+    arity of the enclosing procedure's declared outputs.
+
+    `Γ ⊢ Return none ⇐ T`
+
+    `Γ_proc.outputs = [T_o],  Γ ⊢ e ⇐ T_o  ∴  Γ ⊢ Return (some e) ⇐ T`
+
+    `Γ_proc.outputs = []  ∴  Γ ⊢ Return (some e) ↝ error: "void procedure cannot return a value"`
+
+    `Γ_proc.outputs = [T_1; …; T_n] (n ≥ 2)  ∴  Γ ⊢ Return (some e) ↝ error: "multi-output procedure cannot use 'return e'; assign to named outputs instead"`
+
+    `return` is a control-flow jump out of the procedure; it doesn't
+    deliver a value to the enclosing block, so no subsumption against the
+    surrounding `expected` is required. The optional payload is matched
+    against the enclosing procedure's declared outputs (threaded through
+    `ResolveState.expectedReturnTypes`, set from `proc.outputs` by
+    `resolveProcedure` / `resolveInstanceProcedure` for the duration of
+    the body; `none` means "no enclosing procedure" — e.g. resolving a
+    constant initializer — and skips all `Return` checks).
+
+    A bare `return;` is allowed in any context. In a single-output procedure
+    it acts as a Dafny-style early exit — the output parameter retains
+    whatever was last assigned to it. In a single-output procedure, `return e`
+    is checked against the declared output type (closing the prior soundness
+    gap where `return 0` in a `bool`-returning procedure went uncaught).
+
+    Multi-output procedures use named-output assignment (`r := …` on the
+    declared output parameters); `return e` syntactically takes a single
+    `Option StmtExpr` and cannot carry multiple values, so it is flagged
+    with a diagnostic pointing users at the named-output convention. -/
+def Check.return (exprMd : StmtExprMd)
+    (val : Option StmtExprMd) (expected : HighTypeMd)
+    (source : Option FileRange)
+    (h : exprMd.val = .Return val) :
+    ResolveM StmtExprMd := do
+  let expectedReturn := (← get).expectedReturnTypes
+  let val' ← val.attach.mapM (fun a => have := a.property; do
+    match expectedReturn with
+    | some [singleOutput] => Check.resolveStmtExpr a.val singleOutput
+    | _ => let (e', _) ← Synth.resolveStmtExpr a.val; pure e')
+  match val, expectedReturn with
+  | none,   some []          => pure ()
+  | none,   some [_]         => pure ()
+  | none,   some _           => pure ()
+  | some _, some []          =>
+    let diag := diagnosticFromSource source
+      "void procedure cannot return a value"
+    modify fun s => { s with errors := s.errors.push diag }
+  | some _, some [_]         => pure ()
+  | some _, some _           =>
+    let diag := diagnosticFromSource source
+      "multi-output procedure cannot use 'return e'; assign to named outputs instead"
+    modify fun s => { s with errors := s.errors.push diag }
+  | _,      none             => pure ()
+  -- `return` is a control-flow jump; it doesn't deliver a value to the
+  -- enclosing block, so no TVoid-vs-expected subsumption is required.
+  -- The return value (if any) was already checked against the declared
+  -- output above via `expectedReturnTypes`.
+  pure { val := .Return val', source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      simp_all
+      omega
+
+/-- Cases on whether the statement list is empty.
+
+    `Γ_0 = Γ,  Γ_{i-1} ⊢ s_i ⇐ Unknown ⊣ Γ_i (1 ≤ i < n),  Γ_{n-1} ⊢ s_n ⇐ T  ∴  Γ ⊢ Block [s_1; …; s_n] label ⇐ T`
+
+    `TVoid <: T  ∴  Γ ⊢ Block [] label ⇐ T`
+
+    Pushes `expected` into the *last* statement rather than comparing the
+    block's synthesized type at the boundary. Errors fire at the offending
+    subexpression, and `expected` keeps propagating through nested `Block`
+    / `IfThenElse` / `Hole` / `Quantifier`.
+
+    Non-last statements are checked against `Unknown` so their type is
+    accepted regardless: this matches the Java/Python/JavaScript discipline
+    where `f(x);` is a valid statement even when `f` returns a value (the
+    value is discarded). Routing through check mode (rather than synth)
+    means that constructs without a synth rule — control-flow constructs
+    in particular — are still resolved correctly, with their own
+    bidirectional rules pushing `Unknown` into their subexpressions. The
+    trade-off is that a stray expression like `5;` is silently accepted;
+    flagging that belongs to a lint, not the type checker.
+
+    Empty blocks reduce to a subsumption check of `TVoid` against
+    `expected` — the same check `[⇐] Block-Empty` performs when `T`
+    admits `TVoid`. -/
+def Check.block (exprMd : StmtExprMd)
+    (stmts : List StmtExprMd) (label : Option String)
+    (expected : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .Block stmts label) : ResolveM StmtExprMd := do
+  withScope do
+    let unknownTy : HighTypeMd := { val := .Unknown, source := source }
+    let init' ← stmts.dropLast.attach.mapM (fun ⟨s, hMem⟩ => do
+      have : s ∈ stmts := List.dropLast_subset stmts hMem
+      Check.resolveStmtExpr s unknownTy)
+    match _lastResult: stmts.getLast? with
+    | none =>
+      checkSubtype source expected { val := .TVoid, source := source }
+      pure { val := .Block init' label, source := source }
+    | some last =>
+      have := List.mem_of_getLast? _lastResult
+      let last' ← Check.resolveStmtExpr last expected
+      pure { val := .Block (init' ++ [last']) label, source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      try (have := List.sizeOf_lt_of_mem ‹_ ∈ stmts›)
+      try simp_all
+      omega
+
+/-- When there is an else branch:
+
+    `Γ ⊢ cond ⇐ TBool,  Γ ⊢ thenBr ⇐ T,  Γ ⊢ elseBr ⇐ T  ∴  Γ ⊢ IfThenElse cond thenBr (some elseBr) ⇐ T`
+
+    Otherwise:
+
+    `Γ ⊢ cond ⇐ TBool,  Γ ⊢ thenBr ⇐ T,  TVoid <: T  ∴  Γ ⊢ IfThenElse cond thenBr none ⇐ T`
+
+    Pushes `expected` into both branches (rather than going through
+    If-Synth + Sub at the boundary). Errors fire at the offending branch
+    instead of the surrounding `if`. Without an else branch, the construct
+    can only succeed when `expected` admits `TVoid` — the same subsumption
+    check `[⇐] Block-Empty` performs for an empty block. -/
+def Check.ifThenElse (exprMd : StmtExprMd)
+    (cond thenBr : StmtExprMd) (elseBr : Option StmtExprMd)
+    (expected : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .IfThenElse cond thenBr elseBr) : ResolveM StmtExprMd := do
+  let cond' ← Check.resolveStmtExpr cond { val := .TBool, source := cond.source }
+  let thenBr' ← Check.resolveStmtExpr thenBr expected
+  let elseBr' ← elseBr.attach.mapM (fun ⟨e, _⟩ => Check.resolveStmtExpr e expected)
+  if elseBr.isNone then
+    checkSubtype source expected { val := .TVoid, source := source }
+  pure { val := .IfThenElse cond' thenBr' elseBr', source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      try simp_all
+      omega
+
+-- ### Verification statements
+
+/-- `Γ ⊢ cond ⇐ TBool,  TVoid <: T  ∴  Γ ⊢ Assert cond ⇐ T`
+
+    `cond` is checked against `TBool`; the construct produces no value,
+    so `expected` must admit `TVoid`. -/
+def Check.assert (exprMd : StmtExprMd)
+    (condExpr : StmtExprMd) (summary : Option String)
+    (expected : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .Assert ⟨condExpr, summary⟩) :
+    ResolveM StmtExprMd := do
+  let cond' ← Check.resolveStmtExpr condExpr { val := .TBool, source := condExpr.source }
+  checkSubtype source expected { val := .TVoid, source := source }
+  pure { val := .Assert { condition := cond', summary }, source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    try simp_all
+    omega
+
+/-- `Γ ⊢ cond ⇐ TBool,  TVoid <: T  ∴  Γ ⊢ Assume cond ⇐ T`
+
+    `cond` is checked against `TBool`; the construct produces no value,
+    so `expected` must admit `TVoid`. -/
+def Check.assume (exprMd : StmtExprMd)
+    (cond : StmtExprMd) (expected : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .Assume cond) :
+    ResolveM StmtExprMd := do
+  let cond' ← Check.resolveStmtExpr cond { val := .TBool, source := cond.source }
+  checkSubtype source expected { val := .TVoid, source := source }
+  pure { val := .Assume cond', source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    try simp_all
+    omega
+
+-- ### Assignment
+
+/-- `Γ ⊢ targets_i ⇒ T_i,  Γ ⊢ e ⇐ ExpectedTy,  ExpectedTy <: T  ∴  Γ ⊢ Assign targets e ⇐ T`  (T ≠ TVoid)
+
+    `Γ ⊢ targets_i ⇒ T_i,  Γ ⊢ e ⇐ ExpectedTy  ∴  Γ ⊢ Assign targets e ⇐ TVoid`
+
+    where `ExpectedTy = T_1` if `|targets| = 1`, else
+    `MultiValuedExpr [T_1; …; T_n]`.
+
+    The target tuple type is pushed into the RHS via
+    `Check.resolveStmtExpr`, so bidirectional rules in the RHS receive
+    the assignment's type. When `T ≠ TVoid` (expression position) the
+    outer subsumption `ExpectedTy <: T` is enforced. When `T = TVoid`
+    (statement position) the subsumption is skipped: the assignment's
+    value is discarded as a statement, so there is nothing to compare
+    against `expected`. -/
+def Check.assign (exprMd : StmtExprMd)
+    (targets : List VariableMd) (value : StmtExprMd)
+    (expected : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .Assign targets value) : ResolveM StmtExprMd := do
+  let targets' ← targets.attach.mapM fun ⟨v, _⟩ => do
+    let ⟨vv, vs⟩ := v
+    match vv with
+    | .Local ref =>
+      let ref' ← resolveRef ref source
+      pure (⟨.Local ref', vs⟩ : VariableMd)
+    | .Field target fieldName =>
+      let (target', _) ← Synth.resolveStmtExpr target
+      let fieldName' ← resolveFieldRef target' fieldName source
+      pure (⟨.Field target' fieldName', vs⟩ : VariableMd)
+    | .Declare param =>
+      let ty' ← resolveHighType param.type
+      let name' ← defineNameCheckDup param.name (.var param.name ty')
+      pure (⟨.Declare ⟨name', ty'⟩, vs⟩ : VariableMd)
+  let targetType (t : VariableMd) : ResolveM HighTypeMd := do
+    match t.val with
+    | .Local ref => getVarType ref
+    | .Declare param => pure param.type
+    | .Field _ fieldName => getVarType fieldName
+  let targetTys ← targets'.mapM targetType
+  let expectedTy : HighTypeMd := match targetTys with
+    | [single] => single
+    | _        => { val := .MultiValuedExpr targetTys, source := source }
+  let value' ← Check.resolveStmtExpr value expectedTy
+  unless expected.val matches .TVoid do
+    checkSubtype source expected expectedTy
+  pure { val := .Assign targets' value', source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      try simp_all
+      try (have := List.sizeOf_lt_of_mem ‹_ ∈ targets›; simp_all)
+      omega
+
+-- ### Calls
+
+/-- Cases on the arity of the callee's declared outputs.
+
+    `Γ(callee) = static-procedure with inputs Ts and outputs [T],  Γ ⊢ args ⇒ Us,  U_i <: T_i (pairwise)  ∴  Γ ⊢ StaticCall callee args ⇒ T`
+
+    `Γ(callee) = static-procedure with inputs Ts and outputs [T_1; …; T_n] (n ≠ 1),  Γ ⊢ args ⇒ Us,  U_i <: T_i (pairwise)  ∴  Γ ⊢ StaticCall callee args ⇒ MultiValuedExpr [T_1; …; T_n]`
+
+    Callee is resolved against the expected kinds (parameter, static
+    procedure, datatype constructor, constant); each argument is
+    synthesized and checked against the corresponding parameter type. The
+    result type is the (possibly multi-valued) declared output type from
+    `getCallInfo`. -/
+def Synth.staticCall (exprMd : StmtExprMd)
+    (callee : Identifier) (args : List StmtExprMd) (source : Option FileRange)
+    (h : exprMd.val = .StaticCall callee args) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let callee' ← resolveRef callee source
+    (expected := #[.parameter, .staticProcedure, .datatypeConstructor, .constant])
+  let results ← args.mapM Synth.resolveStmtExpr
+  let args' := results.map (·.1)
+  let argTypes := results.map (·.2)
+  let (retTy, paramTypes) ← getCallInfo callee
+  for ((a, aTy), paramTy) in (args'.zip argTypes).zip paramTypes do
+    checkSubtype a.source paramTy aTy
+  pure (.StaticCall callee' args', retTy)
+  termination_by (exprMd, 1)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    have := List.sizeOf_lt_of_mem ‹_ ∈ args›
+    omega
+
+/-- `Γ ⊢ target ⇒ _,  Γ(callee) = instance-procedure with inputs [self; Ts] and outputs [T],  Γ ⊢ args ⇒ Us,  U_i <: T_i (pairwise; self dropped)  ∴  Γ ⊢ InstanceCall target callee args ⇒ T`
+
+    Target is synthesized; callee resolves to an instance or static
+    procedure; arguments are checked pairwise against the callee's
+    parameter types after dropping `self`. -/
+def Synth.instanceCall (exprMd : StmtExprMd)
+    (target : StmtExprMd) (callee : Identifier) (args : List StmtExprMd)
+    (source : Option FileRange)
+    (h : exprMd.val = .InstanceCall target callee args) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let (target', _) ← Synth.resolveStmtExpr target
+  let callee' ← resolveRef callee source
+    (expected := #[.instanceProcedure, .staticProcedure])
+  let results ← args.mapM Synth.resolveStmtExpr
+  let args' := results.map (·.1)
+  let argTypes := results.map (·.2)
+  let (retTy, paramTypes) ← getCallInfo callee
+  let callParamTypes := match paramTypes with | _ :: rest => rest | [] => []
+  for ((a, aTy), paramTy) in (args'.zip argTypes).zip callParamTypes do
+    checkSubtype a.source paramTy aTy
+  pure (.InstanceCall target' callee' args', retTy)
+  termination_by (exprMd, 1)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      try (have := List.sizeOf_lt_of_mem ‹_ ∈ args›)
+      try simp_all
+      omega
+
+-- ### Primitive operations
+
+/-- Cases on the operator family. All operands are synthesized first;
+    then a per-family verification fires using `checkSubtype` (a post-synth
+    subtype test, not bidirectional check resolution).
+
+    `Γ ⊢ args_i ⇒ U_i,  U_i <: TBool,  op ∈ {And, Or, AndThen, OrElse, Not, Implies}  ∴  Γ ⊢ PrimitiveOp op args ⇒ TBool`
+
+    `Γ ⊢ args_i ⇒ U_i,  Numeric U_i,  op ∈ {Lt, Leq, Gt, Geq}  ∴  Γ ⊢ PrimitiveOp op args ⇒ TBool`
+
+    `Γ ⊢ lhs ⇒ T_l,  Γ ⊢ rhs ⇒ T_r,  T_l ~ T_r,  op ∈ {Eq, Neq}  ∴  Γ ⊢ PrimitiveOp op [lhs; rhs] ⇒ TBool`
+
+    `Γ ⊢ args_i ⇒ U_i,  Numeric U_i,  Γ ⊢ args.head ⇒ T,  op ∈ {Neg, Add, Sub, Mul, Div, Mod, DivT, ModT}  ∴  Γ ⊢ PrimitiveOp op args ⇒ T`
+
+    `Γ ⊢ args_i ⇒ U_i,  U_i <: TString,  op = StrConcat  ∴  Γ ⊢ PrimitiveOp op args ⇒ TString`
+
+    `Numeric T` is the predicate "T unfolds to TInt / TReal / TFloat64
+    (or Unknown via the gradual escape hatch)" — not a single type, so it
+    cannot serve as an `expected` for `Check.resolveStmtExpr`. `~` is
+    symmetric consistency under the gradual relation, so equality has no
+    privileged operand direction.
+
+    The result type is `TBool` for booleans/comparisons/equality, the
+    head argument's type for arithmetic ("result is the type of the
+    first argument" handles `int + int → int`, `real + real → real`,
+    etc. without unification — known relaxation: `int + real` passes
+    since each operand individually passes `Numeric`; a proper fix needs
+    numeric promotion or unification), `TString` for concatenation. -/
+def Synth.primitiveOp (exprMd : StmtExprMd) (expr : StmtExpr)
+    (op : Operation) (args : List StmtExprMd) (source : Option FileRange)
+    (h_expr : expr = .PrimitiveOp op args)
+    (h : exprMd.val = .PrimitiveOp op args) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let _ := h_expr  -- carries the constructor identity for `expr` in diagnostics
+  let results ← args.mapM Synth.resolveStmtExpr
+  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
+    | .Neg | .Add | .Sub | .Mul | .Div | .Mod | .DivT | .ModT =>
+      match argTypes.head? with
+      | some headTy => headTy.val
+      | none => HighType.TInt
+    | .StrConcat => HighType.TString
+  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
+  | .Neg | .Add | .Sub | .Mul | .Div | .Mod | .DivT | .ModT | .Lt | .Leq | .Gt | .Geq =>
+    let ctx := (← get).typeContext
+    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).typeContext
+      unless isConsistent ctx lhsTy rhsTy do
+        let diag := diagnosticFromSource source
+          s!"Operands of '{op}' have incompatible types '{formatType lhsTy}' and '{formatType rhsTy}'"
+        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 (.PrimitiveOp op args', { val := resultTy, source := source })
+  termination_by (exprMd, 1)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    have := List.sizeOf_lt_of_mem ‹_ ∈ args›
+    omega
+
+-- ### Object forms
+
+/-- Cases on whether `ref` resolves to a composite/datatype.
+
+    `Γ(ref) is a composite or datatype T  ∴  Γ ⊢ New ref ⇒ UserDefined T`
+
+    `Γ(ref) is not a composite or datatype  ∴  Γ ⊢ New ref ⇒ Unknown`
+
+    When `ref` resolves to a composite or datatype, the type is
+    `UserDefined ref`; otherwise `Unknown` (suppresses cascading errors
+    after the kind diagnostic has already fired). -/
+def Synth.new (ref : Identifier) (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let ref' ← resolveRef ref source
+    (expected := #[.compositeType, .datatypeDefinition])
+  let s ← get
+  let kindOk : Bool := match s.scope.get? ref.text with
+    | some (_, node) => node.kind == .unresolved ||
+        (#[ResolvedNodeKind.compositeType, .datatypeDefinition].contains node.kind)
+    | none => true
+  let ty := if kindOk then { val := HighType.UserDefined ref', source := source }
+            else { val := HighType.Unknown, source := source }
+  pure (.New ref', ty)
+
+/-- `Γ ⊢ target ⇒ _  ∴  Γ ⊢ AsType target T ⇒ T`
+
+    `target` is resolved but not checked against `T` — the cast is the
+    user's claim. The synthesized type is `T`.
+
+    `IsType` is the runtime test counterpart and synthesizes `TBool`. -/
+def Synth.asType (exprMd : StmtExprMd)
+    (target : StmtExprMd) (ty : HighTypeMd)
+    (h : exprMd.val = .AsType target ty) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let (target', _) ← Synth.resolveStmtExpr target
+  let ty' ← resolveHighType ty
+  pure (.AsType target' ty', ty')
+  termination_by (exprMd, 1)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    omega
+
+/-- `Γ ⊢ target ⇒ _  ∴  Γ ⊢ IsType target T ⇒ TBool`
+
+    `target` is resolved; the synthesized type is `TBool`. -/
+def Synth.isType (exprMd : StmtExprMd)
+    (target : StmtExprMd) (ty : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .IsType target ty) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let (target', _) ← Synth.resolveStmtExpr target
+  let ty' ← resolveHighType ty
+  pure (.IsType target' ty', { val := .TBool, source := source })
+  termination_by (exprMd, 1)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    omega
+
+/-- `Γ ⊢ lhs ⇒ T_l,  Γ ⊢ rhs ⇒ T_r,  isReference T_l,  isReference T_r,  T_l ~ T_r  ∴  Γ ⊢ ReferenceEquals lhs rhs ⇒ TBool`
+
+    Both operands must be reference types (`UserDefined` or `Unknown`) —
+    reference equality is meaningless on primitives. The operands must
+    also be mutually consistent (the symmetric `isConsistent`), so
+    `Cat === Dog` is rejected when `Cat` and `Dog` are unrelated
+    user-defined types, while `Cat === Animal` is accepted when `Cat`
+    extends `Animal` (the gradual `Unknown` wildcard makes either side
+    flow freely against the other). -/
+def Synth.refEq (exprMd : StmtExprMd) (expr : StmtExpr)
+    (lhs rhs : StmtExprMd) (source : Option FileRange)
+    (h_expr : expr = .ReferenceEquals lhs rhs)
+    (h : exprMd.val = .ReferenceEquals lhs rhs) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let _ := h_expr
+  let (lhs', lhsTy) ← Synth.resolveStmtExpr lhs
+  let (rhs', rhsTy) ← Synth.resolveStmtExpr rhs
+  let ctx := (← get).typeContext
+  unless isReference ctx lhsTy do
+    typeMismatch lhs'.source (some expr) "expected a reference type" lhsTy
+  unless isReference ctx rhsTy do
+    typeMismatch rhs'.source (some expr) "expected a reference type" rhsTy
+  unless isConsistent ctx lhsTy rhsTy do
+    let diag := diagnosticFromSource source
+      s!"'{expr.constrName}' operands have incompatible types '{formatType lhsTy}' and '{formatType rhsTy}'"
+    modify fun s => { s with errors := s.errors.push diag }
+  pure (.ReferenceEquals lhs' rhs', { val := .TBool, source := source })
+  termination_by (exprMd, 1)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      omega
+
+/-- `Γ ⊢ target ⇒ T_t,  Γ(f) = T_f,  Γ ⊢ newVal ⇐ T_f  ∴  Γ ⊢ PureFieldUpdate target f newVal ⇒ T_t`
+
+    `target` is synthesized, `f` resolved against `T_t` (or the enclosing
+    instance type), and `newVal` checked against the field's declared
+    type. The synthesized type is `T_t` — updating a field on a pure type
+    produces a new value of the same type. -/
+def Synth.pureFieldUpdate (exprMd : StmtExprMd)
+    (target : StmtExprMd) (fieldName : Identifier) (newVal : StmtExprMd)
+    (h : exprMd.val = .PureFieldUpdate target fieldName newVal) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let (target', targetTy) ← Synth.resolveStmtExpr target
+  let fieldName' ← resolveFieldRef target' fieldName target.source
+  let fieldTy ← getVarType fieldName'
+  let newVal' ← Check.resolveStmtExpr newVal fieldTy
+  pure (.PureFieldUpdate target' fieldName' newVal', targetTy)
+  termination_by (exprMd, 1)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      omega
+
+-- ### Verification expressions
+
+/-- `Γ, x : T ⊢ body ⇐ TBool  ∴  Γ ⊢ Quantifier mode ⟨x, T⟩ trig body ⇒ TBool`
+
+    Opens a fresh scope, binds `x : T` (in scope only for the body and
+    trigger), resolves the optional trigger, and checks the body against
+    `TBool` since a quantifier is a proposition. Without that body check,
+    `forall x: int :: x + 1` would be silently accepted. The construct
+    itself synthesizes `TBool`. -/
+def Synth.quantifier (exprMd : StmtExprMd)
+    (mode : QuantifierMode) (param : Parameter)
+    (trigger : Option StmtExprMd) (body : StmtExprMd) (source : Option FileRange)
+    (h : exprMd.val = .Quantifier mode param trigger body) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  withScope do
+    let paramTy' ← resolveHighType param.type
+    let paramName' ← defineNameCheckDup param.name (.quantifierVar param.name paramTy')
+    let trigger' ← trigger.attach.mapM (fun pv => have := pv.property; do
+      let (e', _) ← Synth.resolveStmtExpr pv.val; pure e')
+    let body' ← Check.resolveStmtExpr body { val := .TBool, source := body.source }
+    pure (.Quantifier mode ⟨paramName', paramTy'⟩ trigger' body', { val := .TBool, source := source })
+  termination_by (exprMd, 1)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      try simp_all
+      omega
+
+/-- `Γ ⊢ name ⇒ _  ∴  Γ ⊢ Assigned name ⇒ TBool`
+
+    `name` is synthesized; the construct synthesizes `TBool`. -/
+def Synth.assigned (exprMd : StmtExprMd)
+    (name : StmtExprMd) (source : Option FileRange)
+    (h : exprMd.val = .Assigned name) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let (name', _) ← Synth.resolveStmtExpr name
+  pure (.Assigned name', { val := .TBool, source := source })
+  termination_by (exprMd, 1)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    omega
+
+/-- `Γ ⊢ v ⇐ T  ∴  Γ ⊢ Old v ⇐ T`
+
+    `Old v` has the same type as `v`, so the surrounding expectation
+    propagates straight through. -/
+def Check.old (exprMd : StmtExprMd)
+    (val : StmtExprMd) (expected : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .Old val) :
+    ResolveM StmtExprMd := do
+  let val' ← Check.resolveStmtExpr val expected
+  pure { val := .Old val', source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    omega
+
+/-- `Γ ⊢ v ⇒ T,  isReference T  ∴  Γ ⊢ Fresh v ⇒ TBool`
+
+    `v` is synthesized and must have a reference type (`UserDefined` or
+    `Unknown`) — `Fresh` only makes sense on heap-allocated references, so
+    `fresh(5)` is rejected. The construct itself synthesizes `TBool`. -/
+def Synth.fresh (exprMd : StmtExprMd) (expr : StmtExpr)
+    (val : StmtExprMd) (source : Option FileRange)
+    (h_expr : expr = .Fresh val)
+    (h : exprMd.val = .Fresh val) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let _ := h_expr
+  let (val', valTy) ← Synth.resolveStmtExpr val
+  unless isReference (← get).typeContext valTy do
+    typeMismatch val'.source (some expr) "expected a reference type" valTy
+  pure (.Fresh val', { val := .TBool, source := source })
+  termination_by (exprMd, 1)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    omega
+
+/-- `Γ ⊢ v ⇐ T,  Γ ⊢ proof ⇒ _  ∴  Γ ⊢ ProveBy v proof ⇐ T`
+
+    `ProveBy v proof` has the same type as `v` (the proof is just a hint
+    for downstream verification), so the surrounding expectation
+    propagates into `v`. The proof itself has no constraint on its type
+    and is still synthesized. -/
+def Check.proveBy (exprMd : StmtExprMd)
+    (val proof : StmtExprMd) (expected : HighTypeMd) (source : Option FileRange)
+    (h : exprMd.val = .ProveBy val proof) :
+    ResolveM StmtExprMd := do
+  let val' ← Check.resolveStmtExpr val expected
+  let (proof', _) ← Synth.resolveStmtExpr proof
+  pure { val := .ProveBy val' proof', source := source }
+  termination_by (exprMd, 0)
+  decreasing_by
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      simp [h] at hsz
+      omega
+
+-- ### Self reference
+
+/-- Cases on whether `instanceTypeName` is set (i.e., we're inside an
+    instance method).
+
+    `Γ.instanceTypeName = some T  ∴  Γ ⊢ This ⇒ UserDefined T`
+
+    `Γ.instanceTypeName = none  ∴  Γ ⊢ This ⇒ Unknown`  (emits "'this' is not allowed outside instance methods")
+
+    When `instanceTypeName` is set (we're inside an instance method,
+    populated on `ResolveState` by `resolveInstanceProcedure` for the
+    duration of an instance method body), `This` synthesizes
+    `UserDefined T`. With it, `this.field` and instance-method dispatch
+    synthesize real types instead of being wildcarded through `Unknown`.
+    Otherwise an error is emitted ("'this' is not allowed outside instance
+    methods") and the type collapses to `Unknown` to suppress cascading
+    errors. -/
+def Synth.this (source : Option FileRange) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let s ← get
+  match s.instanceTypeName with
+  | some typeName =>
+    let typeId : Identifier :=
+      match s.scope.get? typeName with
+      | some (uid, _) => { text := typeName, uniqueId := some uid, source := source }
+      | none => { text := typeName, source := source }
+    pure (.This, { val := .UserDefined typeId, source := source })
+  | none =>
+    let diag := diagnosticFromSource source "'this' is not allowed outside instance methods"
+    modify fun s => { s with errors := s.errors.push diag }
+    pure (.This, { val := .Unknown, source := source })
+
+-- ### Untyped forms
+
+/-- `Γ ⊢ Abstract ⇒ Unknown` -/
+def Synth.abstract (source : Option FileRange) : StmtExpr × HighTypeMd :=
+  (.Abstract, { val := .Unknown, source := source })
+
+/-- `Γ ⊢ All ⇒ Unknown` -/
+def Synth.all (source : Option FileRange) : StmtExpr × HighTypeMd :=
+  (.All, { val := .Unknown, source := source })
+
+-- ### ContractOf
+
+/-- Cases on the contract type `ty` and on whether `fn` is a procedure
+    reference.
+
+    `fn = Var (.Local id),  Γ(id) ∈ {staticProcedure, instanceProcedure}  ∴  Γ ⊢ ContractOf Precondition fn ⇒ TBool  and  Γ ⊢ ContractOf PostCondition fn ⇒ TBool`
+
+    `fn = Var (.Local id),  Γ(id) ∈ {staticProcedure, instanceProcedure}  ∴  Γ ⊢ ContractOf Reads fn ⇒ TSet Unknown  and  Γ ⊢ ContractOf Modifies fn ⇒ TSet Unknown`
+
+    `fn is not a procedure reference  ∴  Γ ⊢ ContractOf _ fn ↝ error: "'contractOf' expected a procedure reference"`
+
+    `ContractOf ty fn` extracts a procedure's contract clause as a value:
+    its preconditions (`Precondition`), postconditions (`PostCondition`),
+    reads set (`Reads`), or modifies set (`Modifies`). `fn` must be a
+    direct identifier reference resolving to a procedure — a contract
+    belongs to a *named* procedure, not an arbitrary expression. Anything
+    else fires the diagnostic *"'contractOf' expected a procedure
+    reference"* and the construct synthesizes `Unknown` to suppress
+    cascading errors.
+
+    `Precondition` and `PostCondition` are propositions, hence `TBool`.
+    `Reads` and `Modifies` are sets of heap-allocated locations —
+    composite/datatype references and fields. The element type is left as
+    `Unknown` for now since the rule doesn't yet recover it from `fn`'s
+    declared modifies/reads clauses.
+
+    The constructor is reserved for future use — Laurel's grammar has no
+    `contractOf` production today, and the translator emits "not yet
+    implemented" for it. The typing rule exists so resolution remains
+    exhaustive over `StmtExpr`. -/
+def Synth.contractOf (exprMd : StmtExprMd)
+    (ty : ContractType) (fn : StmtExprMd) (source : Option FileRange)
+    (h : exprMd.val = .ContractOf ty fn) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let (fn', _) ← Synth.resolveStmtExpr fn
+  let s ← get
+  let fnIsProcRef : Bool := match fn'.val with
+    | .Var (.Local ref) =>
+      match s.scope.get? ref.text with
+      | some (_, node) =>
+        node.kind == .staticProcedure ||
+        node.kind == .instanceProcedure ||
+        node.kind == .unresolved
+      | none => true  -- unresolved name already reported
+    | _ => false
+  unless fnIsProcRef do
+    let diag := diagnosticFromSource fn.source
+      "'contractOf' expected a procedure reference"
+    modify fun s => { s with errors := s.errors.push diag }
+  let resultTy : HighType := match ty with
+    | .Precondition | .PostCondition => .TBool
+    | .Reads | .Modifies => .TSet { val := .Unknown, source := none }
+  pure (.ContractOf ty fn', { val := resultTy, source := source })
+  termination_by (exprMd, 1)
+  decreasing_by
+    apply Prod.Lex.left
+    have hsz := exprMd.sizeOf_val_lt
+    simp [h] at hsz
+    omega
+
+-- ### Holes
+
+/-- `T_h <: T  ∴  Γ ⊢ Hole d (some T_h) ⇐ T`
+
+    A typed hole carries the user's annotation `T_h`. The annotation is
+    resolved and verified against the surrounding `expected` type via
+    subsumption; the resolved annotation is preserved on the node so
+    downstream passes (hole elimination) can generate correctly typed
+    uninterpreted functions. -/
+def Check.holeSome (det : Bool) (ty : HighTypeMd) (expected : HighTypeMd)
+    (source : Option FileRange) : ResolveM StmtExprMd := do
+  let ty' ← resolveHighType ty
+  checkSubtype source expected ty'
+  pure { val := .Hole det (some ty'), source := source }
+
+/-- `Γ ⊢ Hole d none ⇐ T  ↦  Γ ⊢ Hole d (some T)`
+
+    An untyped hole in check mode records the expected type on the node
+    so downstream passes (hole elimination) don't have to infer it
+    again. -/
+def Check.holeNone (det : Bool) (expected : HighTypeMd) (source : Option FileRange) :
+    StmtExprMd :=
+  { val := .Hole det (some expected), source := source }
+
+end -- mutual
+end Resolution
+
+open Resolution
+
+/-- Resolve a statement expression, discarding the synthesized type.
+    Use when only the resolved expression is needed (invariants, decreases, etc.). -/
+private def resolveStmtExpr (e : StmtExprMd) : ResolveM StmtExprMd := do
+  let (e', _) ← Synth.resolveStmtExpr e; pure e'
 
 /-- Resolve a parameter: assign a fresh ID and add to scope. -/
 def resolveParameter (param : Parameter) : ResolveM Parameter := do
@@ -511,15 +1535,19 @@ def resolveParameter (param : Parameter) : ResolveM Parameter := do
   let name' ← defineNameCheckDup param.name (.parameter ⟨param.name, ty'⟩)
   return ⟨name', ty'⟩
 
-/-- Resolve a procedure body. -/
-def resolveBody (body : Body) : ResolveM Body := do
+/-- Resolve a procedure body, checking its impl block (if any) against
+    `expected`. The expected type comes from the procedure's declared
+    output: a single output `T` for functional procedures, `TVoid`
+    otherwise. Bodies without an impl block (`Abstract`, `External`) ignore
+    `expected`. -/
+def resolveBody (body : Body) (expected : HighTypeMd) : ResolveM Body := do
   match body with
   | .Transparent b =>
-    let b' ← resolveStmtExpr b
+    let b' ← Check.resolveStmtExpr b expected
     return .Transparent b'
   | .Opaque posts impl mods =>
     let posts' ← posts.mapM (·.mapM resolveStmtExpr)
-    let impl' ← impl.mapM resolveStmtExpr
+    let impl' ← impl.mapM (Check.resolveStmtExpr · expected)
     let mods' ← mods.mapM resolveStmtExpr
     return .Opaque posts' impl' mods'
   | .Abstract posts =>
@@ -527,6 +1555,19 @@ def resolveBody (body : Body) : ResolveM Body := do
     return .Abstract posts'
   | .External => return .External
 
+/-- Compute the expected body type for a procedure. Functional
+    procedures with a single output `T` expect `T` — the body's last
+    statement is the result and must produce a `T`. Non-functional
+    procedures expect `Unknown`: their body is statement-typed and the
+    last statement (if any) is discarded — outputs are observed via
+    `return e` or named-output assignment, validated independently
+    inside `Check.return` via `expectedReturnTypes`. -/
+private def procedureBodyType (isFunctional : Bool) (outputs : List Parameter)
+    (source : Option FileRange) : HighTypeMd :=
+  match isFunctional, outputs with
+  | true, [singleOutput] => singleOutput.type
+  | _, _ => { val := .Unknown, source := source }
+
 /-- Resolve a procedure: resolve its name, then resolve params, contracts, and body in a new scope. -/
 def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
   let procName' ← resolveRef proc.name
@@ -535,7 +1576,11 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
     let outputs' ← proc.outputs.mapM resolveParameter
     let pres' ← proc.preconditions.mapM (·.mapM resolveStmtExpr)
     let dec' ← proc.decreases.mapM resolveStmtExpr
-    let body' ← resolveBody proc.body
+    let savedReturns := (← get).expectedReturnTypes
+    modify fun s => { s with expectedReturnTypes := some (outputs'.map (·.type)) }
+    let bodyExpected := procedureBodyType proc.isFunctional outputs' proc.name.source
+    let body' ← resolveBody proc.body bodyExpected
+    modify fun s => { s with expectedReturnTypes := savedReturns }
     if !proc.isFunctional && body'.isTransparent then
       let diag := diagnosticFromSource proc.name.source
         s!"transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque"
@@ -568,7 +1613,11 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     let outputs' ← proc.outputs.mapM resolveParameter
     let pres' ← proc.preconditions.mapM (·.mapM resolveStmtExpr)
     let dec' ← proc.decreases.mapM resolveStmtExpr
-    let body' ← resolveBody proc.body
+    let savedReturns := (← get).expectedReturnTypes
+    modify fun s => { s with expectedReturnTypes := some (outputs'.map (·.type)) }
+    let bodyExpected := procedureBodyType proc.isFunctional outputs' proc.name.source
+    let body' ← resolveBody proc.body bodyExpected
+    modify fun s => { s with expectedReturnTypes := savedReturns }
     if !proc.isFunctional && body'.isTransparent then
       let diag := diagnosticFromSource proc.name.source
         s!"transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque"
@@ -615,8 +1664,8 @@ def resolveTypeDefinition (td : TypeDefinition) : ResolveM TypeDefinition := do
     -- in scope when resolving the constraint and witness expressions.
     let (valueName', constraint', witness') ← withScope do
       let valueName' ← defineNameCheckDup ct.valueName (.quantifierVar ct.valueName base')
-      let constraint' ← resolveStmtExpr ct.constraint
-      let witness' ← resolveStmtExpr ct.witness
+      let (constraint', _) ← Synth.resolveStmtExpr ct.constraint
+      let (witness', _) ← Synth.resolveStmtExpr ct.witness
       return (valueName', constraint', witness')
     return .Constrained { name := ctName', base := base', valueName := valueName',
                           constraint := constraint', witness := witness' }
@@ -642,7 +1691,7 @@ def resolveTypeDefinition (td : TypeDefinition) : ResolveM TypeDefinition := do
 /-- Resolve a constant definition. -/
 def resolveConstant (c : Constant) : ResolveM Constant := do
   let ty' ← resolveHighType c.type
-  let init' ← c.initializer.mapM resolveStmtExpr
+  let init' ← c.initializer.mapM (Check.resolveStmtExpr · ty')
   let name' ← resolveRef c.name
   return { name := name', type := ty', initializer := init' }
 
@@ -866,7 +1915,8 @@ def resolve (program : Program) (existingModel: Option SemanticModel := none) :
     return { staticProcedures := staticProcs', staticFields := staticFields',
              types := types', constants := constants' }
   let nextId := existingModel.elim 1 (fun m => m.nextId)
-  let (program', finalState) := phase1.run { nextId := nextId }
+  let typeContext := TypeContext.ofTypes program.types
+  let (program', finalState) := phase1.run { nextId := nextId, typeContext }
   -- Phase 2: build refToDef from the resolved program (all definitions now have UUIDs)
   let refToDef := buildRefToDef program'
   { program := program',
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_ArityMismatch.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_ArityMismatch.lean
index 94c0f22371..dea2d510fb 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_ArityMismatch.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_ArityMismatch.lean
@@ -39,7 +39,7 @@ procedure mismatch()
 {
   var x: int;
   assign x := twoReturns()
-//^^^^^^^^^^^^^^^^^^^^^^^^ error: Assignment target count mismatch
+//^^^^^^^^^^^^^^^^^^^^^^^^ error: expected 'int', got '(int, int)'
 };
 "
 
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T9_IfBranchJoin.lean b/StrataTest/Languages/Laurel/Examples/Objects/T9_IfBranchJoin.lean
new file mode 100644
index 0000000000..9149d2e647
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T9_IfBranchJoin.lean
@@ -0,0 +1,35 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+
+namespace Strata
+namespace Laurel
+
+/-
+When the two branches of an `if/else` have different but subtype-related
+types, the construct synthesizes their join (least upper bound) — not the
+then-branch arbitrarily. So `if c then new Left else new Right`, with
+`Left, Right <: Top`, synthesizes `Top`. Storing it in a `Top`-typed
+variable succeeds, but storing it in a `Left`-typed variable is rejected.
+-/
+
+def program := r"
+composite Top { }
+composite Left extends Top { }
+composite Right extends Top { }
+procedure test(c: bool) opaque {
+  var x: Top := if c then new Left else new Right;
+  var y: Left := if c then new Left else new Right
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: expected 'Left', got 'Top'
+};
+"
+
+#guard_msgs (drop info) in
+#eval testInputWithOffset "IfBranchJoin" program 22 processLaurelFile
diff --git a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
new file mode 100644
index 0000000000..b78f3b22df
--- /dev/null
+++ b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
@@ -0,0 +1,197 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Tests that the resolution pass detects type checking errors — e.g. using an int
+where a bool is expected, or passing the wrong type to a procedure.
+-/
+
+import StrataTest.Util.TestDiagnostics
+import Strata.DDM.Elab
+import Strata.DDM.BuiltinDialects.Init
+import Strata.Languages.Laurel.Grammar.LaurelGrammar
+import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
+import Strata.Languages.Laurel.Resolution
+
+open StrataTest.Util
+open Strata
+open Strata.Elab (parseStrataProgramFromDialect)
+
+namespace Strata.Laurel
+
+/-- Run only parsing + resolution and return diagnostics (no SMT verification). -/
+private def processResolution (input : Lean.Parser.InputContext) : IO (Array Diagnostic) := do
+  let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
+  let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name input
+  let uri := Strata.Uri.file input.fileName
+  match Laurel.TransM.run uri (Laurel.parseProgram strataProgram) with
+  | .error e => throw (IO.userError s!"Translation errors: {e}")
+  | .ok program =>
+    let result := resolve program
+    let files := Map.insert Map.empty uri input.fileMap
+    return result.errors.toList.map (fun dm => dm.toDiagnostic files) |>.toArray
+
+/-! ## Non-boolean conditions -/
+
+def ifCondNotBool := r"
+function foo(x: int): int {
+  if x then 1 else 0
+//   ^ error: expected 'bool', got 'int'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "IfCondNotBool" ifCondNotBool 44 processResolution
+
+def assertCondNotBool := r"
+procedure baz() opaque {
+  var x: int := 42;
+  assert x
+//       ^ error: expected 'bool', got 'int'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "AssertCondNotBool" assertCondNotBool 54 processResolution
+
+def assumeCondNotBool := r"
+procedure qux() opaque {
+  var x: int := 42;
+  assume x
+//       ^ error: expected 'bool', got 'int'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "AssumeCondNotBool" assumeCondNotBool 64 processResolution
+
+def whileCondNotBool := r"
+procedure wh() opaque {
+  var x: int := 1;
+  while (x) { }
+//       ^ error: expected 'bool', got 'int'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "WhileCondNotBool" whileCondNotBool 74 processResolution
+
+/-! ## Logical operator type checks -/
+
+def logicalAndNotBool := r"
+function foo(x: int, y: bool): bool {
+  x && y
+//^ error: expected 'bool', got 'int'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "LogicalAndNotBool" logicalAndNotBool 84 processResolution
+
+/-! ## Numeric operator type checks -/
+
+def comparisonNotNumeric := r"
+function cmp(x: string, y: int): bool {
+  x < y
+//^ error: '<' expected a numeric type, got 'string'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "ComparisonNotNumeric" comparisonNotNumeric 94 processResolution
+
+/-! ## Assignment type checks -/
+
+def assignTypeMismatch := r"
+procedure foo() opaque {
+  var x: int := true
+//^^^^^^^^^^^^^^^^^^ error: expected 'int', got 'bool'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "AssignTypeMismatch" assignTypeMismatch 104 processResolution
+
+/-! ## Function return type checks -/
+
+def returnTypeMismatch := r"
+function foo(): int {
+//       ^^^ error: expected 'int', got 'bool'
+  true
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "ReturnTypeMismatch" returnTypeMismatch 114 processResolution
+
+/-! ## Call argument type checks -/
+
+def callArgTypeMismatch := r"
+function bar(x: int): int { x };
+function foo(): int {
+  bar(true)
+//    ^^^^ error: expected 'int', got 'bool'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "CallArgTypeMismatch" callArgTypeMismatch 124 processResolution
+
+/-! ## Equality operator type checks -/
+
+def equalityTypeMismatch := r"
+function cmp(x: int, y: string): bool {
+  x == y
+//^^^^^^ error: Operands of '==' have incompatible types 'int' and 'string'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "EqualityTypeMismatch" equalityTypeMismatch 134 processResolution
+
+/-! ## Multi-output procedures -/
+
+def multiOutputInExpr := r"
+procedure multi(x: int) returns (a: int, b: int) opaque;
+procedure test() opaque {
+  assert multi(1) == 1
+//       ^^^^^^^^^^^^^ error: Operands of '==' have incompatible types '(int, int)' and 'int'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "MultiOutputInExpr" multiOutputInExpr 146 processResolution
+
+def assignTargetCountMismatch := r"
+procedure multi() returns (a: int, b: int) opaque;
+procedure test() opaque {
+  var x: int := multi()
+//^^^^^^^^^^^^^^^^^^^^^ error: expected 'int', got '(int, int)'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "AssignTargetCountMismatch" assignTargetCountMismatch 156 processResolution
+
+/-! ## UserDefined cross-type assignment
+
+Assignments between unrelated composites are rejected: `isSubtype` walks
+`extending` chains, so two composites with no common ancestor are not
+subtypes of each other. -/
+
+def userDefinedCrossType := r"
+composite Dog { }
+composite Cat { }
+procedure test() opaque {
+  var x: Dog := new Cat
+//^^^^^^^^^^^^^^^^^^^^^ error: expected 'Dog', got 'Cat'
+};
+"
+
+#guard_msgs (error, drop all) in
+#eval testInputWithOffset "UserDefinedCrossType" userDefinedCrossType 170 processResolution
+
+end Laurel
diff --git a/docs/verso/LaurelDoc.lean b/docs/verso/LaurelDoc.lean
index 4d153eb439..71c6595c6d 100644
--- a/docs/verso/LaurelDoc.lean
+++ b/docs/verso/LaurelDoc.lean
@@ -146,6 +146,325 @@ A Laurel program consists of procedures, global variables, type definitions, and
 
 {docstring Strata.Laurel.Program}
 
+# Type checking
+
+Type checking is woven into the resolution pass: every
+{name Strata.Laurel.StmtExpr}`StmtExpr` gets a {name Strata.Laurel.HighType}`HighType`, and
+mismatches against the surrounding context become diagnostics. The implementation is in
+`Resolution.lean`.
+
+## Design
+
+### Bidirectional type checking
+
+There are two operations on expressions, written here in standard bidirectional notation:
+
+```
+Γ ⊢ e ⇒ T            -- "e synthesizes T"     (Synth.resolveStmtExpr)
+Γ ⊢ e ⇐ T            -- "e checks against T"  (Check.resolveStmtExpr)
+```
+
+Synthesis returns a type inferred from the expression itself; checking verifies that the
+expression has a given expected type. Each construct picks a mode based on whether its
+type is determined locally (synth) or by context (check). The two judgments are connected
+by a single change-of-direction rule, *subsumption*:
+
+$$`\frac{\Gamma \vdash e \Rightarrow A \quad A <: B}{\Gamma \vdash e \Leftarrow B} \quad \text{([⇐] Sub)}`
+
+The two judgments are implemented as
+{name Strata.Laurel.Resolution.Synth.resolveStmtExpr}`Synth.resolveStmtExpr` and
+{name Strata.Laurel.Resolution.Check.resolveStmtExpr}`Check.resolveStmtExpr`:
+
+{docstring Strata.Laurel.Resolution.Synth.resolveStmtExpr}
+
+{docstring Strata.Laurel.Resolution.Check.resolveStmtExpr}
+
+### Gradual typing
+
+The relation `<:` (used in \[⇐\] Sub) is built from three Lean functions —
+{name Strata.Laurel.isSubtype}`isSubtype`, {name Strata.Laurel.isConsistent}`isConsistent`,
+and {name Strata.Laurel.isConsistentSubtype}`isConsistentSubtype`:
+
+{docstring Strata.Laurel.isSubtype}
+
+{docstring Strata.Laurel.isConsistent}
+
+{docstring Strata.Laurel.isConsistentSubtype}
+
+Side-effecting constructs synthesize {name Strata.Laurel.HighType.TVoid}`TVoid`. This
+includes {name Strata.Laurel.StmtExpr.Return}`Return`,
+{name Strata.Laurel.StmtExpr.Exit}`Exit`, {name Strata.Laurel.StmtExpr.While}`While`,
+{name Strata.Laurel.StmtExpr.Assert}`Assert`, {name Strata.Laurel.StmtExpr.Assume}`Assume`,
+{name Strata.Laurel.Variable.Declare}`Var Declare`, and the opaque/abstract/external bodies
+— recorded in the rules below.
+
+## Typing rules
+
+Each construct is given as a derivation. `Γ` is the current lexical scope (see
+{name Strata.Laurel.ResolveState}`ResolveState`'s `scope`); it threads identically through
+every premise and conclusion unless a rule explicitly extends it (written `Γ, x : T`).
+
+Each rule is tagged with `[⇒]` (synthesis) or `[⇐]` (checking) to make the
+direction explicit.
+
+### Index
+
+- *Subsumption* — \[⇐\] Sub
+- *Literals* — \[⇒\] Lit-Int, \[⇒\] Lit-Bool, \[⇒\] Lit-String, \[⇒\] Lit-Decimal
+- *Variables* — \[⇒\] Var-Local, \[⇒\] Var-Field, \[⇐\] Var-Declare
+- *Control flow* — \[⇐\] If, \[⇐\] If-NoElse;
+  \[⇐\] Block, \[⇐\] Block-Empty; \[⇐\] Exit;
+  \[⇐\] Return-None, \[⇐\] Return-Some, \[⇐\] Return-Void-Error,
+  \[⇐\] Return-Multi-Error; \[⇐\] While
+- *Verification statements* — \[⇐\] Assert, \[⇐\] Assume
+- *Assignment* — \[⇐\] Assign
+- *Calls* — \[⇒\] Static-Call, \[⇒\] Static-Call-Multi, \[⇒\] Instance-Call
+- *Primitive operations* — \[⇒\] Op-Bool, \[⇒\] Op-Cmp, \[⇒\] Op-Eq, \[⇒\] Op-Arith,
+  \[⇒\] Op-Concat
+- *Object forms* — \[⇒\] New-Ok, \[⇒\] New-Fallback; \[⇒\] AsType; \[⇒\] IsType;
+  \[⇒\] RefEq; \[⇒\] PureFieldUpdate
+- *Verification expressions* — \[⇒\] Quantifier, \[⇒\] Assigned, \[⇐\] Old,
+  \[⇒\] Fresh, \[⇐\] ProveBy
+- *Self reference* — \[⇒\] This-Inside, \[⇒\] This-Outside
+- *Untyped forms* — \[⇒\] Abstract / All
+- *ContractOf* — \[⇒\] ContractOf-Bool, \[⇒\] ContractOf-Set, \[⇒\] ContractOf-Error
+- *Holes* — \[⇐\] Hole-Some, \[⇐\] Hole-None
+
+### Subsumption
+
+$$`\frac{\Gamma \vdash e \Rightarrow A \quad A <: B}{\Gamma \vdash e \Leftarrow B} \quad \text{([⇐] Sub)}`
+
+Fallback in {name Strata.Laurel.Resolution.Check.resolveStmtExpr}`Check.resolveStmtExpr` whenever no bespoke check
+rule applies.
+
+### Literals
+
+$$`\frac{}{\Gamma \vdash \mathsf{LiteralInt}\;n \Rightarrow \mathsf{TInt}} \quad \text{([⇒] Lit-Int)}`
+
+{docstring Strata.Laurel.Resolution.Synth.litInt}
+
+$$`\frac{}{\Gamma \vdash \mathsf{LiteralBool}\;b \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Lit-Bool)}`
+
+{docstring Strata.Laurel.Resolution.Synth.litBool}
+
+$$`\frac{}{\Gamma \vdash \mathsf{LiteralString}\;s \Rightarrow \mathsf{TString}} \quad \text{([⇒] Lit-String)}`
+
+{docstring Strata.Laurel.Resolution.Synth.litString}
+
+$$`\frac{}{\Gamma \vdash \mathsf{LiteralDecimal}\;d \Rightarrow \mathsf{TReal}} \quad \text{([⇒] Lit-Decimal)}`
+
+{docstring Strata.Laurel.Resolution.Synth.litDecimal}
+
+### Variables
+
+$$`\frac{\Gamma(x) = T}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Local}\;x) \Rightarrow T} \quad \text{([⇒] Var-Local)}`
+
+{docstring Strata.Laurel.Resolution.Synth.varLocal}
+
+$$`\frac{\Gamma \vdash e \Rightarrow \_ \quad \Gamma(f) = T_f}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Field}\;e\;f) \Rightarrow T_f} \quad \text{([⇒] Var-Field)}`
+
+{docstring Strata.Laurel.Resolution.Synth.varField}
+
+$$`\frac{x \notin \mathrm{dom}(\Gamma) \quad \mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Declare}\;\langle x, T_x\rangle) \Leftarrow T \dashv \Gamma, x : T_x} \quad \text{([⇐] Var-Declare)}`
+
+{docstring Strata.Laurel.Resolution.Check.varDeclare}
+
+### Control flow
+
+$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{thenBr} \Leftarrow T \quad \Gamma \vdash \mathit{elseBr} \Leftarrow T}{\Gamma \vdash \mathsf{IfThenElse}\;\mathit{cond}\;\mathit{thenBr}\;(\mathsf{some}\;\mathit{elseBr}) \Leftarrow T} \quad \text{([⇐] If)}`
+
+$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{thenBr} \Leftarrow T \quad \mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{IfThenElse}\;\mathit{cond}\;\mathit{thenBr}\;\mathsf{none} \Leftarrow T} \quad \text{([⇐] If-NoElse)}`
+
+{docstring Strata.Laurel.Resolution.Check.ifThenElse}
+
+$$`\frac{\Gamma_0 = \Gamma \quad \Gamma_{i-1} \vdash s_i \Rightarrow \_ \dashv \Gamma_i \;(1 \le i < n) \quad \Gamma_{n-1} \vdash s_n \Leftarrow T}{\Gamma \vdash \mathsf{Block}\;[s_1; \ldots; s_n]\;\mathit{label} \Leftarrow T} \quad \text{([⇐] Block)}`
+
+Reading the premise: $`\Gamma_{i-1} \vdash s_i \Rightarrow \_ \dashv \Gamma_i` means $`s_i`
+is resolved under the scope $`\Gamma_{i-1}` produced by its predecessor, synthesizes some
+type (the `_` discards it — non-last statements are sequenced for effect, not value), and
+produces a possibly extended scope $`\Gamma_i` that the next statement sees. In practice
+only `Var (.Declare …)` actually extends the scope; every other construct leaves it
+unchanged so $`\Gamma_i = \Gamma_{i-1}`. The *last* statement $`s_n` is checked against
+the block's expected type $`T` rather than synthesizing freely. The block opens a fresh
+nested scope, so declarations made inside don't leak out — once the block ends, the
+surrounding $`\Gamma` is restored.
+
+Discarding the types of non-last statements matches Java/Python/JavaScript, where
+`f(x);` is a normal statement even when `f` returns a value. The trade-off is that a
+stray expression like `5;` is silently accepted; flagging that belongs to a lint, not
+the type checker.
+
+Pushing $`T` into the tail (rather than synthesizing the whole block and applying
+\[⇐\] Sub at the boundary) means a type mismatch is reported at the offending
+subexpression's source location, and the expectation continues to propagate through
+nested `Block` / `IfThenElse` / `Hole` / `Quantifier` constructs that have their own
+check rules.
+
+$$`\frac{\mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{Block}\;[]\;\mathit{label} \Leftarrow T} \quad \text{([⇐] Block-Empty)}`
+
+With no last statement to push the expectation into, the empty-block check falls back to
+a single subsumption test: an empty block is acceptable wherever `TVoid` is.
+
+{docstring Strata.Laurel.Resolution.Check.block}
+
+$$`\frac{\mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{Exit}\;\mathit{target} \Leftarrow T} \quad \text{([⇐] Exit)}`
+
+{docstring Strata.Laurel.Resolution.Check.exit}
+
+$$`\frac{\mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Leftarrow T} \quad \text{([⇐] Return-None)}`
+
+$$`\frac{\Gamma_{\mathit{proc}}.\mathit{outputs} = [T_o] \quad \Gamma \vdash e \Leftarrow T_o \quad \mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \Leftarrow T} \quad \text{([⇐] Return-Some)}`
+
+$$`\frac{\Gamma_{\mathit{proc}}.\mathit{outputs} = []}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “void procedure cannot return a value”}} \quad \text{([⇐] Return-Void-Error)}`
+
+$$`\frac{\Gamma_{\mathit{proc}}.\mathit{outputs} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “multi-output procedure cannot use ‘return e’; assign to named outputs instead”}} \quad \text{([⇐] Return-Multi-Error)}`
+
+{docstring Strata.Laurel.Resolution.Check.return}
+
+$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{invs}_i \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{dec} \Leftarrow {?} \quad \Gamma \vdash \mathit{body} \Leftarrow T \quad \mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{While}\;\mathit{cond}\;\mathit{invs}\;\mathit{dec}\;\mathit{body} \Leftarrow T} \quad \text{([⇐] While)}`
+
+{docstring Strata.Laurel.Resolution.Check.while}
+
+### Verification statements
+
+$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{Assert}\;\mathit{cond} \Leftarrow T} \quad \text{([⇐] Assert)}`
+
+{docstring Strata.Laurel.Resolution.Check.assert}
+
+$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{Assume}\;\mathit{cond} \Leftarrow T} \quad \text{([⇐] Assume)}`
+
+{docstring Strata.Laurel.Resolution.Check.assume}
+
+### Assignment
+
+$$`\frac{\Gamma \vdash \mathit{targets}_i \Rightarrow T_i \quad \Gamma \vdash e \Leftarrow \mathit{ExpectedTy} \quad \mathit{ExpectedTy} <: T}{\Gamma \vdash \mathsf{Assign}\;\mathit{targets}\;e \Leftarrow T} \quad \text{([⇐] Assign)}`
+
+where `ExpectedTy = T_1` if `|targets| = 1` and `MultiValuedExpr [T_1; …; T_n]` otherwise.
+The target's declared type `T_i` comes from the variable's scope entry (for
+{name Strata.Laurel.Variable.Local}`Local` and {name Strata.Laurel.Variable.Field}`Field`)
+or from the {name Strata.Laurel.Variable.Declare}`Declare`-bound parameter type. The
+RHS receives `ExpectedTy` via `Check.resolveStmtExpr`, so bidirectional rules in the
+RHS propagate the assignment's type into nested constructs.
+
+{docstring Strata.Laurel.Resolution.Check.assign}
+
+### Calls
+
+$$`\frac{\Gamma(\mathit{callee}) = \text{static-procedure with inputs } Ts \text{ and outputs } [T] \quad \Gamma \vdash \mathit{args} \Rightarrow Us \quad U_i <: T_i \text{ (pairwise)}}{\Gamma \vdash \mathsf{StaticCall}\;\mathit{callee}\;\mathit{args} \Rightarrow T} \quad \text{([⇒] Static-Call)}`
+
+$$`\frac{\Gamma(\mathit{callee}) = \text{static-procedure with inputs } Ts \text{ and outputs } [T_1; \ldots; T_n],\; n \ne 1 \quad \Gamma \vdash \mathit{args} \Rightarrow Us \quad U_i <: T_i \text{ (pairwise)}}{\Gamma \vdash \mathsf{StaticCall}\;\mathit{callee}\;\mathit{args} \Rightarrow \mathsf{MultiValuedExpr}\;[T_1; \ldots; T_n]} \quad \text{([⇒] Static-Call-Multi)}`
+
+{docstring Strata.Laurel.Resolution.Synth.staticCall}
+
+$$`\frac{\Gamma \vdash \mathit{target} \Rightarrow \_ \quad \Gamma(\mathit{callee}) = \text{instance-procedure with inputs } [\mathit{self}; Ts] \text{ and outputs } [T] \quad \Gamma \vdash \mathit{args} \Rightarrow Us \quad U_i <: T_i \text{ (pairwise; self dropped)}}{\Gamma \vdash \mathsf{InstanceCall}\;\mathit{target}\;\mathit{callee}\;\mathit{args} \Rightarrow T} \quad \text{([⇒] Instance-Call)}`
+
+{docstring Strata.Laurel.Resolution.Synth.instanceCall}
+
+### Primitive operations
+
+`Numeric` abbreviates "consistent with one of {name Strata.Laurel.HighType.TInt}`TInt`,
+{name Strata.Laurel.HighType.TReal}`TReal`,
+{name Strata.Laurel.HighType.TFloat64}`TFloat64`".
+
+$$`\frac{\Gamma \vdash \mathit{args}_i \Leftarrow \mathsf{TBool} \quad \mathit{op} \in \{\mathsf{And}, \mathsf{Or}, \mathsf{AndThen}, \mathsf{OrElse}, \mathsf{Not}, \mathsf{Implies}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Bool)}`
+
+$$`\frac{\Gamma \vdash \mathit{args}_i \Leftarrow \mathit{Numeric} \quad \mathit{op} \in \{\mathsf{Lt}, \mathsf{Leq}, \mathsf{Gt}, \mathsf{Geq}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Cmp)}`
+
+$$`\frac{\Gamma \vdash \mathit{lhs} \Rightarrow T_l \quad \Gamma \vdash \mathit{rhs} \Rightarrow T_r \quad T_l \sim T_r \quad \mathit{op} \in \{\mathsf{Eq}, \mathsf{Neq}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;[\mathit{lhs}; \mathit{rhs}] \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Eq)}`
+
+$$`\frac{\Gamma \vdash \mathit{args}_i \Leftarrow \mathit{Numeric} \quad \Gamma \vdash \mathit{args}.\mathsf{head} \Rightarrow T \quad \mathit{op} \in \{\mathsf{Neg}, \mathsf{Add}, \mathsf{Sub}, \mathsf{Mul}, \mathsf{Div}, \mathsf{Mod}, \mathsf{DivT}, \mathsf{ModT}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow T} \quad \text{([⇒] Op-Arith)}`
+
+$$`\frac{\Gamma \vdash \mathit{args}_i \Leftarrow \mathsf{TString} \quad \mathit{op} = \mathsf{StrConcat}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TString}} \quad \text{([⇒] Op-Concat)}`
+
+{docstring Strata.Laurel.Resolution.Synth.primitiveOp}
+
+### Object forms
+
+$$`\frac{\Gamma(\mathit{ref}) \text{ is a composite or datatype } T}{\Gamma \vdash \mathsf{New}\;\mathit{ref} \Rightarrow \mathsf{UserDefined}\;T} \quad \text{([⇒] New-Ok)}`
+
+$$`\frac{\Gamma(\mathit{ref}) \text{ is not a composite or datatype}}{\Gamma \vdash \mathsf{New}\;\mathit{ref} \Rightarrow \mathsf{Unknown}} \quad \text{([⇒] New-Fallback)}`
+
+{docstring Strata.Laurel.Resolution.Synth.new}
+
+$$`\frac{\Gamma \vdash \mathit{target} \Rightarrow \_}{\Gamma \vdash \mathsf{AsType}\;\mathit{target}\;T \Rightarrow T} \quad \text{([⇒] AsType)}`
+
+{docstring Strata.Laurel.Resolution.Synth.asType}
+
+$$`\frac{\Gamma \vdash \mathit{target} \Rightarrow \_}{\Gamma \vdash \mathsf{IsType}\;\mathit{target}\;T \Rightarrow \mathsf{TBool}} \quad \text{([⇒] IsType)}`
+
+{docstring Strata.Laurel.Resolution.Synth.isType}
+
+$$`\frac{\Gamma \vdash \mathit{lhs} \Rightarrow T_l \quad \Gamma \vdash \mathit{rhs} \Rightarrow T_r \quad \mathsf{isReference}\;T_l \quad \mathsf{isReference}\;T_r \quad T_l \sim T_r}{\Gamma \vdash \mathsf{ReferenceEquals}\;\mathit{lhs}\;\mathit{rhs} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] RefEq)}`
+
+`isReference T` holds when `T` is a {name Strata.Laurel.HighType.UserDefined}`UserDefined`
+or {name Strata.Laurel.HighType.Unknown}`Unknown` type. `~` is the consistency relation
+{name Strata.Laurel.isConsistent}`isConsistent` — symmetric, with the
+{name Strata.Laurel.HighType.Unknown}`Unknown` wildcard.
+
+{docstring Strata.Laurel.Resolution.Synth.refEq}
+
+$$`\frac{\Gamma \vdash \mathit{target} \Rightarrow T_t \quad \Gamma(f) = T_f \quad \Gamma \vdash \mathit{newVal} \Leftarrow T_f}{\Gamma \vdash \mathsf{PureFieldUpdate}\;\mathit{target}\;f\;\mathit{newVal} \Rightarrow T_t} \quad \text{([⇒] PureFieldUpdate)}`
+
+{docstring Strata.Laurel.Resolution.Synth.pureFieldUpdate}
+
+### Verification expressions
+
+$$`\frac{\Gamma, x : T \vdash \mathit{body} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Quantifier}\;\mathit{mode}\;\langle x, T\rangle\;\mathit{trig}\;\mathit{body} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Quantifier)}`
+
+{docstring Strata.Laurel.Resolution.Synth.quantifier}
+
+$$`\frac{\Gamma \vdash \mathit{name} \Rightarrow \_}{\Gamma \vdash \mathsf{Assigned}\;\mathit{name} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Assigned)}`
+
+{docstring Strata.Laurel.Resolution.Synth.assigned}
+
+$$`\frac{\Gamma \vdash v \Leftarrow T}{\Gamma \vdash \mathsf{Old}\;v \Leftarrow T} \quad \text{([⇐] Old)}`
+
+{docstring Strata.Laurel.Resolution.Check.old}
+
+$$`\frac{\Gamma \vdash v \Rightarrow T \quad \mathsf{isReference}\;T}{\Gamma \vdash \mathsf{Fresh}\;v \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Fresh)}`
+
+{docstring Strata.Laurel.Resolution.Synth.fresh}
+
+$$`\frac{\Gamma \vdash v \Leftarrow T \quad \Gamma \vdash \mathit{proof} \Rightarrow \_}{\Gamma \vdash \mathsf{ProveBy}\;v\;\mathit{proof} \Leftarrow T} \quad \text{([⇐] ProveBy)}`
+
+{docstring Strata.Laurel.Resolution.Check.proveBy}
+
+### Self reference
+
+$$`\frac{\Gamma.\mathit{instanceTypeName} = \mathsf{some}\;T}{\Gamma \vdash \mathsf{This} \Rightarrow \mathsf{UserDefined}\;T} \quad \text{([⇒] This-Inside)}`
+
+$$`\frac{\Gamma.\mathit{instanceTypeName} = \mathsf{none}}{\Gamma \vdash \mathsf{This} \Rightarrow \mathsf{Unknown}\;\;[\text{emits “‘this’ is not allowed outside instance methods”}]} \quad \text{([⇒] This-Outside)}`
+
+{docstring Strata.Laurel.Resolution.Synth.this}
+
+### Untyped forms
+
+$$`\frac{}{\Gamma \vdash \mathsf{Abstract}\;/\;\mathsf{All}\;\ldots \Rightarrow \mathsf{Unknown}} \quad \text{([⇒] Abstract / All)}`
+
+{docstring Strata.Laurel.Resolution.Synth.abstract}
+
+{docstring Strata.Laurel.Resolution.Synth.all}
+
+### ContractOf
+
+$$`\frac{\mathit{fn} = \mathsf{Var}\;(\mathsf{.Local}\;\mathit{id}) \quad \Gamma(\mathit{id}) \in \{\mathit{staticProcedure}, \mathit{instanceProcedure}\}}{\Gamma \vdash \mathsf{ContractOf}\;\mathsf{Precondition}\;\mathit{fn} \Rightarrow \mathsf{TBool} \quad\quad \Gamma \vdash \mathsf{ContractOf}\;\mathsf{PostCondition}\;\mathit{fn} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] ContractOf-Bool)}`
+
+$$`\frac{\mathit{fn} = \mathsf{Var}\;(\mathsf{.Local}\;\mathit{id}) \quad \Gamma(\mathit{id}) \in \{\mathit{staticProcedure}, \mathit{instanceProcedure}\}}{\Gamma \vdash \mathsf{ContractOf}\;\mathsf{Reads}\;\mathit{fn} \Rightarrow \mathsf{TSet}\;\mathsf{Unknown} \quad\quad \Gamma \vdash \mathsf{ContractOf}\;\mathsf{Modifies}\;\mathit{fn} \Rightarrow \mathsf{TSet}\;\mathsf{Unknown}} \quad \text{([⇒] ContractOf-Set)}`
+
+$$`\frac{\mathit{fn} \text{ is not a procedure reference}}{\Gamma \vdash \mathsf{ContractOf}\;\ldots\;\mathit{fn} \rightsquigarrow \text{error: “‘contractOf’ expected a procedure reference”}} \quad \text{([⇒] ContractOf-Error)}`
+
+{docstring Strata.Laurel.Resolution.Synth.contractOf}
+
+### Holes
+
+$$`\frac{T_h <: T}{\Gamma \vdash \mathsf{Hole}\;d\;(\mathsf{some}\;T_h) \Leftarrow T} \quad \text{([⇐] Hole-Some)}`
+
+{docstring Strata.Laurel.Resolution.Check.holeSome}
+
+$$`\frac{}{\Gamma \vdash \mathsf{Hole}\;d\;\mathsf{none} \Leftarrow T \;\;\mapsto\;\; \mathsf{Hole}\;d\;(\mathsf{some}\;T)} \quad \text{([⇐] Hole-None)}`
+
+{docstring Strata.Laurel.Resolution.Check.holeNone}
+
 # Translation Pipeline
 
 Laurel programs are verified by translating them to Strata Core and then invoking the Core