Split Assign into local variable and field assignment

Strata/Languages/Laurel/ConstrainedTypeElim.lean

@@ -137,15 +137,14 @@ def elimStmt (ptMap : ConstrainedTypeMap)
       | some _ => (init, callOpt.toList.map fun c => ⟨.Assert c, source, md⟩)
     pure ([⟨.LocalVariable name ty init', source, md⟩] ++ check)
 
-  | .Assign [target] _ => match target.val with
-    | .Identifier name => do
-      match (← get).get? name.text with
-      | some ty =>
-        let assert := (constraintCallFor ptMap ty name md (src := source)).toList.map
-          fun c => ⟨.Assert c, source, md⟩
-        pure ([stmt] ++ assert)
-      | none => pure [stmt]
-    | _ => pure [stmt]
+  | .Assign [target] _ => do
+    let name := target.val
+    match (← get).get? name.text with
+    | some ty =>
+      let assert := (constraintCallFor ptMap ty name md (src := source)).toList.map
+        fun c => ⟨.Assert c, source, md⟩
+      pure ([stmt] ++ assert)
+    | none => pure [stmt]
 
   | .Block stmts sep =>
     let stmtss ← inScope (stmts.mapM (elimStmt ptMap))

Strata/Languages/Laurel/CoreGroupingAndOrdering.lean

@@ -62,9 +62,10 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
       | some eelse => collectStaticCallNames eelse
       | none => []
   | .Block stmts _ => stmts.flatMap (fun s => collectStaticCallNames s)
-  | .Assign targets v =>
-      targets.flatMap (fun t => collectStaticCallNames t) ++
+  | .Assign _targets v =>
       collectStaticCallNames v
+  | .FieldAssign t _ v =>
+      collectStaticCallNames t ++ collectStaticCallNames v
   | .LocalVariable _ _ initOption =>
       match initOption with
       | some init => collectStaticCallNames init

Strata/Languages/Laurel/EliminateValueReturns.lean

@@ -27,8 +27,7 @@ private def eliminateValueReturnNode (outParam : Identifier) (stmt : StmtExprMd)
   match stmt.val with
   | .Return (some value) =>
     -- Synthesized nodes use default metadata since no diagnostics should be reported on them
-    let target : StmtExprMd := ⟨.Identifier outParam, none, .empty⟩
-    let assign : StmtExprMd := ⟨.Assign [target] value, none, .empty⟩
+    let assign : StmtExprMd := ⟨.Assign [⟨outParam, none, .empty⟩] value, none, .empty⟩
     let ret : StmtExprMd := ⟨.Return none, stmt.source, stmt.md⟩
     ⟨.Block [assign, ret] none, none, .empty⟩
   | _ => stmt

Strata/Languages/Laurel/FilterPrelude.lean

@@ -99,8 +99,10 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
     collectExprNames cond; invs.forM collectExprNames
     dec.forM collectExprNames
     collectExprNames body
-  | .Assign targets value =>
-    collectExprNames value; targets.forM collectExprNames
+  | .Assign _targets value =>
+    collectExprNames value
+  | .FieldAssign target _ value =>
+    collectExprNames target; collectExprNames value
   | .FieldSelect target _ => collectExprNames target
   | .PureFieldUpdate target _ newVal =>
     collectExprNames target; collectExprNames newVal

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -100,11 +100,14 @@ where
       let initOpt := optionArg (init.map fun e => laurelOp "initializer" #[stmtExprToArg e])
       laurelOp "varDecl" #[ident name.text, typeOpt, initOpt]
     | .Assign targets value =>
-      -- Grammar only supports single-target assign; use first target or placeholder
-      let targetArg := match targets with
-        | t :: _ => stmtExprToArg t
-        | [] => laurelOp "identifier" #[ident "_"]
-      laurelOp "assign" #[targetArg, stmtExprToArg value]
+      match targets with
+      | [t] => laurelOp "assign" #[laurelOp "identifier" #[ident t.val.text], stmtExprToArg value]
+      | _ =>
+        let targetArgs := targets.map fun t => ident t.val.text
+        laurelOp "multiAssign" #[commaSep targetArgs.toArray, stmtExprToArg value]
+    | .FieldAssign target member value =>
+      let fieldAccess := laurelOp "fieldAccess" #[stmtExprToArg target, ident member.text]
+      laurelOp "assign" #[fieldAccess, stmtExprToArg value]
     | .FieldSelect target field =>
       laurelOp "fieldAccess" #[stmtExprToArg target, ident field.text]
     | .StaticCall callee args =>
@@ -161,7 +164,7 @@ where
     | .Abstract => laurelOp "identifier" #[ident "abstract"]
     | .All => laurelOp "identifier" #[ident "all"]
     | .PureFieldUpdate target field value =>
-      -- Not directly in grammar; emit as assignment to field
+      -- Not directly in grammar; emit as field assignment
       laurelOp "assign" #[
         laurelOp "fieldAccess" #[stmtExprToArg target, ident field.text],
         stmtExprToArg value

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -248,7 +248,20 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
     | q`Laurel.assign, #[arg0, arg1] =>
       let target ← translateStmtExpr arg0
       let value ← translateStmtExpr arg1
-      return mkStmtExprMd (.Assign [target] value) src
+      match target.val with
+      | .FieldSelect obj member => return mkStmtExprMd (.FieldAssign obj member value) src
+      | .Identifier name => return mkStmtExprMd (.Assign [⟨name, src, .empty⟩] value) src
+      | _ => TransM.error s!"assign target must be an identifier or field access"
+    | q`Laurel.multiAssign, #[arg0, arg1] =>
+      let targets ← match arg0 with
+        | .seq _ .comma args => args.toList.mapM fun a => do
+            let name ← translateIdent a
+            pure (⟨name, src, .empty⟩ : AstNode Identifier)
+        | _ => do
+            let name ← translateIdent arg0
+            pure [⟨name, src, .empty⟩]
+      let value ← translateStmtExpr arg1
+      return mkStmtExprMd (.Assign targets value) src
     | q`Laurel.new, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkStmtExprMd (.New name) src

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -9,7 +9,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: parameterized bvType with arbitrary width
+-- Last grammar change: assign now takes CommaSepBy Ident targets for multi-assign
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -47,6 +47,7 @@ op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
 
 // Assignment
 op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target " := " value;
+op multiAssign (targets: CommaSepBy Ident, value: StmtExpr): StmtExpr => @[prec(10)] "(" targets ") := " value;
 
 // Binary operators
 op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60), leftassoc] lhs " + " rhs;

Strata/Languages/Laurel/HeapParameterization.lean

@@ -66,15 +66,11 @@ def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do
   | .LocalVariable _ _ i => if let some x := i then collectExprMd x
   | .While c invs d b => collectExprMd c; collectExprMd b; for inv in invs do collectExprMd inv; if let some x := d then collectExprMd x
   | .Return v => if let some x := v then collectExprMd x
-  | .Assign assignTargets v =>
-      -- Check if any target is a field assignment (heap write)
-      for ⟨assignTarget, _⟩ in assignTargets.attach do
-        match assignTarget.val with
-        | .FieldSelect _ _ =>
-            modify fun s => { s with writesHeapDirectly := true }
-        | _ => pure ()
-        collectExprMd assignTarget
+  | .Assign _assignTargets v =>
       collectExprMd v
+  | .FieldAssign target _ v =>
+      modify fun s => { s with writesHeapDirectly := true }
+      collectExprMd target; collectExprMd v
   | .PureFieldUpdate t _ v => collectExprMd t; collectExprMd v
   | .PrimitiveOp _ args => for a in args do collectExprMd a
   | .New _ => modify fun s => { s with writesHeapDirectly := true }
@@ -279,11 +275,11 @@ where
             let freshVar ← freshVarName
             let varDecl := mkMd (.LocalVariable freshVar (computeExprType model exprMd) none)
             let callWithHeap := ⟨ .Assign
-              [mkMd (.Identifier heapVar), mkMd (.Identifier freshVar)]
+              [⟨heapVar, none, default⟩, ⟨freshVar, none, default⟩]
               (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩), source, md ⟩
             return ⟨ .Block [varDecl, callWithHeap, mkMd (.Identifier freshVar)] none, source, md ⟩
           else
-            return ⟨ .Assign [mkMd (.Identifier heapVar)] (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩), source, md ⟩
+            return ⟨ .Assign [⟨heapVar, none, default⟩] (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩), source, md ⟩
         else if calleeReadsHeap then
           return ⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩
         else
@@ -318,31 +314,22 @@ where
         let v' ← match v with | some x => some <$> recurse x | none => pure none
         return ⟨ .Return v', source, md ⟩
     | .Assign targets v =>
-        match targets with
-        | [⟨.FieldSelect target fieldName, _, _fieldSelectMd⟩] =>
-            let some qualifiedName := resolveQualifiedFieldName model fieldName
-              | return ⟨ .Hole, source, md ⟩
-            let valTy := (model.get fieldName).getType
-            let target' ← recurse target
-            let v' ← recurse v
-            -- Wrap value in Box constructor
-            recordBoxConstructor model valTy.val
-            let boxedVal := mkMd <| .StaticCall (boxConstructorName model valTy.val) [v']
-            let heapAssign := ⟨ .Assign [mkMd (.Identifier heapVar)]
-              (mkMd (.StaticCall "updateField" [mkMd (.Identifier heapVar), target', mkMd (.StaticCall qualifiedName []), boxedVal])), source, md ⟩
-            if valueUsed then
-              return ⟨ .Block [heapAssign, v'] none, source, md ⟩
-            else
-              return heapAssign
-        | [fieldSelectMd] =>
-          let tgt' ← recurse fieldSelectMd
-          return ⟨ .Assign [tgt'] (← recurse v), source, md ⟩
-        | [] =>
-            return ⟨ .Assign [] (← recurse v), source, md ⟩
-        | tgt :: rest =>
-            let tgt' ← recurse tgt
-            let targets' ← rest.mapM (recurse ·)
-            return ⟨ .Assign (tgt' :: targets') (← recurse v), source, md ⟩
+        return ⟨ .Assign targets (← recurse v), source, md ⟩
+    | .FieldAssign target fieldName v =>
+        let some qualifiedName := resolveQualifiedFieldName model fieldName
+          | return ⟨ .Hole, source, md ⟩
+        let valTy := (model.get fieldName).getType
+        let target' ← recurse target
+        let v' ← recurse v
+        -- Wrap value in Box constructor
+        recordBoxConstructor model valTy.val
+        let boxedVal := mkMd <| .StaticCall (boxConstructorName model valTy.val) [v']
+        let heapAssign := ⟨ .Assign [⟨heapVar, none, default⟩]
+          (mkMd (.StaticCall "updateField" [mkMd (.Identifier heapVar), target', mkMd (.StaticCall qualifiedName []), boxedVal])), source, md ⟩
+        if valueUsed then
+          return ⟨ .Block [heapAssign, v'] none, source, md ⟩
+        else
+          return heapAssign
     | .PureFieldUpdate t f v => return ⟨ .PureFieldUpdate (← recurse t) f (← recurse v), source, md ⟩
     | .PrimitiveOp op args =>
       let args' ← args.mapM (recurse ·)
@@ -411,15 +398,15 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
     let body' ← match proc.body with
       | .Transparent bodyExpr =>
           -- First assign $heap_in to $heap, then transform body using $heap
-          let assignHeap := mkMd (.Assign [mkMd (.Identifier heapName)] (mkMd (.Identifier heapInName)))
+          let assignHeap := mkMd (.Assign [⟨heapName, none, default⟩] (mkMd (.Identifier heapInName)))
           let bodyExpr' ← heapTransformExpr heapName model bodyExpr bodyValueIsUsed
           pure (.Transparent (mkMd (.Block [assignHeap, bodyExpr'] none)))
       | .Opaque postconds impl modif =>
           -- Postconditions use $heap (the output state)
           let postconds' ← postconds.mapM (heapTransformExpr heapName model ·)
           let impl' ← match impl with
             | some implExpr =>
-                let assignHeap := mkMd (.Assign [mkMd (.Identifier heapName)] (mkMd (.Identifier heapInName)))
+                let assignHeap := mkMd (.Assign [⟨heapName, none, default⟩] (mkMd (.Identifier heapInName)))
                 let implExpr' ← heapTransformExpr heapName model implExpr bodyValueIsUsed
                 pure (some (mkMd (.Block [assignHeap, implExpr'] none)))
             | none => pure none

Strata/Languages/Laurel/InferHoleTypes.lean

@@ -126,9 +126,12 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol
       return ⟨.Block (← inferBlockStmts stmts expectedType) label, source, md⟩
   | .Assign targets value =>
       let targetType := match targets with
-        | target :: _ => computeExprType model target
+        | target :: _ => (model.get target.val).getType
         | _ => defaultHoleType
       return ⟨.Assign targets (← inferExpr value targetType), source, md⟩
+  | .FieldAssign target member value =>
+      let targetType := (model.get member).getType
+      return ⟨.FieldAssign target member (← inferExpr value targetType), source, md⟩
   | .LocalVariable name ty init =>
       match init with
       | some initExpr => return ⟨.LocalVariable name ty (some (← inferExpr initExpr ty)), source, md⟩

Strata/Languages/Laurel/Laurel.lean

@@ -258,9 +258,11 @@ inductive StmtExpr : Type where
   | LiteralDecimal (value : Decimal)
   /-- A variable reference by name. -/
   | Identifier (name : Identifier)
-  /-- Assignment to one or more targets. Multiple targets are only allowed when the value is a `StaticCall` to a procedure with multiple outputs. -/
-  | Assign (targets : List (AstNode StmtExpr)) (value : AstNode StmtExpr)
-  /-- Read a field from a target expression. Combined with `Assign` for field writes. -/
+  /-- Assignment to one or more local variable targets. Multiple targets are only allowed when the value is a `StaticCall` to a procedure with multiple outputs. -/
+  | Assign (targets : List (AstNode Identifier)) (value : AstNode StmtExpr)
+  /-- Assignment to a field on a target expression. -/
+  | FieldAssign (target : AstNode StmtExpr) (member : Identifier) (value : AstNode StmtExpr)
+  /-- Read a field from a target expression. -/
   | FieldSelect (target : AstNode StmtExpr) (fieldName : Identifier)
   /-- Update a field on a pure (value) type, producing a new value. -/
   | PureFieldUpdate (target : AstNode StmtExpr) (fieldName : Identifier) (newValue : AstNode StmtExpr)

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -267,6 +267,8 @@ def translateExpr (expr : StmtExprMd)
       return .eq () re1 re2
   | .Assign _ _ =>
       disallowed md "destructive assignments are not supported in functions or contracts"
+  | .FieldAssign _ _ _ =>
+      disallowed md "field assignments are not supported in functions or contracts"
   | .While _ _ _ _ =>
       disallowed md "loops are not supported in functions or contracts"
   | .Exit _ => disallowed md "exit is not supported in expression position"
@@ -403,7 +405,7 @@ def translateStmt (stmt : StmtExprMd)
           return [Core.Statement.init ident coreType .nondet md]
   | .Assign targets value =>
       match targets with
-      | [⟨ .Identifier targetId, _, _ ⟩] =>
+      | [⟨ targetId, _, _ ⟩] =>
           let ident := ⟨targetId.text, ()⟩
           -- Check if RHS is a procedure call (not a function)
           match value.val with
@@ -442,21 +444,19 @@ def translateStmt (stmt : StmtExprMd)
           match value.val with
           | .StaticCall callee args =>
               let coreArgs ← args.mapM (fun a => translateExpr a)
-              let lhsIdents := targets.filterMap fun t =>
-                match t.val with
-                | .Identifier name => some (⟨name.text, ()⟩)
-                | _ => none
+              let lhsIdents := targets.map fun t => ⟨t.val.text, ()⟩
               return [Core.Statement.call lhsIdents callee.text coreArgs (astNodeToCoreMd value)]
           | .InstanceCall .. =>
               -- Instance method call: havoc all target variables
-              let havocStmts := targets.filterMap fun t =>
-                match t.val with
-                | .Identifier name => some (Core.Statement.havoc ⟨name.text, ()⟩ md)
-                | _ => none
-              return (havocStmts)
+              let havocStmts := targets.map fun t =>
+                Core.Statement.havoc ⟨t.val.text, ()⟩ md
+              return havocStmts
           | _ =>
               emitDiagnostic $ md.toDiagnostic "Assignments with multiple target but without a RHS call should not be constructed"
               returnNone
+  | .FieldAssign _ _ _ =>
+      emitDiagnostic $ md.toDiagnostic "FieldAssign should have been eliminated by heap parameterization" DiagnosticType.StrataBug
+      returnNone
   | .IfThenElse cond thenBranch elseBranch =>
       let bcond ← translateExpr cond
       let bthen ← translateStmt thenBranch

Strata/Languages/Laurel/LaurelTypes.lean

@@ -80,6 +80,7 @@ def computeExprType (model : SemanticModel) (expr : StmtExprMd) : HighTypeMd :=
   | .Exit _ => ⟨ .TVoid, source, md ⟩
   | .Return _ => ⟨ .TVoid, source, md ⟩
   | .Assign _ value => computeExprType model value
+  | .FieldAssign _ _ value => computeExprType model value
   | .Assert _ => ⟨ .TVoid, source, md ⟩
   | .Assume _ => ⟨ .TVoid, source, md ⟩
   -- Instance related