sir: certified lowering from Vars to Stack

[Eduardogbg]

this PR defines and verifies the lowering from Vars to Stack. this lowering requires an additional external witness (from plank's rust compiler), namely the stack schedule. it lifts the knowledge of a valid stack schedule into a proven lowering between the languages.

we check a stack schedule is correct by symbolically executing both a Vars and a Stack program against opaque variable names. as long as both executions match, meaning that they fire the same ops against their respective operands, the schedule checks.

• StackSchedule.check validates a whole function's schedule; StackSchedule.Block.check checks one block.
• the schedules we currently handle: reordering independent statements, renaming across block edges (arity-checked), exchange/flippedOp, leftover stack at a halting block, loops. we don't yet accept effectful ops such as icall
• a program certificate pairs an init schedule with an optional main; the lowering theorem is schedule.check = .ok () → Equiv schedule.vars schedule.stack (ProgramSchedule.equiv; StackSchedule.equiv is the one-function corollary)
• rejections are typed: a failing schedule reports its reason (useBeforeDefinition, boundaryArityMismatch, ...)
• a Scheduler is Accepted when every schedule it emits checks and schedules exactly its input (Scheduler.Accepted.equiv, Scheduler.Accepted.schedules_input)
• defined a spillAll scheduler, which loads every operand from its memory slot and stores every result back so nothing stays on the stack between statements, and proved the checker accepts everything it emits (spillAll_accepted)
• check Examples/Corpus.lean to see the equivalence discharged for real scheduler output (straight-line, diamond, loop) and for a two-function program with main
• Examples/Lowering.lean has accepted and rejected schedules, each rejection proving its specific error