codelib: words64 array view + first ∀-quantified loop-over-memory proof

Phase 2b of #68, on top of the MemRegion algebra.

MemArray.lean — Mem.words64 base n : List UInt64, the list view of the u64
array [base, base+8n). Defined via List.range/map so length and indexing are
simp-lemmas; plus words64_ext, words64_write64_outside (framing through
MemRegion), words64_succ (snoc) and words64_write64_extend (the fill step as a
view equation). This is the codelib home for the memory-as-list view merge_sort
(#106) carries privately as wordsAt.

MemFillLoop.lean — fillWords_spec: the canonical fill loop writes v to each of
the n u64 slots of [base, base+8n), proved for ALL n via the invariant/variant
loop rule (wp_loop_cons), with the whole-region result stated as
  st'.mem.words64 base n.toNat = List.replicate n.toNat v.
Every memory example under interpreter/Examples is a concrete native_decide
check because symbolic framing lives downstream here in CodeLib; this is the
first universally-quantified loop-over-memory theorem in the repo, and the
shape merge_sort's proof needs.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: theebayuser

codelib/CodeLib.lean

@@ -5,6 +5,8 @@ import CodeLib.UInt32
 import CodeLib.UInt64
 import CodeLib.RustStd.Frame
 import CodeLib.RustStd.Region
+import CodeLib.RustStd.MemArray
+import CodeLib.RustStd.MemFillLoop
 import CodeLib.RustStd.UInt
 import CodeLib.RustStd.U64.Basic
 import CodeLib.RustStd.U64.AbsDiff

codelib/CodeLib/RustStd/MemArray.lean

@@ -0,0 +1,79 @@
+import CodeLib.RustStd.Region
+
+/-!
+# `CodeLib.RustStd.MemArray`
+
+A `List UInt64` *view* of a `u64` array in linear memory (issue #68, spec
+readability). `Mem.words64 base n` is the length-`n` 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]`.
+
+The view is defined via `List.range`/`map` so `length` and indexing are
+`simp`-lemmas, and its interaction with `write64` factors through the
+`MemRegion` framing algebra: a write disjoint from the array leaves the view
+unchanged (`words64_write64_outside`), and a write to slot `j` sets index `j`
+(`words64_write64_set`).
+-/
+
+namespace Wasm
+
+/-- The `List UInt64` view of the `u64` array `[base, base + 8*n)`. -/
+def Mem.words64 (m : Mem) (base : UInt32) (n : Nat) : List UInt64 :=
+  (List.range n).map fun k => m.read64 (base + 8 * (UInt32.ofNat k))
+
+@[simp] theorem Mem.length_words64 (m : Mem) (base : UInt32) (n : Nat) :
+    (m.words64 base n).length = n := by
+  simp [Mem.words64]
+
+theorem Mem.getElem_words64 (m : Mem) (base : UInt32) (n k : Nat) (h : k < n) :
+    (m.words64 base n)[k]'(by simpa using h) = m.read64 (base + 8 * UInt32.ofNat k) := by
+  simp [Mem.words64]
+
+/-- Two array views agree iff their words agree pointwise. -/
+theorem Mem.words64_ext {m m' : Mem} {base : UInt32} {n : Nat}
+    (h : ∀ k < n, m.read64 (base + 8 * UInt32.ofNat k) = m'.read64 (base + 8 * UInt32.ofNat k)) :
+    m.words64 base n = m'.words64 base n := by
+  apply List.ext_getElem (by simp)
+  intro k hk _
+  simp only [length_words64] at hk
+  rw [getElem_words64 m base n k hk, getElem_words64 m' base n k hk, h k hk]
+
+/-- Under no address wraparound, a `write64` whose target slot `j` is `≥ n`
+(i.e. outside the array `[base, base+8n)`) leaves the view unchanged. -/
+theorem Mem.words64_write64_outside (m : Mem) (base : UInt32) (n : Nat) (a : UInt32) (v : UInt64)
+    (hbnd : base.toNat + 8 * n ≤ 4294967296)
+    (hout : a.toNat + 8 ≤ base.toNat ∨ base.toNat + 8 * n ≤ a.toNat) :
+    (m.write64 a v).words64 base n = m.words64 base n := by
+  apply words64_ext
+  intro k hk
+  have hsize : (UInt32.size : Nat) = 4294967296 := rfl
+  have hkn : (UInt32.ofNat k).toNat = k :=
+    UInt32.toNat_ofNat_of_lt' (by omega : k < UInt32.size)
+  have haddr : (base + 8 * UInt32.ofNat k).toNat = base.toNat + 8 * k := by
+    have := MemRegion.slot64_base_toNat base (UInt32.ofNat k) (by rw [hkn]; omega)
+    rw [hkn] at this
+    exact this
+  exact Mem.read64_write64_disjoint m a _ v (by rw [haddr]; omega)
+
+/-- One more word: `words64 base (n+1)` is `words64 base n` with the `n`-th
+word appended. -/
+theorem Mem.words64_succ (m : Mem) (base : UInt32) (n : Nat) :
+    m.words64 base (n + 1) = m.words64 base n ++ [m.read64 (base + 8 * UInt32.ofNat n)] := by
+  simp [Mem.words64, List.range_succ, List.map_append]
+
+/-- The fill step, as a view equation: if the first `n` words are already `v`
+and slot `n` is written with `v`, the first `n+1` words are `v`. This is the
+loop invariant's inductive step, discharged once here. -/
+theorem Mem.words64_write64_extend (m : Mem) (base : UInt32) (n : Nat) (v : UInt64)
+    (hbnd : base.toNat + 8 * (n + 1) ≤ 4294967296)
+    (hfill : m.words64 base n = List.replicate n v) :
+    (m.write64 (base + 8 * UInt32.ofNat n) v).words64 base (n + 1) = List.replicate (n + 1) v := by
+  have hsize : (UInt32.size : Nat) = 4294967296 := rfl
+  have hkn : (UInt32.ofNat n).toNat = n :=
+    UInt32.toNat_ofNat_of_lt' (by omega : n < UInt32.size)
+  have haddr : (base + 8 * UInt32.ofNat n).toNat = base.toNat + 8 * n := by
+    have := MemRegion.slot64_base_toNat base (UInt32.ofNat n) (by rw [hkn]; omega)
+    rw [hkn] at this; exact this
+  rw [Mem.words64_succ,
+      Mem.words64_write64_outside m base n _ v (by omega) (Or.inr (by rw [haddr])),
+      hfill, Mem.read64_write64_same, List.replicate_succ']

codelib/CodeLib/RustStd/MemFillLoop.lean

@@ -0,0 +1,94 @@
+import CodeLib.RustStd.MemArray
+import Interpreter.Wasm.Wp.Tactic
+import Interpreter.Wasm.Wp.Block
+import Interpreter.Wasm.Wp.Loop
+
+/-!
+# A universally-quantified loop-over-memory proof
+
+Every memory example in `interpreter/.../Examples/` is a concrete
+`native_decide` check, because symbolic memory framing lives here in `CodeLib`,
+downstream of the interpreter. This file closes that gap with the first proof
+that a **loop** establishes a property of a **whole memory region for all `n`**:
+the canonical fill loop writes `v` to each of the `n` `u64` slots of
+`[base, base + 8n)`, and afterwards `mem.words64 base n = replicate n v`.
+
+It exercises the invariant/variant loop rule (`wp_loop_cons`), the `MemRegion`
+framing algebra, and the `words64` view together — the exact shape a
+memory-mutating corpus proof (e.g. `merge_sort`) needs. -/
+
+namespace Wasm
+
+/-- Fill loop. Params `base : i32`, `n : i32`, `v : i64`; local `i : i32`.
+Writes `v` to `mem[base + 8*i]` for `i = 0 … n-1`. Structure mirrors the
+`SimpleLoop` example's while-loop idiom. -/
+def FillWords : Program := [
+  .const 0, .localSet 3,
+  .loop 0 0 [
+    .block 0 0 [
+      .block 0 0 [
+        .localGet 3, .localGet 1, .ltU, .br_if 0,
+        .br 1
+      ],
+      .localGet 0, .localGet 3, .const 3, .shl, .add,
+      .localGet 2, .store64 0,
+      .localGet 3, .const 1, .add, .localSet 3,
+      .br 1 ] ]
+]
+
+set_option maxHeartbeats 1000000 in
+/-- Running `FillWords` on a store whose memory is large enough to hold the
+array (and within the wasm32 page cap, so element addresses do not wrap)
+terminates with `[base, base + 8n)` filled with `v` — stated over the whole
+region via `Mem.words64`. -/
+theorem fillWords_spec (m : Module) (st : Store Unit) (base n : UInt32) (v : UInt64)
+    (hbnd : base.toNat + 8 * n.toNat ≤ st.mem.pages * 65536)
+    (hpages : st.mem.pages ≤ 65536) :
+    wp m FillWords
+        (fun c => ∃ st' s', c = .Fallthrough st' s'
+          ∧ st'.mem.words64 base n.toNat = List.replicate n.toNat v
+          ∧ st'.mem.pages = st.mem.pages)
+        st { params := [.i32 base, .i32 n, .i64 v], locals := [.i32 0], values := [] } := by
+  have hcap : st.mem.pages * 65536 ≤ 4294967296 := by
+    have := Nat.mul_le_mul_right 65536 hpages; omega
+  unfold FillWords
+  wp_run
+  simp
+  apply wp_loop_cons
+    (Inv := fun st' s' => ∃ i : UInt32,
+      s' = ⟨[.i32 base, .i32 n, .i64 v], [.i32 i], []⟩
+      ∧ i.toNat ≤ n.toNat
+      ∧ st'.mem.words64 base i.toNat = List.replicate i.toNat v
+      ∧ st'.mem.pages = st.mem.pages)
+    (μ := fun _ s' => match s'.locals.headD (.i32 0) with | .i32 i => n.toNat - i.toNat | _ => 0)
+  · -- initial: i = 0, region empty
+    exact ⟨0, rfl, by simp, by simp [Mem.words64], rfl⟩
+  · -- step
+    rintro st' s' ⟨i, rfl, hile, hfill, hpg⟩
+    apply wp_block_cons
+    apply wp_block_cons
+    wp_run
+    simp
+    by_cases hlt : i < n
+    · -- body: write slot i, increment
+      have hilt : i.toNat < n.toNat := hlt
+      have hoi : UInt32.ofNat i.toNat = i := by simp [UInt32.ofNat_toNat]
+      have hmod1 : (1 + i.toNat) % 4294967296 = i.toNat + 1 := by
+        rw [Nat.mod_eq_of_lt (by have := n.toNat_lt; omega)]; omega
+      have hshlN : i.toNat <<< 3 = i.toNat * 8 := by rw [Nat.shiftLeft_eq]
+      have hshlU : i <<< 3 = 8 * i := by bv_decide
+      simp only [hlt, ↓reduceIte, hshlN, hmod1]
+      refine ⟨?_, ⟨?_, ?_, hpg⟩, ?_⟩
+      · rw [Nat.mod_eq_of_lt (by omega)]; omega
+      · omega
+      · rw [hshlU, show 8 * i + base = base + 8 * UInt32.ofNat i.toNat by rw [hoi]; bv_decide]
+        exact Mem.words64_write64_extend st'.mem base i.toNat v (by omega) hfill
+      · omega
+    · -- exit: i ≥ n, so i = n; region already fully filled
+      have hin : i.toNat = n.toNat := by
+        have : ¬ i.toNat < n.toNat := hlt
+        omega
+      simp only [hlt, ↓reduceIte]
+      rw [← hin]; exact ⟨hfill, hpg⟩
+
+end Wasm