inflate.c.base.lean

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

1import ZlibF.Zlib.«inflate.c»
2import ZlibF.Proof.«zutil.c»
3
4/-!
5# inflate.c: the stream invariant and the lemmas the stream functions share
6
7The statements of `docs/proof/inflate.md`, the window invariant W and of `docs/spec/api/inflate-stream.md`.
8The definitions of namespace `Zlib.Inflate.Spec` are part of what a theorem means (they are locked by the audit); the
9lemmas of `Zlib.Inflate.Proofs` are not.
10
11* `Uniq`: a block number holds an object of at most one table (the allocator takes `nextBlk` for every kind).
12* `WinInv`: the window of an inflate state.
13* `StInv`: the representation invariant of an inflate state (window, bit buffer, table pointers).
14* `Live`: the stream is one that `inflateStateCheck` accepts, and its state is the record `st` at block `zs`.
15* `Good`: `Live`, `StInv`, `Uniq` and `Fresh` together.
16-/
17
18namespace Zlib.Inflate.Spec
19open C
20
21/-- The heap with the state record `zs` replaced. -/
22def setI (h : Heap) (zs : Nat) (s : InflateState) : Heap := { h with istates := upd h.istates zs (some s) }
23
24/-- 1 if the table entry holds an object, else 0. -/
25def cnt {α : Type} (o : Option α) : Nat := if o.isSome then 1 else 0
26
27@[simp] theorem cnt_none {α : Type} : cnt (none : Option α) = 0 := rfl
28@[simp] theorem cnt_some {α : Type} (a : α) : cnt (some a) = 1 := rfl
29
30/-- A block number holds an object of at most one table. -/
31def Uniq (h : Heap) : Prop := ∀ b,
32  cnt (h.bytes b) + cnt (h.words b) + cnt (h.streams b) + cnt (h.gzheaders b) + cnt (h.dstates b) + cnt (h.istates b) +
33  cnt (h.gzstates b) ≤ 1
34
35/-- The window of an inflate state `st`: `NULL` with nothing in use, or a writable byte block of `2^wbits` bytes.
36`wsize` is 0 or `2^wbits`; `whave` bytes are valid; `wnext` is the next write position, which equals `whave` while the
37window is not full (`docs/proof/inflate.md`, invariant W). -/
38structure WinInv (h : Heap) (st : InflateState) : Prop where
39  wbits : st.wbits.toNat ≤ 15
40  block : st.window = .null ∨
41    ∃ w a, st.window = .ref (.blk w) 0 ∧ h.bytes w = some a ∧ h.ro w = false ∧ a.size = 2 ^ st.wbits.toNat
42  nullws : st.window = .null → st.wsize = 0
43  ws : st.wsize.toNat = 0 ∨ st.wsize.toNat = 2 ^ st.wbits.toNat
44  hv : st.whave.toNat ≤ st.wsize.toNat
45  wn : st.wnext.toNat < st.wsize.toNat ∨ (st.wsize.toNat = 0 ∧ st.wnext.toNat = 0)
46  eq : st.whave.toNat < st.wsize.toNat → st.wnext.toNat = st.whave.toNat
47
48/-- The table pointers of the state `zs`: `next` is in `codes`; `lencode` and `distcode` are both in `codes` (a
49dynamic block, or the start) or are the two static fixed tables (a stream stopped inside a fixed block). -/
50def PtrInv (zs : Nat) (st : InflateState) : Prop :=
51  (∃ i, st.next = .ref (.istate_codes zs) i ∧ i ≤ 1444) ∧
52  ((∃ i j, st.lencode = .ref (.istate_codes zs) i ∧ st.distcode = .ref (.istate_codes zs) j ∧ i ≤ 1443 ∧ j ≤ 1443) ∨
53   (st.lencode = .ref .st_lenfix 0 ∧ st.distcode = .ref .st_distfix 0))
54
55/-- The representation invariant of an inflate state, as far as the stream functions need it: the arrays have the
56size of the C declaration, the window invariant, `reqbits` is a valid window size, the bit buffer holds at most 39 bits
57(`NEEDBITS` of at most 32 bits pulls whole bytes while fewer are present), and the table pointers. -/
58structure StInv (h : Heap) (zs : Nat) (st : InflateState) : Prop where
59  wf : st.WellFormed
60  win : WinInv h st
61  reqbits : st.reqbits.toNat ≤ 15
62  bits : st.bits.toNat ≤ 39
63  ptr : PtrInv zs st
64
65/-- The stream `r` is the record `z`; its state is the record `st` at block `zs`, which points back to the stream; the
66mode is in the range `inflateStateCheck` accepts; the stream has the default allocator functions or none. -/
67structure Live (h : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (st : InflateState) : Prop where
68  hz : r.get h = some z
69  hs : h.istates zs = some st
70  zst : z.state = some (.inflate zs)
71  back : st.strm = some r
72  mode : HEAD ≤ st.mode ∧ st.mode ≤ SYNC
73  zalloc : z.zalloc ≠ .null
74  zfree : z.zfree ≠ .null
75
76/-- The stream functions can allocate and free: the allocator functions are the default ones (the only ones the model
77has; any other makes the translation fault). -/
78def DefAlloc (z : ZStream) : Prop := z.zalloc = .fn "zcalloc" ∧ z.zfree = .fn "zcfree"
79
80/-- Everything the stream functions assume of the heap around a live stream. -/
81structure Good (h : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (st : InflateState) : Prop where
82  live : Live h r zs z st
83  inv : StInv h zs st
84  uniq : Uniq h
85  fresh : Fresh h
86
87/-- The window block of the state, if there is one. -/
88def WinBlk (st : InflateState) (w : Nat) : Prop := st.window = .ref (.blk w) 0
89
90/-- The blocks a stream owns: its state record and its window block. -/
91def OwnedBy (zs : Nat) (st : InflateState) (b : Nat) : Prop := b = zs ∨ ∃ w, WinBlk st w ∧ b = w
92
93end Zlib.Inflate.Spec
94
95namespace Zlib.Inflate.Proofs
96open C Zlib.Inflate Zlib.Inflate.Spec
97
98@[simp] theorem setI_istates_same (h : Heap) (zs : Nat) (s : InflateState) : (setI h zs s).istates zs = some s := by
99  simp [setI]
100@[simp] theorem setI_istates_ne (h : Heap) (zs x : Nat) (s : InflateState) (hx : x ≠ zs) :
101    (setI h zs s).istates x = h.istates x := by simp [setI, upd_ne _ _ _ _ hx]
102@[simp] theorem setI_bytes (h : Heap) (zs : Nat) (s : InflateState) : (setI h zs s).bytes = h.bytes := rfl
103@[simp] theorem setI_streams (h : Heap) (zs : Nat) (s : InflateState) : (setI h zs s).streams = h.streams := rfl
104@[simp] theorem setI_gzstates (h : Heap) (zs : Nat) (s : InflateState) : (setI h zs s).gzstates = h.gzstates := rfl
105@[simp] theorem setI_ro (h : Heap) (zs : Nat) (s : InflateState) : (setI h zs s).ro = h.ro := rfl
106@[simp] theorem setI_nextBlk (h : Heap) (zs : Nat) (s : InflateState) : (setI h zs s).nextBlk = h.nextBlk := rfl
107@[simp] theorem setI_setI (h : Heap) (zs : Nat) (s s' : InflateState) : setI (setI h zs s) zs s' = setI h zs s' := by
108  simp [setI, upd_upd]
109
110theorem ZStreamRef.get_put_same {h : Heap} {r : ZStreamRef} {z : ZStream} (e : r.get h = some z) (v : ZStream) :
111    r.get (r.put h v) = some v := by
112  cases r with
113  | tab i => simp [ZStreamRef.get] at e; simp [ZStreamRef.put, ZStreamRef.get, e]
114  | in_gzstate_strm i =>
115    simp [ZStreamRef.get] at e
116    obtain ⟨g, hg, -⟩ := e
117    simp [ZStreamRef.put, ZStreamRef.get, hg]
118
119@[simp] theorem ZStreamRef.get_setI (h : Heap) (r : ZStreamRef) (zs : Nat) (s : InflateState) :
120    r.get (setI h zs s) = r.get h := by
121  cases r <;> rfl
122
123@[simp] theorem ZStreamRef.put_istates (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).istates = h.istates := by
124  cases r with
125  | tab i => simp only [ZStreamRef.put]; split <;> rfl
126  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
127
128@[simp] theorem ZStreamRef.put_bytes (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).bytes = h.bytes := by
129  cases r with
130  | tab i => simp only [ZStreamRef.put]; split <;> rfl
131  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
132
133@[simp] theorem ZStreamRef.put_ro (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).ro = h.ro := by
134  cases r with
135  | tab i => simp only [ZStreamRef.put]; split <;> rfl
136  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
137
138@[simp] theorem ZStreamRef.put_words (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).words = h.words := by
139  cases r with
140  | tab i => simp only [ZStreamRef.put]; split <;> rfl
141  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
142
143@[simp] theorem ZStreamRef.put_dstates (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).dstates = h.dstates := by
144  cases r with
145  | tab i => simp only [ZStreamRef.put]; split <;> rfl
146  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
147
148@[simp] theorem ZStreamRef.put_gzheaders (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).gzheaders = h.gzheaders := by
149  cases r with
150  | tab i => simp only [ZStreamRef.put]; split <;> rfl
151  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
152
153@[simp] theorem ZStreamRef.put_nextBlk (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).nextBlk = h.nextBlk := by
154  cases r with
155  | tab i => simp only [ZStreamRef.put]; split <;> rfl
156  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
157
158@[simp] theorem ZStreamRef.put_nalloc (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).nalloc = h.nalloc := by
159  cases r with
160  | tab i => simp only [ZStreamRef.put]; split <;> rfl
161  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
162
163@[simp] theorem ZStreamRef.put_allocOk (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).allocOk = h.allocOk := by
164  cases r with
165  | tab i => simp only [ZStreamRef.put]; split <;> rfl
166  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
167
168@[simp] theorem ZStreamRef.put_garbage (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).garbage = h.garbage := by
169  cases r with
170  | tab i => simp only [ZStreamRef.put]; split <;> rfl
171  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
172
173@[simp] theorem ZStreamRef.put_static (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).static = h.static := by
174  cases r with
175  | tab i => simp only [ZStreamRef.put]; split <;> rfl
176  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
177
178@[simp] theorem ZStreamRef.get_put (h : Heap) (r : ZStreamRef) (v : ZStream) :
179    r.get (r.put h v) = (r.get h).map (fun _ => v) := by
180  cases r with
181  | tab i =>
182    simp only [ZStreamRef.put, ZStreamRef.get]
183    cases hh : h.streams i <;> simp [hh]
184  | in_gzstate_strm i =>
185    simp only [ZStreamRef.put, ZStreamRef.get]
186    cases hh : h.gzstates i <;> simp [hh]
187
188@[simp] theorem ZStreamRef.put_put (h : Heap) (r : ZStreamRef) (v v' : ZStream) : r.put (r.put h v) v' = r.put h v' := by
189  cases r with
190  | tab i =>
191    simp only [ZStreamRef.put]
192    cases hh : h.streams i <;> simp [hh, upd_upd]
193  | in_gzstate_strm i =>
194    simp only [ZStreamRef.put]
195    cases hh : h.gzstates i <;> simp [hh, upd_upd]
196
197@[simp] theorem ZStreamRef.put_setI (h : Heap) (r : ZStreamRef) (zs : Nat) (s : InflateState) (v : ZStream) :
198    r.put (setI h zs s) v = setI (r.put h v) zs s := by
199  cases r with
200  | tab i => simp only [ZStreamRef.put, setI]; cases hh : h.streams i <;> simp
201  | in_gzstate_strm i => simp only [ZStreamRef.put, setI]; cases hh : h.gzstates i <;> simp
202
203/-! ### Reading and writing the stream and the state -/
204
205theorem castI {h : Heap} {zs : Nat} : castInflateState (some (.inflate zs)) h = .ok (some (.tab zs), h) := rfl
206
207/-- The access functions as rewrite rules: they read the table, so that a proof rewrites with the facts about the table. -/
208theorem ldI_eq (h : Heap) (i : Nat) : ldInflateState (some (.tab i)) h =
209    match h.istates i with
210    | some v => .ok (v, h)
211    | none => .error (.ub "access through a dangling pointer (inflate_state)") := rfl
212
213theorem ldZ_eq (h : Heap) (r : ZStreamRef) : ldZStream (some r) h =
214    match r.get h with
215    | some v => .ok (v, h)
216    | none => .error (.ub "access through a dangling pointer (z_stream)") := rfl
217
218theorem rdI_eq {α : Type} (h : Heap) (i : Nat) (f : InflateState → α) : rdS (some (.tab i)) f h =
219    match h.istates i with
220    | some v => .ok (f v, h)
221    | none => .error (.ub "access through a dangling pointer (inflate_state)") := by
222  simp only [rdS, bind_app, ldI_eq]; cases h.istates i <;> rfl
223
224theorem rdZ_eq {α : Type} (h : Heap) (r : ZStreamRef) (f : ZStream → α) : rdZ (some r) f h =
225    match r.get h with
226    | some v => .ok (f v, h)
227    | none => .error (.ub "access through a dangling pointer (z_stream)") := by
228  simp only [rdZ, bind_app, ldZ_eq]; cases r.get h <;> rfl
229
230theorem wrI_eq (h : Heap) (i : Nat) (f : InflateState → InflateState) : wrS (some (.tab i)) f h =
231    match h.istates i with
232    | some v => .ok ((), setI h i (f v))
233    | none => .error (.ub "access through a dangling pointer (inflate_state)") := by
234  cases hh : h.istates i with
235  | none => simp [wrS, bind_app, ldI_eq, hh]
236  | some v => simp [wrS, bind_app, ldI_eq, hh, stInflateState_tab hh, setI]
237
238theorem wrZ_eq (h : Heap) (r : ZStreamRef) (f : ZStream → ZStream) : wrZ (some r) f h =
239    match r.get h with
240    | some v => .ok ((), r.put h (f v))
241    | none => .error (.ub "access through a dangling pointer (z_stream)") := by
242  have hro : r.isRo = false := by cases r <;> rfl
243  cases hh : r.get h with
244  | none => simp [wrZ, bind_app, ldZ_eq, hh]
245  | some v => simp [wrZ, bind_app, ldZ_eq, hh, stZStream_ok hh hro]
246
247theorem stI_eq (h : Heap) (i : Nat) (v : InflateState) : stInflateState (some (.tab i)) v h =
248    match h.istates i with
249    | some _ => .ok ((), setI h i v)
250    | none => .error (.ub "access through a dangling pointer (inflate_state)") := by
251  cases hh : h.istates i with
252  | none => simp [stInflateState, InflateStateRef.get, hh]
253  | some w => simp [stInflateState_tab hh, setI, hh]
254
255theorem stZ_eq (h : Heap) (r : ZStreamRef) (v : ZStream) : stZStream (some r) v h =
256    match r.get h with
257    | some _ => .ok ((), r.put h v)
258    | none => .error (.ub "access through a dangling pointer (z_stream)") := by
259  have hro : r.isRo = false := by cases r <;> rfl
260  cases hh : r.get h with
261  | none => simp [stZStream, hh]
262  | some w => simp [stZStream_ok hh hro, hh]
263
264/-- Evaluate a straight-line sequence of accesses to a stream and its state. -/
265macro "isimp" "[" ts:Lean.Parser.Tactic.simpLemma,* "]" : tactic =>
266  `(tactic| simp [bind_app, pure_app, ldI_eq, ldZ_eq, rdI_eq, rdZ_eq, wrI_eq, wrZ_eq, stI_eq, stZ_eq, castI, $ts,*])
267
268/-! ### The stream check -/
269
270theorem stateCheck_live {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
271    (hL : Live h r zs z st) : inflateStateCheck (some r) h = .ok (0, h) := by
272  obtain ⟨hz, hs, zst, back, ⟨m1, m2⟩, za, zf⟩ := hL
273  have e1 : ldZStream (some r) h = .ok (z, h) := ldZStream_ok hz
274  unfold inflateStateCheck
275  have c : ¬ (st.mode < HEAD ∨ SYNC < st.mode) := by
276    rintro (c | c)
277    · have := UInt32.lt_iff_toNat_lt.mp c; have := UInt32.le_iff_toNat_le.mp m1; omega
278    · have := UInt32.lt_iff_toNat_lt.mp c; have := UInt32.le_iff_toNat_le.mp m2; omega
279  simp [bind_app, e1, za, zf, zst, castInflateState_ok, ldInflateState_tab hs, back, c]
280
281end Zlib.Inflate.Proofs
282
283namespace Zlib.Inflate.Spec
284open C
285
286/-- The state record after `inflateResetKeep` (`zs` is its block number). -/
287def resetKeepState (zs : Nat) (st : InflateState) : InflateState :=
288  { st with
289    total := 0, mode := HEAD, last := 0, havedict := 0, flags := -1, dmax := 32768, head := none,
290    hold := 0, bits := 0, next := .ref (.istate_codes zs) 0, distcode := .ref (.istate_codes zs) 0,
291    lencode := .ref (.istate_codes zs) 0, sane := 1, back := -1 }
292
293/-- The stream record after `inflateResetKeep` of a stream whose state is `st`: `adler` is bit 0 of `wrap` unless
294`wrap` is 0. -/
295def resetKeepStream (z : ZStream) (st : InflateState) : ZStream :=
296  { z with
297    total_out := 0, total_in := 0, msg := .null, data_type := 0,
298    adler := if st.wrap != 0 then Zlib.Inflate.i2ul (st.wrap &&& 1) else z.adler }
299
300end Zlib.Inflate.Spec
301
302namespace Zlib.Inflate.Proofs
303open C Zlib.Inflate Zlib.Inflate.Spec
304
305theorem resetKeep_run {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
306    (hL : Live h r zs z st) :
307    inflateResetKeep (some r) h = .ok (Z_OK, setI (r.put h (resetKeepStream z st)) zs (resetKeepState zs st)) := by
308  have hz := hL.hz
309  have hs := hL.hs
310  unfold inflateResetKeep
311  by_cases hw : st.wrap = 0
312  · isimp [stateCheck_live hL, hL.zst, hz, hs, resetKeepState, resetKeepStream, hw, codesP]
313  · isimp [stateCheck_live hL, hL.zst, hz, hs, resetKeepState, resetKeepStream, hw, codesP]
314
315
316/-! ### Which objects exist: the shape of a heap -/
317
318/-- The two heaps hold an object in the same tables at the same block numbers (the objects may differ). -/
319def Shape (h h' : Heap) : Prop := ∀ b, (h'.bytes b).isSome = (h.bytes b).isSome ∧ (h'.words b).isSome = (h.words b).isSome ∧
320  (h'.streams b).isSome = (h.streams b).isSome ∧ (h'.gzheaders b).isSome = (h.gzheaders b).isSome ∧
321  (h'.dstates b).isSome = (h.dstates b).isSome ∧ (h'.istates b).isSome = (h.istates b).isSome ∧
322  (h'.gzstates b).isSome = (h.gzstates b).isSome
323
324theorem Shape.refl (h : Heap) : Shape h h := fun _ => ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
325
326theorem Shape.trans {h1 h2 h3 : Heap} (a : Shape h1 h2) (b : Shape h2 h3) : Shape h1 h3 := by
327  intro x
328  obtain ⟨a1, a2, a3, a4, a5, a6, a7⟩ := a x
329  obtain ⟨b1, b2, b3, b4, b5, b6, b7⟩ := b x
330  exact ⟨b1.trans a1, b2.trans a2, b3.trans a3, b4.trans a4, b5.trans a5, b6.trans a6, b7.trans a7⟩
331
332theorem Shape.uniq {h h' : Heap} (hS : Shape h h') (hU : Uniq h) : Uniq h' := by
333  intro b
334  obtain ⟨e1, e2, e3, e4, e5, e6, e7⟩ := hS b
335  have := hU b
336  simp only [cnt, e1, e2, e3, e4, e5, e6, e7] at this ⊢
337  exact this
338
339theorem Shape.live {h h' : Heap} (hS : Shape h h') (b : Nat) : h'.live b ↔ h.live b := by
340  obtain ⟨e1, e2, e3, e4, e5, e6, e7⟩ := hS b
341  simp only [Heap.live, ← Option.isSome_iff_ne_none, e1, e2, e3, e4, e5, e6, e7]
342
343theorem Shape.fresh {h h' : Heap} (hS : Shape h h') (hn : h'.nextBlk = h.nextBlk) (hF : Fresh h) : Fresh h' := by
344  intro b hb hl
345  exact hF b (by omega) ((hS.live b).1 hl)
346
347theorem shape_setI {h : Heap} {zs : Nat} {s0 : InflateState} (e : h.istates zs = some s0) (s : InflateState) :
348    Shape h (setI h zs s) := by
349  intro b
350  by_cases hb : b = zs
351  · subst hb; simp [setI, e]
352  · simp [setI, upd_ne _ _ _ _ hb]
353
354theorem shape_put {h : Heap} {r : ZStreamRef} {z0 : ZStream} (e : r.get h = some z0) (v : ZStream) :
355    Shape h (r.put h v) := by
356  cases r with
357  | tab i =>
358    simp only [ZStreamRef.get] at e
359    intro b
360    by_cases hb : b = i
361    · subst hb; simp [ZStreamRef.put, e]
362    · simp [ZStreamRef.put, e, upd_ne _ _ _ _ hb]
363  | in_gzstate_strm i =>
364    simp only [ZStreamRef.get] at e
365    obtain ⟨g, hg, -⟩ := Option.map_eq_some_iff.mp e
366    intro b
367    by_cases hb : b = i
368    · subst hb; simp [ZStreamRef.put, hg]
369    · simp [ZStreamRef.put, hg, upd_ne _ _ _ _ hb]
370
371theorem shape_setB {h : Heap} {w : Nat} {a0 : Array UInt8} (e : h.bytes w = some a0) (a : Array UInt8) :
372    Shape h { h with bytes := upd h.bytes w (some a) } := by
373  intro b
374  by_cases hb : b = w
375  · subst hb; simp [e]
376  · simp [upd_ne _ _ _ _ hb]
377
378/-! ### Preserving the invariants -/
379
380theorem _root_.Zlib.Inflate.Spec.WinInv.congr {h h' : Heap} {st : InflateState} (hb : h'.bytes = h.bytes) (hr : h'.ro = h.ro)
381    (hW : WinInv h st) : WinInv h' st := by
382  refine ⟨hW.wbits, ?_, hW.nullws, hW.ws, hW.hv, hW.wn, hW.eq⟩
383  rcases hW.block with hn | ⟨w, a, hw, ha, hro, hsz⟩
384  · exact Or.inl hn
385  · exact Or.inr ⟨w, a, hw, by rw [hb]; exact ha, by rw [hr]; exact hro, hsz⟩
386
387theorem _root_.Zlib.Inflate.Spec.StInv.congr {h h' : Heap} {zs : Nat} {st : InflateState} (hb : h'.bytes = h.bytes) (hr : h'.ro = h.ro)
388    (hI : StInv h zs st) : StInv h' zs st :=
389  ⟨hI.wf, hI.win.congr hb hr, hI.reqbits, hI.bits, hI.ptr⟩
390
391/-- Rewrite the stream record and the state record of a live stream, keeping the state pointer, the back pointer, the
392mode range and the allocator functions. -/
393theorem _root_.Zlib.Inflate.Spec.Good.setZI {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
394    (hG : Good h r zs z st) {z' : ZStream} {st' : InflateState}
395    (hz : z'.state = z.state) (hza : z'.zalloc ≠ .null) (hzf : z'.zfree ≠ .null) (hback : st'.strm = st.strm)
396    (hm : HEAD ≤ st'.mode ∧ st'.mode ≤ SYNC) (hI : StInv h zs st') :
397    Good (setI (r.put h z') zs st') r zs z' st' := by
398  have hS : Shape h (setI (r.put h z') zs st') :=
399    (shape_put hG.live.hz z').trans (shape_setI (by simpa using hG.live.hs) st')
400  refine ⟨⟨?_, by simp, hz.trans hG.live.zst, hback.trans hG.live.back, hm, hza, hzf⟩, StInv.congr (h := h) (h' := setI (r.put h z') zs st') (by simp) (by simp) hI,
401    hS.uniq hG.uniq, hS.fresh (by simp) hG.fresh⟩
402  simp [ZStreamRef.get_put, hG.live.hz]
403
404theorem Shape.owns {h h' : Heap} (hS : Shape h h') {S : Nat → Prop} (hO : h.Owns S) : h'.Owns S :=
405  fun b => (hS.live b).trans (hO b)
406
407/-! ### The stream check, in general -/
408
409theorem hdec {a b : UInt32} : a ≤ b ∨ b < a := by
410  rcases Nat.lt_or_ge b.toNat a.toNat with h | h
411  · exact Or.inr (UInt32.lt_iff_toNat_lt.mpr h)
412  · exact Or.inl (UInt32.le_iff_toNat_le.mpr h)
413
414end Zlib.Inflate.Proofs
415
416namespace Zlib.Inflate.Spec
417open C
418
419/-- The streams `inflateStateCheck` handles: `NULL`, or a live stream record that has a `NULL` allocator function, or no
420state, or a state that is a live inflate state record. (A state that is a deflate state, a freed state or a freed
421stream is undefined behaviour in C and a fault here.) -/
422def StreamDom (h : Heap) (strm : ZStreamPtr) : Prop :=
423  strm = none ∨ ∃ r z, strm = some r ∧ r.get h = some z ∧
424    (z.zalloc = .null ∨ z.zfree = .null ∨ z.state = none ∨ ∃ zs st, z.state = some (.inflate zs) ∧ h.istates zs = some st)
425
426/-- The heap after `free(p)` for a window pointer: the byte block is gone, everything else is as it was. -/
427def freeWin (h : Heap) (p : BPtr) : Heap :=
428  match p with
429  | .ref (.blk w) 0 => { h with bytes := upd h.bytes w none }
430  | _ => h
431
432/-- The stream is one `inflateStateCheck` accepts. -/
433def Initialised (h : Heap) (strm : ZStreamPtr) : Prop := ∃ r zs z st, strm = some r ∧ Live h r zs z st
434
435end Zlib.Inflate.Spec
436
437namespace Zlib.Inflate.Proofs
438open C Zlib.Inflate Zlib.Inflate.Spec
439
440/-- **inflateStateCheck, safety and specification.** On every stream of the domain `StreamDom` (`NULL`, or a live stream
441whose state pointer is `NULL`, an inflate state or irrelevant because an allocator function is `NULL`) the check
442returns without a fault and without changing the heap; it returns 0 exactly for an initialised stream (the stream and
443its state point to each other, the allocator functions are not `NULL`, and the mode is in the range from `HEAD` to
444`SYNC`) and 1 otherwise. -/
445theorem inflateStateCheck_total {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) :
446    ∃ v, inflateStateCheck strm h = .ok (v, h) ∧ (v = 0 ∧ Initialised h strm ∨ v = 1 ∧ ¬ Initialised h strm) := by
447  rcases hD with rfl | ⟨r, z, rfl, hr, hcase⟩
448  · refine ⟨1, by simp [inflateStateCheck], Or.inr ⟨rfl, ?_⟩⟩
449    rintro ⟨r, zs, z, st, hh, -⟩; cases hh
450  · have e1 : ldZStream (some r) h = .ok (z, h) := ldZStream_ok hr
451    by_cases hza : z.zalloc = .null
452    · refine ⟨1, by simp [inflateStateCheck, e1, hza], Or.inr ⟨rfl, ?_⟩⟩
453      rintro ⟨r', zs, z', st, hh, hL⟩
454      cases hh; exact hL.zalloc (by rw [hL.hz] at hr; cases hr; exact hza)
455    by_cases hzf : z.zfree = .null
456    · refine ⟨1, by simp [inflateStateCheck, e1, hza, hzf], Or.inr ⟨rfl, ?_⟩⟩
457      rintro ⟨r', zs, z', st, hh, hL⟩
458      cases hh; exact hL.zfree (by rw [hL.hz] at hr; cases hr; exact hzf)
459    rcases hcase with h1 | h1 | h1 | ⟨zs, st, hzs, hst⟩
460    · exact absurd h1 hza
461    · exact absurd h1 hzf
462    · refine ⟨1, by simp [inflateStateCheck, e1, hza, hzf, h1, castInflateState], Or.inr ⟨rfl, ?_⟩⟩
463      rintro ⟨r', zs, z', st, hh, hL⟩
464      cases hh; rw [hL.hz] at hr; cases hr; rw [hL.zst] at h1; cases h1
465    · have ec : castInflateState z.state h = .ok (some (.tab zs), h) := by rw [hzs]; exact castI
466      by_cases c1 : st.strm = some r
467      · by_cases c2 : st.mode < HEAD ∨ SYNC < st.mode
468        · refine ⟨1, ?_, Or.inr ⟨rfl, ?_⟩⟩
469          · simp [inflateStateCheck, bind_app, e1, castI, ldInflateState_tab hst, hza, hzf, hzs, c1, c2]
470          · rintro ⟨r', zs', z', st', hh, hL⟩
471            cases hh
472            rw [hL.hz] at hr; cases hr
473            rw [hL.zst] at hzs; cases hzs
474            rw [hL.hs] at hst; cases hst
475            have m1 := UInt32.le_iff_toNat_le.mp hL.mode.1
476            have m2 := UInt32.le_iff_toNat_le.mp hL.mode.2
477            rcases c2 with c | c
478            · have := UInt32.lt_iff_toNat_lt.mp c; omega
479            · have := UInt32.lt_iff_toNat_lt.mp c; omega
480        · have m1 : HEAD ≤ st.mode := by
481            rcases hdec (a := HEAD) (b := st.mode) with c | c
482            · exact c
483            · exact absurd (Or.inl c) c2
484          have m2 : st.mode ≤ SYNC := by
485            rcases hdec (a := st.mode) (b := SYNC) with c | c
486            · exact c
487            · exact absurd (Or.inr c) c2
488          have hL : Live h r zs z st := ⟨hr, hst, hzs, c1, ⟨m1, m2⟩, hza, hzf⟩
489          exact ⟨0, stateCheck_live hL, Or.inl ⟨rfl, r, zs, z, st, rfl, hL⟩⟩
490      · refine ⟨1, ?_, Or.inr ⟨rfl, ?_⟩⟩
491        · simp [inflateStateCheck, bind_app, e1, castI, ldInflateState_tab hst, hza, hzf, hzs, c1]
492        · rintro ⟨r', zs', z', st', hh, hL⟩
493          cases hh
494          rw [hL.hz] at hr; cases hr
495          rw [hL.zst] at hzs; cases hzs
496          rw [hL.hs] at hst; cases hst
497          exact c1 hL.back
498
499
500/-- The state check fails: a function that starts with it returns `Z_STREAM_ERROR` and changes nothing. -/
501theorem notInit_check {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ Initialised h strm) :
502    inflateStateCheck strm h = .ok (1, h) := by
503  obtain ⟨v, hv, hc⟩ := inflateStateCheck_total hD
504  rcases hc with ⟨rfl, hI⟩ | ⟨rfl, -⟩
505  · exact absurd hI hN
506  · exact hv
507
508/-! ### `inflateResetKeep` -/
509
510theorem _root_.Zlib.Inflate.Spec.StInv.resetKeep {h : Heap} {zs : Nat} {st : InflateState} (hI : StInv h zs st) :
511    StInv h zs (resetKeepState zs st) := by
512  refine ⟨hI.wf, ?_, hI.reqbits, by simp [resetKeepState], ?_⟩
513  · exact ⟨hI.win.wbits, hI.win.block, hI.win.nullws, hI.win.ws, hI.win.hv, hI.win.wn, hI.win.eq⟩
514  · refine ⟨⟨0, by simp [resetKeepState], by omega⟩, Or.inl ⟨0, 0, by simp [resetKeepState], by simp [resetKeepState], by omega, by omega⟩⟩
515
516theorem mode_head : HEAD ≤ HEAD ∧ HEAD ≤ SYNC := by decide
517
518/-- **inflateResetKeep, safety.** On an initialised stream (`Good`) the call returns `Z_OK`, runs without a fault, and
519changes exactly the stream record (`resetKeepStream`) and the state record (`resetKeepState`). Afterwards the stream is
520initialised again with the invariants intact, and the set of live blocks is the same (no allocation, no free). -/
521theorem inflateResetKeep_safe {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
522    (hG : Good h r zs z st) :
523    ∃ h', C.run (inflateResetKeep (some r)) h = .ok (Z_OK, h') ∧
524      h' = setI (r.put h (resetKeepStream z st)) zs (resetKeepState zs st) ∧
525      Good h' r zs (resetKeepStream z st) (resetKeepState zs st) ∧ (∀ b, h'.live b ↔ h.live b) := by
526  refine ⟨_, resetKeep_run hG.live, rfl, ?_, ?_⟩
527  · exact hG.setZI (by simp [resetKeepStream]) (by simpa [resetKeepStream] using hG.live.zalloc)
528      (by simpa [resetKeepStream] using hG.live.zfree) (by simp [resetKeepState]) (by simpa [resetKeepState] using mode_head)
529      hG.inv.resetKeep
530  · intro b
531    exact ((shape_put hG.live.hz _).trans (shape_setI (by simpa using hG.live.hs) _)).live b
532
533
534/-! ### Uniqueness and freeing -/
535
536theorem Uniq.bytes_only {h : Heap} (hU : Uniq h) {b : Nat} {a : Array UInt8} (hb : h.bytes b = some a) :
537    h.words b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.dstates b = none ∧ h.istates b = none ∧
538    h.gzstates b = none := by
539  have := hU b
540  simp only [hb, cnt_some] at this
541  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
542  · cases hx : h.words b with
543    | none => rfl
544    | some _ => simp only [hx, cnt_some] at this <;> omega
545  · cases hx : h.streams b with
546    | none => rfl
547    | some _ => simp only [hx, cnt_some] at this <;> omega
548  · cases hx : h.gzheaders b with
549    | none => rfl
550    | some _ => simp only [hx, cnt_some] at this <;> omega
551  · cases hx : h.dstates b with
552    | none => rfl
553    | some _ => simp only [hx, cnt_some] at this <;> omega
554  · cases hx : h.istates b with
555    | none => rfl
556    | some _ => simp only [hx, cnt_some] at this <;> omega
557  · cases hx : h.gzstates b with
558    | none => rfl
559    | some _ => simp only [hx, cnt_some] at this <;> omega
560
561theorem Uniq.istates_only {h : Heap} (hU : Uniq h) {b : Nat} {a : InflateState} (hb : h.istates b = some a) :
562    h.words b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.dstates b = none ∧ h.bytes b = none ∧
563    h.gzstates b = none := by
564  have := hU b
565  simp only [hb, cnt_some] at this
566  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
567  · cases hx : h.words b with
568    | none => rfl
569    | some _ => simp only [hx, cnt_some] at this <;> omega
570  · cases hx : h.streams b with
571    | none => rfl
572    | some _ => simp only [hx, cnt_some] at this <;> omega
573  · cases hx : h.gzheaders b with
574    | none => rfl
575    | some _ => simp only [hx, cnt_some] at this <;> omega
576  · cases hx : h.dstates b with
577    | none => rfl
578    | some _ => simp only [hx, cnt_some] at this <;> omega
579  · cases hx : h.bytes b with
580    | none => rfl
581    | some _ => simp only [hx, cnt_some] at this <;> omega
582  · cases hx : h.gzstates b with
583    | none => rfl
584    | some _ => simp only [hx, cnt_some] at this <;> omega
585
586theorem freeWin_blk (h : Heap) (w : Nat) : freeWin h (.ref (.blk w) 0) = { h with bytes := upd h.bytes w none } := rfl
587theorem freeWin_null (h : Heap) : freeWin h .null = h := rfl
588
589@[simp] theorem freeWin_istates (h : Heap) (p : BPtr) : (freeWin h p).istates = h.istates := by
590  unfold freeWin; split <;> rfl
591@[simp] theorem freeWin_streams (h : Heap) (p : BPtr) : (freeWin h p).streams = h.streams := by
592  unfold freeWin; split <;> rfl
593@[simp] theorem freeWin_gzstates (h : Heap) (p : BPtr) : (freeWin h p).gzstates = h.gzstates := by
594  unfold freeWin; split <;> rfl
595@[simp] theorem freeWin_nextBlk (h : Heap) (p : BPtr) : (freeWin h p).nextBlk = h.nextBlk := by
596  unfold freeWin; split <;> rfl
597@[simp] theorem freeWin_words (h : Heap) (p : BPtr) : (freeWin h p).words = h.words := by
598  unfold freeWin; split <;> rfl
599@[simp] theorem freeWin_ro (h : Heap) (p : BPtr) : (freeWin h p).ro = h.ro := by
600  unfold freeWin; split <;> rfl
601@[simp] theorem freeWin_dstates (h : Heap) (p : BPtr) : (freeWin h p).dstates = h.dstates := by
602  unfold freeWin; split <;> rfl
603@[simp] theorem freeWin_gzheaders (h : Heap) (p : BPtr) : (freeWin h p).gzheaders = h.gzheaders := by
604  unfold freeWin; split <;> rfl
605
606@[simp] theorem ZStreamRef.get_freeWin (h : Heap) (p : BPtr) (r : ZStreamRef) : r.get (freeWin h p) = r.get h := by
607  cases r <;> simp [ZStreamRef.get]
608
609@[simp] theorem ZStreamRef.put_freeWin (h : Heap) (p : BPtr) (r : ZStreamRef) (v : ZStream) :
610    r.put (freeWin h p) v = freeWin (r.put h v) p := by
611  cases p with
612  | null => rfl
613  | ref x o =>
614    cases x with
615    | blk w =>
616      cases o with
617      | zero => cases r <;> simp [ZStreamRef.put, freeWin] <;> split <;> rfl
618      | succ o => rfl
619    | _ => rfl
620
621@[simp] theorem setI_freeWin (h : Heap) (p : BPtr) (zs : Nat) (s : InflateState) :
622    setI (freeWin h p) zs s = freeWin (setI h zs s) p := by
623  cases p with
624  | null => rfl
625  | ref x o =>
626    cases x with
627    | blk w => cases o with
628      | zero => simp [freeWin, setI]
629      | succ o => rfl
630    | _ => rfl
631
632theorem zfreeB_run {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hf : z.zfree = .fn "zcfree")
633    {p : BPtr} (hp : p = .null ∨ ∃ b a, p = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false) :
634    ZFREEB (some r) p h = .ok ((), freeWin h p) := by
635  rcases hp with rfl | ⟨b, a, rfl, hb, hro⟩
636  · simp [ZFREEB, ldZ_eq, hz, hf, Zlib.Zutil.zcfree, freeWin_null, freeB_null]
637  · simp [ZFREEB, ldZ_eq, hz, hf, Zlib.Zutil.zcfree, freeWin_blk, freeB_ok hb hro]
638
639theorem uniq_freeWin {h : Heap} (hU : Uniq h) (p : BPtr) : Uniq (freeWin h p) := by
640  cases p with
641  | null => exact hU
642  | ref x o =>
643    cases x with
644    | blk w =>
645      cases o with
646      | zero =>
647        intro b
648        have := hU b
649        by_cases hb : b = w
650        · subst hb
651          simp only [freeWin_blk, upd_same, cnt_none] at this ⊢
652          omega
653        · simpa only [freeWin_blk, upd_ne _ _ _ _ hb] using this
654      | succ o => exact hU
655    | _ => exact hU
656
657theorem live_freeWin {h : Heap} (p : BPtr) (b : Nat) : (freeWin h p).live b → h.live b := by
658  cases p with
659  | null => exact id
660  | ref x o =>
661    cases x with
662    | blk w =>
663      cases o with
664      | zero =>
665        intro hl
666        by_cases hb : b = w
667        · subst hb
668          simp only [Heap.live, freeWin_blk, upd_same] at hl
669          rcases hl with hl | hl
670          · exact absurd rfl hl
671          · exact Or.inr hl
672        · simp only [Heap.live, freeWin_blk, upd_ne _ _ _ _ hb] at hl
673          exact hl
674      | succ o => exact id
675    | _ => exact id
676
677theorem fresh_freeWin {h : Heap} (hF : Fresh h) (p : BPtr) : Fresh (freeWin h p) := by
678  intro b hb hl
679  exact hF b (by simpa using hb) (live_freeWin p b hl)
680
681theorem owns_freeWin {h : Heap} (hU : Uniq h) {w : Nat} {a : Array UInt8} (hb : h.bytes w = some a) {S : Nat → Prop}
682    (hO : h.Owns S) : (freeWin h (.ref (.blk w) 0)).Owns (fun b => S b ∧ b ≠ w) := by
683  intro b
684  by_cases hbw : b = w
685  · subst hbw
686    obtain ⟨e1, e2, e3, e4, e5, e6⟩ := Uniq.bytes_only hU hb
687    simp [Heap.live, freeWin_blk, e1, e2, e3, e4, e5, e6]
688  · have := hO b
689    simp only [Heap.live, freeWin_blk, upd_ne _ _ _ _ hbw] at this ⊢
690    simp [hbw, this]
691
692end Zlib.Inflate.Proofs