deflate_strategies.c.lean

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

1import ZlibF.Zlib.«deflate_base.c»
2
3/-!
4# deflate.c, part 2: `longest_match` and the five compression functions
5
6`longest_match` (the `#ifndef FASTEST`, not `UNALIGNED_OK` version), `deflate_stored`, `deflate_fast`,
7`deflate_slow`, `deflate_rle`, `deflate_huff`. See `deflate_base.c.lean` for the conventions.
8
9Control flow: `for (;;)` with `break` and `return` inside is a `cwhile` over a `LoopS`; `ret = some v` is
10`return v`, `brk = true` is `break` (both skip the rest of the body, as `return` in the body function does). A `continue`
11of `longest_match`'s `do ... while` jumps to its condition.
12-/
13
14namespace Zlib.Deflate
15open C
16open Zlib.Trees («_tr_init» «_tr_flush_bits» «_tr_flush_block» «_tr_stored_block» «_tr_align»)
17open Zlib.Crc32 (crc32 crc32_z)
18
19/-! ## `longest_match` -/
20
21/-- Loop-carried locals of `longest_match`; `brk` is the `break`. -/
22structure LMState where
23  cur_match : UInt32
24  chain_length : UInt32
25  best_len : Int32
26  nice_match : Int32
27  scan : BPtr
28  scan_end1 : UInt8
29  scan_end : UInt8
30  brk : Bool
31
32/-- The condition of the inner `do { } while (*++scan == *++match && ... (8 times) && scan < strend)`; the C unrolls the
33comparisons eight times, the loop here repeats the same step eight times. -/
34def lm_cond (strend scan match_ : BPtr) : M (Bool × BPtr × BPtr) := do
35  let mut scan := scan
36  let mut m := match_
37  for _ in [0:8] do
38    scan ← padd scan 1                       -- ++scan
39    m ← padd m 1                             -- ++match
40    if (← load8 scan) != (← load8 m) then return (false, scan, m)
41  return (← Ptr.lt scan strend, scan, m)     -- scan < strend
42
43/-- The body of the `do` of `longest_match`, up to the end of the compound statement; `continue` is `return st`. -/
44def lm_body (s : DeflateStatePtr) (st : LMState) : M LMState := do
45  let d ← ldDeflateState s
46  -- match = s->window + cur_match;
47  let mut match_ ← padd d.window st.cur_match.toNat
48  let scan := st.scan
49  -- if (match[best_len] != scan_end || match[best_len - 1] != scan_end1 || *match != *scan || *++match != scan[1]) continue;
50  if (← index8 match_ st.best_len.toInt) != st.scan_end then return st
51  if (← index8 match_ (← isub st.best_len 1).toInt) != st.scan_end1 then return st
52  if (← load8 match_) != (← load8 scan) then return st
53  match_ ← padd match_ 1
54  if (← load8 match_) != (← index8 scan 1) then return st
55  -- scan += 2, match++;
56  let scan ← padd scan 2
57  match_ ← padd match_ 1
58  -- strend = s->window + s->strstart + MAX_MATCH;
59  let strend ← padd (← padd d.window d.strstart.toNat) MAX_MATCH_u.toNat
60  -- do { } while (*++scan == *++match && ... && scan < strend);
61  let (scan, _) ← cdoWhile (fun x => pure x)
62    (fun (scan, m) => do
63      let (c, scan, m) ← lm_cond strend scan m
64      pure (c, (scan, m)))
65    (scan, match_)
66  -- len = MAX_MATCH - (int)(strend - scan);
67  let diff ← Ptr.diff strend scan
68  let len ← isub 258 diff.toInt32
69  -- scan = strend - MAX_MATCH;
70  let scan ← psub strend MAX_MATCH_u.toNat
71  let mut st := { st with scan }
72  -- if (len > best_len) { ... }
73  if len > st.best_len then
74    wr s (fun d => { d with match_start := st.cur_match })      -- s->match_start = cur_match;
75    st := { st with best_len := len }                            -- best_len = len;
76    if len ≥ st.nice_match then return { st with brk := true }   -- if (len >= nice_match) break;
77    -- scan_end1 = scan[best_len - 1]; scan_end = scan[best_len];
78    let e1 ← index8 st.scan (← isub st.best_len 1).toInt
79    let e ← index8 st.scan st.best_len.toInt
80    st := { st with scan_end1 := e1, scan_end := e }
81  return st
82
83/-- `local uInt longest_match(deflate_state *s, IPos cur_match)` -/
84def longest_match (s : DeflateStatePtr) (cur_match : UInt32) : M UInt32 := do
85  let d ← ldDeflateState s
86  let mut chain_length : UInt32 := d.max_chain_length      -- unsigned chain_length = s->max_chain_length;
87  let scan ← padd d.window d.strstart.toNat                -- Bytef *scan = s->window + s->strstart;
88  let best_len : Int32 := d.prev_length.toInt32            -- int best_len = (int)s->prev_length;
89  let mut nice_match : Int32 := d.nice_match               -- int nice_match = s->nice_match;
90  -- IPos limit = s->strstart > (IPos)MAX_DIST(s) ? s->strstart - (IPos)MAX_DIST(s) : NIL;
91  let maxd : UInt32 := d.w_size - MIN_LOOKAHEAD_u
92  let limit : UInt32 := if d.strstart > maxd then d.strstart - maxd else 0
93  let prev := d.prev                                       -- Posf *prev = s->prev;
94  let wmask := d.w_mask                                    -- uInt wmask = s->w_mask;
95  -- Bytef *strend = s->window + s->strstart + MAX_MATCH;
96  let _strend ← padd (← padd d.window d.strstart.toNat) MAX_MATCH_u.toNat
97  -- Byte scan_end1 = scan[best_len - 1]; Byte scan_end = scan[best_len];
98  let scan_end1 ← index8 scan (← isub best_len 1).toInt
99  let scan_end ← index8 scan best_len.toInt
100  -- if (s->prev_length >= s->good_match) chain_length >>= 2;
101  if d.prev_length ≥ d.good_match then chain_length := chain_length >>> 2
102  -- if ((uInt)nice_match > s->lookahead) nice_match = (int)s->lookahead;
103  if nice_match.toUInt32 > d.lookahead then nice_match := d.lookahead.toInt32
104  -- do { ... } while ((cur_match = prev[cur_match & wmask]) > limit && --chain_length != 0);
105  let st ← cdoWhile (lm_body s)
106    (fun st => do
107      if st.brk then return (false, st)                       -- break leaves the loop
108      let cm : UInt32 := (← Ptr.index prev (st.cur_match &&& wmask).toNat).toUInt32
109      let st := { st with cur_match := cm }
110      if cm > limit then
111        let cl := st.chain_length - 1                          -- --chain_length
112        return (cl != 0, { st with chain_length := cl })
113      return (false, st))
114    { cur_match, chain_length, best_len, nice_match, scan, scan_end1, scan_end, brk := false }
115  -- if ((uInt)best_len <= s->lookahead) return (uInt)best_len; return s->lookahead;
116  let lookahead ← rd s (·.lookahead)
117  if st.best_len.toUInt32 ≤ lookahead then return st.best_len.toUInt32
118  return lookahead
119
120/-! ## Loop state of the compression functions -/
121
122structure LoopS where
123  hash_head : UInt32 := 0
124  bflush : Bool := false
125  ret : Option block_state := none
126  brk : Bool := false
127
128/-- `for (;;)`: continues until `break` or `return`. -/
129def forever (st : LoopS) : M (Bool × LoopS) := pure (!(st.brk || st.ret.isSome), st)
130
131/-- `MIN(a, b)` is `((a) > (b) ? (b) : (a))` -/
132def MIN {α : Type} [LT α] [DecidableRel (α := α) (· < ·)] (a b : α) : α := if b < a then b else a
133
134/-- The part of the compression functions after the loop that ends with `flush == Z_FINISH`, `s->sym_next`, ...:
135`if (flush == Z_FINISH) { FLUSH_BLOCK(s, 1); return finish_done; } if (s->sym_next) FLUSH_BLOCK(s, 0); return block_done;` -/
136def finish_tail (s : DeflateStatePtr) (flush : Int32) : M block_state := do
137  if flush == Z_FINISH then
138    if let some r := (← FLUSH_BLOCK s 1) then return r
139    return finish_done
140  if (← rd s (·.sym_next)) != 0 then
141    if let some r := (← FLUSH_BLOCK s 0) then return r
142  return block_done
143
144/-! ## `deflate_stored` -/
145
146/-- Locals of the first `do { } while (last == 0)` of `deflate_stored`. -/
147structure StoredS where
148  last : Int32
149  len : UInt32
150  left : UInt32
151  have_ : UInt32
152  all : Bool
153  brk : Bool
154
155/-- `local block_state deflate_stored(deflate_state *s, int flush)` -/
156def deflate_stored (s : DeflateStatePtr) (flush : Int32) : M block_state := do
157  let d ← ldDeflateState s
158  -- unsigned min_block = (unsigned)(MIN(s->pending_buf_size - 5, s->w_size));
159  let mut min_block : UInt32 := (MIN (d.pending_buf_size - 5) d.w_size.toUInt64).toUInt32
160  let strm := d.strm
161  -- unsigned used = s->strm->avail_in;
162  let mut used ← zrd strm (·.avail_in)
163  let st ← cdoWhile
164    (fun (st : StoredS) => do
165      -- len = MAX_STORED;
166      let mut st := { st with len := MAX_STORED }
167      let d ← ldDeflateState s
168      -- have = ((unsigned)s->bi_valid + 42) >> 3;
169      let hv : UInt32 := (d.bi_valid.toUInt32 + 42) >>> 3
170      let z ← ldZStream strm
171      -- if (s->strm->avail_out < have) break;
172      if z.avail_out < hv then return { st with have_ := hv, brk := true }
173      -- have = s->strm->avail_out - have;
174      let mut have_ := z.avail_out - hv
175      -- left = (unsigned)(s->strstart - s->block_start);
176      let left : UInt32 := (← lsub d.strstart.toUInt64.toInt64 d.block_start).toUInt64.toUInt32
177      let mut len := st.len
178      -- if (left < len && s->strm->avail_in < len - left) len = left + s->strm->avail_in;
179      if left < len && z.avail_in < len - left then len := left + z.avail_in
180      -- if (len > have) len = have;
181      if len > have_ then len := have_
182      -- all = len >= left && len - left == s->strm->avail_in;
183      let all := len ≥ left && len - left == z.avail_in
184      -- if (len < min_block && ((len == 0 && flush != Z_FINISH) || flush == Z_NO_FLUSH || !all)) break;
185      if len < min_block && ((len == 0 && flush != Z_FINISH) || flush == Z_NO_FLUSH || !all) then
186        return { st with len, left, have_, all, brk := true }
187      -- last = flush == Z_FINISH && all ? 1 : 0;
188      let last : Int32 := if flush == Z_FINISH && all then 1 else 0
189      -- _tr_stored_block(s, (char *)0, 0L, last);
190      _tr_stored_block s (Ptr.null : BPtr) 0 last
191      -- s->pending_buf[s->pending - 4] = (Bytef)len; ... [-3] = (Bytef)(len >> 8); [-2] = (Bytef)~len; [-1] = (Bytef)(~len >> 8);
192      let d ← ldDeflateState s
193      store8 (← padd d.pending_buf (d.pending - 4).toNat) len.toUInt8
194      store8 (← padd d.pending_buf (d.pending - 3).toNat) (len >>> 8).toUInt8
195      store8 (← padd d.pending_buf (d.pending - 2).toNat) (~~~len).toUInt8
196      store8 (← padd d.pending_buf (d.pending - 1).toNat) ((~~~len) >>> 8).toUInt8
197      -- flush_pending(s->strm);
198      flush_pending strm
199      let mut left := left
200      -- if (left) { ... }
201      if left != 0 then
202        if left > len then left := len
203        let d ← ldDeflateState s
204        let z ← ldZStream strm
205        -- zmemcpy(s->strm->next_out, s->window + s->block_start, left);
206        memcpyB z.next_out (← Ptr.add d.window d.block_start.toInt) left.toNat
207        let no ← padd z.next_out left.toNat
208        zwr strm (fun z => { z with next_out := no, avail_out := z.avail_out - left,
209                                    total_out := z.total_out + left.toUInt64 })
210        let bs ← ladd d.block_start left.toUInt64.toInt64      -- s->block_start += left;
211        wr s (fun d => { d with block_start := bs })
212        len := len - left
213      -- if (len) { read_buf(s->strm, s->strm->next_out, len); ... }
214      if len != 0 then
215        let _ ← read_buf strm (← zrd strm (·.next_out)) len
216        let no ← padd (← zrd strm (·.next_out)) len.toNat
217        zwr strm (fun z => { z with next_out := no, avail_out := z.avail_out - len,
218                                    total_out := z.total_out + len.toUInt64 })
219      pure { st with last, len, left, have_, all, brk := false })
220    (fun st => pure (!st.brk && st.last == 0, st))             -- while (last == 0)
221    { last := 0, len := 0, left := 0, have_ := 0, all := false, brk := false }
222  let mut last := st.last
223  -- used -= s->strm->avail_in;
224  used := used - (← zrd strm (·.avail_in))
225  if used != 0 then
226    let d ← ldDeflateState s
227    if used ≥ d.w_size then
228      -- s->matches = 2; zmemcpy(s->window, s->strm->next_in - s->w_size, s->w_size);
229      memcpyB d.window (← psub (← zrd strm (·.next_in)) d.w_size.toNat) d.w_size.toNat
230      -- s->strstart = s->w_size; s->insert = s->strstart;
231      wr s (fun d => { d with «matches» := 2, strstart := d.w_size, insert := d.w_size })
232    else
233      -- if (s->window_size - s->strstart <= used) { ... }
234      if d.window_size - d.strstart.toUInt64 ≤ used.toUInt64 then
235        let ss := d.strstart - d.w_size                          -- s->strstart -= s->w_size;
236        memcpyB d.window (← padd d.window d.w_size.toNat) ss.toNat -- zmemcpy(s->window, s->window + s->w_size, s->strstart);
237        wr s (fun d => { d with
238          strstart := ss,
239          «matches» := if d.«matches» < 2 then d.«matches» + 1 else d.«matches»,
240          insert := if d.insert > ss then ss else d.insert })
241      -- zmemcpy(s->window + s->strstart, s->strm->next_in - used, used);
242      let d ← ldDeflateState s
243      memcpyB (← padd d.window d.strstart.toNat) (← psub (← zrd strm (·.next_in)) used.toNat) used.toNat
244      -- s->strstart += used; s->insert += MIN(used, s->w_size - s->insert);
245      wr s (fun d => { d with strstart := d.strstart + used,
246                              insert := d.insert + MIN used (d.w_size - d.insert) })
247    -- s->block_start = s->strstart;
248    wr s (fun d => { d with block_start := d.strstart.toUInt64.toInt64 })
249  -- if (s->high_water < s->strstart) s->high_water = s->strstart;
250  wr s (fun d => { d with high_water := if d.high_water < d.strstart.toUInt64 then d.strstart.toUInt64 else d.high_water })
251  -- if (last) { s->bi_used = 8; return finish_done; }
252  if last != 0 then
253    wr s (fun d => { d with bi_used := 8 })
254    return finish_done
255  -- if (flush != Z_NO_FLUSH && flush != Z_FINISH && s->strm->avail_in == 0 && (long)s->strstart == s->block_start) return block_done;
256  let d ← ldDeflateState s
257  if flush != Z_NO_FLUSH && flush != Z_FINISH && (← zrd strm (·.avail_in)) == 0 &&
258      d.strstart.toUInt64.toInt64 == d.block_start then
259    return block_done
260  -- have = (unsigned)(s->window_size - s->strstart);
261  let mut have_ : UInt32 := (d.window_size - d.strstart.toUInt64).toUInt32
262  -- if (s->strm->avail_in > have && s->block_start >= (long)s->w_size) { ... }
263  if (← zrd strm (·.avail_in)) > have_ && d.block_start ≥ d.w_size.toUInt64.toInt64 then
264    let bs ← lsub d.block_start d.w_size.toUInt64.toInt64        -- s->block_start -= s->w_size;
265    let ss := d.strstart - d.w_size                              -- s->strstart -= s->w_size;
266    memcpyB d.window (← padd d.window d.w_size.toNat) ss.toNat
267    wr s (fun d => { d with
268      block_start := bs, strstart := ss,
269      «matches» := if d.«matches» < 2 then d.«matches» + 1 else d.«matches»,
270      insert := if d.insert > ss then ss else d.insert })
271    have_ := have_ + d.w_size                                    -- have += s->w_size;
272  -- if (have > s->strm->avail_in) have = s->strm->avail_in;
273  let ai ← zrd strm (·.avail_in)
274  if have_ > ai then have_ := ai
275  -- if (have) { read_buf(s->strm, s->window + s->strstart, have); ... }
276  if have_ != 0 then
277    let d ← ldDeflateState s
278    let _ ← read_buf strm (← padd d.window d.strstart.toNat) have_
279    wr s (fun d => { d with strstart := d.strstart + have_,
280                            insert := d.insert + MIN have_ (d.w_size - d.insert) })
281  wr s (fun d => { d with high_water := if d.high_water < d.strstart.toUInt64 then d.strstart.toUInt64 else d.high_water })
282  let d ← ldDeflateState s
283  -- have = ((unsigned)s->bi_valid + 42) >> 3;
284  have_ := (d.bi_valid.toUInt32 + 42) >>> 3
285  -- have = (unsigned)MIN(s->pending_buf_size - have, MAX_STORED);
286  have_ := (MIN (d.pending_buf_size - have_.toUInt64) MAX_STORED.toUInt64).toUInt32
287  -- min_block = MIN(have, s->w_size);
288  min_block := MIN have_ d.w_size
289  -- left = (unsigned)(s->strstart - s->block_start);
290  let left : UInt32 := (← lsub d.strstart.toUInt64.toInt64 d.block_start).toUInt64.toUInt32
291  let ai ← zrd strm (·.avail_in)
292  -- if (left >= min_block || ((left || flush == Z_FINISH) && flush != Z_NO_FLUSH && s->strm->avail_in == 0 && left <= have)) { ... }
293  if left ≥ min_block ||
294      ((left != 0 || flush == Z_FINISH) && flush != Z_NO_FLUSH && ai == 0 && left ≤ have_) then
295    let len := MIN left have_                                    -- len = MIN(left, have);
296    -- last = flush == Z_FINISH && s->strm->avail_in == 0 && len == left ? 1 : 0;
297    last := if flush == Z_FINISH && ai == 0 && len == left then 1 else 0
298    -- _tr_stored_block(s, (charf *)s->window + s->block_start, len, last);
299    _tr_stored_block s (← Ptr.add d.window d.block_start.toInt) len.toUInt64 last
300    let bs ← ladd d.block_start len.toUInt64.toInt64             -- s->block_start += len;
301    wr s (fun d => { d with block_start := bs })
302    flush_pending strm
303  -- if (last) s->bi_used = 8;
304  if last != 0 then wr s (fun d => { d with bi_used := 8 })
305  -- return last ? finish_started : need_more;
306  return if last != 0 then finish_started else need_more
307
308/-! ## `deflate_fast` -/
309
310/-- One iteration of `for (;;)` in `deflate_fast`. -/
311def deflate_fast_body (s : DeflateStatePtr) (flush : Int32) (st : LoopS) : M LoopS := do
312  -- if (s->lookahead < MIN_LOOKAHEAD) { ... }
313  if (← rd s (·.lookahead)) < MIN_LOOKAHEAD_u then
314    fill_window s
315    let la ← rd s (·.lookahead)
316    if la < MIN_LOOKAHEAD_u && flush == Z_NO_FLUSH then return { st with ret := some need_more }
317    if la == 0 then return { st with brk := true }
318  -- hash_head = NIL; if (s->lookahead >= MIN_MATCH) INSERT_STRING(s, s->strstart, hash_head);
319  let mut hash_head : UInt32 := 0
320  if (← rd s (·.lookahead)) ≥ MIN_MATCH_u then
321    hash_head ← INSERT_STRING s (← rd s (·.strstart))
322  -- if (hash_head != NIL && s->strstart - hash_head <= MAX_DIST(s)) { s->match_length = longest_match(s, hash_head); }
323  let d ← ldDeflateState s
324  if hash_head != 0 && d.strstart - hash_head ≤ d.w_size - MIN_LOOKAHEAD_u then
325    let ml ← longest_match s hash_head
326    wr s (fun d => { d with match_length := ml })
327  let d ← ldDeflateState s
328  let mut bflush := false
329  if d.match_length ≥ MIN_MATCH_u then
330    -- _tr_tally_dist(s, s->strstart - s->match_start, s->match_length - MIN_MATCH, bflush);
331    bflush ← tally_dist s (d.strstart - d.match_start) (d.match_length - MIN_MATCH_u)
332    -- s->lookahead -= s->match_length;
333    wr s (fun d => { d with lookahead := d.lookahead - d.match_length })
334    let d ← ldDeflateState s
335    -- if (s->match_length <= s->max_insert_length && s->lookahead >= MIN_MATCH) {   (max_insert_length is max_lazy_match)
336    if d.match_length ≤ d.max_lazy_match && d.lookahead ≥ MIN_MATCH_u then
337      wr s (fun d => { d with match_length := d.match_length - 1 })      -- s->match_length--;
338      -- do { s->strstart++; INSERT_STRING(s, s->strstart, hash_head); } while (--s->match_length != 0);
339      let hh ← cdoWhile
340        (fun (_ : UInt32) => do
341          wr s (fun d => { d with strstart := d.strstart + 1 })
342          INSERT_STRING s (← rd s (·.strstart)))
343        (fun hh => do
344          wr s (fun d => { d with match_length := d.match_length - 1 })
345          pure ((← rd s (·.match_length)) != 0, hh))
346        hash_head
347      hash_head := hh
348      wr s (fun d => { d with strstart := d.strstart + 1 })             -- s->strstart++;
349    else
350      -- s->strstart += s->match_length; s->match_length = 0;
351      wr s (fun d => { d with strstart := d.strstart + d.match_length, match_length := 0 })
352      -- s->ins_h = s->window[s->strstart];
353      let d ← ldDeflateState s
354      let c ← index8 d.window d.strstart.toNat
355      wr s (fun d => { d with ins_h := c.toUInt32 })
356      -- UPDATE_HASH(s, s->ins_h, s->window[s->strstart + 1]);
357      UPDATE_HASH s (← index8 d.window (d.strstart + 1).toNat)
358  else
359    -- _tr_tally_lit(s, s->window[s->strstart], bflush);
360    let c ← index8 d.window d.strstart.toNat
361    bflush ← tally_lit s c
362    wr s (fun d => { d with lookahead := d.lookahead - 1, strstart := d.strstart + 1 })
363  -- if (bflush) FLUSH_BLOCK(s, 0);
364  if bflush then
365    if let some r := (← FLUSH_BLOCK s 0) then return { st with hash_head, bflush, ret := some r }
366  return { st with hash_head, bflush }
367
368/-- `local block_state deflate_fast(deflate_state *s, int flush)` -/
369def deflate_fast (s : DeflateStatePtr) (flush : Int32) : M block_state := do
370  let st ← cwhile forever (deflate_fast_body s flush) {}
371  if let some r := st.ret then return r
372  -- s->insert = s->strstart < MIN_MATCH-1 ? s->strstart : MIN_MATCH-1;
373  wr s (fun d => { d with insert := if d.strstart < MIN_MATCH_u - 1 then d.strstart else MIN_MATCH_u - 1 })
374  finish_tail s flush
375
376/-! ## `deflate_slow` -/
377
378/-- One iteration of `for (;;)` in `deflate_slow`. -/
379def deflate_slow_body (s : DeflateStatePtr) (flush : Int32) (st : LoopS) : M LoopS := do
380  if (← rd s (·.lookahead)) < MIN_LOOKAHEAD_u then
381    fill_window s
382    let la ← rd s (·.lookahead)
383    if la < MIN_LOOKAHEAD_u && flush == Z_NO_FLUSH then return { st with ret := some need_more }
384    if la == 0 then return { st with brk := true }
385  -- hash_head = NIL; if (s->lookahead >= MIN_MATCH) INSERT_STRING(s, s->strstart, hash_head);
386  let mut hash_head : UInt32 := 0
387  if (← rd s (·.lookahead)) ≥ MIN_MATCH_u then
388    hash_head ← INSERT_STRING s (← rd s (·.strstart))
389  -- s->prev_length = s->match_length, s->prev_match = s->match_start; s->match_length = MIN_MATCH-1;
390  wr s (fun d => { d with prev_length := d.match_length, prev_match := d.match_start, match_length := MIN_MATCH_u - 1 })
391  let d ← ldDeflateState s
392  -- if (hash_head != NIL && s->prev_length < s->max_lazy_match && s->strstart - hash_head <= MAX_DIST(s)) { ... }
393  if hash_head != 0 && d.prev_length < d.max_lazy_match && d.strstart - hash_head ≤ d.w_size - MIN_LOOKAHEAD_u then
394    let ml ← longest_match s hash_head
395    wr s (fun d => { d with match_length := ml })
396    let d ← ldDeflateState s
397    -- if (s->match_length <= 5 && (s->strategy == Z_FILTERED || (s->match_length == MIN_MATCH && s->strstart - s->match_start > TOO_FAR)))
398    if d.match_length ≤ 5 && (d.strategy == Z_FILTERED ||
399        (d.match_length == MIN_MATCH_u && d.strstart - d.match_start > TOO_FAR)) then
400      wr s (fun d => { d with match_length := MIN_MATCH_u - 1 })
401  let d ← ldDeflateState s
402  let mut bflush := false
403  -- if (s->prev_length >= MIN_MATCH && s->match_length <= s->prev_length) { ... }
404  if d.prev_length ≥ MIN_MATCH_u && d.match_length ≤ d.prev_length then
405    -- uInt max_insert = s->strstart + s->lookahead - MIN_MATCH;
406    let max_insert : UInt32 := d.strstart + d.lookahead - MIN_MATCH_u
407    -- _tr_tally_dist(s, s->strstart - 1 - s->prev_match, s->prev_length - MIN_MATCH, bflush);
408    bflush ← tally_dist s (d.strstart - 1 - d.prev_match) (d.prev_length - MIN_MATCH_u)
409    -- s->lookahead -= s->prev_length - 1; s->prev_length -= 2;
410    wr s (fun d => { d with lookahead := d.lookahead - (d.prev_length - 1), prev_length := d.prev_length - 2 })
411    -- do { if (++s->strstart <= max_insert) { INSERT_STRING(s, s->strstart, hash_head); } } while (--s->prev_length != 0);
412    let hh ← cdoWhile
413      (fun (hh : UInt32) => do
414        wr s (fun d => { d with strstart := d.strstart + 1 })
415        let ss ← rd s (·.strstart)
416        if ss ≤ max_insert then INSERT_STRING s ss else pure hh)
417      (fun hh => do
418        wr s (fun d => { d with prev_length := d.prev_length - 1 })
419        pure ((← rd s (·.prev_length)) != 0, hh))
420      hash_head
421    hash_head := hh
422    -- s->match_available = 0; s->match_length = MIN_MATCH-1; s->strstart++;
423    wr s (fun d => { d with match_available := 0, match_length := MIN_MATCH_u - 1, strstart := d.strstart + 1 })
424    -- if (bflush) FLUSH_BLOCK(s, 0);
425    if bflush then
426      if let some r := (← FLUSH_BLOCK s 0) then return { st with hash_head, bflush, ret := some r }
427  else if d.match_available != 0 then
428    -- _tr_tally_lit(s, s->window[s->strstart - 1], bflush);
429    let c ← index8 d.window (d.strstart - 1).toNat
430    bflush ← tally_lit s c
431    -- if (bflush) { FLUSH_BLOCK_ONLY(s, 0); }
432    if bflush then FLUSH_BLOCK_ONLY s 0
433    -- s->strstart++; s->lookahead--;
434    wr s (fun d => { d with strstart := d.strstart + 1, lookahead := d.lookahead - 1 })
435    -- if (s->strm->avail_out == 0) return need_more;
436    if (← zrd d.strm (·.avail_out)) == 0 then return { st with hash_head, bflush, ret := some need_more }
437  else
438    -- s->match_available = 1; s->strstart++; s->lookahead--;
439    wr s (fun d => { d with match_available := 1, strstart := d.strstart + 1, lookahead := d.lookahead - 1 })
440  return { st with hash_head, bflush }
441
442/-- `local block_state deflate_slow(deflate_state *s, int flush)` -/
443def deflate_slow (s : DeflateStatePtr) (flush : Int32) : M block_state := do
444  let st ← cwhile forever (deflate_slow_body s flush) {}
445  if let some r := st.ret then return r
446  -- if (s->match_available) { _tr_tally_lit(s, s->window[s->strstart - 1], bflush); s->match_available = 0; }
447  let d ← ldDeflateState s
448  if d.match_available != 0 then
449    let c ← index8 d.window (d.strstart - 1).toNat
450    let _ ← tally_lit s c
451    wr s (fun d => { d with match_available := 0 })
452  -- s->insert = s->strstart < MIN_MATCH-1 ? s->strstart : MIN_MATCH-1;
453  wr s (fun d => { d with insert := if d.strstart < MIN_MATCH_u - 1 then d.strstart else MIN_MATCH_u - 1 })
454  finish_tail s flush
455
456/-! ## `deflate_rle` -/
457
458/-- One iteration of `for (;;)` in `deflate_rle`. -/
459def deflate_rle_body (s : DeflateStatePtr) (flush : Int32) (st : LoopS) : M LoopS := do
460  -- if (s->lookahead <= MAX_MATCH) { ... }
461  if (← rd s (·.lookahead)) ≤ MAX_MATCH_u then
462    fill_window s
463    let la ← rd s (·.lookahead)
464    if la ≤ MAX_MATCH_u && flush == Z_NO_FLUSH then return { st with ret := some need_more }
465    if la == 0 then return { st with brk := true }
466  -- s->match_length = 0;
467  wr s (fun d => { d with match_length := 0 })
468  let d ← ldDeflateState s
469  -- if (s->lookahead >= MIN_MATCH && s->strstart > 0) { ... }
470  if d.lookahead ≥ MIN_MATCH_u && d.strstart > 0 then
471    -- scan = s->window + s->strstart - 1; prev = *scan;
472    let mut scan ← psub (← padd d.window d.strstart.toNat) 1
473    let prev : UInt32 := (← load8 scan).toUInt32
474    -- if (prev == *++scan && prev == *++scan && prev == *++scan) { ... }
475    scan ← padd scan 1
476    let mut ok := prev == (← load8 scan).toUInt32
477    if ok then
478      scan ← padd scan 1
479      ok := prev == (← load8 scan).toUInt32
480    if ok then
481      scan ← padd scan 1
482      ok := prev == (← load8 scan).toUInt32
483    if ok then
484      -- strend = s->window + s->strstart + MAX_MATCH;
485      let strend ← padd (← padd d.window d.strstart.toNat) MAX_MATCH_u.toNat
486      -- do { } while (prev == *++scan && ... (8 times) && scan < strend);
487      let scan2 ← cdoWhile (fun x => pure x)
488        (fun scan => do
489          let mut scan := scan
490          for _ in [0:8] do
491            scan ← padd scan 1
492            if prev != (← load8 scan).toUInt32 then return (false, scan)
493          return (← Ptr.lt scan strend, scan))
494        scan
495      -- s->match_length = MAX_MATCH - (uInt)(strend - scan);
496      let diff ← Ptr.diff strend scan2
497      let ml : UInt32 := MAX_MATCH_u - diff.toUInt64.toUInt32
498      wr s (fun d => { d with match_length := ml })
499      -- if (s->match_length > s->lookahead) s->match_length = s->lookahead;
500      wr s (fun d => { d with match_length := if d.match_length > d.lookahead then d.lookahead else d.match_length })
501  let d ← ldDeflateState s
502  let mut bflush := false
503  -- if (s->match_length >= MIN_MATCH) { ... } else { ... }
504  if d.match_length ≥ MIN_MATCH_u then
505    bflush ← tally_dist s 1 (d.match_length - MIN_MATCH_u)      -- _tr_tally_dist(s, 1, s->match_length - MIN_MATCH, bflush);
506    wr s (fun d => { d with lookahead := d.lookahead - d.match_length,
507                            strstart := d.strstart + d.match_length, match_length := 0 })
508  else
509    let c ← index8 d.window d.strstart.toNat
510    bflush ← tally_lit s c
511    wr s (fun d => { d with lookahead := d.lookahead - 1, strstart := d.strstart + 1 })
512  if bflush then
513    if let some r := (← FLUSH_BLOCK s 0) then return { st with bflush, ret := some r }
514  return { st with bflush }
515
516/-- `local block_state deflate_rle(deflate_state *s, int flush)` -/
517def deflate_rle (s : DeflateStatePtr) (flush : Int32) : M block_state := do
518  let st ← cwhile forever (deflate_rle_body s flush) {}
519  if let some r := st.ret then return r
520  wr s (fun d => { d with insert := 0 })                         -- s->insert = 0;
521  finish_tail s flush
522
523/-! ## `deflate_huff` -/
524
525/-- One iteration of `for (;;)` in `deflate_huff`. -/
526def deflate_huff_body (s : DeflateStatePtr) (flush : Int32) (st : LoopS) : M LoopS := do
527  -- if (s->lookahead == 0) { fill_window(s); if (s->lookahead == 0) { if (flush == Z_NO_FLUSH) return need_more; break; } }
528  if (← rd s (·.lookahead)) == 0 then
529    fill_window s
530    if (← rd s (·.lookahead)) == 0 then
531      if flush == Z_NO_FLUSH then return { st with ret := some need_more }
532      return { st with brk := true }
533  -- s->match_length = 0;
534  wr s (fun d => { d with match_length := 0 })
535  -- _tr_tally_lit(s, s->window[s->strstart], bflush);
536  let d ← ldDeflateState s
537  let c ← index8 d.window d.strstart.toNat
538  let bflush ← tally_lit s c
539  wr s (fun d => { d with lookahead := d.lookahead - 1, strstart := d.strstart + 1 })
540  if bflush then
541    if let some r := (← FLUSH_BLOCK s 0) then return { st with bflush, ret := some r }
542  return { st with bflush }
543
544/-- `local block_state deflate_huff(deflate_state *s, int flush)` -/
545def deflate_huff (s : DeflateStatePtr) (flush : Int32) : M block_state := do
546  let st ← cwhile forever (deflate_huff_body s flush) {}
547  if let some r := st.ret then return r
548  wr s (fun d => { d with insert := 0 })                         -- s->insert = 0;
549  finish_tail s flush
550
551end Zlib.Deflate