sir: one step relation for two addressing modes

[Eduardogbg]

SmallStep, Steps and EvalFn become definitions that instantiate a frame-polymorphic transition system in Spec/Machine.lean, and a stack-addressed CFG is the second instance.

What changed

• The parameters are OperandFrame (Environment, Source, Destination, fetch, store) and a Decoder supplying decode, control, resume and entry. SIR instantiates them at Locals with Array VarId on both operand sides; Generic/Cfg.lean instantiates them at a stack with slots, a pop depth, and a consume/produce destination. Generic/Examples.lean runs one program of each end to end.
• The dialogue trichotomy and GenericSteps.confluence_or_queryDivergence are proved once over the frame in Generic/Dialogue.lean and instantiated per decoder in Generic/Corollaries.lean; Proofs/Dialogue.lean and Proofs/StepDet.lean are deleted. Both decoders discharge Decoder.Exclusive and Decoder.Terminal with no premises.
• Operation stays a fixed inductive of SIR's eleven operations, so the abstraction covers addressing modes of one instruction set. A machine that needs further operations edits Spec/Machine.lean.
• The old mutual inductive is gone and no old ↔ new theorem was stated. Theorems.lean is byte-identical, and the TwoFunction, HaltedCall and Memory witnesses re-prove against the generic step with their statements unchanged.

[Eduardogbg]

superseded by #26