Deflate.lean

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

1import ZlibF.Spec.Api.Examples
2
3/-!
4# Deflate model: validity of a completed stream
5
6The proof uses only the existing model relations and format grammar. In particular, replacing a raw
7preset dictionary after an empty-input stream is allowed; decoding an empty output does not depend
8on the dictionary.
9-/
10
11namespace ZlibF.Spec.Api.Proofs
12open ZlibF.Spec
13
14private theorem copyBack_length (dict : List UInt8) (dist n : Nat) (h : List UInt8) :
15    (copyBack dict dist n h).length = h.length + n := by
16  induction n generalizing h with
17  | zero => rfl
18  | succ n ih => simp [copyBack, ih]; omega
19
20private theorem symbols_empty_dict {L D : List Nat} {dict h out : List UInt8} {inp rest : List Bool}
21    (hs : Symbols L D dict h inp rest out) (he : out = []) (dict' : List UInt8) :
22    h = [] ∧ Symbols L D dict' [] inp rest [] := by
23  induction hs with
24  | eob hd => subst he; exact ⟨rfl, .eob hd⟩
25  | lit hd hlt hs ih =>
26    have hn := (ih he).1
27    simp at hn
28  | @copy h inp r1 r2 r3 r4 rest s d xl xd out hd h1 h2 hr1 hd2 h3 hr2 hb hs ih =>
29    have hn := (ih he).1
30    have hl := congrArg List.length hn
31    rw [copyBack_length] at hl
32    have hbase : 0 < lengthBases.getD (s - 257) 0 :=
33      (by decide : ∀ i, i < 29 → 0 < lengthBases.getD i 0) (s - 257) (by omega)
34    simp only [List.length_nil] at hl
35    omega
36
37private theorem body_empty_dict {dict h out : List UInt8} {bt : Nat} {inp rest : List Bool}
38    (hs : Body dict bt h inp rest out) (he : out = []) (dict' : List UInt8) :
39    h = [] ∧ Body dict' bt [] inp rest [] := by
40  cases hs with
41  | stored h1 h2 h3 h4 =>
42    obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.mp he
43    exact ⟨rfl, .stored h1 h2 h3 h4⟩
44  | fixed hs =>
45    obtain ⟨rfl, hs'⟩ := symbols_empty_dict hs he dict'
46    exact ⟨rfl, .fixed hs'⟩
47  | dynamic h1 h2 h3 hc h4 ha hl heob hL hD hs =>
48    obtain ⟨rfl, hs'⟩ := symbols_empty_dict hs he dict'
49    exact ⟨rfl, .dynamic h1 h2 h3 hc h4 ha hl heob hL hD hs'⟩
50
51private theorem blocks_empty_dict {dict h out : List UInt8} {inp rest : List Bool}
52    (hs : Blocks dict h inp rest out) (he : out = []) (dict' : List UInt8) :
53    h = [] ∧ Blocks dict' [] inp rest [] := by
54  induction hs with
55  | last h1 h2 hb =>
56    obtain ⟨rfl, hb'⟩ := body_empty_dict hb he dict'
57    exact ⟨rfl, .last h1 h2 hb'⟩
58  | more h1 h2 hb hs ih =>
59    obtain ⟨hempty, hs'⟩ := ih he
60    obtain ⟨rfl, hb'⟩ := body_empty_dict hb hempty dict'
61    exact ⟨rfl, .more h1 h2 hb' hs'⟩
62
63/-- An empty decoded raw stream remains empty after replacing its preset dictionary. -/
64theorem deflate_empty_dictionary_independent {dict stream : List UInt8}
65    (hs : Deflate.Decodes dict stream []) (dict' : List UInt8) : Deflate.Decodes dict' stream [] := by
66  obtain ⟨rest, hblocks, hrest⟩ := hs
67  exact ⟨rest, (blocks_empty_dict hblocks rfl dict').2, hrest⟩
68
69private theorem valid_state_eq {st st' : DeflState} {produced input : List UInt8}
70    (hp : st'.params = st.params) (hd : st'.dict = st.dict) (hh : st'.hdr = st.hdr)
71    (hv : st.Valid produced input) : st'.Valid produced input := by
72  simpa only [DeflState.Valid, DeflState.dictEff, DeflState.header, hp, hd, hh] using hv
73
74private theorem run_preserves_complete {st st' : DeflState} {c : DeflCall} {o : DeflOut}
75    (hr : DeflRun st c o st')
76    (hprev : st.done = true → st.started = true ∧ (st.precise = true → st.Valid st.produced st.input)) :
77    st'.done = true → st'.started = true ∧ (st'.precise = true → st'.Valid st'.produced st'.input) := by
78  rcases hr with ⟨hf, hp, hpr, hstart, _, _, _, _, _, hend, _, _, _, _, hdone, _, _, hstable,
79    _, _, _, _, hstarted, _⟩
80  rcases hf with ⟨_, _, hi, ho, _, _, hd, hh⟩
81  intro hdone'
82  by_cases hd0 : st.done = true
83  · have hstarted' := hstarted (hprev hd0).1
84    refine ⟨hstarted', fun hprec' => ?_⟩
85    have hprec : st.precise = true := hpr.symm.trans hprec'
86    have hv := valid_state_eq hp hd hh ((hprev hd0).2 hprec)
87    have hn := hstable hd0
88    simpa only [hi, ho, hn.1, hn.2, List.take_zero, List.append_nil] using hv
89  · have hrc := (hdone.mp hdone').resolve_left hd0
90    obtain ⟨_, _, _, _, _, _, hv, _, _⟩ := hend hrc
91    refine ⟨(hstart (Or.inr hrc)).1, fun hprec' => ?_⟩
92    have hprec : st.precise = true := hpr.symm.trans hprec'
93    have hvalid := valid_state_eq hp hd hh (hv hprec)
94    simpa only [hi, ho] using hvalid
95
96private theorem step_preserves_complete {st st' : DeflState} {c : DeflCall} {o : DeflOut}
97    (hr : DeflStep st c o st')
98    (hprev : st.done = true → st.started = true ∧ (st.precise = true → st.Valid st.produced st.input)) :
99    st'.done = true → st'.started = true ∧ (st'.precise = true → st'.Valid st'.produced st'.input) := by
100  by_cases ht : c.flush = .trees
101  · have he := (hr.1 ht).2.2.2
102    subst st'; exact hprev
103  by_cases hb : c.badBuf = true ∨ (st.finishing = true ∧ c.flush ≠ .finish)
104  · have he := (hr.2.1 ht hb).2.2.2
105    subst st'; exact hprev
106  have hbuf : c.badBuf = false := by cases h : c.badBuf <;> simp_all
107  have hnfin : ¬ (st.finishing = true ∧ c.flush ≠ .finish) := fun h => hb (Or.inr h)
108  by_cases hz : c.availOut = 0
109  · have he := (hr.2.2.1 ht hbuf hnfin hz).2.2.2
110    subst st'; exact hprev
111  exact run_preserves_complete (hr.2.2.2 ht hbuf hnfin hz) hprev
112
113private theorem dict_preserves_complete {st st' : DeflState} {d : List UInt8} {rc : Int}
114    (hr : DeflSetDict st d rc st')
115    (hprev : st.done = true → st.started = true ∧ (st.precise = true → st.Valid st.produced st.input)) :
116    st'.done = true → st'.started = true ∧ (st'.precise = true → st'.Valid st'.produced st'.input) := by
117  cases hw : st.params.wrap with
118  | gzip =>
119    simp only [DeflSetDict, hw] at hr
120    rcases hr with ⟨_, rfl⟩
121    exact hprev
122  | zlib =>
123    simp only [DeflSetDict, hw] at hr
124    split at hr
125    · rcases hr with ⟨_, rfl⟩
126      exact hprev
127    · rename_i hn
128      rcases hr with ⟨_, rfl⟩
129      intro hd
130      exact (hn (hprev hd).1).elim
131  | raw =>
132    simp only [DeflSetDict, hw] at hr
133    split at hr
134    · rename_i hi
135      rcases hr with ⟨_, rfl⟩
136      intro hd
137      refine ⟨(hprev hd).1, fun hprec => ?_⟩
138      have hv := (hprev hd).2 hprec
139      have hraw : Deflate.Decodes (st.dictEff.drop (st.dictEff.length - 2 ^ st.params.wbits)) st.produced [] := by
140        simpa only [DeflState.Valid, hw, hi] using hv
141      have hnew := deflate_empty_dictionary_independent hraw (d.drop (d.length - 2 ^ st.params.wbits))
142      simpa only [DeflState.Valid, hw, DeflState.dictEff, Option.getD_some, hi] using hnew
143    · rcases hr with ⟨_, rfl⟩ | ⟨_, rfl⟩
144      · exact hprev
145      · intro hd
146        refine ⟨(hprev hd).1, fun hprec => ?_⟩
147        cases hprec
148
149private theorem header_preserves_complete {st st' : DeflState} {h : GzHead} {rc : Int}
150    (hr : DeflSetHeader st h rc st')
151    (hprev : st.done = true → st.started = true ∧ (st.precise = true → st.Valid st.produced st.input)) :
152    st'.done = true → st'.started = true ∧ (st'.precise = true → st'.Valid st'.produced st'.input) := by
153  unfold DeflSetHeader at hr
154  split at hr
155  · rcases hr with ⟨_, rfl⟩
156    exact hprev
157  · rcases hr with ⟨_, hbad, hgood⟩
158    by_cases hb : st.started = true ∨ ¬ h.Valid
159    · obtain rfl := hbad hb
160      intro hd
161      refine ⟨(hprev hd).1, fun hprec => ?_⟩
162      cases hprec
163    · obtain rfl := hgood hb
164      intro hd
165      exact (hb (Or.inl (hprev hd).1)).elim
166
167/-- A deflate trace preserves the validity of every precise completed stream and the fact that a
168completed stream has started. This includes raw dictionary replacement after an empty-input stream. -/
169theorem deflate_trace_completed {X : List UInt8} {st st' : DeflState} (ht : DeflTrace X st st')
170    (hprev : st.done = true → st.started = true ∧ (st.precise = true → st.Valid st.produced st.input)) :
171    st'.done = true → st'.started = true ∧ (st'.precise = true → st'.Valid st'.produced st'.input) := by
172  induction ht with
173  | nil => exact hprev
174  | step _ hm _ ih => exact ih (step_preserves_complete hm.1 hprev)
175  | dict hm _ ih => exact ih (dict_preserves_complete hm hprev)
176  | header hm _ ih => exact ih (header_preserves_complete hm hprev)
177
178/-- Every precise completed trace of the deflate model has produced a complete stream of its
179configured wrapper for the input it accepted. The parameter and trace domains are exactly those
180of `Goal.deflate_valid`. -/
181theorem deflate_valid : Goal.deflate_valid := by
182  intro p x st _ ht hd hprec
183  exact (deflate_trace_completed ht (by simp [DeflState.fresh]) hd).2 hprec
184
185/-- A buffer-error return after the example finished stream cannot clear its historical `started`
186flag. This excludes the refusal-and-dictionary counterexample found before the monotonicity clause. -/
187theorem deflate_refusal_keeps_started {c : DeflCall} {o : DeflOut} {st' : DeflState}
188    (hr : DeflRun dDoneA c o st') (_hbuf : o.rc = Z.bufError) : st'.started = true := by
189  rcases hr with ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, hstarted, _⟩
190  exact hstarted rfl
191
192end ZlibF.Spec.Api.Proofs