codelib: words32/slot32 twins + verified u32 copy loop (#68 phase 2c)

codelib/CodeLib.lean

@@ -8,6 +8,7 @@ import CodeLib.RustStd.Frame
 import CodeLib.RustStd.Region
 import CodeLib.RustStd.MemArray
 import CodeLib.RustStd.MemFillLoop
+import CodeLib.RustStd.MemCopyLoop
 import CodeLib.RustStd.UInt
 import CodeLib.RustStd.U64.Basic
 import CodeLib.RustStd.U64.AbsDiff

codelib/CodeLib/RustStd/MemArray.lean

@@ -68,14 +68,94 @@ 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]
 
+/-- Writing the `n`-th slot with `w` appends `w` to the length-`n` view (the
+earlier words are framed away). The store-into-a-fresh-slot step shared by
+copy/fill loops over a `u64` array; the 64-bit twin of
+`Mem.words32_write32_snoc`. -/
+theorem Mem.words64_write64_snoc (m : Mem) (base : UInt32) (n : Nat) (w : UInt64)
+    (hbnd : base.toNat + 8 * (n + 1) ≤ 4294967296) :
+    (m.write64 (base + 8 * UInt32.ofNat n) w).words64 base (n + 1)
+      = m.words64 base n ++ [w] := by
+  have haddr := Mem.words64_slotAddr_toNat base n (by omega)
+  rw [Mem.words64_succ,
+      Mem.words64_write64_outside m base n _ w (by omega) (Or.inr (by rw [haddr])),
+      Mem.read64_write64_same]
+
 /-- 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. -/
+loop invariant's inductive step; the `replicate`-specialised corollary of
+`Mem.words64_write64_snoc`. -/
 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']
+  rw [Mem.words64_write64_snoc m base n v hbnd, hfill, List.replicate_succ']
+
+/-! ## 32-bit twin
+
+`Mem.words32` is the `u32` array view, matching the element stride of
+`MemRegion.slot32` (and of the `wordsAt` view carried by the merge_sort work
+in PR #106, so that file can become an import — `wordsAt` is not in-tree yet). -/
+
+/-- The `List UInt32` view of the `u32` array `[base, base + 4*n)`. -/
+def Mem.words32 (m : Mem) (base : UInt32) (n : Nat) : List UInt32 :=
+  (List.range n).map fun k => m.read32 (base + 4 * (UInt32.ofNat k))
+
+@[simp] theorem Mem.length_words32 (m : Mem) (base : UInt32) (n : Nat) :
+    (m.words32 base n).length = n := by
+  simp [Mem.words32]
+
+theorem Mem.getElem_words32 (m : Mem) (base : UInt32) (n k : Nat) (h : k < n) :
+    (m.words32 base n)[k]'(by simpa using h) = m.read32 (base + 4 * UInt32.ofNat k) := by
+  simp [Mem.words32]
+
+/-- Two `u32` array views agree iff their words agree pointwise. -/
+theorem Mem.words32_ext {m m' : Mem} {base : UInt32} {n : Nat}
+    (h : ∀ k < n, m.read32 (base + 4 * UInt32.ofNat k) = m'.read32 (base + 4 * UInt32.ofNat k)) :
+    m.words32 base n = m'.words32 base n := by
+  apply List.ext_getElem (by simp)
+  intro k hk _
+  simp only [length_words32] at hk
+  rw [getElem_words32 m base n k hk, getElem_words32 m' base n k hk, h k hk]
+
+/-- The wasm address of the `k`-th `u32` slot, `base + 4 * k`, is the integer
+`base.toNat + 4 * k` as long as it does not wrap. Shared address bridge for the
+framing lemmas below (and their loop consumers); the 32-bit twin of
+`Mem.words64_slotAddr_toNat`. -/
+theorem Mem.words32_slotAddr_toNat (base : UInt32) (k : Nat)
+    (h : base.toNat + 4 * k < 4294967296) :
+    (base + 4 * UInt32.ofNat k).toNat = base.toNat + 4 * 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.slot32_base_toNat base (UInt32.ofNat k) (by rw [hkn]; omega)
+  rw [hkn] at this; exact this
+
+/-- A `write32` disjoint from the whole `[base, base+4n)` region leaves the
+view unchanged. -/
+theorem Mem.words32_write32_outside (m : Mem) (base : UInt32) (n : Nat) (a v : UInt32)
+    (hbnd : base.toNat + 4 * n ≤ 4294967296)
+    (hout : a.toNat + 4 ≤ base.toNat ∨ base.toNat + 4 * n ≤ a.toNat) :
+    (m.write32 a v).words32 base n = m.words32 base n := by
+  apply words32_ext
+  intro k hk
+  have haddr := Mem.words32_slotAddr_toNat base k (by omega)
+  exact Mem.read32_write32_disjoint m a _ v (by rw [haddr]; omega)
+
+/-- One more word: `words32 base (n+1)` is `words32 base n` with the `n`-th
+word appended. -/
+theorem Mem.words32_succ (m : Mem) (base : UInt32) (n : Nat) :
+    m.words32 base (n + 1) = m.words32 base n ++ [m.read32 (base + 4 * UInt32.ofNat n)] := by
+  simp [Mem.words32, List.range_succ, List.map_append]
+
+/-- Writing the `n`-th slot with `w` appends `w` to the length-`n` view (the
+earlier words are framed away). The store-into-a-fresh-slot step shared by
+copy/fill loops over a `u32` array. -/
+theorem Mem.words32_write32_snoc (m : Mem) (base : UInt32) (n : Nat) (w : UInt32)
+    (hbnd : base.toNat + 4 * (n + 1) ≤ 4294967296) :
+    (m.write32 (base + 4 * UInt32.ofNat n) w).words32 base (n + 1)
+      = m.words32 base n ++ [w] := by
+  have haddr := Mem.words32_slotAddr_toNat base n (by omega)
+  rw [Mem.words32_succ,
+      Mem.words32_write32_outside m base n _ w (by omega) (Or.inr (by rw [haddr])),
+      Mem.read32_write32_same]

codelib/CodeLib/RustStd/MemCopyLoop.lean

@@ -0,0 +1,126 @@
+import CodeLib.RustStd.MemArray
+import Interpreter.Wasm.Wp.Tactic
+import Interpreter.Wasm.Wp.Block
+import Interpreter.Wasm.Wp.Loop
+
+/-!
+# A verified copy loop over a `u32` array
+
+The companion to `MemFillLoop`: the canonical word-by-word copy loop reads each
+of the `n` `u32` words of `[src, src+4n)` and writes it to `[dst, dst+4n)`, and
+afterwards the destination view equals the (unchanged) source view —
+
+```
+st'.mem.words32 dst n = st.mem.words32 src n
+```
+
+for all `n`, given the two regions are disjoint, while every byte outside
+`[dst, dst+4n)` is left untouched (the frame condition, so the theorem composes
+with facts about neighbouring memory). This is the shape LLVM emits
+for a small `copy_from_slice` at `opt-level = 0` (a `load`/`store` loop, not a
+`memory.copy`), and the direct analogue of `merge_sort`'s copy helpers. It
+exercises the invariant/variant loop rule together with the `words32` view and
+`MemRegion` disjointness. -/
+
+namespace Wasm
+
+/-- Copy loop. Params `dst : i32`, `src : i32`, `n : i32`; local `i : i32`.
+Copies `mem[src + 4*i]` to `mem[dst + 4*i]` for `i = 0 … n-1`. -/
+def CopyWords : Program := [
+  .const 0, .localSet 3,
+  .loop 0 0 [
+    .block 0 0 [
+      .block 0 0 [
+        .localGet 3, .localGet 2, .ltU, .br_if 0,
+        .br 1
+      ],
+      .localGet 0, .localGet 3, .const 2, .shl, .add,
+      .localGet 1, .localGet 3, .const 2, .shl, .add,
+      .load32 0, .store32 0,
+      .localGet 3, .const 1, .add, .localSet 3,
+      .br 1 ] ]
+]
+
+set_option maxHeartbeats 1000000 in
+/-- Running `CopyWords` on a store where the two `u32` arrays are addressable,
+within the wasm32 page cap (no wraparound), and **disjoint** terminates with the
+destination holding a copy of the source, the source unchanged. -/
+theorem copyWords_spec (m : Module) (st : Store Unit) (dst src n : UInt32)
+    (hsrc : src.toNat + 4 * n.toNat ≤ st.mem.pages * 65536)
+    (hdst : dst.toNat + 4 * n.toNat ≤ st.mem.pages * 65536)
+    (hpages : st.mem.pages ≤ 65536)
+    (hdisj : MemRegion.Disjoint ⟨dst, 4 * n.toNat⟩ ⟨src, 4 * n.toNat⟩) :
+    wp m CopyWords
+        (fun c => ∃ st' s', c = .Fallthrough st' s'
+          ∧ st'.mem.words32 dst n.toNat = st.mem.words32 src n.toNat
+          ∧ st'.mem.words32 src n.toNat = st.mem.words32 src n.toNat
+          ∧ st'.mem.pages = st.mem.pages
+          ∧ ∀ a : Nat, (a < dst.toNat ∨ dst.toNat + 4 * n.toNat ≤ a) →
+              st'.mem.bytes a = st.mem.bytes a)
+        st { params := [.i32 dst, .i32 src, .i32 n], locals := [.i32 0], values := [] } := by
+  have hcap : st.mem.pages * 65536 ≤ 4294967296 := by
+    have := Nat.mul_le_mul_right 65536 hpages; omega
+  have hdisj : dst.toNat + 4 * n.toNat ≤ src.toNat ∨ src.toNat + 4 * n.toNat ≤ dst.toNat := hdisj
+  unfold CopyWords
+  wp_run
+  simp
+  apply wp_loop_cons
+    (Inv := fun st' s' => ∃ i : UInt32,
+      s' = ⟨[.i32 dst, .i32 src, .i32 n], [.i32 i], []⟩
+      ∧ i.toNat ≤ n.toNat
+      ∧ st'.mem.words32 dst i.toNat = st'.mem.words32 src i.toNat
+      ∧ st'.mem.words32 src n.toNat = st.mem.words32 src n.toNat
+      ∧ st'.mem.pages = st.mem.pages
+      ∧ ∀ a : Nat, (a < dst.toNat ∨ dst.toNat + 4 * 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)
+  · exact ⟨0, rfl, by simp, by simp [Mem.words32], rfl, rfl, fun a _ => rfl⟩
+  · rintro st' s' ⟨i, rfl, hile, hcopy, hsrceq, hpg, hframe⟩
+    apply wp_block_cons
+    apply wp_block_cons
+    wp_run
+    simp
+    by_cases hlt : i < n
+    · -- body: copy word i
+      have hilt : i.toNat < n.toNat := hlt
+      have hoi : UInt32.ofNat i.toNat = i := by simp [UInt32.ofNat_toNat]
+      have hshlU : i <<< 2 = 4 * i := MemRegion.shl2_eq_mul4 i
+      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 <<< 2 = i.toNat * 4 := by rw [Nat.shiftLeft_eq]
+      have haddr_d : 4 * i + dst = dst + 4 * UInt32.ofNat i.toNat := by
+        rw [hoi]; exact UInt32.add_comm _ _
+      have haddr_s : 4 * i + src = src + 4 * UInt32.ofNat i.toNat := by
+        rw [hoi]; exact UInt32.add_comm _ _
+      have hda : (dst + 4 * UInt32.ofNat i.toNat).toNat = dst.toNat + 4 * i.toNat :=
+        Mem.words32_slotAddr_toNat dst i.toNat (by omega)
+      simp only [hlt, ↓reduceIte, hshlU, hshlN, hmod1, haddr_d, haddr_s]
+      set w : UInt32 := st'.mem.read32 (src + 4 * UInt32.ofNat i.toNat) with hw
+      refine ⟨?_, ?_, ⟨?_, ?_, ?_, ?_, ?_⟩, ?_⟩
+      · rw [Nat.mod_eq_of_lt (by omega)]; omega      -- load in bounds
+      · rw [Nat.mod_eq_of_lt (by omega)]; omega      -- store in bounds
+      · omega                                        -- i+1 ≤ n
+      · -- words32 dst (i+1) = words32 src (i+1) at the new store
+        rw [Mem.words32_write32_snoc st'.mem dst i.toNat w (by omega),
+            Mem.words32_write32_outside st'.mem src (i.toNat + 1)
+              (dst + 4 * UInt32.ofNat i.toNat) w (by omega) (by rw [hda]; omega),
+            Mem.words32_succ, hcopy]
+      · -- words32 src n unchanged
+        rw [Mem.words32_write32_outside st'.mem src n.toNat
+              (dst + 4 * UInt32.ofNat i.toNat) w (by omega) (by rw [hda]; omega), hsrceq]
+      · exact hpg                                    -- pages
+      · -- frame: the write lands in `[dst, dst+4n)`, so bytes outside are kept
+        intro a ha
+        rw [Mem.write32_bytes_of_disjoint st'.mem (dst + 4 * UInt32.ofNat i.toNat) w a
+              (by rw [hda]; omega)]
+        exact hframe a ha
+      · omega                                        -- variant
+    · -- exit: i = n, dst view already equals src view
+      have hin : i.toNat = n.toNat := by
+        have : ¬ i.toNat < n.toNat := hlt
+        omega
+      simp only [hlt, ↓reduceIte]
+      rw [hin] at hcopy
+      exact ⟨hcopy.trans hsrceq, hsrceq, hpg, hframe⟩
+
+end Wasm

codelib/CodeLib/RustStd/Region.lean

@@ -188,6 +188,45 @@ theorem slot64_disjoint (base k l : UInt32)
   simp only [slot64]
   omega
 
+/-- The `k`-th 4-byte slot of a `u32` array based at `base` (wasm address
+`base + 4 * k`). The 32-bit twin of `slot64`, matching the `Mem.words32`
+element stride. -/
+def slot32 (base k : UInt32) : MemRegion := ⟨base + 4 * k, 4⟩
+
+/-- `x <<< 2 = 4 * x` on `UInt32`: the `(const 2) shl` address computation LLVM
+emits for a `u32` array index. -/
+theorem shl2_eq_mul4 (x : UInt32) : x <<< (2 % 32 : UInt32) = 4 * x := by bv_decide
+
+/-- The codegen's `(k <<< 2) + base` lands on the slot base address. The
+32-bit twin of `slot64_of_shl` (whose consumer is `SwapElementsSpec`); the
+`u32` element-slot proofs of the merge_sort work (PR #106) are the intended
+consumer here. -/
+theorem slot32_of_shl (base k : UInt32) :
+    k <<< (2 % 32 : UInt32) + base = (slot32 base k).base := by
+  simp only [slot32]; bv_decide
+
+/-- No wraparound: if the slot's true byte offset stays below `2^32`, the wasm
+address of `slot32 base k` is the integer `base.toNat + 4 * k.toNat`. -/
+theorem slot32_base_toNat (base k : UInt32)
+    (h : base.toNat + 4 * k.toNat < 4294967296) :
+    (slot32 base k).base.toNat = base.toNat + 4 * k.toNat := by
+  simp only [slot32, UInt32.toNat_add, UInt32.toNat_mul, UInt32.reduceToNat]
+  omega
+
+/-- Distinct in-bounds element slots of a no-wrap `u32` array are disjoint.
+The 32-bit twin of `slot64_disjoint`, for the same per-element aliasing
+arguments (`SwapElementsSpec`-style) over `u32` arrays (PR #106). -/
+theorem slot32_disjoint (base k l : UInt32)
+    (hk : base.toNat + 4 * k.toNat < 4294967296)
+    (hl : base.toNat + 4 * l.toNat < 4294967296)
+    (hkl : k ≠ l) :
+    (slot32 base k).Disjoint (slot32 base l) := by
+  unfold Disjoint
+  rw [slot32_base_toNat base k hk, slot32_base_toNat base l hl]
+  have : k.toNat ≠ l.toNat := fun he => hkl (UInt32.toNat.inj he)
+  simp only [slot32]
+  omega
+
 end MemRegion
 
 end Wasm