|
| 1 | +import Interpreter.Wasm |
| 2 | +import CodeLib.RustStd.Frame |
| 3 | + |
| 4 | +/-! |
| 5 | +# `CodeLib.RustStd.Region` |
| 6 | +
|
| 7 | +Region-level memory algebra (issue #68, phase 2a), building on the byte-level |
| 8 | +framing lemmas in `CodeLib.RustStd.Frame`. |
| 9 | +
|
| 10 | +* `MemRegion` — a contiguous byte range of linear memory (`base` + `len`), with |
| 11 | + a decidable `Disjoint` predicate stated over `.toNat` intervals. The interval |
| 12 | + disjunction is the same load-bearing shape the `Frame` lemmas consume, so |
| 13 | + `omega` / `decide` keep discharging side conditions on concrete frame slots |
| 14 | + and symbolic array addresses alike. |
| 15 | +* Bridges from `Disjoint` facts to the `Frame` read/write lemmas |
| 16 | + (`Mem.read64_write64_of_region`, …): thin one-liners, so proofs can carry a |
| 17 | + single region fact instead of re-shaping `Or`s at every call site. |
| 18 | +* **Disjoint stores commute** (`Mem.write64_write64_comm`, 32/32 and mixed |
| 19 | + widths): requested in #68 and previously missing everywhere. Proved |
| 20 | + byte-pointwise from the function-model `Mem`. |
| 21 | +* `slot64` — the `k`-th 8-byte element slot of a `u64` array region, with the |
| 22 | + no-wrap and pairwise-disjointness lemmas array proofs otherwise re-derive |
| 23 | + (first consumer: `Project.SwapElements.Spec`). |
| 24 | +-/ |
| 25 | + |
| 26 | +namespace Wasm |
| 27 | + |
| 28 | +/-- A contiguous byte region of linear memory: base address and byte length. |
| 29 | +The `len` is a `Nat` (not `UInt32`): regions are *specification-level* objects, |
| 30 | +and keeping the length unbounded lets `Disjoint` talk about true integer |
| 31 | +intervals with no hidden wraparound. -/ |
| 32 | +structure MemRegion where |
| 33 | + base : UInt32 |
| 34 | + len : Nat |
| 35 | +deriving Repr, DecidableEq |
| 36 | + |
| 37 | +namespace MemRegion |
| 38 | + |
| 39 | +/-- Two regions occupy disjoint integer byte ranges. -/ |
| 40 | +def Disjoint (r₁ r₂ : MemRegion) : Prop := |
| 41 | + r₁.base.toNat + r₁.len ≤ r₂.base.toNat ∨ r₂.base.toNat + r₂.len ≤ r₁.base.toNat |
| 42 | + |
| 43 | +instance (r₁ r₂ : MemRegion) : Decidable (r₁.Disjoint r₂) := by |
| 44 | + unfold Disjoint; exact inferInstance |
| 45 | + |
| 46 | +theorem Disjoint.symm {r₁ r₂ : MemRegion} (h : r₁.Disjoint r₂) : r₂.Disjoint r₁ := |
| 47 | + h.elim Or.inr Or.inl |
| 48 | + |
| 49 | +end MemRegion |
| 50 | + |
| 51 | +/-! ## Bridging `Disjoint` to the `Frame` read/write lemmas |
| 52 | +
|
| 53 | +The `Frame` lemmas take the raw interval disjunction with the *write* address |
| 54 | +on the left; these wrappers take a `Disjoint` fact between the written region |
| 55 | +and the read region, in either order. -/ |
| 56 | + |
| 57 | +theorem Mem.read64_write64_of_region (m : Mem) (a b : UInt32) (v : UInt64) |
| 58 | + (h : MemRegion.Disjoint ⟨a, 8⟩ ⟨b, 8⟩) : |
| 59 | + (m.write64 a v).read64 b = m.read64 b := |
| 60 | + Mem.read64_write64_disjoint m a b v (h.elim Or.inr Or.inl) |
| 61 | + |
| 62 | +theorem Mem.read64_write32_of_region (m : Mem) (a b : UInt32) (v : UInt32) |
| 63 | + (h : MemRegion.Disjoint ⟨b, 4⟩ ⟨a, 8⟩) : |
| 64 | + (m.write32 b v).read64 a = m.read64 a := |
| 65 | + Mem.read64_write32_disjoint m a b v h |
| 66 | + |
| 67 | +theorem Mem.read32_write32_of_region (m : Mem) (a b v : UInt32) |
| 68 | + (h : MemRegion.Disjoint ⟨a, 4⟩ ⟨b, 4⟩) : |
| 69 | + (m.write32 a v).read32 b = m.read32 b := |
| 70 | + Mem.read32_write32_disjoint m a b v (h.elim Or.inr Or.inl) |
| 71 | + |
| 72 | +theorem Mem.read32_write64_of_region (m : Mem) (a b : UInt32) (v : UInt64) |
| 73 | + (h : MemRegion.Disjoint ⟨a, 4⟩ ⟨b, 8⟩) : |
| 74 | + (m.write64 b v).read32 a = m.read32 a := |
| 75 | + Mem.read32_write64_disjoint m a b v h |
| 76 | + |
| 77 | +/-! ## Disjoint stores commute -/ |
| 78 | + |
| 79 | +/-- Two memories with equal page counts and pointwise-equal bytes are equal. -/ |
| 80 | +theorem Mem.ext_bytes {m₁ m₂ : Mem} (hp : m₁.pages = m₂.pages) |
| 81 | + (hb : ∀ i, m₁.bytes i = m₂.bytes i) : m₁ = m₂ := by |
| 82 | + cases m₁; cases m₂ |
| 83 | + simp only [Mem.mk.injEq] |
| 84 | + exact ⟨hp, funext hb⟩ |
| 85 | + |
| 86 | +/-- Inside its 8-byte footprint, the byte written by a `write64` depends only |
| 87 | +on the address and value, not on the underlying memory. -/ |
| 88 | +theorem Mem.write64_bytes_in (m m' : Mem) (a : UInt32) (v : UInt64) (i : Nat) |
| 89 | + (hi : a.toNat ≤ i ∧ i < a.toNat + 8) : |
| 90 | + (m.write64 a v).bytes i = (m'.write64 a v).bytes i := by |
| 91 | + simp only [Mem.write64] |
| 92 | + split_ifs <;> first | rfl | omega |
| 93 | + |
| 94 | +/-- Inside its 4-byte footprint, the byte written by a `write32` depends only |
| 95 | +on the address and value, not on the underlying memory. -/ |
| 96 | +theorem Mem.write32_bytes_in (m m' : Mem) (a v : UInt32) (i : Nat) |
| 97 | + (hi : a.toNat ≤ i ∧ i < a.toNat + 4) : |
| 98 | + (m.write32 a v).bytes i = (m'.write32 a v).bytes i := by |
| 99 | + simp only [Mem.write32] |
| 100 | + split_ifs <;> first | rfl | omega |
| 101 | + |
| 102 | +/-- Two 64-bit stores to disjoint ranges commute. -/ |
| 103 | +theorem Mem.write64_write64_comm (m : Mem) (a b : UInt32) (v w : UInt64) |
| 104 | + (h : MemRegion.Disjoint ⟨a, 8⟩ ⟨b, 8⟩) : |
| 105 | + (m.write64 a v).write64 b w = (m.write64 b w).write64 a v := by |
| 106 | + have hd : a.toNat + 8 ≤ b.toNat ∨ b.toNat + 8 ≤ a.toNat := h |
| 107 | + refine Mem.ext_bytes (by simp) fun i => ?_ |
| 108 | + by_cases hia : a.toNat ≤ i ∧ i < a.toNat + 8 |
| 109 | + · rw [Mem.write64_bytes_of_disjoint _ b w i (by omega)] |
| 110 | + exact Mem.write64_bytes_in m (m.write64 b w) a v i hia |
| 111 | + · by_cases hib : b.toNat ≤ i ∧ i < b.toNat + 8 |
| 112 | + · rw [Mem.write64_bytes_of_disjoint (m.write64 b w) a v i (by omega)] |
| 113 | + exact Mem.write64_bytes_in (m.write64 a v) m b w i hib |
| 114 | + · rw [Mem.write64_bytes_of_disjoint _ b w i (by omega), |
| 115 | + Mem.write64_bytes_of_disjoint _ a v i (by omega), |
| 116 | + Mem.write64_bytes_of_disjoint _ a v i (by omega), |
| 117 | + Mem.write64_bytes_of_disjoint _ b w i (by omega)] |
| 118 | + |
| 119 | +/-- Two 32-bit stores to disjoint ranges commute. -/ |
| 120 | +theorem Mem.write32_write32_comm (m : Mem) (a b : UInt32) (v w : UInt32) |
| 121 | + (h : MemRegion.Disjoint ⟨a, 4⟩ ⟨b, 4⟩) : |
| 122 | + (m.write32 a v).write32 b w = (m.write32 b w).write32 a v := by |
| 123 | + have hd : a.toNat + 4 ≤ b.toNat ∨ b.toNat + 4 ≤ a.toNat := h |
| 124 | + refine Mem.ext_bytes (by simp) fun i => ?_ |
| 125 | + by_cases hia : a.toNat ≤ i ∧ i < a.toNat + 4 |
| 126 | + · rw [Mem.write32_bytes_of_disjoint _ b w i (by omega)] |
| 127 | + exact Mem.write32_bytes_in m (m.write32 b w) a v i hia |
| 128 | + · by_cases hib : b.toNat ≤ i ∧ i < b.toNat + 4 |
| 129 | + · rw [Mem.write32_bytes_of_disjoint (m.write32 b w) a v i (by omega)] |
| 130 | + exact Mem.write32_bytes_in (m.write32 a v) m b w i hib |
| 131 | + · rw [Mem.write32_bytes_of_disjoint _ b w i (by omega), |
| 132 | + Mem.write32_bytes_of_disjoint _ a v i (by omega), |
| 133 | + Mem.write32_bytes_of_disjoint _ a v i (by omega), |
| 134 | + Mem.write32_bytes_of_disjoint _ b w i (by omega)] |
| 135 | + |
| 136 | +/-- A 64-bit store and a 32-bit store to disjoint ranges commute. -/ |
| 137 | +theorem Mem.write64_write32_comm (m : Mem) (a b : UInt32) (v : UInt64) (w : UInt32) |
| 138 | + (h : MemRegion.Disjoint ⟨a, 8⟩ ⟨b, 4⟩) : |
| 139 | + (m.write64 a v).write32 b w = (m.write32 b w).write64 a v := by |
| 140 | + have hd : a.toNat + 8 ≤ b.toNat ∨ b.toNat + 4 ≤ a.toNat := h |
| 141 | + refine Mem.ext_bytes (by simp) fun i => ?_ |
| 142 | + by_cases hia : a.toNat ≤ i ∧ i < a.toNat + 8 |
| 143 | + · rw [Mem.write32_bytes_of_disjoint _ b w i (by omega)] |
| 144 | + exact Mem.write64_bytes_in m (m.write32 b w) a v i hia |
| 145 | + · by_cases hib : b.toNat ≤ i ∧ i < b.toNat + 4 |
| 146 | + · rw [Mem.write64_bytes_of_disjoint (m.write32 b w) a v i (by omega)] |
| 147 | + exact Mem.write32_bytes_in (m.write64 a v) m b w i hib |
| 148 | + · rw [Mem.write32_bytes_of_disjoint _ b w i (by omega), |
| 149 | + Mem.write64_bytes_of_disjoint _ a v i (by omega), |
| 150 | + Mem.write64_bytes_of_disjoint _ a v i (by omega), |
| 151 | + Mem.write32_bytes_of_disjoint _ b w i (by omega)] |
| 152 | + |
| 153 | +/-! ## Array element slots -/ |
| 154 | + |
| 155 | +namespace MemRegion |
| 156 | + |
| 157 | +/-- The `k`-th 8-byte slot of a `u64` array based at `base`. Its `base` is the |
| 158 | +wasm-level address `base + 8 * k` — definitionally the `elemAddr` shape used by |
| 159 | +array specs. -/ |
| 160 | +def slot64 (base k : UInt32) : MemRegion := ⟨base + 8 * k, 8⟩ |
| 161 | + |
| 162 | +/-- `x <<< 3 = 8 * x` on `UInt32`: bridges the `(const 3) shl` address |
| 163 | +computation LLVM emits to the `8 * k` slot offset. -/ |
| 164 | +theorem shl3_eq_mul8 (x : UInt32) : x <<< (3 % 32 : UInt32) = 8 * x := by bv_decide |
| 165 | + |
| 166 | +/-- The codegen's `(k <<< 3) + base` lands on the slot base address. -/ |
| 167 | +theorem slot64_of_shl (base k : UInt32) : |
| 168 | + k <<< (3 % 32 : UInt32) + base = (slot64 base k).base := by |
| 169 | + simp only [slot64]; bv_decide |
| 170 | + |
| 171 | +/-- No wraparound: if the slot's true byte offset stays below `2^32`, the wasm |
| 172 | +address of `slot64 base k` is the integer `base.toNat + 8 * k.toNat`. -/ |
| 173 | +theorem slot64_base_toNat (base k : UInt32) |
| 174 | + (h : base.toNat + 8 * k.toNat < 4294967296) : |
| 175 | + (slot64 base k).base.toNat = base.toNat + 8 * k.toNat := by |
| 176 | + simp only [slot64, UInt32.toNat_add, UInt32.toNat_mul, UInt32.reduceToNat] |
| 177 | + omega |
| 178 | + |
| 179 | +/-- Distinct in-bounds element slots of a no-wrap array are disjoint regions. -/ |
| 180 | +theorem slot64_disjoint (base k l : UInt32) |
| 181 | + (hk : base.toNat + 8 * k.toNat < 4294967296) |
| 182 | + (hl : base.toNat + 8 * l.toNat < 4294967296) |
| 183 | + (hkl : k ≠ l) : |
| 184 | + (slot64 base k).Disjoint (slot64 base l) := by |
| 185 | + unfold Disjoint |
| 186 | + rw [slot64_base_toNat base k hk, slot64_base_toNat base l hl] |
| 187 | + have : k.toNat ≠ l.toNat := fun he => hkl (UInt32.toNat.inj he) |
| 188 | + simp only [slot64] |
| 189 | + omega |
| 190 | + |
| 191 | +end MemRegion |
| 192 | + |
| 193 | +end Wasm |
0 commit comments