1	# DEFLATE, gzip, and zlib decoding (RFC 1951, 1952, 1950) over byte strings. Source: https://github.com/paymog/bend-kit/tree/main/zlib
2	import Base
3	
4	# Bytes are one Char per octet (0..255), as everywhere in bend-kit.
5	
6	def byte(h: Char) -> U32:
7	  Chr{c} = h
8	  c
9	
10	def bits(+n: U32) -> Nat:
11	  U32.to_nat(n)
12	
13	def 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.
17	type Br is Data:
18	  Br{s: String, buf: U32, cnt: U32, over: U32}
19	
20	def br.new(s: String) -> Br:
21	  Br{s, 0, 0, 0}
22	
23	def 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	
31	def br.pull.if(b: Br, short: Bool) -> Br:
32	  match short:
33	    case True{}:
34	      br.pull(b)
35	    case False{}:
36	      b
37	
38	def 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.
43	def 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	
50	def 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	
54	def br.take(b: Br, +n: U32) -> Br & U32:
55	  br.cut(br.fill(3n, b, n), n)
56	
57	def br.drop.of(r: Br & U32) -> Br:
58	  (b, v) = r
59	  b
60	
61	def 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.
65	def br.align(+b: Br) -> Br:
66	  Br{s, buf, +cnt, over} = b
67	  br.drop(b, U32.mod(cnt, 8))
68	
69	def br.ok(+b: Br) -> Bool:
70	  Br{s, buf, cnt, +over} = b
71	  U32.is_eq(over, 0)
72	
73	def 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	
80	def 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.
85	def 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.
90	type Ht is Data:
91	  HtNone{}
92	  HtBad{}
93	  HtLeaf{sym: U32}
94	  HtNode{z: Ht, o: Ht}
95	
96	def 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	
107	def 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	
118	def 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	
129	def 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.
141	def 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.
149	def cnt.add(ar: Array<U32> & U32, +len: U32) -> Array<U32>:
150	  (a, v) = ar
151	  Array.set(U32, a, len, (v + 1 : U32))
152	
153	def 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	
160	def 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	
165	def 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	
169	def 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	
176	def 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	
180	def 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	
187	def 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	
191	def 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	
198	def ht.of(st: Array<U32> & Ht) -> Ht:
199	  (n, t) = st
200	  t
201	
202	def 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.
207	def 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.
211	def 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.
216	def 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	
233	def ht.decode(t: Ht, b: Br) -> Br & U32:
234	  ht.dec(16n, (t, b))
235	
236	def 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	
243	def 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	
250	def 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	
261	def 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
273	def 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	
276	def 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	
279	def 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	
282	def 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
286	def fixed.lit() -> Ht:
287	  ht.build(rep(144n, 8, rep(112n, 9, rep(24n, 7, rep(8n, 8, Nil{})))))
288	
289	def 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.
293	type Ow is Data:
294	  Ow{w: U32, n: U32, racc: String}
295	
296	def 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	
300	type Mo is Data:
301	  MoHead{}
302	  MoCodes{lit: Ht, dist: Ht}
303	  MoDone{}
304	  MoBad{}
305	
306	type Is is Data:
307	  Is{br: Br, o: Ow, mode: Mo, last: Bool}
308	
309	def inf.next(last: Bool) -> Mo:
310	  match last:
311	    case True{}:
312	      MoDone{}
313	    case False{}:
314	      MoHead{}
315	
316	def 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.
320	def sb.put2(p: Array<U32> & Ow, b: Br) -> Array<U32> & Br & Ow:
321	  (a, o) = p
322	  (a, b, o)
323	
324	def 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	
328	def 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	
332	def 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	
339	def 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	
343	def 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	
350	def 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	
354	def 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	
358	def 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.
363	def 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	
366	def 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	
373	def cl.push(bv: Br & U32, acc: List<&2, U32>) -> Br & List<&2, U32>:
374	  (b, v) = bv
375	  (b, Con{v, acc})
376	
377	def cl.one(st: Br & List<&2, U32>) -> Br & List<&2, U32>:
378	  (b, acc) = st
379	  cl.push(br.take(b, 3), acc)
380	
381	def 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.
389	type Cd is Data:
390	  Cd{br: Br, acc: List<&2, U32>, n: U32, prev: U32, bad: Bool}
391	
392	def 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	
395	def 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	
399	def 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	
406	def 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	
413	def 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	
420	def 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	
427	def 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	
434	def 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	
438	def 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	
447	def 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.
452	def 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	
459	def 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	
466	def 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	
470	def 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	
476	def 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	
480	def 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	
484	def dyn.hlit(bv: Br & U32) -> Br & Mo:
485	  (b, +hl) = bv
486	  dyn.hdist(br.take(b, 5), (hl + 257 : U32))
487	
488	def 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.
492	def cp.put(av: Array<U32> & U32, o: Ow) -> Array<U32> & Ow:
493	  (a, +c) = av
494	  out.put(a, c, o)
495	
496	def 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	
501	def 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	
508	def 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	
512	def 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.
517	def 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	
524	def 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	
529	def 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	
536	def 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	
540	def 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	
544	def 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	
552	def 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	
559	def 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	
566	def 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	
570	def 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	
574	def 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	
581	def 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	
588	def 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.
596	def 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.
602	def 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.
620	type Inflated is Data:
621	  Inflated{out: String, rest: String, n: U32}
622	
623	def 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	
631	def 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	
644	def 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	
647	def 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.
655	def inflate(+s: String) -> Maybe<&2, String>:
656	  inflate.out(inflate.rest(s))
657	
658	# CRC-32 (RFC 1952 §8), reflected, polynomial 0xEDB88320.
659	def 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	
662	def 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	
669	def 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	
676	def crc.table() -> Array<U32>:
677	  crc.fill(256n, 0, Array.new(U32, 8n, 0))
678	
679	def 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	
683	def 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	
687	def 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	
694	def crc.of(st: Array<U32> & U32) -> U32:
695	  (a, +c) = st
696	  U32.xor(c, 4294967295)
697	
698	def crc32(s: String) -> U32:
699	  crc.of(crc.go(s, (crc.table(), 4294967295)))
700	
701	# Adler-32 (RFC 1950 §9).
702	def 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	
710	def adler32(s: String) -> U32:
711	  adler.go(s, 1, 0)
712	
713	# Little- and big-endian 32-bit words at the front of s.
714	def 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	
723	def 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	
732	def flag(+f: U32, +bit: U32) -> Bool:
733	  Bool.not(U32.is_zero(U32.and(f, bit)))
734	
735	def 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.
744	def 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	
759	def 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	
770	def 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	
779	def 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	
786	def 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	
793	def 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	
800	def 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	
807	def 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	
816	def 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	
822	def 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	
829	def 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.
838	def 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.
842	def 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	
849	def 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	
856	def 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	
859	def 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{}