deflate.c.engine.hash.lean

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

1/-!
2# deflate.c, engine: the rolling hash and the window arithmetic
3
4Statements about numbers and byte functions that the proofs of `UPDATE_HASH`, `INSERT_STRING`, `fill_window` and
5`longest_match` use. Nothing here mentions the heap or the translation. A window is a function `Nat → UInt8`
6(the content of the window block, read with `getD` outside the block).
7
8Copied from the earlier attempt (`EngineChains`), with the byte array replaced by a byte function.
9-/
10
11namespace Zlib.Deflate.Engine.Proofs
12
13/-- `UPDATE_HASH(s, h, c)`: `((h << hash_shift) ^ c) & hash_mask` on `unsigned`. -/
14def updHash (hsh hm x : UInt32) (c : UInt8) : UInt32 :=
15  ((x <<< hsh) ^^^ c.toUInt32) &&& hm
16
17/-- The hash key of the string at window position `p`: three `UPDATE_HASH` steps from 0. -/
18def hkey (hsh hm : UInt32) (w : Nat → UInt8) (p : Nat) : UInt32 :=
19  updHash hsh hm (updHash hsh hm (updHash hsh hm 0 (w p)) (w (p + 1))) (w (p + 2))
20
21/-- The hash parameters `deflateInit2_` sets: `hash_bits = memLevel + 7` in `8 .. 16`,
22`hash_size = 1 << hash_bits`, `hash_mask = hash_size - 1`, `hash_shift = (hash_bits + 2) / 3`
23(so `3 * hash_shift >= hash_bits`). -/
24structure HashParams (n hsh hm : UInt32) : Prop where
25  bits : ∃ k, 8 ≤ k ∧ k ≤ 16 ∧ n.toNat = 2 ^ k ∧ hm.toNat = 2 ^ k - 1 ∧ k ≤ 3 * hsh.toNat
26  hsh_lt : hsh.toNat < 32
27
28/-- `ins_h` holds a running hash whose last two inputs were the bytes at `p` and `p + 1`. -/
29def InsHForm (hsh hm : UInt32) (w : Nat → UInt8) (p : Nat) (x : UInt32) : Prop :=
30  ∃ z, x = updHash hsh hm (updHash hsh hm z (w p)) (w (p + 1))
31
32theorem bit_upd (hsh hm x : UInt32) (c : UInt8) (i : Nat) :
33    (updHash hsh hm x c).toNat.testBit i =
34      (hm.toNat.testBit i && ((decide (i < 32) && decide (hsh.toNat % 32 ≤ i) &&
35        x.toNat.testBit (i - hsh.toNat % 32)) ^^ c.toNat.testBit i)) := by
36  unfold updHash
37  simp only [UInt32.toNat_and, UInt32.toNat_xor, UInt32.toNat_shiftLeft, Nat.testBit_and,
38    Nat.testBit_xor, UInt8.toNat_toUInt32]
39  rw [Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft]
40  simp only [ge_iff_le, Bool.and_assoc]
41  exact Bool.and_comm _ _
42
43/-- Three `UPDATE_HASH` steps do not depend on the starting value when `hash_mask = 2^k - 1` and
44`3 * hash_shift >= k`. -/
45theorem upd3_indep {hsh hm : UInt32} {k : Nat} (hk : hm.toNat = 2 ^ k - 1)
46    (hks : k ≤ 3 * hsh.toNat) (hs : hsh.toNat < 32) (z : UInt32) (a b c : UInt8) :
47    updHash hsh hm (updHash hsh hm (updHash hsh hm z a) b) c =
48      updHash hsh hm (updHash hsh hm (updHash hsh hm 0 a) b) c := by
49  apply UInt32.toNat_inj.mp
50  apply Nat.eq_of_testBit_eq
51  intro i
52  have hs' : hsh.toNat % 32 = hsh.toNat := Nat.mod_eq_of_lt hs
53  simp only [bit_upd, hk, Nat.testBit_two_pow_sub_one, hs', UInt32.toNat_zero, Nat.zero_testBit]
54  by_cases hi : i < k
55  · have : ¬ (hsh.toNat ≤ i - hsh.toNat - hsh.toNat) := by omega
56    simp [this]
57  · simp [hi]
58
59/-- With at least 8 hash bits, the last byte of an update is determined by the result. -/
60theorem upd_inj {hsh hm : UInt32} {k : Nat} (hk : hm.toNat = 2 ^ k - 1) (h8 : 8 ≤ k)
61    (y : UInt32) (c d : UInt8) (he : updHash hsh hm y c = updHash hsh hm y d) : c = d := by
62  apply UInt8.toNat_inj.mp
63  apply Nat.eq_of_testBit_eq
64  intro i
65  have := congrArg (fun v => v.toNat.testBit i) he
66  simp only [bit_upd, hk, Nat.testBit_two_pow_sub_one] at this
67  by_cases hi : i < 8
68  · have hik : i < k := by omega
69    simp only [hik, decide_true, Bool.true_and] at this
70    exact (Bool.xor_right_inj).mp this
71  · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le c.toNat_lt
72        (Nat.pow_le_pow_right (by decide) (by omega))),
73      Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le d.toNat_lt
74        (Nat.pow_le_pow_right (by decide) (by omega)))]
75
76/-- `UPDATE_HASH` from 0 with byte `c` gives `c` (at least 8 hash bits): the `s->ins_h = s->window[str]`
77initialisation of `fill_window` and `deflate_fast`. -/
78theorem upd_zero {hsh hm : UInt32} {k : Nat} (hk : hm.toNat = 2 ^ k - 1) (h8 : 8 ≤ k)
79    (c : UInt8) : updHash hsh hm 0 c = c.toUInt32 := by
80  apply UInt32.toNat_inj.mp
81  apply Nat.eq_of_testBit_eq
82  intro i
83  simp only [bit_upd, hk, Nat.testBit_two_pow_sub_one, UInt32.toNat_zero, Nat.zero_testBit,
84    Bool.and_false, Bool.false_xor, UInt8.toNat_toUInt32]
85  by_cases hi : i < 8
86  · have hik : i < k := by omega
87    simp [hik]
88  · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le c.toNat_lt
89        (Nat.pow_le_pow_right (by decide) (by omega)))]
90    simp
91
92theorem upd_le (hsh hm x : UInt32) (c : UInt8) : (updHash hsh hm x c).toNat ≤ hm.toNat := by
93  unfold updHash; rw [UInt32.toNat_and]; exact Nat.and_le_right
94
95/-- Every key is below `hash_size`: `head[ins_h]` is in bounds. -/
96theorem hkey_lt {n hsh hm : UInt32} (prm : HashParams n hsh hm) (w : Nat → UInt8) (p : Nat) :
97    (hkey hsh hm w p).toNat < n.toNat := by
98  obtain ⟨k, -, -, hn, hk, -⟩ := prm.bits
99  have := upd_le hsh hm (updHash hsh hm (updHash hsh hm 0 (w p)) (w (p + 1))) (w (p + 2))
100  have : 0 < 2 ^ k := Nat.two_pow_pos k
101  unfold hkey; omega
102
103/-- Every `UPDATE_HASH` result is below `hash_size` (so is `ins_h` after any update). -/
104theorem updHash_lt {n hsh hm : UInt32} (prm : HashParams n hsh hm) (x : UInt32) (c : UInt8) :
105    (updHash hsh hm x c).toNat < n.toNat := by
106  obtain ⟨k, -, -, hn, hk, -⟩ := prm.bits
107  have := upd_le hsh hm x c
108  have : 0 < 2 ^ k := Nat.two_pow_pos k
109  omega
110
111/-- The next update of a primed `ins_h` gives the key of `p`. -/
112theorem hkey_of_form {n hsh hm : UInt32} (prm : HashParams n hsh hm) {w : Nat → UInt8} {p : Nat}
113    {x : UInt32} (hf : InsHForm hsh hm w p x) : updHash hsh hm x (w (p + 2)) = hkey hsh hm w p := by
114  obtain ⟨k, -, -, -, hk, hks⟩ := prm.bits
115  obtain ⟨z, rfl⟩ := hf
116  unfold hkey
117  exact upd3_indep hk hks prm.hsh_lt z _ _ _
118
119/-- After that update, `ins_h` is primed for `p + 1`. -/
120theorem form_next {hsh hm : UInt32} {w : Nat → UInt8} {p : Nat} {x : UInt32}
121    (hf : InsHForm hsh hm w p x) : InsHForm hsh hm w (p + 1) (updHash hsh hm x (w (p + 2))) := by
122  obtain ⟨z, rfl⟩ := hf
123  exact ⟨updHash hsh hm z (w p), rfl⟩
124
125/-- `s->ins_h = s->window[p]; UPDATE_HASH(s, s->ins_h, s->window[p + 1])` primes `ins_h`. -/
126theorem form_init {n hsh hm : UInt32} (prm : HashParams n hsh hm) (w : Nat → UInt8) (p : Nat) :
127    InsHForm hsh hm w p (updHash hsh hm (w p).toUInt32 (w (p + 1))) := by
128  obtain ⟨k, h8, -, -, hk, -⟩ := prm.bits
129  exact ⟨0, by rw [upd_zero hk h8]⟩
130
131/-- A primed `ins_h` only depends on the two bytes at `p`, `p + 1`. -/
132theorem form_congr {hsh hm : UInt32} {w w' : Nat → UInt8} {p p' : Nat} {x : UInt32}
133    (hf : InsHForm hsh hm w p x) (h0 : w' p' = w p) (h1 : w' (p' + 1) = w (p + 1)) :
134    InsHForm hsh hm w' p' x := by
135  obtain ⟨z, rfl⟩ := hf
136  exact ⟨z, by rw [h0, h1]⟩
137
138/-- Equal keys and equal first two bytes give an equal third byte: `longest_match` need not compare `scan[2]`. -/
139theorem hkey_third {n hsh hm : UInt32} (prm : HashParams n hsh hm) {w : Nat → UInt8} {p q : Nat}
140    (hk : (hkey hsh hm w p).toNat = (hkey hsh hm w q).toNat)
141    (h0 : w p = w q) (h1 : w (p + 1) = w (q + 1)) : w (p + 2) = w (q + 2) := by
142  obtain ⟨k, h8, -, -, hmk, -⟩ := prm.bits
143  have he := UInt32.toNat_inj.mp hk
144  unfold hkey at he
145  rw [h0, h1] at he
146  exact upd_inj hmk h8 _ _ _ he
147
148/-- The key only depends on the three bytes at `p`. -/
149theorem hkey_congr {hsh hm : UInt32} {w w' : Nat → UInt8} {p p' : Nat}
150    (h : ∀ j, j < 3 → w' (p' + j) = w (p + j)) : hkey hsh hm w' p' = hkey hsh hm w p := by
151  unfold hkey
152  have e0 := h 0 (by decide); have e1 := h 1 (by decide); have e2 := h 2 (by decide)
153  simp only [Nat.add_zero] at e0
154  rw [e0, e1, e2]
155
156/-! ## The prev slot of a position -/
157
158theorem and_wm_mod {ws b : Nat} (hb : ws = 2 ^ b) (p : Nat) : p &&& (ws - 1) = p % ws := by
159  subst hb; exact Nat.and_two_pow_sub_one_eq_mod p b
160
161theorem and_wm_lt {ws b : Nat} (hb : ws = 2 ^ b) (p : Nat) : p &&& (ws - 1) < ws := by
162  rw [and_wm_mod hb]; exact Nat.mod_lt _ (by subst hb; exact Nat.two_pow_pos b)
163
164theorem and_wm_add {ws b : Nat} (hb : ws = 2 ^ b) (p : Nat) :
165    (p + ws) &&& (ws - 1) = p &&& (ws - 1) := by
166  rw [and_wm_mod hb, and_wm_mod hb, Nat.add_mod_right]
167
168/-- Two positions less than `ws` apart use different `prev` slots. -/
169theorem and_wm_ne {ws b : Nat} (hb : ws = 2 ^ b) {p q : Nat} (hpq : p < q) (hq : q < p + ws) :
170    p &&& (ws - 1) ≠ q &&& (ws - 1) := by
171  rw [and_wm_mod hb, and_wm_mod hb]
172  intro he
173  have h1 : (q - p) % ws = 0 := Nat.sub_mod_eq_zero_of_mod_eq he.symm
174  have h2 := Nat.le_of_dvd (by omega) (Nat.dvd_of_mod_eq_zero h1)
175  omega
176
177end Zlib.Deflate.Engine.Proofs