strata-org · fabiomadge · Jun 16, 2026 · Jun 23, 2026 · Jun 23, 2026 · Jun 23, 2026
@@ -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,37 +35,55 @@ 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
   | .Local name => ⟨.Var (.Local name), source⟩
   | .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)
     (source : Option FileRange) : StmtExprMd :=
   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,21 +101,29 @@ 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). -/
 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
@@ -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 =>

@@ -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

@@ -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

@@ -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

@@ -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;

@@ -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

@@ -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,

@@ -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"

@@ -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

@@ -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

@@ -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⟩