Swap ownership fix ( iprop)

[Isabelle9999]

Builds on the soundness bridge from Isabelle9999#1 (Part 1).

Makes the swap proof load-bearing using separation logic via iris-lean. The postcondition is derived directly from iProp ownership witnesses, every memory operation (3 × i64.load, 3 × i64.store) uses iProp ownership tokens.

How it works: the proof enters iProp via a single wasm_heap_adequacy_with_mem call, which initializes a ghost heap (genHeapInterp σ₀) matching actual memory. From there, every instruction unfolds the iris-lean WP fixpoint (least_fixpoint_unfold_mpr). Each load consumes a pointsTo_u64 token to read a value; each store consumes a token and produces an updated one with the new value. The ghost heap state threads through 16 transitions (σ₁ → ... → σ₁₆'), and the postcondition (values swapped, other memory unchanged) follows from the ownership witnesses (not manual memory disjointness)

Build timeout fix: The 24-entry ghost heap (3 regions × 8 bytes) caused two issues. First, ExtTreeMap's O(n²) comparison-based lookup, solved by PosTrie, a positional binary trie with O(log n) structural lookup. Second, decomposing the ghost heap required 276 address distinctness proofs, each running omega on UInt32 arithmetic. Solved by parameterized lemmas (addr_ne_intra, addr_ne_cross) that prove distinctness once via omega and cache in .olean, and all 276 call sites use by decide instead, with zero omega at elaboration time. The decomposition itself is packaged in a cached wrapper theorem (swap_σ₀_to_pointsTo) called once per case rather than inlined.

For small-step conversion: func2 is straight-line (no loops/blocks), so the proof structure & iProp proof body stays the same. After the small-step rewrite, only the instruction-stepping calls (execOne.eq_def → new step relation) change

[Isabelle9999]

Build on func2_terminates in SwapSepLogic.lean times out because the iProp proof builds a 24-entry ghost heap σ₀ (8 bytes × 3 memory regions: ptr_a, ptr_b, scratch). Each lookup lemma (get? σ₀ addr = some v) requires simp to rewrite through 24 nested PartialMap.insert calls on ExtTreeMap. This causes O(n²) simp steps via typeclass-dispatched comparisons, exceeding any reasonable maxSteps (simp has a configurable maxSteps parameter (default: 128,000) that limits the total
number of rewrite steps per invocation).

The iProp proof itself is fine, Lean's typechecker shows zero errors when given enough heartbeats ( set_option maxHeartbeats 800M0, but 800M heartbeats builds for many hours.

I tried a workaround implementing an opaque swap_σ₀ definition with 24 individual lookup lemmas proven via unfold/split_ifs/helper lemmas, to make the swap proof build within a reasonable time, but I'm not sure if this will work.

Right now I'm also trying to replace iris-lean's ExtTreeMap ( comparison-based maps) with positional binary tries (Appel & Leroy's canonical representation). ExtTreeMap stores entries in a balanced tree ordered by key comparison. When Lean's simp looks up a key in a map built from 24 sequential inserts, it compare the lookup key against each inserted key one by one, starting from the outermost insert and working inward. Each comparison triggers UInt32 ordering via typeclass dispatch. For n entries, this requires n comparisons per lookup × n lookups = O(n²) total
simp steps. Where positional binary tries (used by Coq's stdpp since v1.8.0) encode the key's binary digits as a path through the trie, so no comparisons needed. Lookup follows the path in O(log n) steps regardless of map size.

reference: Coq's stdpp related performance issue (gitlab.mpi-sws.org/iris/stdpp/-/issues/64) and fixed it by re-implementing their finite maps with Appel & Leroy's canonical binary tries in v1.8.0 (gitlab.mpi-sws.org/iris/stdpp/blob/master/CHANGELOG.md, under "std++ 1.8.0"). This implementation is current, std++ 1.13.0 (March 2026).

[Isabelle9999]

superseded