public-infback-init.lean

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

1import ZlibF.Spec.Public.Domains
2import ZlibF.Proof.«infback.c.end»
3
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec Zlib.Infback.Proofs ZlibF.Spec.Public
5
6namespace ZlibF.Spec.Public.InflateBackInitProof
7
8theorem version_value_read {h : Heap} {v : BPtr} {byte : UInt8} (hv : VersionValue h v (some byte)) :
9    v ≠ .null ∧ OkOn h (index8 v 0) byte := by
10  rcases hv with ⟨_,h⟩ | ⟨b, hb, hbytes⟩
11  · cases h
12  · cases hb
13    rcases hbytes with ⟨_,hn,_⟩ | ⟨ref,off,a,rfl,hget,hfit,hlist⟩
14    · cases hn
15    · refine ⟨by simp, ?_⟩
16      have ha : off < a.size := by omega
17      have he : a[off]? = some byte := by
18        have hh := congrArg (fun l : List UInt8 => l[0]?) hlist
19        simpa [List.getElem?_take, List.getElem?_drop] using hh.symm
20      have hbyte : a[off] = byte := by
21        have := Array.getElem?_eq_getElem ha
22        rw [this] at he
23        exact Option.some.inj he
24      have hr := Ptr.index_ok (h := h) (r := ref) (a := a) (off := off) (i := 0) hget (by omega)
25      simpa [hbyte] using hr
26
27theorem init_refusals :
28    (∀ h p wb window version head size, VersionValue h version head →
29      (head ≠ some 49 ∨ size ≠ 112) →
30      C.run (inflateBackInit_ p wb window version size) h = .ok (Z_VERSION_ERROR, h)) ∧
31    (∀ h p wb window version, VersionValue h version (some 49) →
32      (p = none ∨ window = .null ∨ wb.toInt < 8 ∨ 15 < wb.toInt) →
33      C.run (inflateBackInit_ p wb window version 112) h = .ok (Z_STREAM_ERROR, h)) := by
34  constructor
35  · intro h p wb window version head size hv hbad
36    cases head with
37    | none =>
38      rcases hv with ⟨rfl,_⟩ | ⟨b,hb,_⟩
39      · exact inflateBackInit__version_null p wb window size h
40      · cases hb
41    | some b =>
42      obtain ⟨hn,hr⟩ := version_value_read hv
43      by_cases hb : b = 49
44      · subst b
45        have hs : size ≠ 112 := by simpa using hbad
46        exact inflateBackInit__version_size p wb window version size h hn hr hs
47      · exact inflateBackInit__version_char p wb window version size h b hn hr hb
48  · intro h p wb window version hv hbad
49    obtain ⟨hn,hr⟩ := version_value_read hv
50    have hbad' : p = none ∨ window = .null ∨ wb < 8 ∨ wb > 15 := by
51      rcases hbad with h | h | h | h
52      · exact Or.inl h
53      · exact Or.inr (Or.inl h)
54      · exact Or.inr (Or.inr (Or.inl (Int32.lt_iff_toInt_lt.mpr (by simpa using h))))
55      · exact Or.inr (Or.inr (Or.inr (Int32.lt_iff_toInt_lt.mpr (by simpa using h))))
56    exact inflateBackInit__stream_error p wb window version h hn hr hbad'
57
58theorem back_init_success_valid {h : Heap} {r : ZStreamRef} {z : ZStream} {wb : Int32} {window : BPtr}
59    (hF : Fresh h) (hU : Uniq h) (hglob : LibraryGlobals h) (hz : r.get h = some z)
60    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
61    (h8 : ¬ wb < 8) (h15 : ¬ wb > 15) (hwin : window ≠ .null)
62    (hw : Writable h window (2 ^ wb.toInt.toNat)) :
63    BackValid (backOkHeap h r z window wb) r h.nextBlk
64      (initStream2 z h.nextBlk) (backState (h.garbage h.nalloc) window wb) := by
65  have hr := i2u_range h8 h15
66  have hwb : (i2u wb).toNat = wb.toInt.toNat := by
67    unfold i2u
68    rw [Int32.toNat_toUInt32_of_le]
69    · rfl
70    · rw [Int32.le_iff_toInt_le]
71      have hnot : ¬ wb.toInt < 8 := fun he => h8 (Int32.lt_iff_toInt_lt.mpr (by simpa using he))
72      simp only [Int32.toInt_zero]
73      omega
74  have ⟨hu,hf⟩ := backOk_shape hz hF window wb hU
75  refine ⟨?_,?_,?_,?_,?_,wf_backState _ _ _,?_,?_,?_,?_,?_,hf,hu,?_⟩
76  · simp [backOkHeap, hz]
77  · simp [backOkHeap]
78  · simp [initStream2]
79  · rcases hza with e | e <;> simp [initStream2, initStream, e]
80  · rcases hzf with e | e <;> simp [initStream2, initStream, e]
81  · simpa [backState, i2u] using hr.1
82  · simpa [backState, i2u] using hr.2
83  · simp only [backState]
84    exact shl32_one hr.2
85  · simpa [backState] using hwin
86  · rcases hw with ⟨hn,_⟩ | ⟨ref,off,a,hptr,hget,hro,hfit⟩
87    · exact (hwin hn).elim
88    · right
89      refine ⟨ref,off,a,hptr,?_,?_,?_⟩
90      · cases ref <;> simp_all [Space.get, backOkHeap, allocIstHeap]
91      · cases ref <;> simp_all [Space.ro, backOkHeap, allocIstHeap]
92      · simpa [backState, shl32_one hr.2, hwb] using hfit
93  · simpa [LibraryGlobals, backOkHeap, allocIstHeap] using hglob
94
95#print axioms back_init_success_valid
96
97theorem back_init_frame {h : Heap} {r : ZStreamRef} {z : ZStream} {window : BPtr} {wb : Int32}
98    (hz : r.get h = some z) (hF : Fresh h) :
99    Frame h (backOkHeap h r z window wb) (StreamRoot r) := by
100  cases r with
101  | tab k =>
102    have hk : h.streams k = some z := hz
103    simp only [Frame, backOkHeap, allocIstHeap, ZStreamRef.put, hk, upd_same, true_and]
104    refine ⟨by omega, by omega, ?_⟩
105    intro b hb hn
106    have hne : b ≠ h.nextBlk := fun he => hF b (by omega) hb
107    have hk : b ≠ k := fun he => hn (by simpa [StreamRoot] using he)
108    simp [upd_ne, hne, hk]
109  | in_gzstate_strm k =>
110    cases hg : h.gzstates k with
111    | none => simp [ZStreamRef.get, hg] at hz
112    | some g =>
113      simp only [Frame, backOkHeap, allocIstHeap, ZStreamRef.put, hg, upd_same, true_and]
114      refine ⟨by omega, by omega, ?_⟩
115      intro b hb hn
116      have hne : b ≠ h.nextBlk := fun he => hF b (by omega) hb
117      have hk : b ≠ k := fun he => hn (by simpa [StreamRoot] using he)
118      simp [upd_ne, hne, hk]
119
120theorem back_init_live {h : Heap} {r : ZStreamRef} {z : ZStream} {window : BPtr} {wb : Int32}
121    (hz : r.get h = some z) (hF : Fresh h) :
122    LiveChange h (backOkHeap h r z window wb) (fun b => b = h.nextBlk) (fun _ => False) := by
123  have hFp : Fresh (r.put h (initStream z)) := (shape_put hz _).fresh (by simp) hF
124  have hz0 : r.get (allocIstHeap (r.put h (initStream z)) (backState (h.garbage h.nalloc) window wb)) =
125      some (initStream z) := by simp [hz]
126  have ho : h.Owns (fun b => h.live b) := fun _ => Iff.rfl
127  have h1 := owns_allocIst hFp (backState (h.garbage h.nalloc) window wb) ((shape_put hz _).owns ho)
128  simp only [ZStreamRef.put_nextBlk] at h1
129  have h2 := (shape_put hz0 (initStream2 z h.nextBlk)).owns h1
130  intro b
131  simpa [LiveChange, backOkHeap] using h2 b
132
133/-- `int inflateBackInit_(z_streamp strm, int windowBits, unsigned char *window,
134The exact public result, state, frame and ownership contract. -/
135theorem back_init_public : Goal.inflateBackInit_ := by
136  obtain ⟨hversion, hstream⟩ := init_refusals
137  refine ⟨hversion, hstream, ?_⟩
138  intro h r z wb window version hF hU hglob hz halloc hv hlo hhi hwin hwrite
139  obtain ⟨hvn, hv0⟩ := version_value_read hv
140  have h8 : ¬ wb < 8 := by
141    intro hh
142    have hh' := Int32.lt_iff_toInt_lt.mp hh
143    simp at hh'
144    omega
145  have h15 : ¬ wb > 15 := by
146    intro hh
147    have hh' := Int32.lt_iff_toInt_lt.mp hh
148    simp at hh'
149    omega
150  obtain ⟨hza, hzf⟩ := halloc
151  by_cases hok : h.allocOk h.nalloc = true
152  · refine ⟨Z_OK, backOkHeap h r z window wb, ?_, ?_, ?_⟩
153    · exact inflateBackInit__success hz hF hok hza hzf hvn hv0 hwin h8 h15
154    · simp [backOkHeap, allocIstHeap]
155    · have hnot : h.allocOk h.nalloc ≠ false := by rw [hok]; decide
156      simp only [hnot]
157      refine ⟨trivial, ?_, back_init_frame hz hF, back_init_live hz hF⟩
158      simpa [preparedStream, initStream2, initStream, backInitialState, backState, i2u] using
159        (back_init_success_valid hF hU hglob hz hza hzf h8 h15 hwin hwrite)
160  · have hfail : h.allocOk h.nalloc = false := by
161      cases he : h.allocOk h.nalloc <;> simp_all
162    refine ⟨Z_MEM_ERROR, initMemHeap h r z, ?_, ?_, ?_⟩
163    · exact inflateBackInit__memfail hz hF hok hza hzf hvn hv0 hwin h8 h15
164    · simp [initMemHeap]
165    · simp only [hfail, ite_true]
166      refine ⟨trivial, ?_⟩
167      simp [SameObjects, initMemHeap, preparedStream, initStream]
168
169#print axioms back_init_public
170
171
172theorem public_witness_fresh : Fresh witnessHeap := by
173  intro b hb hl
174  have h1 : b ≠ 1 := by simp [witnessHeap] at hb; omega
175  have h2 : b ≠ 2 := by simp [witnessHeap] at hb; omega
176  have h0 : b ≠ 0 := by simp [witnessHeap] at hb; omega
177  simp [Heap.live, witnessHeap, Heap.empty, upd_ne _ _ _ _ h1, upd_ne _ _ _ _ h2, upd_ne _ _ _ _ h0] at hl
178
179theorem public_witness_uniq : Uniq witnessHeap := by
180  intro b
181  by_cases h1 : b = 1
182  · subst h1; simp [witnessHeap, Heap.empty, cnt]
183  by_cases h2 : b = 2
184  · subst h2; simp [witnessHeap, Heap.empty, cnt]
185  by_cases h0 : b = 0
186  · subst h0; simp [witnessHeap, Heap.empty, cnt]
187  simp [witnessHeap, Heap.empty, cnt, upd_ne _ _ _ _ h1, upd_ne _ _ _ _ h2, upd_ne _ _ _ _ h0]
188
189theorem public_witness_domain : InitDomain witnessHeap (.tab 0) (.ref (.blk 1) 0) := by
190  refine ⟨public_witness_fresh, public_witness_uniq, ?_, ?_, default, ?_, ?_, ?_⟩
191  · rfl
192  · right
193    refine ⟨49, rfl, ?_⟩
194    right
195    refine ⟨.blk 1, 0, #[49, 0], rfl, ?_, ?_, ?_⟩ <;> simp [witnessHeap, Space.get, Heap.empty]
196  · simp [ZStreamRef.get, witnessHeap]
197  · exact ⟨Or.inl rfl, Or.inl rfl⟩
198  · rfl
199
200theorem back_domain_general :
201  ∀ h r version wb window,
202    InitDomain h r version → 8 ≤ wb.toInt → wb.toInt ≤ 15 →
203    window ≠ .null → Writable h window (2 ^ wb.toInt.toNat) → h.allocOk h.nalloc = true →
204    ∃ after z s, C.run (inflateBackInit_ (some r) wb window version 112) h =
205      .ok (Z_OK, after) ∧ BackValid after r h.nextBlk z s ∧ s.window = window ∧
206      s.wbits = wb.toUInt32 ∧ Frame h after (StreamRoot r) ∧
207      LiveChange h after (fun b => b = h.nextBlk) (fun _ => False) := by
208  intro h r version wb window hd hlo hhi hn hw ha
209  obtain ⟨hf, hu, hg, hv, z, hz, hd, _⟩ := hd
210  obtain ⟨rc, after, hrun, _, hs⟩ := back_init_public.2.2 h r z wb window version hf hu hg hz hd hv hlo hhi hn hw
211  simp only [ha, Bool.true_eq_false, ite_false] at hs
212  obtain ⟨rfl, valid, frame, live⟩ := hs
213  exact ⟨after, _, _, hrun, valid, rfl, rfl, frame, live⟩
214
215#print axioms public_witness_domain
216#print axioms back_domain_general
217
218theorem public_witness_window {wb : Int32} (hhi : wb.toInt ≤ 15) :
219    Writable witnessHeap (.ref (.blk 2) 0) (2 ^ wb.toInt.toNat) := by
220  right
221  refine ⟨.blk 2, 0, Array.replicate 32768 0, rfl, ?_, ?_, ?_⟩
222  · simp [witnessHeap, Space.get, Heap.empty]
223  · simp [witnessHeap, Space.ro, Heap.empty]
224  · simp only [Nat.zero_add, Array.size_replicate]
225    have he : wb.toInt.toNat ≤ 15 := Int.toNat_le.mpr (by omega)
226    exact Nat.le_trans (Nat.pow_le_pow_right (by decide) he) (by decide)
227
228/-- `int inflateBackInit_(z_streamp strm, int windowBits, unsigned char *window,
229Initialization establishes the public representation domain. -/
230theorem back_init_domain_public : Goal.inflate_back_initialisation_domain := by
231  refine ⟨back_domain_general, public_witness_domain, ?_⟩
232  intro wb hlo hhi
233  obtain ⟨after, z, s, hr, hv, hw, _, _, _⟩ :=
234    back_domain_general witnessHeap (.tab 0) (.ref (.blk 1) 0) wb (.ref (.blk 2) 0)
235      public_witness_domain hlo hhi (by simp) (public_witness_window hhi) (by rfl)
236  exact ⟨after, z, s, hr, hv, hw⟩
237
238#print axioms back_init_domain_public
239
240
241theorem back_immediate_end {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : InflateState}
242    (hv : BackValid h r i z s) :
243    C.run (inflateBackEnd (some r)) h = .ok (Z_OK, backEndHeap h r z i) := by
244  obtain ⟨hz, hs, hstate, _, hfree, _⟩ := hv
245  show inflateBackEnd (some r) h = _
246  unfold inflateBackEnd
247  have hz0 : z.zfree ≠ .null := by rw [hfree]; intro c; cases c
248  have hs0 : z.state ≠ none := by rw [hstate]; intro c; cases c
249  isimp [hz, hs0, hz0, hstate, hfree, zfrees_run hz hfree hs, backEndHeap]
250
251theorem back_end_window {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : InflateState}
252    (hv : BackValid h r i z s) :
253    Writable (backEndHeap h r z i) s.window s.wsize.toNat := by
254  have hw := hv.2.2.2.2.2.2.2.2.2.2.1
255  rcases hw with ⟨hn, hl⟩ | ⟨ref, off, a, hp, hg, hr, hn⟩
256  · exact Or.inl ⟨hn,hl⟩
257  · right
258    refine ⟨ref, off, a, hp, ?_, ?_, hn⟩
259    · cases ref <;> simpa [backEndHeap, freeIst, Space.get] using hg
260    · cases ref <;> simp_all [backEndHeap, freeIst, Space.ro]
261
262#print axioms back_end_window
263
264theorem back_init_then_end {h : Heap} {r : ZStreamRef} {version : BPtr}
265    {wb : Int32} {window : BPtr}
266    (hd : InitDomain h r version) (hlo : 8 ≤ wb.toInt) (hhi : wb.toInt ≤ 15)
267    (hn : window ≠ .null) (hw : Writable h window (2 ^ wb.toInt.toNat))
268    (ha : h.allocOk h.nalloc = true) :
269    ∃ middle final z,
270      C.run (inflateBackInit_ (some r) wb window version 112) h = .ok (Z_OK, middle) ∧
271      C.run (inflateBackEnd (some r)) middle = .ok (Z_OK, final) ∧
272      r.get final = some z ∧ z.state = none ∧
273      Writable final window (2 ^ wb.toInt.toNat) ∧
274      (∀ b, final.live b ↔ h.live b) := by
275  obtain ⟨middle, z, s, hi, hv, hwin, hbits, _, hlive⟩ :=
276    back_domain_general h r version wb window hd hlo hhi hn hw ha
277  let final := backEndHeap middle r z h.nextBlk
278  have hrun := back_immediate_end hv
279  have hget : r.get final = some { z with state := none } := by
280    have hz := hv.1
281    simp [final, backEndHeap, hz]
282  have hwrite := back_end_window hv
283  have hnat : s.wsize.toNat = 2 ^ wb.toInt.toNat := by
284    have hsize := hv.2.2.2.2.2.2.2.2.1
285    rw [hbits] at hsize
286    have hwb : wb.toUInt32.toNat = wb.toInt.toNat := by
287      rw [Int32.toNat_toUInt32_of_le]
288      · rfl
289      · rw [Int32.le_iff_toInt_le]
290        simp only [Int32.toInt_zero]
291        omega
292    simpa [hwb] using hsize
293  refine ⟨middle, final, { z with state := none }, hi, hrun, hget, rfl, ?_, ?_⟩
294  · simpa [final, hwin, hnat] using hwrite
295  · have huniq := hv.2.2.2.2.2.2.2.2.2.2.2.2.1
296    have hs := hv.2.1
297    have hz := hv.1
298    have ho : middle.Owns (fun b => middle.live b) := fun _ => Iff.rfl
299    have hf := owns_freeIst huniq hs ho
300    have hz' : r.get (freeIst middle h.nextBlk) = some z := by simpa using hz
301    have hend := (shape_put hz' {z with state := none}).owns hf
302    intro b
303    have hbefore : ¬ h.live h.nextBlk := (hd.1) _ (Nat.le_refl _)
304    have hmid := hlive b
305    have he := hend b
306    simp only [not_false_eq_true, and_true] at hmid
307    constructor
308    · intro hh
309      have hparts := he.mp hh
310      rcases hmid.mp hparts.1 with old | new
311      · exact old
312      · exact (hparts.2 new).elim
313    · intro hh
314      apply he.mpr
315      refine ⟨hmid.mpr (Or.inl hh), ?_⟩
316      intro eq
317      subst b
318      exact hbefore hh
319
320#print axioms back_init_then_end
321
322end ZlibF.Spec.Public.InflateBackInitProof