diff --git a/Strata/Languages/Laurel/EliminateIncrDecr.lean b/Strata/Languages/Laurel/EliminateIncrDecrAndCompoundAssign.lean
similarity index 51%
rename from Strata/Languages/Laurel/EliminateIncrDecr.lean
rename to Strata/Languages/Laurel/EliminateIncrDecrAndCompoundAssign.lean
index 2ebc08dfe9..88e8686a23 100644
--- a/Strata/Languages/Laurel/EliminateIncrDecr.lean
+++ b/Strata/Languages/Laurel/EliminateIncrDecrAndCompoundAssign.lean
@@ -11,11 +11,12 @@ import Strata.Languages.Laurel.MapStmtExpr
 import Strata.Util.Tactics
 
 /-!
-# Eliminate Increment / Decrement
+# Eliminate Increment / Decrement and Compound Assignment
 
-Lowers `.IncrDecr` nodes (Java-style `++x`, `x++`, `--x`, `x--`) into
+Lowers `.IncrDecr` nodes (Java-style `++x`, `x++`, `--x`, `x--`) and
+`.CompoundAssign` nodes (C-style `x += e`, `-=`, `*=`, `/=`, `%=`, `^=`) into
 existing Laurel constructs. Runs before `LiftImperativeExpressions` so that
-later passes never see `.IncrDecr`.
+later passes never see either node.
 
 The lowering, parameterised on `op` (`Incr | Decr`) and `mode` (`Pre | Post`):
 
@@ -34,19 +35,30 @@ The lowering, parameterised on `op` (`Incr | Decr`) and `mode` (`Pre | Post`):
   x--  ⇝  ((x := x - 1) + 1)
   ```
 
+Compound assignment `x op= e` lowers to `x := x op e` — always new-valued, so
+unlike postfix `IncrDecr` it needs no old-value recovery. Both share the same
+core (`lowerOpAssign`), with `IncrDecr` supplying `rhs = 1`.
+
 The pass uses the generic `mapStmtExpr` bottom-up traversal from
-`MapStmtExpr.lean`. The only constructor that changes is `.IncrDecr`; all
-other nodes are left as-is by the traversal's default recursion.
+`MapStmtExpr.lean`. The only constructors that change are `.IncrDecr` and
+`.CompoundAssign`; all other nodes are left as-is by the traversal's default
+recursion.
 
-The target of `.IncrDecr` must be a `Variable.Local` or `Variable.Field` —
-the concrete-to-abstract translator already enforces this.
+The target of `.IncrDecr` / `.CompoundAssign` must be a `Variable.Local` or
+`Variable.Field` — the concrete-to-abstract translator already enforces this.
 -/
 
 namespace Strata.Laurel
 
 public section
 
-/-- Reconstruct the read-side `StmtExprMd` for a `Variable`. -/
+/-- Reconstruct the read-side `StmtExprMd` for a `Variable`.
+
+    A `.Field` target duplicates the object subtree into the read operand (the lowering
+    emits `target op rhs`). This is sound — and term-size cost only, not a correctness
+    risk — because a field read lowers to the pure, obligation-free `readField` lookup,
+    so both copies read the same `$heap` at the same point. (Revisit if field reads ever
+    gain a precondition.) -/
 private def targetAsRead (target : VariableMd) : StmtExprMd :=
   let source := target.source
   match target.val with
@@ -54,6 +66,16 @@ private def targetAsRead (target : VariableMd) : StmtExprMd :=
   | .Field tgt fieldName => ⟨.Var (.Field tgt fieldName), source⟩
   | .Declare param => ⟨.Var (.Local param.name), source⟩
 
+/-- Build `.Assign [target] (target ⊕ rhs)` where `⊕` is `primOp`, yielding the new
+    value. Shared by the `IncrDecr` lowering (`rhs = 1`) and `CompoundAssign` (user's
+    RHS). The `.PrimitiveOp` keeps the default `skipProof := false`, so `/=`/`%=` carry
+    the same division-by-zero obligation as a hand-written `x := x / e`. -/
+private def lowerOpAssign (primOp : Operation) (target : VariableMd)
+    (rhs : StmtExprMd) (source : Option FileRange) : StmtExprMd :=
+  let read := targetAsRead target
+  let updated : StmtExprMd := ⟨.PrimitiveOp primOp [read, rhs], source⟩
+  ⟨.Assign [target] updated, source⟩
+
 /-- Build `.Assign [target] (target ⊕ 1)` where `⊕` is `Add` for `Incr` and
     `Sub` for `Decr`. The resulting assignment expression yields the new value. -/
 private def lowerToAssign (op : IncrDecrOp) (target : VariableMd)
@@ -61,10 +83,7 @@ private def lowerToAssign (op : IncrDecrOp) (target : VariableMd)
   let primOp : Operation := match op with
     | .Incr => .Add
     | .Decr => .Sub
-  let one : StmtExprMd := ⟨.LiteralInt 1, source⟩
-  let read := targetAsRead target
-  let updated : StmtExprMd := ⟨.PrimitiveOp primOp [read, one], source⟩
-  ⟨.Assign [target] updated, source⟩
+  lowerOpAssign primOp target ⟨.LiteralInt 1, source⟩ source
 
 /-- Lower a single `.IncrDecr` node to the expression form that yields the
     correct value for the given `mode` (Pre or Post). -/
@@ -82,10 +101,18 @@ private def lowerIncrDecr (mode : IncrDecrMode) (op : IncrDecrOp)
     ⟨.PrimitiveOp inverseOp [assign, one], source⟩
 
 /-- The rewrite step applied bottom-up by `mapStmtExpr`. Replaces `.IncrDecr`
-    with its lowered form; all other nodes pass through unchanged. -/
+    and `.CompoundAssign` with their lowered forms; all other nodes pass through.
+
+    `IncrDecr` and `CompoundAssign` share one lowering, `x := x ⊕ rhs` via
+    `lowerOpAssign` (`IncrDecr` supplies `rhs = 1`). We fuse both here rather
+    than lowering `IncrDecr → CompoundAssign → :=` in separate passes: same
+    shared lowering, one fewer traversal. Prefix `++x` is exactly that
+    assignment; only postfix `x++` adds an inverse-op wrapper to recover the
+    old value. -/
 private def rewriteNode (node : StmtExprMd) : StmtExprMd :=
   match node.val with
   | .IncrDecr mode op target => lowerIncrDecr mode op target node.source
+  | .CompoundAssign op target rhs => lowerOpAssign op target rhs node.source
   | _ => node
 
 /-- Apply the rewrite to a procedure (body, preconditions, decreases, invokeOn). -/
@@ -93,10 +120,10 @@ private def lowerProcedure (proc : Procedure) : Procedure :=
   mapProcedureM (m := Id) (mapStmtExpr rewriteNode) proc
 
 /--
-Eliminate every `.IncrDecr` node in a Laurel program by lowering it to
-existing constructs. After this pass, no `.IncrDecr` node remains.
+Eliminate every `.IncrDecr` and `.CompoundAssign` node in a Laurel program by
+lowering it to existing constructs. After this pass, neither node remains.
 -/
-def eliminateIncrDecr (program : Program) : Program :=
+def eliminateIncrDecrAndCompoundAssign (program : Program) : Program :=
   let staticProcs := program.staticProcedures.map lowerProcedure
   let types := program.types.map fun td =>
     match td with
@@ -105,11 +132,11 @@ def eliminateIncrDecr (program : Program) : Program :=
     | other => other
   { program with staticProcedures := staticProcs, types := types }
 
-/-- Pipeline pass: eliminate increment/decrement operators. -/
-public def eliminateIncrDecrPass : LaurelPass where
-  name := "EliminateIncrDecr"
-  documentation := "Lowers Java-style increment/decrement operators (`++x`, `x++`, `--x`, `x--`) into existing Laurel assignment and arithmetic constructs. Prefix forms yield the new value; postfix forms yield the old value. Runs early so that no later pass observes an `.IncrDecr` node."
-  run := fun p _m => (eliminateIncrDecr p, [], {})
+/-- Pipeline pass: eliminate increment/decrement and compound-assignment operators. -/
+public def eliminateIncrDecrAndCompoundAssignPass : LaurelPass where
+  name := "EliminateIncrDecrAndCompoundAssign"
+  documentation := "Lowers Java-style increment/decrement operators (`++x`, `x++`, `--x`, `x--`) and C-style compound assignments (`x += e`, `-=`, `*=`, `/=`, `%=`, `^=`) into existing Laurel assignment and arithmetic constructs. Prefix `++`/`--` and compound assignment yield the new value; postfix `++`/`--` yield the old value. Runs early so that no later pass observes an `.IncrDecr` or `.CompoundAssign` node."
+  run := fun p _m => (eliminateIncrDecrAndCompoundAssign p, [], {})
 
 end -- public section
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean
index 18bbca462b..fff2de1677 100644
--- a/Strata/Languages/Laurel/FilterPrelude.lean
+++ b/Strata/Languages/Laurel/FilterPrelude.lean
@@ -108,6 +108,12 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
     | .Field tgt _ => collectExprNames tgt
     | .Local _ => pure ()
     | .Declare param => collectHighTypeNames param.type
+  | .CompoundAssign _ target rhs =>
+    (match target.val with
+     | .Field tgt _ => collectExprNames tgt
+     | .Local _ => pure ()
+     | .Declare param => collectHighTypeNames param.type)
+    collectExprNames rhs
   | .Var (.Field target _) => collectExprNames target
   | .Var (.Declare param) => collectHighTypeNames param.type
   | .PureFieldUpdate target _ newVal =>
diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
index a4cd2ba3a0..af7cfd8414 100644
--- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
@@ -141,6 +141,20 @@ where
         | .Local name => laurelOp "identifier" #[ident name.text]
         | .Declare param => laurelOp "identifier" #[ident param.name.text]
       laurelOp opName #[targetArg]
+    | .CompoundAssign op target rhs =>
+      -- `op` is invariably Add/Sub/Mul/Div/Mod/StrConcat (the C2A translator only
+      -- builds those); the fallback emits a non-reparsing sentinel so a future
+      -- miswiring fails the round-trip instead of silently masquerading as `+=`.
+      let opName := match op with
+        | .Add => "addAssign" | .Sub => "subAssign" | .Mul => "mulAssign"
+        | .Div => "divAssign" | .Mod => "modAssign" | .StrConcat => "strConcatAssign"
+        | _ => "invalidCompoundAssign"
+      let targetArg := match target.val with
+        | .Field obj fieldName =>
+          laurelOp "fieldAccess" #[stmtExprToArg obj, ident fieldName.text]
+        | .Local name => laurelOp "identifier" #[ident name.text]
+        | .Declare param => laurelOp "identifier" #[ident param.name.text]
+      laurelOp opName #[targetArg, stmtExprToArg rhs]
     | .StaticCall callee args =>
       let calleeArg := laurelOp "identifier" #[ident callee.text]
       let argsArr := args.map stmtExprToArg |>.toArray
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index 2fe575e1cf..50a3775398 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -268,6 +268,24 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
     | q`Laurel.postDecr, #[arg0] =>
       let target ← translateIncrDecrTarget arg0 "postDecr"
       return mkStmtExprMd (.IncrDecr .Post .Decr target) src
+    | q`Laurel.addAssign, #[arg0, arg1] =>
+      let target ← translateIncrDecrTarget arg0 "+="
+      return mkStmtExprMd (.CompoundAssign .Add target (← translateStmtExpr arg1)) src
+    | q`Laurel.subAssign, #[arg0, arg1] =>
+      let target ← translateIncrDecrTarget arg0 "-="
+      return mkStmtExprMd (.CompoundAssign .Sub target (← translateStmtExpr arg1)) src
+    | q`Laurel.mulAssign, #[arg0, arg1] =>
+      let target ← translateIncrDecrTarget arg0 "*="
+      return mkStmtExprMd (.CompoundAssign .Mul target (← translateStmtExpr arg1)) src
+    | q`Laurel.divAssign, #[arg0, arg1] =>
+      let target ← translateIncrDecrTarget arg0 "/="
+      return mkStmtExprMd (.CompoundAssign .Div target (← translateStmtExpr arg1)) src
+    | q`Laurel.modAssign, #[arg0, arg1] =>
+      let target ← translateIncrDecrTarget arg0 "%="
+      return mkStmtExprMd (.CompoundAssign .Mod target (← translateStmtExpr arg1)) src
+    | q`Laurel.strConcatAssign, #[arg0, arg1] =>
+      let target ← translateIncrDecrTarget arg0 "^="
+      return mkStmtExprMd (.CompoundAssign .StrConcat target (← translateStmtExpr arg1)) src
     | q`Laurel.multiAssign, #[targetsSeq, valueArg] =>
       let targets ← match targetsSeq with
         | .seq _ .comma args => args.toList.mapM fun targ => do
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 80f80911ba..13114f04a4 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -12,7 +12,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: renamed strConcat token to `^`; added preIncr/preDecr/postIncr/postDecr; `return` value is now Option StmtExpr (supports a valueless return).
+-- Last grammar change: added compound assignment ops (`+=`, `-=`, `*=`, `/=`, `%=`, `^=`).
 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 ae8316a01b..058b9a28b2 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -50,6 +50,16 @@ op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
 // Assignment
 op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target " := " value;
 
+// Compound assignment (`x op= e`). Same precedence as `assign`; rightassoc so
+// `a += b += c` groups as `a += (b += c)`. Lvalue-ness of `target` is enforced in
+// the concrete-to-abstract translator, not the grammar.
+op addAssign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10), rightassoc] target " += " value;
+op subAssign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10), rightassoc] target " -= " value;
+op mulAssign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10), rightassoc] target " *= " value;
+op divAssign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10), rightassoc] target " /= " value;
+op modAssign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10), rightassoc] target " %= " value;
+op strConcatAssign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10), rightassoc] target " ^= " value;
+
 // Multi-target assignment: assign var x: int, y, var z: int := call()
 // Uses the 'assign' keyword to avoid ambiguity with other comma-separated constructs.
 category AssignTarget;
diff --git a/Strata/Languages/Laurel/LaurelAST.lean b/Strata/Languages/Laurel/LaurelAST.lean
index d9638174b0..30371149f4 100644
--- a/Strata/Languages/Laurel/LaurelAST.lean
+++ b/Strata/Languages/Laurel/LaurelAST.lean
@@ -328,6 +328,15 @@ inductive StmtExpr : Type where
       yielded value is discarded.
       Eliminated by the `EliminateIncrDecr` pass before lifting imperative expressions. -/
   | IncrDecr (mode : IncrDecrMode) (op : IncrDecrOp) (target : AstNode Variable)
+  /-- C-style compound assignment (`x += e`, `x -= e`, `x *= e`, `x /= e`, `x %= e`),
+      plus `x ^= e` for string concatenation (Laurel uses `^` for concat, OCaml-style,
+      not bitwise XOR). Lowers to `target := target op rhs` and yields the new value.
+      The target must be a `Local` or `Field` `Variable`.
+      Invariant: `op` is one of `Add`/`Sub`/`Mul`/`Div`/`Mod`/`StrConcat` — the only
+      operators the concrete-to-abstract translator ever constructs here. Downstream
+      sites may treat any other `Operation` as a `StrataBug`.
+      Eliminated by the `EliminateIncrDecr` pass before lifting imperative expressions. -/
+  | CompoundAssign (op : Operation) (target : AstNode Variable) (rhs : AstNode StmtExpr)
   /-- Update a field on a pure (value) type, producing a new value. -/
   | PureFieldUpdate (target : AstNode StmtExpr) (fieldName : Identifier) (newValue : AstNode StmtExpr)
   /-- Call a static procedure by name with the given arguments. -/
@@ -402,6 +411,7 @@ def StmtExpr.constrName : StmtExpr → String
   | .Assign ..           => ":="
   | .IncrDecr _ .Incr .. => "++"
   | .IncrDecr _ .Decr .. => "--"
+  | .CompoundAssign ..   => "compound assignment"
   | .PureFieldUpdate ..  => "field update"
   | .StaticCall ..       => "call"
   | .PrimitiveOp op ..   => toString op
@@ -741,6 +751,7 @@ def StmtExpr.constructorName (e : StmtExpr) : String :=
   | .All => "All"
   | .Hole .. => "Hole"
   | .IncrDecr .. => "IncrDecr"
+  | .CompoundAssign .. => "CompoundAssign"
 
 /-- Check whether a single modifies entry is the wildcard (`*`). -/
 def StmtExprMd.isWildcard (m : StmtExprMd) : Bool := match m.val with | .All => true | _ => false
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index ce500d1ab3..63e1b01e2f 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -7,7 +7,7 @@ module
 
 public import Strata.Languages.Laurel.LaurelToCoreTranslator
 import Strata.Languages.Laurel.DesugarShortCircuit
-import Strata.Languages.Laurel.EliminateIncrDecr
+import Strata.Languages.Laurel.EliminateIncrDecrAndCompoundAssign
 import Strata.Languages.Laurel.MergeAndLiftReturns
 import Strata.Languages.Laurel.EliminateValueInReturns
 import Strata.Languages.Laurel.ModifiesClauses
@@ -93,7 +93,7 @@ abbrev TranslateResultWithLaurel := (Option Core.Program) × (List DiagnosticMod
 
 /-- The ordered sequence of Laurel-to-Laurel lowering passes. -/
 def laurelPipeline : Array LaurelPass := #[
-  eliminateIncrDecrPass,
+  eliminateIncrDecrAndCompoundAssignPass,
   typeAliasElimPass,
   filterNonCompositeModifiesPass,
   liftInstanceProceduresPass,
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index 7ffdc5b0dd..f0431092cc 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -261,6 +261,9 @@ def translateExpr (expr : StmtExprMd)
   | .IncrDecr _ _ _ =>
       throwExprDiagnostic $ diagnosticFromSource expr.source
         "IncrDecr should have been eliminated by EliminateIncrDecr pass" DiagnosticType.StrataBug
+  | .CompoundAssign _ _ _ =>
+      throwExprDiagnostic $ diagnosticFromSource expr.source
+        "CompoundAssign should have been eliminated by EliminateIncrDecr pass" DiagnosticType.StrataBug
   | .While _ _ _ _ =>
       disallowed expr.source "loops are not supported in functions or contracts"
   | .Exit _ => disallowed expr.source "exit is not supported in expression position"
diff --git a/Strata/Languages/Laurel/LaurelTypes.lean b/Strata/Languages/Laurel/LaurelTypes.lean
index f39632ca90..7e34d1f6d0 100644
--- a/Strata/Languages/Laurel/LaurelTypes.lean
+++ b/Strata/Languages/Laurel/LaurelTypes.lean
@@ -89,6 +89,12 @@ def computeExprType (model : SemanticModel) (expr : StmtExprMd) : HighTypeMd :=
     | .Local id => (model.get id).getType
     | .Field _ fieldName => (model.get fieldName).getType
     | .Declare _ => ⟨ .TVoid, source ⟩  -- shouldn't happen; rejected by translator
+  | .CompoundAssign _ target _ =>
+    -- Yields the new value, whose type is the target variable's type.
+    match target.val with
+    | .Local id => (model.get id).getType
+    | .Field _ fieldName => (model.get fieldName).getType
+    | .Declare _ => ⟨ .TVoid, source ⟩  -- shouldn't happen; rejected by translator
   | .Assert _ => ⟨ .TVoid, source ⟩
   | .Assume _ => ⟨ .TVoid, source ⟩
   -- Instance related
diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 2d15f56c2f..664cfa4268 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -156,6 +156,7 @@ def containsAssignment (expr : StmtExprMd) : Bool :=
   match val with
   | .Assign .. => true
   | .IncrDecr .. => true
+  | .CompoundAssign .. => true
   | .StaticCall _ args => args.attach.any (fun x => containsAssignment x.val)
   | .PrimitiveOp _ args _ => args.attach.any (fun x => containsAssignment x.val)
   | .Block stmts _ => stmts.attach.any (fun x => containsAssignment x.val)
@@ -175,6 +176,7 @@ def containsBareAssignment (expr : StmtExprMd) : Bool :=
   match val with
   | .Assign .. => true
   | .IncrDecr .. => true
+  | .CompoundAssign .. => true
   | .StaticCall _ args => args.attach.any (fun x => containsBareAssignment x.val)
   | .PrimitiveOp _ args _ => args.attach.any (fun x => containsBareAssignment x.val)
   | .Block _ _ => false
diff --git a/Strata/Languages/Laurel/MapStmtExpr.lean b/Strata/Languages/Laurel/MapStmtExpr.lean
index 4db4592b29..7a198edd7e 100644
--- a/Strata/Languages/Laurel/MapStmtExpr.lean
+++ b/Strata/Languages/Laurel/MapStmtExpr.lean
@@ -59,6 +59,11 @@ def mapStmtExprM [Monad m] (f : StmtExprMd → m StmtExprMd) (expr : StmtExprMd)
   | .IncrDecr mode op ⟨.Field tgt fieldName, vs⟩ =>
     pure ⟨.IncrDecr mode op ⟨.Field (← mapStmtExprM f tgt) fieldName, vs⟩, source⟩
   | .IncrDecr _ _ ⟨.Local _, _⟩ | .IncrDecr _ _ ⟨.Declare _, _⟩ => pure expr
+  -- `.CompoundAssign` carries an `rhs` that must be traversed even for Local/Declare targets.
+  | .CompoundAssign op ⟨.Field tgt fieldName, vs⟩ rhs =>
+    pure ⟨.CompoundAssign op ⟨.Field (← mapStmtExprM f tgt) fieldName, vs⟩ (← mapStmtExprM f rhs), source⟩
+  | .CompoundAssign op target rhs =>
+    pure ⟨.CompoundAssign op target (← mapStmtExprM f rhs), source⟩
   | .PureFieldUpdate target fieldName newValue =>
     pure ⟨.PureFieldUpdate (← mapStmtExprM f target) fieldName (← mapStmtExprM f newValue), source⟩
   | .StaticCall callee args =>
@@ -149,6 +154,12 @@ def mapStmtExprPrePostM [Monad m] (pre : StmtExprMd → m (Option StmtExprMd))
   | .IncrDecr mode op ⟨.Field tgt fieldName, vs⟩ =>
     pure ⟨.IncrDecr mode op ⟨.Field (← mapStmtExprPrePostM pre post tgt) fieldName, vs⟩, source⟩
   | .IncrDecr _ _ ⟨.Local _, _⟩ | .IncrDecr _ _ ⟨.Declare _, _⟩ => pure expr
+  -- `.CompoundAssign` carries an `rhs` that must be traversed even for Local/Declare targets.
+  | .CompoundAssign op ⟨.Field tgt fieldName, vs⟩ rhs =>
+    pure ⟨.CompoundAssign op ⟨.Field (← mapStmtExprPrePostM pre post tgt) fieldName, vs⟩
+      (← mapStmtExprPrePostM pre post rhs), source⟩
+  | .CompoundAssign op target rhs =>
+    pure ⟨.CompoundAssign op target (← mapStmtExprPrePostM pre post rhs), source⟩
   | .PureFieldUpdate target fieldName newValue =>
     pure ⟨.PureFieldUpdate (← mapStmtExprPrePostM pre post target) fieldName
       (← mapStmtExprPrePostM pre post newValue), source⟩
@@ -254,6 +265,8 @@ def mapNodeHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (expr : StmtEx
     pure ⟨.Assign targets' value, source⟩
   | .IncrDecr mode op target =>
     pure ⟨.IncrDecr mode op ⟨← mapVariableHighTypesM f target.val, target.source⟩, source⟩
+  | .CompoundAssign op target rhs =>
+    pure ⟨.CompoundAssign op ⟨← mapVariableHighTypesM f target.val, target.source⟩ rhs, 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⟩
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index f79b5fb5ee..b0a0f2e546 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -504,6 +504,25 @@ private def underlyingBaseType (s : ResolveState) (fuel : Nat) (ty : HighType) :
       | _ => ty
     | _ => ty
 
+/-- A short display name for a primitive/base `HighType`, for compound-assignment
+    diagnostics. Shared by the target check and the RHS check so their wording
+    cannot drift. -/
+private def highTypeDisplayName : HighType → String
+  | .TInt => "int" | .TReal => "real" | .TFloat64 => "float64"
+  | .TString => "string" | .TBool => "bool" | .TBv n => s!"bv{n}"
+  | .UserDefined r => r.text | _ => "<unknown>"
+
+/-- Whether the (already base-peeled) element type `baseTy` is an acceptable target
+    for compound-assignment operator `op`. Used by the resolution-time target check
+    (`checkCompoundAssignTargetType`), driven by what the Laurel→Core lowering of
+    `target op rhs` supports: `+= -= *= /=` accept `int`/`real`; `%=` is `int`-only
+    (`.Mod` has no real lowering); `^=` is `string`-only. -/
+private def compoundAssignAccepts (op : Operation) (baseTy : HighType) : Bool :=
+  match op with
+  | .StrConcat => match baseTy with | .TString => true | _ => false
+  | .Mod       => match baseTy with | .TInt => true | _ => false
+  | _          => match baseTy with | .TInt | .TReal => true | _ => false
+
 /-- Look up the declared type of an `IncrDecr` target during resolution.
     Handles `Local` (scope lookup) and `Field` (type-scope lookup); returns
     `none` when the type cannot be determined (e.g. an unresolved name). -/
@@ -557,6 +576,30 @@ private def checkIncrDecrTargetType (op : IncrDecrOp) (target : VariableMd)
            Use an explicit assignment instead, e.g. 'x := x + 1'."
       modify fun s => { s with errors := s.errors.push diag }
 
+/-- Emit a diagnostic if a compound-assignment operator is applied to an unsupported
+    target element type, per `compoundAssignAccepts`. Checks only the *target*; the RHS
+    is type-checked by the `Check.resolveStmtExpr` call in `Synth.compoundAssign`. -/
+private def checkCompoundAssignTargetType (op : Operation) (target : VariableMd)
+    (source : Option FileRange) : ResolveM Unit := do
+  match (← incrDecrTargetType target) with
+  | none => pure ()
+  | some ty =>
+    let s ← get
+    let baseTy := underlyingBaseType s 100 ty
+    let opTok := match op with
+      | .Add => "+=" | .Sub => "-=" | .Mul => "*=" | .Div => "/="
+      | .Mod => "%=" | .StrConcat => "^=" | _ => "(compound assignment)"
+    if !(compoundAssignAccepts op baseTy) then
+      let allowed := match op with
+        | .StrConcat => "'string'"
+        | .Mod => "'int' and int-based constrained types (e.g. 'nat')"
+        | _ => "'int', int-based constrained types (e.g. 'nat'), and 'real'"
+      let tyName := highTypeDisplayName baseTy
+      let diag := diagnosticFromSource source
+        s!"The '{opTok}' operator is only supported on {allowed}, but the operand has \
+           type '{tyName}'. Use an explicit assignment instead, e.g. 'x := x {opTok.dropEnd 1} e'."
+      modify fun s => { s with errors := s.errors.push diag }
+
 /-! ## Typing rules
 
 The judgment is bidirectional:
@@ -665,6 +708,8 @@ def Synth.resolveStmtExpr (exprMd : StmtExprMd) : ResolveM (StmtExprMd × HighTy
   | .Var (.Local ref) => Synth.varLocal ref source
   | .IncrDecr mode op target =>
     Synth.incrDecr exprMd mode op target source (by rw [h_node])
+  | .CompoundAssign op target rhs =>
+    Synth.compoundAssign exprMd op target rhs source (by rw [h_node])
   | .Var (.Field target fieldName) =>
     Synth.varField exprMd target fieldName source (by rw [h_node])
   | .Assign targets value =>
@@ -1611,6 +1656,62 @@ def Synth.incrDecr (exprMd : StmtExprMd)
     simp only [Variable.Field.sizeOf_spec] at hsz2
     omega
 
+/-- (CompoundAssign)
+    ```
+    Γ ⊢ target ⇒ T    T accepts op    Γ ⊢ rhs ⇐ T
+    ─────────────────────────────────────────────
+    Γ ⊢ CompoundAssign op target rhs ⇒ T
+    ```
+    `x op= e` reads and writes its target, so it synthesizes the target's own type
+    `T` and checks the RHS against it. Reviewable by analogy to two existing rules:
+    target resolution is identical to `Synth.incrDecr` (including the conservative
+    `.Declare` arm — unlike `Synth.assign`, the target is never *introduced*, so no
+    `defineNameCheckDup`); the RHS is then checked against the single target type with
+    `Check.resolveStmtExpr`, as `Synth.assign` does for its (here always single) target.
+    The element type is checked by `checkCompoundAssignTargetType`. Used in expression
+    position (`var y := (x += 2)`); in statement position the value is discarded by
+    `Check.statement`. -/
+def Synth.compoundAssign (exprMd : StmtExprMd)
+    (op : Operation) (target : VariableMd) (rhs : StmtExprMd)
+    (source : Option FileRange)
+    (h : exprMd.val = .CompoundAssign op target rhs) :
+    ResolveM (StmtExpr × HighTypeMd) := do
+  let target' ← match h_tgt : target.val with
+    | .Local ref =>
+      let ref' ← resolveRef ref source
+      pure (⟨.Local ref', target.source⟩ : VariableMd)
+    | .Field tgt fieldName =>
+      let (tgt', _) ← Synth.resolveStmtExpr tgt
+      let fieldName' ← resolveFieldRef tgt' fieldName source
+      pure (⟨.Field tgt' fieldName', target.source⟩ : VariableMd)
+    | .Declare param =>
+      -- Should not occur — the translator rejects a declaration target.
+      let ty' ← resolveHighType param.type
+      pure (⟨.Declare ⟨param.name, ty'⟩, target.source⟩ : VariableMd)
+  checkCompoundAssignTargetType op target' source
+  let resultTy ← match target'.val with
+    | .Local ref => getVarType ref
+    | .Declare param => pure param.type
+    | .Field _ fieldName => getVarType fieldName
+  let rhs' ← Check.resolveStmtExpr rhs resultTy
+  pure (.CompoundAssign op target' rhs', resultTy)
+  termination_by (exprMd, 1)
+  decreasing_by
+    -- Two recursive calls, two obligations, both discharged by this block:
+    -- `Check rhs` (rhs is a direct subterm) needs only the CompoundAssign step;
+    -- `Synth tgt` (Field arm, tgt nested in the target) also needs the `target`
+    -- step — hence the `try`. This is `Synth.incrDecr`'s proof generalised with
+    -- `all_goals` to also cover the rhs obligation.
+    all_goals
+      apply Prod.Lex.left
+      have hsz := exprMd.sizeOf_val_lt
+      rw [h] at hsz
+      simp only [StmtExpr.CompoundAssign.sizeOf_spec] at hsz
+      try (have hsz2 := target.sizeOf_val_lt
+           rw [h_tgt] at hsz2
+           simp only [Variable.Field.sizeOf_spec] at hsz2)
+      omega
+
 -- ### Calls
 
 /-- Cases on the arity of the callee's declared outputs.
@@ -2840,6 +2941,8 @@ private def collectStmtExpr (map : Std.HashMap Nat ResolvedNode) (expr : StmtExp
     collectStmtExpr map value
   | .IncrDecr _ _ ⟨.Field tgt _, _⟩ => collectStmtExpr map tgt
   | .IncrDecr _ _ ⟨.Local _, _⟩ | .IncrDecr _ _ ⟨.Declare _, _⟩ => map
+  | .CompoundAssign _ ⟨.Field tgt _, _⟩ rhs => collectStmtExpr (collectStmtExpr map tgt) rhs
+  | .CompoundAssign _ _ rhs => collectStmtExpr map rhs
   | .Var (.Field target _) => collectStmtExpr map target
   | .PureFieldUpdate target _ newVal =>
     let map := collectStmtExpr map target
@@ -3038,6 +3141,14 @@ def validateDiamondFieldAccessesForStmtExpr (model : SemanticModel)
       let fieldError := checkDiamondFieldAccess model tgt fieldName target.source
       innerErrors ++ fieldError
     | .Local _ | .Declare _ => []
+  | .CompoundAssign _ target rhs =>
+    let rhsErrors := validateDiamondFieldAccessesForStmtExpr model rhs
+    let targetErrors := match _htgt : target.val with
+      | .Field tgt fieldName =>
+        validateDiamondFieldAccessesForStmtExpr model tgt
+          ++ checkDiamondFieldAccess model tgt fieldName target.source
+      | .Local _ | .Declare _ => []
+    targetErrors ++ rhsErrors
   | _ => []
   termination_by sizeOf expr
   decreasing_by
diff --git a/StrataTest/Languages/Laurel/CompoundAssignLiftTest.lean b/StrataTest/Languages/Laurel/CompoundAssignLiftTest.lean
new file mode 100644
index 0000000000..4e99f44e98
--- /dev/null
+++ b/StrataTest/Languages/Laurel/CompoundAssignLiftTest.lean
@@ -0,0 +1,141 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+/-
+Tests that the EliminateIncrDecr + LiftImperativeExpressions pipeline correctly
+lowers C-style compound assignment (`+=`, `-=`, …) by comparing the lowered
+Laurel against expected output. `x op= e` lowers to `x := x op e`; in expression
+position the assignment is lifted out and yields the new value.
+-/
+
+meta import StrataDDM.Elab
+meta import StrataDDM.BuiltinDialects.Init
+meta import Strata.Languages.Laurel.Grammar
+meta import Strata.Languages.Laurel.LaurelToCoreTranslator
+meta import Strata.Languages.Laurel.EliminateIncrDecrAndCompoundAssign
+meta import Strata.Languages.Laurel.LiftImperativeExpressions
+
+meta section
+
+open Strata
+open StrataDDM (initDialect)
+open StrataDDM.Elab (parseStrataProgramFromDialect)
+
+namespace Strata.Laurel
+
+/-- Parse, run EliminateIncrDecr (which also eliminates CompoundAssign), then
+    LiftImperativeExpressions, so test output reflects the Laurel fed to Core. -/
+def parseLowerCompoundAssign (input : String) : IO Program := do
+  let inputCtx := StrataDDM.Parser.stringInputContext "test" input
+  let dialects := StrataDDM.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
+  let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name inputCtx
+  let uri := Strata.Uri.file "test"
+  match Laurel.TransM.run uri (Laurel.parseProgram strataProgram) with
+  | .error e => throw (IO.userError s!"Translation errors: {e}")
+  | .ok program =>
+    let program := eliminateIncrDecrAndCompoundAssign program
+    let result := resolve program
+    let (program, model) := (result.program, result.model)
+    pure (liftExpressionAssignments model program)
+
+/-- Statement form: `x += 3` lowers to a clean `x := x + 3`. -/
+def stmtFormProgram : String := r"
+procedure stmtForm()
+  opaque
+{
+  var x: int := 0;
+  x += 3;
+  x -= 1
+};
+"
+
+/--
+info: procedure stmtForm()
+  opaque
+{
+  var x: int := 0;
+  x := x + 3;
+  x := x - 1
+};
+-/
+#guard_msgs in
+#eval! do
+  let program ← parseLowerCompoundAssign stmtFormProgram
+  for proc in program.staticProcedures do
+    IO.println (toString (Std.Format.pretty (Std.ToFormat.format proc)))
+
+/-- Expression position: `(x += 2)` yields the new value; the assignment is
+    lifted out ahead of the use. -/
+def exprFormProgram : String := r"
+procedure exprForm()
+  opaque
+{
+  var x: int := 5;
+  var y: int := (x += 2);
+  assert x == 7;
+  assert y == 7
+};
+"
+
+/--
+info: procedure exprForm()
+  opaque
+{
+  var x: int := 5;
+  var $x_0: int := x;
+  x := x + 2;
+  var y: int := x;
+  assert x == 7;
+  assert y == 7
+};
+-/
+#guard_msgs in
+#eval! do
+  let program ← parseLowerCompoundAssign exprFormProgram
+  for proc in program.staticProcedures do
+    IO.println (toString (Std.Format.pretty (Std.ToFormat.format proc)))
+
+/-- Nested side-effecting RHS: `x += (y += 1)` lowers bottom-up. One level of
+    nesting is supported. Deeper nesting (`x += (y += (z += 1))`) hits a
+    pre-existing limitation of `LiftImperativeExpressions` — it errors with
+    "destructive assignments … should have been lifted" — that also affects plain
+    nested assignment (`x := (y := (z := 5))`) on the base, independent of compound
+    assignment. Not exercised here so the test doesn't pin that broken output. -/
+def nestedRhsProgram : String := r"
+procedure nestedRhs()
+  opaque
+{
+  var x: int := 1;
+  var y: int := 10;
+  x += (y += 1);
+  assert y == 11;
+  assert x == 12
+};
+"
+
+/--
+info: procedure nestedRhs()
+  opaque
+{
+  var x: int := 1;
+  var y: int := 10;
+  var $y_0: int := y;
+  y := y + 1;
+  x := x + y;
+  assert y == 11;
+  assert x == 12
+};
+-/
+#guard_msgs in
+#eval! do
+  let program ← parseLowerCompoundAssign nestedRhsProgram
+  for proc in program.staticProcedures do
+    IO.println (toString (Std.Format.pretty (Std.ToFormat.format proc)))
+
+end Laurel
+end Strata
+end
diff --git a/StrataTest/Languages/Laurel/CompoundAssignTypeRejectionTest.lean b/StrataTest/Languages/Laurel/CompoundAssignTypeRejectionTest.lean
new file mode 100644
index 0000000000..57bb0b42f4
--- /dev/null
+++ b/StrataTest/Languages/Laurel/CompoundAssignTypeRejectionTest.lean
@@ -0,0 +1,162 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Compound-assignment type rules. The accepted element types are per-operator,
+driven by what the Laurel→Core lowering of `target op rhs` supports:
+
+  * `+= -= *= /=` — `int`, int-based constrained types, and `real`.
+  * `%=`          — `int` (and int-based constrained) only (`.Mod` has no real
+                    lowering).
+  * `^=`          — `string` only.
+
+Two independent checks reject a bad compound assignment: `checkCompoundAssignTargetType`
+flags an operator applied to an unsupported *target* element type (e.g. `^=` on an int,
+`%=`/`+=` on a real/bv), and the bidirectional typing's `Check` rule flags a *RHS* whose
+type doesn't match the target (`expected 'T', got 'U'`). A statement that is wrong both
+ways (e.g. `s += 1`: `+=` rejects a string target, and the int RHS mismatches the string
+target) legitimately reports both — same as elsewhere in the type checker.
+
+This file also pins the *intended* asymmetry with `++`/`--`: `r += 1.0` on a real
+succeeds (user-written RHS), while `r++` is rejected (synthesized int `1`; `realVar + 1`
+is a type error under strict numeric typing). That asymmetry is deliberate, not a bug.
+-/
+
+import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+open Strata
+
+/-! ## Rejected: target-type violations
+
+Each uses a RHS whose type matches the target, so only the target-type check fires
+(an op-vs-target mismatch, not a RHS mismatch). -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+procedure strConcatOnInt() opaque {
+  var x: int := 0;
+  x ^= 1
+//^^^^^^ error: The '^=' operator is only supported on 'string'
+};
+procedure addOnString() opaque {
+  var s: string := "a";
+  s += "b"
+//^^^^^^^^ error: but the operand has type 'string'
+};
+procedure modOnReal() opaque {
+  var r: real := 1.0;
+  r %= 2.0
+//^^^^^^^^ error: The '%=' operator is only supported on 'int' and int-based constrained types
+};
+procedure addOnBv(y: bv 32) opaque {
+  var b: bv 32 := y;
+  b += y
+//^^^^^^ error: but the operand has type 'bv32'
+};
+procedure addOnFloat64(g: float64) opaque {
+  var f: float64 := g;
+  f += g
+//^^^^^^ error: but the operand has type 'float64'
+};
+procedure modOnBv(y: bv 32) opaque {
+  var b: bv 32 := y;
+  b %= y
+//^^^^^^ error: The '%=' operator is only supported on 'int' and int-based constrained types
+};
+procedure concatOnReal() opaque {
+  var r: real := 1.0;
+  r ^= r
+//^^^^^^ error: The '^=' operator is only supported on 'string'
+};
+#end
+
+/-! ## Rejected: RHS-type mismatch (valid target, wrong RHS — caught by the `Check` rule) -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+procedure intPlusString() opaque {
+  var x: int := 0;
+  x += "s"
+//     ^^^ error: expected 'int', got 'string'
+};
+procedure strConcatIntRhs() opaque {
+  var s: string := "a";
+  s ^= 1
+//     ^ error: expected 'string', got 'int'
+};
+#end
+
+/-! ## Accepted: `+=` on int, real, and a constrained int -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+constrained nat = v: int where v >= 0 witness 0
+procedure addReal() opaque {
+  var r: real := 1.0;
+  r += 1.0;
+  assert r == 2.0
+};
+procedure addNat() opaque {
+  var n: nat := 1;
+  n += 2;
+  assert n == 3
+};
+#end
+
+/-! ## The intended `++`-vs-`+=` asymmetry on reals
+
+`r += 1.0` succeeds (above); `r++` is rejected (below). Side by side so the
+divergence is documented as deliberate, not a regression to be "fixed". -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+procedure incrReal() opaque {
+  var r: real := 1.0;
+  r++
+//^^^ error: The increment ('++') operator is only supported on 'int' and int-based constrained types
+};
+#end
+
+/-! ## A real-based constrained type is rejected by `%=` (peels to `real`)
+
+`checkCompoundAssignTargetType` peels the constraint via `underlyingBaseType`, so a
+`real`-backed constrained type lands on the same `%=`-rejects-`real` rule. -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+constrained posReal = v: real where v >= 0.0 witness 0.0
+procedure modConstrainedReal() opaque {
+  var r: posReal := 1.0;
+  r %= 2.0
+//^^^^^^^^ error: The '%=' operator is only supported on 'int' and int-based constrained types
+};
+#end
+
+/-! ## `/= 0` and `%= 0` retain the division-by-zero proof obligation (`skipProof := false`)
+
+`x /= d` / `x %= d` lower to `x := x / d` / `x := x % d`, which carry the divisor≠0 VC.
+With an unconstrained divisor the assertion-that-it-succeeds cannot be proved. -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+procedure divByZero(d: int) opaque {
+  var x: int := 10;
+  x /= d
+//^^^^^^ error: assertion does not hold
+};
+procedure modByZero(d: int) opaque {
+  var x: int := 10;
+  x %= d
+//^^^^^^ error: assertion does not hold
+};
+#end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T24_CompoundAssign.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T24_CompoundAssign.lean
new file mode 100644
index 0000000000..055456d106
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T24_CompoundAssign.lean
@@ -0,0 +1,245 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+open Strata
+
+/-!
+End-to-end verification of C-style compound assignment (`+=`, `-=`, `*=`,
+`/=`, `%=`, and `^=` for string concatenation), on locals (first program) and on composite-type fields
+including chained targets (second program), in both statement and expression
+positions.
+
+`x op= e` lowers (in `EliminateIncrDecr`) to `x := x op e` and yields the new
+value. The accepted element types are per-operator: `+= -= *= /=` work on `int`
+and `real`; `%=` is `int`-only; `^=` is `string`-only. (Rejections are covered in
+`CompoundAssignTypeRejectionTest.lean`; the `++`/`--`-vs-`+=` real asymmetry is
+pinned there too.)
+
+Field targets go through Laurel's heap parameterization: `EliminateIncrDecr`
+(pass 1) lowers `(c#n) += e` to `c#n := c#n + e`; `HeapParameterization` (pass 5)
+rewrites the field-assign into `$tmp`/`$heap` local-target sequences, so by the
+time `LiftImperativeExpressions` (pass 11) runs every assignment target is a
+local. `c#n += e` parses paren-free because `fieldAccess` (prec 95) binds tighter
+than `+=` (prec 10).
+-/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+constrained nat = v: int where v >= 0 witness 0
+procedure intOperators()
+  opaque
+{
+  var x: int := 10;
+  x += 5;
+  assert x == 15;
+  x -= 3;
+  assert x == 12;
+  x *= 2;
+  assert x == 24;
+  x /= 4;
+  assert x == 6;
+  x %= 4;
+  assert x == 2
+};
+
+procedure exprYieldsNewValue()
+  opaque
+{
+  var x: int := 5;
+  // Compound assignment in expression position yields the NEW value.
+  var y: int := (x += 2);
+  assert x == 7;
+  assert y == 7
+};
+
+procedure exprYieldsNewValueNonPlus()
+  opaque
+{
+  // The yielded value is the new value for every operator, not just `+=`.
+  var x: int := 10;
+  var y: int := (x -= 3);
+  assert x == 7;
+  assert y == 7;
+  var s: string := "a";
+  var t: string := (s ^= "b");
+  assert s == "ab";
+  assert t == "ab"
+};
+
+procedure intDivMod()
+  opaque
+{
+  // Integer `/=` truncates and `%=` is the matching remainder (not exact division).
+  var x: int := 7;
+  x /= 2;
+  assert x == 3;
+  var w: int := 7;
+  w %= 3;
+  assert w == 1
+};
+
+procedure nestedRhs()
+  opaque
+{
+  var x: int := 1;
+  var y: int := 10;
+  // RHS itself contains a compound assignment; lowered bottom-up.
+  x += (y += 1);
+  assert y == 11;
+  assert x == 12
+};
+
+procedure realOperators()
+  opaque
+{
+  var r: real := 1.5;
+  r += 2.5;
+  assert r == 4.0;
+  r -= 1.0;
+  assert r == 3.0;
+  r *= 2.0;
+  assert r == 6.0;
+  r /= 2.0;
+  assert r == 3.0
+};
+
+procedure stringConcat()
+  opaque
+{
+  var s: string := "foo";
+  s ^= "bar";
+  assert s == "foobar"
+};
+
+procedure constrainedInt()
+  opaque
+{
+  var n: nat := 3;
+  n += 2;
+  assert n == 5
+};
+
+procedure rightAssocChain()
+  opaque
+{
+  // The ops are `rightassoc`, so `a += b += c` groups as `a += (b += c)`.
+  var a: int := 1;
+  var b: int := 2;
+  var c: int := 3;
+  a += b += c;
+  // b += c : b becomes 5, yields 5; a += 5 : a becomes 6.
+  assert b == 5;
+  assert a == 6
+};
+#end
+
+-- Compound assignment on composite-type fields, including chained targets.
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Counter {
+  var n: int
+}
+
+composite Inner {
+  var count: int
+}
+
+composite Outer {
+  var inner: Inner
+}
+
+composite RBox {
+  var r: real
+}
+
+composite SBox {
+  var s: string
+}
+
+procedure fieldStatement()
+  opaque
+{
+  var c: Counter := new Counter;
+  c#n := 10;
+  c#n += 5;
+  assert c#n == 15;
+  c#n -= 3;
+  assert c#n == 12;
+  c#n *= 2;
+  assert c#n == 24
+};
+
+procedure fieldInExpression()
+  opaque
+{
+  var c: Counter := new Counter;
+  c#n := 5;
+  // Yields the NEW field value (7); c#n is updated to 7.
+  var y: int := (c#n += 2);
+  assert c#n == 7;
+  assert y == 7
+};
+
+// Compound assign through a chained field target (`o#inner#count += e`).
+procedure chainedFieldStatement()
+  opaque
+{
+  var o: Outer := new Outer;
+  var i: Inner := new Inner;
+  o#inner := i;
+  o#inner#count := 10;
+  o#inner#count += 5;
+  assert o#inner#count == 15
+};
+
+procedure chainedFieldInExpression()
+  opaque
+{
+  var o: Outer := new Outer;
+  var i: Inner := new Inner;
+  o#inner := i;
+  o#inner#count := 5;
+  var y: int := (o#inner#count += 2);
+  assert o#inner#count == 7;
+  assert y == 7
+};
+
+// Non-`+=`/`int` operators on field targets: real `/=`, string `^=`, and an
+// int field `/=` (whose lowered division-by-zero VC must discharge for a
+// constant nonzero divisor). These exercise the field heap-rewrite path for
+// the operators the single `c#n += …` cases above don't reach.
+procedure realFieldDiv()
+  opaque
+{
+  var b: RBox := new RBox;
+  b#r := 6.0;
+  b#r /= 2.0;
+  assert b#r == 3.0
+};
+
+procedure stringFieldConcat()
+  opaque
+{
+  var b: SBox := new SBox;
+  b#s := "foo";
+  b#s ^= "bar";
+  assert b#s == "foobar"
+};
+
+procedure intFieldDiv()
+  opaque
+{
+  var c: Counter := new Counter;
+  c#n := 7;
+  c#n /= 2;
+  assert c#n == 3
+};
+#end
diff --git a/StrataTest/Languages/Laurel/IncrDecrLiftTest.lean b/StrataTest/Languages/Laurel/IncrDecrLiftTest.lean
index b9d00c16cd..4b705d8c79 100644
--- a/StrataTest/Languages/Laurel/IncrDecrLiftTest.lean
+++ b/StrataTest/Languages/Laurel/IncrDecrLiftTest.lean
@@ -16,7 +16,7 @@ meta import StrataDDM.Elab
 meta import StrataDDM.BuiltinDialects.Init
 meta import Strata.Languages.Laurel.Grammar
 meta import Strata.Languages.Laurel.LaurelToCoreTranslator
-meta import Strata.Languages.Laurel.EliminateIncrDecr
+meta import Strata.Languages.Laurel.EliminateIncrDecrAndCompoundAssign
 meta import Strata.Languages.Laurel.LiftImperativeExpressions
 
 meta section
@@ -38,7 +38,7 @@ def parseLowerIncrDecr (input : String) : IO Program := do
   | .error e => throw (IO.userError s!"Translation errors: {e}")
   | .ok program =>
     -- Step 1: eliminate IncrDecr
-    let program := eliminateIncrDecr program
+    let program := eliminateIncrDecrAndCompoundAssign program
     -- Step 2: resolve so liftExpressionAssignments has a valid SemanticModel
     let result := resolve program
     let (program, model) := (result.program, result.model)