sep-logic ownership: make the pointsTo layer load-bearing (Part 1: soundness bridge)

[mfornet]

Draft / WIP — stacked on top of cajal-technologies#133 (sep-logic-swap). Review this as an incremental follow-up to that PR, not a replacement.

Goal

Make the separation-logic ownership layer in cajal-technologies#133 actually load-bearing. Today func2_terminates reads/writes st.mem directly and proves disjointness of ptr_a/ptr_b/scratch with the manual byte-range lemmas (read64_write64_ne, write64_bytes_ne, hdisj) — the exact "manual byte-range lemmas" the PR description says ∗ replaces. The pointsTo_u64/swap_ownership/load_sound/store_sound machinery is defined but never consumed. This branch wires ownership in so the manual framing disappears.

Status

Part 1 — verified soundness bridge (this commit, 1d067ed). Builds clean (codelib + programs/lean).

• WasmHeap: added byte64/byte32 little-endian extractors that match Mem.write32/write64's stored-byte form exactly, and redefined pointsTo_u64/pointsTo_u32 in terms of them. Using the interpreter's own bit form (shift+mask) is what lets the bridge close by bv_decide instead of intractable v.toNat / 256^i % 256 Nat-division reasoning. Ownership is opaque to swap_ownership/arrayAt_*, so those proofs are untouched.
• WasmRules: replaced the decorative single-byte load_sound/store_sound with the real bridge:
  • read64_of_digits, write64_byte, write64_bytes_ne — pure Mem facts.
  • read64_sound (load): agreement + owning the 8 digit-bytes of v ⟹ mem.read64 addr = v.
  • write64_agree (store): updating exactly the 8 digit cells keeps agreement with mem.write64 addr v, with no disjointness hypotheses — an owned cell distinct from the 8 written keys cannot lie in [addr, addr+8) (no-wraparound), so write64 leaves it intact. This is the lemma that replaces read64_write64_ne.

This directly resolves the "decorative soundness bridge" finding: load_sound/store_sound are now real, tested, and shaped to be consumed by the WP rules.

Remaining (Part 2 — plan is fully mapped; mechanics prototyped)

1. Couple agreement into the WP. wp_wasm_F's general case becomes
   ∀ σ, ⌜heapAgreesWithMem σ ws.st.mem⌝ -∗ genHeapInterp σ ==∗ ∃ σ' st' locals', ⌜execOne …⌝ ∗ ⌜heapAgreesWithMem σ' st'.mem⌝ ∗ genHeapInterp σ' ∗ Φ ….
   Cascades to BIMonoPred.mono_pred, wp_wasm_step, and wasm_adequacy (each just threads the extra pure agree hyp/obligation — prototyped locally). wp_wasm_step specialises to memory-preserving instructions (extra hmem : st'.mem = st.mem), which is exactly why store instructions can no longer use it.
2. Ownership load64/store64 rules — mirror iris-lean HeapLang wp_load/wp_store (Iris/HeapLang/PrimitiveLaws.lean):
   • read: icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq extracts each get? σ (addr+i) = some (some (byte64 v i)) while retaining genHeapInterp σ; feed read64_sound ⇒ the loaded value is v.
   • write: imod genHeap_update $$ [$Hσ $Hpt] with ⟨Hσ, Hpt⟩ on each of the 8 cells; feed write64_agree ⇒ new agreement, no disjointness side-conditions.
     Minor bookkeeping: bridge pointsTo_u64's literal cell offsets (addr+1 … addr+7) to read64_sound/write64_agree's addr + UInt32.ofNat i.
3. wasm_heap_adequacy init from memory — build σ from the program's footprint bytes and hand out pointsTo_u64 via genHeap_init (which already yields [∗map] l↦v, l ↦ v); HeapLang's heap_adequacy adapted to the fixed byte array. This is the largest remaining piece.
4. Rewrite func2/func3 to use the ownership rules and delete read64_write64_ne / write64_bytes_ne / read64_write32_ne / hdisj from the swap proof. (store32/func3 also needs the u32 analogues write32_byte/write32_agree/read32_sound, straight copies of the u64 ones.)

🤖 Generated with Claude Code