infback.c.lean

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

1import ZlibF.Zlib.«inflate.c»
2
3/-!
4# infback.c — faithful translation
5
6Source: `infback.c` of the verified source, default x86_64 Linux build (same configuration as `inflate.c.lean`; read its
7header first: the registers, the monad `X`, `goto inf_leave` as `throw Ex.leave`, the loops).
8
9## The call-backs
10
11`inflateBack` takes the caller's functions as parameters (they are caller code, not library code):
12
13* `in_func`: `unsigned (*)(void *in_desc, z_const unsigned char **buf)` is `InCb`. The C passes `&next`, the address of
14  the local `next`. A pointer to a scalar is passed by value (decision D3 of the notes): the call-back receives the
15  current value of `next` and returns `(count, new value of *buf)`. A call-back that keeps the address and writes
16  through it after it returned is not modelled.
17* `out_func`: `int (*)(void *out_desc, unsigned char *buf, unsigned len)` is `OutCb`.
18
19Both run on the shared heap, so they can read and write any block. `inflateBack` makes no assumption about them; a
20theorem about it has to state what it needs (`docs/proof/callbacks.md`).
21
22## Other decisions
23
24* `inflateBackInit_` does **not** zero the state: the record is `allocInflateState`, arbitrary integers and null
25  pointers, and only the fields the C writes are written.
26* `ret` is not initialised in the C before `for (;;)`; it is set before every `goto inf_leave`. It starts as `0` here.
27-/
28
29namespace Zlib.Infback
30open C
31open Zlib.Crc32 (crc32)
32open Zlib.Inffast (inflate_fast)
33open Zlib.Inftrees (inflate_table inflate_fixed)
34open Zlib.Inflate (X Ex IL Stop xwhile xwhileBrk xdoWhile xloopBrk shl32 shr32 shl64 u2i i2u chkI32 BITS DROPBITS BYTEBITS
35  INITBITS LOAD RESTORE rdS wrS rdZ wrZ lensP workP codesP orderAt setMsg setMode ZALLOCS ZFREES)
36
37/-- `in_func`: `unsigned (*)(void FAR *, z_const unsigned char FAR * FAR *)`; see the file comment. -/
38abbrev InCb := BPtr → BPtr → M (UInt32 × BPtr)
39/-- `out_func`: `int (*)(void FAR *, unsigned char FAR *, unsigned)` -/
40abbrev OutCb := BPtr → BPtr → UInt32 → M Int32
41
42/-- What `inflateBack()` and its macros share. -/
43structure BCtx where
44  strm : ZStreamPtr
45  st : InflateStatePtr
46  inCb : InCb
47  inDesc : BPtr
48  outCb : OutCb
49  outDesc : BPtr
50
51/-- `int ZEXPORT inflateBackInit_(z_streamp strm, int windowBits, unsigned char FAR *window, const char *version,
52int stream_size)` -/
53def inflateBackInit_ (strm : ZStreamPtr) (windowBits : Int32) (window : BPtr) (version : BPtr) (stream_size : Int32) :
54    M Int32 := do
55  -- if (version == Z_NULL || version[0] != ZLIB_VERSION[0] || stream_size != (int)(sizeof(z_stream))) return Z_VERSION_ERROR;
56  if version == .null then return Z_VERSION_ERROR
57  if (← index8 version 0) != 49 then return Z_VERSION_ERROR
58  if stream_size != 112 then return Z_VERSION_ERROR
59  -- if (strm == Z_NULL || window == Z_NULL || windowBits < 8 || windowBits > 15) return Z_STREAM_ERROR;
60  if strm == none || window == .null || windowBits < 8 || windowBits > 15 then return Z_STREAM_ERROR
61  -- strm->msg = Z_NULL;
62  wrZ strm fun z => { z with msg := .null }
63  -- if (strm->zalloc == (alloc_func)0) { strm->zalloc = zcalloc; strm->opaque = (voidpf)0; }
64  if (← rdZ strm (·.zalloc)) == .null then
65    wrZ strm fun z => { z with zalloc := .fn "zcalloc", «opaque» := .null }
66  -- if (strm->zfree == (free_func)0) strm->zfree = zcfree;
67  if (← rdZ strm (·.zfree)) == .null then
68    wrZ strm fun z => { z with zfree := .fn "zcfree" }
69  -- state = (struct inflate_state FAR *)ZALLOC(strm, 1, sizeof(struct inflate_state));   (not zeroed)
70  let state ← ZALLOCS strm
71  -- if (state == Z_NULL) return Z_MEM_ERROR;
72  if state == none then return Z_MEM_ERROR
73  -- strm->state = (struct internal_state FAR *)state;
74  wrZ strm fun z => { z with state := StateRef.ofInflateState state }
75  -- state->dmax = 32768U; state->wbits = (uInt)windowBits; state->wsize = 1U << windowBits;
76  let ws ← shl32 1 (i2u windowBits)
77  -- state->window = window; state->wnext = 0; state->whave = 0; state->sane = 1;
78  wrS state fun s => { s with
79    dmax := 32768, wbits := i2u windowBits, wsize := ws, window := window, wnext := 0, whave := 0, sane := 1 }
80  return Z_OK
81
82/-! ## The macros of `infback.c` that differ from `inflate.c` -/
83
84/-- `PULL()`: calls the caller's `in` when `have == 0`; `goto inf_leave` with `next = NULL`, `ret = Z_BUF_ERROR` if it
85returns 0. -/
86def PULL (c : BCtx) : X Unit := do
87  let l ← get
88  if l.have_ == 0 then
89    -- have = in(in_desc, &next);
90    let (h, nx) ← c.inCb c.inDesc l.next
91    set { l with have_ := h, next := nx }
92    if h == 0 then
93      -- next = Z_NULL; ret = Z_BUF_ERROR; goto inf_leave;
94      set { l with have_ := h, next := .null, ret := Z_BUF_ERROR }
95      throw Ex.leave
96
97/-- `PULLBYTE()` -/
98def PULLBYTE (c : BCtx) : X Unit := do
99  PULL c
100  let l ← get
101  -- have--; hold += (unsigned long)(*next++) << bits; bits += 8;
102  let b ← load8 l.next
103  let nx ← l.next.add 1
104  let sh ← shl64 b.toUInt64 l.bits
105  set { l with have_ := l.have_ - 1, next := nx, hold := l.hold + sh, bits := l.bits + 8 }
106
107/-- `NEEDBITS(n)` -/
108def NEEDBITS (c : BCtx) (n : UInt32) : X Unit :=
109  xwhile (do return (← get).bits < n) (PULLBYTE c)
110
111/-- `ROOM()`: when the window is full, hand it to `out`. -/
112def ROOM (c : BCtx) : X Unit := do
113  let l ← get
114  if l.left == 0 then
115    -- put = state->window; left = state->wsize; state->whave = left;
116    let s ← ldInflateState c.st
117    set { l with put := s.window, left := s.wsize }
118    wrS c.st fun s => { s with whave := s.wsize }
119    -- if (out(out_desc, put, left)) { ret = Z_BUF_ERROR; goto inf_leave; }
120    if (← c.outCb c.outDesc s.window s.wsize) != 0 then
121      modify fun l => { l with ret := Z_BUF_ERROR }
122      throw Ex.leave
123
124/-- `strm->msg = "..."; state->mode = BAD;` -/
125def badMode (c : BCtx) (msg : String) : M Unit := do
126  setMsg c.strm msg
127  setMode c.st BAD
128
129/-- `for (;;) { here = TABLE[BITS(bitsOfTable)]; if ((unsigned)(here.bits) <= bits) break; PULLBYTE(); }` -/
130def lookup1 (c : BCtx) (dist : Bool) : X Unit :=
131  xloopBrk (do
132    let s ← ldInflateState c.st
133    let tab := if dist then s.distcode else s.lencode
134    let nb := if dist then s.distbits else s.lenbits
135    let b ← BITS nb
136    let here ← Ptr.index tab (b.toNat : Int)
137    modify fun l => { l with here := here }
138    if here.bits.toUInt32 <= (← get).bits then return true
139    PULLBYTE c
140    return false)
141
142/-- `for (;;) { here = TABLE[last.val + (BITS(last.bits + last.op) >> last.bits)]; if ((unsigned)(last.bits + here.bits) <= bits) break; PULLBYTE(); }` -/
143def lookup2 (c : BCtx) (dist : Bool) : X Unit :=
144  xloopBrk (do
145    let s ← ldInflateState c.st
146    let tab := if dist then s.distcode else s.lencode
147    let last := (← get).last
148    let b ← BITS (last.bits.toUInt32 + last.op.toUInt32)
149    let sh ← shr32 b last.bits.toUInt32
150    let here ← Ptr.index tab ((last.val.toUInt32 + sh).toNat : Int)
151    modify fun l => { l with here := here }
152    if (last.bits.toUInt32 + here.bits.toUInt32) <= (← get).bits then return true
153    PULLBYTE c
154    return false)
155
156/-! ## The modes -/
157
158/-- `case LEN:` -/
159def back_LEN (c : BCtx) : X Unit := do
160  let l ← get
161  -- if (have >= 6 && left >= 258) { RESTORE(); inflate_fast(strm, state->wsize); LOAD(); break; }
162  if l.have_ >= 6 && l.left >= 258 then
163    RESTORE c.strm c.st
164    inflate_fast c.strm (← rdS c.st (·.wsize))
165    LOAD c.strm c.st
166    return
167  lookup1 c false
168  let here := (← get).here
169  -- if (here.op && (here.op & 0xf0) == 0) {
170  if here.op != 0 && (here.op &&& 0xf0) == 0 then
171    modify fun l => { l with last := here }
172    lookup2 c false
173    DROPBITS (← get).last.bits.toUInt32
174  -- DROPBITS(here.bits); state->length = (unsigned)here.val;
175  let here := (← get).here
176  DROPBITS here.bits.toUInt32
177  wrS c.st fun s => { s with length := here.val.toUInt32 }
178  -- if (here.op == 0) { ROOM(); *put++ = (unsigned char)(state->length); left--; state->mode = LEN; break; }
179  if here.op == 0 then
180    ROOM c
181    let l ← get
182    store8 l.put (← ldInflateState c.st).length.toUInt8
183    let p ← l.put.add 1
184    set { l with put := p, left := l.left - 1 }
185    setMode c.st LEN
186    return
187  -- if (here.op & 32) { state->mode = TYPE; break; }
188  if (here.op &&& 32) != 0 then
189    setMode c.st TYPE
190    return
191  -- if (here.op & 64) { "invalid literal/length code"; BAD; break; }
192  if (here.op &&& 64) != 0 then
193    badMode c "invalid literal/length code"
194    return
195  -- state->extra = (unsigned)(here.op) & 15; if (state->extra != 0) { NEEDBITS; length += BITS(extra); DROPBITS(extra); }
196  wrS c.st fun s => { s with extra := here.op.toUInt32 &&& 15 }
197  let ex := here.op.toUInt32 &&& 15
198  if ex != 0 then
199    NEEDBITS c ex
200    let b ← BITS ex
201    wrS c.st fun s => { s with length := s.length + b }
202    DROPBITS ex
203  -- get distance code
204  lookup1 c true
205  let here := (← get).here
206  if (here.op &&& 0xf0) == 0 then
207    modify fun l => { l with last := here }
208    lookup2 c true
209    DROPBITS (← get).last.bits.toUInt32
210  let here := (← get).here
211  DROPBITS here.bits.toUInt32
212  -- if (here.op & 64) { "invalid distance code"; BAD; break; }
213  if (here.op &&& 64) != 0 then
214    badMode c "invalid distance code"
215    return
216  -- state->offset = (unsigned)here.val; state->extra = (unsigned)(here.op) & 15;
217  wrS c.st fun s => { s with offset := here.val.toUInt32, extra := here.op.toUInt32 &&& 15 }
218  let ex := here.op.toUInt32 &&& 15
219  if ex != 0 then
220    NEEDBITS c ex
221    let b ← BITS ex
222    wrS c.st fun s => { s with offset := s.offset + b }
223    DROPBITS ex
224  -- if (state->offset > state->wsize - (state->whave < state->wsize ? left : 0)) { "invalid distance too far back"; BAD; break; }
225  let s ← ldInflateState c.st
226  let l ← get
227  if s.offset > s.wsize - (if s.whave < s.wsize then l.left else 0) then
228    badMode c "invalid distance too far back"
229    return
230  -- do { ROOM(); copy = state->wsize - state->offset; ...; do { *put++ = *from++; } while (--copy); } while (state->length != 0);
231  xdoWhile
232    (do
233      ROOM c
234      let s ← ldInflateState c.st
235      let l ← get
236      -- copy = state->wsize - state->offset;
237      let copy := s.wsize - s.offset
238      -- if (copy < left) { from = put + copy; copy = left - copy; } else { from = put - state->offset; copy = left; }
239      let (from_, copy) ← if copy < l.left then do
240          pure (← l.put.add (copy.toNat : Int), l.left - copy)
241        else do
242          pure (← l.put.add (-(s.offset.toNat : Int)), l.left)
243      -- if (copy > state->length) copy = state->length;
244      let copy := if copy > s.length then s.length else copy
245      -- state->length -= copy; left -= copy;
246      wrS c.st fun s => { s with length := s.length - copy }
247      set { l with copy := copy, from_ := from_, left := l.left - copy }
248      xdoWhile
249        (do
250          let l ← get
251          let b ← load8 l.from_
252          store8 l.put b
253          let p ← l.put.add 1
254          let f ← l.from_.add 1
255          set { l with put := p, from_ := f })
256        (do
257          let l ← get
258          let n := l.copy - 1
259          set { l with copy := n }
260          return n != 0))
261    (do return (← rdS c.st (·.length)) != 0)
262
263/-- `case TABLE:` (falls through into `LEN`) -/
264def back_TABLE (c : BCtx) : X Unit := do
265  NEEDBITS c 14
266  let b ← BITS 5
267  wrS c.st fun s => { s with nlen := b + 257 }
268  DROPBITS 5
269  let b ← BITS 5
270  wrS c.st fun s => { s with ndist := b + 1 }
271  DROPBITS 5
272  let b ← BITS 4
273  wrS c.st fun s => { s with ncode := b + 4 }
274  DROPBITS 4
275  -- if (state->nlen > 286 || state->ndist > 30) { "too many length or distance symbols"; BAD; break; }
276  let s ← ldInflateState c.st
277  if s.nlen > 286 || s.ndist > 30 then
278    badMode c "too many length or distance symbols"
279    return
280  -- state->have = 0; while (state->have < state->ncode) { NEEDBITS(3); lens[order[have++]] = BITS(3); DROPBITS(3); }
281  wrS c.st fun s => { s with «have» := 0 }
282  xwhile
283    (do let s ← ldInflateState c.st; return s.«have» < s.ncode)
284    (do
285      NEEDBITS c 3
286      let s ← ldInflateState c.st
287      wrS c.st fun s => { s with «have» := s.«have» + 1 }
288      let o ← orderAt s.«have»
289      let b ← BITS 3
290      Ptr.store (← (lensP c.st).add (o.toNat : Int)) b.toUInt16
291      DROPBITS 3)
292  xwhile
293    (do let s ← ldInflateState c.st; return s.«have» < 19)
294    (do
295      let s ← ldInflateState c.st
296      wrS c.st fun s => { s with «have» := s.«have» + 1 }
297      let o ← orderAt s.«have»
298      Ptr.store (← (lensP c.st).add (o.toNat : Int)) (0 : UInt16))
299  -- state->next = state->codes; state->lencode = (code const FAR *)(state->next); state->lenbits = 7;
300  wrS c.st fun s => { s with next := codesP c.st, lencode := codesP c.st, lenbits := 7 }
301  let s ← ldInflateState c.st
302  let (r, nx, lb) ← inflate_table CODES (lensP c.st) 19 s.next s.lenbits (workP c.st)
303  wrS c.st fun s => { s with next := nx, lenbits := lb }
304  modify fun l => { l with ret := r }
305  if r != 0 then
306    badMode c "invalid code lengths set"
307    return
308  -- state->have = 0; while (state->have < state->nlen + state->ndist) { ... }
309  wrS c.st fun s => { s with «have» := 0 }
310  xwhileBrk
311    (do let s ← ldInflateState c.st; return s.«have» < s.nlen + s.ndist)
312    (do
313      lookup1 c false
314      let here := (← get).here
315      if here.val < 16 then
316        DROPBITS here.bits.toUInt32
317        let s ← ldInflateState c.st
318        Ptr.store (← (lensP c.st).add (s.«have».toNat : Int)) here.val
319        wrS c.st fun s => { s with «have» := s.«have» + 1 }
320        return false
321      else
322        if here.val == 16 then
323          NEEDBITS c (here.bits.toUInt32 + 2)
324          DROPBITS here.bits.toUInt32
325          let s ← ldInflateState c.st
326          if s.«have» == 0 then
327            badMode c "invalid bit length repeat"
328            return true
329          -- len = (unsigned)(state->lens[state->have - 1]); copy = 3 + BITS(2); DROPBITS(2);
330          let v ← Ptr.index (lensP c.st) ((s.«have» - 1).toNat : Int)
331          let b ← BITS 2
332          modify fun l => { l with len := v.toUInt32, copy := 3 + b }
333          DROPBITS 2
334        else if here.val == 17 then
335          NEEDBITS c (here.bits.toUInt32 + 3)
336          DROPBITS here.bits.toUInt32
337          let b ← BITS 3
338          modify fun l => { l with len := 0, copy := 3 + b }
339          DROPBITS 3
340        else
341          NEEDBITS c (here.bits.toUInt32 + 7)
342          DROPBITS here.bits.toUInt32
343          let b ← BITS 7
344          modify fun l => { l with len := 0, copy := 11 + b }
345          DROPBITS 7
346        let s ← ldInflateState c.st
347        if s.«have» + (← get).copy > s.nlen + s.ndist then
348          badMode c "invalid bit length repeat"
349          return true
350        xwhile
351          (do
352            let l ← get
353            set { l with copy := l.copy - 1 }
354            return l.copy != 0)
355          (do
356            let s ← ldInflateState c.st
357            Ptr.store (← (lensP c.st).add (s.«have».toNat : Int)) (← get).len.toUInt16
358            wrS c.st fun s => { s with «have» := s.«have» + 1 })
359        return false)
360  -- if (state->mode == BAD) break;
361  if (← rdS c.st (·.mode)) == BAD then return
362  -- if (state->lens[256] == 0) { "invalid code -- missing end-of-block"; BAD; break; }
363  if (← Ptr.index (lensP c.st) 256) == (0 : UInt16) then
364    badMode c "invalid code -- missing end-of-block"
365    return
366  wrS c.st fun s => { s with next := codesP c.st, lencode := codesP c.st, lenbits := 9 }
367  let s ← ldInflateState c.st
368  let (r, nx, lb) ← inflate_table LENS (lensP c.st) s.nlen s.next s.lenbits (workP c.st)
369  wrS c.st fun s => { s with next := nx, lenbits := lb }
370  modify fun l => { l with ret := r }
371  if r != 0 then
372    badMode c "invalid literal/lengths set"
373    return
374  wrS c.st fun s => { s with distcode := s.next, distbits := 6 }
375  let s ← ldInflateState c.st
376  let (r, nx, db) ← inflate_table DISTS (← (lensP c.st).add (s.nlen.toNat : Int)) s.ndist s.next s.distbits (workP c.st)
377  wrS c.st fun s => { s with next := nx, distbits := db }
378  modify fun l => { l with ret := r }
379  if r != 0 then
380    badMode c "invalid distances set"
381    return
382  -- state->mode = LEN; /* fallthrough */
383  setMode c.st LEN
384  back_LEN c
385
386/-- `case STORED:` -/
387def back_STORED (c : BCtx) : X Unit := do
388  BYTEBITS
389  NEEDBITS c 32
390  let l ← get
391  if (l.hold &&& (0xffff : UInt64)) != ((l.hold >>> 16) ^^^ (0xffff : UInt64)) then
392    badMode c "invalid stored block lengths"
393    return
394  wrS c.st fun s => { s with length := l.hold.toUInt32 &&& 0xffff }
395  INITBITS
396  -- while (state->length != 0) { copy = state->length; PULL(); ROOM(); ... }
397  xwhile
398    (do return (← rdS c.st (·.length)) != 0)
399    (do
400      let s ← ldInflateState c.st
401      modify fun l => { l with copy := s.length }
402      PULL c
403      ROOM c
404      let l ← get
405      let mut copy := l.copy
406      if copy > l.have_ then copy := l.have_
407      if copy > l.left then copy := l.left
408      memcpyB l.put l.next copy.toNat
409      let nx ← l.next.add (copy.toNat : Int)
410      let pt ← l.put.add (copy.toNat : Int)
411      set { l with copy := copy, have_ := l.have_ - copy, next := nx, left := l.left - copy, put := pt }
412      wrS c.st fun s => { s with length := s.length - copy })
413  setMode c.st TYPE
414
415/-- `case TYPE:` -/
416def back_TYPE (c : BCtx) : X Unit := do
417  -- if (state->last) { BYTEBITS(); state->mode = DONE; break; }
418  if (← rdS c.st (·.last)) != 0 then
419    BYTEBITS
420    setMode c.st DONE
421    return
422  NEEDBITS c 3
423  let b ← BITS 1
424  wrS c.st fun s => { s with last := u2i b }
425  DROPBITS 1
426  match (← BITS 2) with
427  | 0 => setMode c.st STORED
428  | 1 =>
429    inflate_fixed c.st
430    setMode c.st LEN
431  | 2 => setMode c.st TABLE
432  | _ => badMode c "invalid block type"
433  DROPBITS 2
434
435/-- The `switch (state->mode)` of `inflateBack()`. -/
436def back_dispatch (c : BCtx) : X Unit := do
437  let m ← rdS c.st (·.mode)
438  if m == TYPE then back_TYPE c
439  else if m == STORED then back_STORED c
440  else if m == TABLE then back_TABLE c
441  else if m == LEN then back_LEN c
442  else if m == DONE then
443    -- ret = Z_STREAM_END; goto inf_leave;
444    modify fun l => { l with ret := Z_STREAM_END }
445    throw Ex.leave
446  else if m == BAD then
447    modify fun l => { l with ret := Z_DATA_ERROR }
448    throw Ex.leave
449  else
450    -- default: ret = Z_STREAM_ERROR; goto inf_leave;
451    modify fun l => { l with ret := Z_STREAM_ERROR }
452    throw Ex.leave
453
454/-- `int ZEXPORT inflateBack(z_streamp strm, in_func in, void FAR *in_desc, out_func out, void FAR *out_desc)` -/
455def inflateBack (strm : ZStreamPtr) (inCb : InCb) (in_desc : BPtr) (outCb : OutCb) (out_desc : BPtr) : M Int32 := do
456  -- if (strm == Z_NULL || strm->state == Z_NULL) return Z_STREAM_ERROR;
457  if strm == none then return Z_STREAM_ERROR
458  let z ← ldZStream strm
459  if z.state == none then return Z_STREAM_ERROR
460  -- state = (struct inflate_state FAR *)strm->state;
461  let st ← castInflateState z.state
462  -- strm->msg = Z_NULL; state->mode = TYPE; state->last = 0; state->whave = 0;
463  wrZ strm fun z => { z with msg := .null }
464  wrS st fun s => { s with mode := TYPE, last := 0, whave := 0 }
465  -- next = strm->next_in; have = next != Z_NULL ? strm->avail_in : 0; hold = 0; bits = 0;
466  let z ← ldZStream strm
467  let s ← ldInflateState st
468  let next := z.next_in
469  let have_ := if next != .null then z.avail_in else 0
470  -- put = state->window; left = state->wsize;
471  let l0 : IL := { IL.init with next := next, have_ := have_, hold := 0, bits := 0, put := s.window, left := s.wsize }
472  let c : BCtx := { strm, st, inCb, inDesc := in_desc, outCb, outDesc := out_desc }
473  -- for (;;) switch (state->mode) { ... }
474  let (_, l) ← StateT.run (ExceptT.run (xwhile (pure true) (back_dispatch c))) l0
475  -- inf_leave: if (left < state->wsize) { if (out(out_desc, state->window, state->wsize - left) && ret == Z_STREAM_END) ret = Z_BUF_ERROR; }
476  let s ← ldInflateState st
477  let mut ret := l.ret
478  if l.left < s.wsize then
479    if (← outCb out_desc s.window (s.wsize - l.left)) != 0 && ret == Z_STREAM_END then ret := Z_BUF_ERROR
480  -- strm->next_in = next; strm->avail_in = have; return ret;
481  wrZ strm fun z => { z with next_in := l.next, avail_in := l.have_ }
482  return ret
483
484/-- `int ZEXPORT inflateBackEnd(z_streamp strm)` -/
485def inflateBackEnd (strm : ZStreamPtr) : M Int32 := do
486  -- if (strm == Z_NULL || strm->state == Z_NULL || strm->zfree == (free_func)0) return Z_STREAM_ERROR;
487  if strm == none then return Z_STREAM_ERROR
488  let z ← ldZStream strm
489  if z.state == none || z.zfree == .null then return Z_STREAM_ERROR
490  -- ZFREE(strm, strm->state); strm->state = Z_NULL;
491  let st ← castInflateState z.state
492  ZFREES strm st
493  wrZ strm fun z => { z with state := none }
494  return Z_OK
495
496end Zlib.Infback