InflateFastMatchHistory.lean

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

1import ZlibF.Spec.InflateFastMatchHistory
2import ZlibF.Math.LZ77Copy
3import ZlibF.Math.LZ77History
4
5/-!
6# The fast copier's physical pieces form one independent match
7
8Every window segment is related to its chronological ring position. The
9pieces are then joined with the bytewise copyBack composition theorem.
10-/
11
12set_option autoImplicit false
13
14namespace Zlib.Inffast.Proofs
15open C Zlib.Inffast.Spec Zlib.Inffast.Spec.MatchHistory
16open ZlibF.Spec ZlibF.Math.LZ77Copy ZlibF.Math.LZ77History
17open Zlib.Inflate.Spec (ringSlot)
18
19private theorem saved_length (W : Array UInt8) (ws wn wh woff : Nat) :
20    (saved W ws wn wh woff).length = wh := by simp [saved]
21
22private theorem saved_get (W : Array UInt8) (ws wn wh woff j : Nat) (hj : j < wh) :
23    (saved W ws wn wh woff).getD j 0 = W.getD (woff + ringSlot ws wn wh j) 0 := by
24  have hlen : j < (saved W ws wn wh woff).length := by simpa [saved] using hj
25  rw [← List.getElem_eq_getD (h := hlen) 0]
26  simp only [saved, List.getElem_map, List.getElem_range]
27
28private theorem before_wrap (ws wn wh back i : Nat)
29    (hwh : wh ≤ ws) (hb : back ≤ wh) (hw : wn < back) (hi : i < back - wn) :
30    ringSlot ws wn wh (wh - back + i) = ws + wn - back + i := by
31  have hfull : ¬ wh ≤ wn := by omega
32  have hindex : wh - back + i < wh - wn := by omega
33  simp only [ringSlot, hfull, hindex, ite_false, ite_true]
34  omega
35
36private theorem after_wrap (ws wn wh back i : Nat)
37    (hb : back ≤ wh) (hw : wn < back) (hi : i < wn) :
38    ringSlot ws wn wh (wh - wn + i) = i := by
39  have hfull : ¬ wh ≤ wn := by omega
40  have hindex : ¬ wh - wn + i < wh - wn := by omega
41  simp only [ringSlot, hfull, hindex, ite_false]
42  omega
43
44private theorem no_wrap (ws wn wh back i : Nat)
45    (hb : back ≤ wh) (hw : back ≤ wn) (hi : i < back) :
46    ringSlot ws wn wh (wh - back + i) = wn - back + i := by
47  by_cases hfull : wh ≤ wn
48  · simp only [ringSlot, hfull, ite_true]
49    omega
50  · have hindex : ¬ wh - back + i < wh - wn := by omega
51    simp only [ringSlot, hfull, hindex, ite_false]
52    omega
53
54/-- Both window segments, followed by overlapping output if necessary,
55implement one independent copyBack on the actual chronological history. -/
56theorem fast_match_array_refines_lz77 : MatchHistory.Goal.match_array_refines_lz77 := by
57  intro W A ws wn wh woff bg o dist len hwh hwn hW hbg hroom hd havail
58  let count := o - bg
59  let history := saved W ws wn wh woff
60  let current := writtenBytes A o count
61  have hcount : count ≤ o := by dsimp [count]; omega
62  have hhistory : history.length = wh := saved_length W ws wn wh woff
63  by_cases route : o - bg < dist
64  · let back := dist - count
65    have hroute : count < dist := route
66    have hback : 0 < back ∧ back ≤ wh := by dsimp [back]; dsimp [count] at *; omega
67    have hstorage : woff + ws ≤ W.size := hW (by omega)
68    have first : ∀ (n sourceOffset : Nat), n ≤ back → o + n ≤ A.size →
69        sourceOffset + n ≤ W.size →
70        (∀ i, i < n → W.getD (sourceOffset + i) 0 =
71          history.getD (history.length + count - dist + i) 0) →
72        writtenBytes (blitN W n sourceOffset o A) (o + n) (count + n) =
73          copyBack history dist n current := by
74      intro n sourceOffset hn hr hs hp
75      exact window_copy_refines_lz77 history A W o count sourceOffset dist n
76        hcount hroute (by rw [hhistory]; exact havail) (by dsimp [back] at hn; exact hn) hr hs hp
77    have finish : ∀ (B : Array UInt8) (k : Nat),
78        B.size = A.size → k ≤ len → dist ≤ count + k →
79        writtenBytes B (o + k) (count + k) = copyBack history dist k current →
80        writtenBytes (cpyN (len - k) (o + k - dist) (o + k) B)
81          (o + len) (count + len) = copyBack history dist len current := by
82      intro B k hsz hk hdist hp
83      have H := output_copy_refines_lz77 history B (o + k) (count + k) dist (len - k)
84        (by omega) hd hdist (by omega)
85      have hoff : o + k + (len - k) = o + len := by omega
86      have hc : count + k + (len - k) = count + len := by omega
87      rw [hoff, hc, hp, ← copy_back_compose] at H
88      simpa only [show k + (len - k) = len by omega] using H
89    by_cases hzero : wn = 0
90    · have segment : ∀ n, n ≤ back → n ≤ len →
91          writtenBytes (blitN W n (woff + ws - back) o A) (o + n) (count + n) =
92            copyBack history dist n current := by
93        intro n hn hlen
94        apply first n (woff + ws - back) hn (by omega) (by omega)
95        intro i hi
96        have hj : history.length + count - dist + i < wh := by rw [hhistory]; dsimp [back] at hn; omega
97        have hidx : history.length + count - dist + i = wh - back + i := by rw [hhistory]; dsimp [back]; omega
98        rw [hidx, saved_get W ws wn wh woff _ (by omega)]
99        rw [before_wrap ws wn wh back i hwh hback.2 (by omega) (by omega)]
100        congr 1
101        omega
102      by_cases hlen : back < len
103      · have hprefix := segment back (by omega) (by omega)
104        have H := finish (blitN W back (woff + ws - back) o A) back
105          (blitN_size ..) (by omega) (by dsimp [back]; omega) hprefix
106        simpa [matchArr, route, hzero, hlen, back, count, history, current] using H
107      · have H := segment len (by omega) (by omega)
108        simpa [matchArr, route, hzero, hlen, back, count, history, current] using H
109    · by_cases hwrap : wn < back
110      · let k := back - wn
111        have hkpos : 0 < k := by dsimp [k]; omega
112        have segment : ∀ n, n ≤ k → n ≤ len →
113            writtenBytes (blitN W n (woff + ws + wn - back) o A) (o + n) (count + n) =
114              copyBack history dist n current := by
115          intro n hn hlen
116          apply first n (woff + ws + wn - back) (by dsimp [k] at hn; omega) (by omega) (by dsimp [k] at hn; omega)
117          intro i hi
118          have hidx : history.length + count - dist + i = wh - back + i := by rw [hhistory]; dsimp [back]; omega
119          rw [hidx, saved_get W ws wn wh woff _ (by dsimp [k] at hn; omega)]
120          rw [before_wrap ws wn wh back i hwh hback.2 hwrap (by dsimp [k] at hn; omega)]
121          congr 1
122          omega
123        by_cases hlen1 : k < len
124        · let B := blitN W k (woff + ws + wn - back) o A
125          have hB : B.size = A.size := blitN_size ..
126          have hfirst := segment k (by omega) (by omega)
127          have second : ∀ n, n ≤ wn → n ≤ len - k →
128              writtenBytes (blitN W n woff (o + k) B) (o + k + n) (count + k + n) =
129                copyBack history dist (k + n) current := by
130            intro n hn hlen
131            have H := window_copy_refines_lz77 history B W (o + k) (count + k) woff dist n
132              (by omega) (by dsimp [k, back]; omega) (by rw [hhistory]; omega)
133              (by dsimp [k, back]; omega) (by omega) (by omega) ?_
134            · rw [show writtenBytes B (o + k) (count + k) = copyBack history dist k current from hfirst,
135                ← copy_back_compose] at H
136              exact H
137            · intro i hi
138              have hidx : history.length + (count + k) - dist + i = wh - wn + i := by
139                rw [hhistory]; dsimp [k, back]; omega
140              rw [hidx, saved_get W ws wn wh woff _ (by omega)]
141              rw [after_wrap ws wn wh back i hback.2 hwrap (by omega)]
142          by_cases hlen2 : wn < len - k
143          · have hsecond := second wn (by omega) (by omega)
144            have heq : k + wn = back := by dsimp [k]; omega
145            have hprefix : writtenBytes (blitN W wn woff (o + k) B) (o + back) (count + back) =
146                copyBack history dist back current := by simpa only [Nat.add_assoc, heq] using hsecond
147            have H := finish (blitN W wn woff (o + k) B) back
148              (by simp only [blitN_size]; exact hB) (by dsimp [k] at hlen2; omega)
149              (by dsimp [back]; omega) hprefix
150            have hlenrem : len - k - wn = len - back := by dsimp [k]; omega
151            simpa [matchArr, route, hzero, hwrap, hlen1, hlen2, hlenrem, B, k, back, count,
152              history, current, Nat.add_assoc, heq] using H
153          · have H := second (len - k) (by omega) (by omega)
154            have hlenfull : k + (len - k) = len := by omega
155            simpa [matchArr, route, hzero, hwrap, hlen1, hlen2, B, k, back, count,
156              history, current, Nat.add_assoc, hlenfull] using H
157        · have H := segment len (by omega) (by omega)
158          simpa [matchArr, route, hzero, hwrap, hlen1, k, back, count, history, current] using H
159      · have segment : ∀ n, n ≤ back → n ≤ len →
160            writtenBytes (blitN W n (woff + wn - back) o A) (o + n) (count + n) =
161              copyBack history dist n current := by
162          intro n hn hlen
163          apply first n (woff + wn - back) hn (by omega) (by omega)
164          intro i hi
165          have hidx : history.length + count - dist + i = wh - back + i := by rw [hhistory]; dsimp [back]; omega
166          rw [hidx, saved_get W ws wn wh woff _ (by omega)]
167          rw [no_wrap ws wn wh back i hback.2 (by omega) (by omega)]
168          congr 1
169          omega
170        by_cases hlen : back < len
171        · have H := finish (blitN W back (woff + wn - back) o A) back
172            (blitN_size ..) (by omega) (by dsimp [back]; omega) (segment back (by omega) (by omega))
173          simpa [matchArr, route, hzero, hwrap, hlen, back, count, history, current] using H
174        · have H := segment len (by omega) (by omega)
175          simpa [matchArr, route, hzero, hwrap, hlen, back, count, history, current] using H
176  · have H := output_copy_refines_lz77 (saved W ws wn wh woff) A o (o - bg) dist len
177      (by omega) hd (by omega) hroom
178    simpa only [matchArr, route, ite_false] using H
179
180end Zlib.Inffast.Proofs