DeflateFlush.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.DeflateBounds
2
3namespace ZlibF.Spec.Api.Proofs
4open ZlibF.Spec
5
6private def FlushInvariant (s : DeflState) : Prop :=
7  s.done = true → s.started = true ∧ s.finishing = true ∧
8    (s.precise = true → s.params.wrap = .raw → s.dict = none → ∀ pl il,
9      s.fullAt = some (pl, il) → Deflate.Decodes [] (s.produced.drop pl) (s.input.drop il))
10
11private theorem flush_run {st st' : DeflState} {c : DeflCall} {o : DeflOut}
12    (hr : DeflRun st c o st') (hroom : c.availOut ≠ 0)
13    (hfinish : st.done = true → c.flush = .finish) (hp : FlushInvariant st) : FlushInvariant st' := by
14  rcases hr with ⟨hf, hparams, hprec, hstart, hrcs, _, _, _, hokfinish, hend, _, _, _, hfullold, hdone, _, hbuf,
15    hstable, _, _, _, _, hstarted, _⟩
16  rcases hf with ⟨_, _, hi, ho, _, _, hd, _⟩
17  intro hdone'
18  by_cases hd0 : st.done = true
19  · have hs := hstable hd0
20    have hfinish' := hfinish hd0
21    have hrnot : o.rc ≠ Z.ok := by
22      intro he
23      have := hokfinish he hfinish'
24      rw [hs.2] at this
25      simp only [List.length_nil] at this
26      exact hroom this.symm
27    have hfin : st'.finishing = true := by
28      rcases hrcs with he | he | he
29      · exact (hrnot he).elim
30      · exact (hend he).2.2.2.1
31      · exact (hbuf he).2.trans (hp hd0).2.1
32    refine ⟨hstarted (hp hd0).1, hfin, fun hpr hw hdict pl il hfull => ?_⟩
33    have hold : st'.fullAt = st.fullAt := by
34      apply hfullold
35      intro hcontra
36      have he : Flush.finish = Flush.fullFlush := hfinish'.symm.trans hcontra.2.2
37      cases he
38    have hprior := (hp hd0).2.2 (hprec.symm.trans hpr) (by simpa [hparams] using hw)
39      (by simpa [hd] using hdict) pl il (by simpa [hold] using hfull)
40    simpa only [hi, ho, hs.1, hs.2, List.take_zero, List.append_nil] using hprior
41  · have hrc := (hdone.mp hdone').resolve_left hd0
42    refine ⟨(hstart (Or.inr hrc)).1, (hend hrc).2.2.2.1, fun hpr hw hdict pl il hfull => ?_⟩
43    have hold : st'.fullAt = st.fullAt := by
44      apply hfullold
45      intro hc
46      have he : Z.ok = Z.streamEnd := hc.1.symm.trans hrc
47      cases he
48    have hprior := (hend hrc).2.2.2.2.2.2.2.1 (hprec.symm.trans hpr)
49      (by simpa [hparams] using hw) (by simpa [hd] using hdict) pl il (by simpa [hold] using hfull)
50    simpa only [hi, ho] using hprior
51
52private theorem flush_step {st st' : DeflState} {c : DeflCall} {o : DeflOut}
53    (hr : DeflStep st c o st') (hp : FlushInvariant st) : FlushInvariant st' := by
54  by_cases ht : c.flush = .trees
55  · have he := (hr.1 ht).2.2.2
56    subst st'; exact hp
57  by_cases hb : c.badBuf = true ∨ (st.finishing = true ∧ c.flush ≠ .finish)
58  · have he := (hr.2.1 ht hb).2.2.2
59    subst st'; exact hp
60  have hbuf : c.badBuf = false := by cases h : c.badBuf <;> simp_all
61  have hnfin : ¬ (st.finishing = true ∧ c.flush ≠ .finish) := fun h => hb (Or.inr h)
62  by_cases hz : c.availOut = 0
63  · have he := (hr.2.2.1 ht hbuf hnfin hz).2.2.2
64    subst st'; exact hp
65  have hfinish : st.done = true → c.flush = .finish := by
66    intro hd
67    by_cases he : c.flush = .finish
68    · exact he
69    · exact (hnfin ⟨(hp hd).2.1, he⟩).elim
70  exact flush_run (hr.2.2.2 ht hbuf hnfin hz) hz hfinish hp
71
72private theorem flush_dict {st st' : DeflState} {d : List UInt8} {rc : Int}
73    (hr : DeflSetDict st d rc st') (hp : FlushInvariant st) : FlushInvariant st' := by
74  cases hw : st.params.wrap with
75  | gzip => simp only [DeflSetDict, hw] at hr; rcases hr with ⟨_, rfl⟩; exact hp
76  | zlib =>
77    simp only [DeflSetDict, hw] at hr
78    split at hr
79    · rcases hr with ⟨_, rfl⟩; exact hp
80    · rename_i hn
81      rcases hr with ⟨_, rfl⟩
82      intro hd
83      exact (hn (hp hd).1).elim
84  | raw =>
85    simp only [DeflSetDict, hw] at hr
86    split at hr
87    · rcases hr with ⟨_, rfl⟩
88      intro hd
89      refine ⟨(hp hd).1, (hp hd).2.1, ?_⟩
90      intro _ _ hdict
91      cases hdict
92    · rcases hr with ⟨_, rfl⟩ | ⟨_, rfl⟩
93      · exact hp
94      · intro hd
95        refine ⟨(hp hd).1, (hp hd).2.1, ?_⟩
96        intro hprec
97        cases hprec
98
99private theorem flush_header {st st' : DeflState} {h : GzHead} {rc : Int}
100    (hr : DeflSetHeader st h rc st') (hp : FlushInvariant st) : FlushInvariant st' := by
101  unfold DeflSetHeader at hr
102  split at hr
103  · rcases hr with ⟨_, rfl⟩; exact hp
104  · rcases hr with ⟨_, hbad, hgood⟩
105    by_cases hb : st.started = true ∨ ¬ h.Valid
106    · obtain rfl := hbad hb
107      intro hd
108      refine ⟨(hp hd).1, (hp hd).2.1, ?_⟩
109      intro hprec
110      cases hprec
111    · obtain rfl := hgood hb
112      intro hd
113      exact (hb (Or.inl (hp hd).1)).elim
114
115private theorem trace_flush {X : List UInt8} {st st' : DeflState} (ht : DeflTrace X st st')
116    (hp : FlushInvariant st) : FlushInvariant st' := by
117  induction ht with
118  | nil => exact hp
119  | step _ hm _ ih => exact ih (flush_step hm.1 hp)
120  | dict hm _ ih => exact ih (flush_dict hm hp)
121  | header hm _ ih => exact ih (flush_header hm hp)
122
123private theorem params_step {st st' : DeflState} {c : DeflCall} {o : DeflOut}
124    (hr : DeflStep st c o st') : st'.params = st.params := by
125  by_cases ht : c.flush = .trees
126  · rw [(hr.1 ht).2.2.2]
127  by_cases hb : c.badBuf = true ∨ (st.finishing = true ∧ c.flush ≠ .finish)
128  · rw [(hr.2.1 ht hb).2.2.2]
129  have hbuf : c.badBuf = false := by cases h : c.badBuf <;> simp_all
130  have hnfin : ¬ (st.finishing = true ∧ c.flush ≠ .finish) := fun h => hb (Or.inr h)
131  by_cases hz : c.availOut = 0
132  · rw [(hr.2.2.1 ht hbuf hnfin hz).2.2.2]
133  exact (hr.2.2.2 ht hbuf hnfin hz).2.1
134
135private theorem params_dict {st st' : DeflState} {d : List UInt8} {rc : Int}
136    (hr : DeflSetDict st d rc st') : st'.params = st.params := by
137  cases hw : st.params.wrap with
138  | gzip => simp only [DeflSetDict, hw] at hr; rcases hr with ⟨_, rfl⟩; rfl
139  | zlib =>
140    simp only [DeflSetDict, hw] at hr
141    split at hr <;> rcases hr with ⟨_, rfl⟩ <;> rfl
142  | raw =>
143    simp only [DeflSetDict, hw] at hr
144    split at hr
145    · rcases hr with ⟨_, rfl⟩; rfl
146    · rcases hr with ⟨_, rfl⟩ | ⟨_, rfl⟩ <;> rfl
147
148private theorem params_header {st st' : DeflState} {h : GzHead} {rc : Int}
149    (hr : DeflSetHeader st h rc st') : st'.params = st.params := by
150  unfold DeflSetHeader at hr
151  split at hr
152  · rcases hr with ⟨_, rfl⟩; rfl
153  · rcases hr with ⟨_, hbad, hgood⟩
154    by_cases hb : st.started = true ∨ ¬ h.Valid
155    · rw [hbad hb]
156    · rw [hgood hb]
157
158/-- Deflate calls, dictionary updates, and header updates preserve stream parameters. -/
159theorem deflate_trace_params {X : List UInt8} {st st' : DeflState} (ht : DeflTrace X st st') :
160    st'.params = st.params := by
161  induction ht with
162  | nil => rfl
163  | step _ hm _ ih => exact ih.trans (params_step hm.1)
164  | dict hm _ ih => exact ih.trans (params_dict hm)
165  | header hm _ ih => exact ih.trans (params_header hm)
166
167/-- The abstract completed raw-stream trace retains the independent full-flush suffix.
168Refinement of the translated compressor is a separate obligation. -/
169theorem deflate_full_flush_resync : Goal.deflate_full_flush_resync := by
170  intro p x s pl il _ hw ht hd hp hdict hfull
171  have hparams : s.params = p := by simpa [DeflState.fresh] using deflate_trace_params ht
172  exact (trace_flush ht (by simp [FlushInvariant, DeflState.fresh]) hd).2.2 hp
173    (by simpa [hparams] using hw) hdict pl il hfull
174
175#print axioms deflate_full_flush_resync
176end ZlibF.Spec.Api.Proofs