gzwrite.c.lean

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

1import ZlibF.Zlib.«gzlib.c»
2import ZlibF.Zlib.«deflate.c»
3
4/-!
5# gzwrite.c — faithful translation
6
7Source: `gzwrite.c` of the verified source (unpatched), default x86_64 Linux build. `STDC` is defined, so
8`gz_vacate`, `gzvprintf` and the `va_list` version of `gzprintf` are compiled; `HAVE_VSNPRINTF` is defined and
9`HAS_vsnprintf_void` is not, so the live call is `len = vsnprintf(next, state->size, format, va);`. The old-style
10`gzprintf` with twenty `int` arguments is not compiled.
11
12Decisions: `gzvprintf`/`gzprintf` take the variadic arguments as a list `VaArg` (`Zlib.GzFs`); `vsnprintf` is the
13model of `gzfs.lean`. `unsigned char buf[1]` of `gzputc` is a local block freed before every return.
14`write` goes through `GzFs.fsWrite`: the bytes it writes are read from the heap first (a fault if the range is not
15inside its object).
16-/
17
18namespace Zlib.Gzwrite
19open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib
20open Zlib.Deflate (deflateInit2_ deflateReset deflate deflateParams deflateEnd)
21
22/-- `local int gz_init(gz_statep state)` -/
23def gz_init (state : GzStatePtr) : G Int32 := do
24  let strm := strmOf state
25  -- state->in = (unsigned char *)malloc(state->want << 1);
26  let s ← ldS state
27  let inb ← allocB (s.want <<< 1).toNat
28  updS state fun s => { s with «in» := inb }
29  if inb == .null then
30    gz_error state Z_MEM_ERROR (← strLit "out of memory")
31    return -1
32  -- if (!state->direct) { ... }
33  let s ← ldS state
34  if s.direct == 0 then
35    -- state->out = (unsigned char *)malloc(state->want);
36    let outb ← allocB s.want.toNat
37    updS state fun s => { s with out := outb }
38    if outb == .null then
39      freeB (← ldS state).«in»
40      gz_error state Z_MEM_ERROR (← strLit "out of memory")
41      return -1
42    -- strm->zalloc = Z_NULL; strm->zfree = Z_NULL; strm->opaque = Z_NULL;
43    updZ strm fun z => { z with zalloc := .null, zfree := .null, «opaque» := .null }
44    -- ret = deflateInit2(strm, state->level, Z_DEFLATED, MAX_WBITS + 16, DEF_MEM_LEVEL, state->strategy);
45    let s ← ldS state
46    let ver ← strLit ZLIB_VERSION
47    let ret ← deflateInit2_ strm s.level Z_DEFLATED (MAX_WBITS + 16) DEF_MEM_LEVEL s.strategy ver 112
48    if ret != Z_OK then
49      let s ← ldS state
50      freeB s.out
51      freeB s.«in»
52      gz_error state Z_MEM_ERROR (← strLit "out of memory")
53      return -1
54  -- strm->next_in = NULL;
55  updZ strm fun z => { z with next_in := .null }
56  -- state->size = state->want;
57  updS state fun s => { s with size := s.want }
58  -- if (!state->direct) { strm->avail_out = state->size; strm->next_out = state->out; state->x.next = strm->next_out; }
59  let s ← ldS state
60  if s.direct == 0 then
61    updZ strm fun z => { z with avail_out := s.size, next_out := s.out }
62    let z ← ldZ strm
63    updX state fun x => { x with next := z.next_out }
64  return 0
65
66structure CompLoop where
67  ret : Int32
68  «have» : UInt32
69  res : Option Int32
70
71/-- `local int gz_comp(gz_statep state, int flush)`. `max` is `((unsigned)-1 >> 2) + 1`; the `return -1` inside the
72loops is the tag `res`. -/
73def gz_comp (state : GzStatePtr) (flush : Int32) : G Int32 := do
74  let strm := strmOf state
75  let max : UInt32 := (((0 : UInt32) - 1) >>> 2) + 1
76  -- if (state->size == 0 && gz_init(state) == -1) return -1;
77  if (← ldS state).size == 0 then
78    if (← gz_init state) == -1 then return -1
79  -- if (state->direct) { while (strm->avail_in) {...} return 0; }
80  if (← ldS state).direct != 0 then
81    let r ← gwhile
82      (fun (r : Option Int32) => do
83        if r.isSome then return (false, r)
84        return ((← ldZ strm).avail_in != 0, r))
85      (fun _ => do
86        setErrno 0
87        updS state fun s => { s with again := 0 }
88        let z ← ldZ strm
89        let s ← ldS state
90        let put : UInt32 := if z.avail_in > max then max else z.avail_in
91        let bs ← loadBytes z.next_in put.toNat
92        let writ := (← fsWrite s.fd bs).toInt32
93        if writ < 0 then
94          if BLOCKED (← getErrno) then updS state fun s => { s with again := 1 }
95          gz_error state Z_ERRNO (← zstrerror)
96          return some (-1)
97        let z ← ldZ strm
98        let np ← z.next_in.add writ.toInt
99        updZ strm fun z => { z with avail_in := z.avail_in - writ.toUInt32, next_in := np }
100        return none)
101      none
102    return r.getD 0
103  -- if (state->reset) { ... }
104  if (← ldS state).reset != 0 then
105    let z ← ldZ strm
106    if z.avail_in == 0 && flush == Z_NO_FLUSH then return 0
107    let _ ← deflateReset strm
108    updS state fun s => { s with reset := 0 }
109  -- ret = Z_OK; do { ... } while (have);
110  let l ← gdoWhile
111    (fun (l : CompLoop) => do
112      let z ← ldZ strm
113      let mut l := l
114      -- if (strm->avail_out == 0 || (flush != Z_NO_FLUSH && (flush != Z_FINISH || ret == Z_STREAM_END))) {
115      if z.avail_out == 0 || (flush != Z_NO_FLUSH && (flush != Z_FINISH || l.ret == Z_STREAM_END)) then
116        -- while (strm->next_out > state->x.next) {
117        let r ← gwhile
118          (fun (r : Option Int32) => do
119            if r.isSome then return (false, r)
120            let z ← ldZ strm
121            let s ← ldS state
122            return (← Ptr.lt s.x.next z.next_out, r))
123          (fun _ => do
124            setErrno 0
125            updS state fun s => { s with again := 0 }
126            let z ← ldZ strm
127            let s ← ldS state
128            -- put = next_out - x.next > (int)max ? max : (unsigned)(next_out - x.next);
129            let d ← Ptr.diff z.next_out s.x.next
130            let put : UInt32 := if d > (Int64.ofNat max.toNat) then max else d.toUInt64.toUInt32
131            let bs ← loadBytes s.x.next put.toNat
132            let writ := (← fsWrite s.fd bs).toInt32
133            if writ < 0 then
134              if BLOCKED (← getErrno) then updS state fun s => { s with again := 1 }
135              gz_error state Z_ERRNO (← zstrerror)
136              return some (-1)
137            let s ← ldS state
138            let nx ← s.x.next.add writ.toInt
139            updX state fun x => { x with next := nx }
140            return none)
141          none
142        if r.isSome then return { l with res := r }
143        -- if (strm->avail_out == 0) { strm->avail_out = state->size; next_out = out; x.next = out; }
144        if (← ldZ strm).avail_out == 0 then
145          let s ← ldS state
146          updZ strm fun z => { z with avail_out := s.size, next_out := s.out }
147          updX state fun x => { x with next := s.out }
148      -- have = strm->avail_out; ret = deflate(strm, flush);
149      let hv := (← ldZ strm).avail_out
150      let ret ← deflate strm flush
151      if ret == Z_STREAM_ERROR then
152        gz_error state Z_STREAM_ERROR (← strLit "internal error: deflate stream corrupt")
153        return { l with ret, res := some (-1) }
154      -- have -= strm->avail_out;
155      return { l with ret, «have» := hv - (← ldZ strm).avail_out })
156    (fun l => pure (l.res.isNone && l.«have» != 0, l))
157    { ret := Z_OK, «have» := 0, res := none }
158  if let some r := l.res then return r
159  -- if (flush == Z_FINISH) state->reset = 1;
160  if flush == Z_FINISH then updS state fun s => { s with reset := 1 }
161  return 0
162
163structure ZeroLoop where
164  first : Bool
165  res : Option Int32
166
167/-- `local int gz_zero(gz_statep state)` -/
168def gz_zero (state : GzStatePtr) : G Int32 := do
169  let strm := strmOf state
170  -- if (state->size == 0 && gz_init(state) == -1) return -1;
171  if (← ldS state).size == 0 then
172    if (← gz_init state) == -1 then return -1
173  -- if (strm->avail_in && gz_comp(state, Z_NO_FLUSH) == -1) return -1;
174  if (← ldZ strm).avail_in != 0 then
175    if (← gz_comp state Z_NO_FLUSH) == -1 then return -1
176  -- first = 1; do { ... } while (state->skip);
177  let l ← gdoWhile
178    (fun (l : ZeroLoop) => do
179      let s ← ldS state
180      -- n = GT_OFF(state->size) || (z_off64_t)state->size > state->skip ? (unsigned)state->skip : state->size;
181      let mut n : UInt32 ← if (← GT_OFF s.size) || u32ToI64 s.size > s.skip then pure s.skip.toUInt64.toUInt32
182        else pure s.size
183      let mut first := l.first
184      if first then
185        memsetB s.«in» 0 n.toNat
186        first := false
187      -- strm->avail_in = n; strm->next_in = state->in; ret = gz_comp(state, Z_NO_FLUSH);
188      updZ strm fun z => { z with avail_in := n, next_in := s.«in» }
189      let ret ← gz_comp state Z_NO_FLUSH
190      -- n -= strm->avail_in; state->x.pos += n; state->skip -= n;
191      n := n - (← ldZ strm).avail_in
192      let s ← ldS state
193      let np ← i64add s.x.pos (u32ToI64 n)
194      updX state fun x => { x with pos := np }
195      let s ← ldS state
196      let sk ← i64sub s.skip (u32ToI64 n)
197      updS state fun s => { s with skip := sk }
198      if ret == -1 then
199        let s ← ldS state
200        updZ strm fun z => { z with avail_in := 0, next_in := s.«in» }
201        return { first, res := some (-1) }
202      return { first, res := none })
203    (fun l => do
204      if l.res.isSome then return (false, l)
205      return ((← ldS state).skip != 0, l))
206    { first := true, res := none }
207  return l.res.getD 0
208
209structure WriteLoop where
210  len : UInt64
211  buf : BPtr
212  res : Option UInt64
213  brk : Bool
214
215/-- `local z_size_t gz_write(gz_statep state, voidpc buf, z_size_t len)` -/
216def gz_write (state : GzStatePtr) (buf : BPtr) (len : UInt64) : G UInt64 := do
217  let strm := strmOf state
218  -- z_size_t put = len;
219  let put := len
220  -- if (len == 0) return 0;
221  if len == 0 then return 0
222  -- if (state->size == 0 && gz_init(state) == -1) return 0;
223  if (← ldS state).size == 0 then
224    if (← gz_init state) == -1 then return 0
225  -- if (state->skip && gz_zero(state) == -1) return 0;
226  if (← ldS state).skip != 0 then
227    if (← gz_zero state) == -1 then return 0
228  -- if (len < state->size) { for (;;) {...} }
229  if len < (← ldS state).size.toUInt64 then
230    let l ← gwhile
231      (fun (l : WriteLoop) => pure (!l.brk && l.res.isNone, l))
232      (fun (l : WriteLoop) => do
233        -- if (state->strm.avail_in == 0) state->strm.next_in = state->in;
234        if (← ldZ strm).avail_in == 0 then
235          let s ← ldS state
236          updZ strm fun z => { z with next_in := s.«in» }
237        -- have = (unsigned)((state->strm.next_in + state->strm.avail_in) - state->in);
238        let z ← ldZ strm
239        let s ← ldS state
240        let tp ← z.next_in.add z.avail_in.toNat
241        let hv : UInt32 := (← Ptr.diff tp s.«in»).toUInt64.toUInt32
242        -- copy = state->size - have; if (copy > len) copy = (unsigned)len;
243        let mut copy := s.size - hv
244        if copy.toUInt64 > l.len then copy := l.len.toUInt32
245        -- memcpy(state->in + have, buf, copy);
246        memcpyB (← s.«in».add hv.toNat) l.buf copy.toNat
247        -- state->strm.avail_in += copy; state->x.pos += copy;
248        updZ strm fun z => { z with avail_in := z.avail_in + copy }
249        let s ← ldS state
250        let np ← i64add s.x.pos (u32ToI64 copy)
251        updX state fun x => { x with pos := np }
252        -- buf = (const char *)buf + copy; len -= copy;
253        let buf ← l.buf.add copy.toNat
254        let len := l.len - copy.toUInt64
255        -- if (len == 0) break;
256        if len == 0 then return { l with buf, len, brk := true }
257        -- if (gz_comp(state, Z_NO_FLUSH) == -1) return state->again ? put - len : 0;
258        if (← gz_comp state Z_NO_FLUSH) == -1 then
259          return { l with buf, len, res := some (if (← ldS state).again != 0 then put - len else 0) }
260        return { l with buf, len })
261      { len, buf, res := none, brk := false }
262    if let some r := l.res then return r
263  else
264    -- if (state->strm.avail_in && gz_comp(state, Z_NO_FLUSH) == -1) return 0;
265    if (← ldZ strm).avail_in != 0 then
266      if (← gz_comp state Z_NO_FLUSH) == -1 then return 0
267    -- state->strm.next_in = (z_const Bytef *)buf;
268    updZ strm fun z => { z with next_in := buf }
269    -- do { unsigned n = (unsigned)-1; ... } while (len);
270    let l ← gdoWhile
271      (fun (l : WriteLoop) => do
272        let mut n : UInt32 := 0xFFFFFFFF
273        if n.toUInt64 > l.len then n := l.len.toUInt32
274        updZ strm fun z => { z with avail_in := n }
275        let ret ← gz_comp state Z_NO_FLUSH
276        n := n - (← ldZ strm).avail_in
277        let s ← ldS state
278        let np ← i64add s.x.pos (u32ToI64 n)
279        updX state fun x => { x with pos := np }
280        let len := l.len - n.toUInt64
281        if ret == -1 then
282          let s ← ldS state
283          updZ strm fun z => { z with avail_in := 0, next_in := s.«in» }
284          return { l with len, res := some (if s.again != 0 then put - len else 0) }
285        return { l with len })
286      (fun l => pure (l.res.isNone && l.len != 0, l))
287      { len, buf, res := none, brk := false }
288    if let some r := l.res then return r
289    -- state->strm.next_in = state->in;
290    let s ← ldS state
291    updZ strm fun z => { z with next_in := s.«in» }
292  -- return put;
293  return put
294
295/-- `int ZEXPORT gzwrite(gzFile file, voidpc buf, unsigned len)` -/
296def gzwrite (file : GzFilePtr) (buf : BPtr) (len : UInt32) : G Int32 := do
297  if file.isNone then return 0
298  let state := castState file
299  let s ← ldS state
300  -- if (state->mode != GZ_WRITE || (state->err != Z_OK && !state->again)) return 0;
301  if s.mode != GZ_WRITE || (s.err != Z_OK && s.again == 0) then return 0
302  gz_error state Z_OK .null
303  -- if ((int)len < 0) { gz_error(state, Z_DATA_ERROR, "requested length does not fit in int"); return 0; }
304  if len.toInt32 < 0 then
305    gz_error state Z_DATA_ERROR (← strLit "requested length does not fit in int")
306    return 0
307  -- return (int)gz_write(state, buf, len);
308  return (← gz_write state buf len.toUInt64).toUInt32.toInt32
309
310/-- `z_size_t ZEXPORT gzfwrite(voidpc buf, z_size_t size, z_size_t nitems, gzFile file)` -/
311def gzfwrite (buf : BPtr) (size nitems : UInt64) (file : GzFilePtr) : G UInt64 := do
312  if file.isNone then return 0
313  let state := castState file
314  let s ← ldS state
315  if s.mode != GZ_WRITE || (s.err != Z_OK && s.again == 0) then return 0
316  gz_error state Z_OK .null
317  -- len = nitems * size; if (size && len / size != nitems) { ... return 0; }
318  let len := nitems * size
319  if size != 0 && len / size != nitems then
320    gz_error state Z_STREAM_ERROR (← strLit "request does not fit in a size_t")
321    return 0
322  -- return len ? gz_write(state, buf, len) / size : 0;
323  if len != 0 then return (← gz_write state buf len) / size else return 0
324
325/-- `int ZEXPORT gzputc(gzFile file, int c)` -/
326def gzputc (file : GzFilePtr) (c : Int32) : G Int32 := do
327  -- unsigned have; unsigned char buf[1];
328  if file.isNone then return -1
329  let state := castState file
330  let strm := strmOf state
331  let s ← ldS state
332  if s.mode != GZ_WRITE || (s.err != Z_OK && s.again == 0) then return -1
333  gz_error state Z_OK .null
334  -- if (state->skip && gz_zero(state) == -1) return -1;
335  if (← ldS state).skip != 0 then
336    if (← gz_zero state) == -1 then return -1
337  -- if (state->size) { ... }
338  if (← ldS state).size != 0 then
339    if (← ldZ strm).avail_in == 0 then
340      let s ← ldS state
341      updZ strm fun z => { z with next_in := s.«in» }
342    let z ← ldZ strm
343    let s ← ldS state
344    let tp ← z.next_in.add z.avail_in.toNat
345    let hv : UInt32 := (← Ptr.diff tp s.«in»).toUInt64.toUInt32
346    if hv < s.size then
347      store8 (← s.«in».add hv.toNat) c.toUInt32.toUInt8
348      updZ strm fun z => { z with avail_in := z.avail_in + 1 }
349      let np ← i64add s.x.pos 1
350      updX state fun x => { x with pos := np }
351      return c &&& 0xff
352  -- buf[0] = (unsigned char)c; if (gz_write(state, buf, 1) != 1) return -1; return c & 0xff;
353  let buf ← allocLocal 1
354  store8 buf c.toUInt32.toUInt8
355  let w ← gz_write state buf 1
356  freeB buf
357  if w != 1 then return -1
358  return c &&& 0xff
359
360/-- `int ZEXPORT gzputs(gzFile file, const char *s)` -/
361def gzputs (file : GzFilePtr) (str : BPtr) : G Int32 := do
362  if file.isNone then return -1
363  let state := castState file
364  let s ← ldS state
365  if s.mode != GZ_WRITE || (s.err != Z_OK && s.again == 0) then return -1
366  gz_error state Z_OK .null
367  -- len = strlen(s); if ((int)len < 0 || (unsigned)len != len) { ... return -1; }
368  let len ← strlenB str
369  if len.toUInt32.toInt32 < 0 || len.toUInt32.toUInt64 != len then
370    gz_error state Z_STREAM_ERROR (← strLit "string length does not fit in int")
371    return -1
372  -- put = gz_write(state, s, len); return len && put == 0 ? -1 : (int)put;
373  let put ← gz_write state str len
374  return if len != 0 && put == 0 then -1 else put.toUInt32.toInt32
375
376/-- `local int gz_vacate(gz_statep state)` -/
377def gz_vacate (state : GzStatePtr) : G Int32 := do
378  let strm := strmOf state
379  -- if (strm->next_in == NULL || strm->next_in + strm->avail_in <= state->in + state->size) return 0;
380  let z ← ldZ strm
381  if z.next_in == .null then return 0
382  let s ← ldS state
383  let a ← z.next_in.add z.avail_in.toNat
384  let b ← s.«in».add s.size.toNat
385  if (← Ptr.le a b) then return 0
386  -- (void)gz_comp(state, Z_NO_FLUSH);
387  let _ ← gz_comp state Z_NO_FLUSH
388  -- if (strm->avail_in == 0) { strm->next_in = state->in; return 0; }
389  if (← ldZ strm).avail_in == 0 then
390    let s ← ldS state
391    updZ strm fun z => { z with next_in := s.«in» }
392    return 0
393  -- memmove(state->in, strm->next_in, strm->avail_in); strm->next_in = state->in;
394  let z ← ldZ strm
395  let s ← ldS state
396  memmoveB s.«in» z.next_in z.avail_in.toNat
397  updZ strm fun z => { z with next_in := s.«in» }
398  -- return strm->avail_in > state->size;
399  return if (← ldZ strm).avail_in > s.size then 1 else 0
400
401/-- `int ZEXPORTVA gzvprintf(gzFile file, const char *format, va_list va)` -/
402def gzvprintf (file : GzFilePtr) (format : BPtr) (va : List VaArg) : G Int32 := do
403  if file.isNone then return Z_STREAM_ERROR
404  let state := castState file
405  let strm := strmOf state
406  let s ← ldS state
407  if s.mode != GZ_WRITE || (s.err != Z_OK && s.again == 0) then return Z_STREAM_ERROR
408  gz_error state Z_OK .null
409  -- if (state->size == 0 && gz_init(state) == -1) return state->err;
410  if (← ldS state).size == 0 then
411    if (← gz_init state) == -1 then return (← ldS state).err
412  -- if (state->skip && gz_zero(state) == -1) return state->err;
413  if (← ldS state).skip != 0 then
414    if (← gz_zero state) == -1 then return (← ldS state).err
415  -- ret = gz_vacate(state);
416  let ret ← gz_vacate state
417  let s ← ldS state
418  if s.err != 0 then
419    if ret != 0 && s.again != 0 then
420      gz_error state Z_BUF_ERROR (← strLit "stalled write on gzprintf")
421      return (← ldS state).err
422    if s.again == 0 then return s.err
423  -- if (strm->avail_in == 0) strm->next_in = state->in;
424  if (← ldZ strm).avail_in == 0 then
425    let s ← ldS state
426    updZ strm fun z => { z with next_in := s.«in» }
427  -- next = (char *)(state->in + (strm->next_in - state->in) + strm->avail_in);
428  let z ← ldZ strm
429  let s ← ldS state
430  let d ← Ptr.diff z.next_in s.«in»
431  let next ← (← s.«in».add d.toInt).add z.avail_in.toNat
432  -- next[state->size - 1] = 0;
433  store8 (← next.add (s.size - 1).toNat) 0
434  -- len = vsnprintf(next, state->size, format, va);
435  let len ← vsnprintf next s.size.toUInt64 format va
436  -- if (len == 0 || (unsigned)len >= state->size || next[state->size - 1] != 0) return 0;
437  if len == 0 || len.toUInt32 ≥ s.size then return 0
438  if (← index8 next (s.size - 1).toNat) != 0 then return 0
439  -- strm->avail_in += (unsigned)len; state->x.pos += len;
440  updZ strm fun z => { z with avail_in := z.avail_in + len.toUInt32 }
441  let s ← ldS state
442  let np ← i64add s.x.pos len.toInt64
443  updX state fun x => { x with pos := np }
444  -- ret = gz_vacate(state); if (ret) { ... }
445  let ret ← gz_vacate state
446  if ret != 0 then
447    updZ strm fun z => { z with avail_in := z.avail_in - len.toUInt32 }
448    let s ← ldS state
449    let np ← i64sub s.x.pos len.toInt64
450    updX state fun x => { x with pos := np }
451    if (← ldS state).again != 0 then
452      gz_error state Z_BUF_ERROR (← strLit "stalled write on gzprintf")
453    return (← ldS state).err
454  -- if (state->err && !state->again) return state->err; return len;
455  let s ← ldS state
456  if s.err != 0 && s.again == 0 then return s.err
457  return len
458
459/-- `int ZEXPORTVA gzprintf(gzFile file, const char *format, ...)`: `va_start` / `gzvprintf` / `va_end`. -/
460def gzprintf (file : GzFilePtr) (format : BPtr) (va : List VaArg) : G Int32 :=
461  gzvprintf file format va
462
463/-- `int ZEXPORT gzflush(gzFile file, int flush)` -/
464def gzflush (file : GzFilePtr) (flush : Int32) : G Int32 := do
465  if file.isNone then return Z_STREAM_ERROR
466  let state := castState file
467  let s ← ldS state
468  if s.mode != GZ_WRITE || (s.err != Z_OK && s.again == 0) then return Z_STREAM_ERROR
469  gz_error state Z_OK .null
470  -- if (flush < 0 || flush > Z_FINISH) return Z_STREAM_ERROR;
471  if flush < 0 || flush > Z_FINISH then return Z_STREAM_ERROR
472  -- if (state->skip && gz_zero(state) == -1) return state->err;
473  if (← ldS state).skip != 0 then
474    if (← gz_zero state) == -1 then return (← ldS state).err
475  -- (void)gz_comp(state, flush); return state->err;
476  let _ ← gz_comp state flush
477  return (← ldS state).err
478
479/-- `int ZEXPORT gzsetparams(gzFile file, int level, int strategy)`. Candidate finding (unconfirmed): the result
480(`Z_BUF_ERROR`) of `deflateParams` is ignored and the new level and strategy are stored anyway; see
481`docs/design/external-io.md`. -/
482def gzsetparams (file : GzFilePtr) (level strategy : Int32) : G Int32 := do
483  if file.isNone then return Z_STREAM_ERROR
484  let state := castState file
485  let strm := strmOf state
486  let s ← ldS state
487  -- if (state->mode != GZ_WRITE || (state->err != Z_OK && !state->again) || state->direct) return Z_STREAM_ERROR;
488  if s.mode != GZ_WRITE || (s.err != Z_OK && s.again == 0) || s.direct != 0 then return Z_STREAM_ERROR
489  gz_error state Z_OK .null
490  -- if (level == state->level && strategy == state->strategy) return Z_OK;
491  let s ← ldS state
492  if level == s.level && strategy == s.strategy then return Z_OK
493  -- if (state->skip && gz_zero(state) == -1) return state->err;
494  if s.skip != 0 then
495    if (← gz_zero state) == -1 then return (← ldS state).err
496  -- if (state->size) { ... }
497  if (← ldS state).size != 0 then
498    if (← ldZ strm).avail_in != 0 then
499      if (← gz_comp state Z_BLOCK) == -1 then return (← ldS state).err
500    let _ ← deflateParams strm level strategy
501  -- state->level = level; state->strategy = strategy; return Z_OK;
502  updS state fun s => { s with level, strategy }
503  return Z_OK
504
505/-- `int ZEXPORT gzclose_w(gzFile file)` -/
506def gzclose_w (file : GzFilePtr) : G Int32 := do
507  let mut ret := Z_OK
508  if file.isNone then return Z_STREAM_ERROR
509  let state := castState file
510  let s ← ldS state
511  -- if (state->mode != GZ_WRITE) return Z_STREAM_ERROR;
512  if s.mode != GZ_WRITE then return Z_STREAM_ERROR
513  -- if (state->skip && gz_zero(state) == -1) ret = state->err;
514  if s.skip != 0 then
515    if (← gz_zero state) == -1 then ret := (← ldS state).err
516  -- if (gz_comp(state, Z_FINISH) == -1) ret = state->err;
517  if (← gz_comp state Z_FINISH) == -1 then ret := (← ldS state).err
518  -- if (state->size) { if (!state->direct) { (void)deflateEnd(&(state->strm)); free(state->out); } free(state->in); }
519  let s ← ldS state
520  if s.size != 0 then
521    if s.direct == 0 then
522      let _ ← deflateEnd (strmOf state)
523      freeB s.out
524    freeB s.«in»
525  -- gz_error(state, Z_OK, NULL); free(state->path);
526  gz_error state Z_OK .null
527  let s ← ldS state
528  freeB s.path
529  -- if (close(state->fd) == -1) ret = Z_ERRNO;
530  if (← fsClose s.fd) == -1 then ret := Z_ERRNO
531  -- free(state); return ret;
532  freeGzState state
533  return ret
534
535end Zlib.Gzwrite