feat(laurel): add Java-style compound assignment (+= -= *= /= %= ^=)

Compound assignment is the general case of which `++`/`--` is the degenerate
`x op= 1` form. `x op= e` lowers to `x := x op e` and yields the new value,
usable as a statement (`x += 2;`) or in expression position (`int y := (x += 2)`).

* AST: new `StmtExpr.CompoundAssign (op : Operation) (target) (rhs)` ctor. The
  `op` is invariably one of Add/Sub/Mul/Div/Mod/StrConcat (enforced by the
  concrete-to-abstract translator); downstream sites treat any other as a bug.

* Grammar: `+= -= *= /= %= ^=` at prec(10), rightassoc. Mixed `:=`/`op=`
  chaining is unsupported paren-free, matching `:=`'s existing behavior (plain
  `x := y := z` also does not parse); `a += b += c` groups right.

* Lowering: `EliminateIncrDecr.lowerToAssign` is generalized to `lowerOpAssign`
  (arbitrary `Operation` + RHS), shared with the `++`/`--` path (rhs = 1). The
  `.PrimitiveOp` keeps `skipProof := false`, so `/=`/`%=` carry the same
  division-by-zero proof obligation as a hand-written `x := x / e`. Runs first in
  the pipeline, so no later pass observes `.CompoundAssign`.

* Type checking is construct-keyed, by design: `++`/`--` reject `real` (the
  synthesized int `1` cannot type-check against a real under strict numeric
  typing), but `+= -= *= /=` accept `real` because the RHS is user-written;
  `%=` is int-only (`.Mod` has no real lowering); `^=` is string-only. The
  shared `compoundAssignAccepts` predicate drives both the resolution-time
  target check and the model-based RHS-type check (`compoundAssignRhsErrors`,
  run in the post-resolution validation phase). The RHS check is suppressed
  when the target type is already invalid, so one mistake yields one error.

* All exhaustive `StmtExpr` matches updated (MapStmtExpr traverses the rhs even
  for Local/Declare targets, FilterPrelude, computeExprType, both grammar
  translators, the Core-translator defensive arm, the lift `contains*` helpers,
  resolution `collectStmtExpr` and the diamond-field walker).

Tests:
* T24_CompoundAssign: each operator on int; real for `+= -= *= /=`; string for
  `^=`; constrained-int (`nat`); expression position; nested side-effecting RHS;
  right-associative `a += b += c`.
* T24b_CompoundAssignField: field target `c#n += e` and chained `o#inner#count
  += e`, both statement and expression position.
* CompoundAssignTypeRejectionTest: per-operator target rejections; RHS-type
  mismatches; the intended `r += 1.0` accepts / `r++` rejects asymmetry; and a
  `/= 0` verification failure pinning `skipProof := false`.
* CompoundAssignLiftTest: golden lowering for statement, expression, and
  nested-RHS forms.

Author: fabiomadge

Strata/Languages/Laurel/EliminateIncrDecr.lean

@@ -46,25 +46,40 @@ namespace Strata.Laurel
 
 public section
 
-/-- Reconstruct the read-side `StmtExprMd` for a `Variable`. -/
+/-- Reconstruct the read-side `StmtExprMd` for a `Variable`.
+
+    For a `.Field` target this duplicates the object subtree `tgt` into the read
+    operand (the lowering emits `target op rhs`, so `target` appears on both sides).
+    That is sound because a field read lowers (in `HeapParameterization`) to a pure,
+    total, obligation-free `readField(heap, obj, field)` map lookup, and both copies
+    read the same `$heap` snapshot at the same program point — so they are provably
+    equal regardless of how complex `tgt` is (e.g. a chained `a#b#c`). The only cost
+    is VC/term-size duplication, not a correctness risk. (If field reads ever gain a
+    precondition — e.g. a null/allocated check — this duplication would need revisiting.) -/
 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`. The resulting
+    assignment expression yields the new value. Shared by the `IncrDecr` lowering
+    (with `rhs = 1`) and the `CompoundAssign` lowering (with the user's RHS). -/
+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). -/
@@ -86,6 +101,12 @@ private def lowerIncrDecr (mode : IncrDecrMode) (op : IncrDecrOp)
 private def rewriteNode (node : StmtExprMd) : StmtExprMd :=
   match node.val with
   | .IncrDecr mode op target => lowerIncrDecr mode op target node.source
+  | .CompoundAssign op target rhs =>
+    -- `x op= e  ⇝  (x := x op e)`, yielding the new value. No Pre/Post dance:
+    -- compound assignment is always new-valued. The `.PrimitiveOp` keeps the
+    -- default `skipProof := false`, so `/=`/`%=` carry the same division-by-zero
+    -- proof obligations as a hand-written `x := x / e`.
+    lowerOpAssign op target rhs node.source
   | _ => node
 
 /-- Apply the rewrite to a procedure (body, preconditions, decreases, invokeOn). -/

Strata/Languages/Laurel/FilterPrelude.lean

@@ -109,6 +109,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 =>

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -143,6 +143,22 @@ 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 one of Add/Sub/Mul/Div/Mod/StrConcat (enforced by the
+      -- concrete-to-abstract translator); any other Operation is a bug upstream.
+      let opName := match op with
+        | .Add => "addAssign" | .Sub => "subAssign" | .Mul => "mulAssign"
+        | .Div => "divAssign" | .Mod => "modAssign" | .StrConcat => "strConcatAssign"
+        -- Unreachable by the ctor invariant. Emit a sentinel that will NOT re-parse
+        -- (rather than silently masquerading as `+=`), so a future miswiring is caught
+        -- by the round-trip rather than corrupting output.
+        | _ => "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

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

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: fieldAccess now @[prec(95), leftassoc] (paren-free `c#n++` and chained `a#b#c`).
+-- Last grammar change: added compound assignment ops (`+=`, `-=`, `*=`, `/=`, `%=`, `^=`).
 public import StrataDDM.AST
 import StrataDDM.BuiltinDialects.Init
 import StrataDDM.Integration.Lean.HashCommands

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -53,6 +53,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;

Strata/Languages/Laurel/LaurelAST.lean

@@ -319,6 +319,14 @@ 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)
+  /-- Java-style compound assignment (`x += e`, `x -= e`, `x *= e`, `x /= e`,
+      `x %= e`, `x ^= e`). 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. -/
@@ -528,6 +536,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

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -257,6 +257,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"

Strata/Languages/Laurel/LaurelTypes.lean

@@ -88,6 +88,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

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