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

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,81 @@
+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 its length is a `simp`-lemma
+(`length_words64`) and indexing rewrites through `getElem_words64` (kept off
+`simp` because of its bounds side-goal). Its interaction with `write64` factors
+through the `MemRegion` framing algebra: a write disjoint from the array leaves
+the view unchanged (`words64_write64_outside`), and writing `v` to the next slot
+past a `v`-filled prefix extends the fill by one (`words64_write64_extend`).
+-/
+
+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]
+
+/-- The wasm address of the `k`-th `u64` slot, `base + 8 * k`, is the integer
+`base.toNat + 8 * k` as long as it does not wrap. Shared address bridge for the
+framing lemmas below (and their loop consumers). -/
+theorem Mem.words64_slotAddr_toNat (base : UInt32) (k : Nat)
+    (h : base.toNat + 8 * k < 4294967296) :
+    (base + 8 * UInt32.ofNat k).toNat = base.toNat + 8 * k := by
+  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 := MemRegion.slot64_base_toNat base (UInt32.ofNat k) (by rw [hkn]; omega)
+  rw [hkn] at this; exact this
+
+/-- 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 haddr := Mem.words64_slotAddr_toNat base k (by omega)
+  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 haddr := Mem.words64_slotAddr_toNat base n (by omega)
+  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,110 @@
+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` while
+every byte *outside* `[base, base + 8n)` is left untouched (the frame
+condition, so the theorem composes with facts about neighbouring memory).
+
+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` — and every byte outside the region left unchanged. -/
+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
+          ∧ ∀ a : Nat, (a < base.toNat ∨ base.toNat + 8 * n.toNat ≤ a) →
+              st'.mem.bytes a = st.mem.bytes a)
+        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
+      ∧ ∀ a : Nat, (a < base.toNat ∨ base.toNat + 8 * n.toNat ≤ a) →
+          st'.mem.bytes a = st.mem.bytes a)
+    (μ := fun _ s' => match s'.locals.headD (.i32 0) with | .i32 i => n.toNat - i.toNat | _ => 0)
+  · -- initial: i = 0, region empty, memory untouched
+    exact ⟨0, rfl, by simp, by simp [Mem.words64], rfl, fun a _ => rfl⟩
+  · -- step
+    rintro st' s' ⟨i, rfl, hile, hfill, hpg, hframe⟩
+    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]
+      -- The `(const 3) shl` address computation is the `MemRegion` slot bridge.
+      have hshlU : i <<< 3 = 8 * i := MemRegion.shl3_eq_mul8 i
+      have haddrU : i <<< 3 + base = base + 8 * UInt32.ofNat i.toNat := by
+        rw [hshlU, hoi]; bv_decide
+      have haddrN : (i <<< 3 + base).toNat = base.toNat + 8 * i.toNat := by
+        rw [haddrU]; exact Mem.words64_slotAddr_toNat base i.toNat (by omega)
+      simp only [hlt, ↓reduceIte, hshlN, hmod1]
+      refine ⟨?_, ⟨?_, ?_, hpg, ?_⟩, ?_⟩
+      · rw [Nat.mod_eq_of_lt (by omega)]; omega
+      · omega
+      · rw [haddrU]
+        exact Mem.words64_write64_extend st'.mem base i.toNat v (by omega) hfill
+      · -- frame: the write lands in `[base, base+8n)`, so bytes outside are kept
+        intro a ha
+        rw [Mem.write64_bytes_of_disjoint st'.mem (i <<< 3 + base) v a (by rw [haddrN]; omega)]
+        exact hframe a ha
+      · 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]
+      refine ⟨?_, hpg, hframe⟩
+      rw [← hin]; exact hfill
+
+end Wasm