deflate.c.life.bound.lean

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

1import ZlibF.Proof.«deflate.c.base»
2
3/-!
4# deflate.c: `deflateBound_z` and `deflateBound`
5
6The bound is a closed formula of `w_bits`, `hash_bits`, `level`, the length of the wrapper and the source length. The
7wrapper length depends on the state: 0 for a raw stream, 6 or 10 for a zlib stream (10 once a dictionary was loaded:
8`strstart` is not 0), 18 plus the lengths of the user's header parts for a gzip stream.
9-/
10
11namespace Zlib.Deflate.Spec
12open C
13
14/-- `fixedlen` of `deflateBound_z`: an upper bound for the fixed-code deflate size (wraps to the maximum). -/
15def fixedLen (n : UInt64) : UInt64 :=
16  if n + (n >>> 3) + (n >>> 8) + (n >>> 9) + 4 < n then 0xffffffffffffffff else n + (n >>> 3) + (n >>> 8) + (n >>> 9) + 4
17
18/-- `storelen` of `deflateBound_z`: an upper bound for the stored-block size. -/
19def storeLen (n : UInt64) : UInt64 :=
20  if n + (n >>> 5) + (n >>> 7) + (n >>> 11) + 7 < n then 0xffffffffffffffff else n + (n >>> 5) + (n >>> 7) + (n >>> 11) + 7
21
22/-- The bound for a stream with no usable state (the check refuses it): the larger of the two plus 18. -/
23def boundNoStateP (fx st : UInt64) : UInt64 :=
24  let bound := if fx > st then fx else st
25  if bound + 18 < bound then 0xffffffffffffffff else bound + 18
26
27def boundNoState (n : UInt64) : UInt64 := boundNoStateP (fixedLen n) (storeLen n)
28
29/-- The bound of a valid stream with the window bits, the hash bits, the level and the wrapper length `wl`, from the
30values `fx` (`fixedlen`) and `st` (`storelen`). -/
31def boundTailP (w_bits hash_bits : UInt32) (level : Int32) (wl : UInt64) (fx st n : UInt64) : UInt64 :=
32  if w_bits != 15 || hash_bits != 15 then
33    let bound := if w_bits ≤ hash_bits && level != 0 then fx else st
34    if bound + wl < bound then 0xffffffffffffffff else bound + wl
35  else
36    let bound := n + (n >>> 12) + (n >>> 14) + (n >>> 25) + 13 - 6 + wl
37    if bound < n then 0xffffffffffffffff else bound
38
39def boundTail (w_bits hash_bits : UInt32) (level : Int32) (wl : UInt64) (n : UInt64) : UInt64 :=
40  boundTailP w_bits hash_bits level wl (fixedLen n) (storeLen n) n
41
42/-- The NUL-terminated string of length `len` starts at the pointer `p`: the bytes `p[0 .. len)` are not 0, `p[len]`
43is 0, all inside one live array (a heap block or a string literal). The length is below `2^64`, the loop fuel of the
44model (an array of `2^64` elements does not exist; Lean cannot prove it). -/
45def GzStr (h : Heap) (p : BPtr) (len : Nat) : Prop :=
46  ∃ r off a, p = .ref r off ∧ Space.get h r = some a ∧ off + len < a.size ∧ a[off + len]? = some 0 ∧
47    (∀ i, i < len → a[off + i]? ≠ some 0) ∧ len < 2 ^ 64
48
49/-- `p` is `NULL` or the start of a NUL-terminated string. -/
50def StrOk (h : Heap) (p : BPtr) : Prop := p = .null ∨ ∃ len, GzStr h p len
51
52/-- The number of bytes `deflate` writes for the string at `p`: 0 for `NULL`, else its length and the terminating zero. -/
53def StrPart (h : Heap) (p : BPtr) (k : UInt64) : Prop :=
54  (p = .null ∧ k = 0) ∨ ∃ len, GzStr h p len ∧ k = UInt64.ofNat (len + 1)
55
56/-- `wl` is the length of the wrapper of the state record `d`: raw 0; zlib 6, plus 4 when `strstart` is not 0; gzip 18,
57plus the parts of the user's header when there is one: the extra field (two length bytes and the field), the name, the
58comment and the header CRC (two bytes). The wrapper is read from the absolute value of `wrap`. -/
59def WrapLen (h : Heap) (d : DeflateState) (wl : UInt64) : Prop :=
60  (d.wrap = 0 ∧ wl = 0) ∨ ((d.wrap = 1 ∨ d.wrap = -1) ∧ wl = 6 + (if d.strstart != 0 then 4 else 0)) ∨
61  ((d.wrap = 2 ∨ d.wrap = -2) ∧ ((d.gzhead = none ∧ wl = 18) ∨
62    ∃ g gh kn kc, d.gzhead = some (.tab g) ∧ h.gzheaders g = some gh ∧ StrPart h gh.name kn ∧ StrPart h gh.comment kc ∧
63      wl = 18 + (if gh.extra = .null then 0 else ((2 : UInt32) + gh.extra_len).toUInt64) + kn + kc +
64        (if gh.hcrc != 0 then 2 else 0)))
65
66/-- The user's header, if there is one, has NUL-terminated `name` and `comment` (or `NULL`), as `zlib.h` requires. -/
67def HdrStrOk (h : Heap) (d : DeflateState) : Prop :=
68  d.gzhead = none ∨ ∃ g gh, d.gzhead = some (.tab g) ∧ h.gzheaders g = some gh ∧ StrOk h gh.name ∧ StrOk h gh.comment
69
70end Zlib.Deflate.Spec
71
72namespace Zlib.Deflate.Proofs
73open C Zlib.Deflate Zlib.Deflate.Spec
74
75/-- The loop `do { wraplen++; } while (*str++);` over a string of length `len` adds `len + 1` to `wraplen` and leaves the
76pointer one past the terminating zero; it reads the heap only. -/
77theorem strLoop_run {h : Heap} {p : BPtr} {len : Nat} (hs : GzStr h p len) (w : UInt64) :
78    OkOn h (cdoWhile (fun (s : UInt64 × BPtr) => (pure (s.1 + 1, s.2) : M (UInt64 × BPtr)))
79      (fun (s : UInt64 × BPtr) => do
80        let b ← load8 s.2
81        pure (b != 0, (s.1, ← padd s.2 1)))
82      (w, p)) (w + UInt64.ofNat (len + 1), (match p with | .ref r off => .ref r (off + len + 1) | .null => .null)) := by
83  obtain ⟨r, off, a, rfl, hg, hlt, hz, hnz, hlen⟩ := hs
84  simp only
85  obtain ⟨k0, hk0⟩ : ∃ k, k = len := ⟨_, rfl⟩
86  have key := cdoWhile_ok (h := h)
87    (body := fun (s : UInt64 × BPtr) => (pure (s.1 + 1, s.2) : M (UInt64 × BPtr)))
88    (cond := fun (s : UInt64 × BPtr) => do
89        let b ← load8 s.2
90        pure (b != 0, (s.1, ← padd s.2 1)))
91    (P := fun k s => ∃ i, i + k = len ∧ s = (w + UInt64.ofNat i, (Ptr.ref r (off + i) : BPtr)))
92    (Q := fun s => s = (w + UInt64.ofNat (len + 1), (Ptr.ref r (off + len + 1) : BPtr)))
93    ?_ ?_ (k := len) (s := (w, (Ptr.ref r off : BPtr))) ⟨0, by omega, by simp⟩ (by unfold fuel; omega)
94  · obtain ⟨s', hs', rfl⟩ := key
95    exact hs'
96  · rintro k s ⟨i, hi, rfl⟩
97    have hlt' : off + i < a.size := by omega
98    have hnz' : a[off + i]? ≠ some 0 := hnz i (by omega)
99    have hne : a[off + i] ≠ 0 := by
100      intro h0; apply hnz'; simp [hlt', h0]
101    refine ⟨(w + UInt64.ofNat i + 1, Ptr.ref r (off + i)), (w + UInt64.ofNat (i + 1), Ptr.ref r (off + (i + 1))), rfl, ?_, i + 1, by omega, ?_⟩
102    · have e1 := Ptr.load_ok (r := r) (off := off + i) hg hlt'
103      have e2 := Ptr.add_nat_ok (r := r) (off := off + i) (n := 1) hg (by omega)
104      show OkOn h (do let b ← load8 (Ptr.ref r (off + i)); pure (b != 0, (w + UInt64.ofNat i + 1, ← padd (Ptr.ref r (off + i)) 1))) _
105      refine OkOn.bind (x := a[off + i]) e1 ?_
106      refine OkOn.bind (x := Ptr.ref r (off + i + 1)) e2 ?_
107      have hb : (a[off + i] != 0) = true := by simpa using hne
108      have e3 : w + UInt64.ofNat i + 1 = w + UInt64.ofNat (i + 1) := by
109        rw [UInt64.ofNat_add]; simp [UInt64.add_assoc]
110      unfold OkOn
111      simp [hb, e3, Nat.add_assoc]
112    · simp [Nat.add_assoc]
113  · rintro s ⟨i, hi, rfl⟩
114    have hi' : i = len := by omega
115    subst hi'
116    have hlt' : off + i < a.size := hlt
117    have hz' : a[off + i] = 0 := by
118      have := hz; simp [hlt'] at this; exact this
119    refine ⟨(w + UInt64.ofNat i + 1, Ptr.ref r (off + i)), (w + UInt64.ofNat i + 1, Ptr.ref r (off + i + 1)), rfl, ?_, ?_⟩
120    · have e1 := Ptr.load_ok (r := r) (off := off + i) hg hlt'
121      have e2 := Ptr.add_nat_ok (r := r) (off := off + i) (n := 1) hg (by omega)
122      show OkOn h (do let b ← load8 (Ptr.ref r (off + i)); pure (b != 0, (w + UInt64.ofNat i + 1, ← padd (Ptr.ref r (off + i)) 1))) _
123      refine OkOn.bind (x := a[off + i]) e1 ?_
124      refine OkOn.bind (x := Ptr.ref r (off + i + 1)) e2 ?_
125      unfold OkOn
126      simp [hz']
127    · have e3 : w + UInt64.ofNat i + 1 = w + UInt64.ofNat (i + 1) := by
128        rw [UInt64.ofNat_add]; simp [UInt64.add_assoc]
129      simp [e3]
130
131
132theorem wrap_cases {w : Int32} (h1 : -2 ≤ w.toInt) (h2 : w.toInt ≤ 2) :
133    w = 0 ∨ w = 1 ∨ w = -1 ∨ w = 2 ∨ w = -2 := by
134  have : w.toInt = 0 ∨ w.toInt = 1 ∨ w.toInt = -1 ∨ w.toInt = 2 ∨ w.toInt = -2 := by omega
135  rcases this with e | e | e | e | e
136  · exact Or.inl (Int32.toInt_inj.mp (e.trans (by decide)))
137  · exact Or.inr (Or.inl (Int32.toInt_inj.mp (e.trans (by decide))))
138  · exact Or.inr (Or.inr (Or.inl (Int32.toInt_inj.mp (e.trans (by decide)))))
139  · exact Or.inr (Or.inr (Or.inr (Or.inl (Int32.toInt_inj.mp (e.trans (by decide))))))
140  · exact Or.inr (Or.inr (Or.inr (Or.inr (Int32.toInt_inj.mp (e.trans (by decide))))))
141
142/-- `deflateBound_z` after `fixedlen` and `storelen` are computed, as a function of the two values. -/
143def boundBody (strm : ZStreamPtr) (fixedlen storelen : UInt64) (sourceLen : UInt64) : M UInt64 := do
144  if (← deflateStateCheck strm) != 0 then
145    let bound := if fixedlen > storelen then fixedlen else storelen
146    return if bound + 18 < bound then 0xffffffffffffffff else bound + 18
147  let s ← castDeflateState (← zrd strm (·.state))
148  let d ← ldDeflateState s
149  let w ← if d.wrap < 0 then ineg d.wrap else pure d.wrap
150  let mut wraplen : UInt64 := 18
151  if w == 0 then
152    wraplen := 0
153  else if w == 1 then
154    wraplen := 6 + (if d.strstart != 0 then 4 else 0)
155  else if w == 2 then
156    wraplen := 18
157    if d.gzhead != none then
158      let gh ← ldGzHeader d.gzhead
159      if gh.extra != .null then wraplen := wraplen + ((2 : UInt32) + gh.extra_len).toUInt64
160      if gh.name != .null then
161        let (wl, _) ← cdoWhile
162          (fun (wl, str) => pure (wl + 1, str))
163          (fun (wl, str) => do
164            let b ← load8 str
165            pure (b != 0, (wl, ← padd str 1)))
166          (wraplen, gh.name)
167        wraplen := wl
168      if gh.comment != .null then
169        let (wl, _) ← cdoWhile
170          (fun (wl, str) => pure (wl + 1, str))
171          (fun (wl, str) => do
172            let b ← load8 str
173            pure (b != 0, (wl, ← padd str 1)))
174          (wraplen, gh.comment)
175        wraplen := wl
176      if gh.hcrc != 0 then wraplen := wraplen + 2
177  else
178    wraplen := 18
179  if d.w_bits != 15 || d.hash_bits != 15 then
180    let bound := if d.w_bits ≤ d.hash_bits && d.level != 0 then fixedlen else storelen
181    return if bound + wraplen < bound then 0xffffffffffffffff else bound + wraplen
182  let bound : UInt64 := sourceLen + (sourceLen >>> 12) + (sourceLen >>> 14) + (sourceLen >>> 25) + 13 - 6 + wraplen
183  return if bound < sourceLen then 0xffffffffffffffff else bound
184
185theorem deflateBound_z_eq (strm : ZStreamPtr) (n : UInt64) :
186    deflateBound_z strm n = boundBody strm (fixedLen n) (storeLen n) n := by
187  unfold deflateBound_z boundBody fixedLen storeLen
188  by_cases c1 : n + (n >>> 3) + (n >>> 8) + (n >>> 9) + 4 < n <;>
189    by_cases c2 : n + (n >>> 5) + (n >>> 7) + (n >>> 11) + 7 < n <;>
190    simp only [c1, c2, ↓reduceIte] <;> rfl
191
192theorem ineg_m2 : ineg (-2) = (pure 2 : M Int32) := by
193  unfold ineg chk32
194  simp
195
196theorem ineg_m1 : ineg (-1) = (pure 1 : M Int32) := by
197  unfold ineg chk32
198  simp
199
200theorem boundBody_nostate {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
201    (fx st n : UInt64) : boundBody strm fx st n h = .ok (boundNoStateP fx st, h) := by
202  unfold boundBody
203  simp [bind_app, notInit_check hD hN, boundNoStateP]
204
205theorem boundBody_raw {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
206    (hL : DLive h r ds z d) (hw : d.wrap = 0) (fx st n : UInt64) :
207    boundBody (some r) fx st n h = .ok (boundTailP d.w_bits d.hash_bits d.level 0 fx st n, h) := by
208  unfold boundBody
209  dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw]
210  by_cases c : ¬d.w_bits = 15 ∨ ¬d.hash_bits = 15 <;> simp [boundTailP, c]
211
212theorem boundBody_zlib {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
213    (hL : DLive h r ds z d) (hw : d.wrap = 1 ∨ d.wrap = -1) (fx st n : UInt64) :
214    boundBody (some r) fx st n h =
215      .ok (boundTailP d.w_bits d.hash_bits d.level (6 + (if d.strstart != 0 then 4 else 0)) fx st n, h) := by
216  unfold boundBody
217  rcases hw with hw | hw
218  · dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw]
219    by_cases c : ¬d.w_bits = 15 ∨ ¬d.hash_bits = 15 <;> simp [boundTailP, c]
220  · dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw, ineg_m1]
221    by_cases c : ¬d.w_bits = 15 ∨ ¬d.hash_bits = 15 <;> simp [boundTailP, c]
222
223
224theorem boundBody_gz_nohead {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
225    (hL : DLive h r ds z d) (hw : d.wrap = 2 ∨ d.wrap = -2) (hg : d.gzhead = none) (fx st n : UInt64) :
226    boundBody (some r) fx st n h = .ok (boundTailP d.w_bits d.hash_bits d.level 18 fx st n, h) := by
227  unfold boundBody
228  rcases hw with hw | hw
229  · dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw, hg]
230    by_cases c : ¬d.w_bits = 15 ∨ ¬d.hash_bits = 15 <;> simp [boundTailP, c]
231  · dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw, hg, ineg_m2]
232    by_cases c : ¬d.w_bits = 15 ∨ ¬d.hash_bits = 15 <;> simp [boundTailP, c]
233
234theorem GzStr.ne_null {h : Heap} {p : BPtr} {len : Nat} (hs : GzStr h p len) : p ≠ .null := by
235  obtain ⟨r, off, a, rfl, -⟩ := hs
236  intro e; cases e
237
238theorem strLoop_eq {h : Heap} {p : BPtr} {len : Nat} (hs : GzStr h p len) (w : UInt64) :
239    cdoWhile (fun (s : UInt64 × BPtr) => (pure (s.1 + 1, s.2) : M (UInt64 × BPtr)))
240      (fun (s : UInt64 × BPtr) => do
241        let b ← load8 s.2
242        pure (b != 0, (s.1, ← padd s.2 1)))
243      (w, p) h = .ok ((w + UInt64.ofNat (len + 1), (match p with | .ref r off => .ref r (off + len + 1) | .null => .null)), h) :=
244  strLoop_run hs w
245
246set_option maxHeartbeats 1600000 in
247theorem boundBody_gz_head {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
248    (hL : DLive h r ds z d) (hw : d.wrap = 2 ∨ d.wrap = -2) {g : Nat} {gh : GzHeader}
249    (hg : d.gzhead = some (.tab g)) (hgh : h.gzheaders g = some gh) {kn kc : UInt64}
250    (hn : StrPart h gh.name kn) (hc : StrPart h gh.comment kc) (fx st n : UInt64) :
251    boundBody (some r) fx st n h = .ok (boundTailP d.w_bits d.hash_bits d.level
252      (18 + (if gh.extra = .null then 0 else ((2 : UInt32) + gh.extra_len).toUInt64) + kn + kc +
253        (if gh.hcrc != 0 then 2 else 0)) fx st n, h) := by
254  unfold boundBody
255  rcases hw with hw | hw
256  · rcases hn with ⟨hn0, rfl⟩ | ⟨ln, hs1, rfl⟩ <;> rcases hc with ⟨hc0, rfl⟩ | ⟨lc, hs2, rfl⟩ <;>
257      by_cases he : gh.extra = .null <;> by_cases hh : gh.hcrc = 0 <;> by_cases c : ¬d.w_bits = 15 ∨ ¬d.hash_bits = 15 <;>
258      (try have := GzStr.ne_null ‹GzStr h gh.name _›) <;> (try have := GzStr.ne_null ‹GzStr h gh.comment _›) <;>
259      dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw, hg, ldGzHeader_tab hgh] <;>
260      simp (disch := assumption) [boundTailP, c, he, hh, *, strLoop_eq]
261  · rcases hn with ⟨hn0, rfl⟩ | ⟨ln, hs1, rfl⟩ <;> rcases hc with ⟨hc0, rfl⟩ | ⟨lc, hs2, rfl⟩ <;>
262      by_cases he : gh.extra = .null <;> by_cases hh : gh.hcrc = 0 <;> by_cases c : ¬d.w_bits = 15 ∨ ¬d.hash_bits = 15 <;>
263      (try have := GzStr.ne_null ‹GzStr h gh.name _›) <;> (try have := GzStr.ne_null ‹GzStr h gh.comment _›) <;>
264      dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw, hg, ldGzHeader_tab hgh, ineg_m2] <;>
265      simp (disch := assumption) [boundTailP, c, he, hh, *, strLoop_eq]
266
267
268
269theorem StrOk.part {h : Heap} {p : BPtr} (hs : StrOk h p) : ∃ k, StrPart h p k := by
270  rcases hs with rfl | ⟨len, hl⟩
271  · exact ⟨0, Or.inl ⟨rfl, rfl⟩⟩
272  · exact ⟨_, Or.inr ⟨len, hl, rfl⟩⟩
273
274theorem _root_.Zlib.Deflate.Spec.DStInv.wrapLen {h : Heap} {ds : Nat} {d : DeflateState} (hI : DStInv h ds d) (hs : HdrStrOk h d) :
275    ∃ wl, WrapLen h d wl := by
276  have hw := wrap_cases (w := d.wrap) hI.wrap_lo hI.wrap_hi
277  rcases hw with hw | hw | hw | hw | hw
278  · exact ⟨0, Or.inl ⟨hw, rfl⟩⟩
279  · exact ⟨_, Or.inr (Or.inl ⟨Or.inl hw, rfl⟩)⟩
280  · exact ⟨_, Or.inr (Or.inl ⟨Or.inr hw, rfl⟩)⟩
281  all_goals
282    rcases hs with hg | ⟨g, gh, hg, hgh, hn, hc⟩
283    · exact ⟨18, Or.inr (Or.inr ⟨by simp [hw], Or.inl ⟨hg, rfl⟩⟩)⟩
284    · obtain ⟨kn, hkn⟩ := StrOk.part hn
285      obtain ⟨kc, hkc⟩ := StrOk.part hc
286      exact ⟨_, Or.inr (Or.inr ⟨by simp [hw], Or.inr ⟨g, gh, kn, kc, hg, hgh, hkn, hkc, rfl⟩⟩)⟩
287
288theorem boundBody_wl {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
289    (hL : DLive h r ds z d) {wl : UInt64} (hwl : WrapLen h d wl) (fx st n : UInt64) :
290    boundBody (some r) fx st n h = .ok (boundTailP d.w_bits d.hash_bits d.level wl fx st n, h) := by
291  rcases hwl with ⟨hw, rfl⟩ | ⟨hw, rfl⟩ | ⟨hw, ⟨hg, rfl⟩ | ⟨g, gh, kn, kc, hg, hgh, hn, hc, rfl⟩⟩
292  · exact boundBody_raw hL hw fx st n
293  · exact boundBody_zlib hL hw fx st n
294  · exact boundBody_gz_nohead hL hw hg fx st n
295  · exact boundBody_gz_head hL hw hg hgh hn hc fx st n
296
297/-- **deflateBound_z, safety and specification.** On an initialised stream with the invariant, and a user gzip header
298(if there is one) whose `name` and `comment` are `NULL` or NUL-terminated strings (`zlib.h` requires it; the
299precondition `HdrStrOk`), the call never faults and leaves the heap unchanged. Its value is the closed formula
300`boundTail` of `w_bits`, `hash_bits`, `level`, the wrapper length `wl` (`WrapLen`: 0 for raw, 6 or 10 for zlib, 18 and the
301parts of the header for gzip) and the source length. -/
302theorem deflateBound_z_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
303    (hG : DGood h r ds z d) (hs : HdrStrOk h d) (n : UInt64) :
304    ∃ wl, WrapLen h d wl ∧
305      C.run (deflateBound_z (some r) n) h = .ok (boundTail d.w_bits d.hash_bits d.level wl n, h) := by
306  obtain ⟨wl, hwl⟩ := hG.inv.wrapLen hs
307  refine ⟨wl, hwl, ?_⟩
308  rw [C.run, deflateBound_z_eq, boundBody_wl hG.live hwl]
309  rfl
310
311/-- **deflateBound_z on a stream the check refuses** (including `NULL`): the value `boundNoState`, the heap unchanged. -/
312theorem deflateBound_z_nostate {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
313    (n : UInt64) : C.run (deflateBound_z strm n) h = .ok (boundNoState n, h) := by
314  rw [C.run, deflateBound_z_eq, boundBody_nostate hD hN]
315  rfl
316
317/-- **deflateBound, safety and specification.** `deflateBound` is `deflateBound_z` (on this target `uLong` and
318`z_size_t` are both 64 bits, so the final saturation never applies). -/
319theorem deflateBound_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
320    (hG : DGood h r ds z d) (hs : HdrStrOk h d) (n : UInt64) :
321    ∃ wl, WrapLen h d wl ∧
322      C.run (deflateBound (some r) n) h = .ok (boundTail d.w_bits d.hash_bits d.level wl n, h) := by
323  obtain ⟨wl, hwl, e⟩ := deflateBound_z_safe hG hs n
324  refine ⟨wl, hwl, ?_⟩
325  unfold deflateBound
326  simp [C.run, bind_app] at e ⊢
327  simp [e]
328
329/-- **deflateBound on a stream the check refuses**: `boundNoState`, the heap unchanged. -/
330theorem deflateBound_nostate {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
331    (n : UInt64) : C.run (deflateBound strm n) h = .ok (boundNoState n, h) := by
332  have e := deflateBound_z_nostate hD hN n
333  unfold deflateBound
334  simp [C.run, bind_app] at e ⊢
335  simp [e]
336
337end Zlib.Deflate.Proofs