sir: parametric machine and the Vars and Stack languages

[Eduardogbg]

this PR splits SIR into two languages: Vars (a CFG over named locals with block arguments) and Stack (variables materialized on the stack and in memory slots; the last layer before bytecode). supersedes #20, #22, #23, #24.

• both are instances of one Machine, parametric over an OperandFrame (how an instruction fetches operands and stores results: locals vs the stack), a Decoder (how the program is read: next instruction, terminators, internal-call return, function entry) and a MemoryPolicy (which regions an allocation may take). the two languages differ precisely in their OperandFrame and Decoder; the memory model is shared.
• a Decoder carries proofs that an instruction and a terminator never sit at the same control point (exclusive) and that nothing decodes after returned/halted (terminal).
• allocation is nondeterministic (any valid region of the requested size); we define bumpAlloc and prove the policy allows it (memoryPolicy_allows_bumpAlloc), so a bump allocator is one legal implementation. also adds a zeroed malloc beside mallocUninit.
• mstore32 fails out-of-bounds; mload32 stays an oracle read.
• determinism and confluence are proved once at the Machine level, under NoMload (in-bounds mloads are deterministic, so this can be weakened) and [deterministic policy OR NoMalloc]; Vars and Stack export them 1:1 under MemOracleFree.
• Function := { entry : Block, rest : Array Block } always has an entry block, and Program := { init : Function, main : Option Function, rest : Array Function } always has an init function and optionally a separate main function.
• instead of a horizontal Sir/{Spec,Proofs,Theorems}/*.lean split, a vertical one: Sir/{Machine,Vars,Stack}/{Spec,Proofs,Theorems}.lean, with Spec/ and Proofs/ subdirectories where a module needs them.

[Eduardogbg]

Replaced by #29 and #30.