deflate.c.engine.slide.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«deflate.c.engine.macros»
2import ZlibF.Proof.«deflate.c.engine.chains»
3
4/-!
5# deflate.c, engine: `slide_hash`
6
7`slide_hash` rescales `head` (`hash_size` entries) and `prev` (`w_size` entries): every entry `m` becomes
8`m >= w_size ? m - w_size : NIL`, and `slid` becomes 1. Both loops are `do ... while (--n)` loops that walk a
9pointer down from the end of the array; they run `n` times when `n >= 1`. The entries may hold any value (`prev` is
10never cleared), so the theorem holds for every content of the two arrays.
11-/
12
13namespace Zlib.Deflate.Engine.Proofs
14open C Zlib.Deflate
15
16/-- The body of the two loops of `slide_hash`, as in the translation. -/
17def slBody (wsize : UInt32) : UInt32 × WPtr → M (UInt32 × WPtr) := fun (n, p) => do
18  let p ← psub p 1
19  let m : UInt32 := (← Ptr.load p).toUInt32
20  Ptr.store p (if m ≥ wsize then (m - wsize).toUInt16 else (0 : UInt16))
21  pure (n, p)
22
23/-- The condition `while (--n)` of the two loops. -/
24def slCond : UInt32 × WPtr → M (Bool × (UInt32 × WPtr)) := fun (n, p) => let n := n - 1; pure (n != 0, (n, p))
25
26theorem slide_hash_unfold (s : DeflateStatePtr) : slide_hash s = (do
27    let d ← ldDeflateState s
28    let wsize : UInt32 := d.w_size
29    let n : UInt32 := d.hash_size
30    let p : WPtr ← padd d.head n.toNat
31    let (_, _) ← cdoWhile (slBody wsize) slCond (n, p)
32    let n : UInt32 := wsize
33    let p : WPtr ← padd d.prev n.toNat
34    let (_, _) ← cdoWhile (slBody wsize) slCond (n, p)
35    wr s (fun d => { d with slid := 1 })) := rfl
36
37
38theorem slideVal_eq (wsize : UInt32) (m : UInt16) :
39    (if m.toUInt32 ≥ wsize then (m.toUInt32 - wsize).toUInt16 else (0 : UInt16)) = slideVal wsize m := by
40  unfold slideVal; split <;> simp_all
41
42theorem u32_sub_one_toNat (n : UInt32) (h : 1 ≤ n.toNat) : (n - 1).toNat = n.toNat - 1 := by
43  rw [UInt32.toNat_sub_of_le]; · simp
44  rw [UInt32.le_iff_toNat_le]; simpa using h
45
46/-- **The loop of `slide_hash`** on one array: for `cnt >= 1` entries below the pointer, the loop does not fault and
47slides each of the first `cnt` entries; the rest of the array and every other table stay as they were. The result is
48the heap with the one block replaced. -/
49theorem slide_loop {h0 : Heap} {b : Nat} {a0 : Array UInt16} (w : UInt32) (cnt : Nat)
50    (hb : h0.words b = some a0) (hpos : 1 ≤ cnt) (hcs : cnt ≤ a0.size) (hc32 : cnt < 2 ^ 32) :
51    ∃ a : Array UInt16, cdoWhile (slBody w) slCond (UInt32.ofNat cnt, Ptr.ref (WRef.blk b) cnt) h0 =
52      .ok ((0, Ptr.ref (WRef.blk b) 0), { h0 with words := upd h0.words b (some a) }) ∧
53      a.size = a0.size ∧ ∀ i, wfn a i = if i < cnt then slideVal w (wfn a0 i) else wfn a0 i := by
54  let P : Nat → UInt32 × WPtr → Heap → Prop := fun k s h =>
55    s.1.toNat = k + 1 ∧ s.2 = Ptr.ref (WRef.blk b) (k + 1) ∧ k + 1 ≤ cnt ∧
56    ∃ a : Array UInt16, h = { h0 with words := upd h0.words b (some a) } ∧ a.size = a0.size ∧
57      ∀ i, wfn a i = if k + 1 ≤ i ∧ i < cnt then slideVal w (wfn a0 i) else wfn a0 i
58  let Q : UInt32 × WPtr → Heap → Prop := fun s h =>
59    s = (0, Ptr.ref (WRef.blk b) 0) ∧
60    ∃ a : Array UInt16, h = { h0 with words := upd h0.words b (some a) } ∧ a.size = a0.size ∧
61      ∀ i, wfn a i = if i < cnt then slideVal w (wfn a0 i) else wfn a0 i
62  -- one iteration of the body on a state satisfying the invariant for `k + 1` remaining iterations
63  have body : ∀ k (n : UInt32) (a : Array UInt16), n.toNat = k + 1 → k + 1 ≤ cnt → a.size = a0.size →
64      slBody w (n, Ptr.ref (WRef.blk b) (k + 1)) { h0 with words := upd h0.words b (some a) } =
65        .ok ((n, Ptr.ref (WRef.blk b) k), { h0 with words := upd h0.words b (some (a.set! k (slideVal w (wfn a k)))) }) := by
66    intro k n a hn hk hsz
67    have hg : Space.get ({ h0 with words := upd h0.words b (some a) } : Heap) (WRef.blk b) = some a := by simp
68    have hk' : k < a.size := by omega
69    have hp : psub (Ptr.ref (WRef.blk b) (k + 1)) 1 { h0 with words := upd h0.words b (some a) } =
70        .ok (Ptr.ref (WRef.blk b) k, { h0 with words := upd h0.words b (some a) }) := by
71      have := psub_ok' (h := { h0 with words := upd h0.words b (some a) }) (r := WRef.blk b) (a := a)
72        (off := k + 1) (n := 1) hg (by omega) (by omega)
73      simpa using this
74    have hl : Ptr.load (Ptr.ref (WRef.blk b) k) { h0 with words := upd h0.words b (some a) } =
75        .ok (a[k], { h0 with words := upd h0.words b (some a) }) :=
76      Ptr.load_ok (r := WRef.blk b) hg hk'
77    have hst := Ptr.store_ok (h := { h0 with words := upd h0.words b (some a) }) (r := WRef.blk b) (a := a)
78      (off := k) (v := slideVal w a[k]) hg (by simp) hk'
79    simp only [slBody, bind_app, hp, hl, slideVal_eq, hst, pure_app]
80    simp [wfn_getElem a k hk', upd_upd]
81  have hs := cdoWhile_run (σ := UInt32 × WPtr) (body := slBody w) (cond := slCond) (h := h0) P Q
82    (s := (UInt32.ofNat cnt, Ptr.ref (WRef.blk b) cnt)) (k := cnt - 1) ?_ ?_ ?_ ?_
83  · obtain ⟨s', h', hrun, hq⟩ := hs
84    obtain ⟨hs', a, hh', hsz, hw⟩ := hq
85    subst hs' hh'
86    exact ⟨a, hrun, hsz, hw⟩
87  · -- the step
88    intro k s h hP
89    obtain ⟨hn, hp, hkc, a, rfl, hsz, hw⟩ := hP
90    obtain ⟨n, p⟩ := s
91    simp only at hn hp
92    subst hp
93    have hb' := body (k + 1) n a hn hkc hsz
94    have hn1 : (n - 1).toNat = k + 1 := by rw [u32_sub_one_toNat n (by omega)]; omega
95    refine ⟨(n, Ptr.ref (WRef.blk b) (k + 1)),
96      { h0 with words := upd h0.words b (some (a.set! (k + 1) (slideVal w (wfn a (k + 1))))) },
97      (n - 1, Ptr.ref (WRef.blk b) (k + 1)),
98      { h0 with words := upd h0.words b (some (a.set! (k + 1) (slideVal w (wfn a (k + 1))))) }, hb', ?_, ?_⟩
99    · simp only [slCond, pure_app]
100      have : (n - 1 != 0) = true := by
101        simp only [bne_iff_ne, ne_eq]; intro h; rw [h] at hn1; simp at hn1
102      rw [this]
103    · refine ⟨hn1, rfl, by omega, a.set! (k + 1) (slideVal w (wfn a (k + 1))), rfl, by simp [hsz], ?_⟩
104      intro i
105      rw [wfn_set _ _ _ (by omega)]
106      by_cases hi : i = k + 1
107      · subst hi
108        rw [hw (k + 1)]
109        have : ¬ (k + 1 + 1 ≤ k + 1 ∧ k + 1 < cnt) := by omega
110        simp only [this, ite_false]
111        have : k + 1 ≤ k + 1 ∧ k + 1 < cnt := by omega
112        simp [this]
113      · rw [ite_eq_right hi, hw i]
114        by_cases h1 : k + 1 + 1 ≤ i ∧ i < cnt
115        · have : k + 1 ≤ i ∧ i < cnt := by omega
116          simp [h1, this]
117        · have : ¬ (k + 1 ≤ i ∧ i < cnt) := by omega
118          simp [h1, this]
119  · -- the last iteration
120    intro s h hP
121    obtain ⟨hn, hp, hkc, a, rfl, hsz, hw⟩ := hP
122    obtain ⟨n, p⟩ := s
123    simp only at hn hp
124    subst hp
125    have hb' := body 0 n a hn hkc hsz
126    have hn1 : (n - 1) = 0 := by
127      apply UInt32.toNat_inj.mp; rw [u32_sub_one_toNat n (by omega)]; simp; omega
128    refine ⟨(n, Ptr.ref (WRef.blk b) 0),
129      { h0 with words := upd h0.words b (some (a.set! 0 (slideVal w (wfn a 0)))) },
130      (0, Ptr.ref (WRef.blk b) 0),
131      { h0 with words := upd h0.words b (some (a.set! 0 (slideVal w (wfn a 0)))) }, hb', ?_, ?_⟩
132    · simp only [slCond, pure_app, hn1]
133      rfl
134    · refine ⟨rfl, a.set! 0 (slideVal w (wfn a 0)), rfl, by simp [hsz], ?_⟩
135      intro i
136      rw [wfn_set _ _ _ (by omega)]
137      by_cases hi : i = 0
138      · subst hi
139        rw [hw 0]
140        have : ¬ (0 + 1 ≤ 0 ∧ 0 < cnt) := by omega
141        simp only [this, ite_false]
142        have : 0 < cnt := by omega
143        simp [this]
144      · rw [ite_eq_right hi, hw i]
145        by_cases h1 : 0 + 1 ≤ i ∧ i < cnt
146        · simp [h1]
147        · have : ¬ (i < cnt) := by omega
148          simp [this]
149  · -- the start
150    have hn : (UInt32.ofNat cnt).toNat = cnt := by simp; omega
151    refine ⟨by rw [hn]; omega, ?_, by omega, a0, ?_, rfl, ?_⟩
152    · show Ptr.ref (WRef.blk b) cnt = Ptr.ref (WRef.blk b) (cnt - 1 + 1)
153      congr 1; omega
154    · rw [upd_self _ _ _ hb]
155    · intro i
156      have : ¬ (cnt - 1 + 1 ≤ i ∧ i < cnt) := by omega
157      simp [this]
158  · show cnt - 1 < 2 ^ 64
159    omega
160
161
162/-- **slide_hash, safety and exact effect.** For `head` a block of at least `hash_size >= 1` words and `prev` a different
163block of at least `w_size >= 1` words (with any content: `prev` is never cleared), `slide_hash` does not fault. Every
164entry `m` of `head[0 .. hash_size)` and of `prev[0 .. w_size)` becomes `m >= w_size ? m - w_size : 0`, the entries
165beyond stay as they were, and `slid` becomes 1. No other table, block or field changes. -/
166theorem slide_hash_ok {h : Heap} {sr hb pb : Nat} {d : DeflateState} {ha pa : Array UInt16}
167    (hd : h.dstates sr = some d) (hhead : d.head = .ref (.blk hb) 0) (hprev : d.prev = .ref (.blk pb) 0)
168    (hh : h.words hb = some ha) (hp : h.words pb = some pa) (hne : hb ≠ pb)
169    (h1 : d.hash_size.toNat ≤ ha.size) (h2 : d.w_size.toNat ≤ pa.size)
170    (hn1 : 1 ≤ d.hash_size.toNat) (hn2 : 1 ≤ d.w_size.toNat) :
171    ∃ ha' pa' : Array UInt16, slide_hash (some (.tab sr)) h = .ok ((), { h with
172      words := upd (upd h.words hb (some ha')) pb (some pa'),
173      dstates := upd h.dstates sr (some { d with slid := 1 }) }) ∧
174    ha'.size = ha.size ∧ pa'.size = pa.size ∧
175    (∀ i, wfn ha' i = if i < d.hash_size.toNat then slideVal d.w_size (wfn ha i) else wfn ha i) ∧
176    (∀ i, wfn pa' i = if i < d.w_size.toNat then slideVal d.w_size (wfn pa i) else wfn pa i) := by
177  have hh32 : d.hash_size.toNat < 2 ^ 32 := d.hash_size.toNat_lt
178  have hw32 : d.w_size.toNat < 2 ^ 32 := d.w_size.toNat_lt
179  obtain ⟨a1, hr1, hs1, hw1⟩ := slide_loop (h0 := h) (b := hb) (a0 := ha) d.w_size d.hash_size.toNat hh hn1 h1 hh32
180  obtain ⟨H1, hH1⟩ : ∃ x : Heap, x = { h with words := upd h.words hb (some a1) } := ⟨_, rfl⟩
181  rw [← hH1] at hr1
182  have hp1 : H1.words pb = some pa := by rw [hH1]; simp [upd_ne _ _ _ _ hne.symm, hp]
183  obtain ⟨a2, hr2, hs2, hw2⟩ := slide_loop (h0 := H1) (b := pb) (a0 := pa) d.w_size d.w_size.toNat hp1 hn2 h2 hw32
184  obtain ⟨H2, hH2⟩ : ∃ x : Heap, x = { H1 with words := upd H1.words pb (some a2) } := ⟨_, rfl⟩
185  rw [← hH2] at hr2
186  have hd2 : H2.dstates sr = some d := by rw [hH2, hH1]; exact hd
187  have e0 : ldDeflateState (some (.tab sr)) h = .ok (d, h) := ldDeflateState_tab hd
188  have e1 : padd d.head d.hash_size.toNat h = .ok (.ref (.blk hb) d.hash_size.toNat, h) := by
189    rw [hhead]
190    simpa using padd_ok' (h := h) (r := WRef.blk hb) (a := ha) (off := 0) (n := d.hash_size.toNat) hh (by omega)
191  have e2 : padd d.prev d.w_size.toNat H1 = .ok (.ref (.blk pb) d.w_size.toNat, H1) := by
192    rw [hprev]
193    simpa using padd_ok' (h := H1) (r := WRef.blk pb) (a := pa) (off := 0) (n := d.w_size.toNat) hp1 (by omega)
194  have e3 : ldDeflateState (some (.tab sr)) H2 = .ok (d, H2) := ldDeflateState_tab hd2
195  refine ⟨a1, a2, ?_, hs1, hs2, hw1, hw2⟩
196  rw [slide_hash_unfold]
197  rw [UInt32.ofNat_toNat] at hr1 hr2
198  simp only [bind_app, e0, e1, hr1, e2, hr2, wr, e3]
199  rw [stDeflateState_tab hd2]
200  simp [hH2, hH1]
201
202end Zlib.Deflate.Engine.Proofs