Add observation-labelled pure-core small-step semantics

[Abraxas1010]

Summary

This introduces the first coherent observation-labelled small-step slice for the Iris migration and preserves the existing big-step interpreter as a refinement oracle.

• defines the Expr/ThreadState/MachineStore/Config split and authoritative labelled Step relation
• provides the deterministic executable step? with global soundness, completeness, determinism, terminality, runtime/store preservation, and well-formedness progress/preservation proofs
• covers 16 pure-core constructors: locals/constants, i32 add/sub/mul/divU, and the straight-line i64 expression image (add/sub/mul/le_s/eq/ne/eqz/extend_i32_u)
• adds trace concatenation, observation and administrative-erasure homomorphisms, additive iterator-fuel composition, exact post-terminal fuel monotonicity, and iterator-to-trace correspondence
• proves exact one-step and whole-program agreement with the existing interpreter for constructively well-formed pure-core programs
• adds the iris-lean language adapter, concrete success/trap/invalid/i64 canaries, and a generated 231-constructor migration coverage ledger checked by CI

Why

Talos's iris migration needs a relational semantics suitable for Iris while retaining an executable runner and a mechanically checked bridge to the current interpreter. This PR establishes that foundation on a deliberately bounded, coherent instruction family. It does not claim structured control flow, memory, or complete Wasm semantic preservation; those remain later migration layers.

Validation

• warning-free Lean builds: Interpreter (3,063 jobs), CodeLib (3,254), programs (3,285), verifier (42)
• runner smoke tests pass, including success, trap, Wasm decoding, and out-of-fuel cases
• complete official Wast suite exercised: 65,142 commands; regenerated testsuite_report.txt is byte-identical to the committed baseline; zero out-of-fuel regressions
• V8/miscast differential: 50/50 agreements, zero soundness or value findings
• generated coverage ledger fresh across all 231 Instruction constructors
• semantic-output and coverage-ledger mutation controls are rejected
• Rust workspace build and tests pass
• cargo clippy retains one unrelated pre-existing float_trunc x != x/clippy::eq_op failure; this PR does not modify that file

Trust scope

The principal new trace, fuel, and invariant theorems have measured axiom footprint [propext]; stepper soundness additionally uses the repository's existing quotient footprint. The old/new refinement theorems inherit [Classical.choice, Quot.sound] from the existing interpreter path. No sorry, admit, new axiom declaration, or compiler-only decision axiom is introduced.

Contributor and collaboration

This contribution was prepared by Richard Goodman — Apoth3osis (rgoodman@apoth3osis.io). Please reach out by email to discuss this work and opportunities for further collaboration on the Iris migration, WebAssembly semantics, and formal verification.

AI tooling assisted implementation and review. Richard Goodman remains accountable for the contribution and is available to discuss every part of the design and proof surface.

[mfornet]

Welcome, and thanks for your contribution.

Please, notice that the iris migration was already finished (still need to be tested in depth though). Please use the latest main. I'm going to close this PR.