|
| 1 | +import CodeLib.RustStd.MemArray |
| 2 | +import Interpreter.Wasm.Wp.Tactic |
| 3 | +import Interpreter.Wasm.Wp.Block |
| 4 | +import Interpreter.Wasm.Wp.Loop |
| 5 | + |
| 6 | +/-! |
| 7 | +# A verified copy loop over a `u32` array |
| 8 | +
|
| 9 | +The companion to `MemFillLoop`: the canonical word-by-word copy loop reads each |
| 10 | +of the `n` `u32` words of `[src, src+4n)` and writes it to `[dst, dst+4n)`, and |
| 11 | +afterwards the destination view equals the (unchanged) source view — |
| 12 | +
|
| 13 | +``` |
| 14 | +st'.mem.words32 dst n = st.mem.words32 src n |
| 15 | +``` |
| 16 | +
|
| 17 | +for all `n`, given the two regions are disjoint. This is the shape LLVM emits |
| 18 | +for a small `copy_from_slice` at `opt-level = 0` (a `load`/`store` loop, not a |
| 19 | +`memory.copy`), and the direct analogue of `merge_sort`'s copy helpers. It |
| 20 | +exercises the invariant/variant loop rule together with the `words32` view and |
| 21 | +`MemRegion` disjointness. -/ |
| 22 | + |
| 23 | +namespace Wasm |
| 24 | + |
| 25 | +/-- Copy loop. Params `dst : i32`, `src : i32`, `n : i32`; local `i : i32`. |
| 26 | +Copies `mem[src + 4*i]` to `mem[dst + 4*i]` for `i = 0 … n-1`. -/ |
| 27 | +def CopyWords : Program := [ |
| 28 | + .const 0, .localSet 3, |
| 29 | + .loop 0 0 [ |
| 30 | + .block 0 0 [ |
| 31 | + .block 0 0 [ |
| 32 | + .localGet 3, .localGet 2, .ltU, .br_if 0, |
| 33 | + .br 1 |
| 34 | + ], |
| 35 | + .localGet 0, .localGet 3, .const 2, .shl, .add, |
| 36 | + .localGet 1, .localGet 3, .const 2, .shl, .add, |
| 37 | + .load32 0, .store32 0, |
| 38 | + .localGet 3, .const 1, .add, .localSet 3, |
| 39 | + .br 1 ] ] |
| 40 | +] |
| 41 | + |
| 42 | +set_option maxHeartbeats 1000000 in |
| 43 | +/-- Running `CopyWords` on a store where the two `u32` arrays are addressable, |
| 44 | +within the wasm32 page cap (no wraparound), and **disjoint** terminates with the |
| 45 | +destination holding a copy of the source, the source unchanged. -/ |
| 46 | +theorem copyWords_spec (m : Module) (st : Store Unit) (dst src n : UInt32) |
| 47 | + (hsrc : src.toNat + 4 * n.toNat ≤ st.mem.pages * 65536) |
| 48 | + (hdst : dst.toNat + 4 * n.toNat ≤ st.mem.pages * 65536) |
| 49 | + (hpages : st.mem.pages ≤ 65536) |
| 50 | + (hdisj : dst.toNat + 4 * n.toNat ≤ src.toNat ∨ src.toNat + 4 * n.toNat ≤ dst.toNat) : |
| 51 | + wp m CopyWords |
| 52 | + (fun c => ∃ st' s', c = .Fallthrough st' s' |
| 53 | + ∧ st'.mem.words32 dst n.toNat = st.mem.words32 src n.toNat |
| 54 | + ∧ st'.mem.words32 src n.toNat = st.mem.words32 src n.toNat |
| 55 | + ∧ st'.mem.pages = st.mem.pages) |
| 56 | + st { params := [.i32 dst, .i32 src, .i32 n], locals := [.i32 0], values := [] } := by |
| 57 | + have hcap : st.mem.pages * 65536 ≤ 4294967296 := by |
| 58 | + have := Nat.mul_le_mul_right 65536 hpages; omega |
| 59 | + unfold CopyWords |
| 60 | + wp_run |
| 61 | + simp |
| 62 | + apply wp_loop_cons |
| 63 | + (Inv := fun st' s' => ∃ i : UInt32, |
| 64 | + s' = ⟨[.i32 dst, .i32 src, .i32 n], [.i32 i], []⟩ |
| 65 | + ∧ i.toNat ≤ n.toNat |
| 66 | + ∧ st'.mem.words32 dst i.toNat = st'.mem.words32 src i.toNat |
| 67 | + ∧ st'.mem.words32 src n.toNat = st.mem.words32 src n.toNat |
| 68 | + ∧ st'.mem.pages = st.mem.pages) |
| 69 | + (μ := fun _ s' => match s'.locals.headD (.i32 0) with | .i32 i => n.toNat - i.toNat | _ => 0) |
| 70 | + · exact ⟨0, rfl, by simp, by simp [Mem.words32], rfl, rfl⟩ |
| 71 | + · rintro st' s' ⟨i, rfl, hile, hcopy, hsrceq, hpg⟩ |
| 72 | + apply wp_block_cons |
| 73 | + apply wp_block_cons |
| 74 | + wp_run |
| 75 | + simp |
| 76 | + by_cases hlt : i < n |
| 77 | + · -- body: copy word i |
| 78 | + have hilt : i.toNat < n.toNat := hlt |
| 79 | + have hoi : UInt32.ofNat i.toNat = i := by simp [UInt32.ofNat_toNat] |
| 80 | + have hshlU : i <<< 2 = 4 * i := by bv_decide |
| 81 | + have hmod1 : (1 + i.toNat) % 4294967296 = i.toNat + 1 := by |
| 82 | + rw [Nat.mod_eq_of_lt (by have := n.toNat_lt; omega)]; omega |
| 83 | + have hshlN : i.toNat <<< 2 = i.toNat * 4 := by rw [Nat.shiftLeft_eq] |
| 84 | + have haddr_d : 4 * i + dst = dst + 4 * UInt32.ofNat i.toNat := by rw [hoi]; bv_decide |
| 85 | + have haddr_s : 4 * i + src = src + 4 * UInt32.ofNat i.toNat := by rw [hoi]; bv_decide |
| 86 | + have hda : (dst + 4 * UInt32.ofNat i.toNat).toNat = dst.toNat + 4 * i.toNat := by |
| 87 | + rw [hoi]; have := MemRegion.slot32_base_toNat dst i (by omega) |
| 88 | + simpa [MemRegion.slot32] using this |
| 89 | + simp only [hlt, ↓reduceIte, hshlU, hshlN, hmod1, haddr_d, haddr_s] |
| 90 | + set w : UInt32 := st'.mem.read32 (src + 4 * UInt32.ofNat i.toNat) with hw |
| 91 | + refine ⟨?_, ?_, ⟨?_, ?_, ?_, ?_⟩, ?_⟩ |
| 92 | + · rw [Nat.mod_eq_of_lt (by omega)]; omega -- load in bounds |
| 93 | + · rw [Nat.mod_eq_of_lt (by omega)]; omega -- store in bounds |
| 94 | + · omega -- i+1 ≤ n |
| 95 | + · -- words32 dst (i+1) = words32 src (i+1) at the new store |
| 96 | + rw [Mem.words32_write32_snoc st'.mem dst i.toNat w (by omega), |
| 97 | + Mem.words32_write32_outside st'.mem src (i.toNat + 1) |
| 98 | + (dst + 4 * UInt32.ofNat i.toNat) w (by omega) (by rw [hda]; omega), |
| 99 | + Mem.words32_succ, hcopy] |
| 100 | + · -- words32 src n unchanged |
| 101 | + rw [Mem.words32_write32_outside st'.mem src n.toNat |
| 102 | + (dst + 4 * UInt32.ofNat i.toNat) w (by omega) (by rw [hda]; omega), hsrceq] |
| 103 | + · exact hpg -- pages |
| 104 | + · omega -- variant |
| 105 | + · -- exit: i = n, dst view already equals src view |
| 106 | + have hin : i.toNat = n.toNat := by |
| 107 | + have : ¬ i.toNat < n.toNat := hlt |
| 108 | + omega |
| 109 | + simp only [hlt, ↓reduceIte] |
| 110 | + rw [hin] at hcopy |
| 111 | + exact ⟨hcopy.trans hsrceq, hsrceq, hpg⟩ |
| 112 | + |
| 113 | +end Wasm |
0 commit comments