DeflateBounds.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.Deflate
2
3namespace ZlibF.Spec.Api.Proofs
4open ZlibF.Spec
5
6private def BoundInvariant (s : DeflState) : Prop :=
7  s.done = true → s.started = true ∧ (s.clean = true → s.produced.length ≤ s.bound s.input.length)
8
9private theorem bound_run {st st' : DeflState} {c : DeflCall} {o : DeflOut}
10    (hr : DeflRun st c o st') (hp : BoundInvariant st) : BoundInvariant st' := by
11  rcases hr with ⟨hf, hparams, _, hstart, _, _, _, _, _, hend, _, _, _, _, hdone, _, _, hstable,
12    _, hclean, _, _, hstarted, _⟩
13  rcases hf with ⟨_, _, hi, ho, _, _, hd, hh⟩
14  intro hdone'
15  by_cases hd0 : st.done = true
16  · refine ⟨hstarted (hp hd0).1, fun hc => ?_⟩
17    have hb := (hp hd0).2 (hclean hc)
18    have he := hstable hd0
19    have hbound : st'.bound st'.input.length = st.bound st.input.length := by
20      simp only [DeflState.bound, DeflState.header, DeflState.dictEff, hparams, hd, hh, hi,
21        he.1, List.take_zero, List.append_nil]
22      rfl
23    simpa only [ho, he.2, List.append_nil, hbound] using hb
24  · have hrc := (hdone.mp hdone').resolve_left hd0
25    refine ⟨(hstart (Or.inr hrc)).1, fun hc => ?_⟩
26    have hb := (hend hrc).2.2.2.2.2.2.2.2 (hclean hc)
27    have hbound : st'.bound st'.input.length = st.bound (st.input ++ c.inp.take o.consumed).length := by
28      simp only [DeflState.bound, DeflState.header, DeflState.dictEff, hparams, hd, hh, hi]
29      rfl
30    simpa only [ho, hbound] using hb
31
32private theorem bound_step {st st' : DeflState} {c : DeflCall} {o : DeflOut}
33    (hr : DeflStep st c o st') (hp : BoundInvariant st) : BoundInvariant st' := by
34  by_cases ht : c.flush = .trees
35  · have he := (hr.1 ht).2.2.2
36    subst st'; exact hp
37  by_cases hb : c.badBuf = true ∨ (st.finishing = true ∧ c.flush ≠ .finish)
38  · have he := (hr.2.1 ht hb).2.2.2
39    subst st'; exact hp
40  have hbuf : c.badBuf = false := by cases h : c.badBuf <;> simp_all
41  have hnfin : ¬ (st.finishing = true ∧ c.flush ≠ .finish) := fun h => hb (Or.inr h)
42  by_cases hz : c.availOut = 0
43  · have he := (hr.2.2.1 ht hbuf hnfin hz).2.2.2
44    subst st'; exact hp
45  exact bound_run (hr.2.2.2 ht hbuf hnfin hz) hp
46
47private theorem bound_dict {st st' : DeflState} {d : List UInt8} {rc : Int}
48    (hr : DeflSetDict st d rc st') (hp : BoundInvariant st) : BoundInvariant st' := by
49  cases hw : st.params.wrap with
50  | gzip =>
51    simp only [DeflSetDict, hw] at hr
52    rcases hr with ⟨_, rfl⟩
53    exact hp
54  | zlib =>
55    simp only [DeflSetDict, hw] at hr
56    split at hr
57    · rcases hr with ⟨_, rfl⟩
58      exact hp
59    · rename_i hn
60      rcases hr with ⟨_, rfl⟩
61      intro hd
62      exact (hn (hp hd).1).elim
63  | raw =>
64    simp only [DeflSetDict, hw] at hr
65    split at hr
66    · rcases hr with ⟨_, rfl⟩
67      intro hd
68      refine ⟨(hp hd).1, fun hc => ?_⟩
69      have hb := (hp hd).2 hc
70      simpa only [DeflState.bound, DeflState.header, DeflState.dictEff, hw] using hb
71    · rcases hr with ⟨_, rfl⟩ | ⟨_, rfl⟩
72      · exact hp
73      · intro hd
74        refine ⟨(hp hd).1, fun hc => ?_⟩
75        cases hc
76
77private theorem bound_header {st st' : DeflState} {h : GzHead} {rc : Int}
78    (hr : DeflSetHeader st h rc st') (hp : BoundInvariant st) : BoundInvariant st' := by
79  unfold DeflSetHeader at hr
80  split at hr
81  · rcases hr with ⟨_, rfl⟩
82    exact hp
83  · rcases hr with ⟨_, hbad, hgood⟩
84    by_cases hb : st.started = true ∨ ¬ h.Valid
85    · obtain rfl := hbad hb
86      intro hd
87      refine ⟨(hp hd).1, fun hc => ?_⟩
88      cases hc
89    · obtain rfl := hgood hb
90      intro hd
91      exact (hb (Or.inl (hp hd).1)).elim
92
93private theorem trace_bound {X : List UInt8} {st st' : DeflState} (ht : DeflTrace X st st')
94    (hp : BoundInvariant st) : BoundInvariant st' := by
95  induction ht with
96  | nil => exact hp
97  | step _ hm _ ih => exact ih (bound_step hm.1 hp)
98  | dict hm _ ih => exact ih (bound_dict hm hp)
99  | header hm _ ih => exact ih (bound_header hm hp)
100
101/-- The abstract trace model bounds a clean completed stream. This does not establish the
102corresponding refinement for translated C. -/
103theorem deflate_bound_adequate : Goal.deflate_bound_adequate := by
104  intro p x st _ ht hd hc
105  exact (trace_bound ht (by simp [BoundInvariant, DeflState.fresh]) hd).2 hc
106
107private theorem step_input_prefix {x : List UInt8} {st st' : DeflState} {c : DeflCall} {o : DeflOut}
108    (hs : DeflStep st c o st') (hin : st.input <+: x) (hc : c.inp <+: x.drop st.input.length) :
109    st'.input <+: x := by
110  have hframe : st'.input = st.input ++ c.inp.take o.consumed := by
111    by_cases ht : c.flush = .trees
112    · rcases hs.1 ht with ⟨_, hz, _, rfl⟩
113      simp [hz]
114    by_cases hb : c.badBuf = true ∨ (st.finishing = true ∧ c.flush ≠ .finish)
115    · rcases hs.2.1 ht hb with ⟨_, hz, _, rfl⟩
116      simp [hz]
117    have hbuf : c.badBuf = false := by cases h : c.badBuf <;> simp_all
118    have hnfin : ¬ (st.finishing = true ∧ c.flush ≠ .finish) := fun h => hb (Or.inr h)
119    by_cases hz : c.availOut = 0
120    · rcases hs.2.2.1 ht hbuf hnfin hz with ⟨_, hn, _, rfl⟩
121      simp [hn]
122    exact (hs.2.2.2 ht hbuf hnfin hz).1.2.2.1
123  rw [hframe]
124  have htake : c.inp.take o.consumed <+: x.drop st.input.length :=
125    (List.take_prefix _ _).trans hc
126  obtain ⟨tail, htail⟩ := hin
127  rw [← htail, List.drop_left] at htake
128  obtain ⟨tail', htail'⟩ := htake
129  refine ⟨tail', ?_⟩
130  simp only [htail, htail', List.append_assoc]
131
132private theorem dict_input {s s' : DeflState} {d : List UInt8} {r : Int}
133    (hm : DeflSetDict s d r s') : s'.input = s.input := by
134  cases hw : s.params.wrap with
135  | gzip => simp only [DeflSetDict, hw] at hm; rcases hm with ⟨_, rfl⟩; rfl
136  | zlib =>
137    simp only [DeflSetDict, hw] at hm
138    split at hm <;> rcases hm with ⟨_, rfl⟩ <;> rfl
139  | raw =>
140    simp only [DeflSetDict, hw] at hm
141    split at hm
142    · rcases hm with ⟨_, rfl⟩; rfl
143    · rcases hm with ⟨_, rfl⟩ | ⟨_, rfl⟩ <;> rfl
144
145private theorem header_input {s s' : DeflState} {h : GzHead} {r : Int}
146    (hm : DeflSetHeader s h r s') : s'.input = s.input := by
147  unfold DeflSetHeader at hm
148  split at hm
149  · rcases hm with ⟨_, rfl⟩; rfl
150  · rcases hm with ⟨_, hb, hg⟩
151    by_cases he : s.started = true ∨ ¬ h.Valid
152    · rw [hb he]
153    · rw [hg he]
154
155private theorem trace_input_prefix {x : List UInt8} {st st' : DeflState} (ht : DeflTrace x st st')
156    (hin : st.input <+: x) : st'.input <+: x := by
157  induction ht with
158  | nil => exact hin
159  | step hp hm _ ih => exact ih (step_input_prefix hm.1 hin hp)
160  | dict hm _ ih => exact ih (by rw [dict_input hm]; exact hin)
161  | header hm _ ih => exact ih (by rw [header_input hm]; exact hin)
162
163/-- A finish call in the abstract model completes when the stated bound fits. -/
164theorem deflate_completes : Goal.deflate_completes := by
165  intro p x s c r s' _ ht hc hp hfin hd hbuf hflush hin hroom hbound hm
166  have hprefix : s.input <+: x := trace_input_prefix ht (by simp [DeflState.fresh])
167  have hcat : s.input ++ c.inp = x := by
168    rw [hin]
169    obtain ⟨tail, htail⟩ := hprefix
170    rw [← htail, List.drop_left]
171  have hrun : DeflRun s c r.out s' := by
172    apply hm.1.2.2.2
173    · rw [hflush]; decide
174    · exact hbuf
175    · rw [hfin]; simp
176    · omega
177  rcases hrun with ⟨hframe, _, _, _, _, _, _, _, _, hend, _, _, _, _, _, _, _, _, _, _, _, _, _, hlive⟩
178  have hr : r.out.rc = Z.streamEnd := by
179    apply hlive hflush hc hp hfin hd
180    have hlen : s.input.length + c.inp.length = x.length := by
181      have he := congrArg List.length hcat
182      simpa only [List.length_append] using he
183    simpa [hlen] using hbound
184  have hend' := hend hr
185  refine ⟨?_, hend'.2.2.1, ?_⟩
186  · exact hm.2.trans hr
187  · rw [hframe.2.2.1, hend'.2.1, List.take_length, hcat]
188
189#print axioms deflate_bound_adequate
190#print axioms deflate_completes
191end ZlibF.Spec.Api.Proofs