feat(formal): real-lift R-mem (kernel) — linear memory + heap tuple round-trips

[hyperpolymath]

Fifth rung of the real lift (formal/REAL-LIFT.adoc): linear memory — the word-addressed heap and the deterministic cell layout (field i at base+i) the codegen's elaboration nodes assume, the precondition for arrays/records/strings/floats. Axiom-free.

Branch note: on claude/lucid-cray-4a22dp-rmem (per the per-rung branch convention, since the prior …/-r2loops and base branches are now protected post-merge). Diff is against current main, so it shows only the R-mem changes.

What landed

Target IR (RealWasm.v)

• Adds the faithful lib/wasm.ml memory instructions I32Load (off) / I32Store (off) to instr (+ dead step1 arms). Zero blast radius — wexec, cexec, compile_correct, and compile_stmt_correct all still compile unchanged.

R-mem kernel (new file RealMem.v)

• Word-addressed memory mem := list Z (each cell one i32), with mem_get / mem_set and the heap round-trip lemmas (get-after-set same/other, length) reused directly from RealWasm's set_nth_eq / set_nth_neq / set_nth_length.
• A bump allocator alloc n m = (length m, m ++ repeat 0 n) (base = current size) with base/length lemmas.
• The memory-aware executor mexec — because memory ops are straight-line (no nested control), mexec is a structural Fixpoint on the instruction list, no fuel needed (unlike R2's wexec / R2-loops' cexec). I32Load off pops addr a, pushes mem[⌊a⌋+off]; I32Store off pops value then addr, writes mem[⌊a⌋+off]; everything else defers to the memory-free step1. Plus the clean structural sequencing lemma mexec_app.
• mexec_store_then_load — storing v at a fresh in-range cell then loading it back yields v (set_nth's get-after-set, lifted through mexec).
• mexec_pair_build_proj — build a 2-cell tuple at base (store v0 at base+0, v1 at base+1) then project both fields back: the field i at base+i heap layout, proved as a get-after-set round-trip (Nat2Z.id discharges the Z.of_nat/Z.to_nat address round-trip).

Verification

coqc 8.18, whole formal/ track re-audited against current main:

• 20 files compile, 35 Print Assumptions reports, every one "Closed under the global context" — zero axioms, no Admitted.

Docs

formal/REAL-LIFT.adoc (R-mem row ⏳ + §8 status), formal/README.adoc (RealMem row + "real lift R0 → R-mem"), docs/PROOF-NEEDS.adoc (counts 19→20 / 33→35). _CoqProject / justfile / .hypatia-ignore wire RealMem.v in.

Remaining R-mem (next sub-rungs)

Runtime memory.grow/size allocator instruction; byte-granular layout; control-bearing field expressions (fuse mexec with the R2-loops cexec); and the full source tuple/array/record + indexing/field-access compile-correctness. Then R-float / R-str / R-call per the ladder.

Refs REAL-LIFT.adoc, docs/PROOF-NEEDS.adoc (K-1 row).

🤖 Generated with Claude Code

https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

---

Generated by Claude Code

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud