codelib: address review — frame condition, slot-addr helper, doc + reuse fixes

Follow-up to review of the words64 array view + fill-loop proof:

- fillWords_spec now carries a frame condition: every byte outside
  `[base, base+8n)` is preserved (postcondition + loop invariant), so the
  theorem composes with facts about neighbouring memory (the merge_sort shape).
- Extract `Mem.words64_slotAddr_toNat`, the shared no-wrap slot-address bridge,
  and use it in `words64_write64_outside` / `_extend` (was duplicated inline).
- FillWords' `(const 3) shl` step reuses `MemRegion.shl3_eq_mul8` instead of a
  fresh `bv_decide`.
- MemArray module docstring: drop the stale `words64_write64_set` reference
  (the lemma is `words64_write64_extend`) and correct the simp-lemma note
  (`getElem_words64` is intentionally not `@[simp]`).

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

Author: 2 people

codelib/CodeLib/RustStd/MemArray.lean

@@ -8,11 +8,12 @@ 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`).
+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
@@ -38,6 +39,18 @@ theorem Mem.words64_ext {m m' : Mem} {base : UInt32} {n : Nat}
   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)
@@ -46,13 +59,7 @@ theorem Mem.words64_write64_outside (m : Mem) (base : UInt32) (n : Nat) (a : UIn
     (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
+  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
@@ -68,12 +75,7 @@ theorem Mem.words64_write64_extend (m : Mem) (base : UInt32) (n : Nat) (v : UInt
     (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
+  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

@@ -11,7 +11,9 @@ Every memory example in `interpreter/.../Examples/` is a concrete
 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`.
+`[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
@@ -40,14 +42,16 @@ 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`. -/
+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)
+          ∧ 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
@@ -59,12 +63,14 @@ theorem fillWords_spec (m : Module) (st : Store Unit) (base n : UInt32) (v : UIn
       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)
+      ∧ 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
-    exact ⟨0, rfl, by simp, by simp [Mem.words64], rfl⟩
+  · -- 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⟩
+    rintro st' s' ⟨i, rfl, hile, hfill, hpg, hframe⟩
     apply wp_block_cons
     apply wp_block_cons
     wp_run
@@ -76,19 +82,29 @@ theorem fillWords_spec (m : Module) (st : Store Unit) (base n : UInt32) (v : UIn
       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
+      -- 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⟩, ?_⟩
+      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]
+      · 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]
-      rw [← hin]; exact ⟨hfill, hpg⟩
+      refine ⟨?_, hpg, hframe⟩
+      rw [← hin]; exact hfill
 
 end Wasm