deflate.c.engine.lmcond.lean

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

1import ZlibF.Zlib.«deflate_strategies.c»
2import ZlibF.Proof.«deflate.c.engine.macros»
3import ZlibF.Proof.«deflate.c.engine.match»
4
5/-!
6# deflate.c, engine: the comparison step of `longest_match`
7
8`lm_cond` is the condition of the inner `do ... while`: `*++scan == *++match && ... (8 times) && scan < strend`.
9`lmCondR n` is the same computation written as a recursion on the number of comparisons left. `lm_cond_eq` shows that
10the translation is `lmCondR 8`; `lmCondR_ok` says what `n` comparisons do inside a window block: they stop at the
11first position where the two strings differ, or run out and test `scan < strend`.
12-/
13
14namespace Zlib.Deflate.Engine.Proofs
15open C Zlib.Deflate
16
17/-- The recursion on the number of comparisons left. -/
18def lmCondR (strend : BPtr) : Nat → BPtr → BPtr → M (Bool × BPtr × BPtr)
19  | 0, scan, m => do return (← Ptr.lt scan strend, scan, m)
20  | n + 1, scan, m => do
21    let scan ← padd scan 1
22    let m ← padd m 1
23    if (← load8 scan) != (← load8 m) then return (false, scan, m)
24    lmCondR strend n scan m
25
26/-- The offset at which `n` comparisons from offset `t` stop: the first `i` in `1 .. n` with
27`w (S + t + i) != w (C + t + i)` gives `some (t + i)`; `none` when all `n` agree. -/
28def cmpSteps (w : Nat → UInt8) (S C : Nat) : Nat → Nat → Option Nat
29  | 0, _ => none
30  | n + 1, t => if w (S + t + 1) ≠ w (C + t + 1) then some (t + 1) else cmpSteps w S C n (t + 1)
31
32theorem cmpSteps_some {w : Nat → UInt8} {S C : Nat} :
33    ∀ n t k, cmpSteps w S C n t = some k → t + 1 ≤ k ∧ k ≤ t + n ∧ w (S + k) ≠ w (C + k) ∧
34      ∀ j, t + 1 ≤ j → j < k → w (S + j) = w (C + j) := by
35  intro n
36  induction n with
37  | zero => intro t k h; simp [cmpSteps] at h
38  | succ n ih =>
39    intro t k h
40    unfold cmpSteps at h
41    split at h
42    · rename_i hne
43      cases h
44      refine ⟨by omega, by omega, by rwa [show S + (t + 1) = S + t + 1 by omega, show C + (t + 1) = C + t + 1 by omega],
45        fun j h1 h2 => by omega⟩
46    · rename_i heq
47      obtain ⟨a, b, c, d⟩ := ih (t + 1) k h
48      refine ⟨by omega, by omega, c, fun j h1 h2 => ?_⟩
49      by_cases hj : j = t + 1
50      · subst hj
51        have e : w (S + t + 1) = w (C + t + 1) := by simpa using heq
52        rwa [show S + (t + 1) = S + t + 1 by omega, show C + (t + 1) = C + t + 1 by omega]
53      · exact d j (by omega) h2
54
55theorem cmpSteps_none {w : Nat → UInt8} {S C : Nat} :
56    ∀ n t, cmpSteps w S C n t = none → ∀ j, t + 1 ≤ j → j ≤ t + n → w (S + j) = w (C + j) := by
57  intro n
58  induction n with
59  | zero => intro t _ j h1 h2; omega
60  | succ n ih =>
61    intro t h j h1 h2
62    unfold cmpSteps at h
63    split at h
64    · simp at h
65    · rename_i heq
66      by_cases hj : j = t + 1
67      · subst hj
68        have e : w (S + t + 1) = w (C + t + 1) := by simpa using heq
69        rwa [show S + (t + 1) = S + t + 1 by omega, show C + (t + 1) = C + t + 1 by omega]
70      · exact ih (t + 1) h j (by omega) (by omega)
71
72/-- **n comparisons of `lm_cond` inside the window.** The scan and match pointers are at offsets `S + t` and `C + t`
73of one byte block, `C <= S`, and the end pointer is `S + 258`; the reads stay below `S + 258 < size`. The result
74stops at the first differing position, or tests `scan < strend` after `n` equal comparisons. -/
75theorem lmCondR_ok {h : Heap} {wb : Nat} {wa : Array UInt8} (hw : h.bytes wb = some wa) (S C : Nat)
76    (hS : S + 258 < wa.size) (hCS : C ≤ S) :
77    ∀ n t, t + n ≤ 258 →
78      lmCondR (.ref (.blk wb) (S + 258)) n (.ref (.blk wb) (S + t)) (.ref (.blk wb) (C + t)) h =
79        .ok ((match cmpSteps (bfn wa) S C n t with
80          | some k => (false, Ptr.ref (BRef.blk wb) (S + k), Ptr.ref (BRef.blk wb) (C + k))
81          | none => (decide (S + (t + n) < S + 258), Ptr.ref (BRef.blk wb) (S + (t + n)),
82              Ptr.ref (BRef.blk wb) (C + (t + n)))), h) := by
83  intro n
84  induction n with
85  | zero =>
86    intro t ht
87    have : OkOn h (Ptr.lt (Ptr.ref (BRef.blk wb) (S + t)) (Ptr.ref (BRef.blk wb) (S + 258))) (decide (S + t < S + 258)) :=
88      Ptr.lt_ok (r := BRef.blk wb) (by simpa using hw) (by omega) (by omega)
89    simp only [lmCondR, cmpSteps, bind_app, Nat.add_zero]
90    unfold OkOn at this
91    rw [this]; rfl
92  | succ n ih =>
93    intro t ht
94    have g : Space.get h (BRef.blk wb) = some wa := by simpa using hw
95    have hs1 : S + t + 1 < wa.size := by omega
96    have hc1 : C + t + 1 < wa.size := by omega
97    have p1 : padd (Ptr.ref (BRef.blk wb) (S + t)) 1 h = .ok (Ptr.ref (BRef.blk wb) (S + t + 1), h) :=
98      padd_ok' g (by omega)
99    have p2 : padd (Ptr.ref (BRef.blk wb) (C + t)) 1 h = .ok (Ptr.ref (BRef.blk wb) (C + t + 1), h) :=
100      padd_ok' g (by omega)
101    have l1 : load8 (Ptr.ref (BRef.blk wb) (S + t + 1)) h = .ok (wa[S + t + 1], h) := Ptr.load_ok g hs1
102    have l2 : load8 (Ptr.ref (BRef.blk wb) (C + t + 1)) h = .ok (wa[C + t + 1], h) := Ptr.load_ok g hc1
103    have b1 : bfn wa (S + t + 1) = wa[S + t + 1] := by simp [bfn, Array.getD_eq_getD_getElem?, hs1]
104    have b2 : bfn wa (C + t + 1) = wa[C + t + 1] := by simp [bfn, Array.getD_eq_getD_getElem?, hc1]
105    simp only [lmCondR, bind_app, p1, p2, l1, l2]
106    by_cases hne : wa[S + t + 1] = wa[C + t + 1]
107    · have hne' : ¬ (bfn wa (S + t + 1) ≠ bfn wa (C + t + 1)) := by rw [b1, b2]; simpa using hne
108      have hih := ih (t + 1) (by omega)
109      rw [show S + (t + 1) = S + t + 1 by omega, show C + (t + 1) = C + t + 1 by omega,
110        show t + 1 + n = t + (n + 1) by omega] at hih
111      simp only [cmpSteps, hne', ite_false, hne, bne_self_eq_false, Bool.false_eq_true, hih]
112    · have hne' : bfn wa (S + t + 1) ≠ bfn wa (C + t + 1) := by rw [b1, b2]; exact hne
113      have hb : (wa[S + t + 1] != wa[C + t + 1]) = true := by simpa using hne
114      simp only [cmpSteps, ite_eq_left hne', hb]
115      rfl
116
117end Zlib.Deflate.Engine.Proofs