GzipRoundtrip.lean

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

1import ZlibF.Proof.Api.Roundtrip
2
3namespace ZlibF.Spec.Api.Proofs
4open ZlibF.Spec
5
6private def HeaderInvariant (s : DeflState) : Prop := s.precise = true → s.header.Valid
7
8private theorem header_run {st st' : DeflState} {c : DeflCall} {o : DeflOut}
9    (hr : DeflRun st c o st') (hp : HeaderInvariant st) : HeaderInvariant st' := by
10  have hh := hr.1.2.2.2.2.2.2.2
11  have hprec := hr.2.2.1
12  intro h
13  have hv := hp (hprec.symm.trans h)
14  simpa [DeflState.header, hh] using hv
15
16private theorem header_step {st st' : DeflState} {c : DeflCall} {o : DeflOut}
17    (hr : DeflStep st c o st') (hp : HeaderInvariant st) : HeaderInvariant st' := by
18  by_cases ht : c.flush = .trees
19  · rw [(hr.1 ht).2.2.2]; exact hp
20  by_cases hb : c.badBuf = true ∨ (st.finishing = true ∧ c.flush ≠ .finish)
21  · rw [(hr.2.1 ht hb).2.2.2]; exact hp
22  have hbuf : c.badBuf = false := by cases h : c.badBuf <;> simp_all
23  have hnfin : ¬ (st.finishing = true ∧ c.flush ≠ .finish) := fun h => hb (Or.inr h)
24  by_cases hz : c.availOut = 0
25  · rw [(hr.2.2.1 ht hbuf hnfin hz).2.2.2]; exact hp
26  exact header_run (hr.2.2.2 ht hbuf hnfin hz) hp
27
28private theorem header_dict {st st' : DeflState} {d : List UInt8} {rc : Int}
29    (hr : DeflSetDict st d rc st') (hp : HeaderInvariant st) : HeaderInvariant st' := by
30  cases hw : st.params.wrap with
31  | gzip => simp only [DeflSetDict, hw] at hr; rcases hr with ⟨_, rfl⟩; exact hp
32  | zlib =>
33    simp only [DeflSetDict, hw] at hr
34    split at hr <;> rcases hr with ⟨_, rfl⟩ <;> exact hp
35  | raw =>
36    simp only [DeflSetDict, hw] at hr
37    split at hr
38    · rcases hr with ⟨_, rfl⟩; exact hp
39    · rcases hr with ⟨_, rfl⟩ | ⟨_, rfl⟩
40      · exact hp
41      · intro h
42        cases h
43
44private theorem header_set {st st' : DeflState} {h : GzHead} {rc : Int}
45    (hr : DeflSetHeader st h rc st') (hp : HeaderInvariant st) : HeaderInvariant st' := by
46  unfold DeflSetHeader at hr
47  split at hr
48  · rcases hr with ⟨_, rfl⟩; exact hp
49  · rcases hr with ⟨_, hbad, hgood⟩
50    by_cases hb : st.started = true ∨ ¬ h.Valid
51    · rw [hbad hb]
52      intro he
53      cases he
54    · rw [hgood hb]
55      intro _
56      simpa [DeflState.header] using (not_or.mp hb).2
57
58/-- A precise deflate model trace has a valid gzip header. -/
59theorem deflate_trace_header_valid {X : List UInt8} {p : DeflParams} {st : DeflState}
60    (ht : DeflTrace X (DeflState.fresh p) st) (hp : st.precise = true) : st.header.Valid := by
61  have preserve : ∀ {a b : DeflState}, DeflTrace X a b → HeaderInvariant a → HeaderInvariant b := by
62    intro a b trace
63    induction trace with
64    | nil => exact id
65    | step _ hm _ ih => intro h; exact ih (header_step hm.1 h)
66    | dict hm _ ih => intro h; exact ih (header_dict hm h)
67    | header hm _ ih => intro h; exact ih (header_set hm h)
68  apply preserve ht _ hp
69  intro _
70  simp [DeflState.fresh, DeflState.header, GzHead.default, GzHead.Valid]
71
72private theorem header_flags (h : GzHead) :
73    h.flg.toUInt8.toNat < 32 ∧ (h.flg.toUInt8.toNat / 2 % 2 = 1 ↔ h.hcrc = true) := by
74  cases h with
75  | mk text time os extra name comment hcrc =>
76    cases text <;> cases hcrc <;> cases extra <;> cases name <;> cases comment <;> simp [GzHead.flg]
77
78/-- The concrete header bytes of a valid header form a gzip member recognized by the format grammar. -/
79theorem gzip_decode_with_header {p : DeflParams} {h : GzHead} {stream output : List UInt8}
80    (hv : h.Valid) (hd : Gzip.DecodesWith (h.bytes p) stream output) :
81    Gzip.Decodes stream output := by
82  obtain ⟨rest, hs, hprefix⟩ := hd
83  obtain ⟨hf, hhcrc⟩ := header_flags h
84  refine ⟨h.flg.toUInt8, le32 h.time, (xflOf p).toUInt8, h.os.toUInt8,
85    h.extra.getD [], h.name.getD [], h.comment.getD [], rest, hf, ?_, ?_, ?_, ?_, ?_, hprefix⟩
86  · exact ZlibF.Spec.le32_length _
87  · cases he : h.extra with
88    | none => simp
89    | some e => simpa [he] using hv.1 e he
90  · cases hn : h.name with
91    | none => simp
92    | some name => simpa [hn] using hv.2.1 name hn
93  · cases hc : h.comment with
94    | none => simp
95    | some comment => simpa [hc] using hv.2.2 comment hc
96  · rw [hs]
97    simp only [GzHead.bytes, GzHead.core]
98    congr 1
99    split <;> simp_all
100
101/-- A precise completed gzip trace is a valid gzip stream. -/
102theorem gzip_trace_decodes {p : DeflParams} {x : List UInt8} {s : DeflState}
103    (hc : DeflCfg p) (hw : p.wrap = .gzip) (ht : DeflTrace x (DeflState.fresh p) s)
104    (hd : s.done = true) (hp : s.precise = true) (hi : s.input = x) :
105    Gzip.Decodes s.produced x := by
106  have hparam : s.params = p := by simpa [DeflState.fresh] using deflate_trace_params ht
107  have hv := deflate_valid p x s hc ht hd hp
108  have hd' : Gzip.DecodesWith (s.header.bytes p) s.produced x := by
109    simpa [DeflState.Valid, hparam, hw, hi] using hv
110  exact gzip_decode_with_header (deflate_trace_header_valid ht hp) hd'
111
112private theorem gzip_not_needs_dict {w : Wrap} {stream output : List UInt8}
113    (hd : Gzip.Decodes stream output) : ¬ HdrNeedsDict w 15 stream := by
114  obtain ⟨rest, hhead⟩ := ZlibF.Spec.gzip_head hd
115  rintro ⟨_, cmf, flg, r, hs, hh, _, _⟩
116  rw [hs] at hhead
117  simp only [List.cons.injEq] at hhead
118  have he : cmf = 31 := hhead.1
119  rw [he] at hh
120  exact (by decide : ¬ ((31 : UInt8).toNat % 16 = 8)) hh.1
121
122/-- The gzip and automatic-detection cases of the abstract round trip. -/
123theorem roundtrip_gzip {p : DeflParams} {x : List UInt8} {sd : DeflState} {si : InflState} {w : Wrap}
124    (hc : DeflCfg p) (hw : p.wrap = .gzip) (ht : DeflTrace x (DeflState.fresh p) sd)
125    (hd : sd.done = true) (hp : sd.precise = true) (hi : sd.input = x)
126    (hwrap : w = .gzip ∨ w = .auto)
127    (hr : InflTrace sd.produced sd.dictEff (InflStart w 15 sd.dictEff) si) :
128    si.phase ≠ .bad ∧ si.out <+: x ∧ (si.phase = .done → si.out = x ∧ si.seen = sd.produced) := by
129  have hcfg : InflCfg w 15 := by
130    rcases hwrap with rfl | rfl
131    · exact ⟨31, by decide⟩
132    · exact ⟨47, by decide⟩
133  have hwindow : FullWindow w 15 sd.produced := by
134    rcases hwrap with rfl | rfl
135    · exact Or.inr rfl
136    · exact Or.inl rfl
137  have hdecode : Layer.Decodes w 15 sd.dictEff sd.produced x := by
138    have h := gzip_trace_decodes hc hw ht hd hp hi
139    rcases hwrap with rfl | rfl
140    · exact h
141    · exact Or.inr h
142  have h := inflate_decodes w 15 sd.dictEff sd.produced x si hcfg hdecode hwindow hr
143  exact ⟨h.1, h.2.2.1, h.2.2.2.2⟩
144
145/-- The gzip cases of the no-dictionary model round-trip completion goal. -/
146theorem roundtrip_gzip_completes {p : DeflParams} {x : List UInt8} {sd : DeflState}
147    {si si' : InflState} {w : Wrap} {c : InflCall} {r : InflRes}
148    (hc : DeflCfg p) (hw : p.wrap = .gzip) (ht : DeflTrace x (DeflState.fresh p) sd)
149    (hd : sd.done = true) (hp : sd.precise = true) (hi : sd.input = x) (_hn : sd.dictEff = [])
150    (hwrap : w = .gzip ∨ w = .auto)
151    (hr : InflTrace sd.produced [] (InflStart w 15 []) si) (hphase : si.phase = .running)
152    (hbuf : c.badBuf = false) (hin : c.inp = sd.produced.drop si.seen.length)
153    (hroom : x.length ≤ si.out.length + c.availOut)
154    (hflush : c.flush = .noFlush ∨ c.flush = .syncFlush ∨ c.flush = .finish)
155    (hm : InflModel si (.inflate c) r si') :
156    (r.rc = Z.streamEnd ∧ r.out.produced = x.drop si.out.length) ∨ r.rc = Z.memError := by
157  have hcfg : InflCfg w 15 := by
158    rcases hwrap with rfl | rfl
159    · exact ⟨31, by decide⟩
160    · exact ⟨47, by decide⟩
161  have hwindow : FullWindow w 15 sd.produced := by
162    rcases hwrap with rfl | rfl
163    · exact Or.inr rfl
164    · exact Or.inl rfl
165  have hformat := gzip_trace_decodes hc hw ht hd hp hi
166  have hdecode : Layer.Decodes w 15 [] sd.produced x := by
167    rcases hwrap with rfl | rfl
168    · exact hformat
169    · exact Or.inr hformat
170  have hnodict := gzip_not_needs_dict (w := w) hformat
171  rcases inflate_completes w 15 [] sd.produced x si c r si' hcfg hdecode hwindow hnodict
172      hr hphase hbuf hin hroom hflush hm with ⟨h1, _, h2⟩ | hmem
173  · exact Or.inl ⟨h1, h2⟩
174  · exact Or.inr hmem
175
176/-- The abstract model round trip for every compatible wrapper and dictionary. -/
177theorem roundtrip : Goal.roundtrip := by
178  intro p x sd w b si hc hcompat ht hd hp hi hr
179  obtain ⟨_, rfl, hwrap⟩ := hcompat
180  rcases hwrap with ⟨hw, rfl⟩ | ⟨hw, hwrap⟩ | ⟨hw, hwrap⟩
181  · exact roundtrip_raw hc hw ht hd hp hi hr
182  · exact roundtrip_zlib hc hw ht hd hp hi hwrap hr
183  · exact roundtrip_gzip hc hw ht hd hp hi hwrap hr
184
185/-- The no-dictionary abstract round trip completes with enough output space, or reports allocation failure. -/
186theorem roundtrip_completes : Goal.roundtrip_completes := by
187  intro p x sd w b si c r si' hc hcompat ht hd hp hi hn hr hphase hbuf hin hroom hflush hm
188  obtain ⟨_, rfl, hwrap⟩ := hcompat
189  rcases hwrap with ⟨hw, rfl⟩ | ⟨hw, hwrap⟩ | ⟨hw, hwrap⟩
190  · exact roundtrip_raw_completes hc hw ht hd hp hi hn hr hphase hbuf hin hroom hflush hm
191  · exact roundtrip_zlib_completes hc hw ht hd hp hi hn hwrap hr hphase hbuf hin hroom hflush hm
192  · exact roundtrip_gzip_completes hc hw ht hd hp hi hn hwrap hr hphase hbuf hin hroom hflush hm
193
194#print axioms roundtrip
195#print axioms roundtrip_completes
196#print axioms gzip_decode_with_header
197#print axioms deflate_trace_header_valid
198end ZlibF.Spec.Api.Proofs