Merge PR #1076 and PR #1077

.gitignore

@@ -12,4 +12,4 @@ vcs/*.smt2
 *.py.ion
 *.py.ion.core.st
 
-Strata.code-workspace
+Strata.code-workspace

Strata/Languages/Laurel/ConstrainedTypeElim.lean

@@ -55,7 +55,7 @@ def constraintCallFor (ptMap : ConstrainedTypeMap) (ty : HighType)
     (varName : Identifier) (src : Option FileRange := none) : Option StmtExprMd :=
   match ty with
   | .UserDefined name => if ptMap.contains name.text then
-      some ⟨.StaticCall (mkId s!"{name.text}$constraint") [⟨.Identifier varName, src⟩], src⟩
+      some ⟨.StaticCall (mkId s!"{name.text}$constraint") [⟨.Var (.Local varName), src⟩], src⟩
     else none
   | _ => none
 
@@ -68,7 +68,7 @@ def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Proce
       if ptMap.contains parent.text then
         let paramId := { ct.valueName with uniqueId := none }
         let paramRef : StmtExprMd :=
-          { val := .Identifier paramId, source := none }
+          { val := .Var (.Local paramId), source := none }
         let parentCall : StmtExprMd :=
           { val := .StaticCall (mkId s!"{parent.text}$constraint") [paramRef], source := none }
         { val := .PrimitiveOp .And [ct.constraint, parentCall], source := none }
@@ -86,14 +86,21 @@ private def wrap (stmts : List StmtExprMd) (src : Option FileRange)
     : StmtExprMd :=
   match stmts with | [s] => s | ss => ⟨.Block ss none, src⟩
 
+def resolveVariable (ptMap : ConstrainedTypeMap) (v : VariableMd) : VariableMd :=
+  match v.val with
+  | .Declare param => ⟨.Declare { param with type := resolveType ptMap param.type }, v.source⟩
+  | _ => v
+
 /-- Resolve constrained types in type positions and inject constraint calls into quantifier bodies.
     Recursion into StmtExprMd children is handled by `mapStmtExpr`. -/
 def resolveExprNode (ptMap : ConstrainedTypeMap) (expr : StmtExprMd) : StmtExprMd :=
   let source := expr.source
 
   match expr.val with
-  | .LocalVariable n ty init =>
-    ⟨.LocalVariable n (resolveType ptMap ty) init, source⟩
+  | .Assign targets value =>
+    ⟨.Assign (targets.map (resolveVariable ptMap)) value, source⟩
+  | .Var (.Declare param) =>
+    ⟨.Var (.Declare { param with type := resolveType ptMap param.type }), source⟩
   | .Quantifier mode param trigger body =>
     let param' := { param with type := resolveType ptMap param.type }
     -- With bottom-up traversal, `body` is already recursed into. The newly
@@ -122,25 +129,31 @@ def elimStmt (ptMap : ConstrainedTypeMap)
   let source := stmt.source
 
   match _h : stmt.val with
-  | .LocalVariable name ty init =>
-    let callOpt := constraintCallFor ptMap ty.val name (src := source)
-    if callOpt.isSome then modify fun pv => pv.insert name.text ty.val
-    let (init', check) : Option StmtExprMd × List StmtExprMd := match init with
-      | none => match callOpt with
-        | some c => (none, [⟨.Assume c, source⟩])
-        | none => (none, [])
-      | some _ => (init, callOpt.toList.map fun c => ⟨.Assert { condition := c }, source⟩)
-    pure ([⟨.LocalVariable name ty init', source⟩] ++ check)
-
-  | .Assign [target] _ => match target.val with
-    | .Identifier name => do
-      match (← get).get? name.text with
-      | some ty =>
-        let assert := (constraintCallFor ptMap ty name (src := source)).toList.map
-          fun c => ⟨.Assert { condition := c }, source⟩
-        pure ([stmt] ++ assert)
-      | none => pure [stmt]
-    | _ => pure [stmt]
+  | .Var (.Declare param) =>
+    let callOpt := constraintCallFor ptMap param.type.val param.name (src := source)
+    if callOpt.isSome then modify fun pv => pv.insert param.name.text param.type.val
+    let check := match callOpt with
+      | some c => [⟨.Assume c, source⟩]
+      | none => []
+    pure ([stmt] ++ check)
+
+  | .Assign targets _value =>
+    -- Handle Declare targets for constrained type elimination
+    let declareChecks ← targets.foldlM (init := ([] : List StmtExprMd)) fun acc target =>
+      match target.val with
+      | .Declare param => do
+        let callOpt := constraintCallFor ptMap param.type.val param.name (src := source)
+        if callOpt.isSome then modify fun pv => pv.insert param.name.text param.type.val
+        pure (acc ++ callOpt.toList.map fun c => ⟨.Assert { condition := c }, source⟩)
+      | .Local name => do
+        match (← get).get? name.text with
+        | some ty =>
+          let assert := (constraintCallFor ptMap ty name (src := source)).toList.map
+            fun c => ⟨.Assert { condition := c }, source⟩
+          pure (acc ++ assert)
+        | none => pure acc
+      | _ => pure acc
+    pure ([stmt] ++ declareChecks)
 
   | .Block stmts sep =>
     let stmtss ← inScope (stmts.mapM (elimStmt ptMap))
@@ -205,7 +218,7 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
 
   let witnessId : Identifier := mkId "$witness"
   let witnessInit : StmtExprMd :=
-    ⟨.LocalVariable witnessId (resolveType ptMap ct.base) (some ct.witness), src⟩
+    ⟨.Assign [⟨.Declare ⟨witnessId, resolveType ptMap ct.base⟩, src⟩] ct.witness, src⟩
   let assert : StmtExprMd :=
     ⟨.Assert { condition := (constraintCallFor ptMap (.UserDefined ct.name) witnessId (src := src)).get! }, src⟩
   { name := mkId s!"$witness_{ct.name.text}"

Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean

@@ -25,6 +25,7 @@ def coreDefinitionsForLaurelDDM :=
 #strata
 program Laurel;
 
+datatype LaurelResolutionErrorPlaceholder {}
 datatype Float64IsNotSupportedYet {}
 
 // The types for these Map functions are incorrect.

Strata/Languages/Laurel/CoreGroupingAndOrdering.lean

@@ -62,13 +62,11 @@ 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 =>
+      -- Targets are Variables; Field targets can contain StmtExpr children,
+      -- but field-target assigns are eliminated before this pass runs,
+      -- so we only need to collect from the value.
       collectStaticCallNames v
-  | .LocalVariable _ _ initOption =>
-      match initOption with
-      | some init => collectStaticCallNames init
-      | none => []
   | .Return v =>
       match v with
       | some x => collectStaticCallNames x
@@ -85,7 +83,7 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
       | some t => collectStaticCallNames t
       | none => []) ++
       collectStaticCallNames body
-  | .FieldSelect t _ => collectStaticCallNames t
+  | .Var (.Field t _) => collectStaticCallNames t
   | .PureFieldUpdate t _ v => collectStaticCallNames t ++ collectStaticCallNames v
   | .InstanceCall t _ args =>
       collectStaticCallNames t ++ args.flatMap (fun a => collectStaticCallNames a)
@@ -98,7 +96,11 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
   | .Assigned v => collectStaticCallNames v
   | _ => []
 termination_by sizeOf expr
-decreasing_by all_goals (have := AstNode.sizeOf_val_lt ‹_›; term_by_mem)
+decreasing_by
+  all_goals simp_wf
+  all_goals (try have := AstNode.sizeOf_val_lt expr)
+  all_goals (try term_by_mem)
+  all_goals omega
 
 /--
 Build the procedure call graph, run Tarjan's SCC algorithm, and return each SCC

Strata/Languages/Laurel/EliminateHoles.lean

@@ -52,7 +52,7 @@ private def mkHoleCall (holeType : HighTypeMd) : ElimHoleM StmtExprMd := do
     body := .Opaque [] none []
   }
   modify fun s => { s with generatedFunctions := s.generatedFunctions ++ [holeProc] }
-  return bare (.StaticCall holeName (inputs.map (fun p => bare (.Identifier p.name))))
+  return bare (.StaticCall holeName (inputs.map (fun p => bare (.Var (.Local p.name)))))
 
 /-- Replace a deterministic `.Hole` with a call to a fresh uninterpreted function.
     Non-hole nodes pass through unchanged; recursion is handled by `mapStmtExprM`. -/

Strata/Languages/Laurel/EliminateValueReturns.lean

@@ -27,7 +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 := { val := .Identifier outParam, source := none }
+    let target : VariableMd := { val := .Local outParam, source := none }
     let assign : StmtExprMd := { val := .Assign [target] value, source := none }
     let ret : StmtExprMd := { val := .Return none, source := stmt.source }
     { val := .Block [assign, ret] none, source := none }

Strata/Languages/Laurel/FilterPrelude.lean

@@ -78,7 +78,7 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do
   | .Pure base => collectHighTypeNames base
   | .Intersection types => types.forM collectHighTypeNames
   | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString | .THeap
-  | .TBv _ | .Unknown => pure ()
+  | .TBv _ | .Unknown | .MultiValuedExpr _ => pure ()
 
 /-- Collect all referenced names (procedure calls, type references) from a StmtExpr tree. -/
 private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
@@ -92,16 +92,19 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
     collectExprNames cond; collectExprNames thenB
     elseB.forM collectExprNames
   | .Block stmts _ => stmts.forM collectExprNames
-  | .LocalVariable _ ty init =>
-    collectHighTypeNames ty
-    init.forM collectExprNames
   | .While cond invs dec body =>
     collectExprNames cond; invs.forM collectExprNames
     dec.forM collectExprNames
     collectExprNames body
   | .Assign targets value =>
-    collectExprNames value; targets.forM collectExprNames
-  | .FieldSelect target _ => collectExprNames target
+    collectExprNames value
+    for ⟨t, _⟩ in targets.attach do
+      match t.val with
+      | .Field target _ => collectExprNames target
+      | .Local _ => pure ()
+      | .Declare param => collectHighTypeNames param.type
+  | .Var (.Field target _) => collectExprNames target
+  | .Var (.Declare param) => collectHighTypeNames param.type
   | .PureFieldUpdate target _ newVal =>
     collectExprNames target; collectExprNames newVal
   | .PrimitiveOp _ args => args.forM collectExprNames
@@ -120,7 +123,7 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
   | .ReferenceEquals lhs rhs => collectExprNames lhs; collectExprNames rhs
   | .Hole _ ty => ty.forM collectHighTypeNames
   | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _
-  | .Identifier _ | .This | .Abstract | .All => pure ()
+  | .Var (.Local _) | .This | .Abstract | .All => pure ()
 
 /-- Collect names from a procedure body. -/
 private def collectBodyNames (body : Body) : CollectM Unit := do
@@ -177,7 +180,7 @@ private partial def collectInvokeOnTargets (expr : StmtExprMd)
   | .StaticCall callee args =>
     let rest ← args.flatMapM collectInvokeOnTargets
     return callee.text :: rest
-  | .Identifier _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _
+  | .Var (.Local _) | .LiteralInt _ | .LiteralBool _ | .LiteralString _
   | .LiteralDecimal _ => return []
   | _ =>
     throw s!"FilterPrelude.collectInvokeOnTargets: unexpected node in invokeOn expression"

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -62,6 +62,7 @@ partial def highTypeValToArg : HighType → Arg
     | [] => laurelOp "compositeType" #[ident "Unknown"]
     | t :: _ => highTypeToArg t
   | .Unknown => laurelOp "compositeType" #[ident "Unknown"]
+  | .MultiValuedExpr _ => laurelOp "compositeType" #[ident "Unknown"]
 
 end
 
@@ -80,6 +81,10 @@ private def operationName : Operation → String
 partial def stmtExprToArg (s : StmtExprMd) : Arg :=
   stmtExprValToArg s.val
 where
+  variableToArg : Variable → Arg
+    | .Local name => laurelOp "identifier" #[ident name.text]
+    | .Field target field => laurelOp "fieldAccess" #[stmtExprToArg target, ident field.text]
+    | .Declare param => laurelOp "identifier" #[ident param.name.text]
   stmtExprValToArg : StmtExpr → Arg
     | .LiteralBool b => laurelOp "literalBool" #[boolToArg b]
     | .LiteralInt n =>
@@ -90,23 +95,37 @@ where
     | .LiteralString s => laurelOp "string" #[.strlit sr s]
     | .Hole true _ => laurelOp "hole"
     | .Hole false _ => laurelOp "nondetHole"
-    | .Identifier name => laurelOp "identifier" #[ident name.text]
+    | .Var (.Local name) => laurelOp "identifier" #[ident name.text]
     | .Block stmts label =>
       let stmtArgs := stmts.map stmtExprToArg |>.toArray
       match label with
       | none => laurelOp "block" #[semicolonSep stmtArgs]
       | some l => laurelOp "labelledBlock" #[semicolonSep stmtArgs, ident l]
-    | .LocalVariable name ty init =>
-      let typeOpt := optionArg (some (laurelOp "typeAnnotation" #[highTypeToArg ty]))
-      let initOpt := optionArg (init.map fun e => laurelOp "initializer" #[stmtExprToArg e])
-      laurelOp "varDecl" #[ident name.text, typeOpt, initOpt]
+    | .Var (.Declare param) =>
+      let typeOpt := optionArg (some (laurelOp "typeAnnotation" #[highTypeToArg param.type]))
+      let initOpt := optionArg none
+      laurelOp "varDecl" #[ident param.name.text, typeOpt, initOpt]
+    | .Assign [⟨.Declare param, _⟩] value =>
+      let typeOpt := optionArg (some (laurelOp "typeAnnotation" #[highTypeToArg param.type]))
+      let initOpt := optionArg (some (laurelOp "initializer" #[stmtExprToArg value]))
+      laurelOp "varDecl" #[ident param.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]
-    | .FieldSelect target field =>
+      if targets.length > 1 then
+        let targetArgs := targets.map fun t =>
+          match t.val with
+          | .Declare param => laurelOp "assignTargetDecl" #[ident param.name.text, highTypeToArg param.type]
+          | .Local name => laurelOp "assignTargetVar" #[ident name.text]
+          | .Field target _ =>
+            match target.val with
+            | .Var (.Local name) => laurelOp "assignTargetField" #[ident name.text, ident (match t.val with | .Field _ f => f.text | _ => "_")]
+            | _ => laurelOp "assignTargetVar" #[ident "_"]
+        laurelOp "multiAssign" #[commaSep targetArgs.toArray, stmtExprToArg value]
+      else
+        let targetArg := match targets with
+          | t :: _ => variableToArg t.val
+          | [] => laurelOp "identifier" #[ident "_"]
+        laurelOp "assign" #[targetArg, stmtExprToArg value]
+    | .Var (.Field target field) =>
       laurelOp "fieldAccess" #[stmtExprToArg target, ident field.text]
     | .StaticCall callee args =>
       let calleeArg := laurelOp "identifier" #[ident callee.text]
@@ -358,6 +377,12 @@ def formatTypeDefinition : TypeDefinition → Format
   | .Datatype ty => formatDatatypeDefinition ty
   | .Alias ta => "type " ++ format ta.name ++ " = " ++ formatHighType ta.target
 
+def formatVariable (v : Variable) : Format :=
+  formatArg (stmtExprToArg ⟨.Var v, none⟩)
+
+def formatVariableMd (v : VariableMd) : Format :=
+  formatArg (stmtExprToArg ⟨.Var v.val, v.source⟩)
+
 def formatConstant (c : Constant) : Format :=
   "const " ++ format c.name ++ ": " ++ formatHighType c.type ++
   match c.initializer with
@@ -375,6 +400,8 @@ instance : Std.ToFormat CompositeType where format := formatCompositeType
 instance : Std.ToFormat ConstrainedType where format := formatConstrainedType
 instance : Std.ToFormat DatatypeConstructor where format := formatDatatypeConstructor
 instance : Std.ToFormat DatatypeDefinition where format := formatDatatypeDefinition
+instance : Std.ToFormat Variable where format := formatVariable
+instance : Std.ToFormat VariableMd where format := formatVariableMd
 instance : Std.ToFormat Constant where format := formatConstant
 instance : Std.ToFormat TypeDefinition where format := formatTypeDefinition
 instance : Std.ToFormat Program where format := formatProgram

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -82,7 +82,7 @@ def translateBool (arg : Arg) : TransM Bool := do
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
 instance : Inhabited Parameter where
-  default := { name := "" , type := { val := .Unknown, source := none } }
+  default := { name := "" , type := default }
 
 def mkHighTypeMd (t : HighType) (source : Option FileRange) : HighTypeMd := { val := t, source := source }
 def mkStmtExprMd (e : StmtExpr) (source : Option FileRange) : StmtExprMd := { val := e, source := source }
@@ -240,15 +240,42 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
           | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
         | .option _ none => pure none
         | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
-      return mkStmtExprMd (.LocalVariable name varType value) src
+      match value with
+      | some init => return mkStmtExprMd (.Assign [⟨.Declare ⟨name, varType⟩, src⟩] init) src
+      | none => return mkStmtExprMd (.Var (.Declare ⟨name, varType⟩)) src
     | q`Laurel.identifier, #[arg0] =>
       let name ← translateIdent arg0
-      return mkStmtExprMd (.Identifier name) src
+      return mkStmtExprMd (.Var (.Local name)) src
     | q`Laurel.parenthesis, #[arg0] => translateStmtExpr arg0
     | q`Laurel.assign, #[arg0, arg1] =>
       let target ← translateStmtExpr arg0
+      let targetVar : VariableMd ← match target.val with
+        | .Var v => pure ⟨v, target.source⟩
+        | _ => TransM.error s!"assign target must be a variable or field access"
       let value ← translateStmtExpr arg1
-      return mkStmtExprMd (.Assign [target] value) src
+      return mkStmtExprMd (.Assign [targetVar] value) src
+    | q`Laurel.multiAssign, #[targetsSeq, valueArg] =>
+      let targets ← match targetsSeq with
+        | .seq _ .comma args => args.toList.mapM fun targ => do
+          let tSrc ← getArgFileRange targ
+          let .op top := targ
+            | TransM.error s!"multiAssign target expects operation"
+          match top.name, top.args with
+          | q`Laurel.assignTargetDecl, #[nameArg, typeArg] =>
+            let name ← translateIdent nameArg
+            let ty ← translateHighType typeArg
+            pure (⟨.Declare ⟨name, ty⟩, tSrc⟩ : VariableMd)
+          | q`Laurel.assignTargetVar, #[nameArg] =>
+            let name ← translateIdent nameArg
+            pure (⟨.Local name, tSrc⟩ : VariableMd)
+          | q`Laurel.assignTargetField, #[objArg, fieldArg] =>
+            let obj ← translateIdent objArg
+            let field ← translateIdent fieldArg
+            pure (⟨.Field ⟨.Var (.Local obj), tSrc⟩ field, tSrc⟩ : VariableMd)
+          | _, _ => TransM.error s!"multiAssign: unexpected target {repr top.name}"
+        | _ => pure []
+      let value ← translateStmtExpr valueArg
+      return mkStmtExprMd (.Assign targets value) src
     | q`Laurel.new, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkStmtExprMd (.New name) src
@@ -263,7 +290,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
     | q`Laurel.call, #[arg0, argsSeq] =>
       let callee ← translateStmtExpr arg0
       let calleeName := match callee.val with
-        | .Identifier name => name
+        | .Var (.Local name) => name
         | _ => ""
       let argsList ← match argsSeq with
         | .seq _ .comma args => args.toList.mapM translateStmtExpr
@@ -285,7 +312,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let obj ← translateStmtExpr objArg
       let field ← translateIdent fieldArg
       let fieldSrc ← getArgFileRange fieldArg
-      return mkStmtExprMd (.FieldSelect obj field) fieldSrc
+      return mkStmtExprMd (.Var (.Field obj field)) fieldSrc
     | q`Laurel.while, #[condArg, invSeqArg, bodyArg] =>
       let cond ← translateStmtExpr condArg
       let invariants ← match invSeqArg with