deflate_base.c.lean

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

1import ZlibF.Runtime.Alloc
2import ZlibF.Runtime.Tables
3import ZlibF.Zlib.«adler32.c»
4import ZlibF.Zlib.«zutil.c»
5import ZlibF.Zlib.«trees.c»
6import ZlibF.Zlib.«crc32.c»
7
8/-!
9# deflate.c, part 1: shared definitions, hash macros, `slide_hash`, `read_buf`, `fill_window`, `flush_pending`
10
11Source: `deflate.c` and `deflate.h` of the verified source (no patch touches them), default x86_64 Linux build
12(LP64; `GZIP` defined; `LIT_MEM`, `FASTEST`, `UNALIGNED_OK`, `ZLIB_DEBUG`, `Z_SOLO` undefined). The other parts of
13the file are `deflate_strategies.c.lean` (`longest_match`, `deflate_stored`, `deflate_fast`, `deflate_slow`,
14`deflate_rle`, `deflate_huff`) and `deflate.c.lean` (the public functions).
15
16Decisions (each is also marked where it is used):
17
18* A `deflate_state *` is a `DeflateStatePtr`, a `z_streamp` a `ZStreamPtr`. `s->f` is `rd s (·.f)`, and `s->f = v` is
19  `wr s (fun d => { d with f := v })`: a load of the record, a record update and a store, so every access faults on a
20  null, dangling or wrong-kind pointer.
21* `ZALLOC`/`ZFREE` call through `strm->zalloc`/`zfree`. Only the default `zcalloc`/`zcfree` (`FnPtr.fn "zcalloc"`,
22  `"zcfree"`, installed by `deflateInit2_`) are modelled; any other function is `ub "custom allocator not modelled"`.
23  `Posf *` blocks (`prev`, `head`) are blocks of the `words` table, so `ZALLOC(strm, n, sizeof(Pos))` is `allocW`
24  of the number of 16-bit words in the `n * 2` bytes (the product is taken in `unsigned`, as in `zcalloc`)
25  and `zmemzero` of such a block counts words.
26* Signed `int` and `long` arithmetic is checked (`iadd`, `isub`, `ishl`, ...: overflow and invalid shifts are
27  `Fault.ub`); unsigned arithmetic wraps.
28* An `unsigned char *` or `char *` is a `BPtr`; `p + n` is `Ptr.add`, `*p` is `Ptr.load`, `p[i]` is `index8`.
29* Output parameters (`unsigned *pending`, `uInt *dictLength`, `z_size_t *destLen`) are modelled in the files that
30  use them as an input value and a result.
31* The control tags of loops with `break` or `return` are fields of the loop state.
32-/
33
34namespace Zlib.Deflate
35open C
36open Zlib.Trees («_tr_init» «_tr_flush_bits» «_tr_flush_block» «_tr_stored_block» «_tr_align»)
37open Zlib.Crc32 (crc32 crc32_z)
38
39/-! ## Constants of `deflate.c` and `deflate.h` -/
40
41def MIN_MATCH_u : UInt32 := 3          -- MIN_MATCH
42def MAX_MATCH_u : UInt32 := 258        -- MAX_MATCH
43def MIN_LOOKAHEAD_u : UInt32 := 262    -- MIN_LOOKAHEAD = MAX_MATCH+MIN_MATCH+1
44def WIN_INIT_u : UInt64 := 258         -- WIN_INIT = MAX_MATCH
45def MAX_STORED : UInt32 := 65535
46def TOO_FAR : UInt32 := 4096
47def sizeof_z_stream : Int32 := 112     -- sizeof(z_stream), LP64
48
49/-- `block_state` (`enum`, so `unsigned`). -/
50abbrev block_state := UInt32
51def need_more : block_state := 0
52def block_done : block_state := 1
53def finish_started : block_state := 2
54def finish_done : block_state := 3
55
56/-- Which function `config.func` points to (D-6: function pointers to the local compressors are an enum). -/
57inductive CompressFunc where
58  | stored | fast | slow
59  deriving DecidableEq, Inhabited
60
61/-- `struct config_s` -/
62structure Config where
63  good_length : UInt16
64  max_lazy : UInt16
65  nice_length : UInt16
66  max_chain : UInt16
67  func : CompressFunc
68  deriving Inhabited
69
70/-- `local const config configuration_table[10]` -/
71def configuration_table : Array Config := #[
72  -- level 0
73  ⟨0, 0, 0, 0, .stored⟩,
74  -- level 1
75  ⟨4, 4, 8, 4, .fast⟩,
76  -- level 2
77  ⟨4, 5, 16, 8, .fast⟩,
78  -- level 3
79  ⟨4, 6, 32, 32, .fast⟩,
80  -- level 4
81  ⟨4, 4, 16, 16, .slow⟩,
82  -- level 5
83  ⟨8, 16, 32, 32, .slow⟩,
84  -- level 6
85  ⟨8, 16, 128, 128, .slow⟩,
86  -- level 7
87  ⟨8, 32, 128, 256, .slow⟩,
88  -- level 8
89  ⟨32, 128, 258, 1024, .slow⟩,
90  -- level 9
91  ⟨32, 258, 258, 4096, .slow⟩]
92
93/-- `configuration_table[level]`: an index outside `0..9` is undefined. -/
94def config_at (level : Int32) : M Config :=
95  if 0 ≤ level.toInt ∧ level.toInt < 10 then pure configuration_table[level.toInt.toNat]!
96  else ub "configuration_table index out of range"
97
98/-! ## Checked signed arithmetic and shifts -/
99
100def chk32 (v : Int) : M Int32 :=
101  if -2147483648 ≤ v ∧ v ≤ 2147483647 then pure (Int32.ofInt v) else ub "signed int overflow"
102def chk64 (v : Int) : M Int64 :=
103  if -9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807 then pure (Int64.ofInt v) else ub "signed long overflow"
104def iadd (a b : Int32) : M Int32 := chk32 (a.toInt + b.toInt)
105def isub (a b : Int32) : M Int32 := chk32 (a.toInt - b.toInt)
106def ineg (a : Int32) : M Int32 := chk32 (-a.toInt)
107def ladd (a b : Int64) : M Int64 := chk64 (a.toInt + b.toInt)
108def lsub (a b : Int64) : M Int64 := chk64 (a.toInt - b.toInt)
109/-- `a << n` for `int`: the count must be in `0..31` and the result representable (`a >= 0`). -/
110def ishl (a : Int32) (n : Int) : M Int32 :=
111  if 0 ≤ n ∧ n < 32 ∧ 0 ≤ a.toInt then chk32 (a.toInt * 2 ^ n.toNat) else ub "invalid shift of an int"
112/-- `a << n` for `unsigned`: the count must be in `0..31`. -/
113def ushl (a : UInt32) (n : UInt32) : M UInt32 :=
114  if n < 32 then pure (a <<< n) else ub "invalid shift of an unsigned"
115
116/-! ## Field access -/
117
118/-- `s->f` (read). -/
119@[inline] def rd {α : Type} (s : DeflateStatePtr) (f : DeflateState → α) : M α := do
120  return f (← ldDeflateState s)
121/-- `s->f = v` and the like (a record update). -/
122@[inline] def wr (s : DeflateStatePtr) (f : DeflateState → DeflateState) : M Unit := do
123  let d ← ldDeflateState s
124  stDeflateState s (f d)
125/-- `strm->f` (read). -/
126@[inline] def zrd {α : Type} (strm : ZStreamPtr) (f : ZStream → α) : M α := do
127  return f (← ldZStream strm)
128/-- `strm->f = v` and the like. -/
129@[inline] def zwr (strm : ZStreamPtr) (f : ZStream → ZStream) : M Unit := do
130  let z ← ldZStream strm
131  stZStream strm (f z)
132
133/-- `p + n` for a pointer and a nonnegative count. -/
134@[inline] def padd {R T : Type} [Space Heap R T] (p : Ptr R) (n : Nat) : M (Ptr R) := Ptr.add p (n : Int)
135/-- `p - n`. -/
136@[inline] def psub {R T : Type} [Space Heap R T] (p : Ptr R) (n : Nat) : M (Ptr R) := Ptr.add p (-(n : Int))
137/-- `p[i] = v` for a byte pointer and an index. -/
138@[inline] def store_at (p : BPtr) (i : Nat) (v : UInt8) : M Unit := do
139  store8 (← padd p i) v
140
141/-- `ZALLOC`/`ZFREE` of the default allocator only. -/
142def zalloc_default (strm : ZStreamPtr) : M Unit := do
143  let z ← ldZStream strm
144  if z.zalloc != FnPtr.fn "zcalloc" then ub "custom allocator not modelled"
145def zfree_default (strm : ZStreamPtr) : M Unit := do
146  let z ← ldZStream strm
147  if z.zfree != FnPtr.fn "zcfree" then ub "custom allocator not modelled"
148
149/-- `ZALLOC(strm, items, size)` for a byte block (`zcalloc`: `malloc(items * size)`, product in `unsigned`). -/
150def ZALLOC_bytes (strm : ZStreamPtr) (items size : UInt32) : M BPtr := do
151  zalloc_default strm
152  let z ← ldZStream strm
153  Zlib.Zutil.zcalloc z.«opaque» items size
154/-- `ZALLOC(strm, items, sizeof(Pos))` for a `Posf *` block (a block of 16-bit words). -/
155def ZALLOC_words (strm : ZStreamPtr) (items : UInt32) : M WPtr := do
156  zalloc_default strm
157  -- zcalloc: malloc(items * size) with the product in `unsigned`; the block of `Pos` has that many bytes / 2 words
158  let bytes : UInt32 := items * 2
159  allocW (bytes.toNat / 2)
160/-- `ZFREE(strm, addr)` of a byte block. -/
161def ZFREE_bytes (strm : ZStreamPtr) (p : BPtr) : M Unit := do
162  zfree_default strm
163  freeB p
164/-- `ZFREE(strm, addr)` of a block of words. -/
165def ZFREE_words (strm : ZStreamPtr) (p : WPtr) : M Unit := do
166  zfree_default strm
167  freeW p
168
169/-- `ERR_MSG(err)` -/
170def ERR_MSG (err : Int32) : M BPtr := Zlib.Zutil.zError err
171
172/-! ## Macros of `deflate.c` and `deflate.h` -/
173
174/-- `put_byte(s, c)`: `{s->pending_buf[s->pending++] = (Bytef)(c);}` (no capacity test, I-1). -/
175def put_byte (s : DeflateStatePtr) (c : UInt8) : M Unit := do
176  let d ← ldDeflateState s
177  store_at d.pending_buf d.pending.toNat c
178  stDeflateState s { d with pending := d.pending + 1 }
179
180/-- `UPDATE_HASH(s, s->ins_h, c)`: `s->ins_h = ((s->ins_h << s->hash_shift) ^ (c)) & s->hash_mask` (`c` is an
181`int` made of a byte). -/
182def UPDATE_HASH (s : DeflateStatePtr) (c : UInt8) : M Unit := do
183  let d ← ldDeflateState s
184  let sh ← ushl d.ins_h d.hash_shift
185  stDeflateState s { d with ins_h := (sh ^^^ c.toUInt32) &&& d.hash_mask }
186
187/-- `INSERT_STRING(s, str, match_head)`: returns the new `match_head`.
188`(UPDATE_HASH(s, s->ins_h, s->window[(str) + (MIN_MATCH-1)]),
189  match_head = s->prev[(str) & s->w_mask] = s->head[s->ins_h], s->head[s->ins_h] = (Pos)(str))` -/
190def INSERT_STRING (s : DeflateStatePtr) (str : UInt32) : M UInt32 := do
191  let d ← ldDeflateState s
192  let c ← index8 d.window (str + (MIN_MATCH_u - 1)).toNat
193  UPDATE_HASH s c
194  let d ← ldDeflateState s
195  let v ← Ptr.index d.head d.ins_h.toNat
196  Ptr.store (← padd d.prev (str &&& d.w_mask).toNat) v
197  Ptr.store (← padd d.head d.ins_h.toNat) str.toUInt16
198  return v.toUInt32
199
200/-- `CLEAR_HASH(s)`: `s->head[s->hash_size - 1] = NIL; zmemzero(s->head, (unsigned)(s->hash_size - 1)*sizeof(*s->head));
201s->slid = 0;` (the `memset` of `2 * (hash_size - 1)` bytes is `hash_size - 1` words). -/
202def CLEAR_HASH (s : DeflateStatePtr) : M Unit := do
203  let d ← ldDeflateState s
204  Ptr.store (← padd d.head (d.hash_size - 1).toNat) (0 : UInt16)
205  Ptr.fill d.head (0 : UInt16) (d.hash_size - 1).toNat
206  wr s (fun d => { d with slid := 0 })
207
208/-- `d_code(dist)`: `((dist) < 256 ? _dist_code[dist] : _dist_code[256+((dist)>>7)])` (`dist` is a `ush`). -/
209def d_code (dist : UInt16) : M UInt8 :=
210  if dist.toNat < 256 then index8 (.ref BRef.st_dist_code 0) dist.toNat
211  else index8 (.ref BRef.st_dist_code 0) (256 + (dist >>> 7).toNat)
212
213/-- `s->tree[i].Freq++` for the tree array `r` (`ush`, wraps). -/
214def freq_inc (r : CtDataRef) (i : Nat) : M Unit := do
215  let p : CtDataPtr := .ref r 0
216  let q ← padd p i
217  let e ← Ptr.load q
218  Ptr.store q { e with fc := e.fc + 1 }
219
220/-- `_tr_tally_lit(s, c, flush)` (`flush` is the result). -/
221def tally_lit (s : DeflateStatePtr) (c : UInt8) : M Bool := do
222  let cc := c   -- uch cc = (c);
223  let d ← ldDeflateState s
224  -- s->sym_buf[s->sym_next++] = 0; (twice) = cc;
225  store_at d.sym_buf d.sym_next.toNat 0
226  store_at d.sym_buf (d.sym_next + 1).toNat 0
227  store_at d.sym_buf (d.sym_next + 2).toNat cc
228  stDeflateState s { d with sym_next := d.sym_next + 3 }
229  -- s->dyn_ltree[cc].Freq++;
230  match s with
231  | none => ub "null deflate_state"
232  | some (.tab id) =>
233    freq_inc (.dstate_dyn_ltree id) cc.toNat
234    -- flush = (s->sym_next == s->sym_end);
235    let d ← ldDeflateState s
236    return d.sym_next == d.sym_end
237
238/-- `_tr_tally_dist(s, distance, length, flush)` (the arguments are `unsigned` expressions). -/
239def tally_dist (s : DeflateStatePtr) (distance length : UInt32) : M Bool := do
240  let len : UInt8 := length.toUInt8            -- uch len = (uch)(length);
241  let dist : UInt16 := distance.toUInt16       -- ush dist = (ush)(distance);
242  let d ← ldDeflateState s
243  store_at d.sym_buf d.sym_next.toNat dist.toUInt8
244  store_at d.sym_buf (d.sym_next + 1).toNat (dist >>> 8).toUInt8
245  store_at d.sym_buf (d.sym_next + 2).toNat len
246  stDeflateState s { d with sym_next := d.sym_next + 3 }
247  let dist : UInt16 := dist - 1                -- dist--;
248  match s with
249  | none => ub "null deflate_state"
250  | some (.tab id) =>
251    -- s->dyn_ltree[_length_code[len]+LITERALS+1].Freq++;
252    let lc ← index8 (.ref BRef.st_length_code 0) len.toNat
253    freq_inc (.dstate_dyn_ltree id) (lc.toNat + 256 + 1)
254    -- s->dyn_dtree[d_code(dist)].Freq++;
255    let dc ← d_code dist
256    freq_inc (.dstate_dyn_dtree id) dc.toNat
257    let d ← ldDeflateState s
258    return d.sym_next == d.sym_end
259
260/-! ## `slide_hash` -/
261
262/-- `local void slide_hash(deflate_state *s)` -/
263def slide_hash (s : DeflateStatePtr) : M Unit := do
264  let d ← ldDeflateState s
265  let wsize : UInt32 := d.w_size                 -- uInt wsize = s->w_size;
266  let n : UInt32 := d.hash_size                  -- n = s->hash_size;
267  let p : WPtr ← padd d.head n.toNat             -- p = &s->head[n];
268  -- do { m = *--p; *p = (Pos)(m >= wsize ? m - wsize : NIL); } while (--n);
269  let (_, _) ← cdoWhile
270    (fun (n, p) => do
271      let p ← psub p 1
272      let m : UInt32 := (← Ptr.load p).toUInt32
273      Ptr.store p (if m ≥ wsize then (m - wsize).toUInt16 else (0 : UInt16))
274      pure (n, p))
275    (fun (n, p) => let n := n - 1; pure (n != 0, (n, p)))
276    (n, p)
277  -- #ifndef FASTEST
278  let n : UInt32 := wsize                        -- n = wsize;
279  let p : WPtr ← padd d.prev n.toNat             -- p = &s->prev[n];
280  let (_, _) ← cdoWhile
281    (fun (n, p) => do
282      let p ← psub p 1
283      let m : UInt32 := (← Ptr.load p).toUInt32
284      Ptr.store p (if m ≥ wsize then (m - wsize).toUInt16 else (0 : UInt16))
285      pure (n, p))
286    (fun (n, p) => let n := n - 1; pure (n != 0, (n, p)))
287    (n, p)
288  -- s->slid = 1;
289  wr s (fun d => { d with slid := 1 })
290
291/-! ## `read_buf` and `fill_window` -/
292
293/-- `local unsigned read_buf(z_streamp strm, Bytef *buf, unsigned size)` -/
294def read_buf (strm : ZStreamPtr) (buf : BPtr) (size : UInt32) : M UInt32 := do
295  let mut len ← zrd strm (·.avail_in)            -- unsigned len = strm->avail_in;
296  if len > size then len := size
297  if len == 0 then return 0
298  -- strm->avail_in -= len;
299  zwr strm (fun z => { z with avail_in := z.avail_in - len })
300  -- zmemcpy(buf, strm->next_in, len);
301  memcpyB buf (← zrd strm (·.next_in)) len.toNat
302  let sp ← castDeflateState (← zrd strm (·.state))
303  let wrap ← rd sp (·.wrap)
304  if wrap == 1 then
305    -- strm->adler = adler32(strm->adler, buf, len);
306    let a ← zrd strm (·.adler)
307    let r ← Zlib.Adler32.adler32 a buf len
308    zwr strm (fun z => { z with adler := r })
309  else if wrap == 2 then
310    -- strm->adler = crc32(strm->adler, buf, len);
311    let a ← zrd strm (·.adler)
312    let r ← crc32 a buf len
313    zwr strm (fun z => { z with adler := r })
314  -- strm->next_in += len; strm->total_in += len;
315  let ni ← padd (← zrd strm (·.next_in)) len.toNat
316  zwr strm (fun z => { z with next_in := ni, total_in := z.total_in + len.toUInt64 })
317  return len
318
319/-- `local void fill_window(deflate_state *s)`.
320The loop `do { ... } while (cond)` has two `break`s; the state of the outer loop is the flag `brk`. The
321`if (sizeof(int) <= 2)` block is dead (`sizeof(int)` is 4). -/
322def fill_window (s : DeflateStatePtr) : M Unit := do
323  let wsize ← rd s (·.w_size)                    -- uInt wsize = s->w_size;
324  let _ ← cdoWhile
325    (fun (_ : Bool) => do
326      let d ← ldDeflateState s
327      -- more = (unsigned)(s->window_size -(ulg)s->lookahead -(ulg)s->strstart);
328      let mut more : UInt32 := (d.window_size - d.lookahead.toUInt64 - d.strstart.toUInt64).toUInt32
329      -- if (s->strstart >= wsize + MAX_DIST(s)) { ... }   (MAX_DIST(s) = w_size - MIN_LOOKAHEAD)
330      if d.strstart ≥ wsize + (d.w_size - MIN_LOOKAHEAD_u) then
331        -- zmemcpy(s->window, s->window + wsize, (unsigned)wsize - more);
332        memcpyB d.window (← padd d.window wsize.toNat) (wsize - more).toNat
333        wr s (fun d => { d with match_start := d.match_start - wsize }) -- s->match_start -= wsize;
334        wr s (fun d => { d with strstart := d.strstart - wsize })       -- s->strstart -= wsize;
335        let block_start ← lsub (← rd s (·.block_start)) wsize.toUInt64.toInt64
336        wr s (fun d => { d with block_start })                         -- s->block_start -= (long) wsize;
337        -- if (s->insert > s->strstart) s->insert = s->strstart;
338        wr s (fun d => { d with insert := if d.insert > d.strstart then d.strstart else d.insert })
339        slide_hash s
340        more := more + wsize                                             -- more += wsize;
341      -- if (s->strm->avail_in == 0) break;
342      let strm ← rd s (·.strm)
343      if (← zrd strm (·.avail_in)) == 0 then return true
344      -- n = read_buf(s->strm, s->window + s->strstart + s->lookahead, more);
345      let d ← ldDeflateState s
346      let dst ← padd (← padd d.window d.strstart.toNat) d.lookahead.toNat
347      let n ← read_buf strm dst more
348      wr s (fun d => { d with lookahead := d.lookahead + n })            -- s->lookahead += n;
349      -- if (s->lookahead + s->insert >= MIN_MATCH) { ... }
350      let d ← ldDeflateState s
351      if d.lookahead + d.insert ≥ MIN_MATCH_u then
352        let str : UInt32 := d.strstart - d.insert                    -- uInt str = s->strstart - s->insert;
353        -- s->ins_h = s->window[str];
354        let c0 ← index8 d.window str.toNat
355        wr s (fun d => { d with ins_h := c0.toUInt32 })
356        -- UPDATE_HASH(s, s->ins_h, s->window[str + 1]);
357        UPDATE_HASH s (← index8 d.window (str + 1).toNat)
358        -- while (s->insert) { ... }
359        let (_, _) ← cwhile
360          (fun (str, brk) => do
361            let ins ← rd s (·.insert)
362            pure (ins != 0 && !brk, (str, brk)))
363          (fun (str, brk) => do
364            let d ← ldDeflateState s
365            -- UPDATE_HASH(s, s->ins_h, s->window[str + MIN_MATCH-1]);
366            UPDATE_HASH s (← index8 d.window (str + (MIN_MATCH_u - 1)).toNat)
367            let d ← ldDeflateState s
368            -- s->prev[str & s->w_mask] = s->head[s->ins_h];
369            let v ← Ptr.index d.head d.ins_h.toNat
370            Ptr.store (← padd d.prev (str &&& d.w_mask).toNat) v
371            -- s->head[s->ins_h] = (Pos)str;
372            Ptr.store (← padd d.head d.ins_h.toNat) str.toUInt16
373            -- str++; s->insert--;
374            let str := str + 1
375            wr s (fun d => { d with insert := d.insert - 1 })
376            -- if (s->lookahead + s->insert < MIN_MATCH) break;
377            let d ← ldDeflateState s
378            pure (str, d.lookahead + d.insert < MIN_MATCH_u))
379          (str, false)
380      pure false)
381    (fun brk => do
382      if brk then return (false, brk)
383      -- while (s->lookahead < MIN_LOOKAHEAD && s->strm->avail_in != 0)
384      let d ← ldDeflateState s
385      if d.lookahead < MIN_LOOKAHEAD_u then
386        return ((← zrd d.strm (·.avail_in)) != 0, brk)
387      return (false, brk))
388    false
389  -- if (s->high_water < s->window_size) { ... }
390  let d ← ldDeflateState s
391  if d.high_water < d.window_size then
392    let curr : UInt64 := d.strstart.toUInt64 + d.lookahead.toUInt64   -- ulg curr = s->strstart + (ulg)(s->lookahead);
393    if d.high_water < curr then
394      -- init = s->window_size - curr; if (init > WIN_INIT) init = WIN_INIT;
395      let mut init : UInt64 := d.window_size - curr
396      if init > WIN_INIT_u then init := WIN_INIT_u
397      -- zmemzero(s->window + curr, (unsigned)init);
398      memsetB (← padd d.window curr.toNat) 0 init.toUInt32.toNat
399      wr s (fun d => { d with high_water := curr + init })              -- s->high_water = curr + init;
400    else if d.high_water < curr + WIN_INIT_u then
401      -- init = (ulg)curr + WIN_INIT - s->high_water;
402      let mut init : UInt64 := curr + WIN_INIT_u - d.high_water
403      -- if (init > s->window_size - s->high_water) init = s->window_size - s->high_water;
404      if init > d.window_size - d.high_water then init := d.window_size - d.high_water
405      -- zmemzero(s->window + s->high_water, (unsigned)init);
406      memsetB (← padd d.window d.high_water.toNat) 0 init.toUInt32.toNat
407      wr s (fun d => { d with high_water := d.high_water + init })      -- s->high_water += init;
408
409/-! ## `putShortMSB`, `flush_pending` -/
410
411/-- `local void putShortMSB(deflate_state *s, uInt b)` -/
412def putShortMSB (s : DeflateStatePtr) (b : UInt32) : M Unit := do
413  put_byte s (b >>> 8).toUInt8        -- put_byte(s, (Byte)(b >> 8));
414  put_byte s (b &&& 0xff).toUInt8     -- put_byte(s, (Byte)(b & 0xff));
415
416/-- `local void flush_pending(z_streamp strm)` -/
417def flush_pending (strm : ZStreamPtr) : M Unit := do
418  let s ← castDeflateState (← zrd strm (·.state))       -- deflate_state *s = strm->state;
419  _tr_flush_bits s                                       -- _tr_flush_bits(s);
420  let z ← ldZStream strm
421  let d ← ldDeflateState s
422  -- len = s->pending > strm->avail_out ? strm->avail_out : (unsigned)s->pending;
423  let len : UInt32 := if d.pending > z.avail_out.toUInt64 then z.avail_out else d.pending.toUInt32
424  if len == 0 then return                                -- if (len == 0) return;
425  -- zmemcpy(strm->next_out, s->pending_out, len);
426  memcpyB z.next_out d.pending_out len.toNat
427  -- strm->next_out += len; s->pending_out += len;
428  let no ← padd z.next_out len.toNat
429  let po ← padd d.pending_out len.toNat
430  -- strm->total_out += len; strm->avail_out -= len;
431  stZStream strm { z with next_out := no, total_out := z.total_out + len.toUInt64, avail_out := z.avail_out - len }
432  -- s->pending -= len;
433  let pend := d.pending - len.toUInt64
434  stDeflateState s { d with pending_out := po, pending := pend }
435  -- if (s->pending == 0) s->pending_out = s->pending_buf;
436  if pend == 0 then wr s (fun d => { d with pending_out := d.pending_buf })
437
438/-- `FLUSH_BLOCK_ONLY(s, last)` -/
439def FLUSH_BLOCK_ONLY (s : DeflateStatePtr) (last : Int32) : M Unit := do
440  let d ← ldDeflateState s
441  -- (s->block_start >= 0L ? (charf *)&s->window[(unsigned)s->block_start] : (charf *)Z_NULL)
442  let buf ← if d.block_start ≥ 0 then padd d.window d.block_start.toUInt64.toUInt32.toNat else pure (Ptr.null : BPtr)
443  -- (ulg)((long)s->strstart - s->block_start)
444  let n ← lsub d.strstart.toUInt64.toInt64 d.block_start
445  «_tr_flush_block» s buf n.toUInt64 last
446  -- s->block_start = s->strstart;
447  wr s (fun d => { d with block_start := d.strstart.toUInt64.toInt64 })
448  -- flush_pending(s->strm);
449  flush_pending (← rd s (·.strm))
450
451/-- `FLUSH_BLOCK(s, last)`: the `return`s of the macro are `some state`; `none` falls through. -/
452def FLUSH_BLOCK (s : DeflateStatePtr) (last : Int32) : M (Option block_state) := do
453  FLUSH_BLOCK_ONLY s last
454  let d ← ldDeflateState s
455  if (← zrd d.strm (·.avail_out)) == 0 then
456    if last == 0 then return some need_more                 -- if (!(last)) return need_more;
457    if d.pending != 0 || d.wrap != 0 then return some finish_started
458  return none
459
460end Zlib.Deflate