REFERENCE / ZLIB × LEAN
deflate_strategies.c.lean
Source snapshot ·
07fbe6f737b69791 · Source at the matching commit ↗Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.
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