iris-lean to prove SwapElementsSpec

[Isabelle9999]

Overview

This PR integrates [iris-lean] into Talos and uses it to prove SwapElementsSpec end-to-end — zero sorry, zero fallback to the existing wp/wp_run system. The proof demonstrates per-instruction stepping rules in the iProp world, compositional function specs at the Prop level, and a clean iProp-to-Prop extraction path that every other program proof can reuse.

The goal is to establish the infrastructure and pattern for separation-logic-based verification, with module linking and shared memory reasoning as the targets.

Honest scope note: the ghost heap threaded through the iProp WP is not yet tied to the physical st.mem (see the status note in WasmRules.lean). Memory disjointness in the swap proof comes from pure Mem.*_disjoint framing hypotheses, not from ∗. The pointsTo/arrayAt ownership layer (WasmHeap.lean) is built and proven, ready for the state interpretation that will connect the two; until that lands, ∗-based disjointness is infrastructure, not the working mechanism.

How it works

The proof flows through five parts. Parts 1 – 4 (ghost state model, WP fixpoint, per-instruction rules, composition rules) are build-once infrastructure, written once in codelib/CodeLib/SepLogic/ and can be reused by every program proof without modification. Part 5 (the proof in SwapSepLogic.lean) is swap-specific. A new program adds its own part 5; the rest is inherited.

1 — Ghost state model (WasmHeap.lean)

Wasm's byte-addressable linear memory is modeled as an iris-lean GenHeap: each
address addr : UInt32 owns a ghost cell addr ↦w byte (scoped notation). Multi-byte ownership
is built on top:

• pointsTo_u64 addr v — owns 8 consecutive bytes at addr containing v
  (little-endian). Matches swap's 64-bit array elements.
• pointsTo_u32 addr v — owns 4 consecutive bytes (for future u32 arrays).
• arrayAt ptr xs — owns |xs| consecutive u32 elements. Comes with arrayAt_append
  (split arrays at a midpoint), arrayAt_set (update one element), and arrayAt_get
  (extract one element — derived from arrayAt_set at the just-read value). These are
  the standard array-ownership triad from HeapLang's array library, adapted for Wasm's
  flat memory.

Soundness bridge (WasmRules.lean): load_sound and store_sound connect ghost
ownership to physical memory through the interpreter's Mem.read8/Mem.write8:
if heapAgreesWithMem σ mem, ghost-heap reads agree with mem.read8, and
ghost-heap writes produce a Mem.write8 image that agrees with the updated ghost
heap. Not yet consumed by the WP — staged for the future state interpretation.

2 — Weakest precondition (Adequacy.lean, first half)

wp_wasm is defined as a bi_least_fixpoint over wp_wasm_F, the WP functional.
For an instruction sequence instr :: rest, the functional says: for any ghost heap
state σ, executing instr produces a new state σ' and continuation, and the WP holds
for rest under σ'. This is the standard Iris WP pattern, instantiated for Wasm's
big-step execOne.

wasm_adequacy extracts a pure proposition from the iProp world: genHeapInterp σ ∗ wp_wasm ... ⊢ |==> ⌜wp_wasm_prop ...⌝

wasm_heap_adequacy wraps the full lifecycle: creates ghost state via
genHeap_init_names, runs the user's iProp proof, applies wasm_adequacy,
and extracts the pure result via pure_soundness. This is the single entry
point: any program proof calls wasm_heap_adequacy with an iProp proof and
gets back a wp_wasm_prop at the Prop level. Analogous to HeapLang's
heap_adequacy.

3 — Per-instruction iProp rules (Adequacy.lean, second half)

Each Wasm instruction gets a stepping rule that wraps wp_wasm_step (which
unfolds the fixpoint one step via least_fixpoint_unfold). For pure instructions
(const, add, localGet, etc.), the ghost heap passes through unchanged — the
ghost_id combinator discharges that obligation in one token per step. A
wp_wasm_ret terminal rule closes the chain.

Currently implemented: globalGet/globalSet, localGet/localSet, const,
add, sub, load32/load64, store32/store64. Adding a new instruction
rule is mechanical (~10 lines, same pattern).

4 — Composition rules (Adequacy.lean)

Proved once and reused by every program:

• wp_wasm_prop_call — if a callee terminates with postcondition P, and P
  implies the continuation's WP, then the call instruction succeeds. Fuel
  composition (callee and continuation may need different fuel amounts) is
  handled inside the lemma. Used four times in the swap proof (func0→func1,
  func1→func2, func4→func3, func4→func0), composed with the callee's
  TerminatesWith via TerminatesWith.mono. This is the intra-module version
  of what module linking will do inter-module.

• wp_wasm_prop_of_exec_eq — hop over an already-traced straight-line or
  block prefix to the next composition point (typically a .call). This is
  what removes concrete fuel bookkeeping from program proofs: only structural
  offsets (the block nesting depth) appear.

• wp_wasm_prop_block — Wasm's .block instruction runs its body; if the
  body ends in Fallthrough or Break 0, the block succeeds and execution
  continues. Mirrors exec_block_cons. Validated on toy examples for both
  disjuncts. Note: swap's bounds-check blocks exit via an outward break
  (Break 1) on the happy path, which is outside this rule's shape — func1
  traces the block section once at the exec level and hops over it instead.

• wp_wasm_prop_loop — loop invariant rule with a termination measure
  (invariant I, measure μ, per-iteration Fallthrough/Break-0 disjunction),
  proved by strong induction on the measure. Includes a below-stack pin across
  iterations. Validated on a toy countdown loop.

• wp_wasm_prop_to_TerminatesWith — bridges wp_wasm_prop (our internal
  representation) to TerminatesWith (Talos's spec-level statement).

5 — Swap proof (SwapSepLogic.lean)

• func2_terminates (core swap): wasm_heap_adequacy enters the iProp world;
  17 instructions stepped via per-instruction rules with ghost_id; the memory
  postcondition is pre-proved on the write64 chain with the Mem.*_disjoint
  framing lemmas.

• func3_terminates (frame setup): same iProp pipeline; two store32 operations
  spill ptr/len onto the shadow stack.

• func1_terminates_sw (bounds check + call): wp_wasm_prop_of_exec_eq hops
  over the three nested bounds-check blocks (happy path: br_if 1 breaks outward),
  then wp_wasm_prop_call splices in func2_terminates. Address arithmetic reuses
  elemAddr_of_shl from Spec.lean.

• swap_spec_sep (top-level): two hops and two wp_wasm_prop_calls compose
  func3_terminates and func0_terminates_sw, finishing with
  wp_wasm_prop_to_TerminatesWith → SwapElementsSpec.

Spec preconditions (Spec.lean, landed in #110/#151 line)

SwapElementsSpec carries two preconditions beyond the informal contract —
st.mem.pages ≤ 65536 and st.globals.globals[0]? = some (.i32 1048576) —
see the Spec.lean module docstring for why the statement is false without them.

What this enables next

The build-once infrastructure is being consumed by a merge_sort proof in progress, validating that the pattern generalizes beyond swap. The composition rules are designed with module linking in mind — wp_wasm_prop_call's shape (callee spec + continuation) is the intra-module version of what linking does inter-module.

Testing

• lake -d codelib build — passes, zero errors
• lake -d programs/lean build — passes, zero errors
• Sorry count: 0
• No axioms introduced
• No usage of old-system wp/wp_run/of_wp_entry_for/wp_call_tw

Generated with Claude Code

---

Description updated by maintainer alongside the review-fix commit: corrected the list of implemented instruction rules (ltU/leU/gtU/geU/and/eqz/shl/mul rules do not exist yet), described the actual composition mechanism (wp_wasm_prop_call + exec-level hops; the block rule is toy-validated but not applicable to swap's outward-breaking blocks), and added the scope note that ghost ownership is not yet tied to physical memory.