document Iris migration architecture

Author: mfornet

AGENTS.md

@@ -10,6 +10,156 @@ The interpreter is deliberately optimized for **simplicity of reasoning, not exe
 
 Lean toolchain is pinned in `lean-toolchain`.
 
+## Iris migration (`iris` branch only)
+
+> **Temporary branch-scoped notice.** This section must exist only on the
+> `iris` integration branch and branches created from `iris` during the
+> migration. It overrides conflicting guidance elsewhere in this file,
+> especially guidance to preserve the current big-step interpreter's shape.
+> Before merging the completed migration into `main`, remove this notice or
+> update it to describe the new permanent architecture.
+
+The purpose of the `iris` branch is to integrate
+[iris-lean](https://github.com/leanprover-community/iris-lean) and migrate the
+reference Wasm interpreter from its current fuel-bounded big-step semantics to
+small-step semantics suitable for Iris.
+
+The migration is complete when:
+
+- The interpreter is fully expressed using small-step semantics in the form
+  expected by iris-lean.
+- Every currently supported Wasm feature and test remains covered, with no
+  semantic regressions.
+- Differential testing remains possible. In particular, there must still be an
+  executable, fuel-bounded way to run Wasm code, built by iterating the
+  executable small-step function rather than by maintaining a second semantics.
+- All required iris-lean language and proof-mode instances are implemented, so
+  downstream proofs can use iris-lean directly.
+- Existing proofs and theorem statements need not retain their exact shape.
+  Nevertheless, preserve the intent and coverage of existing examples whenever
+  possible, rewriting them against the new semantics rather than silently
+  deleting them.
+
+The intended split between an Iris expression and state is approximately:
+
+```lean
+inductive Expr
+  | running : ThreadState → Expr
+  | done : List WasmVal → Expr
+  | trapped : TrapReason → Expr
+  deriving BEq, Repr
+
+structure Store where
+  functions : Array Function
+  memories : Array Memory
+  globals : Array Global
+  tables : Array Table
+  deriving BEq, Repr
+```
+
+Treat this as an architectural guide, not a requirement to preserve these exact
+names. `Expr` contains the whole per-execution `ThreadState`, not merely the
+remaining instruction list. `Store` contains the shared runtime resources.
+Keep that ownership boundary explicit when adding fields: thread-local control
+and operand state belongs in `ThreadState`; resources observed or mutated
+through the runtime store belong in `Store`.
+
+For convenient executable interpretation, package the Iris expression and
+state together, while keeping the relational semantics authoritative:
+
+```lean
+/- Convenient packaging for the executable interpreter. The Iris adapter will
+   split this back into its `Expr` and `State` arguments. -/
+structure Config where
+  expr : Expr
+  store : Store
+  deriving BEq, Repr
+
+inductive Step : Config → Config → Prop where
+  -- Full definition of all valid transitions.
+
+def step? : Config → Option Config
+  | ⟨.running thread, store⟩ => stepRunning? thread store
+  | ⟨.done _, _⟩ => none
+  | ⟨.trapped _, _⟩ => none
+
+theorem step?_sound {config config' : Config} :
+    step? config = some config' → Step config config' := by
+  sorry
+
+theorem step?_complete {config config' : Config} :
+    Step config config' → step? config = some config' := by
+  sorry
+
+theorem step_sound {config config' : Config} :
+    step? config = some config' → Step config config' :=
+  step?_sound
+
+theorem step_complete {config config' : Config} :
+    Step config config' → step? config = some config' :=
+  step?_complete
+
+theorem step_iff {config config' : Config} :
+    step? config = some config' ↔ Step config config' :=
+  ⟨step_sound, step_complete⟩
+```
+
+The exact iris-lean adapter must follow the API of the pinned iris-lean
+dependency. Implement every required instance from this `Expr`/`Store` split
+and prove it against `Step`; do not introduce a parallel Iris-only transition
+relation.
+
+Use instruction-level granularity as the default: one `Step` should normally
+execute one Wasm instruction. Administrative transitions may execute no Wasm
+instruction when they expose or remove control frames, prepare or return from a
+function call, propagate a trap, or otherwise reorganize the machine so the
+next instruction can run. Prefer small, explicit administrative transitions
+over hiding multi-stage control behavior inside a single large step. A
+transition may perform the atomic state effects intrinsic to its instruction;
+do not split an instruction solely to mirror implementation helper functions.
+Document intentional exceptions and keep the granularity consistent across
+related instructions.
+
+For now, assume the Wasm semantics implemented here is deterministic, as
+required by `step? : Config → Option Config` and `step?_complete`. Whenever a
+feature appears nondeterministic—or depends on unspecified host behavior,
+scheduling, external input, or an arbitrary choice—flag it before implementing
+the transition. Record whether the behavior can be made deterministic by an
+explicit input or policy in `Store`. If genuine nondeterminism is required,
+stop and decide how to represent executable successor choices and adapt the
+Iris semantics and correspondence theorem; never choose an outcome silently.
+
+During the migration:
+
+- Pin iris-lean to a known revision. Upgrade it intentionally, recording any
+  adapter or instance changes required by the new API.
+- Treat the instruction and administrative-step policy above as the default
+  Iris atomicity boundary. Review deviations explicitly; do not change
+  granularity merely to make the executable runner more convenient.
+- Make the relational `Step` and executable `step?` correspond in every PR.
+  A new transition is incomplete until both sides and their soundness and
+  completeness proofs agree.
+- State and preserve invariants at transition boundaries, including stack
+  typing, index validity, store-extension/ownership properties, and the
+  distinction between normal completion and traps.
+- Keep `.done` and `.trapped` terminal. Out-of-fuel belongs to the executable
+  runner's result, not to `Expr` or the semantic relation.
+- Add regression or differential tests while porting each instruction family.
+  Where feasible, compare the new runner with the old interpreter until the old
+  implementation is removed.
+- Keep migration PRs reviewable and layered: introduce representation and
+  compatibility lemmas first, then port coherent instruction families and
+  their examples. Do not remove the old path before equivalent coverage exists.
+- Build every affected package in dependency order. A successful build remains
+  the test criterion throughout the transition.
+
+iris-lean does not currently provide total-execution reasoning for this
+integration. Iris proofs therefore establish behavior conditional on reaching
+completion; they do not establish termination. This loss of total-correctness
+claims is accepted during the migration. Keep termination-sensitive theorem
+intent documented so it can be restored if total reasoning becomes available,
+and do not describe a partial-correctness result as a termination proof.
+
 ## Repository layout
 
 Three Lake packages in a monorepo, forming a strict dependency chain: