strata-org · keyboardDrummer · Jun 19, 2026 · Jun 18, 2026 · Jun 18, 2026 · Jun 18, 2026
@@ -33,7 +33,6 @@ def collectTypeRefs : HighTypeMd → List String
   | ⟨.UserDefined name, _⟩ => [name.text]
   | ⟨.TSet elem, _⟩ => collectTypeRefs elem
   | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v
-  | ⟨.TTypedField vt, _⟩ => collectTypeRefs vt
   | ⟨.Applied base args, _⟩ =>
       collectTypeRefs base ++ args.flatMap collectTypeRefs
   | ⟨.Pure base, _⟩ => collectTypeRefs base

@@ -71,14 +71,13 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do
   match ty.val with
   | .UserDefined name => addTypeName name.text
   | .TCore _ => pure ()
-  | .TTypedField vt => collectHighTypeNames vt
   | .TSet et => collectHighTypeNames et
   | .TMap kt vt => collectHighTypeNames kt; collectHighTypeNames vt
   | .Applied base args =>
     collectHighTypeNames base; args.forM collectHighTypeNames
   | .Pure base => collectHighTypeNames base
   | .Intersection types => types.forM collectHighTypeNames
-  | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString | .THeap
+  | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString
   | .TBv _ | .Unknown | .MultiValuedExpr _ => pure ()
 
 /-- Collect all referenced names (procedure calls, type references) from a StmtExpr tree. -/

@@ -49,9 +49,7 @@ partial def highTypeValToArg : HighType → Arg
   | .UserDefined name => laurelOp "compositeType" #[ident name.text]
   | .TCore s => laurelOp "coreType" #[ident s]
   | .TVoid => laurelOp "compositeType" #[ident "void"]
-  | .THeap => laurelOp "compositeType" #[ident "Heap"]
-  -- Type parameters discarded; the grammar cannot represent Field[T] or Set[T]
-  | .TTypedField _vt => laurelOp "compositeType" #[ident "Field"]
+  -- Type parameters discarded; the grammar cannot represent Set[T]
   | .TSet _et => laurelOp "compositeType" #[ident "Set"]
   | .Applied base _args =>
     -- Applied types are not directly representable in the grammar;

@@ -25,12 +25,12 @@ and a `nextReference: int` for allocating new objects. Box is a sum type with co
 primitive type (BoxInt, BoxBool, BoxFloat64, BoxComposite). Composite is a type synonym for int.
 
 1. Procedures that write the heap get an inout heap parameter
-   - Input: `heap : THeap`
-   - Output: `heap : THeap`
+   - Input: `heap : Heap`
+   - Output: `heap : Heap`
    - Field writes become: `heap := updateField(heap, obj, field, BoxT(value))`
 
 2. Procedures that only read the heap get an in heap parameter
-   - Input: `heap : THeap`
+   - Input: `heap : Heap`
    - Field reads become: `Box..tVal(readField(heap, obj, field))`
 
 3. Procedure calls are transformed:
@@ -480,8 +480,11 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
   if writesHeap then
     -- This procedure writes the heap - add $heap_in as input and $heap as output
     -- At the start, assign $heap_in to $heap, then use $heap throughout
-    let heapInParam : Parameter := { name := heapInName, type := ⟨.THeap, none⟩ }
-    let heapOutParam : Parameter := { name := heapName, type := ⟨.THeap, none⟩ }
+    -- Type the heap parameters as the prelude `Heap` datatype so they stay
+    -- consistent with the generated heap functions (`readField`, `updateField`,
+    -- `increment`, `Heap..nextReference!`), all of which are declared over `Heap`.
+    let heapInParam : Parameter := { name := heapInName, type := ⟨.UserDefined "Heap", proc.name.source⟩ }
+    let heapOutParam : Parameter := { name := heapName, type := ⟨.UserDefined "Heap", proc.name.source⟩ }
 
     let inputs' := heapInParam :: proc.inputs
     let outputs' := heapOutParam :: proc.outputs
@@ -519,8 +522,10 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
       body := body' }
 
   else if readsHeap then
-    -- This procedure only reads the heap - add $heap as input only
-    let heapParam : Parameter := { name := heapName, type := ⟨.THeap, none⟩ }
+    -- This procedure only reads the heap - add $heap as input only.
+    -- Use the prelude `Heap` datatype for the parameter type (see the
+    -- writes-heap branch above for rationale).
+    let heapParam : Parameter := { name := heapName, type := ⟨.UserDefined "Heap", proc.name.source⟩ }
     let inputs' := heapParam :: proc.inputs
 
     let preconditions' ← proc.preconditions.mapM (·.mapM (heapTransformExpr heapName model))
@@ -578,7 +583,7 @@ def heapParameterization (model: SemanticModel) (program : Program) : Program :=
 public def heapParameterizationPass : LaurelPass where
   name := "HeapParameterization"
   documentation := "Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as `Map Composite (Map Field Box)`. Procedures that write the heap receive both an input and output heap parameter; procedures that only read the heap receive an input heap parameter. Field reads and writes are rewritten to use `readField` and `updateField` functions."
-  needsResolves := true
+  needsResolves := false -- Only resolve again after completing HeapParam, ModifiesClauses and TypeHierarchy. These are logically one pass.
   run := fun p m =>
     (heapParameterization m p, [], {})
   comesBefore := [

@@ -135,8 +135,7 @@ structure AstNode (t : Type) : Type where
 The type system for Laurel programs.
 
 `HighType` covers primitive types (`TVoid`, `TBool`, `TInt`, `TReal`, `TFloat64`,
-`TString`), internal types used by the heap parameterization pass (`THeap`,
-`TTypedField`), collection types (`TSet`), user-defined types (`UserDefined`),
+`TString`), collection types (`TSet`), user-defined types (`UserDefined`),
 generic applications (`Applied`), value types (`Pure`), and intersection types
 (`Intersection`).
 -/
@@ -153,10 +152,6 @@ inductive HighType : Type where
   | TReal
   /-- String type for text data. -/
   | TString
-  /-- Internal type representing the heap. Introduced by the heap parameterization pass; not accessible via grammar. -/
-  | THeap
-  /-- Internal type for a field constant with a known value type. Introduced by the heap parameterization pass; not accessible via grammar. -/
-  | TTypedField (valueType : AstNode HighType)
   /-- Set type, e.g. `Set int`. -/
   | TSet (elementType : AstNode HighType)
   /-- Map type. -/
@@ -527,9 +522,7 @@ def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.va
   | HighType.TFloat64, HighType.TFloat64 => true
   | HighType.TReal, HighType.TReal => true
   | HighType.TString, HighType.TString => true
-  | HighType.THeap, HighType.THeap => true
   | HighType.TBv n1, HighType.TBv n2 => n1 == n2
-  | HighType.TTypedField t1, HighType.TTypedField t2 => highEq t1 t2
   | 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
@@ -630,7 +623,7 @@ def isSubtype (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool :=
 /- ### Variance policy (covers `isSubtype` and `isConsistent`)
    All child-carrying constructors are INVARIANT by design: `isConsistent`
    bottoms out in `highEq` (structural equality) for `TSet`, `TMap`,
-   `TTypedField`, `Applied`, `Pure`, and `Intersection`. So `TSet Unknown ~
+   `Applied`, `Pure`, and `Intersection`. So `TSet Unknown ~
    TSet TInt` is FALSE — `Unknown` is a wildcard only at the TOP of a type,
    never under a constructor. This is intentional: `TSet` / `TMap` are MUTABLE
    collections, where covariance would be unsound; if you don't know the

@@ -145,12 +145,12 @@ private def runLaurelPasses
 
   -- Initial resolution
   let result := resolve program
-  let resolutionErrors : List DiagnosticModel := result.errors.toList
+  let resolutionErrors : Std.HashSet DiagnosticModel := Std.HashSet.ofArray result.errors
   let (program, model) := (result.program, result.model)
 
   let mut program := program
   let mut model := model
-  let mut allDiags : List DiagnosticModel := resolutionErrors
+  let mut allDiags : List DiagnosticModel := result.errors.toList
   let mut allStats : Statistics := {}
 
   for pass in laurelPipeline do
@@ -163,7 +163,13 @@ private def runLaurelPasses
       let result := resolve program (some model)
       let newErrors := result.errors.filter fun e => !resolutionErrors.contains e
       if !newErrors.isEmpty then
+        let newDiags := newErrors.toList.map fun d =>
+          { d with
+              message :=
+                s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d.message}"
+              type := .StrataBug }
         emit pass.name "laurel.st" program
+        return (program, model, allDiags ++ newDiags, allStats)
       program := result.program
       model := result.model
     emit pass.name "laurel.st" program

@@ -79,13 +79,10 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do
   | .TString => return LMonoTy.string
   | .TBv n => return LMonoTy.bitvec n
   | .TVoid => return LMonoTy.bool -- Using bool as placeholder for void
-  | .THeap => return .tcons "Heap" []
-  | .TTypedField _ => return .tcons "Field" []
   | .TSet elementType => return Core.mapTy (← translateType elementType) LMonoTy.bool
   | .TMap keyType valueType => return Core.mapTy (← translateType keyType) (← translateType valueType)
   | .UserDefined name =>
     match model.get? name with
-    | some (.compositeType _) => return .tcons "Composite" []
     | some (.datatypeDefinition dt) => return .tcons dt.name.text []
     | some (.datatypeConstructor typeName _) => return .tcons typeName.text []
     | _ => do -- resolution should have already emitted a diagnostic
@@ -287,6 +284,8 @@ def translateExpr (expr : StmtExprMd)
       throwExprDiagnostic $ diagnosticFromSource expr.source s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldId.text}" DiagnosticType.StrataBug
   | .Block (⟨ .Assign _ _, assignSource⟩ :: tail) _ =>
       disallowed assignSource "destructive assignments are not supported in transparent bodies or contracts"
+  | .Block (⟨ .While _ _ _ _, whileSource⟩ :: tail) _ =>
+      disallowed whileSource "loops are not supported in functions or contracts"
   | .Block (head :: tail) _ =>
       throwExprDiagnostic $ diagnosticFromSource expr.source s!"block expression starting with {head.val.constructorName} should have been lowered in a separate pass" DiagnosticType.StrataBug
   | .Block [] _ =>

@@ -439,7 +439,7 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
       -- If the RHS is a direct imperative StaticCall, don't lift it —
       -- translateStmt handles Assign + StaticCall directly as a call statement.
       match _: valueMd with
-      | AstNode.mk value _ =>
+      | AstNode.mk value callSource =>
       match _: value with
       | .StaticCall callee args =>
           let model := (← get).model
@@ -452,7 +452,7 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
             let seqArgs ← args.mapM transformExpr
             let argPrepends ← takePrepends
             modify fun s => { s with subst := [] }
-            return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs, source⟩, source⟩]
+            return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs, callSource⟩, source⟩]
       | _ =>
           let seqValue ← transformExpr valueMd
           let prepends ← takePrepends

@@ -137,5 +137,107 @@ def mapProgramM [Monad m] (f : StmtExprMd → m StmtExprMd) (program : Program)
 def mapProgram (f : StmtExprMd → StmtExprMd) (program : Program) : Program :=
   mapProgramM (m := Id) f program
 
+/-! ## Type-annotation traversals
+
+`mapStmtExprHighTypesM` and friends apply a `HighType → HighType` rewrite to
+*every* type annotation reachable from a node / procedure / program, reusing
+`mapStmtExprM` for the structural recursion. This is the single source of truth
+for "rewrite all type references", so passes don't have to enumerate the
+type-carrying constructors by hand (and silently miss one). The supplied `f` is
+responsible for recursing into compound types (`TSet`/`TMap`/`Applied`/…). -/
+
+/-- Rewrite the declared type carried by a `Variable` (only `Declare` carries one). -/
+def mapVariableHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (v : Variable) : m Variable := do
+  match v with
+  | .Declare param => pure (.Declare { param with type := ← f param.type })
+  | .Local _ | .Field _ _ => pure v
+
+/--
+Apply `f` to every `HighType` annotation carried *directly* by a single
+`StmtExpr` node: local declarations (in `Var`, `Assign` targets, and `IncrDecr`
+targets), quantifier binders, `AsType`/`IsType` type arguments, and typed
+`Hole`s. Does **not** recurse into child expressions — compose with
+`mapStmtExprM` (see `mapStmtExprHighTypesM`) for a whole-tree traversal.
+-/
+def mapNodeHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (expr : StmtExprMd) : m StmtExprMd := do
+  let source := expr.source
+  match expr.val with
+  | .Var v => pure ⟨.Var (← mapVariableHighTypesM f v), source⟩
+  | .Assign targets value =>
+    let targets' ← targets.mapM (fun t => do pure (⟨← mapVariableHighTypesM f t.val, t.source⟩ : VariableMd))
+    pure ⟨.Assign targets' value, source⟩
+  | .IncrDecr mode op target =>
+    pure ⟨.IncrDecr mode op ⟨← mapVariableHighTypesM f target.val, target.source⟩, source⟩
+  | .Quantifier mode param trigger body =>
+    pure ⟨.Quantifier mode { param with type := ← f param.type } trigger body, source⟩
+  | .AsType target ty => pure ⟨.AsType target (← f ty), source⟩
+  | .IsType target ty => pure ⟨.IsType target (← f ty), source⟩
+  | .Hole det (some ty) => pure ⟨.Hole det (some (← f ty)), source⟩
+  | _ => pure expr
+
+/-- Apply `f` to every `HighType` annotation appearing anywhere in a `StmtExprMd`. -/
+def mapStmtExprHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (expr : StmtExprMd) : m StmtExprMd :=
+  mapStmtExprM (mapNodeHighTypesM f) expr
+
+/-- Pure version of `mapStmtExprHighTypesM`. -/
+def mapStmtExprHighTypes (f : HighTypeMd → HighTypeMd) (expr : StmtExprMd) : StmtExprMd :=
+  mapStmtExprHighTypesM (m := Id) f expr
+
+/-- Apply `f` to every `HighType` annotation in a procedure: parameter types,
+    body, preconditions, decreases measure, and auto-invocation trigger. -/
+def mapProcedureHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (proc : Procedure) : m Procedure := do
+  let mapExpr := mapStmtExprHighTypesM f
+  let mapParam (p : Parameter) : m Parameter := do pure { p with type := ← f p.type }
+  let body' ← match proc.body with
+    | .Transparent b => pure (.Transparent (← mapExpr b))
+    | .Opaque ps impl mods =>
+      pure (.Opaque (← ps.mapM (·.mapM mapExpr)) (← impl.mapM mapExpr) (← mods.mapM mapExpr))
+    | .Abstract ps => pure (.Abstract (← ps.mapM (·.mapM mapExpr)))
+    | .External => pure .External
+  return { proc with
+    inputs := ← proc.inputs.mapM mapParam
+    outputs := ← proc.outputs.mapM mapParam
+    body := body'
+    preconditions := ← proc.preconditions.mapM (·.mapM mapExpr)
+    decreases := ← proc.decreases.mapM mapExpr
+    invokeOn := ← proc.invokeOn.mapM mapExpr }
+
+/-- Apply `f` to every `HighType` annotation in a type definition: composite
+    fields and instance procedures, constrained base/constraint/witness,
+    datatype constructor argument types, and alias targets. -/
+def mapTypeDefinitionHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (td : TypeDefinition) : m TypeDefinition := do
+  match td with
+  | .Composite ct =>
+    pure (.Composite { ct with
+      fields := ← ct.fields.mapM (fun fld => do pure { fld with type := ← f fld.type })
+      instanceProcedures := ← ct.instanceProcedures.mapM (mapProcedureHighTypesM f) })
+  | .Constrained ct =>
+    pure (.Constrained { ct with
+      base := ← f ct.base
+      constraint := ← mapStmtExprHighTypesM f ct.constraint
+      witness := ← mapStmtExprHighTypesM f ct.witness })
+  | .Datatype dt =>
+    pure (.Datatype { dt with
+      constructors := ← dt.constructors.mapM (fun ctor => do
+        pure { ctor with args := ← ctor.args.mapM (fun p => do pure { p with type := ← f p.type }) }) })
+  | .Alias ta => pure (.Alias { ta with target := ← f ta.target })
+
+/-- Apply `f` to a constant's declared type and (optional) initializer. -/
+def mapConstantHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (c : Constant) : m Constant := do
+  pure { c with type := ← f c.type, initializer := ← c.initializer.mapM (mapStmtExprHighTypesM f) }
+
+/-- Apply `f` to every `HighType` annotation anywhere in a program: procedures,
+    static fields, type definitions, and constants. -/
+def mapProgramHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (program : Program) : m Program := do
+  return { program with
+    staticProcedures := ← program.staticProcedures.mapM (mapProcedureHighTypesM f)
+    staticFields := ← program.staticFields.mapM (fun fld => do pure { fld with type := ← f fld.type })
+    types := ← program.types.mapM (mapTypeDefinitionHighTypesM f)
+    constants := ← program.constants.mapM (mapConstantHighTypesM f) }
+
+/-- Pure version of `mapProgramHighTypesM`. -/
+def mapProgramHighTypes (f : HighTypeMd → HighTypeMd) (program : Program) : Program :=
+  mapProgramHighTypesM (m := Id) f program
+
 end -- public section
 end Strata.Laurel
@@ -126,7 +126,7 @@ def buildModifiesEnsures (proc: Procedure) (model: SemanticModel) (modifiesExprs
   -- Build: antecedent ==> heapUnchanged
   let implBody := mkMd <| .PrimitiveOp .Implies [antecedent, heapUnchanged]
   -- Build: forall $obj: Composite, $fld: Field => ...
-  let innerForall := mkMd <| .Quantifier .Forall ⟨ fldName, { val := .TTypedField { val := .TInt, source := none }, source := none } ⟩ none implBody
+  let innerForall := mkMd <| .Quantifier .Forall ⟨ fldName, { val := .UserDefined "Field", source := none } ⟩ none implBody
   let outerForall : StmtExprMd := { val := .Quantifier .Forall ⟨ objName, { val := .UserDefined "Composite", source := none } ⟩ none innerForall, source := proc.name.source }
   some outerForall