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

[MikaelMayer]

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

[MikaelMayer]

Implementation Notes

What this PR does

• Removes the modifies field from Procedure.Spec in the Core AST
• During DDM-to-Core translation, a pre-pass collects modifies info for all procedures, then:
  • Procedure declarations get modifies variables as extra in+out parameters
  • Call sites get modifies variables as extra args and LHS
• All downstream consumers updated: type checking, evaluation, call elimination, semantics, WF, backends

Assumptions made

1. The input/output disjointness check was relaxed because modifies-derived parameters legitimately appear in both inputs and outputs (the input is the pre-state value, the output is the post-state value)
2. The Laurel translator was already setting modifies to [] before this change, so Laurel programs should be unaffected
3. The Boole translator now ignores modifies clauses in the spec (they would need similar treatment to DDM if Boole programs use modifies)

Current state

• All source files compile successfully
• Test expected outputs need updating to reflect the new procedure signatures where modifies variables appear as parameters. This is an intentional behavioral change.
• The sorry-based proofs in CallElimCorrect.lean, ProcedureWF.lean, and StatementSemanticsProps.lean were updated to match the new signatures but remain as sorry

[MikaelMayer]

We discussed together and we decided we also want to REMOVE the modifies clauses from the concrete syntax as well as the global variables. This is a bigger change, but a welcome improvement that will reduce the scope of Core while retaining full generality.
Dialects like Bool and Laurel that depend on modifies clauses or global variables would just use the input/output parameter encoding.

[MikaelMayer]

🤖 Implemented the removal of modifies clauses and global variables from the Core DDM concrete syntax.

What changed:

• Removed modifies_spec and command_var from the Core DDM grammar
• Added them to the Boole grammar so Boole/Laurel dialects can still use them (they translate to input/output parameters when going to Core)
• Removed the collectModifiesInfo pre-pass and modifiesMap from the DDM→Core translator
• Updated ProcedureType, ProcedureEval, and CallElim to support old() for input/output parameters (not just globals)
• Rewrote all Core DDM tests to use explicit input/output parameters instead of globals and modifies clauses
• Updated Procedure.lean documentation

All existing tests pass.

[aqjune-aws]

Addressed comments, thank you all