Skip to content

Commit 1c41a12

Browse files
theebayuserclaude
theebayuser
and
claude
authored
programs: prove SwapElementsSpec (swap_elements total correctness) (#137)
* codelib: generalize NumInteger's memory framing lemmas into RustStd.Frame Every opt-0 spec proof over linear memory needs the same read-after-write algebra: a read at B is unaffected by a write to a disjoint range at A. Those six lemmas lived as private copies in the NumInteger spec, so each new memory-based target (next: swap_elements, #110) would re-derive them. Move them into CodeLib.RustStd.Frame alongside the existing read-after-write-same lemmas: - Mem.write{32,64}_bytes_of_disjoint (byte-level footprints) - Mem.read{32,64}_write{32,64}_disjoint (all four width combinations) Statements are verbatim, only namespaced under Mem.; the .toNat disjunction shape is load-bearing because call sites discharge the side condition with `decide`/`omega` on concrete frame addresses. The disjoint family is deliberately not @[simp] (each rewrite has a side condition); only the unconditional same/pages lemmas stay global simp. NumInteger now consumes the shared copies, shrinking its spec by ~85 lines. Phase 1 of #68. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * programs: prove SwapElementsSpec (swap_elements total correctness) Discharges the statement-only `SwapElementsSpec` that #110 registered with "No proof is attempted here". The export swaps two `u64` elements of a slice in place; the proof follows the opt-0 call graph func4 → func3 → func0 → func1 → func2 with a per-function `TerminatesWith` lemma at each `call`, consuming the memory-framing family from `CodeLib.RustStd.Frame` (#131) at the leaves. Highlights: - func2_swap: the exchange leaf, stated as an explicit final-memory equation so callers frame reads themselves. - func1_swap: drives the three nested bounds-check `block`s; `i,j < len` makes both `panic`/`unreachable` branches dead, selecting the swap. - func4_swap: threads the shadow-stack frame (global 0 := 1048560), the fat pointer materialised by func3, and the teardown, then decodes the swap into the read-based postcondition. - elemAddr_toNat / elemAddr_disjoint: no-wrap address algebra. Two preconditions are added to the sketch, both documented in the module docstring as *necessary for soundness*, not convenience: the shadow-stack pointer is pinned to its initial value (`global 0 = 1048576`) and the memory respects the wasm32 page cap (`pages ≤ 65536`, ruling out `ptr + 8*k` wraparound). Without either, an input satisfying the original four hypotheses makes the postcondition false. They mirror the shadow-stack pin already used by `total_variation` and the interpreter's own in-bounds model. `lake build` green across the whole programs package; no `sorry`, no lint. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent 5c40dc9 commit 1c41a12

3 files changed

Lines changed: 409 additions & 109 deletions

File tree

‎codelib/CodeLib/RustStd/Frame.lean‎

Lines changed: 101 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,14 +16,23 @@ form that does not care about the concrete spill address:
1616
* `Mem.read{32,64}_write{32,64}_same` — read-after-write at the same
1717
address returns the value (no bound on the address needed).
1818
* `Mem.write{32,64}_pages` — a store leaves the page count unchanged.
19+
* `Mem.read{32,64}_write{32,64}_disjoint` — a read is unaffected by a
20+
write to a disjoint byte range, in every width combination, built on
21+
the byte-level `Mem.write{32,64}_bytes_of_disjoint`. Proofs that juggle
22+
several frame slots (argument spills vs. scratch vs. result) need these
23+
to carry a value across the unrelated stores in between.
1924
2025
The in-bounds (no-trap) obligation also needs `sp - 16` not to underflow;
2126
that is `UInt32.toNat_sub_of_le`, which Lean core already provides
2227
(`Init.Data.UInt.Lemmas`), so it is used directly rather than re-proved here.
2328
24-
The four `Mem.*` lemmas are intentionally global `@[simp]` — confluent,
25-
terminating rewrites used corpus-wide. Op-specific lemmas (e.g. `popcnt`
26-
bounds) are added here only once a real proof first consumes them.
29+
The unconditional `_same`/`_pages` lemmas are intentionally global `@[simp]`
30+
— confluent, terminating rewrites used corpus-wide. The `_disjoint` family
31+
is deliberately **not** `@[simp]`: each rewrite carries a disjointness side
32+
condition, so proofs name these lemmas explicitly (in a `simp only` set or
33+
a `rw`) and discharge the side goal with `decide` / `omega` on the concrete
34+
frame addresses. Op-specific lemmas (e.g. `popcnt` bounds) are added here
35+
only once a real proof first consumes them.
2736
-/
2837

2938
namespace Wasm
@@ -53,6 +62,95 @@ returns the stored value. -/
5362
Nat.reduceEqDiff]
5463
bv_decide
5564

65+
/-! ## Byte-level write footprints
66+
67+
A write only touches the bytes inside its footprint. These are the
68+
building blocks for the word-level disjointness lemmas below, and are
69+
occasionally useful on their own when a proof descends to `Mem.bytes`. -/
70+
71+
/-- A byte outside the 8-byte footprint of a `write64` is unchanged. -/
72+
theorem Mem.write64_bytes_of_disjoint (m : Mem) (a : UInt32) (v : UInt64) (i : Nat)
73+
(h : i < a.toNat ∨ a.toNat + 8 ≤ i) :
74+
(m.write64 a v).bytes i = m.bytes i := by
75+
simp only [Mem.write64]
76+
have h0 : i ≠ a.toNat := by omega
77+
have h1 : i ≠ a.toNat + 1 := by omega
78+
have h2 : i ≠ a.toNat + 2 := by omega
79+
have h3 : i ≠ a.toNat + 3 := by omega
80+
have h4 : i ≠ a.toNat + 4 := by omega
81+
have h5 : i ≠ a.toNat + 5 := by omega
82+
have h6 : i ≠ a.toNat + 6 := by omega
83+
have h7 : i ≠ a.toNat + 7 := by omega
84+
simp [h0, h1, h2, h3, h4, h5, h6, h7]
85+
86+
/-- A byte outside the 4-byte footprint of a `write32` is unchanged. -/
87+
theorem Mem.write32_bytes_of_disjoint (m : Mem) (a v : UInt32) (i : Nat)
88+
(h : i < a.toNat ∨ a.toNat + 4 ≤ i) :
89+
(m.write32 a v).bytes i = m.bytes i := by
90+
simp only [Mem.write32]
91+
have h0 : i ≠ a.toNat := by omega
92+
have h1 : i ≠ a.toNat + 1 := by omega
93+
have h2 : i ≠ a.toNat + 2 := by omega
94+
have h3 : i ≠ a.toNat + 3 := by omega
95+
simp [h0, h1, h2, h3]
96+
97+
/-! ## Disjoint read/write framing
98+
99+
A read is unaffected by a write to a disjoint byte range, in all four
100+
width combinations of the opt-0 corpus (`read{32,64}` × `write{32,64}`).
101+
The disjointness hypothesis puts one footprint entirely before the other,
102+
stated on `.toNat` so that `decide` / `omega` closes it when the frame
103+
addresses are concrete. -/
104+
105+
/-- A 64-bit read is unaffected by a 64-bit write to a disjoint 8-byte
106+
range. -/
107+
theorem Mem.read64_write64_disjoint (m : Mem) (a b : UInt32) (v : UInt64)
108+
(h : b.toNat + 8 ≤ a.toNat ∨ a.toNat + 8 ≤ b.toNat) :
109+
(m.write64 a v).read64 b = m.read64 b := by
110+
simp only [Mem.read64]
111+
rw [Mem.write64_bytes_of_disjoint m a v b.toNat (by omega),
112+
Mem.write64_bytes_of_disjoint m a v (b.toNat + 1) (by omega),
113+
Mem.write64_bytes_of_disjoint m a v (b.toNat + 2) (by omega),
114+
Mem.write64_bytes_of_disjoint m a v (b.toNat + 3) (by omega),
115+
Mem.write64_bytes_of_disjoint m a v (b.toNat + 4) (by omega),
116+
Mem.write64_bytes_of_disjoint m a v (b.toNat + 5) (by omega),
117+
Mem.write64_bytes_of_disjoint m a v (b.toNat + 6) (by omega),
118+
Mem.write64_bytes_of_disjoint m a v (b.toNat + 7) (by omega)]
119+
120+
/-- A 64-bit read is unaffected by a 32-bit write to a disjoint range. -/
121+
theorem Mem.read64_write32_disjoint (m : Mem) (a b : UInt32) (v : UInt32)
122+
(h : b.toNat + 4 ≤ a.toNat ∨ a.toNat + 8 ≤ b.toNat) :
123+
(m.write32 b v).read64 a = m.read64 a := by
124+
simp only [Mem.read64]
125+
rw [Mem.write32_bytes_of_disjoint m b v a.toNat (by omega),
126+
Mem.write32_bytes_of_disjoint m b v (a.toNat + 1) (by omega),
127+
Mem.write32_bytes_of_disjoint m b v (a.toNat + 2) (by omega),
128+
Mem.write32_bytes_of_disjoint m b v (a.toNat + 3) (by omega),
129+
Mem.write32_bytes_of_disjoint m b v (a.toNat + 4) (by omega),
130+
Mem.write32_bytes_of_disjoint m b v (a.toNat + 5) (by omega),
131+
Mem.write32_bytes_of_disjoint m b v (a.toNat + 6) (by omega),
132+
Mem.write32_bytes_of_disjoint m b v (a.toNat + 7) (by omega)]
133+
134+
/-- A 32-bit read is unaffected by a 32-bit write to a disjoint range. -/
135+
theorem Mem.read32_write32_disjoint (m : Mem) (a b v : UInt32)
136+
(h : b.toNat + 4 ≤ a.toNat ∨ a.toNat + 4 ≤ b.toNat) :
137+
(m.write32 a v).read32 b = m.read32 b := by
138+
simp only [Mem.read32]
139+
rw [Mem.write32_bytes_of_disjoint m a v b.toNat (by omega),
140+
Mem.write32_bytes_of_disjoint m a v (b.toNat + 1) (by omega),
141+
Mem.write32_bytes_of_disjoint m a v (b.toNat + 2) (by omega),
142+
Mem.write32_bytes_of_disjoint m a v (b.toNat + 3) (by omega)]
143+
144+
/-- A 32-bit read is unaffected by a 64-bit write to a disjoint range. -/
145+
theorem Mem.read32_write64_disjoint (m : Mem) (a : UInt32) (b : UInt32) (v : UInt64)
146+
(h : a.toNat + 4 ≤ b.toNat ∨ b.toNat + 8 ≤ a.toNat) :
147+
(m.write64 b v).read32 a = m.read32 a := by
148+
simp only [Mem.read32]
149+
rw [Mem.write64_bytes_of_disjoint m b v a.toNat (by omega),
150+
Mem.write64_bytes_of_disjoint m b v (a.toNat + 1) (by omega),
151+
Mem.write64_bytes_of_disjoint m b v (a.toNat + 2) (by omega),
152+
Mem.write64_bytes_of_disjoint m b v (a.toNat + 3) (by omega)]
153+
56154
/-! ## Stores preserve the page count -/
57155

58156
@[simp] theorem Mem.write32_pages (m : Mem) (a v : UInt32) :

‎programs/lean/Project/NumInteger/Spec.lean‎

Lines changed: 9 additions & 92 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,8 @@ hands pointers to `func1`, the actual binary-GCD loop. `func1` copies the
1414
operands into its own 48-byte scratch frame and runs Stein's algorithm
1515
entirely through `i64.load`/`i64.store`. The proof therefore threads the
1616
running values through the memory model with the read-after-write framing
17-
lemmas below, reusing the `UInt64` Stein lemmas from `CodeLib` for the
18-
arithmetic core.
17+
lemmas from `CodeLib.RustStd.Frame`, reusing the `UInt64` Stein lemmas
18+
from `CodeLib` for the arithmetic core.
1919
-/
2020

2121
namespace Project.NumInteger.Spec
@@ -24,89 +24,6 @@ open Wasm
2424

2525
set_option maxRecDepth 1048576
2626

27-
/-! ## Memory framing lemmas
28-
29-
Read-after-write algebra over the function-model `Mem`, specialized to the
30-
64-bit loads/stores this module performs. A 64-bit read sees a same-address
31-
64-bit write and is unaffected by a disjoint 64-bit or 32-bit write; a
32-
32-bit read sees a same-address 32-bit write. These are generic `Mem` facts
33-
developed here while the proof drives them out. -/
34-
35-
/-- A byte outside the 8-byte footprint of a `write64` is unchanged. -/
36-
theorem write64_bytes_of_disjoint (m : Mem) (a : UInt32) (v : UInt64) (i : Nat)
37-
(h : i < a.toNat ∨ a.toNat + 8 ≤ i) :
38-
(m.write64 a v).bytes i = m.bytes i := by
39-
simp only [Mem.write64]
40-
have h0 : i ≠ a.toNat := by omega
41-
have h1 : i ≠ a.toNat + 1 := by omega
42-
have h2 : i ≠ a.toNat + 2 := by omega
43-
have h3 : i ≠ a.toNat + 3 := by omega
44-
have h4 : i ≠ a.toNat + 4 := by omega
45-
have h5 : i ≠ a.toNat + 5 := by omega
46-
have h6 : i ≠ a.toNat + 6 := by omega
47-
have h7 : i ≠ a.toNat + 7 := by omega
48-
simp [h0, h1, h2, h3, h4, h5, h6, h7]
49-
50-
/-- A 64-bit read is unaffected by a 64-bit write to a disjoint 8-byte
51-
range. -/
52-
theorem read64_write64_disjoint (m : Mem) (a b : UInt32) (v : UInt64)
53-
(h : b.toNat + 8 ≤ a.toNat ∨ a.toNat + 8 ≤ b.toNat) :
54-
(m.write64 a v).read64 b = m.read64 b := by
55-
simp only [Mem.read64]
56-
rw [write64_bytes_of_disjoint m a v b.toNat (by omega),
57-
write64_bytes_of_disjoint m a v (b.toNat + 1) (by omega),
58-
write64_bytes_of_disjoint m a v (b.toNat + 2) (by omega),
59-
write64_bytes_of_disjoint m a v (b.toNat + 3) (by omega),
60-
write64_bytes_of_disjoint m a v (b.toNat + 4) (by omega),
61-
write64_bytes_of_disjoint m a v (b.toNat + 5) (by omega),
62-
write64_bytes_of_disjoint m a v (b.toNat + 6) (by omega),
63-
write64_bytes_of_disjoint m a v (b.toNat + 7) (by omega)]
64-
65-
/-- A byte outside the 4-byte footprint of a `write32` is unchanged. -/
66-
theorem write32_bytes_of_disjoint (m : Mem) (a v : UInt32) (i : Nat)
67-
(h : i < a.toNat ∨ a.toNat + 4 ≤ i) :
68-
(m.write32 a v).bytes i = m.bytes i := by
69-
simp only [Mem.write32]
70-
have h0 : i ≠ a.toNat := by omega
71-
have h1 : i ≠ a.toNat + 1 := by omega
72-
have h2 : i ≠ a.toNat + 2 := by omega
73-
have h3 : i ≠ a.toNat + 3 := by omega
74-
simp [h0, h1, h2, h3]
75-
76-
/-- A 64-bit read is unaffected by a 32-bit write to a disjoint range. -/
77-
theorem read64_write32_disjoint (m : Mem) (a b : UInt32) (v : UInt32)
78-
(h : b.toNat + 4 ≤ a.toNat ∨ a.toNat + 8 ≤ b.toNat) :
79-
(m.write32 b v).read64 a = m.read64 a := by
80-
simp only [Mem.read64]
81-
rw [write32_bytes_of_disjoint m b v a.toNat (by omega),
82-
write32_bytes_of_disjoint m b v (a.toNat + 1) (by omega),
83-
write32_bytes_of_disjoint m b v (a.toNat + 2) (by omega),
84-
write32_bytes_of_disjoint m b v (a.toNat + 3) (by omega),
85-
write32_bytes_of_disjoint m b v (a.toNat + 4) (by omega),
86-
write32_bytes_of_disjoint m b v (a.toNat + 5) (by omega),
87-
write32_bytes_of_disjoint m b v (a.toNat + 6) (by omega),
88-
write32_bytes_of_disjoint m b v (a.toNat + 7) (by omega)]
89-
90-
/-- A 32-bit read is unaffected by a 32-bit write to a disjoint range. -/
91-
theorem read32_write32_disjoint (m : Mem) (a b v : UInt32)
92-
(h : b.toNat + 4 ≤ a.toNat ∨ a.toNat + 4 ≤ b.toNat) :
93-
(m.write32 a v).read32 b = m.read32 b := by
94-
simp only [Mem.read32]
95-
rw [write32_bytes_of_disjoint m a v b.toNat (by omega),
96-
write32_bytes_of_disjoint m a v (b.toNat + 1) (by omega),
97-
write32_bytes_of_disjoint m a v (b.toNat + 2) (by omega),
98-
write32_bytes_of_disjoint m a v (b.toNat + 3) (by omega)]
99-
100-
/-- A 32-bit read is unaffected by a 64-bit write to a disjoint range. -/
101-
theorem read32_write64_disjoint (m : Mem) (a : UInt32) (b : UInt32) (v : UInt64)
102-
(h : a.toNat + 4 ≤ b.toNat ∨ b.toNat + 8 ≤ a.toNat) :
103-
(m.write64 b v).read32 a = m.read32 a := by
104-
simp only [Mem.read32]
105-
rw [write64_bytes_of_disjoint m b v a.toNat (by omega),
106-
write64_bytes_of_disjoint m b v (a.toNat + 1) (by omega),
107-
write64_bytes_of_disjoint m b v (a.toNat + 2) (by omega),
108-
write64_bytes_of_disjoint m b v (a.toNat + 3) (by omega)]
109-
11027
/-! ## Shift-amount bridge
11128
11229
The wasm computes each Stein shift count by `i64.ctz`, narrows it to an
@@ -232,7 +149,7 @@ theorem meatLoop_wp (env : HostEnv Unit) (stm : Store Unit) (a b : UInt64)
232149
Nat.reduceLT, Nat.reduceAdd, Nat.reduceMul, Nat.reduceSub, reduceIte,
233150
Nat.reduceLeDiff,
234151
UInt32.reduceAdd, UInt32.reduceToNat, gt_iff_lt,
235-
read64_write64_disjoint, read64_write32_disjoint,
152+
Mem.read64_write64_disjoint, Mem.read64_write32_disjoint,
236153
Mem.read32_write32_same,
237154
hpg, ha, hb,
238155
Mem.write64_pages, Mem.write32_pages]
@@ -261,8 +178,8 @@ theorem meatLoop_wp (env : HostEnv Unit) (stm : Store Unit) (a b : UInt64)
261178
have hLpg : stL.mem.pages = 16 := by rw [hstL]; simp [hpg]
262179
have hLa : stL.mem.read64 1048520 = ao := by
263180
rw [hstL]
264-
rw [read64_write64_disjoint _ _ _ _ (by decide),
265-
read64_write32_disjoint _ _ _ _ (by decide),
181+
rw [Mem.read64_write64_disjoint _ _ _ _ (by decide),
182+
Mem.read64_write32_disjoint _ _ _ _ (by decide),
266183
Mem.read64_write64_same]
267184
have hLb : stL.mem.read64 1048528 = bo := by
268185
rw [hstL]; rw [Mem.read64_write64_same]
@@ -318,7 +235,7 @@ theorem meatLoop_wp (env : HostEnv Unit) (stm : Store Unit) (a b : UInt64)
318235
List.getElem?_cons_zero, List.getElem?_cons_succ, List.set_cons_zero, List.set_cons_succ,
319236
Nat.reduceLT, Nat.reduceAdd, Nat.reduceMul, Nat.reduceSub, reduceIte,
320237
UInt32.reduceAdd, UInt32.reduceToNat, gt_iff_lt, hpg', hxr, hyr,
321-
Mem.read64_write64_same, read64_write64_disjoint, read64_write32_disjoint,
238+
Mem.read64_write64_same, Mem.read64_write64_disjoint, Mem.read64_write32_disjoint,
322239
Mem.read32_write32_same,
323240
Mem.write64_pages, Mem.write32_pages]
324241
simp only [List.take_zero, List.drop_zero, List.nil_append]
@@ -395,12 +312,12 @@ theorem func1_terminates (env : HostEnv Unit) (st1 : Store Unit) (a b : UInt64)
395312
-- After frame setup + the two argument copies the memory is
396313
-- `(st1.mem.write64 1048520 a).write64 1048528 b`, the frame pointer is
397314
-- `local2 = 1048512`, and the bound checks are discharged by `hpg`.
398-
simp [ha, hb, read64_write64_disjoint, hpg]
315+
simp [ha, hb, Mem.read64_write64_disjoint, hpg]
399316
-- Memory now holds `a` at slot 1048520 and `b` at slot 1048528; frame
400317
-- pointer (local 2) is 1048512. Abbreviate the in-frame store.
401318
set M0 : Mem := (st1.mem.write64 1048520 a).write64 1048528 b with hM0
402319
have hM0a : M0.read64 1048520 = a := by
403-
rw [hM0, read64_write64_disjoint _ _ _ _ (by decide), Mem.read64_write64_same]
320+
rw [hM0, Mem.read64_write64_disjoint _ _ _ _ (by decide), Mem.read64_write64_same]
404321
have hM0b : M0.read64 1048528 = b := by
405322
rw [hM0, Mem.read64_write64_same]
406323
have hM0pg : M0.pages = 16 := by rw [hM0]; simp [hpg]
@@ -492,7 +409,7 @@ theorem func0_terminates (env : HostEnv Unit) (a b : UInt64) :
492409
(func1_terminates env _ a b []
493410
(by rw [Mem.write64_pages, Mem.write64_pages]; exact hp)
494411
(by rfl)
495-
(by rw [read64_write64_disjoint _ _ _ _ (by decide), Mem.read64_write64_same])
412+
(by rw [Mem.read64_write64_disjoint _ _ _ _ (by decide), Mem.read64_write64_same])
496413
(by rw [Mem.read64_write64_same]))
497414
-- The call returns `gcd a b`; restore the stack pointer and `ret`.
498415
rintro stA vsA ⟨hAglob, rfl⟩

0 commit comments

Comments
 (0)