Roundtrip.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.Dictionary
2import ZlibF.Proof.Api.DeflateFlush
3import ZlibF.Proof.Api.Inflate
4
5namespace ZlibF.Spec.Api.Proofs
6open ZlibF.Spec
7
8/-- Configurations accepted by the deflate initializer use at most 15 window bits. -/
9theorem deflate_config_window_limit (p : DeflParams) (h : DeflCfg p) : p.wbits ≤ 15 := by
10  obtain ⟨level, method, bits, mem, strategy, he⟩ := h
11  simp only [deflInit?] at he
12  split at he <;> (try simp_all)
13  all_goals split at he <;> (try simp_all)
14  all_goals split at he <;> (try simp_all)
15  all_goals obtain ⟨hc, hp⟩ := he
16  all_goals subst p
17  all_goals simp_all
18  all_goals omega
19
20/-- A completed raw deflate model trace is valid for a full-window raw decoder. -/
21theorem raw_trace_decodes {p : DeflParams} {x : List UInt8} {s : DeflState}
22    (hc : DeflCfg p) (hw : p.wrap = .raw) (ht : DeflTrace x (DeflState.fresh p) s)
23    (hd : s.done = true) (hp : s.precise = true) (hi : s.input = x) :
24    Layer.Decodes .raw 15 s.dictEff s.produced x := by
25  have hparam : s.params = p := by simpa [DeflState.fresh] using deflate_trace_params ht
26  have hv := deflate_valid p x s hc ht hd hp
27  have hd : Deflate.Decodes (s.dictEff.drop (s.dictEff.length - 2 ^ p.wbits)) s.produced x := by
28    simpa [DeflState.Valid, hparam, hw, hi] using hv
29  exact ZlibF.Spec.Proofs.raw_full_window (deflate_config_window_limit p hc) hd
30
31/-- The raw case of the abstract round trip, for every legal compressor window and dictionary.
32Implementation refinement and the wrapped cases remain separate. -/
33theorem roundtrip_raw {p : DeflParams} {x : List UInt8} {sd : DeflState} {si : InflState}
34    (hc : DeflCfg p) (hw : p.wrap = .raw) (ht : DeflTrace x (DeflState.fresh p) sd)
35    (hd : sd.done = true) (hp : sd.precise = true) (hi : sd.input = x)
36    (hr : InflTrace sd.produced sd.dictEff (InflStart .raw 15 sd.dictEff) si) :
37    si.phase ≠ .bad ∧ si.out <+: x ∧ (si.phase = .done → si.out = x ∧ si.seen = sd.produced) := by
38  have hcfg : InflCfg .raw 15 := ⟨-15, by decide⟩
39  have hwindow : FullWindow .raw 15 sd.produced := rfl
40  have h := inflate_decodes .raw 15 sd.dictEff sd.produced x si hcfg
41    (raw_trace_decodes hc hw ht hd hp hi) hwindow hr
42  exact ⟨h.1, h.2.2.1, h.2.2.2.2⟩
43
44/-- A completed zlib-wrapped trace is valid for a full-window zlib or auto decoder. -/
45theorem zlib_trace_decodes {p : DeflParams} {x : List UInt8} {s : DeflState} {w : Wrap}
46    (hc : DeflCfg p) (hw : p.wrap = .zlib) (ht : DeflTrace x (DeflState.fresh p) s)
47    (hd : s.done = true) (hp : s.precise = true) (hi : s.input = x)
48    (hwrap : w = .zlib ∨ w = .auto) :
49    Layer.Decodes w 15 s.dictEff s.produced x := by
50  have hparam : s.params = p := by simpa [DeflState.fresh] using deflate_trace_params ht
51  have hv := deflate_valid p x s hc ht hd hp
52  have hv' : Zlib.Decodes s.dictEff s.produced x ∧
53      s.produced.head?.map (·.toNat / 16 + 8) = some p.wbits ∧
54      ∃ cmf flg r, s.produced = cmf :: flg :: r ∧ (flg.toNat / 32 % 2 = 1 ↔ s.dictEff ≠ []) := by
55    simpa [DeflState.Valid, hparam, hw, hi] using hv
56  have hf : ZlibFits 15 s.produced := by
57    cases hh : s.produced.head? with
58    | none => simp [hh] at hv'
59    | some c =>
60      have he : c.toNat / 16 + 8 = p.wbits := by simpa [hh] using hv'.2.1
61      exact Or.inr ⟨c, hh, by rw [he]; exact deflate_config_window_limit p hc⟩
62  rcases hwrap with rfl | rfl
63  · exact ⟨hv'.1, hf⟩
64  · exact Or.inl ⟨hv'.1, hf⟩
65
66/-- The zlib and automatic-detection cases of the abstract round trip. -/
67theorem roundtrip_zlib {p : DeflParams} {x : List UInt8} {sd : DeflState} {si : InflState} {w : Wrap}
68    (hc : DeflCfg p) (hw : p.wrap = .zlib) (ht : DeflTrace x (DeflState.fresh p) sd)
69    (hd : sd.done = true) (hp : sd.precise = true) (hi : sd.input = x)
70    (hwrap : w = .zlib ∨ w = .auto)
71    (hr : InflTrace sd.produced sd.dictEff (InflStart w 15 sd.dictEff) si) :
72    si.phase ≠ .bad ∧ si.out <+: x ∧ (si.phase = .done → si.out = x ∧ si.seen = sd.produced) := by
73  have hcfg : InflCfg w 15 := by
74    rcases hwrap with rfl | rfl
75    · exact ⟨15, by decide⟩
76    · exact ⟨47, by decide⟩
77  have hwindow : FullWindow w 15 sd.produced := by
78    rcases hwrap with rfl | rfl <;> exact Or.inl rfl
79  have h := inflate_decodes w 15 sd.dictEff sd.produced x si hcfg
80    (zlib_trace_decodes hc hw ht hd hp hi hwrap) hwindow hr
81  exact ⟨h.1, h.2.2.1, h.2.2.2.2⟩
82
83/-- With an empty effective dictionary, a zlib trace does not request one in its header. -/
84theorem zlib_trace_no_dictionary {p : DeflParams} {x : List UInt8} {sd : DeflState} {w : Wrap}
85    (hc : DeflCfg p) (hw : p.wrap = .zlib) (ht : DeflTrace x (DeflState.fresh p) sd)
86    (hd : sd.done = true) (hp : sd.precise = true) (hi : sd.input = x) (hn : sd.dictEff = []) :
87    ¬ HdrNeedsDict w 15 sd.produced := by
88  have hparam : sd.params = p := by simpa [DeflState.fresh] using deflate_trace_params ht
89  have hv := deflate_valid p x sd hc ht hd hp
90  have hv' : Zlib.Decodes sd.dictEff sd.produced x ∧
91      sd.produced.head?.map (·.toNat / 16 + 8) = some p.wbits ∧
92      ∃ cmf flg r, sd.produced = cmf :: flg :: r ∧ (flg.toNat / 32 % 2 = 1 ↔ sd.dictEff ≠ []) := by
93    simpa [DeflState.Valid, hparam, hw, hi] using hv
94  have hflag := hv'.2.2
95  rintro ⟨_, cmf, flg, rest, he, _, hset, _⟩
96  obtain ⟨cmf', flg', rest', he', hf⟩ := hflag
97  rw [he] at he'
98  simp only [List.cons.injEq] at he'
99  obtain ⟨rfl, rfl, _⟩ := he'
100  exact (hf.mp hset) hn
101
102/-- The no-dictionary zlib and auto round trips complete in the model with enough output space. -/
103theorem roundtrip_zlib_completes {p : DeflParams} {x : List UInt8} {sd : DeflState}
104    {si si' : InflState} {w : Wrap} {c : InflCall} {r : InflRes}
105    (hc : DeflCfg p) (hw : p.wrap = .zlib) (ht : DeflTrace x (DeflState.fresh p) sd)
106    (hd : sd.done = true) (hp : sd.precise = true) (hi : sd.input = x) (hn : sd.dictEff = [])
107    (hwrap : w = .zlib ∨ w = .auto)
108    (hr : InflTrace sd.produced [] (InflStart w 15 []) si) (hphase : si.phase = .running)
109    (hbuf : c.badBuf = false) (hin : c.inp = sd.produced.drop si.seen.length)
110    (hroom : x.length ≤ si.out.length + c.availOut)
111    (hflush : c.flush = .noFlush ∨ c.flush = .syncFlush ∨ c.flush = .finish)
112    (hm : InflModel si (.inflate c) r si') :
113    (r.rc = Z.streamEnd ∧ r.out.produced = x.drop si.out.length) ∨ r.rc = Z.memError := by
114  have hcfg : InflCfg w 15 := by
115    rcases hwrap with rfl | rfl
116    · exact ⟨15, by decide⟩
117    · exact ⟨47, by decide⟩
118  have hdecode : Layer.Decodes w 15 [] sd.produced x := by
119    simpa [hn] using zlib_trace_decodes hc hw ht hd hp hi hwrap
120  have hwindow : FullWindow w 15 sd.produced := by
121    rcases hwrap with rfl | rfl <;> exact Or.inl rfl
122  have hnodict := zlib_trace_no_dictionary (w := w) hc hw ht hd hp hi hn
123  rcases inflate_completes w 15 [] sd.produced x si c r si' hcfg hdecode hwindow hnodict
124      hr hphase hbuf hin hroom hflush hm with ⟨h1, _, h2⟩ | hmem
125  · exact Or.inl ⟨h1, h2⟩
126  · exact Or.inr hmem
127
128/-- The no-dictionary raw round trip completes in the model when output space is sufficient. -/
129theorem roundtrip_raw_completes {p : DeflParams} {x : List UInt8} {sd : DeflState} {si si' : InflState}
130    {c : InflCall} {r : InflRes}
131    (hc : DeflCfg p) (hw : p.wrap = .raw) (ht : DeflTrace x (DeflState.fresh p) sd)
132    (hd : sd.done = true) (hp : sd.precise = true) (hi : sd.input = x) (hn : sd.dictEff = [])
133    (hr : InflTrace sd.produced [] (InflStart .raw 15 []) si) (hphase : si.phase = .running)
134    (hbuf : c.badBuf = false) (hin : c.inp = sd.produced.drop si.seen.length)
135    (hroom : x.length ≤ si.out.length + c.availOut)
136    (hflush : c.flush = .noFlush ∨ c.flush = .syncFlush ∨ c.flush = .finish)
137    (hm : InflModel si (.inflate c) r si') :
138    (r.rc = Z.streamEnd ∧ r.out.produced = x.drop si.out.length) ∨ r.rc = Z.memError := by
139  have hcfg : InflCfg .raw 15 := ⟨-15, by decide⟩
140  have hdecode : Layer.Decodes .raw 15 [] sd.produced x := by
141    simpa [hn] using raw_trace_decodes hc hw ht hd hp hi
142  have hwindow : FullWindow .raw 15 sd.produced := rfl
143  have hnodict : ¬ HdrNeedsDict .raw 15 sd.produced := by simp [HdrNeedsDict]
144  rcases inflate_completes .raw 15 [] sd.produced x si c r si' hcfg hdecode hwindow hnodict
145      hr hphase hbuf hin hroom hflush hm with ⟨h1, _, h2⟩ | hmem
146  · exact Or.inl ⟨h1, h2⟩
147  · exact Or.inr hmem
148
149#print axioms roundtrip_raw
150#print axioms roundtrip_raw_completes
151#print axioms roundtrip_zlib
152#print axioms roundtrip_zlib_completes
153end ZlibF.Spec.Api.Proofs