Deflate.lean

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

1import ZlibF.Proof.Format.Huffman
2import ZlibF.Spec.Format.Deflate
3
4/-!
5# Format meta-theory: a deflate stream has one decoding, and it does not depend on what follows
6
7* `Blocks.det`: the blocks that parse a bit list leave a unique rest and a unique output.
8* `Blocks.append`: a parse of a bit list is a parse of the list followed by whole bytes, leaving
9  the same bytes after it.
10* `Prefix.det`, `Prefix.ext`: the consequences for `Deflate.Prefix`.
11-/
12
13namespace ZlibF.Spec
14
15namespace Proofs
16
17theorem bytesToBits_len (t : List UInt8) : (bytesToBits t).length = 8 * t.length := by
18  induction t with
19  | nil => rfl
20  | cons b t ih => simp [bytesToBits, byteBits] at *; omega
21
22theorem readBits_append : ∀ (n : Nat) (inp : List Bool) (v : Nat) (r X : List Bool),
23    readBits n inp = some (v, r) → readBits n (inp ++ X) = some (v, r ++ X)
24  | 0, inp, v, r, X, h => by
25    simp only [readBits, Option.some.injEq, Prod.mk.injEq] at h
26    obtain ⟨rfl, rfl⟩ := h
27    simp [readBits]
28  | n + 1, [], v, r, X, h => by simp [readBits] at h
29  | n + 1, b :: i, v, r, X, h => by
30    cases hq : readBits n i with
31    | none => simp [readBits, hq] at h
32    | some p =>
33      obtain ⟨v', r'⟩ := p
34      simp only [readBits, hq, Option.some.injEq, Prod.mk.injEq] at h
35      obtain ⟨rfl, rfl⟩ := h
36      have := readBits_append n i v' r' X hq
37      simp [readBits, this]
38
39theorem readBytes_append : ∀ (n : Nat) (inp : List Bool) (v : List UInt8) (r X : List Bool),
40    readBytes n inp = some (v, r) → readBytes n (inp ++ X) = some (v, r ++ X)
41  | 0, inp, v, r, X, h => by
42    simp only [readBytes, Option.some.injEq, Prod.mk.injEq] at h
43    obtain ⟨rfl, rfl⟩ := h
44    simp [readBytes]
45  | n + 1, inp, v, r, X, h => by
46    cases hq : readBits 8 inp with
47    | none => simp [readBytes, hq] at h
48    | some p =>
49      obtain ⟨a, i⟩ := p
50      cases hq2 : readBytes n i with
51      | none => simp [readBytes, hq, hq2] at h
52      | some p2 =>
53        obtain ⟨bs, i2⟩ := p2
54        simp only [readBytes, hq, hq2, Option.some.injEq, Prod.mk.injEq] at h
55        obtain ⟨rfl, rfl⟩ := h
56        simp [readBytes, readBits_append 8 inp a i X hq, readBytes_append n i bs i2 X hq2]
57
58theorem readNats_append (w : Nat) : ∀ (n : Nat) (inp : List Bool) (v : List Nat) (r X : List Bool),
59    readNats w n inp = some (v, r) → readNats w n (inp ++ X) = some (v, r ++ X)
60  | 0, inp, v, r, X, h => by
61    simp only [readNats, Option.some.injEq, Prod.mk.injEq] at h
62    obtain ⟨rfl, rfl⟩ := h
63    simp [readNats]
64  | n + 1, inp, v, r, X, h => by
65    cases hq : readBits w inp with
66    | none => simp [readNats, hq] at h
67    | some p =>
68      obtain ⟨a, i⟩ := p
69      cases hq2 : readNats w n i with
70      | none => simp [readNats, hq, hq2] at h
71      | some p2 =>
72        obtain ⟨bs, i2⟩ := p2
73        simp only [readNats, hq, hq2, Option.some.injEq, Prod.mk.injEq] at h
74        obtain ⟨rfl, rfl⟩ := h
75        simp [readNats, readBits_append w inp a i X hq, readNats_append w n i bs i2 X hq2]
76
77theorem readCodeLenLens_append (n : Nat) (inp : List Bool) (cl : List Nat) (r X : List Bool)
78    (h : readCodeLenLens n inp = some (cl, r)) :
79    readCodeLenLens n (inp ++ X) = some (cl, r ++ X) := by
80  unfold readCodeLenLens at h ⊢
81  cases hq : readNats 3 n inp with
82  | none => simp [hq] at h
83  | some p =>
84    obtain ⟨vs, i⟩ := p
85    simp only [hq, Option.some.injEq, Prod.mk.injEq] at h
86    obtain ⟨rfl, rfl⟩ := h
87    simp [readNats_append 3 n inp vs i X hq]
88
89end Proofs
90
91open Proofs
92
93/-! ## Extension -/
94
95theorem Symbols.append {L D : List Nat} {dict : List UInt8} (hL : Ext L) (hD : Ext D)
96    {h : List UInt8} {inp rest : List Bool} {out : List UInt8}
97    (hs : Symbols L D dict h inp rest out) (X : List Bool) :
98    Symbols L D dict h (inp ++ X) (rest ++ X) out := by
99  induction hs with
100  | eob hd => exact .eob (hL _ _ _ X hd)
101  | lit hd hlt _ ih => exact .lit (hL _ _ _ X hd) hlt ih
102  | copy hd h1 h2 hr1 hd2 h3 hr2 hb _ ih =>
103    exact .copy (hL _ _ _ X hd) h1 h2 (readBits_append _ _ _ _ X hr1) (hD _ _ _ X hd2) h3
104      (readBits_append _ _ _ _ X hr2) hb ih
105
106theorem CodeLens.append {cl : List Nat} {total : Nat} (hc : Ext cl)
107    {acc : List Nat} {inp rest : List Bool} {lens : List Nat}
108    (hs : CodeLens cl total acc inp rest lens) (X : List Bool) :
109    CodeLens cl total acc (inp ++ X) (rest ++ X) lens := by
110  induction hs with
111  | done h => exact .done h
112  | len hlt hd hs _ ih => exact .len hlt (hc _ _ _ X hd) hs ih
113  | rep16 hlt hd hne hr hb _ ih =>
114    exact .rep16 hlt (hc _ _ _ X hd) hne (readBits_append _ _ _ _ X hr) hb ih
115  | rep17 hlt hd hr hb _ ih =>
116    exact .rep17 hlt (hc _ _ _ X hd) (readBits_append _ _ _ _ X hr) hb ih
117  | rep18 hlt hd hr hb _ ih =>
118    exact .rep18 hlt (hc _ _ _ X hd) (readBits_append _ _ _ _ X hr) hb ih
119
120theorem Body.append {dict : List UInt8} {bt : Nat} {h : List UInt8} {inp rest : List Bool}
121    {out : List UInt8} (hb : Body dict bt h inp rest out) (X : List Bool) (hX : X.length % 8 = 0) :
122    Body dict bt h (inp ++ X) (rest ++ X) out := by
123  cases hb with
124  | stored h1 h2 h3 h4 =>
125    refine .stored ?_ (readBits_append _ _ _ _ X h2) h3 (readBytes_append _ _ _ _ X h4)
126    have e : (inp ++ X).length % 8 = inp.length % 8 := by
127      simp only [List.length_append]; omega
128    rw [e, List.drop_append_of_le_length (Nat.mod_le _ _)]
129    exact readBits_append _ _ _ _ X h1
130  | fixed hs => exact .fixed (hs.append ext_fixedLit ext_fixedDist X)
131  | dynamic h1 h2 h3 h4 h5 ha h6 h7 h8 h9 hs =>
132    exact .dynamic (readBits_append _ _ _ _ X h1) (readBits_append _ _ _ _ X h2)
133      (readBits_append _ _ _ _ X h3) h4 (readCodeLenLens_append _ _ _ _ X h5) ha
134      ((h6.append (ext_acceptable ha) X)) h7 h8 h9
135      (hs.append (ext_acceptable h8) (ext_acceptable h9) X)
136
137/-- A parse of `inp` is a parse of `inp ++ X` that leaves `rest ++ X`, when `X` is whole bytes. -/
138theorem Blocks.append {dict : List UInt8} {h : List UInt8} {inp rest : List Bool} {out : List UInt8}
139    (hb : Blocks dict h inp rest out) (X : List Bool) (hX : X.length % 8 = 0) :
140    Blocks dict h (inp ++ X) (rest ++ X) out := by
141  induction hb with
142  | last h1 h2 hbody =>
143    exact .last (readBits_append _ _ _ _ X h1) (readBits_append _ _ _ _ X h2) (hbody.append X hX)
144  | more h1 h2 hbody _ ih =>
145    exact .more (readBits_append _ _ _ _ X h1) (readBits_append _ _ _ _ X h2) (hbody.append X hX) ih
146
147/-! ## Determinism -/
148
149private theorem some_inj {α β : Type} {a a' : α} {b b' : β} (h : some (a, b) = some (a', b')) :
150    a = a' ∧ b = b' := by
151  simpa using h
152
153theorem Symbols.det {L D : List Nat} {dict : List UInt8} {h : List UInt8} {inp r1 r2 : List Bool}
154    {o1 o2 : List UInt8} (h1 : Symbols L D dict h inp r1 o1) (h2 : Symbols L D dict h inp r2 o2) :
155    r1 = r2 ∧ o1 = o2 := by
156  induction h1 generalizing r2 o2 with
157  | eob hd =>
158    cases h2 with
159    | eob hd' => rw [hd] at hd'; obtain ⟨-, rfl⟩ := some_inj hd'; exact ⟨rfl, rfl⟩
160    | lit hd' hlt _ => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
161    | copy hd' h257 => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
162  | lit hd hlt _ ih =>
163    cases h2 with
164    | eob hd' => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
165    | lit hd' hlt' hs' =>
166      rw [hd] at hd'; obtain ⟨rfl, rfl⟩ := some_inj hd'; exact ih hs'
167    | copy hd' h257 => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
168  | copy hd h257 h285 hr1 hd2 h29 hr2 hb _ ih =>
169    cases h2 with
170    | eob hd' => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
171    | lit hd' hlt => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
172    | copy hd' h257' h285' hr1' hd2' h29' hr2' hb' hs' =>
173      rw [hd] at hd'; obtain ⟨rfl, rfl⟩ := some_inj hd'
174      rw [hr1] at hr1'; obtain ⟨rfl, rfl⟩ := some_inj hr1'
175      rw [hd2] at hd2'; obtain ⟨rfl, rfl⟩ := some_inj hd2'
176      rw [hr2] at hr2'; obtain ⟨rfl, rfl⟩ := some_inj hr2'
177      exact ih hs'
178
179theorem CodeLens.det {cl : List Nat} {total : Nat} {acc : List Nat} {inp r1 r2 : List Bool}
180    {l1 l2 : List Nat} (h1 : CodeLens cl total acc inp r1 l1) (h2 : CodeLens cl total acc inp r2 l2) :
181    r1 = r2 ∧ l1 = l2 := by
182  induction h1 generalizing r2 l2 with
183  | done h =>
184    cases h2 with
185    | done h' => exact ⟨rfl, rfl⟩
186    | len hlt => omega
187    | rep16 hlt => omega
188    | rep17 hlt => omega
189    | rep18 hlt => omega
190  | len hlt hd hs _ ih =>
191    cases h2 with
192    | done h' => omega
193    | len hlt' hd' hs' hr =>
194      rw [hd] at hd'; obtain ⟨rfl, rfl⟩ := some_inj hd'; exact ih hr
195    | rep16 hlt' hd' => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
196    | rep17 hlt' hd' => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
197    | rep18 hlt' hd' => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
198  | rep16 hlt hd hne hr hb _ ih =>
199    cases h2 with
200    | done h' => omega
201    | len hlt' hd' hs' => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
202    | rep16 hlt' hd' hne' hr' hb' hs' =>
203      rw [hd] at hd'; obtain ⟨-, rfl⟩ := some_inj hd'
204      rw [hr] at hr'; obtain ⟨rfl, rfl⟩ := some_inj hr'
205      exact ih hs'
206    | rep17 hlt' hd' => rw [hd] at hd'; obtain ⟨h, -⟩ := some_inj hd'; omega
207    | rep18 hlt' hd' => rw [hd] at hd'; obtain ⟨h, -⟩ := some_inj hd'; omega
208  | rep17 hlt hd hr hb _ ih =>
209    cases h2 with
210    | done h' => omega
211    | len hlt' hd' hs' => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
212    | rep16 hlt' hd' => rw [hd] at hd'; obtain ⟨h, -⟩ := some_inj hd'; omega
213    | rep17 hlt' hd' hr' hb' hs' =>
214      rw [hd] at hd'; obtain ⟨-, rfl⟩ := some_inj hd'
215      rw [hr] at hr'; obtain ⟨rfl, rfl⟩ := some_inj hr'
216      exact ih hs'
217    | rep18 hlt' hd' => rw [hd] at hd'; obtain ⟨h, -⟩ := some_inj hd'; omega
218  | rep18 hlt hd hr hb _ ih =>
219    cases h2 with
220    | done h' => omega
221    | len hlt' hd' hs' => rw [hd] at hd'; obtain ⟨rfl, -⟩ := some_inj hd'; omega
222    | rep16 hlt' hd' => rw [hd] at hd'; obtain ⟨h, -⟩ := some_inj hd'; omega
223    | rep17 hlt' hd' => rw [hd] at hd'; obtain ⟨h, -⟩ := some_inj hd'; omega
224    | rep18 hlt' hd' hr' hb' hs' =>
225      rw [hd] at hd'; obtain ⟨-, rfl⟩ := some_inj hd'
226      rw [hr] at hr'; obtain ⟨rfl, rfl⟩ := some_inj hr'
227      exact ih hs'
228
229theorem Body.det {dict : List UInt8} {bt : Nat} {h : List UInt8} {inp r1 r2 : List Bool}
230    {o1 o2 : List UInt8} (h1 : Body dict bt h inp r1 o1) (h2 : Body dict bt h inp r2 o2) :
231    r1 = r2 ∧ o1 = o2 := by
232  cases h1 with
233  | stored a1 a2 _ a4 =>
234    cases h2 with
235    | stored b1 b2 _ b4 =>
236      rw [a1] at b1; obtain ⟨rfl, rfl⟩ := some_inj b1
237      rw [a2] at b2; obtain ⟨rfl, rfl⟩ := some_inj b2
238      rw [a4] at b4; obtain ⟨rfl, rfl⟩ := some_inj b4
239      exact ⟨rfl, rfl⟩
240  | fixed hs =>
241    cases h2 with
242    | fixed hs' => exact hs.det hs'
243  | dynamic a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 hs =>
244    cases h2 with
245    | dynamic b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 hs' =>
246      rw [a1] at b1; obtain ⟨rfl, rfl⟩ := some_inj b1
247      rw [a2] at b2; obtain ⟨rfl, rfl⟩ := some_inj b2
248      rw [a3] at b3; obtain ⟨rfl, rfl⟩ := some_inj b3
249      rw [a5] at b5; obtain ⟨rfl, rfl⟩ := some_inj b5
250      obtain ⟨rfl, rfl⟩ := a7.det b7
251      exact hs.det hs'
252
253/-- The blocks that parse a bit list leave a unique rest and a unique output. -/
254theorem Blocks.det {dict : List UInt8} {h : List UInt8} {inp r1 r2 : List Bool}
255    {o1 o2 : List UInt8} (h1 : Blocks dict h inp r1 o1) (h2 : Blocks dict h inp r2 o2) :
256    r1 = r2 ∧ o1 = o2 := by
257  induction h1 generalizing r2 o2 with
258  | last a1 a2 ab =>
259    cases h2 with
260    | last b1 b2 bb =>
261      rw [a1] at b1; obtain ⟨-, rfl⟩ := some_inj b1
262      rw [a2] at b2; obtain ⟨rfl, rfl⟩ := some_inj b2
263      exact ab.det bb
264    | more b1 => rw [a1] at b1; obtain ⟨h, -⟩ := some_inj b1; omega
265  | more a1 a2 ab _ ih =>
266    cases h2 with
267    | last b1 => rw [a1] at b1; obtain ⟨h, -⟩ := some_inj b1; omega
268    | more b1 b2 bb bs =>
269      rw [a1] at b1; obtain ⟨-, rfl⟩ := some_inj b1
270      rw [a2] at b2; obtain ⟨rfl, rfl⟩ := some_inj b2
271      obtain ⟨rfl, rfl⟩ := ab.det bb
272      exact ih bs
273
274/-! ## `Deflate.Prefix` -/
275
276/-- The output of a prefix parse is a function of the dictionary and the stream. -/
277theorem Prefix.det {dict s t1 t2 o1 o2 : List UInt8} (h1 : Deflate.Prefix dict s t1 o1)
278    (h2 : Deflate.Prefix dict s t2 o2) : o1 = o2 := by
279  obtain ⟨r1, b1, -⟩ := h1
280  obtain ⟨r2, b2, -⟩ := h2
281  exact (b1.det b2).2
282
283/-- A parse of `s` followed by trailer `t1` is a parse of `s ++ t` with trailer `t1 ++ t`
284(same output), and the other way round. -/
285theorem Prefix.ext {dict s t t1 t2 o1 o2 : List UInt8} (h1 : Deflate.Prefix dict s t1 o1)
286    (h2 : Deflate.Prefix dict (s ++ t) t2 o2) : t2.length = t1.length + t.length ∧ o1 = o2 := by
287  obtain ⟨r1, b1, p1⟩ := h1
288  obtain ⟨r2, b2, p2⟩ := h2
289  have hX : (bytesToBits t).length % 8 = 0 := by rw [Proofs.bytesToBits_len]; omega
290  have b1' : Blocks dict [] (bytesToBits (s ++ t)) (r1 ++ bytesToBits t) o1 := by
291    have := b1.append (bytesToBits t) hX
292    simpa [bytesToBits, List.flatMap_append] using this
293  obtain ⟨hr, ho⟩ := b1'.det b2
294  subst hr
295  refine ⟨?_, ho⟩
296  have l1 := congrArg List.length p1
297  have l2 := congrArg List.length p2
298  simp only [List.length_drop, List.length_append, Proofs.bytesToBits_len] at l1 l2
299  have : (r1.length + 8 * t.length) % 8 = r1.length % 8 := by omega
300  rw [this] at l2
301  omega
302
303end ZlibF.Spec