deflate.c.engine.match.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1/-!
2# deflate.c, engine: the match length of `longest_match`
3
4For a candidate match at window position `C` and the string at `S = strstart`, `longest_match` first compares
5`match[best_len]`, `match[best_len - 1]`, `match[0]`, `match[1]` with the scan; if all agree it assumes
6`match[2] = scan[2]` (the hash chain guarantees this, `hkey_third`) and compares from index 3 on, up to `MAX_MATCH = 258`.
7The unrolled loop compares eight positions per round and stops at the first mismatch or at `strend = S + 258`.
8The length is `258 - (strend - scan)`, that is the scan offset at which the loop stopped.
9
10`firstMis w S C j` is that offset when the loop is at offset `j - 1` and no position below `j` is known to
11differ: the first `k >= j` below 258 where the two strings differ, or 258. `firstMis_spec` is the characterisation
12the heap proof of the loop maintains step by step.
13-/
14
15namespace Zlib.Deflate.Engine.Proofs
16
17/-- The first `k` with `j <= k < 258` where `w (S + k) != w (C + k)`, or `258` when there is none. -/
18def firstMis (w : Nat → UInt8) (S C j : Nat) : Nat :=
19  if h : j < 258 then (if w (S + j) = w (C + j) then firstMis w S C (j + 1) else j) else 258
20termination_by 258 - j
21
22theorem firstMis_ge (w : Nat → UInt8) (S C : Nat) : ∀ n j, 258 - j = n → j ≤ 258 → j ≤ firstMis w S C j := by
23  intro n
24  induction n using Nat.strongRecOn with
25  | _ n ih =>
26    intro j hn hj
27    unfold firstMis
28    split
29    · rename_i h
30      split
31      · have := ih (258 - (j + 1)) (by omega) (j + 1) rfl (by omega)
32        omega
33      · omega
34    · omega
35
36theorem firstMis_le (w : Nat → UInt8) (S C : Nat) : ∀ n j, 258 - j = n → firstMis w S C j ≤ 258 := by
37  intro n
38  induction n using Nat.strongRecOn with
39  | _ n ih =>
40    intro j hn
41    unfold firstMis
42    split
43    · rename_i h
44      split
45      · exact ih (258 - (j + 1)) (by omega) (j + 1) rfl
46      · omega
47    · omega
48
49/-- The characterisation of `firstMis`: the strings agree on `[j, r)` and, when `r < 258`, differ at `r`. -/
50theorem firstMis_spec (w : Nat → UInt8) (S C : Nat) : ∀ n j, 258 - j = n → j ≤ 258 →
51    (∀ k, j ≤ k → k < firstMis w S C j → w (S + k) = w (C + k)) ∧
52    (firstMis w S C j < 258 → w (S + firstMis w S C j) ≠ w (C + firstMis w S C j)) := by
53  intro n
54  induction n using Nat.strongRecOn with
55  | _ n ih =>
56    intro j hn hj
57    have e : firstMis w S C j = if j < 258 then (if w (S + j) = w (C + j) then firstMis w S C (j + 1) else j) else 258 := by
58      rw [firstMis]; rfl
59    by_cases h : j < 258
60    · by_cases hw : w (S + j) = w (C + j)
61      · have e2 : firstMis w S C j = firstMis w S C (j + 1) := by rw [e]; simp [h, hw]
62        obtain ⟨a, b⟩ := ih (258 - (j + 1)) (by omega) (j + 1) rfl (by omega)
63        rw [e2]
64        refine ⟨fun k hk1 hk2 => ?_, b⟩
65        by_cases hkj : k = j
66        · subst hkj; exact hw
67        · exact a k (by omega) hk2
68      · have e2 : firstMis w S C j = j := by rw [e]; simp [h, hw]
69        rw [e2]
70        exact ⟨fun k hk1 hk2 => by omega, fun _ => hw⟩
71    · have e2 : firstMis w S C j = 258 := by rw [e]; simp [h]
72      rw [e2]
73      exact ⟨fun k hk1 hk2 => by omega, fun h' => by omega⟩
74
75/-- The scan offset the loop reaches is determined by agreement below it and disagreement at it: if the strings
76agree on `[j, r)`, `j <= r <= 258`, and differ at `r` when `r < 258`, then `r = firstMis j`. -/
77theorem firstMis_unique (w : Nat → UInt8) (S C : Nat) {j r : Nat} (hj : j ≤ r) (hr : r ≤ 258)
78    (hag : ∀ k, j ≤ k → k < r → w (S + k) = w (C + k)) (hst : r < 258 → w (S + r) ≠ w (C + r)) :
79    firstMis w S C j = r := by
80  obtain ⟨a, b⟩ := firstMis_spec w S C _ j rfl (by omega)
81  have hge := firstMis_ge w S C _ j rfl (by omega)
82  have hle := firstMis_le w S C _ j rfl
83  refine Classical.byContradiction fun hne => ?_
84  rcases Nat.lt_or_gt_of_ne hne with hlt | hgt
85  · exact b (by omega) (hag _ hge hlt)
86  · by_cases h258 : r < 258
87    · exact hst h258 (a r hj hgt)
88    · omega
89
90/-- The length that `longest_match` computes for a candidate that passed the four early tests and whose third
91byte agrees: `firstMis` from index 3. It is at least 3 and at most 258, and the strings agree on `[0, len)`
92given they agree on `[0, 3)`. -/
93def matchLen (w : Nat → UInt8) (S C : Nat) : Nat := firstMis w S C 3
94
95theorem matchLen_bounds (w : Nat → UInt8) (S C : Nat) : 3 ≤ matchLen w S C ∧ matchLen w S C ≤ 258 :=
96  ⟨firstMis_ge w S C _ 3 rfl (by omega), firstMis_le w S C _ 3 rfl⟩
97
98/-- If the strings at `S` and `C` agree on the first three bytes, they agree on `[0, matchLen)`: the bytes before the
99first position from index 3 on where they differ (or 258). -/
100theorem matchLen_agree (w : Nat → UInt8) (S C : Nat)
101    (h0 : w S = w C) (h1 : w (S + 1) = w (C + 1)) (h2 : w (S + 2) = w (C + 2)) :
102    ∀ j, j < matchLen w S C → w (S + j) = w (C + j) := by
103  intro j hj
104  by_cases h3 : j < 3
105  · obtain h | h | h : j = 0 ∨ j = 1 ∨ j = 2 := by omega
106    · subst h; simpa using h0
107    · subst h; exact h1
108    · subst h; exact h2
109  · exact (firstMis_spec w S C _ 3 rfl (by omega)).1 j (by omega) hj
110
111theorem matchLen_stop (w : Nat → UInt8) (S C : Nat) (h : matchLen w S C < 258) :
112    w (S + matchLen w S C) ≠ w (C + matchLen w S C) :=
113  (firstMis_spec w S C _ 3 rfl (by omega)).2 h
114
115/-! ## The best length
116
117`best_len` only grows, and only to a length the loop measured. The cap at `lookahead` at the end keeps a
118returned length below the valid data. -/
119
120/-- The result `longest_match` returns: `best_len` if it is at most `lookahead`, else `lookahead`. -/
121def lmResult (best la : Nat) : Nat := if best ≤ la then best else la
122
123theorem lmResult_le (best la : Nat) : lmResult best la ≤ best ∧ lmResult best la ≤ la := by
124  unfold lmResult; split <;> omega
125
126end Zlib.Deflate.Engine.Proofs