zlib.bend
bend-kit-zlib@0.1.3.0 · 1,227 lines · 0 definitions
1# DEFLATE, gzip, and zlib encoding and decoding (RFC 1951, 1952, 1950) over byte strings, plus gzip, zstd, and brotli through the C libraries. Source: https://github.com/paymog/bend-kit/tree/main/zlib
2import Base
3
4# Bytes are one Char per octet (0..255), as everywhere in bend-kit.
5
6def byte(h: Char) -> U32:
7 Chr{c} = h
8 c
9
10def bits(+n: U32) -> Nat:
11 U32.to_nat(n)
12
13def mask(+n: U32) -> U32:
14 (U32.shln(1, bits(n)) - 1 : U32)
15
16# Bit reader. over counts bytes read past the end; any over means the input was cut short.
17type Br is Data:
18 Br{s: String, buf: U32, cnt: U32, over: U32}
19
20def br.new(s: String) -> Br:
21 Br{s, 0, 0, 0}
22
23def br.pull(b: Br) -> Br:
24 Br{s, +buf, +cnt, +over} = b
25 match s:
26 case SNil{}:
27 Br{SNil{}, buf, (cnt + 8 : U32), (over + 1 : U32)}
28 case SCon{h, t}:
29 Br{t, U32.or(buf, U32.shln(byte(h), bits(cnt))), (cnt + 8 : U32), over}
30
31def br.pull.if(b: Br, short: Bool) -> Br:
32 match short:
33 case True{}:
34 br.pull(b)
35 case False{}:
36 b
37
38def br.short(+b: Br, +n: U32) -> Bool:
39 Br{s, buf, +cnt, over} = b
40 U32.is_lt(cnt, n)
41
42# n is at most 16, so three bytes always fill the buffer.
43def br.fill(fuel: Nat, +b: Br, +n: U32) -> Br:
44 match fuel:
45 case 0n:
46 b
47 case 1n+f:
48 br.fill(f, br.pull.if(b, br.short(b, n)), n)
49
50def br.cut(b: Br, +n: U32) -> Br & U32:
51 Br{s, +buf, cnt, over} = b
52 (Br{s, U32.shrn(buf, bits(n)), (cnt - n : U32), over}, U32.and(buf, mask(n)))
53
54def br.take(b: Br, +n: U32) -> Br & U32:
55 br.cut(br.fill(3n, b, n), n)
56
57def br.drop.of(r: Br & U32) -> Br:
58 (b, v) = r
59 b
60
61def br.drop(b: Br, +n: U32) -> Br:
62 br.drop.of(br.cut(b, n))
63
64# RFC 1951 §3.2.4: a stored block starts on a byte boundary.
65def br.align(+b: Br) -> Br:
66 Br{s, buf, +cnt, over} = b
67 br.drop(b, U32.mod(cnt, 8))
68
69def br.ok(+b: Br) -> Bool:
70 Br{s, buf, cnt, +over} = b
71 U32.is_eq(over, 0)
72
73def br.bytes(k: Nat, +buf: U32) -> String:
74 match k:
75 case 0n:
76 SNil{}
77 case 1n+p:
78 SCon{Chr{U32.and(buf, 255)}, br.bytes(p, U32.shrn(buf, 8n))}
79
80def br.rest.of(b: Br) -> String:
81 Br{s, +buf, +cnt, over} = b
82 br.bytes(bits(U32.div(cnt, 8)), buf) ++ s
83
84# Whole bytes still in the buffer go back in front of the unread input.
85def br.rest(+b: Br) -> String:
86 br.rest.of(br.align(b))
87
88# Huffman codes as a trie: one step per bit. A read bit picks o (1) or z (0).
89# Bad: two codes collided, so the code set was over-subscribed.
90type Ht is Data:
91 HtNone{}
92 HtBad{}
93 HtLeaf{sym: U32}
94 HtNode{z: Ht, o: Ht}
95
96def ht.left(t: Ht) -> Ht:
97 match t:
98 case HtNode{z, o}:
99 z
100 case HtNone{}:
101 HtNone{}
102 case HtBad{}:
103 HtBad{}
104 case HtLeaf{s}:
105 HtBad{}
106
107def ht.right(t: Ht) -> Ht:
108 match t:
109 case HtNode{z, o}:
110 o
111 case HtNone{}:
112 HtNone{}
113 case HtBad{}:
114 HtBad{}
115 case HtLeaf{s}:
116 HtBad{}
117
118def ht.leaf(t: Ht, +sym: U32) -> Ht:
119 match t:
120 case HtNone{}:
121 HtLeaf{sym}
122 case HtBad{}:
123 HtBad{}
124 case HtLeaf{s}:
125 HtBad{}
126 case HtNode{z, o}:
127 HtBad{}
128
129def ht.ins(path: List<&2, Bool>, +t: Ht, +sym: U32) -> Ht:
130 match path:
131 case Nil{}:
132 ht.leaf(t, sym)
133 case Con{b, rest}:
134 match b:
135 case True{}:
136 HtNode{ht.left(t), ht.ins(rest, ht.right(t), sym)}
137 case False{}:
138 HtNode{ht.ins(rest, ht.left(t), sym), ht.right(t)}
139
140# The code's bits, most significant first: the order the stream sends them.
141def ht.path(n: Nat, +code: U32, acc: List<&2, Bool>) -> List<&2, Bool>:
142 match n:
143 case 0n:
144 acc
145 case 1n+p:
146 ht.path(p, U32.shr(code), Con{U32.is_eq(U32.and(code, 1), 1), acc})
147
148# Canonical codes (RFC 1951 §3.2.2): count lengths, find each length's first code, then assign in symbol order.
149def cnt.add(ar: Array<U32> & U32, +len: U32) -> Array<U32>:
150 (a, v) = ar
151 Array.set(U32, a, len, (v + 1 : U32))
152
153def cnt.go(xs: List<&2, U32>, a: Array<U32>) -> Array<U32>:
154 match xs:
155 case Nil{}:
156 a
157 case Con{+l, t}:
158 cnt.go(t, cnt.add(Array.get(U32, a, l), l))
159
160def nx.set(+i: U32, cv: Array<U32> & U32, n: Array<U32>, +code: U32) -> Array<U32> & Array<U32> & U32:
161 (c, v) = cv
162 +code2 = U32.shl((code + Bool.pick(U32, U32.is_eq(i, 1), 0, v) : U32))
163 (c, Array.set(U32, n, i, code2), code2)
164
165def nx.step(+i: U32, st: Array<U32> & Array<U32> & U32) -> Array<U32> & Array<U32> & U32:
166 (c, n, code) = st
167 nx.set(i, Array.get(U32, c, (i - 1 : U32)), n, code)
168
169def nx.go(k: Nat, +i: U32, st: Array<U32> & Array<U32> & U32) -> Array<U32> & Array<U32> & U32:
170 match k:
171 case 0n:
172 st
173 case 1n+f:
174 nx.go(f, (i + 1 : U32), nx.step(i, st))
175
176def as.put(+l: U32, +sym: U32, nv: Array<U32> & U32, t: Ht) -> Array<U32> & Ht:
177 (n, +code) = nv
178 (Array.set(U32, n, l, (code + 1 : U32)), ht.ins(ht.path(bits(l), code, Nil{}), t, sym))
179
180def as.one.nz(+l: U32, +sym: U32, n: Array<U32>, t: Ht, zero: Bool) -> Array<U32> & Ht:
181 match zero:
182 case True{}:
183 (n, t)
184 case False{}:
185 as.put(l, sym, Array.get(U32, n, l), t)
186
187def as.one(+l: U32, +sym: U32, st: Array<U32> & Ht) -> Array<U32> & Ht:
188 (n, t) = st
189 as.one.nz(l, sym, n, t, U32.is_zero(l))
190
191def as.go(xs: List<&2, U32>, +sym: U32, st: Array<U32> & Ht) -> Array<U32> & Ht:
192 match xs:
193 case Nil{}:
194 st
195 case Con{+l, t}:
196 as.go(t, (sym + 1 : U32), as.one(l, sym, st))
197
198def ht.of(st: Array<U32> & Ht) -> Ht:
199 (n, t) = st
200 t
201
202def ht.assign(xs: List<&2, U32>, st: Array<U32> & Array<U32> & U32) -> Ht:
203 (c, n, code) = st
204 ht.of(as.go(xs, 0, (n, HtNone{})))
205
206# lens[i] is the code length of symbol i; 0 means the symbol is unused.
207def ht.build(+lens: List<&2, U32>) -> Ht:
208 ht.assign(lens, nx.go(15n, 1, (cnt.go(lens, Array.new(U32, 4n, 0)), Array.new(U32, 4n, 0), 0)))
209
210# No code: 9999, never a symbol.
211def ht.step(z: Ht, o: Ht, bv: Br & U32) -> Ht & Br:
212 (b, +v) = bv
213 (Bool.pick(Ht, U32.is_eq(v, 1), o, z), b)
214
215# A code is at most 15 bits (§3.2.7), so 16 steps always reach a leaf or a miss.
216def ht.dec(fuel: Nat, st: Ht & Br) -> Br & U32:
217 match fuel:
218 case 0n:
219 (t, b) = st
220 (b, 9999)
221 case 1n+f:
222 (t, b) = st
223 match t:
224 case HtLeaf{s}:
225 (b, s)
226 case HtNone{}:
227 (b, 9999)
228 case HtBad{}:
229 (b, 9999)
230 case HtNode{z, o}:
231 ht.dec(f, ht.step(z, o, br.take(b, 1)))
232
233def ht.decode(t: Ht, b: Br) -> Br & U32:
234 ht.dec(16n, (t, b))
235
236def nth(xs: List<&2, U32>, +i: U32) -> U32:
237 match xs:
238 case Nil{}:
239 0
240 case Con{h, t}:
241 Bool.pick(U32, U32.is_zero(i), h, nth(t, (i - 1 : U32)))
242
243def rep(k: Nat, +v: U32, acc: List<&2, U32>) -> List<&2, U32>:
244 match k:
245 case 0n:
246 acc
247 case 1n+p:
248 rep(p, v, Con{v, acc})
249
250def take.n(k: Nat, xs: List<&2, U32>) -> List<&2, U32>:
251 match k:
252 case 0n:
253 Nil{}
254 case 1n+p:
255 match xs:
256 case Nil{}:
257 Nil{}
258 case Con{h, t}:
259 Con{h, take.n(p, t)}
260
261def drop.n(k: Nat, xs: List<&2, U32>) -> List<&2, U32>:
262 match k:
263 case 0n:
264 xs
265 case 1n+p:
266 match xs:
267 case Nil{}:
268 Nil{}
269 case Con{h, t}:
270 drop.n(p, t)
271
272# RFC 1951 §3.2.5
273def len.base() -> List<&2, U32>:
274 [3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 15, 17, 19, 23, 27, 31, 35, 43, 51, 59, 67, 83, 99, 115, 131, 163, 195, 227, 258]
275
276def len.extra() -> List<&2, U32>:
277 [0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4, 5, 5, 5, 5, 0]
278
279def dist.base() -> List<&2, U32>:
280 [1, 2, 3, 4, 5, 7, 9, 13, 17, 25, 33, 49, 65, 97, 129, 193, 257, 385, 513, 769, 1025, 1537, 2049, 3073, 4097, 6145, 8193, 12289, 16385, 24577]
281
282def dist.extra() -> List<&2, U32>:
283 [0, 0, 0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 10, 11, 11, 12, 12, 13, 13]
284
285# RFC 1951 §3.2.6
286def fixed.lit() -> Ht:
287 ht.build(rep(144n, 8, rep(112n, 9, rep(24n, 7, rep(8n, 8, Nil{})))))
288
289def fixed.dist() -> Ht:
290 ht.build(rep(30n, 5, Nil{}))
291
292# Output: the 32 KiB window (indexes wrap), the write position, the byte count, and the bytes, reversed.
293type Ow is Data:
294 Ow{w: U32, n: U32, racc: String}
295
296def out.put(win: Array<U32>, +c: U32, o: Ow) -> Array<U32> & Ow:
297 Ow{+w, +n, racc} = o
298 (Array.set(U32, win, w, c), Ow{(w + 1 : U32), (n + 1 : U32), SCon{Chr{c}, racc}})
299
300type Mo is Data:
301 MoHead{}
302 MoCodes{lit: Ht, dist: Ht}
303 MoDone{}
304 MoBad{}
305
306type Is is Data:
307 Is{br: Br, o: Ow, mode: Mo, last: Bool}
308
309def inf.next(last: Bool) -> Mo:
310 match last:
311 case True{}:
312 MoDone{}
313 case False{}:
314 MoHead{}
315
316def inf.bad(win: Array<U32>, b: Br, o: Ow) -> Array<U32> & Is:
317 (win, Is{b, o, MoBad{}, True{}})
318
319# Stored block (§3.2.4): LEN, then NLEN (its complement), then LEN raw bytes.
320def sb.put2(p: Array<U32> & Ow, b: Br) -> Array<U32> & Br & Ow:
321 (a, o) = p
322 (a, b, o)
323
324def sb.put(win: Array<U32>, bv: Br & U32, o: Ow) -> Array<U32> & Br & Ow:
325 (b, +c) = bv
326 sb.put2(out.put(win, c, o), b)
327
328def sb.byte(st: Array<U32> & Br & Ow) -> Array<U32> & Br & Ow:
329 (win, b, o) = st
330 sb.put(win, br.take(b, 8), o)
331
332def sb.go(k: Nat, st: Array<U32> & Br & Ow) -> Array<U32> & Br & Ow:
333 match k:
334 case 0n:
335 st
336 case 1n+f:
337 sb.go(f, sb.byte(st))
338
339def sb.done(t: Array<U32> & Br & Ow, +last: Bool) -> Array<U32> & Is:
340 (win, b, o) = t
341 (win, Is{b, o, inf.next(last), last})
342
343def sb.ok(win: Array<U32>, b: Br, +len: U32, o: Ow, +last: Bool, ok: Bool) -> Array<U32> & Is:
344 match ok:
345 case False{}:
346 inf.bad(win, b, o)
347 case True{}:
348 sb.done(sb.go(bits(len), (win, b, o)), last)
349
350def sb.nlen(win: Array<U32>, bv: Br & U32, +len: U32, o: Ow, +last: Bool) -> Array<U32> & Is:
351 (b, +nlen) = bv
352 sb.ok(win, b, len, o, last, U32.is_eq(U32.xor(len, 65535), nlen))
353
354def sb.len(win: Array<U32>, bv: Br & U32, o: Ow, +last: Bool) -> Array<U32> & Is:
355 (b, +len) = bv
356 sb.nlen(win, br.take(b, 16), len, o, last)
357
358def inf.stored(win: Array<U32>, b: Br, o: Ow, +last: Bool) -> Array<U32> & Is:
359 sb.len(win, br.take(br.align(b), 16), o, last)
360
361# Dynamic block (§3.2.7): code lengths for the code-length code, then the lengths themselves.
362# cl.slot[i]: where symbol i's length sits in the order the stream sends them.
363def cl.slot() -> List<&2, U32>:
364 [3, 17, 15, 13, 11, 9, 7, 5, 4, 6, 8, 10, 12, 14, 16, 18, 0, 1, 2]
365
366def cl.place(xs: List<&2, U32>, +vals: List<&2, U32>) -> List<&2, U32>:
367 match xs:
368 case Nil{}:
369 Nil{}
370 case Con{+i, t}:
371 Con{nth(vals, i), cl.place(t, vals)}
372
373def cl.push(bv: Br & U32, acc: List<&2, U32>) -> Br & List<&2, U32>:
374 (b, v) = bv
375 (b, Con{v, acc})
376
377def cl.one(st: Br & List<&2, U32>) -> Br & List<&2, U32>:
378 (b, acc) = st
379 cl.push(br.take(b, 3), acc)
380
381def cl.read(k: Nat, st: Br & List<&2, U32>) -> Br & List<&2, U32>:
382 match k:
383 case 0n:
384 st
385 case 1n+f:
386 cl.read(f, cl.one(st))
387
388# Lengths so far (reversed), how many, the last one (for code 16), and whether it went wrong.
389type Cd is Data:
390 Cd{br: Br, acc: List<&2, U32>, n: U32, prev: U32, bad: Bool}
391
392def cd.fill(+b: Br, +acc: List<&2, U32>, +n: U32, +v: U32, +cnt: U32, +total: U32) -> Cd:
393 Bool.pick(Cd, U32.is_lt(total, (n + cnt : U32)), Cd{b, acc, n, v, True{}}, Cd{b, rep(bits(cnt), v, acc), (n + cnt : U32), v, False{}})
394
395def cd.rep(bv: Br & U32, +v: U32, +base: U32, acc: List<&2, U32>, +n: U32, +total: U32) -> Cd:
396 (b, +e) = bv
397 cd.fill(b, acc, n, v, (base + e : U32), total)
398
399def cd.prev(b: Br, acc: List<&2, U32>, +n: U32, +prev: U32, +total: U32, ok: Bool) -> Cd:
400 match ok:
401 case False{}:
402 Cd{b, acc, n, prev, True{}}
403 case True{}:
404 cd.rep(br.take(b, 2), prev, 3, acc, n, total)
405
406def cd.z18(b: Br, acc: List<&2, U32>, +n: U32, +total: U32, ok: Bool) -> Cd:
407 match ok:
408 case True{}:
409 cd.rep(br.take(b, 7), 0, 11, acc, n, total)
410 case False{}:
411 Cd{b, acc, n, 0, True{}}
412
413def cd.z17(b: Br, acc: List<&2, U32>, +n: U32, +s: U32, +total: U32, ok: Bool) -> Cd:
414 match ok:
415 case True{}:
416 cd.rep(br.take(b, 3), 0, 3, acc, n, total)
417 case False{}:
418 cd.z18(b, acc, n, total, U32.is_eq(s, 18))
419
420def cd.c16(b: Br, acc: List<&2, U32>, +n: U32, +prev: U32, +s: U32, +total: U32, ok: Bool) -> Cd:
421 match ok:
422 case True{}:
423 cd.prev(b, acc, n, prev, total, U32.is_lt(0, n))
424 case False{}:
425 cd.z17(b, acc, n, s, total, U32.is_eq(s, 17))
426
427def cd.lit(b: Br, acc: List<&2, U32>, +n: U32, +prev: U32, +s: U32, +total: U32, ok: Bool) -> Cd:
428 match ok:
429 case True{}:
430 Cd{b, Con{s, acc}, (n + 1 : U32), s, False{}}
431 case False{}:
432 cd.c16(b, acc, n, prev, s, total, U32.is_eq(s, 16))
433
434def cd.sym(bv: Br & U32, acc: List<&2, U32>, +n: U32, +prev: U32, +total: U32) -> Cd:
435 (b, +s) = bv
436 cd.lit(b, acc, n, prev, s, total, U32.is_lt(s, 16))
437
438def cd.step.go(+cl: Ht, +total: U32, stop: Bool, cs: Cd) -> Cd:
439 match stop:
440 case False{}:
441 Cd{b, acc, +n, +prev, bad} = cs
442 cd.sym(ht.decode(cl, b), acc, n, prev, total)
443 case True{}:
444 Cd{b, acc, n, prev, bad} = cs
445 Cd{b, acc, n, prev, bad}
446
447def cd.stop(+st: Cd, +total: U32) -> Bool:
448 Cd{b, acc, +n, prev, +bad} = st
449 Bool.or(bad, U32.is_le(total, n))
450
451# Each step adds at least one length, so total steps suffice.
452def cd.go(k: Nat, +cl: Ht, +total: U32, +st: Cd) -> Cd:
453 match k:
454 case 0n:
455 st
456 case 1n+f:
457 cd.go(f, cl, total, cd.step.go(cl, total, cd.stop(st, total), st))
458
459def dyn.tables(b: Br, +lens: List<&2, U32>, +hlit: U32, bad: Bool) -> Br & Mo:
460 match bad:
461 case True{}:
462 (b, MoBad{})
463 case False{}:
464 (b, MoCodes{ht.build(take.n(bits(hlit), lens)), ht.build(drop.n(bits(hlit), lens))})
465
466def dyn.done(st: Cd, +hlit: U32, +total: U32) -> Br & Mo:
467 Cd{b, acc, +n, prev, +bad} = st
468 dyn.tables(b, List.reverse(&2, U32, acc), hlit, Bool.or(bad, Bool.not(U32.is_eq(n, total))))
469
470def dyn.lens(st: Br & List<&2, U32>, +hlit: U32, +hdist: U32) -> Br & Mo:
471 (b, acc) = st
472 +total = (hlit + hdist : U32)
473 +clens = cl.place(cl.slot(), List.reverse(&2, U32, acc))
474 dyn.done(cd.go(bits(total), ht.build(clens), total, Cd{b, Nil{}, 0, 0, False{}}), hlit, total)
475
476def dyn.clen(bv: Br & U32, +hlit: U32, +hdist: U32) -> Br & Mo:
477 (b, +hclen) = bv
478 dyn.lens(cl.read(bits((hclen + 4 : U32)), (b, Nil{})), hlit, hdist)
479
480def dyn.hdist(bv: Br & U32, +hlit: U32) -> Br & Mo:
481 (b, +hd) = bv
482 dyn.clen(br.take(b, 4), hlit, (hd + 1 : U32))
483
484def dyn.hlit(bv: Br & U32) -> Br & Mo:
485 (b, +hl) = bv
486 dyn.hdist(br.take(b, 5), (hl + 257 : U32))
487
488def dyn.read(b: Br) -> Br & Mo:
489 dyn.hlit(br.take(b, 5))
490
491# A match copies len bytes from d back; the window's indexes wrap, so w - d needs no mask.
492def cp.put(av: Array<U32> & U32, o: Ow) -> Array<U32> & Ow:
493 (a, +c) = av
494 out.put(a, c, o)
495
496def cp.one(+d: U32, st: Array<U32> & Ow) -> Array<U32> & Ow:
497 (win, o) = st
498 Ow{+w, n, racc} = o
499 cp.put(Array.get(U32, win, (w - d : U32)), Ow{w, n, racc})
500
501def cp.go(k: Nat, +d: U32, st: Array<U32> & Ow) -> Array<U32> & Ow:
502 match k:
503 case 0n:
504 st
505 case 1n+f:
506 cp.go(f, d, cp.one(d, st))
507
508def inf.codes(p: Array<U32> & Ow, b: Br, +lit: Ht, +dist: Ht, +last: Bool) -> Array<U32> & Is:
509 (win, o) = p
510 (win, Is{b, o, MoCodes{lit, dist}, last})
511
512def ow.n(+o: Ow) -> U32:
513 Ow{w, +n, racc} = o
514 n
515
516# RFC 1951 §3.2.5: a distance may not reach before the first byte out.
517def inf.far(win: Array<U32>, b: Br, +o: Ow, +len: U32, +d: U32, +lit: Ht, +dist: Ht, +last: Bool, ok: Bool) -> Array<U32> & Is:
518 match ok:
519 case False{}:
520 inf.bad(win, b, o)
521 case True{}:
522 inf.codes(cp.go(bits(len), d, (win, o)), b, lit, dist, last)
523
524def inf.dx(win: Array<U32>, bv: Br & U32, +db: U32, +len: U32, +o: Ow, +lit: Ht, +dist: Ht, +last: Bool) -> Array<U32> & Is:
525 (b, +e) = bv
526 +d = (db + e : U32)
527 inf.far(win, b, o, len, d, lit, dist, last, U32.is_le(d, ow.n(o)))
528
529def inf.ds(win: Array<U32>, b: Br, +ds: U32, +len: U32, +o: Ow, +lit: Ht, +dist: Ht, +last: Bool, ok: Bool) -> Array<U32> & Is:
530 match ok:
531 case False{}:
532 inf.bad(win, b, o)
533 case True{}:
534 inf.dx(win, br.take(b, nth(dist.extra(), ds)), nth(dist.base(), ds), len, o, lit, dist, last)
535
536def inf.d(win: Array<U32>, bv: Br & U32, +len: U32, +o: Ow, +lit: Ht, +dist: Ht, +last: Bool) -> Array<U32> & Is:
537 (b, +ds) = bv
538 inf.ds(win, b, ds, len, o, lit, dist, last, U32.is_lt(ds, 30))
539
540def inf.lx(win: Array<U32>, bv: Br & U32, +lb: U32, +o: Ow, +lit: Ht, +dist: Ht, +last: Bool) -> Array<U32> & Is:
541 (b, +e) = bv
542 inf.d(win, ht.decode(dist, b), (lb + e : U32), o, lit, dist, last)
543
544def inf.ls(win: Array<U32>, b: Br, +s: U32, +o: Ow, +lit: Ht, +dist: Ht, +last: Bool, ok: Bool) -> Array<U32> & Is:
545 match ok:
546 case False{}:
547 inf.bad(win, b, o)
548 case True{}:
549 +i = (s - 257 : U32)
550 inf.lx(win, br.take(b, nth(len.extra(), i)), nth(len.base(), i), o, lit, dist, last)
551
552def inf.end(win: Array<U32>, b: Br, +s: U32, +o: Ow, +lit: Ht, +dist: Ht, +last: Bool, eob: Bool) -> Array<U32> & Is:
553 match eob:
554 case True{}:
555 (win, Is{b, o, inf.next(last), last})
556 case False{}:
557 inf.ls(win, b, s, o, lit, dist, last, U32.is_le(s, 285))
558
559def inf.lit(win: Array<U32>, b: Br, +s: U32, +o: Ow, +lit: Ht, +dist: Ht, +last: Bool, ok: Bool) -> Array<U32> & Is:
560 match ok:
561 case True{}:
562 inf.codes(out.put(win, s, o), b, lit, dist, last)
563 case False{}:
564 inf.end(win, b, s, o, lit, dist, last, U32.is_eq(s, 256))
565
566def inf.sym(win: Array<U32>, bv: Br & U32, +o: Ow, +lit: Ht, +dist: Ht, +last: Bool) -> Array<U32> & Is:
567 (b, +s) = bv
568 inf.lit(win, b, s, o, lit, dist, last, U32.is_lt(s, 256))
569
570def inf.dyn(win: Array<U32>, bm: Br & Mo, o: Ow, +last: Bool) -> Array<U32> & Is:
571 (b, m) = bm
572 (win, Is{b, o, m, last})
573
574def inf.t2(win: Array<U32>, b: Br, o: Ow, +last: Bool, is2: Bool) -> Array<U32> & Is:
575 match is2:
576 case True{}:
577 inf.dyn(win, dyn.read(b), o, last)
578 case False{}:
579 inf.bad(win, b, o)
580
581def inf.t1(win: Array<U32>, b: Br, o: Ow, +last: Bool, +t: U32, is1: Bool) -> Array<U32> & Is:
582 match is1:
583 case True{}:
584 (win, Is{b, o, MoCodes{fixed.lit(), fixed.dist()}, last})
585 case False{}:
586 inf.t2(win, b, o, last, U32.is_eq(t, 2))
587
588def inf.t0(win: Array<U32>, b: Br, o: Ow, +last: Bool, +t: U32, is0: Bool) -> Array<U32> & Is:
589 match is0:
590 case True{}:
591 inf.stored(win, b, o, last)
592 case False{}:
593 inf.t1(win, b, o, last, t, U32.is_eq(t, 1))
594
595# §3.2.3: BFINAL, then BTYPE.
596def inf.head(win: Array<U32>, bv: Br & U32, o: Ow) -> Array<U32> & Is:
597 (b, +v) = bv
598 +t = U32.shr(v)
599 inf.t0(win, b, o, U32.is_eq(U32.and(v, 1), 1), t, U32.is_zero(t))
600
601# Every step reads at least one bit, so 8 steps per input byte always finish a valid stream.
602def inf.go(k: Nat, st: Array<U32> & Is) -> Array<U32> & Is:
603 match k:
604 case 0n:
605 st
606 case 1n+f:
607 (win, ist) = st
608 Is{b, o, mode, +last} = ist
609 match mode:
610 case MoHead{}:
611 inf.go(f, inf.head(win, br.take(b, 3), o))
612 case MoCodes{+lit, +dist}:
613 inf.go(f, inf.sym(win, ht.decode(lit, b), o, lit, dist, last))
614 case MoDone{}:
615 (win, Is{b, o, MoDone{}, last})
616 case MoBad{}:
617 (win, Is{b, o, MoBad{}, last})
618
619# out: the bytes; rest: the input after the stream; n: len(out) mod 2^32.
620type Inflated is Data:
621 Inflated{out: String, rest: String, n: U32}
622
623def inf.fin(ok: Bool, b: Br, o: Ow) -> Maybe<&2, Inflated>:
624 match ok:
625 case False{}:
626 None{}
627 case True{}:
628 Ow{w, n, racc} = o
629 Some{Inflated{String.reverse(racc), br.rest(b), n}}
630
631def inf.result(st: Array<U32> & Is) -> Maybe<&2, Inflated>:
632 (win, ist) = st
633 Is{+b, o, mode, last} = ist
634 match mode:
635 case MoDone{}:
636 inf.fin(br.ok(b), b, o)
637 case MoHead{}:
638 None{}
639 case MoCodes{l, d}:
640 None{}
641 case MoBad{}:
642 None{}
643
644def inflate.rest(+s: String) -> Maybe<&2, Inflated>:
645 inf.result(inf.go(Nat.add(Nat.mul(String.length(s), 8n), 8n), (Array.new(U32, 15n, 0), Is{br.new(s), Ow{0, 0, ""}, MoHead{}, False{}})))
646
647def inflate.out(m: Maybe<&2, Inflated>) -> Maybe<&2, String>:
648 match m:
649 case None{}:
650 None{}
651 case Some{Inflated{out, rest, n}}:
652 Some{out}
653
654# Raw DEFLATE. None: malformed or cut short.
655def inflate(+s: String) -> Maybe<&2, String>:
656 inflate.out(inflate.rest(s))
657
658# CRC-32 (RFC 1952 §8), reflected, polynomial 0xEDB88320.
659def crc.bit(+c: U32) -> U32:
660 Bool.pick(U32, U32.is_eq(U32.and(c, 1), 1), U32.xor(U32.shr(c), 3988292384), U32.shr(c))
661
662def crc.bits(k: Nat, +c: U32) -> U32:
663 match k:
664 case 0n:
665 c
666 case 1n+p:
667 crc.bits(p, crc.bit(c))
668
669def crc.fill(k: Nat, +i: U32, a: Array<U32>) -> Array<U32>:
670 match k:
671 case 0n:
672 a
673 case 1n+p:
674 crc.fill(p, (i + 1 : U32), Array.set(U32, a, i, crc.bits(8n, i)))
675
676def crc.table() -> Array<U32>:
677 crc.fill(256n, 0, Array.new(U32, 8n, 0))
678
679def crc.mix(av: Array<U32> & U32, +c: U32) -> Array<U32> & U32:
680 (a, +t) = av
681 (a, U32.xor(t, U32.shrn(c, 8n)))
682
683def crc.step(st: Array<U32> & U32, +b: U32) -> Array<U32> & U32:
684 (a, +c) = st
685 crc.mix(Array.get(U32, a, U32.and(U32.xor(c, b), 255)), c)
686
687def crc.go(s: String, st: Array<U32> & U32) -> Array<U32> & U32:
688 match s:
689 case SNil{}:
690 st
691 case SCon{h, t}:
692 crc.go(t, crc.step(st, byte(h)))
693
694def crc.of(st: Array<U32> & U32) -> U32:
695 (a, +c) = st
696 U32.xor(c, 4294967295)
697
698def crc32(s: String) -> U32:
699 crc.of(crc.go(s, (crc.table(), 4294967295)))
700
701# Adler-32 (RFC 1950 §9).
702def adler.go(s: String, +a: U32, +b: U32) -> U32:
703 match s:
704 case SNil{}:
705 U32.or(U32.shln(b, 16n), a)
706 case SCon{h, t}:
707 +a2 = U32.mod((a + byte(h) : U32), 65521)
708 adler.go(t, a2, U32.mod((b + a2 : U32), 65521))
709
710def adler32(s: String) -> U32:
711 adler.go(s, 1, 0)
712
713# Little- and big-endian 32-bit words at the front of s.
714def le32(s: String) -> Maybe<&2, U32>:
715 match s:
716 case SCon{Chr{+a}, SCon{Chr{+b}, SCon{Chr{+c}, SCon{Chr{+d}, t}}}}:
717 Some{U32.or(U32.or(a, U32.shln(b, 8n)), U32.or(U32.shln(c, 16n), U32.shln(d, 24n)))}
718 case SNil{}:
719 None{}
720 case SCon{x, y}:
721 None{}
722
723def be32(s: String) -> Maybe<&2, U32>:
724 match s:
725 case SCon{Chr{+a}, SCon{Chr{+b}, SCon{Chr{+c}, SCon{Chr{+d}, t}}}}:
726 Some{U32.or(U32.or(U32.shln(a, 24n), U32.shln(b, 16n)), U32.or(U32.shln(c, 8n), d))}
727 case SNil{}:
728 None{}
729 case SCon{x, y}:
730 None{}
731
732def flag(+f: U32, +bit: U32) -> Bool:
733 Bool.not(U32.is_zero(U32.and(f, bit)))
734
735def check(ok: Bool, +out: String) -> Maybe<&2, String>:
736 match ok:
737 case True{}:
738 Some{out}
739 case False{}:
740 None{}
741
742# RFC 1952 §2.3: after the fixed 10 bytes, optional FEXTRA, FNAME, FCOMMENT, FHCRC.
743# hit: the byte just read was the terminating zero.
744def gz.zstr(s: String, hit: Bool) -> Maybe<&2, String>:
745 match s:
746 case SNil{}:
747 match hit:
748 case True{}:
749 Some{SNil{}}
750 case False{}:
751 None{}
752 case SCon{Chr{+c}, t}:
753 match hit:
754 case True{}:
755 Some{SCon{Chr{c}, t}}
756 case False{}:
757 gz.zstr(t, U32.is_zero(c))
758
759def gz.skip(k: Nat, s: String) -> Maybe<&2, String>:
760 match k:
761 case 0n:
762 Some{s}
763 case 1n+p:
764 match s:
765 case SNil{}:
766 None{}
767 case SCon{h, t}:
768 gz.skip(p, t)
769
770def gz.extra.len(s: String) -> Maybe<&2, String>:
771 match s:
772 case SCon{Chr{+a}, SCon{Chr{+b}, t}}:
773 gz.skip(bits(U32.or(a, U32.shln(b, 8n))), t)
774 case SNil{}:
775 None{}
776 case SCon{x, y}:
777 None{}
778
779def gz.fextra(on: Bool, +s: String) -> Maybe<&2, String>:
780 match on:
781 case True{}:
782 gz.extra.len(s)
783 case False{}:
784 Some{s}
785
786def gz.fstr(on: Bool, +s: String) -> Maybe<&2, String>:
787 match on:
788 case True{}:
789 gz.zstr(s, False{})
790 case False{}:
791 Some{s}
792
793def gz.fhcrc(on: Bool, +s: String) -> Maybe<&2, String>:
794 match on:
795 case True{}:
796 gz.skip(2n, s)
797 case False{}:
798 Some{s}
799
800def gz.flags(+f: U32, s: String) -> Maybe<&2, String>:
801 do Maybe<&2, String>:
802 s1 : String <- gz.fextra(flag(f, 4), s)
803 s2 : String <- gz.fstr(flag(f, 8), s1)
804 s3 : String <- gz.fstr(flag(f, 16), s2)
805 gz.fhcrc(flag(f, 2), s3)
806
807def gz.head(s: String) -> Maybe<&2, String>:
808 match s:
809 case SCon{Chr{+id1}, SCon{Chr{+id2}, SCon{Chr{+cm}, SCon{Chr{+f}, t}}}}:
810 Bool.pick(Maybe<&2, String>, Bool.and(Bool.and(U32.is_eq(id1, 31), U32.is_eq(id2, 139)), U32.is_eq(cm, 8)), gz.flags(f, String.drop(t, 6n)), None{})
811 case SNil{}:
812 None{}
813 case SCon{x, y}:
814 None{}
815
816def gz.trail2(+out: String, +n: U32, crc: Maybe<&2, U32>, size: Maybe<&2, U32>) -> Maybe<&2, String>:
817 do Maybe<&2, String>:
818 c : U32 <- crc
819 z : U32 <- size
820 check(Bool.and(U32.is_eq(c, crc32(out)), U32.is_eq(z, n)), out)
821
822def gz.trail(m: Maybe<&2, Inflated>) -> Maybe<&2, String>:
823 match m:
824 case None{}:
825 None{}
826 case Some{Inflated{+out, +rest, +n}}:
827 gz.trail2(out, n, le32(rest), le32(String.drop(rest, 4n)))
828
829def gz.body(m: Maybe<&2, String>) -> Maybe<&2, String>:
830 match m:
831 case None{}:
832 None{}
833 case Some{+s}:
834 gz.trail(inflate.rest(s))
835
836# One gzip member; the CRC-32 and ISIZE must match. None: malformed, cut short, or corrupt.
837# ponytail: bytes after the first member are ignored; loop over members if a server concatenates them.
838def gunzip(s: String) -> Maybe<&2, String>:
839 gz.body(gz.head(s))
840
841# RFC 1950: CMF and FLG, then DEFLATE, then Adler-32, big-endian.
842def zl.sum(+out: String, a: Maybe<&2, U32>) -> Maybe<&2, String>:
843 match a:
844 case None{}:
845 None{}
846 case Some{+v}:
847 check(U32.is_eq(v, adler32(out)), out)
848
849def zl.trail(m: Maybe<&2, Inflated>) -> Maybe<&2, String>:
850 match m:
851 case None{}:
852 None{}
853 case Some{Inflated{+out, +rest, n}}:
854 zl.sum(out, be32(rest))
855
856def zl.ok(+cmf: U32, +flg: U32) -> Bool:
857 Bool.and(Bool.and(U32.is_eq(U32.and(cmf, 15), 8), U32.is_le(U32.shrn(cmf, 4n), 7)), Bool.and(U32.is_zero(U32.mod((cmf * 256 + flg : U32), 31)), Bool.not(flag(flg, 32))))
858
859def unzlib(s: String) -> Maybe<&2, String>:
860 match s:
861 case SCon{Chr{+cmf}, SCon{Chr{+flg}, +t}}:
862 Bool.pick(Maybe<&2, String>, zl.ok(cmf, flg), zl.trail(inflate.rest(t)), None{})
863 case SNil{}:
864 None{}
865 case SCon{x, y}:
866 None{}
867
868# DEFLATE encoding: LZ77 over hash chains, then one final fixed-Huffman block (RFC 1951 §3.2.6).
869# ponytail: fixed Huffman only; dynamic trees would cut text output further.
870
871# Bit writer: bits wait in buf, least significant first; racc holds the bytes out, reversed.
872type Bw is Data:
873 Bw{buf: U32, cnt: U32, racc: String}
874
875def bw.emit(w: Bw) -> Bw:
876 Bw{+buf, cnt, racc} = w
877 Bw{U32.shrn(buf, 8n), (cnt - 8 : U32), SCon{Chr{U32.and(buf, 255)}, racc}}
878
879def bw.emit.if(w: Bw, full: Bool) -> Bw:
880 match full:
881 case True{}:
882 bw.emit(w)
883 case False{}:
884 w
885
886def bw.full(+w: Bw) -> Bool:
887 Bw{buf, +cnt, racc} = w
888 U32.is_le(8, cnt)
889
890# A put adds at most 16 bits to at most 7, so two emits drain every whole byte.
891def bw.drain(fuel: Nat, +w: Bw) -> Bw:
892 match fuel:
893 case 0n:
894 w
895 case 1n+f:
896 bw.drain(f, bw.emit.if(w, bw.full(w)))
897
898def bw.put(w: Bw, +v: U32, +n: U32) -> Bw:
899 Bw{buf, +cnt, racc} = w
900 bw.drain(2n, Bw{U32.or(buf, U32.shln(v, bits(cnt))), (cnt + n : U32), racc})
901
902def bw.out(w: Bw) -> String:
903 Bw{buf, cnt, racc} = w
904 String.reverse(racc)
905
906# Seven zero bits push out a partial last byte.
907def bw.done(w: Bw) -> String:
908 bw.out(bw.put(w, 0, 7))
909
910# A Huffman code goes out most significant bit first, so it is reversed before the put.
911def rev(k: Nat, +v: U32, +acc: U32) -> U32:
912 match k:
913 case 0n:
914 acc
915 case 1n+p:
916 rev(p, U32.shr(v), U32.or(U32.shl(acc), U32.and(v, 1)))
917
918def bw.code(w: Bw, cl: U32 & U32) -> Bw:
919 (+c, +l) = cl
920 bw.put(w, rev(bits(l), c, 0), l)
921
922# RFC 1951 §3.2.6: the fixed code of literal/length symbol s, and its length.
923def fx.hi(+s: U32, lo: Bool) -> U32 & U32:
924 match lo:
925 case True{}:
926 ((s - 256 : U32), 7)
927 case False{}:
928 ((s - 88 : U32), 8)
929
930def fx.mid(+s: U32, lo: Bool) -> U32 & U32:
931 match lo:
932 case True{}:
933 ((s + 256 : U32), 9)
934 case False{}:
935 fx.hi(s, U32.is_lt(s, 280))
936
937def fx.low(+s: U32, lo: Bool) -> U32 & U32:
938 match lo:
939 case True{}:
940 ((s + 48 : U32), 8)
941 case False{}:
942 fx.mid(s, U32.is_lt(s, 256))
943
944def fx.lit(+s: U32) -> U32 & U32:
945 fx.low(s, U32.is_lt(s, 144))
946
947# The last index whose base is at most v, with that base and its extra-bit count; bases ascend.
948type Cx is Data:
949 Cx{i: U32, base: U32, extra: U32}
950
951def cx.go(bs: List<&2, U32>, es: List<&2, U32>, +v: U32, +i: U32, +best: Cx) -> Cx:
952 match bs:
953 case Nil{}:
954 best
955 case Con{+b, bt}:
956 match es:
957 case Nil{}:
958 best
959 case Con{+e, et}:
960 cx.go(bt, et, v, (i + 1 : U32), Bool.pick(Cx, U32.is_le(b, v), Cx{i, b, e}, best))
961
962def em.len(w: Bw, +len: U32, c: Cx) -> Bw:
963 Cx{+i, +b, +e} = c
964 bw.put(bw.code(w, fx.lit((i + 257 : U32))), (len - b : U32), e)
965
966def em.dist(w: Bw, +d: U32, c: Cx) -> Bw:
967 Cx{+i, +b, +e} = c
968 bw.put(bw.put(w, rev(5n, i, 0), 5), (d - b : U32), e)
969
970def em.match(w: Bw, +len: U32, +d: U32) -> Bw:
971 em.dist(em.len(w, len, cx.go(len.base(), len.extra(), len, 0, Cx{0, 3, 0})), d, cx.go(dist.base(), dist.extra(), d, 0, Cx{0, 1, 0}))
972
973def em.lit(w: Bw, +c: U32) -> Bw:
974 bw.code(w, fx.lit(c))
975
976# Match finder: the input, the newest position + 1 per hash, and per position the previous one with its hash (0: none).
977type Lz is Type:
978 Lz{src: Array<U32>, head: Array<U32>, prev: Array<U32>}
979
980def lz.at.of(r: Array<U32> & U32, head: Array<U32>, prev: Array<U32>) -> Lz & U32:
981 (src, v) = r
982 (Lz{src, head, prev}, v)
983
984def lz.at(z: Lz, +i: U32) -> Lz & U32:
985 Lz{src, head, prev} = z
986 lz.at.of(Array.get(U32, src, i), head, prev)
987
988def lz.drop(r: Lz & U32) -> Lz:
989 (z, v) = r
990 z
991
992def lz.h3(r: Lz & U32, +a: U32, +b: U32) -> Lz & U32:
993 (z, +c) = r
994 (z, U32.and(U32.xor(U32.xor(U32.shln(a, 10n), U32.shln(b, 5n)), c), 32767))
995
996def lz.h2(r: Lz & U32, +i: U32, +a: U32) -> Lz & U32:
997 (z, +b) = r
998 lz.h3(lz.at(z, (i + 2 : U32)), a, b)
999
1000def lz.h1(r: Lz & U32, +i: U32) -> Lz & U32:
1001 (z, +a) = r
1002 lz.h2(lz.at(z, (i + 1 : U32)), i, a)
1003
1004def lz.hash(z: Lz, +i: U32) -> Lz & U32:
1005 lz.h1(lz.at(z, i), i)
1006
1007def lz.link(r: Array<U32> & U32, +i: U32, +h: U32, src: Array<U32>, prev: Array<U32>) -> Lz & U32:
1008 (head, +old) = r
1009 (Lz{src, Array.set(U32, head, h, (i + 1 : U32)), Array.set(U32, prev, U32.and(i, 32767), old)}, old)
1010
1011def lz.ins.of(r: Lz & U32, +i: U32) -> Lz & U32:
1012 (z, +h) = r
1013 Lz{src, head, prev} = z
1014 lz.link(Array.get(U32, head, h), i, h, src, prev)
1015
1016# Links position i into the chain for its next three bytes; answers the chain's previous head.
1017def lz.insert(z: Lz, +i: U32) -> Lz & U32:
1018 lz.ins.of(lz.hash(z, i), i)
1019
1020# Match length: bytes at a + k and b + k compared so far, and whether the last pair was equal.
1021type Ml is Type:
1022 Ml{z: Lz, a: U32, b: U32, k: U32, eq: Bool}
1023
1024def ml.cmp(r: Lz & U32, +a: U32, +b: U32, +k: U32, +x: U32) -> Ml:
1025 (z, +y) = r
1026 Ml{z, a, b, (k + 1 : U32), U32.is_eq(x, y)}
1027
1028def ml.read(r: Lz & U32, +a: U32, +b: U32, +k: U32) -> Ml:
1029 (z, +x) = r
1030 ml.cmp(lz.at(z, (b + k : U32)), a, b, k, x)
1031
1032def ml.len(+k: U32, eq: Bool) -> U32:
1033 match eq:
1034 case True{}:
1035 k
1036 case False{}:
1037 (k - 1 : U32)
1038
1039# Counts equal bytes from a and from b, up to fuel.
1040def ml.go(fuel: Nat, st: Ml) -> Lz & U32:
1041 match fuel:
1042 case 0n:
1043 Ml{z, a, b, +k, eq} = st
1044 (z, ml.len(k, eq))
1045 case 1n+f:
1046 Ml{z, +a, +b, +k, eq} = st
1047 match eq:
1048 case True{}:
1049 ml.go(f, ml.read(lz.at(z, (a + k : U32)), a, b, k))
1050 case False{}:
1051 (z, (k - 1 : U32))
1052
1053# Chain walk at i: candidate c (position + 1), the longest match so far, and whether to go on.
1054type Ch is Type:
1055 Ch{z: Lz, i: U32, c: U32, max: U32, blen: U32, bdist: U32, go: Bool}
1056
1057# RFC 1951 §3.2.5: a distance is at most 32768.
1058def ch.ok(+i: U32, +c: U32, +max: U32, +blen: U32) -> Bool:
1059 Bool.and(Bool.and(U32.is_lt(0, c), U32.is_lt((i - c : U32), 32768)), U32.is_lt(blen, max))
1060
1061def ch.next(r: Array<U32> & U32, src: Array<U32>, head: Array<U32>, +i: U32, +max: U32, +blen: U32, +bdist: U32) -> Ch:
1062 (prev, +c) = r
1063 Ch{Lz{src, head, prev}, i, c, max, blen, bdist, ch.ok(i, c, max, blen)}
1064
1065def ch.best(r: Lz & U32, +i: U32, +p: U32, +max: U32, +blen: U32, +bdist: U32) -> Ch:
1066 (z, +len) = r
1067 Lz{src, head, prev} = z
1068 +more = U32.is_lt(blen, len)
1069 ch.next(Array.get(U32, prev, U32.and(p, 32767)), src, head, i, max, Bool.pick(U32, more, len, blen), Bool.pick(U32, more, (i - p : U32), bdist))
1070
1071def ch.go(fuel: Nat, st: Ch) -> Ch:
1072 match fuel:
1073 case 0n:
1074 st
1075 case 1n+f:
1076 Ch{z, +i, +c, +max, +blen, +bdist, go} = st
1077 match go:
1078 case True{}:
1079 +p = (c - 1 : U32)
1080 ch.go(f, ch.best(ml.go(bits(max), Ml{z, i, p, 0, True{}}), i, p, max, blen, bdist))
1081 case False{}:
1082 Ch{z, i, c, max, blen, bdist, False{}}
1083
1084# Encoder: match finder, bit writer, position, input length, and whether bytes are left.
1085type Es is Type:
1086 Es{z: Lz, w: Bw, i: U32, n: U32, more: Bool}
1087
1088def es.lit.of(r: Lz & U32, w: Bw, +i: U32, +n: U32) -> Es:
1089 (z, +c) = r
1090 +j = (i + 1 : U32)
1091 Es{z, em.lit(w, c), j, n, U32.is_lt(j, n)}
1092
1093def es.lit(z: Lz, w: Bw, +i: U32, +n: U32) -> Es:
1094 es.lit.of(lz.at(z, i), w, i, n)
1095
1096def ins.one(ok: Bool, z: Lz, +j: U32) -> Lz:
1097 match ok:
1098 case True{}:
1099 lz.drop(lz.insert(z, j))
1100 case False{}:
1101 z
1102
1103# Positions inside a match join their chains too, when three bytes remain.
1104def ins.go(k: Nat, z: Lz, +j: U32, +n: U32) -> Lz:
1105 match k:
1106 case 0n:
1107 z
1108 case 1n+f:
1109 ins.go(f, ins.one(U32.is_le((j + 3 : U32), n), z, j), (j + 1 : U32), n)
1110
1111def es.emit(hit: Bool, z: Lz, w: Bw, +i: U32, +n: U32, +blen: U32, +bdist: U32) -> Es:
1112 match hit:
1113 case True{}:
1114 +j = (i + blen : U32)
1115 Es{ins.go(bits((blen - 1 : U32)), z, (i + 1 : U32), n), em.match(w, blen, bdist), j, n, U32.is_lt(j, n)}
1116 case False{}:
1117 es.lit(z, w, i, n)
1118
1119def es.pick(st: Ch, w: Bw, +n: U32) -> Es:
1120 Ch{z, +i, c, max, +blen, +bdist, go} = st
1121 es.emit(U32.is_le(3, blen), z, w, i, n, blen, bdist)
1122
1123# ponytail: greedy parse, 32 chain steps; lazy matching would compress text further.
1124def es.chain(r: Lz & U32, w: Bw, +i: U32, +n: U32) -> Es:
1125 (z, +c) = r
1126 +room = (n - i : U32)
1127 +max = Bool.pick(U32, U32.is_lt(room, 258), room, 258)
1128 es.pick(ch.go(32n, Ch{z, i, c, max, 0, 0, ch.ok(i, c, max, 0)}), w, n)
1129
1130def es.find(short: Bool, z: Lz, w: Bw, +i: U32, +n: U32) -> Es:
1131 match short:
1132 case True{}:
1133 es.lit(z, w, i, n)
1134 case False{}:
1135 es.chain(lz.insert(z, i), w, i, n)
1136
1137# Each step consumes at least one byte, so n steps finish.
1138def es.go(fuel: Nat, st: Es) -> Es:
1139 match fuel:
1140 case 0n:
1141 st
1142 case 1n+f:
1143 Es{z, w, +i, +n, more} = st
1144 match more:
1145 case True{}:
1146 es.go(f, es.find(U32.is_lt((n - i : U32), 3), z, w, i, n))
1147 case False{}:
1148 Es{z, w, i, n, False{}}
1149
1150def es.out(st: Es) -> String:
1151 Es{z, w, i, n, more} = st
1152 bw.done(em.lit(w, 256))
1153
1154def slen(s: String, +n: U32) -> U32:
1155 match s:
1156 case SNil{}:
1157 n
1158 case SCon{h, t}:
1159 slen(t, (n + 1 : U32))
1160
1161def src.fill(s: String, +i: U32, a: Array<U32>) -> Array<U32>:
1162 match s:
1163 case SNil{}:
1164 a
1165 case SCon{h, t}:
1166 src.fill(t, (i + 1 : U32), Array.set(U32, a, i, byte(h)))
1167
1168# The smallest depth whose 2^depth slots hold n.
1169def depth(k: Nat, +d: Nat, +n: U32) -> Nat:
1170 match k:
1171 case 0n:
1172 d
1173 case 1n+f:
1174 Bool.pick(Nat, U32.is_le(n, U32.shln(1, d)), d, depth(f, 1n+d, n))
1175
1176# Raw DEFLATE. The header bits are BFINAL = 1 and BTYPE = 01.
1177def deflate(+s: String) -> String:
1178 +n = slen(s, 0)
1179 src = src.fill(s, 0, Array.new(U32, depth(31n, 0n, n), 0))
1180 es.out(es.go(bits(n), Es{Lz{src, Array.new(U32, 15n, 0), Array.new(U32, 15n, 0)}, Bw{3, 3, ""}, 0, n, U32.is_lt(0, n)}))
1181
1182def str.of(xs: List<&2, U32>, t: String) -> String:
1183 match xs:
1184 case Nil{}:
1185 t
1186 case Con{c, r}:
1187 SCon{Chr{c}, str.of(r, t)}
1188
1189def le32.put(+v: U32, t: String) -> String:
1190 str.of([U32.and(v, 255), U32.and(U32.shrn(v, 8n), 255), U32.and(U32.shrn(v, 16n), 255), U32.shrn(v, 24n)], t)
1191
1192def be32.put(+v: U32, t: String) -> String:
1193 str.of([U32.shrn(v, 24n), U32.and(U32.shrn(v, 16n), 255), U32.and(U32.shrn(v, 8n), 255), U32.and(v, 255)], t)
1194
1195# One gzip member (RFC 1952): no flags, mtime 0, OS unknown.
1196def gzip(+s: String) -> String:
1197 str.of([31, 139, 8, 0, 0, 0, 0, 0, 0, 255], deflate(s) ++ le32.put(crc32(s), le32.put(slen(s, 0), "")))
1198
1199# RFC 1950: CMF 0x78 (32 KiB window), FLG 0x01 (fastest), then DEFLATE, then Adler-32.
1200def zlib(+s: String) -> String:
1201 str.of([120, 1], deflate(s) ++ be32.put(adler32(s), ""))
1202
1203# Zstandard frames (RFC 8878) through libzstd, as (len, words) like Wire.recv.words.
1204# Fails with EFBIG when the output passes max bytes, and ENOENT without libzstd.
1205def zstd.words(max: U32, len: U32, words: Array<U32>) ->
1206 IO(Result<&1, &1, U32 & String, U32 & Array<U32>>):
1207 import "./effs/zlib.c"
1208 import "./effs/zlib.js"
1209
1210# gzip or zlib data (RFC 1952, 1950) through libz, found from the header. Every gzip member is decoded in turn, as gzip -d does.
1211# Fails with EFBIG when the output passes max bytes, and ENOENT without libz.
1212def inflate.words(max: U32, len: U32, words: Array<U32>) ->
1213 IO(Result<&1, &1, U32 & String, U32 & Array<U32>>):
1214 import "./effs/zlib.c"
1215 import "./effs/zlib.js"
1216
1217# One gzip member at level 6 through libz.
1218def gzip.words(len: U32, words: Array<U32>) ->
1219 IO(Result<&1, &1, U32 & String, U32 & Array<U32>>):
1220 import "./effs/zlib.c"
1221 import "./effs/zlib.js"
1222
1223# Brotli (RFC 7932) through libbrotlidec. Fails as zstd.words does.
1224def brotli.words(max: U32, len: U32, words: Array<U32>) ->
1225 IO(Result<&1, &1, U32 & String, U32 & Array<U32>>):
1226 import "./effs/zlib.c"
1227 import "./effs/zlib.js"