deflate.c.lean

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

1import ZlibF.Zlib.«deflate_base.c»
2import ZlibF.Zlib.«deflate_strategies.c»
3
4/-!
5# deflate.c, part 3: the public functions
6
7Faithful translation of `deflate.c` (default x86_64 Linux build). Parts 1 and 2 are `deflate_base.c.lean`
8(`slide_hash`, `read_buf`, `fill_window`, `flush_pending`, the macros) and `deflate_strategies.c.lean`
9(`longest_match`, `deflate_stored`, ..., `deflate_huff`).
10
11**Order.** Lean needs a definition before its use, so the order differs from the C where a function is only declared
12(in `zlib.h`) when it is used: `deflateEnd`, `deflateResetKeep`, `lm_init`, `deflateReset` come before
13`deflateInit2_`, and `deflateParams` and `deflateCopy` come after `deflate`. No function changes.
14
15**Output parameters.** C passes `unsigned *pending`, `int *bits`, `uInt *dictLength`. The runtime has no pointer to
16a scalar cell, so these functions take a `Bool` ("the pointer is not NULL") and return the value that would be
17stored (`none` when nothing is stored). `deflatePending` stores `*pending` twice when it overflows; the last value
18is returned.
19
20**`deflate` of the gzip header** (`name`, `comment`): the two loops are textually identical except for the field
21`name` / `comment` (and the `gzindex = 0` after the name); one function `gz_string_loop` with a selector serves both.
22-/
23
24namespace Zlib.Deflate
25open C
26open Zlib.Trees («_tr_init» «_tr_flush_bits» «_tr_flush_block» «_tr_stored_block» «_tr_align»)
27open Zlib.Crc32 (crc32 crc32_z)
28
29/-- The z_stream pointer value `Z_NULL`. -/
30abbrev Z_NULL_strm : ZStreamPtr := none
31
32/-- `local int deflateStateCheck(z_streamp strm)` -/
33def deflateStateCheck (strm : ZStreamPtr) : M Int32 := do
34  -- if (strm == Z_NULL || strm->zalloc == (alloc_func)0 || strm->zfree == (free_func)0) return 1;
35  if strm == none then return 1
36  let z ← ldZStream strm
37  if z.zalloc == FnPtr.null || z.zfree == FnPtr.null then return 1
38  -- s = strm->state;
39  let s ← castDeflateState z.state
40  -- if (s == Z_NULL || s->strm != strm || (s->status != INIT_STATE && ... )) return 1;
41  if s == none then return 1
42  let d ← ldDeflateState s
43  if d.strm != strm || (d.status != INIT_STATE && d.status != GZIP_STATE && d.status != EXTRA_STATE &&
44      d.status != NAME_STATE && d.status != COMMENT_STATE && d.status != HCRC_STATE &&
45      d.status != BUSY_STATE && d.status != FINISH_STATE) then return 1
46  return 0
47
48/-- `ERR_RETURN(strm, err)`: `return (strm->msg = ERR_MSG(err), (err))` -/
49def ERR_RETURN (strm : ZStreamPtr) (err : Int32) : M Int32 := do
50  let m ← ERR_MSG err
51  zwr strm (fun z => { z with msg := m })
52  return err
53
54/-- `int ZEXPORT deflateEnd(z_streamp strm)` -/
55def deflateEnd (strm : ZStreamPtr) : M Int32 := do
56  if (← deflateStateCheck strm) != 0 then return Z_STREAM_ERROR
57  let sp ← castDeflateState (← zrd strm (·.state))
58  -- status = strm->state->status;
59  let status ← rd sp (·.status)
60  -- TRY_FREE(strm, strm->state->pending_buf); head; prev; window
61  let pb ← rd sp (·.pending_buf)
62  if pb != .null then ZFREE_bytes strm pb
63  let hd ← rd sp (·.head)
64  if hd != .null then ZFREE_words strm hd
65  let pv ← rd sp (·.prev)
66  if pv != .null then ZFREE_words strm pv
67  let wd ← rd sp (·.window)
68  if wd != .null then ZFREE_bytes strm wd
69  -- ZFREE(strm, strm->state);
70  zfree_default strm
71  freeDeflateState sp
72  -- strm->state = Z_NULL;
73  zwr strm (fun z => { z with state := none })
74  -- return status == BUSY_STATE ? Z_DATA_ERROR : Z_OK;
75  return if status == BUSY_STATE then Z_DATA_ERROR else Z_OK
76
77/-- `int ZEXPORT deflateResetKeep(z_streamp strm)` -/
78def deflateResetKeep (strm : ZStreamPtr) : M Int32 := do
79  if (← deflateStateCheck strm) != 0 then return Z_STREAM_ERROR
80  -- strm->total_in = strm->total_out = 0; strm->msg = Z_NULL; strm->data_type = Z_UNKNOWN;
81  zwr strm (fun z => { z with total_in := 0, total_out := 0, msg := .null, data_type := Z_UNKNOWN })
82  -- s = (deflate_state *)strm->state; s->pending = 0; s->pending_out = s->pending_buf;
83  let s ← castDeflateState (← zrd strm (·.state))
84  wr s (fun d => { d with pending := 0, pending_out := d.pending_buf })
85  -- if (s->wrap < 0) s->wrap = -s->wrap;
86  let d ← ldDeflateState s
87  if d.wrap < 0 then
88    let w ← ineg d.wrap
89    wr s (fun d => { d with wrap := w })
90  -- s->status = s->wrap == 2 ? GZIP_STATE : INIT_STATE;
91  wr s (fun d => { d with status := if d.wrap == 2 then GZIP_STATE else INIT_STATE })
92  -- strm->adler = s->wrap == 2 ? crc32(0L, Z_NULL, 0) : adler32(0L, Z_NULL, 0);
93  let adler ← if (← rd s (·.wrap)) == 2 then crc32 0 (Ptr.null : BPtr) 0 else Zlib.Adler32.adler32 0 (Ptr.null : BPtr) 0
94  zwr strm (fun z => { z with adler })
95  -- s->last_flush = -2; s->gzhead = Z_NULL;
96  wr s (fun d => { d with last_flush := -2, gzhead := none })
97  -- { uInt matches = s->level == 0 ? s->matches : 0; _tr_init(s); s->matches = matches; }
98  let d ← ldDeflateState s
99  let «matches» : UInt32 := if d.level == 0 then d.«matches» else 0
100  _tr_init s
101  wr s (fun d => { d with «matches» := «matches» })
102  -- s->block_start = (long)s->strstart; s->lookahead = 0;
103  -- s->match_length = s->prev_length = MIN_MATCH-1; s->match_available = 0;
104  wr s (fun d => { d with block_start := d.strstart.toUInt64.toInt64, lookahead := 0,
105                          match_length := MIN_MATCH_u - 1, prev_length := MIN_MATCH_u - 1, match_available := 0 })
106  return Z_OK
107
108/-- `local void lm_init(deflate_state *s)` -/
109def lm_init (s : DeflateStatePtr) : M Unit := do
110  -- s->window_size = (ulg)2L*s->w_size;
111  wr s (fun d => { d with window_size := 2 * d.w_size.toUInt64 })
112  CLEAR_HASH s
113  -- s->matches = 0;
114  wr s (fun d => { d with «matches» := 0 })
115  -- s->max_lazy_match = configuration_table[s->level].max_lazy; good_match; nice_match; max_chain_length
116  let c ← config_at (← rd s (·.level))
117  wr s (fun d => { d with max_lazy_match := c.max_lazy.toUInt32, good_match := c.good_length.toUInt32,
118                          nice_match := c.nice_length.toUInt32.toInt32, max_chain_length := c.max_chain.toUInt32 })
119  -- s->strstart = 0; s->block_start = 0L; s->lookahead = 0; s->insert = 0;
120  -- s->match_length = s->prev_length = MIN_MATCH-1; s->match_available = 0; s->ins_h = 0;
121  wr s (fun d => { d with strstart := 0, block_start := 0, lookahead := 0, insert := 0,
122                          match_length := MIN_MATCH_u - 1, prev_length := MIN_MATCH_u - 1,
123                          match_available := 0, ins_h := 0 })
124
125/-- `int ZEXPORT deflateReset(z_streamp strm)` -/
126def deflateReset (strm : ZStreamPtr) : M Int32 := do
127  let ret ← deflateResetKeep strm
128  if ret == Z_OK then lm_init (← castDeflateState (← zrd strm (·.state)))
129  return ret
130
131/-- `int ZEXPORT deflateInit2_(z_streamp strm, int level, int method, int windowBits, int memLevel, int strategy,
132const char *version, int stream_size)` -/
133def deflateInit2_ (strm : ZStreamPtr) (level method windowBits memLevel strategy : Int32) (version : BPtr)
134    (stream_size : Int32) : M Int32 := do
135  let mut level := level
136  let mut windowBits := windowBits
137  let mut wrap : Int32 := 1
138  -- static const char my_version[] = ZLIB_VERSION;  (first character '1')
139  -- if (version == Z_NULL || version[0] != my_version[0] || stream_size != sizeof(z_stream)) return Z_VERSION_ERROR;
140  if version == .null then return Z_VERSION_ERROR
141  if (← load8 version) != 49 || stream_size != sizeof_z_stream then return Z_VERSION_ERROR
142  -- if (strm == Z_NULL) return Z_STREAM_ERROR;
143  if strm == none then return Z_STREAM_ERROR
144  -- strm->msg = Z_NULL;
145  zwr strm (fun z => { z with msg := .null })
146  -- if (strm->zalloc == (alloc_func)0) { strm->zalloc = zcalloc; strm->opaque = (voidpf)0; }
147  if (← zrd strm (·.zalloc)) == FnPtr.null then
148    zwr strm (fun z => { z with zalloc := FnPtr.fn "zcalloc", «opaque» := .null })
149  -- if (strm->zfree == (free_func)0) strm->zfree = zcfree;
150  if (← zrd strm (·.zfree)) == FnPtr.null then
151    zwr strm (fun z => { z with zfree := FnPtr.fn "zcfree" })
152  -- if (level == Z_DEFAULT_COMPRESSION) level = 6;
153  if level == Z_DEFAULT_COMPRESSION then level := 6
154  if windowBits < 0 then
155    -- suppress zlib wrapper
156    wrap := 0
157    if windowBits < -15 then return Z_STREAM_ERROR
158    windowBits ← ineg windowBits
159  else if windowBits > 15 then
160    wrap := 2                                    -- write gzip wrapper instead
161    windowBits ← isub windowBits 16
162  -- if (memLevel < 1 || ... ) return Z_STREAM_ERROR;
163  if memLevel < 1 || memLevel > MAX_MEM_LEVEL || method != Z_DEFLATED ||
164      windowBits < 8 || windowBits > 15 || level < 0 || level > 9 ||
165      strategy < 0 || strategy > Z_FIXED || (windowBits == 8 && wrap != 1) then
166    return Z_STREAM_ERROR
167  -- if (windowBits == 8) windowBits = 9;
168  if windowBits == 8 then windowBits := 9
169  -- s = (deflate_state *) ZALLOC(strm, 1, sizeof(deflate_state)); if (s == Z_NULL) return Z_MEM_ERROR;
170  zalloc_default strm
171  let s ← allocDeflateState
172  if s == none then return Z_MEM_ERROR
173  -- zmemzero(s, sizeof(deflate_state));
174  stDeflateState s DeflateState.zeroed
175  -- strm->state = (struct internal_state FAR *)s; s->strm = strm; s->status = INIT_STATE;
176  zwr strm (fun z => { z with state := StateRef.ofDeflateState s })
177  -- s->wrap = wrap; s->w_bits = (uInt)windowBits; s->w_size = 1 << s->w_bits; s->w_mask = s->w_size - 1;
178  let w_bits : UInt32 := windowBits.toUInt32
179  let w_size : UInt32 := (← ishl 1 w_bits.toNat).toUInt32
180  -- s->hash_bits = (uInt)memLevel + 7; s->hash_size = 1 << s->hash_bits; s->hash_mask = s->hash_size - 1;
181  let hash_bits : UInt32 := memLevel.toUInt32 + 7
182  let hash_size : UInt32 := (← ishl 1 hash_bits.toNat).toUInt32
183  wr s (fun d => { d with strm := strm, status := INIT_STATE, wrap := wrap, w_bits := w_bits, w_size := w_size,
184                          w_mask := w_size - 1, hash_bits := hash_bits, hash_size := hash_size,
185                          hash_mask := hash_size - 1,
186                          -- s->hash_shift = ((s->hash_bits + MIN_MATCH-1) / MIN_MATCH);
187                          hash_shift := (hash_bits + (MIN_MATCH_u - 1)) / MIN_MATCH_u })
188  -- s->window = (Bytef *) ZALLOC(strm, s->w_size, 2*sizeof(Byte));
189  let window ← ZALLOC_bytes strm w_size 2
190  wr s (fun d => { d with window })
191  -- s->prev = (Posf *) ZALLOC(strm, s->w_size, sizeof(Pos));
192  let prev ← ZALLOC_words strm w_size
193  wr s (fun d => { d with prev })
194  -- s->head = (Posf *) ZALLOC(strm, s->hash_size, sizeof(Pos));
195  let head ← ZALLOC_words strm hash_size
196  wr s (fun d => { d with head })
197  -- s->high_water = 0;
198  -- s->lit_bufsize = 1 << (memLevel + 6);
199  let lit_bufsize : UInt32 := (← ishl 1 (← iadd memLevel 6).toInt.toNat).toUInt32
200  wr s (fun d => { d with high_water := 0, lit_bufsize })
201  -- s->pending_buf = (uchf *) ZALLOC(strm, s->lit_bufsize, LIT_BUFS);
202  let pending_buf ← ZALLOC_bytes strm lit_bufsize 4
203  -- s->pending_buf_size = (ulg)s->lit_bufsize * 4;
204  wr s (fun d => { d with pending_buf, pending_buf_size := lit_bufsize.toUInt64 * 4 })
205  -- if (s->window == Z_NULL || s->prev == Z_NULL || s->head == Z_NULL || s->pending_buf == Z_NULL) { ... }
206  if window == .null || prev == .null || head == .null || pending_buf == .null then
207    -- s->status = FINISH_STATE; strm->msg = ERR_MSG(Z_MEM_ERROR); deflateEnd (strm); return Z_MEM_ERROR;
208    wr s (fun d => { d with status := FINISH_STATE })
209    let m ← ERR_MSG Z_MEM_ERROR
210    zwr strm (fun z => { z with msg := m })
211    let _ ← deflateEnd strm
212    return Z_MEM_ERROR
213  -- s->sym_buf = s->pending_buf + s->lit_bufsize; s->sym_end = (s->lit_bufsize - 1) * 3;
214  let sym_buf ← padd pending_buf lit_bufsize.toNat
215  wr s (fun d => { d with sym_buf, sym_end := (lit_bufsize - 1) * 3 })
216  -- s->level = level; s->strategy = strategy; s->method = (Byte)method;
217  wr s (fun d => { d with level, strategy, «method» := method.toUInt32.toUInt8 })
218  -- return deflateReset(strm);
219  deflateReset strm
220
221/-- `int ZEXPORT deflateInit_(z_streamp strm, int level, const char *version, int stream_size)` -/
222def deflateInit_ (strm : ZStreamPtr) (level : Int32) (version : BPtr) (stream_size : Int32) : M Int32 :=
223  deflateInit2_ strm level Z_DEFLATED MAX_WBITS DEF_MEM_LEVEL Z_DEFAULT_STRATEGY version stream_size
224
225/-- `int ZEXPORT deflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)` -/
226def deflateSetDictionary (strm : ZStreamPtr) (dictionary : BPtr) (dictLength : UInt32) : M Int32 := do
227  let mut dictionary := dictionary
228  let mut dictLength := dictLength
229  -- if (deflateStateCheck(strm) || dictionary == Z_NULL) return Z_STREAM_ERROR;
230  if (← deflateStateCheck strm) != 0 || dictionary == .null then return Z_STREAM_ERROR
231  let s ← castDeflateState (← zrd strm (·.state))
232  let d ← ldDeflateState s
233  let wrap := d.wrap
234  -- if (wrap == 2 || (wrap == 1 && s->status != INIT_STATE) || s->lookahead || (wrap == 0 && (long)s->strstart != s->block_start))
235  if wrap == 2 || (wrap == 1 && d.status != INIT_STATE) || d.lookahead != 0 ||
236      (wrap == 0 && d.strstart.toUInt64.toInt64 != d.block_start) then
237    return Z_STREAM_ERROR
238  -- if (wrap == 1) strm->adler = adler32(strm->adler, dictionary, dictLength);
239  if wrap == 1 then
240    let a ← zrd strm (·.adler)
241    let r ← Zlib.Adler32.adler32 a dictionary dictLength
242    zwr strm (fun z => { z with adler := r })
243  -- s->wrap = 0;
244  wr s (fun d => { d with wrap := 0 })
245  -- if (dictLength >= s->w_size) { ... }
246  if dictLength ≥ d.w_size then
247    if wrap == 0 then
248      CLEAR_HASH s
249      wr s (fun d => { d with strstart := 0, block_start := 0, insert := 0 })
250    -- dictionary += dictLength - s->w_size; dictLength = s->w_size;
251    dictionary ← padd dictionary (dictLength - d.w_size).toNat
252    dictLength := d.w_size
253  -- avail = strm->avail_in; next = strm->next_in;
254  let z ← ldZStream strm
255  let avail := z.avail_in
256  let next := z.next_in
257  -- strm->avail_in = dictLength; strm->next_in = (z_const Bytef *)dictionary;
258  zwr strm (fun z => { z with avail_in := dictLength, next_in := dictionary })
259  fill_window s
260  -- while (s->lookahead >= MIN_MATCH) { ... }
261  let _ ← cwhile
262    (fun (u : Unit) => do pure ((← rd s (·.lookahead)) ≥ MIN_MATCH_u, u))
263    (fun (u : Unit) => do
264      let d ← ldDeflateState s
265      let str : UInt32 := d.strstart                            -- str = s->strstart;
266      let n : UInt32 := d.lookahead - (MIN_MATCH_u - 1)         -- n = s->lookahead - (MIN_MATCH-1);
267      -- do { UPDATE_HASH(...); s->prev[str & s->w_mask] = s->head[s->ins_h]; s->head[s->ins_h] = (Pos)str; str++; } while (--n);
268      let (str, _) ← cdoWhile
269        (fun (str, n) => do
270          let d ← ldDeflateState s
271          UPDATE_HASH s (← index8 d.window (str + (MIN_MATCH_u - 1)).toNat)
272          let d ← ldDeflateState s
273          let v ← Ptr.index d.head d.ins_h.toNat
274          Ptr.store (← padd d.prev (str &&& d.w_mask).toNat) v
275          Ptr.store (← padd d.head d.ins_h.toNat) str.toUInt16
276          pure (str + 1, n))
277        (fun (str, n) => let n := n - 1; pure (n != 0, (str, n)))
278        (str, n)
279      -- s->strstart = str; s->lookahead = MIN_MATCH-1; fill_window(s);
280      wr s (fun d => { d with strstart := str, lookahead := MIN_MATCH_u - 1 })
281      fill_window s
282      pure u)
283    ()
284  -- s->strstart += s->lookahead; s->block_start = (long)s->strstart; s->insert = s->lookahead; s->lookahead = 0;
285  wr s (fun d => { d with strstart := d.strstart + d.lookahead })
286  wr s (fun d => { d with block_start := d.strstart.toUInt64.toInt64, insert := d.lookahead, lookahead := 0 })
287  -- s->match_length = s->prev_length = MIN_MATCH-1; s->match_available = 0;
288  wr s (fun d => { d with match_length := MIN_MATCH_u - 1, prev_length := MIN_MATCH_u - 1, match_available := 0 })
289  -- strm->next_in = next; strm->avail_in = avail; s->wrap = wrap;
290  zwr strm (fun z => { z with next_in := next, avail_in := avail })
291  wr s (fun d => { d with wrap })
292  return Z_OK
293
294/-- `int ZEXPORT deflateGetDictionary(z_streamp strm, Bytef *dictionary, uInt *dictLength)`; the second component
295is `*dictLength` when `hasDictLength` (the pointer is not NULL) and `none` otherwise. -/
296def deflateGetDictionary (strm : ZStreamPtr) (dictionary : BPtr) (hasDictLength : Bool) :
297    M (Int32 × Option UInt32) := do
298  if (← deflateStateCheck strm) != 0 then return (Z_STREAM_ERROR, none)
299  let s ← castDeflateState (← zrd strm (·.state))
300  let d ← ldDeflateState s
301  -- len = s->strstart + s->lookahead; if (len > s->w_size) len = s->w_size;
302  let mut len : UInt32 := d.strstart + d.lookahead
303  if len > d.w_size then len := d.w_size
304  -- if (dictionary != Z_NULL && len) zmemcpy(dictionary, s->window + s->strstart + s->lookahead - len, len);
305  if dictionary != .null && len != 0 then
306    let from_ ← padd (← padd d.window d.strstart.toNat) d.lookahead.toNat
307    memcpyB dictionary (← psub from_ len.toNat) len.toNat
308  -- if (dictLength != Z_NULL) *dictLength = len;
309  return (Z_OK, if hasDictLength then some len else none)
310
311/-- `int ZEXPORT deflateSetHeader(z_streamp strm, gz_headerp head)` -/
312def deflateSetHeader (strm : ZStreamPtr) (head : GzHeaderPtr) : M Int32 := do
313  if (← deflateStateCheck strm) != 0 then return Z_STREAM_ERROR
314  let s ← castDeflateState (← zrd strm (·.state))
315  if (← rd s (·.wrap)) != 2 then return Z_STREAM_ERROR
316  wr s (fun d => { d with gzhead := head })
317  return Z_OK
318
319/-- `int ZEXPORT deflatePending(z_streamp strm, unsigned *pending, int *bits)`; the results are the values stored
320through `pending` and `bits` (when the pointer is not NULL). -/
321def deflatePending (strm : ZStreamPtr) (hasPending hasBits : Bool) :
322    M (Int32 × Option UInt32 × Option Int32) := do
323  if (← deflateStateCheck strm) != 0 then return (Z_STREAM_ERROR, none, none)
324  let s ← castDeflateState (← zrd strm (·.state))
325  let d ← ldDeflateState s
326  -- if (bits != Z_NULL) *bits = strm->state->bi_valid;
327  let bits := if hasBits then some d.bi_valid else none
328  if hasPending then
329    -- *pending = (unsigned)strm->state->pending;
330    let p : UInt32 := d.pending.toUInt32
331    -- if (*pending != strm->state->pending) { *pending = (unsigned)-1; return Z_BUF_ERROR; }
332    if p.toUInt64 != d.pending then return (Z_BUF_ERROR, some 0xffffffff, bits)
333    return (Z_OK, some p, bits)
334  return (Z_OK, none, bits)
335
336/-- `int ZEXPORT deflateUsed(z_streamp strm, int *bits)` -/
337def deflateUsed (strm : ZStreamPtr) (hasBits : Bool) : M (Int32 × Option Int32) := do
338  if (← deflateStateCheck strm) != 0 then return (Z_STREAM_ERROR, none)
339  let s ← castDeflateState (← zrd strm (·.state))
340  let d ← ldDeflateState s
341  return (Z_OK, if hasBits then some d.bi_used else none)
342
343/-- `int ZEXPORT deflatePrime(z_streamp strm, int bits, int value)` -/
344def deflatePrime (strm : ZStreamPtr) (bits value : Int32) : M Int32 := do
345  let mut bits := bits
346  let mut value := value
347  if (← deflateStateCheck strm) != 0 then return Z_STREAM_ERROR
348  let s ← castDeflateState (← zrd strm (·.state))
349  -- if (bits < 0 || bits > 16) return Z_BUF_ERROR;
350  if bits < 0 || bits > 16 then return Z_BUF_ERROR
351  -- if (s->pending_out != s->pending_buf) { ... move partially flushed pending output to buffer start }
352  let d ← ldDeflateState s
353  if d.pending_out != d.pending_buf then
354    -- Bytef *to = s->pending_buf, *from = s->pending_out; ulg n = s->pending; while (n--) *to++ = *from++;
355    let _ ← cwhile
356      (fun (n, to, from_) => pure (n != 0, (n - 1, to, from_)))
357      (fun (n, to, from_) => do
358        store8 to (← load8 from_)
359        pure (n, ← padd to 1, ← padd from_ 1))
360      (d.pending, d.pending_buf, d.pending_out)
361    wr s (fun d => { d with pending_out := d.pending_buf })
362  -- need = (s->bi_valid + bits) >> 3;
363  let d ← ldDeflateState s
364  let need : Int32 := (← iadd d.bi_valid bits) >>> 3
365  -- if (s->pending_buf_size - s->pending < (ulg)need) return Z_BUF_ERROR;
366  if d.pending_buf_size - d.pending < need.toInt64.toUInt64 then return Z_BUF_ERROR
367  -- do { ... } while (bits);
368  let (_, _) ← cdoWhile
369    (fun (bits, value) => do
370      let d ← ldDeflateState s
371      -- put = Buf_size - s->bi_valid; if (put > bits) put = bits;
372      let mut put ← isub Buf_size d.bi_valid
373      if put > bits then put := bits
374      -- s->bi_buf |= (ush)((value & ((1 << put) - 1)) << s->bi_valid);
375      let mask ← isub (← ishl 1 put.toInt) 1
376      let sh ← ishl (value &&& mask) d.bi_valid.toInt
377      wr s (fun d => { d with bi_buf := d.bi_buf ||| sh.toInt16.toUInt16 })
378      -- s->bi_valid += put;
379      let bv ← iadd d.bi_valid put
380      wr s (fun d => { d with bi_valid := bv })
381      -- _tr_flush_bits(s);
382      _tr_flush_bits s
383      -- value >>= put; bits -= put;
384      pure (← isub bits put, value >>> put))
385    (fun (bits, value) => pure (bits != 0, (bits, value)))
386    (bits, value)
387  return Z_OK
388
389/-- `HCRC_UPDATE(beg)`: `if (s->gzhead->hcrc && s->pending > (beg)) strm->adler = crc32_z(strm->adler,
390s->pending_buf + (beg), s->pending - (beg));` -/
391def HCRC_UPDATE (strm : ZStreamPtr) (s : DeflateStatePtr) (beg : UInt64) : M Unit := do
392  let d ← ldDeflateState s
393  let gh ← ldGzHeader d.gzhead
394  if gh.hcrc != 0 && d.pending > beg then
395    let a ← zrd strm (·.adler)
396    let r ← crc32_z a (← padd d.pending_buf beg.toNat) (d.pending - beg)
397    zwr strm (fun z => { z with adler := r })
398
399/-- State of the loop that copies the gzip `extra` field. -/
400structure ExtraS where
401  beg : UInt64
402  left : UInt64
403  ret : Bool
404
405/-- State of the `do { ... } while (val != 0)` loops that copy the gzip name and comment. -/
406structure StrS where
407  beg : UInt64
408  val : Int32
409  ret : Bool
410
411/-- The `NAME_STATE` and `COMMENT_STATE` loops of `deflate`: `ulg beg = s->pending; int val; do { if (s->pending ==
412s->pending_buf_size) { HCRC_UPDATE(beg); flush_pending(strm); if (s->pending != 0) { s->last_flush = -1; return Z_OK; }
413beg = 0; } val = s->gzhead->name[s->gzindex++]; put_byte(s, val); } while (val != 0); HCRC_UPDATE(beg);`
414(`sel` selects `name` or `comment`). Returns `true` if the C returns `Z_OK` from inside the loop. -/
415def gz_string_loop (strm : ZStreamPtr) (s : DeflateStatePtr) (sel : GzHeader → BPtr) : M Bool := do
416  let beg ← rd s (·.pending)
417  let st ← cdoWhile
418    (fun (st : StrS) => do
419      let mut beg := st.beg
420      let d ← ldDeflateState s
421      if d.pending == d.pending_buf_size then
422        HCRC_UPDATE strm s beg
423        flush_pending strm
424        if (← rd s (·.pending)) != 0 then
425          wr s (fun d => { d with last_flush := -1 })
426          return { st with ret := true }
427        beg := 0
428      let d ← ldDeflateState s
429      let gh ← ldGzHeader d.gzhead
430      -- val = s->gzhead->name[s->gzindex++];
431      let b ← index8 (sel gh) d.gzindex.toNat
432      wr s (fun d => { d with gzindex := d.gzindex + 1 })
433      put_byte s b
434      pure { st with beg, val := b.toUInt32.toInt32 })
435    (fun st => pure (!st.ret && st.val != 0, st))
436    { beg, val := 0, ret := false }
437  if st.ret then return true
438  HCRC_UPDATE strm s st.beg
439  return false
440
441/-- `RANK(f)`: `(((f) * 2) - ((f) > 4 ? 9 : 0))` -/
442def RANK (f : Int32) : M Int32 := do
443  isub (← chk32 (f.toInt * 2)) (if f > 4 then 9 else 0)
444
445/-- `int ZEXPORT deflate(z_streamp strm, int flush)` -/
446def deflate (strm : ZStreamPtr) (flush : Int32) : M Int32 := do
447  -- if (deflateStateCheck(strm) || flush > Z_BLOCK || flush < 0) return Z_STREAM_ERROR;
448  if (← deflateStateCheck strm) != 0 || flush > Z_BLOCK || flush < 0 then return Z_STREAM_ERROR
449  -- s = strm->state;
450  let s ← castDeflateState (← zrd strm (·.state))
451  let z ← ldZStream strm
452  let d ← ldDeflateState s
453  -- if (strm->next_out == Z_NULL || (strm->avail_in != 0 && strm->next_in == Z_NULL) || (s->status == FINISH_STATE && flush != Z_FINISH))
454  if z.next_out == .null || (z.avail_in != 0 && z.next_in == .null) ||
455      (d.status == FINISH_STATE && flush != Z_FINISH) then
456    return ← ERR_RETURN strm Z_STREAM_ERROR
457  -- if (strm->avail_out == 0) ERR_RETURN(strm, Z_BUF_ERROR);
458  if z.avail_out == 0 then return ← ERR_RETURN strm Z_BUF_ERROR
459  -- old_flush = s->last_flush; s->last_flush = flush;
460  let old_flush := d.last_flush
461  wr s (fun d => { d with last_flush := flush })
462  -- Flush as much pending output as possible
463  if d.pending != 0 then
464    flush_pending strm
465    if (← zrd strm (·.avail_out)) == 0 then
466      wr s (fun d => { d with last_flush := -1 })
467      return Z_OK
468  else if z.avail_in == 0 && (← RANK flush) ≤ (← RANK old_flush) && flush != Z_FINISH then
469    return ← ERR_RETURN strm Z_BUF_ERROR
470  -- if (s->status == FINISH_STATE && strm->avail_in != 0) ERR_RETURN(strm, Z_BUF_ERROR);
471  if (← rd s (·.status)) == FINISH_STATE && (← zrd strm (·.avail_in)) != 0 then
472    return ← ERR_RETURN strm Z_BUF_ERROR
473  -- Write the header
474  if (← rd s (·.status)) == INIT_STATE && (← rd s (·.wrap)) == 0 then
475    wr s (fun d => { d with status := BUSY_STATE })
476  if (← rd s (·.status)) == INIT_STATE then
477    -- zlib header: uInt header = (Z_DEFLATED + ((s->w_bits - 8) << 4)) << 8;
478    let d ← ldDeflateState s
479    let mut header : UInt32 := ((8 : UInt32) + ((d.w_bits - 8) <<< 4)) <<< 8
480    -- level_flags
481    let level_flags : UInt32 :=
482      if d.strategy ≥ Z_HUFFMAN_ONLY || d.level < 2 then 0
483      else if d.level < 6 then 1
484      else if d.level == 6 then 2
485      else 3
486    header := header ||| (level_flags <<< 6)                  -- header |= (level_flags << 6);
487    if d.strstart != 0 then header := header ||| 0x20          -- header |= PRESET_DICT;
488    header := header + (31 - (header % 31))                    -- header += 31 - (header % 31);
489    putShortMSB s header
490    -- Save the adler32 of the preset dictionary:
491    if (← rd s (·.strstart)) != 0 then
492      let a ← zrd strm (·.adler)
493      putShortMSB s (a >>> 16).toUInt32
494      putShortMSB s (a &&& 0xffff).toUInt32
495    -- strm->adler = adler32(0L, Z_NULL, 0); s->status = BUSY_STATE;
496    let r ← Zlib.Adler32.adler32 0 (Ptr.null : BPtr) 0
497    zwr strm (fun z => { z with adler := r })
498    wr s (fun d => { d with status := BUSY_STATE })
499    -- Compression must start with an empty pending buffer
500    flush_pending strm
501    if (← rd s (·.pending)) != 0 then
502      wr s (fun d => { d with last_flush := -1 })
503      return Z_OK
504  -- #ifdef GZIP
505  if (← rd s (·.status)) == GZIP_STATE then
506    -- gzip header: strm->adler = crc32(0L, Z_NULL, 0);
507    let r ← crc32 0 (Ptr.null : BPtr) 0
508    zwr strm (fun z => { z with adler := r })
509    put_byte s 31
510    put_byte s 139
511    put_byte s 8
512    let d ← ldDeflateState s
513    -- the XFL byte: s->level == 9 ? 2 : (s->strategy >= Z_HUFFMAN_ONLY || s->level < 2 ? 4 : 0)
514    let xfl : UInt8 := if d.level == 9 then 2 else if d.strategy ≥ Z_HUFFMAN_ONLY || d.level < 2 then 4 else 0
515    if d.gzhead == none then
516      put_byte s 0
517      put_byte s 0
518      put_byte s 0
519      put_byte s 0
520      put_byte s 0
521      put_byte s xfl
522      put_byte s OS_CODE.toUInt32.toUInt8
523      wr s (fun d => { d with status := BUSY_STATE })
524      -- Compression must start with an empty pending buffer
525      flush_pending strm
526      if (← rd s (·.pending)) != 0 then
527        wr s (fun d => { d with last_flush := -1 })
528        return Z_OK
529    else
530      let gh ← ldGzHeader d.gzhead
531      -- put_byte(s, (text ? 1 : 0) + (hcrc ? 2 : 0) + (extra == NULL ? 0 : 4) + (name == NULL ? 0 : 8) + (comment == NULL ? 0 : 16));
532      -- (each term is a constant, so the sum is at most 31 and cannot overflow)
533      put_byte s (((if gh.text != 0 then 1 else 0) + (if gh.hcrc != 0 then 2 else 0) +
534        (if gh.extra == .null then 0 else 4) + (if gh.name == .null then 0 else 8) +
535        (if gh.comment == .null then 0 else 16) : Nat).toUInt8)
536      put_byte s (gh.time &&& 0xff).toUInt8
537      put_byte s ((gh.time >>> 8) &&& 0xff).toUInt8
538      put_byte s ((gh.time >>> 16) &&& 0xff).toUInt8
539      put_byte s ((gh.time >>> 24) &&& 0xff).toUInt8
540      put_byte s xfl
541      put_byte s (gh.os &&& 0xff).toUInt32.toUInt8
542      if gh.extra != .null then
543        put_byte s (gh.extra_len &&& 0xff).toUInt8
544        put_byte s ((gh.extra_len >>> 8) &&& 0xff).toUInt8
545      if gh.hcrc != 0 then
546        -- strm->adler = crc32_z(strm->adler, s->pending_buf, s->pending);
547        let d ← ldDeflateState s
548        let a ← zrd strm (·.adler)
549        let r ← crc32_z a d.pending_buf d.pending
550        zwr strm (fun z => { z with adler := r })
551      -- s->gzindex = 0; s->status = EXTRA_STATE;
552      wr s (fun d => { d with gzindex := 0, status := EXTRA_STATE })
553  if (← rd s (·.status)) == EXTRA_STATE then
554    let d ← ldDeflateState s
555    let gh ← ldGzHeader d.gzhead
556    if gh.extra != .null then
557      -- ulg beg = s->pending; ulg left = (s->gzhead->extra_len & 0xffff) - s->gzindex;
558      let st ← cwhile
559        (fun (st : ExtraS) => do
560          let d ← ldDeflateState s
561          pure (!st.ret && d.pending + st.left > d.pending_buf_size, st))
562        (fun (st : ExtraS) => do
563          let d ← ldDeflateState s
564          let gh ← ldGzHeader d.gzhead
565          -- ulg copy = s->pending_buf_size - s->pending;
566          let copy := d.pending_buf_size - d.pending
567          -- zmemcpy(s->pending_buf + s->pending, s->gzhead->extra + s->gzindex, copy);
568          memcpyB (← padd d.pending_buf d.pending.toNat) (← padd gh.extra d.gzindex.toNat) copy.toNat
569          -- s->pending = s->pending_buf_size; HCRC_UPDATE(beg); s->gzindex += copy;
570          wr s (fun d => { d with pending := d.pending_buf_size })
571          HCRC_UPDATE strm s st.beg
572          wr s (fun d => { d with gzindex := d.gzindex + copy })
573          flush_pending strm
574          if (← rd s (·.pending)) != 0 then
575            wr s (fun d => { d with last_flush := -1 })
576            return { st with ret := true }
577          -- beg = 0; left -= copy;
578          pure { st with beg := 0, left := st.left - copy })
579        { beg := d.pending, left := (gh.extra_len &&& 0xffff).toUInt64 - d.gzindex, ret := false }
580      if st.ret then return Z_OK
581      -- zmemcpy(s->pending_buf + s->pending, s->gzhead->extra + s->gzindex, left);
582      let d ← ldDeflateState s
583      let gh ← ldGzHeader d.gzhead
584      memcpyB (← padd d.pending_buf d.pending.toNat) (← padd gh.extra d.gzindex.toNat) st.left.toNat
585      -- s->pending += left; HCRC_UPDATE(beg); s->gzindex = 0;
586      wr s (fun d => { d with pending := d.pending + st.left })
587      HCRC_UPDATE strm s st.beg
588      wr s (fun d => { d with gzindex := 0 })
589    wr s (fun d => { d with status := NAME_STATE })
590  if (← rd s (·.status)) == NAME_STATE then
591    let d ← ldDeflateState s
592    let gh ← ldGzHeader d.gzhead
593    if gh.name != .null then
594      if (← gz_string_loop strm s (·.name)) then return Z_OK
595      wr s (fun d => { d with gzindex := 0 })
596    wr s (fun d => { d with status := COMMENT_STATE })
597  if (← rd s (·.status)) == COMMENT_STATE then
598    let d ← ldDeflateState s
599    let gh ← ldGzHeader d.gzhead
600    if gh.comment != .null then
601      if (← gz_string_loop strm s (·.comment)) then return Z_OK
602    wr s (fun d => { d with status := HCRC_STATE })
603  if (← rd s (·.status)) == HCRC_STATE then
604    let d ← ldDeflateState s
605    let gh ← ldGzHeader d.gzhead
606    if gh.hcrc != 0 then
607      -- if (s->pending + 2 > s->pending_buf_size) { flush_pending(strm); if (s->pending != 0) {...return Z_OK;} }
608      if d.pending + 2 > d.pending_buf_size then
609        flush_pending strm
610        if (← rd s (·.pending)) != 0 then
611          wr s (fun d => { d with last_flush := -1 })
612          return Z_OK
613      let a ← zrd strm (·.adler)
614      put_byte s (a &&& 0xff).toUInt8
615      put_byte s ((a >>> 8) &&& 0xff).toUInt8
616      let r ← crc32 0 (Ptr.null : BPtr) 0
617      zwr strm (fun z => { z with adler := r })
618    wr s (fun d => { d with status := BUSY_STATE })
619    -- Compression must start with an empty pending buffer
620    flush_pending strm
621    if (← rd s (·.pending)) != 0 then
622      wr s (fun d => { d with last_flush := -1 })
623      return Z_OK
624  -- Start a new block or continue the current one.
625  let d ← ldDeflateState s
626  if (← zrd strm (·.avail_in)) != 0 || d.lookahead != 0 || (flush != Z_NO_FLUSH && d.status != FINISH_STATE) then
627    -- bstate = s->level == 0 ? deflate_stored(s, flush) : s->strategy == Z_HUFFMAN_ONLY ? deflate_huff(s, flush) :
628    --          s->strategy == Z_RLE ? deflate_rle(s, flush) : (*(configuration_table[s->level].func))(s, flush);
629    let bstate : block_state ←
630      if d.level == 0 then deflate_stored s flush
631      else if d.strategy == Z_HUFFMAN_ONLY then deflate_huff s flush
632      else if d.strategy == Z_RLE then deflate_rle s flush
633      else do
634        match (← config_at d.level).func with
635        | .stored => deflate_stored s flush
636        | .fast => deflate_fast s flush
637        | .slow => deflate_slow s flush
638    -- if (bstate == finish_started || bstate == finish_done) s->status = FINISH_STATE;
639    if bstate == finish_started || bstate == finish_done then
640      wr s (fun d => { d with status := FINISH_STATE })
641    -- if (bstate == need_more || bstate == finish_started) { if (strm->avail_out == 0) s->last_flush = -1; return Z_OK; }
642    if bstate == need_more || bstate == finish_started then
643      if (← zrd strm (·.avail_out)) == 0 then
644        wr s (fun d => { d with last_flush := -1 })
645      return Z_OK
646    if bstate == block_done then
647      if flush == Z_PARTIAL_FLUSH then
648        _tr_align s
649      else if flush != Z_BLOCK then
650        -- FULL_FLUSH or SYNC_FLUSH
651        _tr_stored_block s (Ptr.null : BPtr) 0 0
652        if flush == Z_FULL_FLUSH then
653          CLEAR_HASH s                                        -- forget history
654          if (← rd s (·.lookahead)) == 0 then
655            wr s (fun d => { d with strstart := 0, block_start := 0, insert := 0 })
656      flush_pending strm
657      if (← zrd strm (·.avail_out)) == 0 then
658        wr s (fun d => { d with last_flush := -1 })
659        return Z_OK
660  -- if (flush != Z_FINISH) return Z_OK; if (s->wrap <= 0) return Z_STREAM_END;
661  if flush != Z_FINISH then return Z_OK
662  if (← rd s (·.wrap)) ≤ 0 then return Z_STREAM_END
663  -- Write the trailer
664  if (← rd s (·.wrap)) == 2 then
665    let a ← zrd strm (·.adler)
666    put_byte s (a &&& 0xff).toUInt8
667    put_byte s ((a >>> 8) &&& 0xff).toUInt8
668    put_byte s ((a >>> 16) &&& 0xff).toUInt8
669    put_byte s ((a >>> 24) &&& 0xff).toUInt8
670    let t ← zrd strm (·.total_in)
671    put_byte s (t &&& 0xff).toUInt8
672    put_byte s ((t >>> 8) &&& 0xff).toUInt8
673    put_byte s ((t >>> 16) &&& 0xff).toUInt8
674    put_byte s ((t >>> 24) &&& 0xff).toUInt8
675  else
676    let a ← zrd strm (·.adler)
677    putShortMSB s (a >>> 16).toUInt32
678    putShortMSB s (a &&& 0xffff).toUInt32
679  flush_pending strm
680  -- if (s->wrap > 0) s->wrap = -s->wrap; /* write the trailer only once! */
681  let w ← rd s (·.wrap)
682  if w > 0 then
683    let nw ← ineg w
684    wr s (fun d => { d with wrap := nw })
685  -- return s->pending != 0 ? Z_OK : Z_STREAM_END;
686  return if (← rd s (·.pending)) != 0 then Z_OK else Z_STREAM_END
687
688/-- `int ZEXPORT deflateParams(z_streamp strm, int level, int strategy)` -/
689def deflateParams (strm : ZStreamPtr) (level strategy : Int32) : M Int32 := do
690  let mut level := level
691  if (← deflateStateCheck strm) != 0 then return Z_STREAM_ERROR
692  let s ← castDeflateState (← zrd strm (·.state))
693  -- if (level == Z_DEFAULT_COMPRESSION) level = 6;
694  if level == Z_DEFAULT_COMPRESSION then level := 6
695  -- if (level < 0 || level > 9 || strategy < 0 || strategy > Z_FIXED) return Z_STREAM_ERROR;
696  if level < 0 || level > 9 || strategy < 0 || strategy > Z_FIXED then return Z_STREAM_ERROR
697  -- func = configuration_table[s->level].func;
698  let d ← ldDeflateState s
699  let func := (← config_at d.level).func
700  -- if ((strategy != s->strategy || func != configuration_table[level].func) && s->last_flush != -2) { ... }
701  let differs ← if strategy != d.strategy then pure true else do
702    pure (func != (← config_at level).func)
703  if differs && d.last_flush != -2 then
704    -- Flush the last buffer:
705    let err ← deflate strm Z_BLOCK
706    if err == Z_STREAM_ERROR then return err
707    -- if (strm->avail_in || (s->strstart - s->block_start) + s->lookahead) return Z_BUF_ERROR;
708    let d ← ldDeflateState s
709    let diff ← lsub d.strstart.toUInt64.toInt64 d.block_start
710    let tot ← ladd diff d.lookahead.toUInt64.toInt64
711    if (← zrd strm (·.avail_in)) != 0 || tot != 0 then return Z_BUF_ERROR
712  -- if (s->level != level) { ... }
713  let d ← ldDeflateState s
714  if d.level != level then
715    if d.level == 0 && d.«matches» != 0 then
716      if d.«matches» == 1 then slide_hash s else CLEAR_HASH s
717      wr s (fun d => { d with «matches» := 0 })
718    -- s->level = level; s->max_lazy_match = ...; good_match; nice_match; max_chain_length
719    let c ← config_at level
720    wr s (fun d => { d with level := level, max_lazy_match := c.max_lazy.toUInt32, good_match := c.good_length.toUInt32,
721                            nice_match := c.nice_length.toUInt32.toInt32, max_chain_length := c.max_chain.toUInt32 })
722  -- s->strategy = strategy;
723  wr s (fun d => { d with strategy })
724  return Z_OK
725
726/-- `int ZEXPORT deflateTune(z_streamp strm, int good_length, int max_lazy, int nice_length, int max_chain)` -/
727def deflateTune (strm : ZStreamPtr) (good_length max_lazy nice_length max_chain : Int32) : M Int32 := do
728  if (← deflateStateCheck strm) != 0 then return Z_STREAM_ERROR
729  let s ← castDeflateState (← zrd strm (·.state))
730  wr s (fun d => { d with good_match := good_length.toUInt32, max_lazy_match := max_lazy.toUInt32,
731                          nice_match := nice_length, max_chain_length := max_chain.toUInt32 })
732  return Z_OK
733
734/-- `z_size_t ZEXPORT deflateBound_z(z_streamp strm, z_size_t sourceLen)` -/
735def deflateBound_z (strm : ZStreamPtr) (sourceLen : UInt64) : M UInt64 := do
736  -- fixedlen = sourceLen + (sourceLen >> 3) + (sourceLen >> 8) + (sourceLen >> 9) + 4;
737  let mut fixedlen : UInt64 := sourceLen + (sourceLen >>> 3) + (sourceLen >>> 8) + (sourceLen >>> 9) + 4
738  if fixedlen < sourceLen then fixedlen := 0xffffffffffffffff
739  -- storelen = sourceLen + (sourceLen >> 5) + (sourceLen >> 7) + (sourceLen >> 11) + 7;
740  let mut storelen : UInt64 := sourceLen + (sourceLen >>> 5) + (sourceLen >>> 7) + (sourceLen >>> 11) + 7
741  if storelen < sourceLen then storelen := 0xffffffffffffffff
742  -- if (deflateStateCheck(strm)) { bound = max(fixedlen, storelen); return bound + 18 < bound ? -1 : bound + 18; }
743  if (← deflateStateCheck strm) != 0 then
744    let bound := if fixedlen > storelen then fixedlen else storelen
745    return if bound + 18 < bound then 0xffffffffffffffff else bound + 18
746  let s ← castDeflateState (← zrd strm (·.state))
747  let d ← ldDeflateState s
748  -- switch (s->wrap < 0 ? -s->wrap : s->wrap)
749  let w ← if d.wrap < 0 then ineg d.wrap else pure d.wrap
750  let mut wraplen : UInt64 := 18
751  if w == 0 then
752    wraplen := 0                                                 -- raw deflate
753  else if w == 1 then
754    wraplen := 6 + (if d.strstart != 0 then 4 else 0)           -- zlib wrapper
755  else if w == 2 then
756    wraplen := 18                                                -- gzip wrapper
757    if d.gzhead != none then
758      let gh ← ldGzHeader d.gzhead
759      -- if (s->gzhead->extra != Z_NULL) wraplen += 2 + s->gzhead->extra_len;  (2 + uInt is computed in unsigned)
760      if gh.extra != .null then wraplen := wraplen + ((2 : UInt32) + gh.extra_len).toUInt64
761      -- str = s->gzhead->name; if (str != Z_NULL) do { wraplen++; } while (*str++);
762      if gh.name != .null then
763        let (wl, _) ← cdoWhile
764          (fun (wl, str) => pure (wl + 1, str))
765          (fun (wl, str) => do
766            let b ← load8 str
767            pure (b != 0, (wl, ← padd str 1)))
768          (wraplen, gh.name)
769        wraplen := wl
770      if gh.comment != .null then
771        let (wl, _) ← cdoWhile
772          (fun (wl, str) => pure (wl + 1, str))
773          (fun (wl, str) => do
774            let b ← load8 str
775            pure (b != 0, (wl, ← padd str 1)))
776          (wraplen, gh.comment)
777        wraplen := wl
778      -- if (s->gzhead->hcrc) wraplen += 2;
779      if gh.hcrc != 0 then wraplen := wraplen + 2
780  else
781    wraplen := 18                                                -- for compiler happiness
782  -- if (s->w_bits != 15 || s->hash_bits != 8 + 7) { ... }
783  if d.w_bits != 15 || d.hash_bits != 15 then
784    let bound := if d.w_bits ≤ d.hash_bits && d.level != 0 then fixedlen else storelen
785    return if bound + wraplen < bound then 0xffffffffffffffff else bound + wraplen
786  -- bound = sourceLen + (sourceLen >> 12) + (sourceLen >> 14) + (sourceLen >> 25) + 13 - 6 + wraplen;
787  let bound : UInt64 := sourceLen + (sourceLen >>> 12) + (sourceLen >>> 14) + (sourceLen >>> 25) + 13 - 6 + wraplen
788  return if bound < sourceLen then 0xffffffffffffffff else bound
789
790/-- `uLong ZEXPORT deflateBound(z_streamp strm, uLong sourceLen)` -/
791def deflateBound (strm : ZStreamPtr) (sourceLen : UInt64) : M UInt64 := do
792  let bound ← deflateBound_z strm sourceLen
793  -- return (uLong)bound != bound ? (uLong)-1 : (uLong)bound;   (uLong and z_size_t are both 64 bits)
794  return bound
795
796/-- `int ZEXPORT deflateCopy(z_streamp dest, z_streamp source)` (the `MAXSEG_64K` branch is not compiled; `LIT_MEM`
797is undefined). -/
798def deflateCopy (dest source : ZStreamPtr) : M Int32 := do
799  -- if (dest == Z_NULL) return Z_STREAM_ERROR;
800  if dest == none then return Z_STREAM_ERROR
801  -- if (deflateStateCheck(source)) { dest->state = Z_NULL; return Z_STREAM_ERROR; }
802  if (← deflateStateCheck source) != 0 then
803    zwr dest (fun z => { z with state := none })
804    return Z_STREAM_ERROR
805  -- ss = source->state;
806  let ss ← castDeflateState (← zrd source (·.state))
807  -- ds = (deflate_state *) ZALLOC(source, 1, sizeof(deflate_state));
808  zalloc_default source
809  let ds ← allocDeflateState
810  if ds == none then
811    zwr dest (fun z => { z with state := none })
812    return Z_MEM_ERROR
813  -- zmemcpy(ds, ss, sizeof(deflate_state));
814  copyDeflateState ds ss
815  -- ds->window = ZALLOC(source, ds->w_size, 2*sizeof(Byte)); ds->prev = ...; ds->head = ...; ds->pending_buf = ...
816  let dd ← ldDeflateState ds
817  let window ← ZALLOC_bytes source dd.w_size 2
818  wr ds (fun d => { d with window })
819  let prev ← ZALLOC_words source dd.w_size
820  wr ds (fun d => { d with prev })
821  let head ← ZALLOC_words source dd.hash_size
822  wr ds (fun d => { d with head })
823  let pending_buf ← ZALLOC_bytes source dd.lit_bufsize 4
824  wr ds (fun d => { d with pending_buf })
825  if window == .null || prev == .null || head == .null || pending_buf == .null then
826    -- TRY_FREE(source, ds->pending_buf); head; prev; window; ZFREE(source, ds);
827    if pending_buf != .null then ZFREE_bytes source pending_buf
828    if head != .null then ZFREE_words source head
829    if prev != .null then ZFREE_words source prev
830    if window != .null then ZFREE_bytes source window
831    zfree_default source
832    freeDeflateState ds
833    zwr dest (fun z => { z with state := none })
834    return Z_MEM_ERROR
835  -- zmemcpy(dest, source, sizeof(z_stream)); dest->state = (struct internal_state FAR *) ds; ds->strm = dest;
836  -- (memcpy of overlapping objects is undefined when dest == source)
837  copyZStream dest source
838  zwr dest (fun z => { z with state := StateRef.ofDeflateState ds })
839  wr ds (fun d => { d with strm := dest })
840  -- zmemcpy(ds->window, ss->window, ss->high_water);
841  let sd ← ldDeflateState ss
842  memcpyB window sd.window sd.high_water.toNat
843  -- zmemcpy(ds->prev, ss->prev, (ss->slid || ss->strstart - ss->insert > ds->w_size ? ds->w_size : ss->strstart - ss->insert) * sizeof(Pos));
844  -- (the byte count is twice the number of 16-bit words)
845  let cnt : UInt32 := if sd.slid != 0 || sd.strstart - sd.insert > dd.w_size then dd.w_size else sd.strstart - sd.insert
846  Ptr.memcpy prev sd.prev cnt.toNat
847  -- zmemcpy(ds->head, ss->head, ds->hash_size * sizeof(Pos));
848  Ptr.memcpy head sd.head dd.hash_size.toNat
849  -- ds->pending_out = ds->pending_buf + (ss->pending_out - ss->pending_buf);
850  let off ← Ptr.diff sd.pending_out sd.pending_buf
851  let pending_out ← Ptr.add pending_buf off.toInt
852  wr ds (fun d => { d with pending_out })
853  -- zmemcpy(ds->pending_out, ss->pending_out, ss->pending);
854  memcpyB pending_out sd.pending_out sd.pending.toNat
855  -- ds->sym_buf = ds->pending_buf + ds->lit_bufsize; zmemcpy(ds->sym_buf, ss->sym_buf, ss->sym_next);
856  let sym_buf ← padd pending_buf dd.lit_bufsize.toNat
857  wr ds (fun d => { d with sym_buf })
858  memcpyB sym_buf sd.sym_buf sd.sym_next.toNat
859  -- ds->l_desc.dyn_tree = ds->dyn_ltree; ds->d_desc.dyn_tree = ds->dyn_dtree; ds->bl_desc.dyn_tree = ds->bl_tree;
860  match ds with
861  | none => ub "null deflate_state"
862  | some (.tab id) =>
863    wr ds (fun d => { d with
864      l_desc := { d.l_desc with dyn_tree := .ref (.dstate_dyn_ltree id) 0 },
865      d_desc := { d.d_desc with dyn_tree := .ref (.dstate_dyn_dtree id) 0 },
866      bl_desc := { d.bl_desc with dyn_tree := .ref (.dstate_bl_tree id) 0 } })
867  return Z_OK
868
869end Zlib.Deflate