public-inflate-init.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.Public.Domains
2import ZlibF.Proof.«inflate.c.hdr»
3
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec.Public ZlibF.Spec
5
6namespace ZlibF.Spec.Public.Proofs.InflateInit
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
27
28theorem init_ok_frame {h : Heap} {r : ZStreamRef} {z : ZStream} {wrap wb : Int32}
29    (hz : r.get h = some z) (hF : Fresh h) :
30    Frame h (initOkHeap h r z wrap wb) (StreamRoot r) := by
31  unfold initOkHeap
32  dsimp only
33  rw [reset2Heap_null _ _ (initState r) (by rfl)]
34  cases r with
35  | tab k =>
36    have hk : h.streams k = some z := hz
37    simp only [Frame, allocIstHeap, setI, ZStreamRef.put, hk,
38      upd_same, true_and]
39    refine ⟨by omega, by omega, ?_⟩
40    intro b hb hn
41    have hne : b ≠ h.nextBlk := fun he => hF b (by omega) hb
42    have hk : b ≠ k := fun he => hn (by simpa [StreamRoot] using he)
43    simp [upd_ne, hne, hk]
44  | in_gzstate_strm k =>
45    cases hg : h.gzstates k with
46    | none => simp [ZStreamRef.get, hg] at hz
47    | some g =>
48      simp only [Frame, allocIstHeap, setI, ZStreamRef.put, hg,
49        upd_same, true_and]
50      refine ⟨by omega, by omega, ?_⟩
51      intro b hb hn
52      have hne : b ≠ h.nextBlk := fun he => hF b (by omega) hb
53      have hk : b ≠ k := fun he => hn (by simpa [StreamRoot] using he)
54      simp [upd_ne, hne, hk]
55
56#print axioms init_ok_frame
57
58theorem init15_initial {h : Heap} {r : ZStreamRef} {z : ZStream} {v : BPtr}
59    (hF : Fresh h) (hU : Uniq h) (hz : r.get h = some z)
60    (ha : h.allocOk h.nalloc = true)
61    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc")
62    (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
63    (hv : v ≠ .null) (hv0 : OkOn h (index8 v 0) 49) :
64    InflateInitial h (initOkHeap h r z 5 15) r .zlib 15 := by
65  obtain ⟨after, _, he, hg, ho⟩ :=
66    inflateInit2_ok hU hF hz ha hza hzf hv hv0 (w := 15) params15
67  subst after
68  let z' := resetKeepStream (initStream2 z h.nextBlk) (resetPre (reset2Pre 5 15 (initState r)))
69  let s' := resetKeepState h.nextBlk (resetPre (reset2Pre 5 15 (initState r)))
70  refine ⟨z', s', hg, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, init_ok_frame hz hF, ?_⟩
71  all_goals try { rfl }
72  all_goals try { rcases hza with e | e <;> rcases hzf with f | f <;>
73    simp [z', resetKeepStream, resetPre, reset2Pre, initState, initStream2, initStream,
74      InflateState.zeroed, InflateState.garbage, i2u, i2ul, e, f, HEAD] }
75  intro b
76  have hh := ho (fun b => h.live b) (fun _ => Iff.rfl) b
77  simpa [LiveChange] using hh
78
79#print axioms init15_initial
80
81/-- `int inflateInit_(z_streamp strm, const char *version, int stream_size)`
82The exact public result, state, frame and ownership contract. -/
83theorem init15_public : Goal.inflateInit_ := by
84  refine ⟨?_, ?_, ?_⟩
85  · intro h p version head size hv hbad
86    cases head with
87    | none =>
88      rcases hv with ⟨rfl, _⟩ | ⟨b, hb, _⟩
89      · exact inflateInit2_version_null p 15 size h
90      · cases hb
91    | some b =>
92      obtain ⟨hn, hr⟩ := version_value_read hv
93      by_cases hb : b = 49
94      · subst b
95        have hs : size ≠ 112 := by simpa using hbad
96        exact inflateInit2_version_size p 15 version size h hn hr hs
97      · exact inflateInit2_version_char p 15 version size h b hn hr hb
98  · intro h version hv
99    obtain ⟨hn, hr⟩ := version_value_read hv
100    exact inflateInit2_nullstream 15 version h hn hr
101  · intro h r z version hf hu _ hz ha hv
102    obtain ⟨hn, hr⟩ := version_value_read hv
103    obtain ⟨hza, hzf⟩ := ha
104    by_cases hok : h.allocOk h.nalloc = true
105    · refine ⟨Z_OK, initOkHeap h r z 5 15, ?_, ?_, ?_⟩
106      · exact inflateInit2_success hz hf hok hza hzf hn hr params15
107      · simp [initOkHeap, reset2Heap_null _ _ (initState r) (by rfl), allocIstHeap, setI]
108      · have hnot : h.allocOk h.nalloc ≠ false := by rw [hok]; decide
109        simp only [hnot]
110        change True ∧ InflateInitial h (initOkHeap h r z 5 15) r .zlib 15
111        exact ⟨trivial, init15_initial hf hu hz hok hza hzf hn hr⟩
112    · have hfail : h.allocOk h.nalloc = false := by cases he : h.allocOk h.nalloc <;> simp_all
113      refine ⟨Z_MEM_ERROR, initMemHeap h r z, ?_, ?_, ?_⟩
114      · exact inflateInit2_memfail hz hf hok hza hzf hn hr
115      · simp [initMemHeap]
116      · simp only [hfail, ite_true]
117        refine ⟨trivial, ?_⟩
118        simp [SameObjects, initMemHeap, preparedStream, initStream]
119
120#print axioms init15_public
121
122theorem params_equiv (w : Int32) :
123    reset2Params w = (Api.inflWbits w.toInt).map (fun (wr, n) =>
124      ((match wr with | .raw => 0 | .zlib => 5 | .gzip => 6 | .auto => 7 : Int32), Int32.ofInt n)) := by
125  by_cases hlo : w.toInt < -15
126  · have hn : w < 0 := Int32.lt_iff_toInt_lt.mpr (by simpa using (show w.toInt < 0 by omega))
127    have h15 : w < -15 := Int32.lt_iff_toInt_lt.mpr (by simpa using hlo)
128    simp [reset2Params, hn, h15, Api.inflWbits, hlo, show w.toInt < 0 by omega]
129  · by_cases hhi : 48 ≤ w.toInt
130    · have hn : ¬ w < 0 := fun x => by have := Int32.lt_iff_toInt_lt.mp x; simp at this; omega
131      have h48 : ¬ w < 48 := fun x => by have := Int32.lt_iff_toInt_lt.mp x; simp at this; omega
132      have h16 : 15 < w := Int32.lt_iff_toInt_lt.mpr (by simpa using (show 15 < w.toInt by omega))
133      have hb : badBits w = true := by simp [badBits, h16, show w ≠ 0 by intro h; subst w; simp at hhi]
134      have hdiv0 : w.toInt / 16 ≠ 0 := by omega
135      have hdiv1 : w.toInt / 16 ≠ 1 := by omega
136      have hdiv2 : w.toInt / 16 ≠ 2 := by omega
137      simp [reset2Params, hn, h48, hb, Api.inflWbits, show ¬ w.toInt < 0 by omega, hdiv0, hdiv1, hdiv2]
138    · have hc : w.toInt = -15 ∨ w.toInt = -14 ∨ w.toInt = -13 ∨ w.toInt = -12 ∨
139        w.toInt = -11 ∨ w.toInt = -10 ∨ w.toInt = -9 ∨ w.toInt = -8 ∨
140        w.toInt = -7 ∨ w.toInt = -6 ∨ w.toInt = -5 ∨ w.toInt = -4 ∨
141        w.toInt = -3 ∨ w.toInt = -2 ∨ w.toInt = -1 ∨ w.toInt = 0 ∨
142        w.toInt = 1 ∨ w.toInt = 2 ∨ w.toInt = 3 ∨ w.toInt = 4 ∨
143        w.toInt = 5 ∨ w.toInt = 6 ∨ w.toInt = 7 ∨ w.toInt = 8 ∨
144        w.toInt = 9 ∨ w.toInt = 10 ∨ w.toInt = 11 ∨ w.toInt = 12 ∨
145        w.toInt = 13 ∨ w.toInt = 14 ∨ w.toInt = 15 ∨ w.toInt = 16 ∨
146        w.toInt = 17 ∨ w.toInt = 18 ∨ w.toInt = 19 ∨ w.toInt = 20 ∨
147        w.toInt = 21 ∨ w.toInt = 22 ∨ w.toInt = 23 ∨ w.toInt = 24 ∨
148        w.toInt = 25 ∨ w.toInt = 26 ∨ w.toInt = 27 ∨ w.toInt = 28 ∨
149        w.toInt = 29 ∨ w.toInt = 30 ∨ w.toInt = 31 ∨ w.toInt = 32 ∨
150        w.toInt = 33 ∨ w.toInt = 34 ∨ w.toInt = 35 ∨ w.toInt = 36 ∨
151        w.toInt = 37 ∨ w.toInt = 38 ∨ w.toInt = 39 ∨ w.toInt = 40 ∨
152        w.toInt = 41 ∨ w.toInt = 42 ∨ w.toInt = 43 ∨ w.toInt = 44 ∨
153        w.toInt = 45 ∨ w.toInt = 46 ∨ w.toInt = 47 := by omega
154      have hw : w = Int32.ofInt w.toInt := (Int32.ofInt_toInt w).symm
155      rcases hc with hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
156        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
157        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
158        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
159        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
160        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
161        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
162        hcase | hcase | hcase | hcase | hcase | hcase | hcase
163      all_goals rw [hcase] at hw; subst w; decide
164
165#print axioms params_equiv
166
167theorem api_bits_bound (w : Int) (wr : Api.Wrap) (n : Nat)
168    (h : Api.inflWbits w = some (wr, n)) : n ≤ 15 := by
169  unfold Api.inflWbits at h
170  repeat' split at h
171  all_goals simp_all <;> omega
172
173
174theorem public_witness_fresh : Fresh witnessHeap := by
175  intro b hb hl
176  have h1 : b ≠ 1 := by simp [witnessHeap] at hb; omega
177  have h2 : b ≠ 2 := by simp [witnessHeap] at hb; omega
178  have h0 : b ≠ 0 := by simp [witnessHeap] at hb; omega
179  simp [Heap.live, witnessHeap, Heap.empty, upd_ne _ _ _ _ h1, upd_ne _ _ _ _ h2, upd_ne _ _ _ _ h0] at hl
180
181theorem public_witness_uniq : Uniq witnessHeap := by
182  intro b
183  by_cases h1 : b = 1
184  · subst h1; simp [witnessHeap, Heap.empty, cnt]
185  by_cases h2 : b = 2
186  · subst h2; simp [witnessHeap, Heap.empty, cnt]
187  by_cases h0 : b = 0
188  · subst h0; simp [witnessHeap, Heap.empty, cnt]
189  simp [witnessHeap, Heap.empty, cnt, upd_ne _ _ _ _ h1, upd_ne _ _ _ _ h2, upd_ne _ _ _ _ h0]
190
191theorem public_witness_domain : InitDomain witnessHeap (.tab 0) (.ref (.blk 1) 0) := by
192  refine ⟨public_witness_fresh, public_witness_uniq, ?_, ?_, default, ?_, ?_, ?_⟩
193  · rfl
194  · right
195    refine ⟨49, rfl, ?_⟩
196    right
197    refine ⟨.blk 1, 0, #[49, 0], rfl, ?_, ?_, ?_⟩ <;> simp [witnessHeap, Space.get, Heap.empty]
198  · simp [ZStreamRef.get, witnessHeap]
199  · exact ⟨Or.inl rfl, Or.inl rfl⟩
200  · rfl
201
202
203def publicWrap : Api.Wrap → Int32
204  | .raw => 0 | .zlib => 5 | .gzip => 6 | .auto => 7
205
206theorem init_any_initial {h : Heap} {r : ZStreamRef} {z : ZStream} {v : BPtr} {w : Int32} {wr : Api.Wrap} {bits : Nat}
207    (hF : Fresh h) (hU : Uniq h) (hz : r.get h = some z)
208    (ha : h.allocOk h.nalloc = true)
209    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc")
210    (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
211    (hv : v ≠ .null) (hv0 : OkOn h (index8 v 0) 49)
212    (hp : Api.inflWbits w.toInt = some (wr, bits)) :
213    InflateInitial h (initOkHeap h r z (publicWrap wr) (Int32.ofInt bits)) r wr bits := by
214  have heq := params_equiv w
215  rw [hp] at heq
216  simp only [Option.map_some] at heq
217  change reset2Params w = some (publicWrap wr, Int32.ofInt bits) at heq
218  have hb := api_bits_bound w.toInt wr bits hp
219  obtain ⟨after, _, he, hg, ho⟩ :=
220    inflateInit2_ok hU hF hz ha hza hzf hv hv0 heq
221  subst after
222  let z' := resetKeepStream (initStream2 z h.nextBlk) (resetPre (reset2Pre (publicWrap wr) (Int32.ofInt bits) (initState r)))
223  let s' := resetKeepState h.nextBlk (resetPre (reset2Pre (publicWrap wr) (Int32.ofInt bits) (initState r)))
224  have hwindow : s'.window = .null := by
225    simp [s', resetKeepState, resetPre, reset2Pre, initState]
226  have hnat : (UInt32.ofNat bits).toNat = bits := by rw [UInt32.toNat_ofNat']; exact Nat.mod_eq_of_lt (by omega)
227  refine ⟨z', s', hg, ?_, ?_, ?_, hwindow, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, init_ok_frame hz hF, ?_⟩
228  all_goals try { rfl }
229  all_goals try { rcases hza with e | e <;> rcases hzf with f | f <;>
230    simp [z', resetKeepStream, resetPre, reset2Pre, initState, initStream2, initStream, e, f] }
231  all_goals try {
232    simp [s', resetKeepState, resetPre, reset2Pre, i2u]
233    change (UInt32.ofNat bits).toNat = bits
234    exact hnat }
235  all_goals try { simp [s', resetKeepState, resetPre, reset2Pre] }
236  intro b
237  have hh := ho (fun b => h.live b) (fun _ => Iff.rfl) b
238  simpa [LiveChange] using hh
239
240
241#print axioms init_any_initial
242
243theorem inflate_domain_general :
244  ∀ h r version wb wrap bits,
245    InitDomain h r version → Api.inflWbits wb.toInt = some (wrap, bits) →
246    h.allocOk h.nalloc = true →
247    ∃ after, C.run (inflateInit2_ (some r) wb version 112) h = .ok (Z_OK, after) ∧
248      InflateInitial h after r wrap bits ∧ StreamReachable .inflate after r := by
249  intro h r version wb wrap bits hd hp ha
250  obtain ⟨hf, hu, hg, hv, z, hz, halloc, _⟩ := hd
251  obtain ⟨hn, hv0⟩ := version_value_read hv
252  have heq := params_equiv wb
253  rw [hp] at heq
254  change reset2Params wb = some (publicWrap wrap, Int32.ofInt bits) at heq
255  let after := initOkHeap h r z (publicWrap wrap) (Int32.ofInt bits)
256  have hr : C.run (inflateInit2_ (some r) wb version 112) h = .ok (Z_OK, after) :=
257    inflateInit2_success hz hf ha halloc.1 halloc.2 hn hv0 heq
258  exact ⟨after, hr, init_any_initial hf hu hz ha halloc.1 halloc.2 hn hv0 hp,
259    StreamReachable.inflateInit hf hu hg hz halloc hv hr⟩
260
261/-- `int inflateInit_(z_streamp strm, const char *version, int stream_size)`
262Initialization establishes the public representation domain. -/
263theorem inflate_initialisation_domain_public : Goal.inflate_initialisation_domain := by
264  refine ⟨inflate_domain_general, public_witness_domain, ?_⟩
265  intro wb wrap bits hp
266  obtain ⟨after, hr, hi, _⟩ := inflate_domain_general witnessHeap (.tab 0) (.ref (.blk 1) 0)
267    wb wrap bits public_witness_domain hp (by rfl)
268  exact ⟨after, hr, hi⟩
269
270#print axioms inflate_initialisation_domain_public
271
272end ZlibF.Spec.Public.Proofs.InflateInit