Integrate Iris small-step Wasm semantics

[mfornet]

What changed

• adds the authoritative relational Wasm small-step semantics and proved executable stepper
• cuts the runner and testsuite harness over to the small-step iterator
• integrates iris-lean Language, state interpretation, lifting, and adequacy
• ties physical memories, globals, tables, segments, and runtime metadata to authoritative ghost state
• migrates the core CodeLib array/u64 rules and symbolic memory fill/copy loops
• adds finite-trace and Iris memory examples, including swap, reverse, partition, merge, bulk memory, and generated swap_elements
• strengthens decoding, validation, structured traps, and testsuite diagnostics
• removes the obsolete custom separation-logic WP/adequacy layer

Why

The fuel-bounded big-step interpreter could execute Wasm but was not suitable as an iris-lean language. This establishes one authoritative small-step relation, a corresponding executable stepper, and an Iris proof stack over that same relation.

Validation

• git diff --check
• cd interpreter && lake build
• cd codelib && lake build
• cd programs/lean && lake build
• focused Lean LSP diagnostics and axiom audits for the new core and memory proofs
• Wasm testsuite report: 64,739 passed, 0 failed, 358 skipped, 0 interpreter errors, 0 out-of-fuel
• differential mutation corpus: 70/70 agreements

Review notes

This PR intentionally stops at the core migration. Further migration or rebuilding of legacy example theorem APIs is deferred. The old big-step path remains where required as a temporary comparison/compatibility oracle; the new runner, testsuite execution, Iris rules, and new proofs use the authoritative small-step path.

Generated root-level .wasm artifacts were intentionally excluded.

[github-actions]

Verifier report preview: https://talos-verifier-report-pr-161.vercel.app

(This URL is stable for this PR — it always points to the latest build of b9ab6bd.)