codelib: words64 array view + first ∀-quantified loop-over-memory proof (#68 phase 2b)

[theebayuser]

Overview

Phase 2b of #68: a List UInt64 view of a u64 array in linear memory, plus the first proof in the repo that a loop establishes a whole-region property for all n.

Stacked on #131, #137, #138 (review the last two commits: MemArray.lean + MemFillLoop.lean).

Mem.words64 — the array view (CodeLib.RustStd.MemArray)

m.words64 base n : List UInt64 is the list of words at base, base+8, …, base+8(n−1), so a spec can say m.words64 base n = vs instead of ∀ k < n, m.read64 (base + 8*k) = vs[k]. Defined via List.range/map, so:

• length_words64, getElem_words64 are simp-lemmas.
• words64_ext — two views agree iff their words agree pointwise.
• words64_write64_outside — a write disjoint from [base, base+8n) leaves the view unchanged (factors through the MemRegion framing from codelib: region-disjointness algebra (MemRegion) + disjoint-write commutation (#68 phase 2a) #138).
• words64_succ — snoc: words64 base (n+1) is words64 base n with the n-th word appended.
• words64_write64_extend — the fill step as a view equation: first n words = v and slot n written with v ⇒ first n+1 words = v.

This is the codelib home for the memory-as-list view that merge_sort (#106) currently carries privately as wordsAt; the 32-bit variant follows the same skeleton if wanted.

The loop-over-memory proof (CodeLib.RustStd.MemFillLoop)

Every memory example under interpreter/.../Examples/ is a concrete native_decide check — because symbolic memory framing lives downstream in CodeLib, so an interpreter example can't reach it. This file closes that gap: fillWords_spec proves that the canonical fill loop (params base, n, v; writes v to each of the n u64 slots) terminates with

st'.mem.words64 base n.toNat = List.replicate n.toNat v

for all n, via the invariant/variant loop rule wp_loop_cons (invariant: "first i words are v, i ≤ n"; variant: n − i). The per-iteration store bound is discharged from the addressability + pages ≤ 65536 no-wrap preconditions, and the inductive step is a one-liner against words64_write64_extend. This is the exact shape a memory-mutating corpus proof (merge_sort) needs, and the first universally-quantified loop-over-memory theorem in the repo.

Verification

• lake build green in codelib/; zero lint warnings.
• #print axioms fillWords_spec → standard axioms + the bv_decide reflection axioms from the shift lemma; no sorryAx.
• Consumers land with the code: words64_write64_outside/_extend are consumed by fillWords_spec; words64 itself by both.

Refs #68, #106.

---

Disclosure per CONTRIBUTING: AI tooling (Claude Code) was used to write and check these proofs; I own the change and am accountable for every line.

🤖 Generated with Claude Code