deflate.c.engine.chains.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.hash»
2
3/-!
4# deflate.c, engine: the hash-chain invariant H
5
6The tables `head` (`hash_size` entries) and `prev` (`w_size` entries) are functions `Nat → UInt16` (the content of
7the array, `0` outside; the proofs relating a heap array to its function are in the memory modules). Positions are
8window indices. `0` is `NIL`.
9
10**H.** A position `p ≠ 0` reachable from `head[k]` through `prev[p & wmask]` while the slot is still its own
11(`top <= p + w_size`, where `top` is one past the last inserted position) was inserted: `p < top`, its first three
12bytes lie below `lim` (the valid window data, `strstart + lookahead`) and hash to `k`, and `prev[p & wmask]` holds
13a smaller position. A slot that was never written is never followed, so the junk in a fresh `prev` is harmless.
14
15The theorems are `chains_insert` (one `INSERT_STRING`), `chains_slide` (`slide_hash` with the window copy),
16`chains_congr`/`chains_mono` (frames), and `chain_ok_of_chains` (the chain `longest_match` walks).
17-/
18
19namespace Zlib.Deflate.Engine.Proofs
20
21/-- Positions reachable in the hash table from `head[k]`, following `prev[p & wmask]` from every reached
22`p ≠ 0` whose slot cannot have been reused yet (`top <= p + ws`). -/
23inductive Reach (head prev : Nat → UInt16) (ws top k : Nat) : Nat → Prop
24  | head : Reach head prev ws top k (head k).toNat
25  | step {p : Nat} : Reach head prev ws top k p → p ≠ 0 → top ≤ p + ws →
26      Reach head prev ws top k (prev (p &&& (ws - 1))).toNat
27
28/-- **H, the hash-chain invariant.** -/
29structure HashChains (head prev : Nat → UInt16) (w : Nat → UInt8) (n hsh hm : UInt32)
30    (ws top lim : Nat) : Prop where
31  node : ∀ k p, k < n.toNat → Reach head prev ws top k p → p ≠ 0 → top ≤ p + ws →
32    p < top ∧ p + 3 ≤ lim ∧ (hkey hsh hm w p).toNat = k ∧ (prev (p &&& (ws - 1))).toNat < p
33
34theorem reach_congr {h1 p1 h2 p2 : Nat → UInt16} {ws top k p : Nat}
35    (hH : ∀ i, h2 i = h1 i) (hP : ∀ i, p2 i = p1 i)
36    (hr : Reach h2 p2 ws top k p) : Reach h1 p1 ws top k p := by
37  induction hr with
38  | head => rw [hH]; exact Reach.head
39  | step _ hp ht ih => rw [hP]; exact Reach.step ih hp ht
40
41/-- Writes outside `head`/`prev`, and window changes at or beyond `lim`, keep the invariant. -/
42theorem chains_congr {h1 p1 h2 p2 : Nat → UInt16} {w w' : Nat → UInt8} {n hsh hm : UInt32}
43    {ws top lim : Nat} (hc : HashChains h1 p1 w n hsh hm ws top lim)
44    (hH : ∀ i, h2 i = h1 i) (hP : ∀ i, p2 i = p1 i)
45    (hw : ∀ i, i < lim → w' i = w i) : HashChains h2 p2 w' n hsh hm ws top lim := by
46  refine ⟨fun k p hk hr hp ht => ?_⟩
47  obtain ⟨a1, a2, a3, a4⟩ := hc.node k p hk (reach_congr hH hP hr) hp ht
48  refine ⟨a1, a2, ?_, by rw [hP]; exact a4⟩
49  rw [hkey_congr (w := w) (p := p) (fun j hj => hw _ (by omega))]; exact a3
50
51theorem reach_mono {h1 p1 : Nat → UInt16} {ws top top' k p : Nat} (ht : top ≤ top')
52    (hr : Reach h1 p1 ws top' k p) : Reach h1 p1 ws top k p := by
53  induction hr with
54  | head => exact Reach.head
55  | step _ hp ht' ih => exact Reach.step ih hp (by omega)
56
57/-- A larger `top` or `lim` keeps the invariant. -/
58theorem chains_mono {h1 p1 : Nat → UInt16} {w : Nat → UInt8} {n hsh hm : UInt32}
59    {ws top lim top' lim' : Nat} (hc : HashChains h1 p1 w n hsh hm ws top lim)
60    (ht : top ≤ top') (hl : lim ≤ lim') : HashChains h1 p1 w n hsh hm ws top' lim' := by
61  refine ⟨fun k p hk hr hp ht' => ?_⟩
62  obtain ⟨a1, a2, a3, a4⟩ := hc.node k p hk (reach_mono ht hr) hp (by omega)
63  exact ⟨by omega, by omega, a3, a4⟩
64
65/-- A non-NIL head entry is below `top`. -/
66theorem head_lt {h1 p1 : Nat → UInt16} {w : Nat → UInt8} {n hsh hm : UInt32} {ws top lim : Nat}
67    (hc : HashChains h1 p1 w n hsh hm ws top lim) {k : Nat} (hk : k < n.toNat)
68    (h0 : (h1 k).toNat ≠ 0) : (h1 k).toNat < top := by
69  by_cases ht : top ≤ (h1 k).toNat + ws
70  · exact (hc.node k _ hk Reach.head h0 ht).1
71  · omega
72
73/-- **INSERT_STRING keeps the invariant.** Inserting position `str >= top` with key `x = hkey str` (its three
74bytes below `lim`): `prev[str & wmask] = head[x]` (`u`), `head[x] = str`. The result satisfies H with
75`top := str + 1`. -/
76theorem chains_insert {h1 p1 h2 p2 : Nat → UInt16} {w : Nat → UInt8} {n hsh hm : UInt32}
77    {ws top lim b : Nat} (hc : HashChains h1 p1 w n hsh hm ws top lim) (hb2 : ws = 2 ^ b)
78    {str x : Nat} {s16 : UInt16} (htop : top ≤ str) (hlim : str + 3 ≤ lim)
79    (hx : (hkey hsh hm w str).toNat = x) (hxn : x < n.toNat)
80    (hs16 : s16.toNat = str)
81    (hH : ∀ i, h2 i = if i = x then s16 else h1 i)
82    (hP : ∀ i, p2 i = if i = str &&& (ws - 1) then h1 x else p1 i) :
83    HashChains h2 p2 w n hsh hm ws (str + 1) lim := by
84  have hws : 0 < ws := by subst hb2; exact Nat.two_pow_pos b
85  have A : ∀ k p, k < n.toNat → Reach h2 p2 ws (str + 1) k p →
86      (k = x ∧ p = str) ∨ Reach h1 p1 ws top k p := by
87    intro k p hk hr
88    induction hr with
89    | head =>
90      rw [hH]
91      split
92      · rename_i e; exact Or.inl ⟨e, hs16⟩
93      · exact Or.inr Reach.head
94    | @step p _ hp ht ih =>
95      rcases ih with ⟨rfl, rfl⟩ | hr
96      · rw [hP, ite_eq_left rfl]
97        exact Or.inr Reach.head
98      · have hpt := (hc.node k p hk hr hp (by omega)).1
99        rw [hP, ite_eq_right (and_wm_ne hb2 (by omega) (by omega))]
100        exact Or.inr (Reach.step hr hp (by omega))
101  refine ⟨fun k p hk hr hp ht => ?_⟩
102  rcases A k p hk hr with ⟨rfl, rfl⟩ | hr0
103  · refine ⟨by omega, hlim, hx, ?_⟩
104    rw [hP, ite_eq_left rfl]
105    by_cases hu0 : (h1 k).toNat = 0
106    · omega
107    · have := head_lt hc hxn hu0; omega
108  · obtain ⟨a1, a2, a3, a4⟩ := hc.node k p hk hr0 hp (by omega)
109    refine ⟨by omega, a2, a3, ?_⟩
110    rw [hP, ite_eq_right (and_wm_ne hb2 (by omega) (by omega))]; exact a4
111
112/-! ## Sliding -/
113
114/-- The value `slide_hash` stores for an entry `m`: `m >= wsize ? m - wsize : NIL`. -/
115def slideVal (w : UInt32) (m : UInt16) : UInt16 :=
116  (if m.toUInt32 >= w then m.toUInt32 - w else 0).toUInt16
117
118theorem slideVal_toNat (w : UInt32) (m : UInt16) (hw : w.toNat ≤ 65536) :
119    (slideVal w m).toNat = if w.toNat ≤ m.toNat then m.toNat - w.toNat else 0 := by
120  unfold slideVal
121  have hm := m.toNat_lt
122  by_cases hge : m.toUInt32 >= w
123  · rw [ite_eq_left hge]
124    have h' : w.toNat ≤ m.toNat := by
125      rw [GE.ge, UInt32.le_iff_toNat_le] at hge; simpa using hge
126    rw [ite_eq_left h']
127    simp only [UInt32.toNat_toUInt16]
128    rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simpa using h')]
129    simp; omega
130  · rw [ite_eq_right hge]
131    have h' : ¬ w.toNat ≤ m.toNat := by
132      rw [GE.ge, UInt32.le_iff_toNat_le] at hge; simpa using hge
133    rw [ite_eq_right h']; rfl
134
135/-- **slide_hash keeps the invariant** (with the window copy of `fill_window`): if every `head` entry and every
136`prev` entry is slid by `w = w_size` and window bytes `i < lim - w` are the old bytes `i + w`, H holds with `top`
137and `lim` lowered by `w`; positions below `w` became NIL. -/
138theorem chains_slide {h1 p1 h2 p2 : Nat → UInt16} {w w' : Nat → UInt8} {n hsh hm ws : UInt32}
139    {top lim b : Nat} (hc : HashChains h1 p1 w n hsh hm ws.toNat top lim)
140    (hb2 : ws.toNat = 2 ^ b) (hw16 : ws.toNat ≤ 65536)
141    (hH : ∀ i, i < n.toNat → h2 i = slideVal ws (h1 i))
142    (hP : ∀ i, i < ws.toNat → p2 i = slideVal ws (p1 i))
143    (hw : ∀ i, i + ws.toNat < lim → w' i = w (i + ws.toNat)) :
144    HashChains h2 p2 w' n hsh hm ws.toNat (top - ws.toNat) (lim - ws.toNat) := by
145  have B : ∀ k p, k < n.toNat → Reach h2 p2 ws.toNat (top - ws.toNat) k p → p ≠ 0 →
146      Reach h1 p1 ws.toNat top k (p + ws.toNat) := by
147    intro k p hk hr
148    induction hr with
149    | head =>
150      intro hv0
151      have := slideVal_toNat ws (h1 k) hw16
152      rw [← hH k hk] at this
153      split at this
154      · rw [show (h2 k).toNat + ws.toNat = (h1 k).toNat by omega]; exact Reach.head
155      · omega
156    | @step p _ hp ht ih =>
157      intro hv0
158      have hr1 := ih hp
159      obtain ⟨-, -, -, hvv⟩ := hc.node k _ hk hr1 (by omega) (by omega)
160      rw [and_wm_add hb2] at hvv
161      have := slideVal_toNat ws (p1 (p &&& (ws.toNat - 1))) hw16
162      rw [← hP _ (and_wm_lt hb2 p)] at this
163      split at this
164      · rw [show (p2 (p &&& (ws.toNat - 1))).toNat + ws.toNat = (p1 (p &&& (ws.toNat - 1))).toNat by omega]
165        have := Reach.step (p := p + ws.toNat) hr1 (by omega) (by omega)
166        rw [and_wm_add hb2] at this
167        exact this
168      · omega
169  refine ⟨fun k p hk hr hp ht => ?_⟩
170  have hr1 := B k p hk hr hp
171  obtain ⟨h1', h2', h3, hvv⟩ := hc.node k _ hk hr1 (by omega) (by omega)
172  refine ⟨by omega, by omega, ?_, ?_⟩
173  · rw [hkey_congr (w := w) (p := p + ws.toNat) (fun j hj => by
174      rw [hw _ (by omega)]; congr 1; omega)]; exact h3
175  · rw [and_wm_add hb2] at hvv
176    rw [hP _ (and_wm_lt hb2 p), slideVal_toNat ws _ hw16]
177    split <;> omega
178
179/-! ## The chain read by `longest_match` -/
180
181/-- `limit` of `longest_match`: `strstart > MAX_DIST ? strstart - MAX_DIST : NIL`. -/
182def lmLimit (ss md : Nat) : Nat := if ss > md then ss - md else 0
183
184/-- Positions visited by the hash chain from `cur`: `cur`, then each `prev[p & wmask]` while it exceeds `limit`. -/
185inductive Chain (prev : Nat → UInt16) (wm limit cur : Nat) : Nat → Prop
186  | start : Chain prev wm limit cur cur
187  | step {p q : Nat} : Chain prev wm limit cur p → q = (prev (p &&& wm)).toNat → limit < q →
188      Chain prev wm limit cur q
189
190/-- **The chain invariant gives what `longest_match` needs.** Right after `INSERT_STRING` at `ss`
191(`head[x] = ss`, `prev[ss & wmask] = c`, the old head) with H at `top = ss + 1`, every position on the chain
192`longest_match` walks from `c` (`1 <= c`, `ss - c <= MAX_DIST`) is in `[1, ss)` and agrees with `ss` in its third
193byte whenever it agrees in the first two. -/
194theorem chain_ok_of_chains {h1 p1 : Nat → UInt16} {w : Nat → UInt8} {n hsh hm : UInt32}
195    {ws lim ss x c : Nat} (prm : HashParams n hsh hm)
196    (hc : HashChains h1 p1 w n hsh hm ws (ss + 1) lim)
197    (hx : (hkey hsh hm w ss).toNat = x) (hxn : x < n.toNat)
198    (hhead : (h1 x).toNat = ss)
199    (hu : (p1 (ss &&& (ws - 1))).toNat = c)
200    (hc1 : 1 ≤ c) (hcs : c < ss) (hdist : ss - c ≤ ws - 262) :
201    ∀ p, Chain p1 (ws - 1) (lmLimit ss (ws - 262)) c p →
202      1 ≤ p ∧ p < ss ∧ (p1 (p &&& (ws - 1))).toNat < p ∧
203      (w p = w ss → w (p + 1) = w (ss + 1) → w (p + 2) = w (ss + 2)) := by
204  have r0 : Reach h1 p1 ws (ss + 1) x ss := hhead ▸ Reach.head
205  have rc : Reach h1 p1 ws (ss + 1) x c := hu ▸ Reach.step r0 (by omega) (by omega)
206  have C : ∀ p, Chain p1 (ws - 1) (lmLimit ss (ws - 262)) c p →
207      Reach h1 p1 ws (ss + 1) x p ∧ p ≠ 0 ∧ ss + 1 ≤ p + ws ∧ p ≤ c := by
208    intro p hp
209    induction hp with
210    | start => exact ⟨rc, by omega, by omega, Nat.le_refl _⟩
211    | @step p q _ hq hlim ih =>
212      obtain ⟨hr, hp0, hpw, hpc⟩ := ih
213      obtain ⟨-, -, -, hlt⟩ := hc.node x p hxn hr hp0 hpw
214      subst hq
215      refine ⟨Reach.step hr hp0 hpw, by unfold lmLimit at hlim; split at hlim <;> omega, ?_, by omega⟩
216      unfold lmLimit at hlim; split at hlim <;> omega
217  intro p hp
218  obtain ⟨hr, hp0, hpw, hpc⟩ := C p hp
219  obtain ⟨-, -, hk, hlt⟩ := hc.node x p hxn hr hp0 hpw
220  exact ⟨by omega, by omega, hlt, fun e0 e1 => hkey_third prm (by rw [hk, hx]) e0 e1⟩
221
222end Zlib.Deflate.Engine.Proofs