strata-org · julesmt · Jun 23, 2026 · Jun 23, 2026 · Jun 23, 2026 · Jun 24, 2026
@@ -8,7 +8,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: fieldAccess prec raised 90 -> 95 (paren-free `c#n++`); shares prec(95) with `call`.
+-- Last grammar change: modifiesClause refs parsed at prec 0 so `modifies o#f` (field target) parses.
 public import StrataDDM.AST
 import StrataDDM.BuiltinDialects.Init
 import StrataDDM.Integration.Lean.HashCommands

@@ -186,7 +186,7 @@ category EnsuresClause;
 op ensuresClause(cond: StmtExpr, errorMessage: Option ErrorSummary): EnsuresClause => "\n  ensures " cond:0 errorMessage;
 
 category ModifiesClause;
-op modifiesClause(refs: CommaSepBy StmtExpr): ModifiesClause => "\n  modifies " refs;
+op modifiesClause(refs: CommaSepBy StmtExpr): ModifiesClause => "\n  modifies " refs:0;
 op modifiesWildcard: ModifiesClause => "\n  modifies *";
 
 category ReturnParameters;

@@ -475,6 +475,16 @@ where
       simp_all
       omega)
 
+/-- Heap-transform a modifies entry. A field target `o#f` is kept symbolic
+(only its owner is lowered) so the modifies pass can match it structurally. -/
+def heapTransformModifiesEntry (heapName : Identifier) (model : SemanticModel)
+    (entry : StmtExprMd) : TransformM StmtExprMd := do
+  match entry.val with
+  | .Var (.Field target fieldName) =>
+      let target' ← heapTransformExpr heapName model target
+      return { entry with val := .Var (.Field target' fieldName) }
+  | _ => heapTransformExpr heapName model entry
+
 def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : TransformM Procedure := do
   let heapName := heapVarName
   let readsHeap := (← get).heapReaders.contains proc.name
@@ -503,7 +513,7 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
                 let implExpr' ← heapTransformExpr heapName model implExpr bodyValueIsUsed
                 pure (some implExpr')
             | none => pure none
-          let modif' ← modif.mapM (heapTransformExpr heapName model ·)
+          let modif' ← modif.mapM (heapTransformModifiesEntry heapName model ·)
           pure (.Opaque postconds' impl' modif')
       | .Abstract postconds =>
           let postconds' ← postconds.mapM (·.mapM (heapTransformExpr heapName model))
@@ -532,7 +542,7 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
       | .Opaque postconds impl modif =>
           let postconds' ← postconds.mapM (·.mapM (heapTransformExpr heapName model))
           let impl' ← impl.mapM (heapTransformExpr heapName model ·)
-          let modif' ← modif.mapM (heapTransformExpr heapName model ·)
+          let modif' ← modif.mapM (heapTransformModifiesEntry heapName model ·)
           pure (.Opaque postconds' impl' modif')
       | .Abstract postconds =>
           let postconds' ← postconds.mapM (·.mapM (heapTransformExpr heapName model))

@@ -265,10 +265,23 @@ or abstract (requiring overriding in extending types).
 inductive Body where
   /-- A transparent body whose implementation is visible to callers. -/
   | Transparent (body : AstNode StmtExpr)
-  /-- An opaque body with a postcondition, optional implementation, and modifies clause. Without an implementation the postcondition is assumed. -/
+  /-- An opaque body with a postcondition, optional implementation, and modifies clause. Without an implementation the postcondition is assumed.
+
+      Each `modifies` entry lists state the procedure may change; everything else
+      on the heap is preserved. The legal forms, recognized by the downstream
+      `ModifiesClauses` pass, are:
+      - `modifies o` — a single object reference; any field of `o` may change.
+      - `modifies s` — an object set; any field of any member of `s` may change.
+      - `modifies o#f` — a single field of a single object; only field `f` of `o`
+        may change (field-granular).
+      - `modifies *` — the wildcard (`StmtExpr.All`); the procedure may change anything.
+
+      A 'field of an object set' (e.g. `s#f`) is intentionally not yet supported:
+      Laurel cannot yet construct set values, so there is no way to test it. -/
   | Opaque
       (postconditions : List Condition)
       (implementation : Option (AstNode StmtExpr))
+      -- See the constructor doc above for the allowed `modifies` forms.
       (modifies : List (AstNode StmtExpr))
       -- TODO: add back non-determinism together with an implementation
       -- deterministic : Bool

@@ -102,7 +102,6 @@ def laurelPipeline : Array LoweringPass := #[
   eliminateIncrDecrPass,
   typeAliasElimPass,
   constrainedTypeElimPass,
-  filterNonCompositeModifiesPass,
   mergeAndLiftReturnsPass,
   liftInstanceProceduresPass,
   eliminateValueInReturnsPass,

@@ -24,15 +24,19 @@ This pass should run after heap parameterization, which has already:
 - Transformed field accesses to readField/updateField calls
 - Collected field constants
 
-The frame condition states: for every object not mentioned in the modifies clause,
-all field values are preserved between the input and output heaps.
+The frame condition is field-granular: each allocated (object, field) pair not
+named in the modifies clause is preserved across the call. A clause may name a
+whole object (all its fields may change) or a single field `o#f` (only that
+field of `o` may change).
 
 Generates:
   forall $obj: Composite, $fld: Field =>
-    $obj < old($heap).nextReference && notModified($obj) ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
+    $obj < old($heap).nextReference && notModified($obj, $fld) ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
 
-where `notModified($obj)` is the conjunction of `$obj != e` for each single entry `e`,
-and `!(select(s, $obj))` for each set entry `s`.
+where notModified($obj, $fld) conjoins, per entry:
+- `$obj != e`                 single object `e`
+- `!(select(s, $obj))`        Set `s`
+- `!($obj == o && $fld == f)` field `(o, f)`
 -/
 
 namespace Strata.Laurel
@@ -42,12 +46,14 @@ public section
 private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none }
 
 /--
-A single entry in a modifies clause, either a single Composite expression
-or a Set of Composite expressions.
+A single entry in a modifies clause: a single Composite expression, a Set of
+Composite expressions, or a single `(object, field)` pair (field-granular).
 -/
 inductive ModifiesEntry where
   | single (expr : StmtExprMd)       -- a single Composite reference
   | set (expr : StmtExprMd)          -- a Set Composite expression
+  -- field-granular: only `fieldConst` of `objExpr` may change
+  | field (objExpr : StmtExprMd) (fieldConst : StmtExprMd)
 
 /--
 Classify a heap-relevant type into a `ModifiesEntry`, or `none` for
@@ -60,28 +66,38 @@ def classifyModifiesType (expr : StmtExprMd) (ty : HighType) : Option ModifiesEn
   | some .compositeSet => some (.set expr)
   | none               => none
 
-/--
-Extract modifies entries from the list of modifies StmtExprs, using the type
-environment and type definitions to distinguish Composite from Set Composite.
-Non-composite types (e.g., global variables of primitive type) are filtered out
-since the frame condition only applies to heap objects.
--/
+/-- Extract modifies entries: a field target `o#f` (kept symbolic by heap
+parameterization) becomes a field-granular entry; other entries are classified
+by type. Non-heap-relevant entries are dropped during resolution. -/
 def extractModifiesEntries (model: SemanticModel)
     (modifiesExprs : List StmtExprMd) : List ModifiesEntry :=
   modifiesExprs.filterMap fun expr =>
-    classifyModifiesType expr (computeExprType model expr).val
+    match expr.val with
+    -- Field target `o#f`: non-composite owners are already dropped during
+    -- resolution, so any field target reaching here owns a heap object.
+    | .Var (.Field objExpr fieldName) =>
+      (resolveQualifiedFieldName model fieldName).map fun qualifiedName =>
+        .field objExpr (mkMd <| .StaticCall qualifiedName [])
+    | _ => classifyModifiesType expr (computeExprType model expr).val
 /--
 Build the "obj is not modified" condition for a single modifies entry as a Laurel StmtExpr.
 - For a single Composite `e`: `$obj != e`
 - For a Set Composite `e`: `!(select(e, $obj))` i.e. $obj is not in the set
+- For a field `(o, f)`: `!($obj == o && $fld == f)` i.e. the quantified
+  `($obj, $fld)` pair is not the modified `(object, field)` pair (field-granular)
 -/
-def buildNotModifiedForEntry (obj : StmtExprMd) (entry : ModifiesEntry) : StmtExprMd :=
+def buildNotModifiedForEntry (obj : StmtExprMd) (fld : StmtExprMd) (entry : ModifiesEntry) : StmtExprMd :=
   match entry with
   | .single expr =>
     mkMd <| .PrimitiveOp .Neq [obj, expr]
   | .set expr =>
     let membership := mkMd <| .StaticCall "select" [expr, obj]
     mkMd <| .PrimitiveOp .Not [membership]
+  | .field objExpr fieldConst =>
+    let objEq := mkMd <| .PrimitiveOp .Eq [obj, objExpr]
+    let fldEq := mkMd <| .PrimitiveOp .Eq [fld, fieldConst]
+    let bothMatch := mkMd <| .PrimitiveOp .And [objEq, fldEq]
+    mkMd <| .PrimitiveOp .Not [bothMatch]
 
 /-- Conjoin a list of StmtExprs with `&&`. -/
 def conjoinAll (exprs : List StmtExprMd) : StmtExprMd :=
@@ -96,7 +112,7 @@ Build the modifies frame condition as a Laurel StmtExpr.
 Generates a single quantified formula:
 
   forall $obj: Composite, $fld: Field =>
-    notModified($obj) && $obj < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
+    notModified($obj, $fld) && $obj < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
 
 Returns `none` if there are no entries.
 -/
@@ -118,7 +134,7 @@ def buildModifiesEnsures (proc: Procedure) (model: SemanticModel) (modifiesExprs
     else
       -- Build the "not modified" precondition from all entries
       -- Combine: $obj < old($heap).nextReference && notModified($obj)
-      let notModified := conjoinAll (entries.map (buildNotModifiedForEntry obj))
+      let notModified := conjoinAll (entries.map (buildNotModifiedForEntry obj fld))
       mkMd <| .PrimitiveOp .And [objAllocated, notModified]
   -- Build: readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
   let readIn := mkMd <| .StaticCall "readField" [heapIn, obj, fld]
@@ -171,51 +187,6 @@ def transformModifiesClauses (model: SemanticModel)
         .ok proc
   | _ => .ok proc
 
-/--
-Filter non-composite modifies entries from a procedure body, collecting diagnostics
-for each filtered entry. This pre-pass ensures that global variables of primitive type
-do not incorrectly trigger heap parameterization.
-Should run before heap parameterization.
--/
-def filterBodyNonCompositeModifies (model : SemanticModel) (body : Body)
-    : Body × List DiagnosticModel :=
-  match body with
-  | .Opaque posts impl mods =>
-    let (kept, diags) := mods.foldl (fun (acc, ds) e =>
-      match e.val with
-      | .All => (acc ++ [e], ds)  -- wildcard is always kept
-      | _ =>
-        let ty := (computeExprType model e).val
-        if isHeapRelevantType ty then (acc ++ [e], ds)
-        else
-          (acc, ds ++ [diagnosticFromSource e.source s!"modifies clause entry has non-composite type '{formatHighTypeVal ty}' and will be ignored"])
-    ) ([], [])
-    (.Opaque posts impl kept, diags)
-  | other => (other, [])
-
-/--
-Filter non-composite modifies entries from all procedures in a program,
-collecting diagnostics. Should run before heap parameterization so that
-the heap parameterization phase remains agnostic to modifies clauses.
--/
-def filterNonCompositeModifies (model : SemanticModel) (program : Program)
-    : Program × List DiagnosticModel :=
-  let (staticProcs, staticDiags) := program.staticProcedures.foldl (fun (ps, ds) proc =>
-    let (body', bodyDiags) := filterBodyNonCompositeModifies model proc.body
-    (ps ++ [{ proc with body := body' }], ds ++ bodyDiags)
-  ) ([], [])
-  let (types', typeDiags) := program.types.foldl (fun (ts, ds) td =>
-    match td with
-    | .Composite ct =>
-      let (instProcs, instDiags) := ct.instanceProcedures.foldl (fun (ps, ds) proc =>
-        let (body', bodyDiags) := filterBodyNonCompositeModifies model proc.body
-        (ps ++ [{ proc with body := body' }], ds ++ bodyDiags)
-      ) ([], [])
-      (ts ++ [.Composite { ct with instanceProcedures := instProcs }], ds ++ instDiags)
-    | other => (ts ++ [other], ds)
-  ) ([], [])
-  ({ program with staticProcedures := staticProcs, types := types' }, staticDiags ++ typeDiags)
-
 /--
 Transform a Laurel program: apply modifies clause transformation to all procedures.
 This is a Laurel → Laurel pass that should run after heap parameterization.
@@ -233,14 +204,6 @@ def modifiesClausesTransform (model: SemanticModel) (program : Program) : Progra
 
 end -- public section
 
-/-- Pipeline pass: filter non-composite modifies clauses. -/
-public def filterNonCompositeModifiesPass : LoweringPass where
-  name := "FilterNonCompositeModifies"
-  documentation := "Filters modifies clauses that refer to non-composite types (e.g. primitives), which cannot be heap-parameterized. Emits a warning for each removed clause. Should run before heap parameterization so that phase remains agnostic to modifies clauses."
-  run := fun p m _ =>
-    let (p', diags) := filterNonCompositeModifies m p
-    (p', diags, {})
-
 /-- Pipeline pass: translate modifies clauses into ensures clauses. -/
 public def modifiesClausesTransformPass : LoweringPass where
   name := "ModifiesClausesTransform"

@@ -2559,6 +2559,51 @@ open Resolution
 private def resolveStmtExpr (e : StmtExprMd) : ResolveM StmtExprMd := do
   let (e', _) ← Synth.resolveStmtExpr e; pure e'
 
+/-- Resolve a single modifies-clause entry, dropping it (with a diagnostic) when
+    its type is not heap-relevant — the frame only applies to heap objects. For a
+    field target `o#f` the *owner* must be heap-relevant; `*` (`.All`) is always
+    kept. The type is unfolded through the `TypeLattice` so aliases/constrained
+    types are classified by their underlying type. Replaces the former
+    `FilterNonCompositeModifies` pass. -/
+private def resolveModifiesEntry (e : StmtExprMd) : ResolveM (Option StmtExprMd) := do
+  let ctx := (← get).typeLattice
+  match e.val with
+  | .All =>
+    -- `modifies *` wildcard: kept regardless of type.
+    let e' ← resolveStmtExpr e
+    return some e'
+  | .Var (.Field target fieldName) =>
+    -- Resolve the owner directly (as `Synth.varField` does) to gate on its type.
+    let (target', ownerTy) ← Synth.resolveStmtExpr target
+    let fieldName' ← resolveFieldRef target' fieldName e.source
+    let e' : StmtExprMd := { val := .Var (.Field target' fieldName'), source := e.source }
+    let ownerTy' := (ctx.unfold ownerTy).val
+    if isHeapRelevantType ownerTy' then
+      return some e'
+    else
+      let diag := diagnosticFromSource e.source
+        s!"modifies clause field target has non-composite owner type \
+           '{formatHighTypeVal ownerTy'}' and will be ignored"
+      modify fun s => { s with errors := s.errors.push diag }
+      return none
+  | _ =>
+    let (e', ty) ← Synth.resolveStmtExpr e
+    let ty' := (ctx.unfold ty).val
+    if isHeapRelevantType ty' then
+      return some e'
+    else
+      let diag := diagnosticFromSource e.source
+        s!"modifies clause entry has non-composite type \
+           '{formatHighTypeVal ty'}' and will be ignored"
+      modify fun s => { s with errors := s.errors.push diag }
+      return none
+
+/-- Resolve the modifies entries of an `Opaque` body, dropping the
+    non-heap-relevant ones via `resolveModifiesEntry`. -/
+private def resolveModifies (mods : List StmtExprMd) : ResolveM (List StmtExprMd) := do
+  let resolved ← mods.mapM resolveModifiesEntry
+  return resolved.filterMap id
+
 /-- Resolve a parameter: assign a fresh ID and add to scope. -/
 def resolveParameter (param : Parameter) : ResolveM Parameter := do
   let ty' ← resolveHighType param.type
@@ -2590,7 +2635,7 @@ def resolveBody (body : Body) : ResolveM Body := do
   | .Opaque posts impl mods =>
     let posts' ← posts.mapM (·.mapM resolveStmtExpr)
     let impl' ← impl.mapM Synth.resolveStmtExpr
-    let mods' ← mods.mapM resolveStmtExpr
+    let mods' ← resolveModifies mods
     return .Opaque posts' (impl'.map (fun t => t.1)) mods'
   | .Abstract posts =>
     let posts' ← posts.mapM (·.mapM resolveStmtExpr)