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