deflate.c.engine.lminner.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.lmcond»
2import ZlibF.Proof.«deflate.c.engine.loops»
3
4/-!
5# deflate.c, engine: the inner comparison loop of `longest_match`
6
7`do { } while (*++scan == *++match && ... && scan < strend);` starting at offset 2 (the first two bytes and, by the
8hash, the third are known equal). The loop does not fault inside the window, leaves the heap alone, and stops with
9`scan` at offset `r = firstMis w S C 3` from `S`, and `match` at offset `r` from `C`.
10-/
11
12namespace Zlib.Deflate.Engine.Proofs
13open C Zlib.Deflate
14
15theorem M_bind_assoc {α β γ : Type} (m : M α) (f : α → M β) (g : β → M γ) :
16    ((m >>= f) >>= g) = (m >>= fun x => f x >>= g) := by
17  funext h
18  simp only [bind_app]
19  cases m h with
20  | error e => rfl
21  | ok p => rfl
22
23theorem M_pure_bind {α β : Type} (a : α) (f : α → M β) : (pure a >>= f) = f a := rfl
24
25theorem M_ite_bind {α β : Type} (c : Prop) [Decidable c] (a b : M α) (f : α → M β) :
26    ((if c then a else b) >>= f) = if c then a >>= f else b >>= f := by
27  split <;> rfl
28
29theorem lm_cond_eq (strend scan m : BPtr) : lm_cond strend scan m = lmCondR strend 8 scan m := by
30  unfold lm_cond
31  simp [List.range', List.forIn'_cons, List.forIn'_nil, lmCondR, M_bind_assoc, M_pure_bind, M_ite_bind]
32
33/-- **The inner loop.** In a byte block `wa` with `S + 258 < wa.size` and `C <= S`, where the strings at `S` and `C`
34agree on the first three bytes, the loop started at offsets 2 does not fault, leaves the heap as it is, and ends with
35`scan = S + r`, `match = C + r`, `r = matchLen` (the first position from 3 on where they differ, or 258). -/
36theorem lm_inner_loop {h : Heap} {wb : Nat} {wa : Array UInt8} (hw : h.bytes wb = some wa) (S C : Nat)
37    (hS : S + 258 < wa.size) (hCS : C ≤ S)
38    (h0 : bfn wa S = bfn wa C) (h1 : bfn wa (S + 1) = bfn wa (C + 1)) (h2 : bfn wa (S + 2) = bfn wa (C + 2)) :
39    cdoWhile (fun x => (pure x : M (BPtr × BPtr)))
40      (fun (scan, m) => do
41        let (c, scan, m) ← lm_cond (Ptr.ref (BRef.blk wb) (S + 258)) scan m
42        pure (c, (scan, m)))
43      (Ptr.ref (BRef.blk wb) (S + 2), Ptr.ref (BRef.blk wb) (C + 2)) h =
44    .ok ((Ptr.ref (BRef.blk wb) (S + matchLen (bfn wa) S C), Ptr.ref (BRef.blk wb) (C + matchLen (bfn wa) S C)), h) := by
45  let Inv : BPtr × BPtr → Heap → Prop := fun s h' =>
46    h' = h ∧ ∃ j, j % 8 = 2 ∧ 2 ≤ j ∧ j ≤ 250 ∧ s = (Ptr.ref (BRef.blk wb) (S + j), Ptr.ref (BRef.blk wb) (C + j)) ∧
47      ∀ k, 3 ≤ k → k ≤ j → bfn wa (S + k) = bfn wa (C + k)
48  let Q : BPtr × BPtr → Heap → Prop := fun s h' =>
49    h' = h ∧ s = (Ptr.ref (BRef.blk wb) (S + matchLen (bfn wa) S C), Ptr.ref (BRef.blk wb) (C + matchLen (bfn wa) S C))
50  let μ : BPtr × BPtr → Nat := fun s => match s.1 with | .null => 0 | .ref _ o => 258 - (o - S)
51  have key := cdoWhile_measure (σ := BPtr × BPtr)
52    (body := fun x => (pure x : M (BPtr × BPtr)))
53    (cond := fun (scan, m) => do
54        let (c, scan, m) ← lm_cond (Ptr.ref (BRef.blk wb) (S + 258)) scan m
55        pure (c, (scan, m)))
56    Inv μ Q ?_ (s := (Ptr.ref (BRef.blk wb) (S + 2), Ptr.ref (BRef.blk wb) (C + 2))) (h := h)
57    ⟨rfl, 2, by omega, by omega, by omega, rfl, fun k hk1 hk2 => by omega⟩ (by unfold fuel; simp only [μ]; omega)
58  · obtain ⟨s', h', hrun, hq, hs⟩ := key
59    rw [hrun, hq, hs]
60  · intro s h' hI
61    obtain ⟨hh', j, hj8, hj2, hj250, hs, hag⟩ := hI
62    have hh2 := hh'.symm
63    subst hh2
64    subst hs
65    have hrun := lmCondR_ok hw S C hS hCS 8 j (by omega)
66    cases hcs : cmpSteps (bfn wa) S C 8 j with
67    | some k =>
68      obtain ⟨hk1, hk2, hk3, hk4⟩ := cmpSteps_some 8 j k hcs
69      refine ⟨_, h, false, (Ptr.ref (BRef.blk wb) (S + k), Ptr.ref (BRef.blk wb) (C + k)), h, rfl, ?_, ?_, ?_⟩
70      · simp only [bind_app, lm_cond_eq, hrun, hcs]
71        try rfl
72      · intro _
73        have : matchLen (bfn wa) S C = k := by
74          unfold matchLen
75          apply firstMis_unique (bfn wa) S C (by omega) (by omega)
76          · intro q hq1 hq2
77            by_cases hqj : q ≤ j
78            · exact hag q hq1 hqj
79            · exact hk4 q (by omega) hq2
80          · intro _; exact hk3
81        refine ⟨rfl, ?_⟩
82        rw [this]
83      · intro hc; simp at hc
84    | none =>
85      have hn := cmpSteps_none 8 j hcs
86      by_cases hlt : S + (j + 8) < S + 258
87      · refine ⟨_, h, true, (Ptr.ref (BRef.blk wb) (S + (j + 8)), Ptr.ref (BRef.blk wb) (C + (j + 8))), h, rfl, ?_, ?_, ?_⟩
88        · simp [bind_app, lm_cond_eq, hrun, hcs, hlt]
89        · intro hc; simp at hc
90        · intro _
91          refine ⟨⟨rfl, j + 8, by omega, by omega, by omega, rfl, ?_⟩, ?_⟩
92          · intro k hk1 hk2
93            by_cases hkj : k ≤ j
94            · exact hag k hk1 hkj
95            · exact hn k (by omega) (by omega)
96          · simp only [μ]; omega
97      · refine ⟨_, h, false, (Ptr.ref (BRef.blk wb) (S + (j + 8)), Ptr.ref (BRef.blk wb) (C + (j + 8))), h, rfl, ?_, ?_, ?_⟩
98        · simp [bind_app, lm_cond_eq, hrun, hcs, hlt]
99        · intro _
100          have : matchLen (bfn wa) S C = 258 := by
101            unfold matchLen
102            apply firstMis_unique (bfn wa) S C (by omega) (by omega)
103            · intro q hq1 hq2
104              by_cases hqj : q ≤ j
105              · exact hag q hq1 hqj
106              · exact hn q (by omega) (by omega)
107            · intro h258; omega
108          refine ⟨rfl, ?_⟩
109          rw [this]
110          have e : j + 8 = 258 := by omega
111          rw [e]
112        · intro hc; simp at hc
113
114end Zlib.Deflate.Engine.Proofs