deflate.c.base.lean

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

1import ZlibF.Zlib.«deflate.c»
2import ZlibF.Proof.«zutil.c»
3import ZlibF.Proof.«trees.c.bits»
4
5/-!
6# deflate.c: the stream invariant and the lemmas the stream functions share
7
8The statements of `docs/spec/api/deflate-stream.md`. The definitions of namespace `Zlib.Deflate.Spec` are part of
9what a theorem means; the lemmas of `Zlib.Deflate.Proofs` are not.
10
11* `Uniq`: a block number holds an object of at most one table.
12* `DBlocks`: the four buffers of a deflate state (window, prev, head, pending_buf) are live blocks of the right size.
13* `DStInv`: the representation invariant of a deflate state record (array sizes, hash and window relations, the
14  ranges of level, strategy and wrapper, the pointers into the blocks, the symbol buffer and the bit buffer).
15* `DLive`: the stream is one that `deflateStateCheck` accepts, and its state is the record `d` at block `ds`.
16* `DGood`: `DLive`, `DStInv`, `Uniq`, `Fresh` and the trees invariant together.
17
18The proofs of the engine (`deflate`, `fill_window`, the strategies) import this module: a function that keeps
19`DGood` keeps the bounds the next function needs.
20
21**The trees invariant.** `DGood` includes `TreesInv h ds` of `trees.c.inv`: the invariant the functions of `trees.c` need
22(descriptors, static tables, the byte block that holds `pending_buf` and `sym_buf`). Several of its facts are also stated
23in `DStInv` (`bits`, `sym`), so that a proof about the lifecycle functions can read them without unpacking it.
24-/
25
26namespace Zlib.Deflate.Spec
27open C
28
29/-- 1 if the table entry holds an object, else 0. -/
30def cnt {α : Type} (o : Option α) : Nat := if o.isSome then 1 else 0
31
32@[simp] theorem cnt_none {α : Type} : cnt (none : Option α) = 0 := rfl
33@[simp] theorem cnt_some {α : Type} (a : α) : cnt (some a) = 1 := rfl
34
35/-- A block number holds an object of at most one table. -/
36def Uniq (h : Heap) : Prop := ∀ b,
37  cnt (h.bytes b) + cnt (h.words b) + cnt (h.streams b) + cnt (h.gzheaders b) + cnt (h.dstates b) + cnt (h.istates b) +
38  cnt (h.gzstates b) ≤ 1
39
40/-- The heap with the deflate state record `ds` replaced. -/
41def setD (h : Heap) (ds : Nat) (d : DeflateState) : Heap := { h with dstates := upd h.dstates ds (some d) }
42
43/-- The status values `deflateStateCheck` accepts: the zlib header, the gzip header, extra, name, comment, header CRC,
44busy and finish. -/
45def GoodStatus (s : Int32) : Prop :=
46  s = INIT_STATE ∨ s = GZIP_STATE ∨ s = EXTRA_STATE ∨ s = NAME_STATE ∨ s = COMMENT_STATE ∨ s = HCRC_STATE ∨
47  s = BUSY_STATE ∨ s = FINISH_STATE
48
49/-- The user's gzip header pointer: `NULL`, or a live `gz_header` record. -/
50def GzOk (h : Heap) (g : Option GzHeaderRef) : Prop :=
51  g = none ∨ ∃ i, g = some (.tab i) ∧ (h.gzheaders i).isSome
52
53/-- The four buffers of the deflate state record `d`: `window` is the writable byte block `w` of `2 * w_size` bytes,
54`pending_buf` the writable byte block `b` of `4 * lit_bufsize` bytes, `prev` and `head` are blocks of 16-bit words that
55hold `w_size` and `hash_size` entries. The four blocks are different. `pending_out` lies in `pending_buf`
56and `pending_out + pending` does not leave it. -/
57structure DBlocks (h : Heap) (d : DeflateState) (w p q b : Nat) : Prop where
58  win : d.window = .ref (.blk w) 0
59  prev : d.prev = .ref (.blk p) 0
60  head : d.head = .ref (.blk q) 0
61  pbuf : d.pending_buf = .ref (.blk b) 0
62  wa : ∃ a, h.bytes w = some a ∧ a.size = 2 * d.w_size.toNat
63  wro : h.ro w = false
64  pa : ∃ a, h.words p = some a ∧ a.size = d.w_size.toNat
65  qa : ∃ a, h.words q = some a ∧ a.size = d.hash_size.toNat
66  ba : ∃ a, h.bytes b = some a ∧ a.size = 4 * d.lit_bufsize.toNat
67  bro : h.ro b = false
68  psize : d.pending_buf_size.toNat = 4 * d.lit_bufsize.toNat
69  wb : w ≠ b
70  pq : p ≠ q
71  pout : ∃ off, d.pending_out = .ref (.blk b) off ∧ off + d.pending.toNat ≤ d.pending_buf_size.toNat
72
73/-- The representation invariant of a deflate state record `d` at block `ds`, as far as the stream functions and the
74engine need it (`deflateInit2_` establishes it).
75
76* sizes: `w_bits` is 9 to 15, `w_size = 2^w_bits`, `w_mask = w_size - 1`, `window_size = 2 * w_size`; `hash_bits` is 8 to
77  16 (`memLevel + 7`), `hash_size = 2^hash_bits`, `hash_mask = hash_size - 1`, `hash_shift = (hash_bits + 2) / 3`,
78  `lit_bufsize = hash_size / 2 = 2^(memLevel + 6)`;
79* ranges: `level` 0 to 9, `strategy` 0 to 4, `method = Z_DEFLATED`, `wrap` from `-2` to `2` (negative after the trailer);
80* `high_water <= window_size`;
81* the symbol buffer overlays `pending_buf` at `lit_bufsize`, `sym_end = 3 (lit_bufsize - 1)`, `sym_next <= sym_end`
82  and a multiple of 3;
83* the bit buffer holds `bi_valid` bits (0 to 16) and no bit above them. -/
84structure DStInv (h : Heap) (ds : Nat) (d : DeflateState) : Prop where
85  wf : d.WellFormed
86  wbits_lo : 9 ≤ d.w_bits.toNat
87  wbits_hi : d.w_bits.toNat ≤ 15
88  wsize : d.w_size.toNat = 2 ^ d.w_bits.toNat
89  wmask : d.w_mask.toNat = d.w_size.toNat - 1
90  wsz : d.window_size.toNat = 2 * d.w_size.toNat
91  hbits_lo : 8 ≤ d.hash_bits.toNat
92  hbits_hi : d.hash_bits.toNat ≤ 16
93  hsize : d.hash_size.toNat = 2 ^ d.hash_bits.toNat
94  hmask : d.hash_mask.toNat = d.hash_size.toNat - 1
95  hshift : d.hash_shift.toNat = (d.hash_bits.toNat + 2) / 3
96  lit : 2 * d.lit_bufsize.toNat = d.hash_size.toNat
97  level_lo : 0 ≤ d.level.toInt
98  level_hi : d.level.toInt ≤ 9
99  strat_lo : 0 ≤ d.strategy.toInt
100  strat_hi : d.strategy.toInt ≤ 4
101  method : d.method = 8
102  wrap_lo : -2 ≤ d.wrap.toInt
103  wrap_hi : d.wrap.toInt ≤ 2
104  hw : d.high_water.toNat ≤ d.window_size.toNat
105  blocks : ∃ w p q b, DBlocks h d w p q b
106  sym : (∃ b, d.pending_buf = .ref (.blk b) 0 ∧ d.sym_buf = .ref (.blk b) d.lit_bufsize.toNat) ∧
107    d.sym_end.toNat = 3 * (d.lit_bufsize.toNat - 1) ∧ d.sym_next.toNat ≤ d.sym_end.toNat ∧ d.sym_next.toNat % 3 = 0
108  bits : 0 ≤ d.bi_valid.toInt ∧ d.bi_valid.toInt ≤ 16 ∧ d.bi_buf.toNat < 2 ^ d.bi_valid.toInt.toNat
109  gz : GzOk h d.gzhead
110
111/-- The stream `r` is the record `z`; its state is the record `d` at block `ds`, which points back to the stream; the
112status is one `deflateStateCheck` accepts; the allocator functions are not `NULL`. -/
113structure DLive (h : Heap) (r : ZStreamRef) (ds : Nat) (z : ZStream) (d : DeflateState) : Prop where
114  hz : r.get h = some z
115  hs : h.dstates ds = some d
116  zst : z.state = some (.deflate ds)
117  back : d.strm = some r
118  status : GoodStatus d.status
119  zalloc : z.zalloc ≠ .null
120  zfree : z.zfree ≠ .null
121
122/-- The stream functions can allocate and free: the allocator functions are the default ones (the only ones the model
123has; any other makes the translation fault). -/
124def DefAlloc (z : ZStream) : Prop := z.zalloc = .fn "zcalloc" ∧ z.zfree = .fn "zcfree"
125
126/-- Everything the stream functions assume of the heap around a live deflate stream. -/
127structure DGood (h : Heap) (r : ZStreamRef) (ds : Nat) (z : ZStream) (d : DeflateState) : Prop where
128  live : DLive h r ds z d
129  inv : DStInv h ds d
130  uniq : Uniq h
131  fresh : Fresh h
132  trees : Zlib.Trees.Proofs.Out.TreesInv h ds
133
134/-- The blocks a stream owns: its state record and the four buffers. -/
135def DOwned (d : DeflateState) (ds : Nat) (x : Nat) : Prop :=
136  x = ds ∨ (∃ w, d.window = .ref (.blk w) 0 ∧ x = w) ∨ (∃ p, d.prev = .ref (.blk p) 0 ∧ x = p) ∨
137  (∃ q, d.head = .ref (.blk q) 0 ∧ x = q) ∨ (∃ b, d.pending_buf = .ref (.blk b) 0 ∧ x = b)
138
139/-- The streams `deflateStateCheck` handles: `NULL`, or a live stream record that has a `NULL` allocator function, or
140no state, or a state that is a live deflate state record. (A state that is an inflate state, a freed state or a freed
141stream is undefined behaviour in C and a fault here.) -/
142def StreamDom (h : Heap) (strm : ZStreamPtr) : Prop :=
143  strm = none ∨ ∃ r z, strm = some r ∧ r.get h = some z ∧
144    (z.zalloc = .null ∨ z.zfree = .null ∨ z.state = none ∨ ∃ ds d, z.state = some (.deflate ds) ∧ h.dstates ds = some d)
145
146/-- The stream is one `deflateStateCheck` accepts. -/
147def DInitialised (h : Heap) (strm : ZStreamPtr) : Prop := ∃ r ds z d, strm = some r ∧ DLive h r ds z d
148
149end Zlib.Deflate.Spec
150
151namespace Zlib.Deflate.Proofs
152open C Zlib.Deflate Zlib.Deflate.Spec
153
154/-! ### Updating the heap -/
155
156@[simp] theorem setD_dstates_same (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).dstates ds = some d := by
157  simp [setD]
158@[simp] theorem setD_dstates_ne (h : Heap) (ds x : Nat) (d : DeflateState) (hx : x ≠ ds) :
159    (setD h ds d).dstates x = h.dstates x := by simp [setD, upd_ne _ _ _ _ hx]
160@[simp] theorem setD_bytes (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).bytes = h.bytes := rfl
161@[simp] theorem setD_words (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).words = h.words := rfl
162@[simp] theorem setD_streams (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).streams = h.streams := rfl
163@[simp] theorem setD_gzstates (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).gzstates = h.gzstates := rfl
164@[simp] theorem setD_gzheaders (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).gzheaders = h.gzheaders := rfl
165@[simp] theorem setD_istates (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).istates = h.istates := rfl
166@[simp] theorem setD_ro (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).ro = h.ro := rfl
167@[simp] theorem setD_static (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).static = h.static := rfl
168@[simp] theorem setD_nextBlk (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).nextBlk = h.nextBlk := rfl
169@[simp] theorem setD_nalloc (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).nalloc = h.nalloc := rfl
170@[simp] theorem setD_allocOk (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).allocOk = h.allocOk := rfl
171@[simp] theorem setD_garbage (h : Heap) (ds : Nat) (d : DeflateState) : (setD h ds d).garbage = h.garbage := rfl
172@[simp] theorem setD_setD (h : Heap) (ds : Nat) (d d' : DeflateState) : setD (setD h ds d) ds d' = setD h ds d' := by
173  simp [setD, upd_upd]
174theorem setD_self {h : Heap} {ds : Nat} {d : DeflateState} (hd : h.dstates ds = some d) : setD h ds d = h := by
175  simp [setD, upd_self _ _ _ hd]
176
177theorem ZStreamRef.get_put_same {h : Heap} {r : ZStreamRef} {z : ZStream} (e : r.get h = some z) (v : ZStream) :
178    r.get (r.put h v) = some v := by
179  cases r with
180  | tab i => simp [ZStreamRef.get] at e; simp [ZStreamRef.put, ZStreamRef.get, e]
181  | in_gzstate_strm i =>
182    simp [ZStreamRef.get] at e
183    obtain ⟨g, hg, -⟩ := e
184    simp [ZStreamRef.put, ZStreamRef.get, hg]
185
186@[simp] theorem ZStreamRef.get_setD (h : Heap) (r : ZStreamRef) (ds : Nat) (d : DeflateState) :
187    r.get (setD h ds d) = r.get h := by
188  cases r <;> rfl
189
190@[simp] theorem ZStreamRef.put_dstates (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).dstates = h.dstates := by
191  cases r with
192  | tab i => simp only [ZStreamRef.put]; split <;> rfl
193  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
194
195@[simp] theorem ZStreamRef.put_bytes (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).bytes = h.bytes := by
196  cases r with
197  | tab i => simp only [ZStreamRef.put]; split <;> rfl
198  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
199
200@[simp] theorem ZStreamRef.put_ro (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).ro = h.ro := by
201  cases r with
202  | tab i => simp only [ZStreamRef.put]; split <;> rfl
203  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
204
205@[simp] theorem ZStreamRef.put_words (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).words = h.words := by
206  cases r with
207  | tab i => simp only [ZStreamRef.put]; split <;> rfl
208  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
209
210@[simp] theorem ZStreamRef.put_istates (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).istates = h.istates := by
211  cases r with
212  | tab i => simp only [ZStreamRef.put]; split <;> rfl
213  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
214
215@[simp] theorem ZStreamRef.put_gzheaders (h : Heap) (r : ZStreamRef) (v : ZStream) :
216    (r.put h v).gzheaders = h.gzheaders := by
217  cases r with
218  | tab i => simp only [ZStreamRef.put]; split <;> rfl
219  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
220
221@[simp] theorem ZStreamRef.put_nextBlk (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).nextBlk = h.nextBlk := by
222  cases r with
223  | tab i => simp only [ZStreamRef.put]; split <;> rfl
224  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
225
226@[simp] theorem ZStreamRef.put_nalloc (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).nalloc = h.nalloc := by
227  cases r with
228  | tab i => simp only [ZStreamRef.put]; split <;> rfl
229  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
230
231@[simp] theorem ZStreamRef.put_allocOk (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).allocOk = h.allocOk := by
232  cases r with
233  | tab i => simp only [ZStreamRef.put]; split <;> rfl
234  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
235
236@[simp] theorem ZStreamRef.put_garbage (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).garbage = h.garbage := by
237  cases r with
238  | tab i => simp only [ZStreamRef.put]; split <;> rfl
239  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
240
241@[simp] theorem ZStreamRef.put_static (h : Heap) (r : ZStreamRef) (v : ZStream) : (r.put h v).static = h.static := by
242  cases r with
243  | tab i => simp only [ZStreamRef.put]; split <;> rfl
244  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
245
246@[simp] theorem ZStreamRef.get_put (h : Heap) (r : ZStreamRef) (v : ZStream) :
247    r.get (r.put h v) = (r.get h).map (fun _ => v) := by
248  cases r with
249  | tab i =>
250    simp only [ZStreamRef.put, ZStreamRef.get]
251    cases hh : h.streams i <;> simp [hh]
252  | in_gzstate_strm i =>
253    simp only [ZStreamRef.put, ZStreamRef.get]
254    cases hh : h.gzstates i <;> simp [hh]
255
256@[simp] theorem ZStreamRef.put_put (h : Heap) (r : ZStreamRef) (v v' : ZStream) : r.put (r.put h v) v' = r.put h v' := by
257  cases r with
258  | tab i =>
259    simp only [ZStreamRef.put]
260    cases hh : h.streams i <;> simp [hh, upd_upd]
261  | in_gzstate_strm i =>
262    simp only [ZStreamRef.put]
263    cases hh : h.gzstates i <;> simp [hh, upd_upd]
264
265@[simp] theorem ZStreamRef.put_setD (h : Heap) (r : ZStreamRef) (ds : Nat) (d : DeflateState) (v : ZStream) :
266    r.put (setD h ds d) v = setD (r.put h v) ds d := by
267  cases r with
268  | tab i => simp only [ZStreamRef.put, setD]; cases hh : h.streams i <;> simp
269  | in_gzstate_strm i => simp only [ZStreamRef.put, setD]; cases hh : h.gzstates i <;> simp
270
271/-! ### Reading and writing the stream and the state -/
272
273theorem castD {h : Heap} {ds : Nat} : castDeflateState (some (.deflate ds)) h = .ok (some (.tab ds), h) := rfl
274
275theorem ldD_eq (h : Heap) (i : Nat) : ldDeflateState (some (.tab i)) h =
276    match h.dstates i with
277    | some v => .ok (v, h)
278    | none => .error (.ub "access through a dangling pointer (deflate_state)") := rfl
279
280theorem ldZ_eq (h : Heap) (r : ZStreamRef) : ldZStream (some r) h =
281    match r.get h with
282    | some v => .ok (v, h)
283    | none => .error (.ub "access through a dangling pointer (z_stream)") := rfl
284
285theorem rdD_eq {α : Type} (h : Heap) (i : Nat) (f : DeflateState → α) : rd (some (.tab i)) f h =
286    match h.dstates i with
287    | some v => .ok (f v, h)
288    | none => .error (.ub "access through a dangling pointer (deflate_state)") := by
289  simp only [rd, bind_app, ldD_eq]; cases h.dstates i <;> rfl
290
291theorem zrd_eq {α : Type} (h : Heap) (r : ZStreamRef) (f : ZStream → α) : zrd (some r) f h =
292    match r.get h with
293    | some v => .ok (f v, h)
294    | none => .error (.ub "access through a dangling pointer (z_stream)") := by
295  simp only [zrd, bind_app, ldZ_eq]; cases r.get h <;> rfl
296
297theorem stD_eq (h : Heap) (i : Nat) (v : DeflateState) : stDeflateState (some (.tab i)) v h =
298    match h.dstates i with
299    | some _ => .ok ((), setD h i v)
300    | none => .error (.ub "access through a dangling pointer (deflate_state)") := by
301  cases hh : h.dstates i with
302  | none => simp [stDeflateState, DeflateStateRef.get, hh]
303  | some w => simp [stDeflateState_tab hh, setD, hh]
304
305theorem wrD_eq (h : Heap) (i : Nat) (f : DeflateState → DeflateState) : wr (some (.tab i)) f h =
306    match h.dstates i with
307    | some v => .ok ((), setD h i (f v))
308    | none => .error (.ub "access through a dangling pointer (deflate_state)") := by
309  cases hh : h.dstates i with
310  | none => simp [wr, bind_app, ldD_eq, hh]
311  | some v => simp [wr, bind_app, ldD_eq, hh, stD_eq]
312
313theorem stZ_eq (h : Heap) (r : ZStreamRef) (v : ZStream) : stZStream (some r) v h =
314    match r.get h with
315    | some _ => .ok ((), r.put h v)
316    | none => .error (.ub "access through a dangling pointer (z_stream)") := by
317  have hro : r.isRo = false := by cases r <;> rfl
318  cases hh : r.get h with
319  | none => simp [stZStream, hh]
320  | some w => simp [stZStream_ok hh hro, hh]
321
322theorem zwr_eq (h : Heap) (r : ZStreamRef) (f : ZStream → ZStream) : zwr (some r) f h =
323    match r.get h with
324    | some v => .ok ((), r.put h (f v))
325    | none => .error (.ub "access through a dangling pointer (z_stream)") := by
326  cases hh : r.get h with
327  | none => simp [zwr, bind_app, ldZ_eq, hh]
328  | some v => simp [zwr, bind_app, ldZ_eq, hh, stZ_eq]
329
330/-- Evaluate a straight-line sequence of accesses to a stream and its deflate state. -/
331macro "dsimp'" "[" ts:Lean.Parser.Tactic.simpLemma,* "]" : tactic =>
332  `(tactic| simp [bind_app, pure_app, ldD_eq, ldZ_eq, rdD_eq, zrd_eq, wrD_eq, zwr_eq, stD_eq, stZ_eq, castD, $ts,*])
333
334/-! ### The stream check -/
335
336theorem hdec {a b : UInt32} : a ≤ b ∨ b < a := by
337  rcases Nat.lt_or_ge b.toNat a.toNat with h | h
338  · exact Or.inr (UInt32.lt_iff_toNat_lt.mpr h)
339  · exact Or.inl (UInt32.le_iff_toNat_le.mpr h)
340
341theorem stateCheck_live {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
342    (hL : DLive h r ds z d) : deflateStateCheck (some r) h = .ok (0, h) := by
343  obtain ⟨hz, hs, zst, back, st, za, zf⟩ := hL
344  have e1 : ldZStream (some r) h = .ok (z, h) := ldZStream_ok hz
345  unfold deflateStateCheck
346  rcases st with hh | hh | hh | hh | hh | hh | hh | hh <;>
347    simp [bind_app, e1, za, zf, zst, castDeflateState_ok, ldDeflateState_tab hs, back, hh]
348
349
350theorem ZStreamRef.put_self {h : Heap} {r : ZStreamRef} {z : ZStream} (e : r.get h = some z) : r.put h z = h := by
351  cases r with
352  | tab i =>
353    simp only [ZStreamRef.get] at e
354    simp [ZStreamRef.put, e, upd_self _ _ _ e]
355  | in_gzstate_strm i =>
356    simp only [ZStreamRef.get] at e
357    obtain ⟨g, hg, rfl⟩ := Option.map_eq_some_iff.mp e
358    simp [ZStreamRef.put, hg, upd_self _ _ _ hg]
359
360/-! ### Which objects exist: the shape of a heap -/
361
362/-- The two heaps hold an object in the same tables at the same block numbers (the objects may differ). -/
363def Shape (h h' : Heap) : Prop := ∀ b, (h'.bytes b).isSome = (h.bytes b).isSome ∧ (h'.words b).isSome = (h.words b).isSome ∧
364  (h'.streams b).isSome = (h.streams b).isSome ∧ (h'.gzheaders b).isSome = (h.gzheaders b).isSome ∧
365  (h'.dstates b).isSome = (h.dstates b).isSome ∧ (h'.istates b).isSome = (h.istates b).isSome ∧
366  (h'.gzstates b).isSome = (h.gzstates b).isSome
367
368theorem _root_.Zlib.Deflate.Proofs.Shape.refl (h : Heap) : Shape h h := fun _ => ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
369
370theorem _root_.Zlib.Deflate.Proofs.Shape.trans {h1 h2 h3 : Heap} (a : Shape h1 h2) (b : Shape h2 h3) : Shape h1 h3 := by
371  intro x
372  obtain ⟨a1, a2, a3, a4, a5, a6, a7⟩ := a x
373  obtain ⟨b1, b2, b3, b4, b5, b6, b7⟩ := b x
374  exact ⟨b1.trans a1, b2.trans a2, b3.trans a3, b4.trans a4, b5.trans a5, b6.trans a6, b7.trans a7⟩
375
376theorem _root_.Zlib.Deflate.Proofs.Shape.uniq {h h' : Heap} (hS : Shape h h') (hU : Uniq h) : Uniq h' := by
377  intro b
378  obtain ⟨e1, e2, e3, e4, e5, e6, e7⟩ := hS b
379  have := hU b
380  simp only [cnt, e1, e2, e3, e4, e5, e6, e7] at this ⊢
381  exact this
382
383theorem _root_.Zlib.Deflate.Proofs.Shape.live {h h' : Heap} (hS : Shape h h') (b : Nat) : h'.live b ↔ h.live b := by
384  obtain ⟨e1, e2, e3, e4, e5, e6, e7⟩ := hS b
385  simp only [Heap.live, ← Option.isSome_iff_ne_none, e1, e2, e3, e4, e5, e6, e7]
386
387theorem _root_.Zlib.Deflate.Proofs.Shape.fresh {h h' : Heap} (hS : Shape h h') (hn : h'.nextBlk = h.nextBlk) (hF : Fresh h) : Fresh h' := by
388  intro b hb hl
389  exact hF b (by omega) ((hS.live b).1 hl)
390
391theorem _root_.Zlib.Deflate.Proofs.Shape.owns {h h' : Heap} (hS : Shape h h') {S : Nat → Prop} (hO : h.Owns S) : h'.Owns S :=
392  fun b => (hS.live b).trans (hO b)
393
394theorem shape_setD {h : Heap} {ds : Nat} {d0 : DeflateState} (e : h.dstates ds = some d0) (d : DeflateState) :
395    Shape h (setD h ds d) := by
396  intro b
397  by_cases hb : b = ds
398  · subst hb; simp [setD, e]
399  · simp [setD, upd_ne _ _ _ _ hb]
400
401theorem shape_put {h : Heap} {r : ZStreamRef} {z0 : ZStream} (e : r.get h = some z0) (v : ZStream) :
402    Shape h (r.put h v) := by
403  cases r with
404  | tab i =>
405    simp only [ZStreamRef.get] at e
406    intro b
407    by_cases hb : b = i
408    · subst hb; simp [ZStreamRef.put, e]
409    · simp [ZStreamRef.put, e, upd_ne _ _ _ _ hb]
410  | in_gzstate_strm i =>
411    simp only [ZStreamRef.get] at e
412    obtain ⟨g, hg, -⟩ := Option.map_eq_some_iff.mp e
413    intro b
414    by_cases hb : b = i
415    · subst hb; simp [ZStreamRef.put, hg]
416    · simp [ZStreamRef.put, hg, upd_ne _ _ _ _ hb]
417
418theorem shape_setB {h : Heap} {w : Nat} {a0 : Array UInt8} (e : h.bytes w = some a0) (a : Array UInt8) :
419    Shape h { h with bytes := upd h.bytes w (some a) } := by
420  intro b
421  by_cases hb : b = w
422  · subst hb; simp [e]
423  · simp [upd_ne _ _ _ _ hb]
424
425theorem shape_setW {h : Heap} {w : Nat} {a0 : Array UInt16} (e : h.words w = some a0) (a : Array UInt16) :
426    Shape h { h with words := upd h.words w (some a) } := by
427  intro b
428  by_cases hb : b = w
429  · subst hb; simp [e]
430  · simp [upd_ne _ _ _ _ hb]
431
432/-! ### Uniqueness -/
433
434theorem _root_.Zlib.Deflate.Spec.Uniq.bytes_only {h : Heap} (hU : Uniq h) {b : Nat} {a : Array UInt8} (hb : h.bytes b = some a) :
435    h.words b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.dstates b = none ∧ h.istates b = none ∧
436    h.gzstates b = none := by
437  have := hU b
438  simp only [hb, cnt_some] at this
439  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
440  · cases hx : h.words b with
441    | none => rfl
442    | some _ => simp only [hx, cnt_some] at this <;> omega
443  · cases hx : h.streams b with
444    | none => rfl
445    | some _ => simp only [hx, cnt_some] at this <;> omega
446  · cases hx : h.gzheaders b with
447    | none => rfl
448    | some _ => simp only [hx, cnt_some] at this <;> omega
449  · cases hx : h.dstates b with
450    | none => rfl
451    | some _ => simp only [hx, cnt_some] at this <;> omega
452  · cases hx : h.istates b with
453    | none => rfl
454    | some _ => simp only [hx, cnt_some] at this <;> omega
455  · cases hx : h.gzstates b with
456    | none => rfl
457    | some _ => simp only [hx, cnt_some] at this <;> omega
458
459theorem _root_.Zlib.Deflate.Spec.Uniq.words_only {h : Heap} (hU : Uniq h) {b : Nat} {a : Array UInt16} (hb : h.words b = some a) :
460    h.bytes b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.dstates b = none ∧ h.istates b = none ∧
461    h.gzstates b = none := by
462  have := hU b
463  simp only [hb, cnt_some] at this
464  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
465  · cases hx : h.bytes b with
466    | none => rfl
467    | some _ => simp only [hx, cnt_some] at this <;> omega
468  · cases hx : h.streams b with
469    | none => rfl
470    | some _ => simp only [hx, cnt_some] at this <;> omega
471  · cases hx : h.gzheaders b with
472    | none => rfl
473    | some _ => simp only [hx, cnt_some] at this <;> omega
474  · cases hx : h.dstates b with
475    | none => rfl
476    | some _ => simp only [hx, cnt_some] at this <;> omega
477  · cases hx : h.istates b with
478    | none => rfl
479    | some _ => simp only [hx, cnt_some] at this <;> omega
480  · cases hx : h.gzstates b with
481    | none => rfl
482    | some _ => simp only [hx, cnt_some] at this <;> omega
483
484theorem _root_.Zlib.Deflate.Spec.Uniq.dstates_only {h : Heap} (hU : Uniq h) {b : Nat} {a : DeflateState} (hb : h.dstates b = some a) :
485    h.bytes b = none ∧ h.words b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.istates b = none ∧
486    h.gzstates b = none := by
487  have := hU b
488  simp only [hb, cnt_some] at this
489  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
490  · cases hx : h.bytes b with
491    | none => rfl
492    | some _ => simp only [hx, cnt_some] at this <;> omega
493  · cases hx : h.words b with
494    | none => rfl
495    | some _ => simp only [hx, cnt_some] at this <;> omega
496  · cases hx : h.streams b with
497    | none => rfl
498    | some _ => simp only [hx, cnt_some] at this <;> omega
499  · cases hx : h.gzheaders b with
500    | none => rfl
501    | some _ => simp only [hx, cnt_some] at this <;> omega
502  · cases hx : h.istates b with
503    | none => rfl
504    | some _ => simp only [hx, cnt_some] at this <;> omega
505  · cases hx : h.gzstates b with
506    | none => rfl
507    | some _ => simp only [hx, cnt_some] at this <;> omega
508
509/-! ### Preserving the invariants -/
510
511theorem _root_.Zlib.Deflate.Spec.DBlocks.congr {h h' : Heap} {d : DeflateState} {w p q b : Nat} (hb : h'.bytes = h.bytes)
512    (hw : h'.words = h.words) (hr : h'.ro = h.ro) (hB : DBlocks h d w p q b) : DBlocks h' d w p q b := by
513  obtain ⟨a1, a2, a3, a4, ⟨x1, y1, z1⟩, r1, ⟨x2, y2, z2⟩, ⟨x3, y3, z3⟩, ⟨x4, y4, z4⟩, r4, ps, wb, pq, po⟩ := hB
514  exact ⟨a1, a2, a3, a4, ⟨x1, by rw [hb]; exact y1, z1⟩, by rw [hr]; exact r1, ⟨x2, by rw [hw]; exact y2, z2⟩,
515    ⟨x3, by rw [hw]; exact y3, z3⟩, ⟨x4, by rw [hb]; exact y4, z4⟩, by rw [hr]; exact r4, ps, wb, pq, po⟩
516
517theorem _root_.Zlib.Deflate.Spec.DStInv.congr {h h' : Heap} {ds : Nat} {d : DeflateState} (hb : h'.bytes = h.bytes) (hw : h'.words = h.words)
518    (hr : h'.ro = h.ro) (hg : h'.gzheaders = h.gzheaders) (hI : DStInv h ds d) : DStInv h' ds d := by
519  obtain ⟨wf, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, ⟨w, p, q, b, hB⟩, sy, bi, gz⟩ := hI
520  refine ⟨wf, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19,
521    ⟨w, p, q, b, hB.congr hb hw hr⟩, sy, bi, ?_⟩
522  rcases gz with g | ⟨i, g, e⟩
523  · exact Or.inl g
524  · exact Or.inr ⟨i, g, by rw [hg]; exact e⟩
525
526theorem _root_.Zlib.Deflate.Spec.DBlocks.keys {h : Heap} {d d' : DeflateState} {w p q b : Nat}
527    (hB : DBlocks h d w p q b) (e1 : d'.window = d.window) (e2 : d'.prev = d.prev) (e3 : d'.head = d.head)
528    (e4 : d'.pending_buf = d.pending_buf) (e5 : d'.w_size = d.w_size) (e6 : d'.hash_size = d.hash_size)
529    (e7 : d'.lit_bufsize = d.lit_bufsize) (e8 : d'.pending_buf_size = d.pending_buf_size)
530    (e9 : d'.pending_out = d.pending_out) (e10 : d'.pending = d.pending) : DBlocks h d' w p q b := by
531  obtain ⟨a1, a2, a3, a4, ⟨x1, y1, z1⟩, r1, ⟨x2, y2, z2⟩, ⟨x3, y3, z3⟩, ⟨x4, y4, z4⟩, r4, ps, wb, pq, ⟨off, po, pl⟩⟩ := hB
532  refine ⟨by rw [e1]; exact a1, by rw [e2]; exact a2, by rw [e3]; exact a3, by rw [e4]; exact a4,
533    ⟨x1, y1, by rw [e5]; exact z1⟩, r1, ⟨x2, y2, by rw [e5]; exact z2⟩, ⟨x3, y3, by rw [e6]; exact z3⟩,
534    ⟨x4, y4, by rw [e7]; exact z4⟩, r4, by rw [e8, e7]; exact ps, wb, pq, ⟨off, by rw [e9]; exact po, by rw [e10, e8]; exact pl⟩⟩
535
536/-- The blocks of the state stay the same when the record changes only in fields other than the ten `DBlocks` reads
537(each equality is `rfl` for a record update that leaves them alone). -/
538theorem _root_.Zlib.Deflate.Spec.DStInv.blocks_keys {h : Heap} {ds : Nat} {d d' : DeflateState} (hI : DStInv h ds d)
539    (e1 : d'.window = d.window) (e2 : d'.prev = d.prev) (e3 : d'.head = d.head)
540    (e4 : d'.pending_buf = d.pending_buf) (e5 : d'.w_size = d.w_size) (e6 : d'.hash_size = d.hash_size)
541    (e7 : d'.lit_bufsize = d.lit_bufsize) (e8 : d'.pending_buf_size = d.pending_buf_size)
542    (e9 : d'.pending_out = d.pending_out) (e10 : d'.pending = d.pending) : ∃ w p q b, DBlocks h d' w p q b := by
543  obtain ⟨w, p, q, b, hB⟩ := hI.blocks
544  exact ⟨w, p, q, b, hB.keys e1 e2 e3 e4 e5 e6 e7 e8 e9 e10⟩
545
546/-- The fields of a state record that `trees.c` relies on are unchanged: the buffers and the symbol buffer, the three tree
547descriptors, the bit buffer and the symbol count. -/
548def TrKeep (d d' : DeflateState) : Prop :=
549  d'.pending_buf = d.pending_buf ∧ d'.pending_buf_size = d.pending_buf_size ∧ d'.sym_buf = d.sym_buf ∧
550  d'.lit_bufsize = d.lit_bufsize ∧ d'.sym_end = d.sym_end ∧ d'.l_desc = d.l_desc ∧ d'.d_desc = d.d_desc ∧
551  d'.bl_desc = d.bl_desc ∧ d'.bi_valid = d.bi_valid ∧ d'.bi_buf = d.bi_buf ∧ d'.sym_next = d.sym_next
552
553/-- Prove `TrKeep d d'` when `d'` is a record update of `d` that leaves those fields alone. -/
554macro "trkeep" : tactic => `(tactic| exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩)
555
556/-- The invariant of `trees.c` survives a change of the state record that keeps the fields of `TrKeep` (and the sizes of
557its arrays), on a heap with the same byte blocks, read-only flags and static tables. -/
558theorem TreesInv.keep {h h' : Heap} {id : Nat} {d d' : DeflateState} (hT : Zlib.Trees.Proofs.Out.TreesInv h id)
559    (hd : h.dstates id = some d) (hb : h'.bytes = h.bytes) (hr : h'.ro = h.ro) (hs : h'.static = h.static)
560    (hd' : h'.dstates id = some d') (hw : d'.WellFormed) (hk : TrKeep d d')
561    (hp : d'.pending.toNat ≤ d'.pending_buf_size.toNat) : Zlib.Trees.Proofs.Out.TreesInv h' id := by
562  obtain ⟨d0, b, buf, hB, hR⟩ := hT
563  have e : d0 = d := Option.some.inj (hB.dstate.symm.trans hd)
564  subst e
565  obtain ⟨k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11⟩ := hk
566  refine ⟨d', b, buf, ⟨hd', hw, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, hp⟩, ?_⟩
567  · rw [hs]; exact hB.static
568  · rw [k1]; exact hB.pbuf
569  · rw [hb]; exact hB.bytes
570  · rw [hr]; exact hB.rw
571  · rw [k4]; exact hB.size
572  · rw [k2]; exact hB.psize
573  · rw [k3, k4]; exact hB.sym
574  · rw [k4]; exact hB.lit_lo
575  · rw [k4]; exact hB.lit_hi
576  · rw [k5, k4]; exact hB.sym_end
577  · refine ⟨by rw [k6]; exact hR.ldyn, by rw [k6]; exact hR.lstat, by rw [k7]; exact hR.ddyn, by rw [k7]; exact hR.dstat,
578      by rw [k8]; exact hR.bldyn, by rw [k8]; exact hR.blstat, by rw [k9]; exact hR.bi_lo, by rw [k9]; exact hR.bi_hi,
579      by rw [k10, k9]; exact hR.bi_buf, by rw [k11, k5]; exact hR.sym_next_le, by rw [k11]; exact hR.sym_next_mod⟩
580
581/-- Replacing a block of words keeps the invariant of `trees.c` (it mentions only byte blocks). -/
582theorem TreesInv.words_set {h : Heap} {id : Nat} (hT : Zlib.Trees.Proofs.Out.TreesInv h id) (x : Nat) (a : Array UInt16) :
583    Zlib.Trees.Proofs.Out.TreesInv { h with words := upd h.words x (some a) } id := by
584  obtain ⟨d, b, buf, hB, hR⟩ := hT
585  exact ⟨d, b, buf, ⟨hB.dstate, hB.wf, hB.static, hB.pbuf, hB.bytes, hB.rw, hB.size, hB.psize, hB.sym, hB.lit_lo,
586    hB.lit_hi, hB.sym_end, hB.pending_le⟩, hR⟩
587
588/-- Replacing a byte block by an array of the same size keeps the invariant of `trees.c`: if it is the block of
589`pending_buf` the content changes, which the invariant allows. -/
590theorem TreesInv.bytes_set {h : Heap} {id : Nat} (hT : Zlib.Trees.Proofs.Out.TreesInv h id) (x : Nat) (a a0 : Array UInt8)
591    (hx : h.bytes x = some a0) (hsz : a.size = a0.size) :
592    Zlib.Trees.Proofs.Out.TreesInv { h with bytes := upd h.bytes x (some a) } id := by
593  obtain ⟨d, b, buf, hB, hR⟩ := hT
594  by_cases hxb : x = b
595  · subst hxb
596    have : buf = a0 := Option.some.inj (hB.bytes.symm.trans hx)
597    subst this
598    exact ⟨d, x, a, ⟨hB.dstate, hB.wf, hB.static, hB.pbuf, by simp, hB.rw, by rw [hsz]; exact hB.size,
599      by rw [hsz]; exact hB.psize, hB.sym, hB.lit_lo, hB.lit_hi, hB.sym_end, hB.pending_le⟩, hR⟩
600  · exact ⟨d, b, buf, ⟨hB.dstate, hB.wf, hB.static, hB.pbuf, by simp [upd_apply, Ne.symm hxb, hB.bytes], hB.rw, hB.size,
601      hB.psize, hB.sym, hB.lit_lo, hB.lit_hi, hB.sym_end, hB.pending_le⟩, hR⟩
602
603theorem _root_.Zlib.Deflate.Spec.DStInv.pending_le {h : Heap} {ds : Nat} {d : DeflateState} (hI : DStInv h ds d) :
604    d.pending.toNat ≤ d.pending_buf_size.toNat := by
605  obtain ⟨w, p, q, b, hB⟩ := hI.blocks
606  obtain ⟨off, -, hpl⟩ := hB.pout
607  omega
608
609/-- Rewrite the stream record and the state record of a live stream, keeping the state pointer, the back pointer and
610the status; the new state record satisfies the invariant and keeps the fields `trees.c` relies on (`TrKeep`). -/
611theorem _root_.Zlib.Deflate.Spec.DGood.setZD {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
612    (hG : DGood h r ds z d) {z' : ZStream} {d' : DeflateState}
613    (hz : z'.state = z.state) (hza : z'.zalloc ≠ .null) (hzf : z'.zfree ≠ .null) (hback : d'.strm = d.strm)
614    (hst : GoodStatus d'.status) (hI : DStInv h ds d') (hk : TrKeep d d') :
615    DGood (setD (r.put h z') ds d') r ds z' d' := by
616  have hS : Shape h (setD (r.put h z') ds d') :=
617    (shape_put hG.live.hz z').trans (shape_setD (by simpa using hG.live.hs) d')
618  have hT : Zlib.Trees.Proofs.Out.TreesInv (setD (r.put h z') ds d') ds :=
619    TreesInv.keep (d := d) (d' := d') (h := h) hG.trees hG.live.hs (by simp) (by simp) (by simp) (by simp) hI.wf hk
620      hI.pending_le
621  refine ⟨⟨?_, by simp, hz.trans hG.live.zst, hback.trans hG.live.back, hst, hza, hzf⟩,
622    DStInv.congr (h := h) (h' := setD (r.put h z') ds d') (by simp) (by simp) (by simp) (by simp) hI,
623    hS.uniq hG.uniq, hS.fresh (by simp) hG.fresh, hT⟩
624  simp [ZStreamRef.get_put, hG.live.hz]
625
626/-- The same for a change of the state record only. -/
627theorem _root_.Zlib.Deflate.Spec.DGood.setD' {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
628    (hG : DGood h r ds z d) {d' : DeflateState} (hback : d'.strm = d.strm) (hst : GoodStatus d'.status)
629    (hI : DStInv h ds d') (hk : TrKeep d d') : DGood (setD h ds d') r ds z d' := by
630  have e : r.put h z = h := ZStreamRef.put_self hG.live.hz
631  have := hG.setZD (z' := z) (d' := d') rfl hG.live.zalloc hG.live.zfree hback hst hI hk
632  rw [e] at this
633  exact this
634
635/-- Replacing a block of words by an array of the same size keeps the four buffers. -/
636theorem _root_.Zlib.Deflate.Spec.DBlocks.words_set {h : Heap} {d : DeflateState} {w p q b : Nat}
637    (hB : DBlocks h d w p q b) (x : Nat) (a : Array UInt16) (a0 : Array UInt16) (hx : h.words x = some a0)
638    (hsz : a.size = a0.size) : DBlocks { h with words := upd h.words x (some a) } d w p q b := by
639  obtain ⟨a1, a2, a3, a4, wa, r1, ⟨pa, hpa, pz⟩, ⟨qa, hqa, qz⟩, ba, r4, ps, wb, pq, po⟩ := hB
640  refine ⟨a1, a2, a3, a4, wa, r1, ?_, ?_, ba, r4, ps, wb, pq, po⟩
641  · by_cases hxp : x = p
642    · subst hxp
643      have : pa = a0 := Option.some.inj (hpa.symm.trans hx)
644      subst this
645      exact ⟨a, by simp, by omega⟩
646    · exact ⟨pa, by simp [upd_apply, Ne.symm hxp, hpa], pz⟩
647  · by_cases hxq : x = q
648    · subst hxq
649      have : qa = a0 := Option.some.inj (hqa.symm.trans hx)
650      subst this
651      exact ⟨a, by simp, by omega⟩
652    · exact ⟨qa, by simp [upd_apply, Ne.symm hxq, hqa], qz⟩
653
654/-- Replacing a byte block by an array of the same size keeps the four buffers. -/
655theorem _root_.Zlib.Deflate.Spec.DBlocks.bytes_set {h : Heap} {d : DeflateState} {w p q b : Nat}
656    (hB : DBlocks h d w p q b) (x : Nat) (a : Array UInt8) (a0 : Array UInt8) (hx : h.bytes x = some a0)
657    (hsz : a.size = a0.size) : DBlocks { h with bytes := upd h.bytes x (some a) } d w p q b := by
658  obtain ⟨a1, a2, a3, a4, ⟨wa, hwa, wz⟩, r1, pa, qa, ⟨ba, hba, bz⟩, r4, ps, wb, pq, po⟩ := hB
659  refine ⟨a1, a2, a3, a4, ?_, r1, pa, qa, ?_, r4, ps, wb, pq, po⟩
660  · by_cases hxw : x = w
661    · subst hxw
662      have : wa = a0 := Option.some.inj (hwa.symm.trans hx)
663      subst this
664      exact ⟨a, by simp, by omega⟩
665    · exact ⟨wa, by simp [upd_apply, Ne.symm hxw, hwa], wz⟩
666  · by_cases hxb : x = b
667    · subst hxb
668      have : ba = a0 := Option.some.inj (hba.symm.trans hx)
669      subst this
670      exact ⟨a, by simp, by omega⟩
671    · exact ⟨ba, by simp [upd_apply, Ne.symm hxb, hba], bz⟩
672
673theorem _root_.Zlib.Deflate.Spec.DStInv.words_set {h : Heap} {ds : Nat} {d : DeflateState} (hI : DStInv h ds d)
674    (x : Nat) (a a0 : Array UInt16) (hx : h.words x = some a0) (hsz : a.size = a0.size) :
675    DStInv { h with words := upd h.words x (some a) } ds d := by
676  obtain ⟨w, p, q, b, hB⟩ := hI.blocks
677  exact { hI with blocks := ⟨w, p, q, b, hB.words_set x a a0 hx hsz⟩ }
678
679theorem _root_.Zlib.Deflate.Spec.DStInv.bytes_set {h : Heap} {ds : Nat} {d : DeflateState} (hI : DStInv h ds d)
680    (x : Nat) (a a0 : Array UInt8) (hx : h.bytes x = some a0) (hsz : a.size = a0.size)
681    (hro : ∀ y, y = x → h.ro y = h.ro y) :
682    DStInv { h with bytes := upd h.bytes x (some a) } ds d := by
683  obtain ⟨w, p, q, b, hB⟩ := hI.blocks
684  exact { hI with blocks := ⟨w, p, q, b, hB.bytes_set x a a0 hx hsz⟩ }
685
686/-- Replacing a block of words of a good heap by an array of the same size keeps it good. -/
687theorem _root_.Zlib.Deflate.Spec.DGood.words_set {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
688    (hG : DGood h r ds z d) (x : Nat) (a a0 : Array UInt16) (hx : h.words x = some a0) (hsz : a.size = a0.size) :
689    DGood { h with words := upd h.words x (some a) } r ds z d := by
690  have hS := shape_setW hx a
691  refine ⟨⟨?_, ?_, hG.live.zst, hG.live.back, hG.live.status, hG.live.zalloc, hG.live.zfree⟩, hG.inv.words_set x a a0 hx hsz,
692    hS.uniq hG.uniq, hS.fresh rfl hG.fresh, TreesInv.words_set hG.trees x a⟩
693  · cases r <;> simpa [ZStreamRef.get] using hG.live.hz
694  · exact hG.live.hs
695
696/-- Replacing a byte block of a good heap by an array of the same size keeps it good. -/
697theorem _root_.Zlib.Deflate.Spec.DGood.bytes_set {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
698    (hG : DGood h r ds z d) (x : Nat) (a a0 : Array UInt8) (hx : h.bytes x = some a0) (hsz : a.size = a0.size) :
699    DGood { h with bytes := upd h.bytes x (some a) } r ds z d := by
700  have hS := shape_setB hx a
701  refine ⟨⟨?_, ?_, hG.live.zst, hG.live.back, hG.live.status, hG.live.zalloc, hG.live.zfree⟩,
702    hG.inv.bytes_set x a a0 hx hsz (fun _ _ => rfl), hS.uniq hG.uniq, hS.fresh rfl hG.fresh, TreesInv.bytes_set hG.trees x a a0 hx hsz⟩
703  · cases r <;> simpa [ZStreamRef.get] using hG.live.hz
704  · exact hG.live.hs
705
706/-- The owned blocks are live. -/
707theorem _root_.Zlib.Deflate.Spec.DOwned.live {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
708    (hG : DGood h r ds z d) {x : Nat} (hx : DOwned d ds x) : h.live x := by
709  obtain ⟨w, p, q, b, hB⟩ := hG.inv.blocks
710  rcases hx with rfl | ⟨w', hw, rfl⟩ | ⟨p', hp, rfl⟩ | ⟨q', hq, rfl⟩ | ⟨b', hb, rfl⟩
711  · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (by simp [hG.live.hs])))))
712  · rw [hB.win] at hw; cases hw
713    obtain ⟨a, ha, -⟩ := hB.wa
714    exact Or.inl (by simp [ha])
715  · rw [hB.prev] at hp; cases hp
716    obtain ⟨a, ha, -⟩ := hB.pa
717    exact Or.inr (Or.inl (by simp [ha]))
718  · rw [hB.head] at hq; cases hq
719    obtain ⟨a, ha, -⟩ := hB.qa
720    exact Or.inr (Or.inl (by simp [ha]))
721  · rw [hB.pbuf] at hb; cases hb
722    obtain ⟨a, ha, -⟩ := hB.ba
723    exact Or.inl (by simp [ha])
724
725
726/-- **deflateStateCheck, safety and specification.** On every stream of the domain `StreamDom` (`NULL`, or a live stream
727whose state pointer is `NULL`, a deflate state, or irrelevant because an allocator function is `NULL`) the check
728returns without a fault and without changing the heap; it returns 0 exactly for an initialised stream (the stream and
729its state point to each other, the allocator functions are not `NULL`, and the status is one of the eight values)
730and 1 otherwise. -/
731theorem deflateStateCheck_total {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) :
732    ∃ v, deflateStateCheck strm h = .ok (v, h) ∧ (v = 0 ∧ DInitialised h strm ∨ v = 1 ∧ ¬ DInitialised h strm) := by
733  rcases hD with rfl | ⟨r, z, rfl, hr, hcase⟩
734  · refine ⟨1, by simp [deflateStateCheck], Or.inr ⟨rfl, ?_⟩⟩
735    rintro ⟨r, ds, z, d, hh, -⟩; cases hh
736  · have e1 : ldZStream (some r) h = .ok (z, h) := ldZStream_ok hr
737    by_cases hza : z.zalloc = .null
738    · refine ⟨1, by simp [deflateStateCheck, e1, hza], Or.inr ⟨rfl, ?_⟩⟩
739      rintro ⟨r', ds, z', d, hh, hL⟩
740      cases hh; exact hL.zalloc (by rw [hL.hz] at hr; cases hr; exact hza)
741    by_cases hzf : z.zfree = .null
742    · refine ⟨1, by simp [deflateStateCheck, e1, hza, hzf], Or.inr ⟨rfl, ?_⟩⟩
743      rintro ⟨r', ds, z', d, hh, hL⟩
744      cases hh; exact hL.zfree (by rw [hL.hz] at hr; cases hr; exact hzf)
745    rcases hcase with h1 | h1 | h1 | ⟨ds, d, hzs, hst⟩
746    · exact absurd h1 hza
747    · exact absurd h1 hzf
748    · refine ⟨1, by simp [deflateStateCheck, e1, hza, hzf, h1, castDeflateState], Or.inr ⟨rfl, ?_⟩⟩
749      rintro ⟨r', ds, z', d, hh, hL⟩
750      cases hh; rw [hL.hz] at hr; cases hr; rw [hL.zst] at h1; cases h1
751    · by_cases c1 : d.strm = some r
752      · by_cases c2 : GoodStatus d.status
753        · have hL : DLive h r ds z d := ⟨hr, hst, hzs, c1, c2, hza, hzf⟩
754          exact ⟨0, stateCheck_live hL, Or.inl ⟨rfl, r, ds, z, d, rfl, hL⟩⟩
755        · refine ⟨1, ?_, Or.inr ⟨rfl, ?_⟩⟩
756          · simp only [GoodStatus, not_or] at c2
757            simp [deflateStateCheck, bind_app, e1, castD, ldD_eq, hza, hzf, hzs, hst, c1, c2]
758          · rintro ⟨r', ds', z', d', hh, hL⟩
759            cases hh
760            rw [hL.hz] at hr; cases hr
761            rw [hL.zst] at hzs; cases hzs
762            rw [hL.hs] at hst; cases hst
763            exact c2 hL.status
764      · refine ⟨1, ?_, Or.inr ⟨rfl, ?_⟩⟩
765        · simp [deflateStateCheck, bind_app, e1, castD, ldD_eq, hza, hzf, hzs, hst, c1]
766        · rintro ⟨r', ds', z', d', hh, hL⟩
767          cases hh
768          rw [hL.hz] at hr; cases hr
769          rw [hL.zst] at hzs; cases hzs
770          rw [hL.hs] at hst; cases hst
771          exact c1 hL.back
772
773/-- The state check fails: a function that starts with it returns `Z_STREAM_ERROR` and changes nothing. -/
774theorem notInit_check {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm) :
775    deflateStateCheck strm h = .ok (1, h) := by
776  obtain ⟨v, hv, hc⟩ := deflateStateCheck_total hD
777  rcases hc with ⟨rfl, hI⟩ | ⟨rfl, -⟩
778  · exact absurd hI hN
779  · exact hv
780
781/-! ### The stream check refuses -/
782
783/-- A function of the shape `if deflateStateCheck strm ≠ 0 then return X; rest` returns `X` and changes nothing when
784the check refuses the stream. -/
785theorem check_refuse {α : Type} {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
786    (X : α) (rest : M α) :
787    (do if (← deflateStateCheck strm) != 0 then return X
788        rest : M α) h = .ok (X, h) := by
789  simp [bind_app, notInit_check hD hN]
790
791end Zlib.Deflate.Proofs