deflate.c.engine.window.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 window arithmetic of `fill_window` and `longest_match`
3
4Statements about natural numbers. `ws` is `w_size` (512 to 32768, a power of two), the window has `2 * ws` bytes,
5`ss` is `strstart`, `la` is `lookahead`, `MIN_LOOKAHEAD = 262`, `MAX_DIST = ws - 262`, `MAX_MATCH = 258`.
6
7**D**, the window range: `ss + la <= 2 * ws`.
8
9These are the numeric facts of `docs/proof/deflate.md` section 3: the slide test, the slide copy, the room left
10after `fill_window`, the `high_water` clearing, and the margins that keep every read of `longest_match` inside the
11window.
12-/
13
14namespace Zlib.Deflate.Engine.Proofs
15
16/-! ## The slide of `fill_window` -/
17
18/-- The amount `fill_window` slides by: `ws` when `strstart >= ws + MAX_DIST = 2 * ws - 262`, else `0`. -/
19def fillD (ws ss : Nat) : Nat := if 2 * ws - 262 ≤ ss then ws else 0
20
21/-- The number of bytes `fill_window` reads when `a` bytes of input are available: the first pass reads
22`MIN(avail_in, more)` with `more = window_size - lookahead - strstart'`. (Later passes of the `do` loop read
23further bytes only while `lookahead < MIN_LOOKAHEAD`; this is the first pass.) -/
24def fillL (ws la ss a : Nat) : Nat := min a (2 * ws - la - (ss - fillD ws ss))
25
26/-- `insert` after one pass of `fill_window`: the slide clamps it to `strstart' = ss - D`; if bytes were read and
27`lookahead' + insert >= MIN_MATCH` the insertion loop runs until `insert = 0` or `lookahead' + insert < MIN_MATCH`,
28leaving `MIN_MATCH - 1 - lookahead'` (truncated at 0). -/
29def fillIns (ins ss D la L : Nat) : Nat :=
30  if L = 0 ∨ la + L + min ins (ss - D) < 3 then min ins (ss - D) else 2 - (la + L)
31
32/-- `high_water` after `fill_window` (`W = window_size`, `curr = strstart + lookahead` after the read): when
33below `W` it is raised to at least `MIN(curr + WIN_INIT, W)`. -/
34def fillHW (hw W curr : Nat) : Nat := if hw < W then max hw (min (curr + 258) W) else hw
35
36theorem fillD_cases (ws ss : Nat) : (fillD ws ss = ws ∧ 2 * ws - 262 ≤ ss) ∨ (fillD ws ss = 0 ∧ ss < 2 * ws - 262) := by
37  unfold fillD; split <;> omega
38
39/-- **Lemma 1** (`I-fw-post-room`). Whenever `fill_window` returns, `strstart < window_size - MIN_LOOKAHEAD`. -/
40theorem fill_post_room {ws ss la : Nat} (hws : 512 ≤ ws) (hD : ss + la ≤ 2 * ws) :
41    ss - fillD ws ss < 2 * ws - 262 := by
42  unfold fillD; split <;> omega
43
44/-- The first read ends inside the window. -/
45theorem fill_fit {ws ss la a : Nat} (hws : 512 ≤ ws) (hD : ss + la ≤ 2 * ws) :
46    (ss - fillD ws ss) + la + fillL ws la ss a ≤ 2 * ws := by
47  unfold fillL fillD; split <;> omega
48
49/-- The slide: `more = window_size - lookahead - strstart` is at most `262` when the slide test holds, so
50`wsize - more` is a proper count and the copy `[ws, 2 * ws - more) -> [0, ws - more)` is inside the window and
51its two ranges do not overlap. Its length is `strstart + lookahead - ws`: the valid data moves down by `ws`. -/
52theorem slide_copy {ws ss la : Nat} (hws : 512 ≤ ws) (hD : ss + la ≤ 2 * ws) (ht : 2 * ws - 262 ≤ ss) :
53    let more := 2 * ws - la - ss
54    more ≤ 262 ∧ more ≤ ws ∧ ws - more = ss + la - ws ∧ ws + (ws - more) ≤ 2 * ws ∧ ws - more ≤ ws ∧
55      ws ≤ ss ∧ (ss - ws) + la ≤ ws := by
56  intro more
57  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> omega
58
59/-- After the slide `more + ws` is the room left: `window_size - lookahead - strstart'`. -/
60theorem slide_more {ws ss la : Nat} (hws : 512 ≤ ws) (hD : ss + la ≤ 2 * ws) (ht : 2 * ws - 262 ≤ ss) :
61    2 * ws - la - ss + ws = 2 * ws - la - (ss - ws) := by omega
62
63/-- The slide test in `unsigned` arithmetic: no wrap in `wsize + (w_size - MIN_LOOKAHEAD)`. -/
64theorem slide_test_nat {ws ss : Nat} (hws : 512 ≤ ws) (hle : ws ≤ 32768) :
65    ws + (ws - 262) = 2 * ws - 262 ∧ ws + (ws - 262) < 2 ^ 32 := by
66  constructor <;> omega
67
68/-! ## The `high_water` clearing -/
69
70/-- First branch (`high_water < curr`): `init = MIN(window_size - curr, WIN_INIT)`, the cleared range
71`[curr, curr + init)` is inside the window, and the new `high_water = curr + init` is `fillHW`. -/
72theorem hw_branch1 {hw W curr init : Nat} (hc : curr ≤ W) (h1 : hw < curr) (hi : init = min (W - curr) 258) :
73    curr + init ≤ W ∧ curr + init = fillHW hw W curr := by
74  unfold fillHW
75  rw [ite_eq_left (by omega)]
76  constructor <;> omega
77
78/-- Second branch (`curr <= high_water < curr + WIN_INIT`): `init` is the smaller of `curr + WIN_INIT - high_water`
79and `window_size - high_water`; the cleared range `[high_water, high_water + init)` is inside the window and the
80new `high_water` is `fillHW`. -/
81theorem hw_branch2 {hw W curr init : Nat} (hc : curr ≤ W) (h1 : hw < W) (h2 : curr ≤ hw) (h3 : hw < curr + 258)
82    (hi : init = min (curr + 258 - hw) (W - hw)) :
83    hw + init ≤ W ∧ hw + init = fillHW hw W curr := by
84  unfold fillHW
85  rw [ite_eq_left h1]
86  constructor <;> omega
87
88theorem fillHW_le {hw W curr : Nat} (hhw : hw ≤ W) : fillHW hw W curr ≤ W := by
89  unfold fillHW; split <;> omega
90
91theorem fillHW_ge (hw W curr : Nat) : hw ≤ fillHW hw W curr := by
92  unfold fillHW; split <;> omega
93
94/-! ## The margins of `longest_match` -/
95
96/-- `longest_match` is called with `strstart <= window_size - MIN_LOOKAHEAD`. Then `scan + MAX_MATCH` (`strend`) and
97the reads `scan[best_len]` (`best_len <= MAX_MATCH`) and `match[best_len]` stay inside the window, for every match
98position `cur_match <= strstart`. -/
99theorem lm_margin {ws ss c : Nat} (hss : ss ≤ 2 * ws - 262) (hc : c ≤ ss) (hws : 512 ≤ ws) :
100    ss + 258 < 2 * ws ∧ c + 258 < 2 * ws ∧ ss + 259 ≤ 2 * ws := by
101  refine ⟨?_, ?_, ?_⟩ <;> omega
102
103/-- The caller's facts give the margin: either `lookahead >= MIN_LOOKAHEAD` and (D) gives
104`strstart <= window_size - MIN_LOOKAHEAD`, or `fill_window` has just run (`fill_post_room`). -/
105theorem caller_margin {ws ss la : Nat} (hD : ss + la ≤ 2 * ws) (hla : 262 ≤ la) :
106    ss ≤ 2 * ws - 262 := by omega
107
108/-- `limit = strstart > MAX_DIST ? strstart - MAX_DIST : NIL`: every chain position above `limit` is within
109`MAX_DIST` of `strstart`. -/
110theorem limit_dist {ws ss p : Nat} (hlim : (if ss > ws - 262 then ss - (ws - 262) else 0) < p) (hp : p ≤ ss)
111    (hws : 512 ≤ ws) : ss - p ≤ ws - 262 := by
112  split at hlim <;> omega
113
114end Zlib.Deflate.Engine.Proofs