sir: text format for Vars

[Eduardogbg]

this PR adds the SIR text format for Vars: lexer, parser, printer, an extractor from .sir to a Lean module, and a well-formedness checker with a soundness theorem.

• the parser covers every Vars statement and terminator (text malloc is Vars.Stmt.malloc, mallocany is mallocUninit). numeric literals in operand position become a fresh const; init is required, main optional; a function's first block is its entry, as in the rust parser.
• for the parser correctness we state and prove:
  • normalize is a normal form for alpha equivalence (alphaEquiv_iff_normalize_eq, alphaEquiv_equivalence).
  • parse ∘ print = normalize for well-formed programs (parse_print_normalize) and parse ∘ print = id on normal forms (parse_print, unconditional since parser output is always normal, parse_normal): print is a section of parse, the normal forms are a retract of the text.
• every WellFormed clause has a proof-free decider in Sir/Vars/Spec/Check.lean (checkIcallArity, checkIretArity, checkAcyclicCalls, checkEntryArity, checkValidJumpTargets, checkVariablesDefinedBeforeUse), failing with a Diagnostic; checkAcyclicCalls computes a rank on the call graph and checks it decreases along every call. checkWellFormed sequences them and wellFormed_of_check : checkWellFormed p = .ok () → p.WellFormed is the exported soundness theorem; the extractor runs the checker, the example programs get their WellFormed witnesses from it by rfl and an ill-formed one is rejected with its diagnostic (Sir/Examples/Text.lean).
• lake env lean --run SirExtract.lean input.sir Output.lean name writes the parsed program as Lean source. examples have their printed text pinned and reparsed (Sir/Examples/Text.lean).

[Philogy]

I'd make the parsing of mnemonics more modular here, every mnemonic is quite repetitive and will be annoying to review once we start adding all the ops