strata-org · julesmt · May 21, 2026
@@ -455,37 +455,31 @@ where
 
 def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : TransformM Procedure := do
   let heapName : Identifier := "$heap"
-  let heapInName : Identifier := "$heap_in"
   let readsHeap := (← get).heapReaders.contains proc.name
   let writesHeap := (← get).heapWriters.contains proc.name
 
   if writesHeap then
-    -- This procedure writes the heap - add $heap_in as input and $heap as output
-    -- At the start, assign $heap_in to $heap, then use $heap throughout
-    let heapInParam : Parameter := { name := heapInName, type := ⟨.THeap, none⟩ }
-    let heapOutParam : Parameter := { name := heapName, type := ⟨.THeap, none⟩ }
+    -- This procedure writes the heap — $heap appears in both inputs and outputs
+    -- (true inout). Core's two-state semantics provide `old $heap` automatically.
+    let heapParam : Parameter := { name := heapName, type := ⟨.THeap, none⟩ }
 
-    let inputs' := heapInParam :: proc.inputs
-    let outputs' := heapOutParam :: proc.outputs
+    let inputs' := heapParam :: proc.inputs
+    let outputs' := heapParam :: proc.outputs
 
-    -- Preconditions use $heap_in (the input state)
-    let preconditions' ← proc.preconditions.mapM (·.mapM (heapTransformExpr heapInName model))
+    -- Preconditions reference $heap (evaluated at entry before any mutation)
+    let preconditions' ← proc.preconditions.mapM (·.mapM (heapTransformExpr heapName model))
 
     let bodyValueIsUsed := !proc.outputs.isEmpty
     let body' ← match proc.body with
       | .Transparent bodyExpr =>
-          -- First assign $heap_in to $heap, then transform body using $heap
-          let assignHeap := mkMd (.Assign [mkVarMd (.Local heapName)] (mkMd (.Var (.Local heapInName))))
           let bodyExpr' ← heapTransformExpr heapName model bodyExpr bodyValueIsUsed
-          pure (.Transparent (mkMd (.Block [assignHeap, bodyExpr'] none)))
+          pure (.Transparent bodyExpr')
       | .Opaque postconds impl modif =>
-          -- Postconditions use $heap (the output state)
           let postconds' ← postconds.mapM (·.mapM (heapTransformExpr heapName model))
           let impl' ← match impl with
             | some implExpr =>
-                let assignHeap := mkMd (.Assign [mkVarMd (.Local heapName)] (mkMd (.Var (.Local heapInName))))
                 let implExpr' ← heapTransformExpr heapName model implExpr bodyValueIsUsed
-                pure (some (mkMd (.Block [assignHeap, implExpr'] none)))
+                pure (some implExpr')
             | none => pure none
           let modif' ← modif.mapM (heapTransformExpr heapName model ·)
           pure (.Opaque postconds' impl' modif')

@@ -10,6 +10,7 @@ import Strata.Languages.Laurel.DesugarShortCircuit
 import Strata.Languages.Laurel.EliminateReturnsInExpression
 import Strata.Languages.Laurel.EliminateValueReturns
 import Strata.Languages.Laurel.ConstrainedTypeElim
+import Strata.Languages.Laurel.PushOldInward
 import Strata.Languages.Laurel.TypeAliasElim
 import Strata.Languages.Core.Verifier
 import Strata.Util.Profile
@@ -111,6 +112,10 @@ private def laurelPipeline : Array LaurelPass := #[
     run := fun p m =>
       let (p', diags) := modifiesClausesTransform m p
       (p', diags, {}) },
+  { name := "PushOldInward"
+    run := fun p _m =>
+      let (p', diags) := pushOldInward p
+      (p', diags, {}) },
   { name := "InferHoleTypes"
     run := fun p m =>
       let (p', diags, stats) := inferHoleTypes m p

@@ -300,7 +300,16 @@ def translateExpr (expr : StmtExprMd)
 
   | .AsType target _ => throwExprDiagnostic $ diagnosticFromSource expr.source "AsType expression translation" DiagnosticType.NotYetImplemented
   | .Assigned _ => throwExprDiagnostic $ diagnosticFromSource expr.source "assigned expression translation" DiagnosticType.NotYetImplemented
-  | .Old value => throwExprDiagnostic $ diagnosticFromSource expr.source "old expression translation" DiagnosticType.NotYetImplemented
+  | .Old value =>
+      -- After PushOldInward, every `Old` immediately wraps a Local Var of an inout parameter.
+      match value.val with
+      | .Var (.Local name) =>
+          let coreTy ← translateType (model.get name).getType
+          return .fvar () (Core.CoreIdent.mkOld name.text) (some coreTy)
+      | _ =>
+          throwExprDiagnostic $ diagnosticFromSource expr.source
+            "old(...) should have been pushed inward to a variable reference"
+            DiagnosticType.StrataBug
   | .Fresh _ => throwExprDiagnostic $ diagnosticFromSource expr.source "fresh expression translation" DiagnosticType.NotYetImplemented
   | .Assert _ => throwExprDiagnostic $ diagnosticFromSource expr.source "assert expression translation" DiagnosticType.NotYetImplemented
   | .Assume _ => throwExprDiagnostic $ diagnosticFromSource expr.source "assume expression translation" DiagnosticType.NotYetImplemented
@@ -351,6 +360,35 @@ def throwStmtDiagnostic (d : DiagnosticModel): TranslateM (List Core.Statement)
   modify fun s => { s with coreProgramHasSuperfluousErrors := true }
   return []
 
+/--
+Look up the callee's signature and convert positional `coreArgs` into Core
+`CallArg`s, emitting `.inoutArg ident` for parameters that appear in both
+inputs and outputs (true inout) and `.inArg` otherwise. Returns the call args
+along with the callee's outputs and inout names so the caller can build the
+matching `.outArg` list.
+-/
+private def buildCallArgs (calleeId : Identifier) (coreArgs : List Core.Expression.Expr)
+    : TranslateM (List (Core.CallArg Core.Expression) × List Parameter × List String) := do
+  let s ← get
+  let (calleeInputs, calleeOutputs) := match s.model.get calleeId with
+    | .staticProcedure proc => (proc.inputs, proc.outputs)
+    | .instanceProcedure _ proc => (proc.inputs, proc.outputs)
+    | _ => ([], [])
+  let calleeInputNames := calleeInputs.map (·.name.text)
+  let calleeOutputNames := calleeOutputs.map (·.name.text)
+  let calleeInoutNames := calleeInputNames.filter (calleeOutputNames.contains ·)
+  let inoutInputIndices := calleeInputNames.zipIdx.filterMap fun (name, i) =>
+    if calleeInoutNames.contains name then some i else none
+  let mut callArgs : List (Core.CallArg Core.Expression) := []
+  for (arg, i) in coreArgs.zipIdx do
+    if inoutInputIndices.contains i then
+      match arg with
+      | .fvar _ ident _ => callArgs := callArgs ++ [.inoutArg ident]
+      | _ => callArgs := callArgs ++ [.inArg arg]
+    else
+      callArgs := callArgs ++ [.inArg arg]
+  return (callArgs, calleeOutputs, calleeInoutNames)
+
 /--
 Translate Laurel StmtExpr to Core Statements using the `TranslateM` monad.
 Diagnostics are emitted into the monad state.
@@ -420,12 +458,14 @@ def translateStmt (stmt : StmtExprMd)
             lhs := lhs ++ [ident]
           | .Field _ _ => pure () -- already handled above
         return (inits, lhs)
-      -- Translate a procedure/instance call: init Declare targets with nondet, then emit call
-      let translateCallTargets (calleeName : String) (args : List StmtExprMd) : TranslateM (List Core.Statement) := do
+      -- Translate a procedure/instance call: init Declare targets with nondet, then emit call.
+      let translateCallTargets (calleeId : Identifier) (args : List StmtExprMd) : TranslateM (List Core.Statement) := do
         let coreArgs ← args.mapM (fun a => translateExpr a)
         let (inits, lhs) ← initTargetsNondet
-        let outArgs : List (Core.CallArg Core.Expression) := lhs.map .outArg
-        return inits ++ [Core.Statement.call calleeName (coreArgs.map .inArg ++ outArgs) md]
+        let (callArgs, _, calleeInoutNames) ← buildCallArgs calleeId coreArgs
+        let outArgs : List (Core.CallArg Core.Expression) :=
+          lhs.filter (fun id => !calleeInoutNames.contains id.name) |>.map .outArg
+        return inits ++ [Core.Statement.call calleeId.text (callArgs ++ outArgs) md]
       -- Match on the value to decide how to translate
       match _hv : value.val with
       | .StaticCall callee args =>
@@ -441,9 +481,9 @@ def translateStmt (stmt : StmtExprMd)
           | _ =>
             throwStmtDiagnostic $ md.toDiagnostic "function call without a single target" DiagnosticType.StrataBug
         else
-          translateCallTargets callee.text args
+          translateCallTargets callee args
       | .InstanceCall _target callee args =>
-          translateCallTargets callee.text args
+          translateCallTargets callee args
       | .Hole _ _ =>
           -- Hole RHS: havoc all targets (unmodeled call side-effect).
           dispatchTargets
@@ -472,22 +512,18 @@ def translateStmt (stmt : StmtExprMd)
         exprAsUnusedInit stmt md
       else
         let coreArgs ← args.mapM (fun a => translateExpr a)
-        -- Generate throwaway LHS variables for all outputs so Core arity
-        -- checking passes (lhs.length == outputs.length).
-        let outputs := match model.get callee with
-          | .staticProcedure proc => proc.outputs
-          | .instanceProcedure _ proc => proc.outputs
-          | _ => []
+        let (callArgs, calleeOutputs, calleeInoutNames) ← buildCallArgs callee coreArgs
+        -- Generate throwaway LHS for output-only params so Core arity checking passes.
         let mut inits : List Core.Statement := []
-        let mut lhs : List Core.CoreIdent := []
-        for out in outputs do
+        let mut outArgs : List (Core.CallArg Core.Expression) := []
+        for out in calleeOutputs do
+          if calleeInoutNames.contains out.name.text then continue
           let id ← freshId
           let ident : Core.CoreIdent := ⟨s!"$unused_{id}", ()⟩
           let coreType := LTy.forAll [] (← translateType out.type)
           inits := inits ++ [Core.Statement.init ident coreType .nondet md]
-          lhs := lhs ++ [ident]
-        let outArgs : List (Core.CallArg Core.Expression) := lhs.map .outArg
-        return inits ++ [Core.Statement.call callee.text (coreArgs.map .inArg ++ outArgs) md]
+          outArgs := outArgs ++ [.outArg ident]
+        return inits ++ [Core.Statement.call callee.text (callArgs ++ outArgs) md]
   | .InstanceCall .. =>
       -- Instance method call as statement: no return value, treated as no-op
       return ([])

@@ -18,7 +18,7 @@ and conjoining it with the postcondition. After this pass, the modifies list
 is cleared since its semantics have been absorbed into the postcondition.
 
 This pass should run after heap parameterization, which has already:
-- Added explicit heap parameters ($heap_in, $heap)
+- Added explicit heap parameter ($heap as inout)
 - Transformed field accesses to readField/updateField calls
 - Collected field constants
 
@@ -27,7 +27,7 @@ all field values are preserved between the input and output heaps.
 
 Generates:
   forall $obj: Composite, $fld: Field =>
-    $obj < $heap_in.nextReference && notModified($obj) ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld)
+    $obj < old($heap).nextReference && notModified($obj) ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
 
 where `notModified($obj)` is the conjunction of `$obj != e` for each single entry `e`,
 and `!(select(s, $obj))` for each set entry `s`.
@@ -94,31 +94,31 @@ Build the modifies frame condition as a Laurel StmtExpr.
 Generates a single quantified formula:
 
   forall $obj: Composite, $fld: Field =>
-    notModified($obj) && $obj < $heap_in.nextReference ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld)
+    notModified($obj) && $obj < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
 
 Returns `none` if there are no entries.
 -/
 def buildModifiesEnsures (proc: Procedure) (model: SemanticModel) (modifiesExprs : List StmtExprMd)
-    (heapInName heapOutName : Identifier) : Option StmtExprMd :=
+    (heapName : Identifier) : Option StmtExprMd :=
   let entries := extractModifiesEntries model modifiesExprs
   let objName : Identifier := "$modifies_obj"
   let fldName : Identifier := "$modifies_fld"
   let obj := mkMd <| .Var (.Local objName)
   let fld := mkMd <| .Var (.Local fldName)
-  let heapIn := mkMd <| .Var (.Local heapInName)
-  let heapOut := mkMd <| .Var (.Local heapOutName)
-      -- Build the "obj is allocated" condition: Composite..ref($obj) < $heap_in.nextReference
+  let heapIn := mkMd <| .Old (mkMd (.Var (.Local heapName)))
+  let heapOut := mkMd <| .Var (.Local heapName)
+      -- Build the "obj is allocated" condition: Composite..ref($obj) < old($heap).nextReference
   let heapCounter := mkMd <| .StaticCall "Heap..nextReference!" [heapIn]
   let objRef := mkMd <| .StaticCall "Composite..ref!" [obj]
   let objAllocated := mkMd <| .PrimitiveOp .Lt [objRef, heapCounter]
   let antecedent := if entries.isEmpty
     then objAllocated
     else
       -- Build the "not modified" precondition from all entries
-      -- Combine: $obj < $heap_in.nextReference && notModified($obj)
+      -- Combine: $obj < old($heap).nextReference && notModified($obj)
       let notModified := conjoinAll (entries.map (buildNotModifiedForEntry obj))
       mkMd <| .PrimitiveOp .And [objAllocated, notModified]
-  -- Build: readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld)
+  -- Build: readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
   let readIn := mkMd <| .StaticCall "readField" [heapIn, obj, fld]
   let readOut := mkMd <| .StaticCall "readField" [heapOut, obj, fld]
   let heapUnchanged := mkMd <| .PrimitiveOp .Eq [readIn, readOut]
@@ -145,7 +145,7 @@ may modify anything on the heap), and the modifies list is simply cleared.
 
 If the procedure has a `$heap` but no modifies clause, adds a postcondition
 that all allocated objects are preserved between heaps:
-  `forall $obj: Composite, $fld: Field => $obj < $heap_in.nextReference ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld)`
+  `forall $obj: Composite, $fld: Field => $obj < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)`
 
 If the modifies clause uses a wildcard (`*`), the frame condition is skipped
 entirely — the procedure may modify anything.
@@ -159,9 +159,8 @@ def transformModifiesClauses (model: SemanticModel)
         -- modifies * means the procedure can modify anything; no frame condition
         .ok { proc with body := .Opaque postconds impl [] }
       else if hasHeapOut proc then
-        let heapInName : Identifier := "$heap_in"
         let heapName : Identifier := "$heap"
-        let frameCondition := buildModifiesEnsures proc model modifiesExprs heapInName heapName
+        let frameCondition := buildModifiesEnsures proc model modifiesExprs heapName
         let postconds' := match frameCondition with
           | some frame => postconds ++ [{ condition := frame, summary := "modifies clause" }]
           | none => postconds