diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index dc54d7617a..2c085ace3b 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -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
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index 53f0c33f99..b41a6ee351 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -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;
diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
index daf9e9f4b7..90644da58e 100644
--- a/Strata/Languages/Laurel/HeapParameterization.lean
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -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))
diff --git a/Strata/Languages/Laurel/LaurelAST.lean b/Strata/Languages/Laurel/LaurelAST.lean
index fb02d7cd59..3ac1d90413 100644
--- a/Strata/Languages/Laurel/LaurelAST.lean
+++ b/Strata/Languages/Laurel/LaurelAST.lean
@@ -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
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index 4e048572c5..076886a2f3 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -102,7 +102,6 @@ def laurelPipeline : Array LoweringPass := #[
   eliminateIncrDecrPass,
   typeAliasElimPass,
   constrainedTypeElimPass,
-  filterNonCompositeModifiesPass,
   mergeAndLiftReturnsPass,
   liftInstanceProceduresPass,
   eliminateValueInReturnsPass,
diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean
index 8b4817224f..f3fbadcdb9 100644
--- a/Strata/Languages/Laurel/ModifiesClauses.lean
+++ b/Strata/Languages/Laurel/ModifiesClauses.lean
@@ -14,9 +14,33 @@ import Strata.Languages.Laurel.LaurelTypes
 import Strata.Languages.Laurel.MapStmtExpr
 
 /-
-Modifies clause transformation (Laurel → Laurel), run after heap parameterization:
-generate a frame per `modifies` clause and clear it. Under array theory with only
-individual refs, callers assume a quantifier-free frame and the body checks it per exit.
+Modifies clause transformation (Laurel → Laurel).
+
+Transforms procedures with modifies clauses by generating a frame condition
+and conjoining it with the postcondition. After this pass, the modifies list
+is cleared since its semantics have been absorbed into the postcondition.
+
+This pass should run after heap parameterization, which has already:
+- Added explicit heap parameter ($heap as inout)
+- Transformed field accesses to readField/updateField calls
+- Collected field constants
+
+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, $fld) ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
+
+where notModified($obj, $fld) conjoins, per entry:
+- `$obj != e`                 single object `e`
+- `!(select(s, $obj))`        Set `s`
+- `!($obj == o && $fld == f)` field `(o, f)`
+
+Under array theory with only individual refs, callers assume a quantifier-free
+(enumerated) frame and the body re-checks the pointwise frame at every exit.
 -/
 
 namespace Strata.Laurel
@@ -26,12 +50,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
@@ -44,28 +70,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 :=
@@ -79,7 +115,9 @@ Quantified (pointwise) frame: every allocated object the `modifies` clause does
 all of its field values across the call.
 
   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.
 -/
 def buildQuantifiedFrame (proc : Procedure) (entries : List ModifiesEntry)
     (heapIn heapOut : StmtExprMd) : StmtExprMd :=
@@ -93,7 +131,9 @@ def buildQuantifiedFrame (proc : Procedure) (entries : List ModifiesEntry)
   let antecedent := if entries.isEmpty
     then objAllocated
     else
-      let notModified := conjoinAll (entries.map (buildNotModifiedForEntry obj))
+      -- Build the "not modified" precondition from all entries
+      -- Combine: $obj < old($heap).nextReference && notModified($obj, $fld)
+      let notModified := conjoinAll (entries.map (buildNotModifiedForEntry obj fld))
       mkMd <| .PrimitiveOp .And [objAllocated, notModified]
   let readIn := mkMd <| .StaticCall "readField" [heapIn, obj, fld]
   let readOut := mkMd <| .StaticCall "readField" [heapOut, obj, fld]
@@ -171,51 +211,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 +228,6 @@ def modifiesClausesTransform (model: SemanticModel) (program : Program) (useEnum
 
 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"
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index a3e3e5090d..dd8e8f70d3 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -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)
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
index ed9bfc9301..7192b5b09e 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
@@ -154,3 +154,301 @@ procedure modifiesWildcardAndSpecificCaller()
 //^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
 };
 #end
+
+/-
+Field-granular modifies clauses (issue #1402).
+
+A `modifies o#f` clause frames only the `(o, f)` pair: every *other* field of `o`
+(and every other object) is preserved across the call, while `o#f` may change.
+This is strictly more precise than the object-granular `modifies o`.
+-/
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Account {
+  var balance: int
+  var count: int
+}
+
+// Opaque stub framing only `self#balance`. Its body writes *only* balance, so it
+// must satisfy its own field-granular frame (callee-side enforcement).
+procedure deposit(self: Account, amount: int) returns (r: bool)
+  opaque
+  modifies self#balance
+{
+  self#balance := self#balance + amount;
+  true
+};
+
+procedure fieldGranularCaller()
+  opaque
+{
+  var a: Account := new Account;
+  var b: Account := new Account;
+  var oldCount: int := a#count;
+  var oldBalance: int := a#balance;
+  var oldBCount: int := b#count;
+  var oldBBalance: int := b#balance;
+  var ok: bool := deposit(a, 100);
+  // Field-granular precision: the unmodified field of the modified object is preserved.
+  assert a#count == oldCount;
+  // Sibling object is fully preserved (object-granular frame already gave this).
+  assert b#count == oldBCount;
+  assert b#balance == oldBBalance;
+  // The modified field may change -> not provable. This negative control proves
+  // the frame is NOT vacuous: it does not silently preserve everything.
+  assert a#balance == oldBalance
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end
+
+/-
+Callee-side enforcement: a body that writes a field OUTSIDE its field-granular
+modifies clause must fail to verify. Here `modifies self#balance` is declared
+but the body also writes `self#count`, which is not framed.
+-/
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Account2 {
+  var balance: int
+  var count: int
+}
+
+procedure overreachingDeposit(self: Account2, amount: int) returns (r: bool)
+//        ^^^^^^^^^^^^^^^^^^^ error: modifies clause could not be proved
+  opaque
+  modifies self#balance
+{
+  self#balance := self#balance + amount;
+  self#count := self#count + 1;
+  true
+};
+#end
+
+/-
+SOUNDNESS GATE (issue #1402): cross-type shared field name.
+
+Cross-type field names: `Box1.x` and `Box2.x` are distinct constants, so framing
+`b1#x` must not leak to `b2#x`. The three sibling asserts hold; modified `b1#x` is UNKNOWN.
+-/
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Box1 {
+  var x: int
+  var y: int
+}
+composite Box2 {
+  var x: int
+  var y: int
+}
+
+procedure bumpBox1X(self: Box1) returns (r: bool)
+  opaque
+  modifies self#x
+{
+  self#x := self#x + 1;
+  true
+};
+
+procedure crossTypeCaller()
+  opaque
+{
+  var b1: Box1 := new Box1;
+  var b2: Box2 := new Box2;
+  var oldB1x: int := b1#x;
+  var oldB1y: int := b1#y;
+  var oldB2x: int := b2#x;
+  var oldB2y: int := b2#y;
+  var ok: bool := bumpBox1X(b1);
+  // Same object, other field: preserved (field granularity).
+  assert b1#y == oldB1y;
+  // Different type, SAME field name `x`: must be preserved (no cross-type leak).
+  assert b2#x == oldB2x;
+  // Different type, other field: preserved.
+  assert b2#y == oldB2y;
+  // Non-vacuity control: modified `b1#x` -> UNKNOWN.
+  assert b1#x == oldB1x
+//^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end
+
+/-
+Vacuity trap: a BODILESS opaque stub must still emit its field frame. The mixed
+PROVED/UNKNOWN outcome proves the frame is emitted and non-vacuous with no body.
+-/
+#eval testLaurel <|
+#strata
+program Laurel;
+composite AccountA {
+  var balance: int
+  var count: int
+}
+
+// Bodiless opaque stub: frames only `self#balance`, no implementation.
+procedure depositStub(self: AccountA)
+  opaque
+  modifies self#balance;
+
+procedure vacuityTrapCaller()
+  opaque
+{
+  var a: AccountA := new AccountA;
+  var b: AccountA := new AccountA;
+  var oldCount: int := a#count;
+  var oldBalance: int := a#balance;
+  var oldBCount: int := b#count;
+  depositStub(a);
+  // Unmodified field of the receiver: preserved (field granularity).
+  assert a#count == oldCount;
+  // Sibling object's field: preserved.
+  assert b#count == oldBCount;
+  // The MODIFIED field may change -> UNKNOWN (non-vacuity).
+  assert a#balance == oldBalance
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end
+
+/-
+Multi-field: `modifies self#x, self#y` frames two fields of one object; the
+third field `z` stays preserved while `x` and `y` may change.
+-/
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Triple {
+  var x: int
+  var y: int
+  var z: int
+}
+
+procedure writeXY(self: Triple)
+  opaque
+  modifies self#x, self#y
+{
+  self#x := self#x + 1;
+  self#y := self#y + 1
+};
+
+procedure multiFieldCaller()
+  opaque
+{
+  var t: Triple := new Triple;
+  var oldX: int := t#x;
+  var oldY: int := t#y;
+  var oldZ: int := t#z;
+  writeXY(t);
+  // Unframed field: preserved.
+  assert t#z == oldZ;
+  // Framed fields: may change -> UNKNOWN.
+  assert t#x == oldX;
+//^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+  assert t#y == oldY
+//^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end
+
+/-
+Mixed: `modifies o, p#f` combines a whole-object entry with a field entry.
+`p`'s other field and a sibling stay preserved; `o#w` and `p#f` go UNKNOWN.
+-/
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Whole {
+  var w: int
+}
+composite Part {
+  var f: int
+  var g: int
+}
+
+procedure mixedMod(o: Whole, p: Part)
+  opaque
+  modifies o, p#f
+{
+  o#w := o#w + 1;
+  p#f := p#f + 1
+};
+
+procedure mixedCaller()
+  opaque
+{
+  var o: Whole := new Whole;
+  var p: Part := new Part;
+  var s: Whole := new Whole;
+  var oldOw: int := o#w;
+  var oldPf: int := p#f;
+  var oldPg: int := p#g;
+  var oldSw: int := s#w;
+  mixedMod(o, p);
+  // `p`'s OTHER field: preserved (field granularity on p#f).
+  assert p#g == oldPg;
+  // Sibling whole object: preserved.
+  assert s#w == oldSw;
+  // Whole-object entry `o`: any field may change -> UNKNOWN.
+  assert o#w == oldOw;
+//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+  // Framed field `p#f`: may change -> UNKNOWN.
+  assert p#f == oldPf
+//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end
+
+/-
+Inheritance: `modifies d#bval` names an INHERITED field (declared in `Base`,
+qualified `Base.bval`). Derived-only `dval` stays preserved; inherited `bval` is UNKNOWN.
+-/
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Base {
+  var bval: int
+}
+composite Derived extends Base {
+  var dval: int
+}
+
+procedure bumpInherited(d: Derived)
+  opaque
+  modifies d#bval
+{
+  d#bval := d#bval + 1
+};
+
+procedure inheritanceCaller()
+  opaque
+{
+  var d: Derived := new Derived;
+  var oldBval: int := d#bval;
+  var oldDval: int := d#dval;
+  bumpInherited(d);
+  // Derived-only field: preserved (inherited field framed, not this one).
+  assert d#dval == oldDval;
+  // Inherited framed field: may change -> UNKNOWN.
+  assert d#bval == oldBval
+//^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end
+
+
+/-
+Callee-side field enforcement: declaring modifies o.x but writing o.y must fail.
+-/
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Pair {
+  var x: int
+  var y: int
+}
+
+procedure overreachX(self: Pair)
+//        ^^^^^^^^^^ error: modifies clause could not be proved
+  opaque
+  modifies self#x
+{
+  self#y := self#y + 1
+};
+#end