Remove global variables and modifies clauses from Core, replace returns with out/inout parameters (#759)

This changes
(1) the Core procedure declaration syntax from separate
input/output parameter lists (`procedure P(x: int) returns (y: int)`)
to a unified parameter list with `out`/`inout` modifiers
(`procedure P(x: int, out y: int)`),
(2) removes the `modifies` clause from procedure specification,
(3) removes global variables from Core, and
(4) changes the syntax of call `call lhs := f(args)` to `call f(x, out
lhs, inout ...)`.

**AST changes (summary: Procedure Header -> none, Decl -> global var
removal, Call -> has list of in/inout/out args)**

- `Procedure.Header.inputs` and `Procedure.Header.outputs` are still
there.
- CST->AST: partition unified bindings into inputs/outputs based on
  modifiers (`inout` appears in both inputs and outputs lists)
- AST->CST: detect `inout` by comparing input/output name overlap,
  emit `out`/`inout` prefixes instead of `returns` clause

Two new functions on `Procedure.Header` (in `Procedure.lean`)
classify parameters by their role:

- `Procedure.Header.getInoutParams`: returns parameters that appear
  in both `inputs` and `outputs` (the intersection). These are the
  parameters for which `old x` snapshots are meaningful.
- `Procedure.Header.getOutputOnlyParams`: returns output parameters
  that do NOT appear in `inputs`. These are output-only parameters
  that have no pre-state.
- Remove `ioDisjoint` from `WFProcedureProp` (inputs and outputs may
  now overlap for inout parameters).

**Removal of Decl.var (global variables)**

- Remove `Decl.var` from `Core.Decl` and `DeclKind.var` from
  `Core.DeclKind`. Global variables no longer exist in the Core AST.
- Remove `Program.getVar?`, `Program.getVarTy?`, `Program.getVarInit?`,
  `Decl.getVar?`, `Decl.getVar`, and related accessors.
- Remove `WFVarProp` from well-formedness definitions and drop the
  `.var` case from `WFDeclProp`.
- `ProcedureType.typeCheck`: old-variable bindings for postconditions
  are now added only for inout parameters (`getInoutParams`), not for
  all program-level globals.
- `StatementType.typeCheckCmd`: add `areInoutArgsValid` check ensuring
  that inout call arguments are simple variable references with the
  same name as the formal parameter.
- `CollectSymbols.lean`: remove `collectGlobalSymbols` (always empty).
- `ProcedureEval.lean`: old-substitution now only covers input
  parameters that also appear as outputs (inout), not program globals.
- `ProgramEval.lean`, `Core.lean`: remove `.var` evaluation case and
  statistics counting.

**Old-expression rules**

- `old(expr)` now applies only to inout parameters (those appearing in
  both inputs and outputs). For input-only parameters, `old x = x` so
  the `old` prefix is not emitted.

**Boole dialect updates (`Verify.lean`)**

The new syntax of Core (`procedure`/`call` with `out`/`inout` params) is
rejected,
to unchange the Core syntax. A new `procedure_signatures.lean` test
covers
accepted and rejected procedure declaration and call statement forms.
Global variables in Boole are translated into `inout` parameters of
procedures
(constant globals to plain parameters).

- Modified globals (`modifies g`) become inout parameters (in both
  `allInputs` and `allOutputs`) via `translateProcedureDecl`.
- Pre-pass collects global variable types into
  `TranslateState.globalVarTypes` and per-procedure modifies info into
  `TranslateState.modifiesMap` via `collectModifiesFromSpec`.
- Read-only globals (referenced but not in `modifies`) become
  input-only parameters so they remain in scope.
- `oldifyExpr` takes `currentInoutNames` and only applies `old` prefix
  to inout variables. For read-only globals, `old g` simplifies to `g`.

**Pass updates**

- `ProcBodyVerify.lean`: prefix is now
  `inputInits ++ outputOnlyInits ++ oldInoutInits ++ assumes`.
- `ProcBodyVerifyCorrect.lean`: full proof rewrite for the new prefix
  structure. Added helper lemmas about `getInoutParams` /
  `getOutputOnlyParams` (subset, disjointness, nodup). All proofs
  complete with zero sorries.
- `CallElim.lean`: old-variable type lookup no longer falls back to
  program-level globals.

**Other changes**

- Update all .core.st examples, expected outputs, and test files
- Add `CoreIdent.mkOld_injective` lemma (Identifiers.lean)
- Add `ioNotOld` to `WFProcedureProp` (no IO var is old-prefixed)
- Editor syntax highlights updated for `out`/`inout` keywords

---------

Co-authored-by: Juneyoung Lee <lebjuney@amazon.com>
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>
Co-authored-by: Shilpi Goel <shigoel@gmail.com>

Author: 4 people

DiffTestCore.lean

@@ -70,7 +70,7 @@ def StrataResult.toStr : StrataResult → String
 /-- Build a Core program that asserts str.in.re(testStr, regexExpr). -/
 def mkProgText (testStr : String) (regexStr : String) : String :=
   "program Core;\n" ++
-  "procedure main() returns () {\n" ++
+  "procedure main() {\n" ++
   s!"  assert [match_check]: (str.in.re(\"{escapeForCore testStr}\", {regexStr}));\n" ++
   "};"
 

Examples/DoubleTwice.core.st

@@ -1,18 +1,18 @@
 program Core;
 
-procedure Double(n : int) returns (result : int)
+procedure Double(n : int, out result : int)
 spec {
   ensures [double_correct]: (result == n * 2);
 }
 {
   result := n + n;
 };
 
-procedure TestProc(x : int) returns (output : int)
+procedure TestProc(x : int, out output : int)
 spec {
   ensures [testProc_result]: (output == x * 4);
 }
 {
-  call output := Double(x);
-  call output := Double(output);
+  call Double(x, out output);
+  call Double(output, out output);
 };

Examples/HeapReasoning.core.st

@@ -18,7 +18,6 @@ function isString(v: Box): bool;
 function isRef(v: Box): bool;
 
 // Replace by allocation time, one tick per 1) allocation 2) method call, const for each Ref = allocation time, prove disjointness by proving that the allocation is greater
-var tickingClock: int;
 function allocationTime(r: Ref): int;
 
 // TODO: What happens if allocating in an if-expression
@@ -68,7 +67,7 @@ axiom [nextFieldType]: forall s: Struct :: isContainerStruct(s) ==> (isRef(s[nex
 function Container_ctorModifiesFrame(h: Heap, testedRef: Ref, r: Ref, methodEntryTime: int): bool {
   testedRef == r || (allocationTime(testedRef) >= methodEntryTime)
 }
-procedure Container_ctor(heap: Heap, r: Ref, initialLychee: int, initialPineapple: int, initialNext: Ref) returns (newHeap: Heap)
+procedure Container_ctor(inout tickingClock: int, heap: Heap, r: Ref, initialLychee: int, initialPineapple: int, initialNext: Ref, out newHeap: Heap)
 spec {
   // Refs are allocated
   free requires tickingClock >= 0;
@@ -120,7 +119,7 @@ function UpdateContainersModifiesFrame(h: Heap, testedRef: Ref, ref1: Ref, metho
 }
 
 // Annotated with "modifies ref1"
-procedure UpdateContainers(heap: Heap, ref1: Ref, ref2: Ref) returns (newHeap: Heap)
+procedure UpdateContainers(inout tickingClock: int, heap: Heap, ref1: Ref, ref2: Ref, out newHeap: Heap)
 spec {
   // Refs are allocated
   free requires tickingClock >= 0;
@@ -190,10 +189,8 @@ function MainModifiesFrame(h: Heap, testedRef: Ref, methodEntryTime: int): bool
 }
 
 // annotated with "modifies {}"
-procedure Main(heap: Heap) returns (newHeap: Heap)
+procedure Main(inout tickingClock: int, heap: Heap, out newHeap: Heap)
 spec {
-  modifies tickingClock;
-
   free requires tickingClock >= 0;
   ensures tickingClock >= old tickingClock;
 
@@ -211,7 +208,7 @@ spec {
   assume allocationTime(c1) == tickingClock;
   assume isContainer(c1);
   tickingClock := tickingClock + 1;           // After allocation: increase the tick
-  call heap_var := Container_ctor(heap_var, c1, 0, 1, null);
+  call Container_ctor(inout tickingClock, heap_var, c1, 0, 1, null, out heap_var);
 
   assert [c1Lychees0]: isContainer(c1) && UnboxingInt(heap_var[c1][lycheeField]) == 0;
   assert [c1Pineapple1]: isContainer(c1) && UnboxingInt(heap_var[c1][pineappleField]) == 1;
@@ -221,7 +218,7 @@ spec {
   assume allocationTime(c2) == tickingClock;
   assume isContainer(c2);
   tickingClock := tickingClock + 1;           // After allocation: increase the tick
-  call heap_var := Container_ctor(heap_var, c2, 0, 0, null);
+  call Container_ctor(inout tickingClock, heap_var, c2, 0, 0, null, out heap_var);
 
   // c1.next := c2
   assert MainModifiesFrame(heap_var, c1, methodEntryTime);       // We can do that since the ticking clock has increased
@@ -233,7 +230,7 @@ spec {
   var rhs2: Box := BoxingRef(c1);
   heap_var := heap_var[c2 := heap_var[c2][nextField := rhs2]];
 
-  call heap_var := UpdateContainers(heap_var, c1, c2);
+  call UpdateContainers(inout tickingClock, heap_var, c1, c2, out heap_var);
 
   assert [c1Lychees1]: isContainer(c1) && UnboxingInt(heap_var[c1][lycheeField]) == 1;
   assert [c1Pineapple2]: isContainer(c1) && UnboxingInt(heap_var[c1][pineappleField]) == 2;

Examples/IrrelevantAxioms.core.st

@@ -15,7 +15,7 @@ axiom [g_idempotent]: forall x: int :: g(g(x)) == g(x);
 function h(x: int): int;
 axiom [h_def]: forall x: int :: h(x) == f(x) + 1;
 
-procedure TestF(x: int) returns (result: int)
+procedure TestF(x: int, out result: int)
 spec {
   ensures [result_positive]: result > 0;
 }

Examples/LoopSimple.core.st

@@ -1,6 +1,6 @@
 program Core;
 
-procedure loopSimple (n: int) returns (r: int)
+procedure loopSimple (n: int, out r: int)
 spec {
   requires (n >= 0);
 }

Examples/ProcedureTypeError.core.st

@@ -15,7 +15,7 @@ program Core;
 //  limitations under the License.
 //
 
-procedure SumPositive(a: int, b: int) returns (c: int)
+procedure SumPositive(a: int, b: int, out c: int)
 spec {
     requires [precond1]: 0 <= a;
     requires [precond2]: c <= b;

Examples/SafeBvOps.core.st

@@ -1,6 +1,6 @@
 program Core;
 
-procedure safe_bv_ops(x: bv32, y: bv32) returns (r: bv32)
+procedure safe_bv_ops(x: bv32, y: bv32, out r: bv32)
 {
     var a: bv32;
     var b: bv32;

Examples/SarifTest.core.st

@@ -1,7 +1,7 @@
 program Core;
 
 // Simple test program for SARIF output
-procedure AddPositive(x : int, y : int) returns (z : int)
+procedure AddPositive(x : int, y : int, out z : int)
 spec {
   requires [x_positive]: (x > 0);
   requires [y_positive]: (y > 0);

Examples/SimpleProc.core.st

@@ -15,13 +15,10 @@ program Core;
 //  limitations under the License.
 //
 
-var g : bool;
-
-procedure Test(x : bool) returns (y : bool)
+procedure Test(inout g : bool, x : bool, out y : bool)
 spec {
   ensures (y == x);
   ensures (x == y);
-  ensures (g == old g);
 }
 {
   y := x || x;

Examples/TwoLoops.core.st

@@ -3,7 +3,7 @@ program Core;
 const N : int;
 axiom [ax_N]: (0 <= N);
 
-procedure TwoLoops() returns ()
+procedure TwoLoops()
 {
   var i : int;
   var j : int;