1	# Bytes, bit streams, Huffman codes, DEFLATE/zlib, checksums, base64 and percent decoding.
2	import Base
3	import gralha-text-scan@0.1.0.1/scan.bend as U
4	
5	# A Bytes is a persistent byte buffer: a balanced tree over a power-of-two capacity.
6	# A flat leaf is one value per index (decoders keep whole words in a Bytes, and
7	# a flat above the leaf level is a uniform run); a word leaf packs four bytes
8	# little-endian, which is how the file effect builds a tree with a quarter of
9	# the nodes and two levels fewer to descend. Each leaf carries its own reading.
10	type ByteTree is Data:
11	  ByteFlat{value: U32}
12	  ByteWord{value: U32}
13	  ByteNode{left: ByteTree, right: ByteTree}
14	
15	def bytes.lane(+index: U32) -> U32:
16	  +k = U32.mod(index, 4)
17	  U.choose(U32, U32.is_eq(k, 0), 1, U.choose(U32, U32.is_eq(k, 1), 256, U.choose(U32, U32.is_eq(k, 2), 65536, 16777216)))
18	
19	def bytes.word.get(+word: U32, +index: U32) -> U32:
20	  U32.mod(U32.div(word, bytes.lane(index)), 256)
21	
22	def bytes.word.put(+word: U32, +index: U32, +v: U32) -> U32:
23	  +lane = bytes.lane(index)
24	  (word - U32.mod(U32.div(word, lane), 256) * lane + v * lane : U32)
25	
26	type Bytes is Data:
27	  Bytes{bufTree: ByteTree, size: U32, capacity: U32}
28	
29	def bytes.empty() -> Bytes:
30	  Bytes{ByteFlat{0}, 0, 1}
31	
32	@unsafe
33	def bytes.tree.get(bufTree: ByteTree, +capacity: U32, +index: U32) -> U32:
34	  match bufTree:
35	    case ByteFlat{v}: v
36	    case ByteWord{v}: bytes.word.get(v, index)
37	    case ByteNode{left, right}:
38	      +half = (capacity / 2 : U32)
39	      bytes.tree.get(U.choose(ByteTree, U32.is_lt(index, half), left, right), half, U32.mod(index, half))
40	
41	@unsafe
42	def bytes.tree.set(+bufTree: ByteTree, +capacity: U32, +index: U32, +v: U32) -> ByteTree:
43	  match bufTree:
44	    case ByteFlat{old}:
45	      U.branch(ByteTree, U32.is_le(capacity, 1), _ => ByteFlat{v}, _ => bytes.tree.set(ByteNode{ByteFlat{old}, ByteFlat{old}}, capacity, index, v))
46	    case ByteWord{old}:
47	      U.branch(ByteTree, U32.is_le(capacity, 4), _ => ByteWord{bytes.word.put(old, index, v)}, _ => bytes.tree.set(ByteNode{ByteWord{old}, ByteWord{old}}, capacity, index, v))
48	    case ByteNode{left, right}:
49	      +half = (capacity / 2 : U32)
50	      U.branch(ByteTree, U32.is_lt(index, half), _ => ByteNode{bytes.tree.set(left, half, index, v), right}, _ => ByteNode{left, bytes.tree.set(right, half, (index - half : U32), v)})
51	
52	def bytes.get(bytes: Bytes, +index: U32) -> U32:
53	  Bytes{bufTree, size, capacity} = bytes
54	  U.branch(U32, U32.is_lt(index, size), _ => bytes.tree.get(bufTree, capacity, index), _ => 0)
55	
56	def bytes.size(bytes: Bytes) -> U32:
57	  Bytes{bufTree, size, capacity} = bytes
58	  size
59	
60	def bytes.set(+bytes: Bytes, +index: U32, v: U32) -> Bytes:
61	  Bytes{bufTree, size, capacity} = bytes
62	  Bytes{bytes.tree.set(bufTree, capacity, index, v), size, capacity}
63	
64	def bytes.push(bytes: Bytes, +v: U32) -> Bytes:
65	  Bytes{bufTree, size, capacity} = bytes
66	  +data = bufTree
67	  +n = size
68	  +cap = capacity
69	  +grow = U32.is_eq(n, cap)
70	  +newcap = U.choose(U32, grow, (cap * 2 : U32), cap)
71	  Bytes{bytes.tree.set(U.choose(ByteTree, grow, ByteNode{data, ByteFlat{0}}, data), newcap, n, v), U32.inc(n), newcap}
72	
73	def bytes.string(s: String, acc: Bytes) -> Bytes:
74	  match s:
75	    case SNil{}: acc
76	    case SCon{Chr{c}, t}: bytes.string(t, bytes.push(acc, c))
77	
78	def bytes.slice(n: Nat, +source: Bytes, +start: U32, target: Bytes) -> Bytes:
79	  match n:
80	    case 0n: target
81	    case 1n+d: bytes.slice(d, source, U32.inc(start), bytes.push(target, bytes.get(source, start)))
82	
83	@unsafe
84	def bytes.be(+bytes: Bytes, +at: U32, count: Nat, acc: U32) -> U32:
85	  match count:
86	    case 0n: acc
87	    case 1n+d: bytes.be(bytes, U32.inc(at), d, (acc * 256 + bytes.get(bytes, at) : U32))
88	
89	def base64.digit(+c: U32) -> U32:
90	  U.choose(U32, U32.is_ge(c, 65) && U32.is_le(c, 90), (c - 65 : U32),
91	    U.choose(U32, U32.is_ge(c, 97) && U32.is_le(c, 122), (c - 71 : U32),
92	      U.choose(U32, U32.is_ge(c, 48) && U32.is_le(c, 57), (c + 4 : U32), U.choose(U32, U32.is_eq(c, 43), 62, U.choose(U32, U32.is_eq(c, 47), 63, 64)))))
93	
94	def base64.read(+s: String, +bits: U32, +count: U32, +out: Bytes) -> Bytes:
95	  match s:
96	    case SNil{}: out
97	    case SCon{Chr{c}, t}:
98	      +v = base64.digit(c)
99	      +n = (count + 6 : U32)
100	      +word = (bits * 64 + v : U32)
101	      U.branch(Bytes, U32.is_eq(c, 61), _ => out,
102	        _ => U.branch(Bytes, U.space(c), _ => base64.read(t, bits, count, out),
103	          _ => U.branch(Bytes, U32.is_lt(v, 64), _ => U.branch(Bytes, U32.is_ge(n, 8),
104	            _ => base64.read(t, U32.mod(word, U32.shln(1, U32.to_nat((n - 8 : U32)))), (n - 8 : U32), bytes.push(out, U32.shrn(word, U32.to_nat((n - 8 : U32))))),
105	            _ => base64.read(t, word, n, out)), _ => bytes.empty())))
106	
107	def base64(s: String) -> Bytes:
108	  base64.read(s, 0, 0, bytes.empty())
109	
110	type BitStream is Data:
111	  BitStream{data: Bytes, position: U32, limit: U32, valid: Bool}
112	
113	type BitRead is Data:
114	  BitRead{value: U32, stream: BitStream}
115	
116	def bits.read(stream: BitStream, +count: U32) -> BitRead:
117	  BitStream{data, position, limit, valid} = stream
118	  +src = data
119	  +pos = position
120	  +end = limit
121	  +at = (pos / 8 : U32)
122	  +word = (bytes.get(src, at) + bytes.get(src, U32.inc(at)) * 256 + bytes.get(src, (at + 2 : U32)) * 65536 : U32)
123	  BitRead{U32.and(U32.shrn(word, U32.to_nat(U32.mod(pos, 8))), (U32.shln(1, U32.to_nat(count)) - 1 : U32)), BitStream{src, (pos + count : U32), end, valid && U32.is_le((pos + count : U32), end)}}
124	
125	def bits.valid(stream: BitStream) -> Bool:
126	  BitStream{data, position, limit, valid} = stream
127	  valid && U32.is_le(position, limit)
128	
129	def bits.invalid(stream: BitStream) -> BitStream:
130	  BitStream{data, position, limit, valid} = stream
131	  BitStream{data, position, limit, False{}}
132	
133	def bits.align(+stream: BitStream) -> BitStream:
134	  BitStream{data, position, limit, valid} = stream
135	  +pos = (((position + 7) / 8) * 8 : U32)
136	  BitStream{data, pos, limit, valid && U32.is_le(pos, limit)}
137	
138	type Huffman is Data:
139	  HuffEmpty{}
140	  HuffBad{}
141	  HuffLeaf{symbol: U32}
142	  HuffNode{zero: Huffman, one: Huffman}
143	
144	@unsafe
145	def huff.insert(+node: Huffman, +depth: Nat, +codeword: U32, +symbol: U32) -> Huffman:
146	  match node:
147	    case HuffBad{}: HuffBad{}
148	    case HuffLeaf{old}: HuffBad{}
149	    case HuffEmpty{}:
150	      match depth:
151	        case 0n: HuffLeaf{symbol}
152	        case 1n+d: huff.insert(HuffNode{HuffEmpty{}, HuffEmpty{}}, 1n+d, codeword, symbol)
153	    case HuffNode{zero, one}:
154	      match depth:
155	        case 0n: HuffBad{}
156	        case 1n+d:
157	          +dd = d
158	          U.branch(Huffman, U32.is_eq(U32.and(codeword, U32.shln(1, dd)), 0), _ => HuffNode{huff.insert(zero, dd, codeword, symbol), one}, _ => HuffNode{zero, huff.insert(one, dd, codeword, symbol)})
159	
160	def huff.counts(n: Nat, +lengths: Bytes, +index: U32, +counts: Bytes) -> Bytes:
161	  match n:
162	    case 0n: counts
163	    case 1n+d:
164	      +len = bytes.get(lengths, index)
165	      huff.counts(d, lengths, U32.inc(index), U.choose(Bytes, U32.is_gt(len, 0) && U32.is_le(len, 15), bytes.set(counts, len, U32.inc(bytes.get(counts, len))), counts))
166	
167	def huff.codes(n: Nat, +counts: Bytes, +length: U32, codeword: U32, codes: Bytes) -> Bytes:
168	  match n:
169	    case 0n: codes
170	    case 1n+d:
171	      +next = ((codeword + bytes.get(counts, (length - 1 : U32))) * 2 : U32)
172	      huff.codes(d, counts, U32.inc(length), next, bytes.push(codes, next))
173	
174	def huff.build.loop(+n: Nat, +lengths: Bytes, +index: U32, +codes: Bytes, +node: Huffman) -> Huffman:
175	  match n:
176	    case 0n: node
177	    case 1n+d:
178	      +len = bytes.get(lengths, index)
179	      +word = bytes.get(codes, len)
180	      U.branch(Huffman, U32.is_eq(len, 0), _ => huff.build.loop(d, lengths, U32.inc(index), codes, node),
181	        _ => U.branch(Huffman, U32.is_le(len, 15) && U32.is_lt(word, U32.shln(1, U32.to_nat(len))), _ => huff.build.loop(d, lengths, U32.inc(index), bytes.set(codes, len, U32.inc(word)), huff.insert(node, U32.to_nat(len), word, index)), _ => HuffBad{}))
182	
183	def huff.build(+lengths: Bytes) -> Huffman:
184	  +n = U32.to_nat(bytes.size(lengths))
185	  +counts = huff.counts(n, lengths, 0, Bytes{ByteFlat{0}, 16, 16})
186	  huff.build.loop(n, lengths, 0, huff.codes(15n, counts, 1, 0, bytes.push(bytes.empty(), 0)), HuffEmpty{})
187	
188	def huff.read.next(read: BitRead, zero: Huffman, one: Huffman, next: Huffman -> BitStream -> BitRead) -> BitRead:
189	  BitRead{bit, stream} = read
190	  next(U.choose(Huffman, U32.is_eq(bit, 0), zero, one))(stream)
191	
192	@unsafe
193	def huff.read(node: Huffman, +stream: BitStream) -> BitRead:
194	  match node:
195	    case HuffEmpty{}: BitRead{0, bits.invalid(stream)}
196	    case HuffBad{}: BitRead{0, bits.invalid(stream)}
197	    case HuffLeaf{symbol}: BitRead{symbol, stream}
198	    case HuffNode{zero, one}: huff.read.next(bits.read(stream, 1), zero, one, node => input => huff.read(node, input))
199	
200	def huff.fixed.lengths(n: Nat, +index: U32, out: Bytes) -> Bytes:
201	  match n:
202	    case 0n: out
203	    case 1n+d: huff.fixed.lengths(d, U32.inc(index), bytes.push(out, U.choose(U32, U32.is_lt(index, 144), 8, U.choose(U32, U32.is_lt(index, 256), 9, U.choose(U32, U32.is_lt(index, 280), 7, 8)))))
204	
205	def bytes.repeat(n: Nat, +v: U32, out: Bytes) -> Bytes:
206	  match n:
207	    case 0n: out
208	    case 1n+d: bytes.repeat(d, v, bytes.push(out, v))
209	
210	def inflate.length.base(index: U32) -> U32:
211	  U.uints.nth(Con{3, Con{4, Con{5, Con{6, Con{7, Con{8, Con{9, Con{10, Con{11, Con{13, Con{15, Con{17, Con{19, Con{23, Con{27, Con{31, Con{35, Con{43, Con{51, Con{59, Con{67, Con{83, Con{99, Con{115, Con{131, Con{163, Con{195, Con{227, Con{258, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
212	
213	def inflate.length.bits(index: U32) -> U32:
214	  U.uints.nth(Con{0, Con{0, Con{0, Con{0, Con{0, Con{0, Con{0, Con{0, Con{1, Con{1, Con{1, Con{1, Con{2, Con{2, Con{2, Con{2, Con{3, Con{3, Con{3, Con{3, Con{4, Con{4, Con{4, Con{4, Con{5, Con{5, Con{5, Con{5, Con{0, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
215	
216	def inflate.distance.base(index: U32) -> U32:
217	  U.uints.nth(Con{1, Con{2, Con{3, Con{4, Con{5, Con{7, Con{9, Con{13, Con{17, Con{25, Con{33, Con{49, Con{65, Con{97, Con{129, Con{193, Con{257, Con{385, Con{513, Con{769, Con{1025, Con{1537, Con{2049, Con{3073, Con{4097, Con{6145, Con{8193, Con{12289, Con{16385, Con{24577, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
218	
219	def inflate.distance.bits(index: U32) -> U32:
220	  U.uints.nth(Con{0, Con{0, Con{0, Con{0, Con{1, Con{1, Con{2, Con{2, Con{3, Con{3, Con{4, Con{4, Con{5, Con{5, Con{6, Con{6, Con{7, Con{7, Con{8, Con{8, Con{9, Con{9, Con{10, Con{10, Con{11, Con{11, Con{12, Con{12, Con{13, Con{13, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
221	
222	def inflate.code.order(index: U32) -> U32:
223	  U.uints.nth(Con{16, Con{17, Con{18, Con{0, Con{8, Con{7, Con{9, Con{6, Con{10, Con{5, Con{11, Con{4, Con{12, Con{3, Con{13, Con{2, Con{14, Con{1, Con{15, Nil{}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
224	
225	type Inflate is Data:
226	  Inflate{stream: BitStream, output: Bytes}
227	
228	def inflate.copy(n: Nat, +distance: U32, +out: Bytes) -> Bytes:
229	  match n:
230	    case 0n: out
231	    case 1n+d: inflate.copy(d, distance, bytes.push(out, bytes.get(out, (bytes.size(out) - distance : U32))))
232	
233	def inflate.distance.extra(read: BitRead, +length: U32, +base: U32, +out: Bytes, limit: U32) -> Inflate:
234	  BitRead{extra, stream} = read
235	  +input = stream
236	  +distance = (base + extra : U32)
237	  U.branch(Inflate, bits.valid(input) && U32.is_gt(distance, 0) && U32.is_le(distance, bytes.size(out)) && U32.is_le(length, (limit - bytes.size(out) : U32)),
238	    _ => Inflate{input, inflate.copy(U32.to_nat(length), distance, out)}, _ => Inflate{bits.invalid(input), out})
239	
240	def inflate.distance(read: BitRead, length: U32, out: Bytes, limit: U32) -> Inflate:
241	  BitRead{symbol, stream} = read
242	  +codeword = symbol
243	  +input = stream
244	  inflate.distance.extra(bits.read(U.choose(BitStream, U32.is_lt(codeword, 30), input, bits.invalid(input)), inflate.distance.bits(codeword)), length, inflate.distance.base(codeword), out, limit)
245	
246	def inflate.length.extra(read: BitRead, base: U32, distance: Huffman, out: Bytes, limit: U32) -> Inflate:
247	  BitRead{extra, stream} = read
248	  inflate.distance(huff.read(distance, stream), (base + extra : U32), out, limit)
249	
250	def inflate.symbol(read: BitRead, distance: Huffman, +out: Bytes, +limit: U32) -> Inflate:
251	  BitRead{symbol, stream} = read
252	  +codeword = symbol
253	  +input = stream
254	  U.branch(Inflate, Bool.not(bits.valid(input)) || U32.is_gt(codeword, 285), _ => Inflate{bits.invalid(input), out},
255	    _ => U.branch(Inflate, U32.is_lt(codeword, 256), _ => U.branch(Inflate, U32.is_lt(bytes.size(out), limit), _ => Inflate{input, bytes.push(out, codeword)}, _ => Inflate{bits.invalid(input), out}),
256	      _ => inflate.length.extra(bits.read(input, inflate.length.bits((codeword - 257 : U32))), inflate.length.base((codeword - 257 : U32)), distance, out, limit)))
257	
258	def inflate.codes.next(+result: Inflate, next: BitStream -> Bytes -> Inflate) -> Inflate:
259	  Inflate{stream, output} = result
260	  U.branch(Inflate, bits.valid(stream), _ => next(stream)(output), _ => result)
261	
262	def inflate.codes.step(+read: BitRead, distance: Huffman, +out: Bytes, limit: U32, next: BitStream -> Bytes -> Inflate) -> Inflate:
263	  BitRead{symbol, stream} = read
264	  U.branch(Inflate, U32.is_eq(symbol, 256), _ => Inflate{stream, out}, _ => inflate.codes.next(inflate.symbol(read, distance, out, limit), next))
265	
266	@unsafe
267	def inflate.codes(+literal: Huffman, +distance: Huffman, stream: BitStream, out: Bytes, +limit: U32) -> Inflate:
268	  inflate.codes.step(huff.read(literal, stream), distance, out, limit, input => output => inflate.codes(literal, distance, input, output, limit))
269	
270	def inflate.stored.byte(read: BitRead, out: Bytes, next: BitStream -> Bytes -> Inflate) -> Inflate:
271	  BitRead{v, stream} = read
272	  next(stream)(bytes.push(out, v))
273	
274	@unsafe
275	def inflate.stored.copy(n: Nat, stream: BitStream, out: Bytes) -> Inflate:
276	  match n:
277	    case 0n: Inflate{stream, out}
278	    case 1n+d: inflate.stored.byte(bits.read(stream, 8), out, input => output => inflate.stored.copy(d, input, output))
279	
280	def inflate.stored.nlen(read: BitRead, +length: U32, +out: Bytes, limit: U32) -> Inflate:
281	  BitRead{inverse, stream} = read
282	  +input = stream
283	  U.branch(Inflate, bits.valid(input) && U32.is_eq(U32.xor(length, inverse), 65535) && U32.is_le(length, (limit - bytes.size(out) : U32)),
284	    _ => inflate.stored.copy(U32.to_nat(length), input, out), _ => Inflate{bits.invalid(input), out})
285	
286	def inflate.stored.len(read: BitRead, out: Bytes, limit: U32) -> Inflate:
287	  BitRead{len, stream} = read
288	  inflate.stored.nlen(bits.read(stream, 16), len, out, limit)
289	
290	type DeflateTrees is Data:
291	  DeflateTrees{literal: Huffman, distance: Huffman, stream: BitStream}
292	
293	def inflate.cl.byte(read: BitRead, codes: Bytes, index: U32, next: BitStream -> Bytes -> Inflate) -> Inflate:
294	  BitRead{len, stream} = read
295	  next(stream)(bytes.set(codes, inflate.code.order(index), len))
296	
297	@unsafe
298	def inflate.cl(n: Nat, +index: U32, stream: BitStream, codes: Bytes) -> Inflate:
299	  match n:
300	    case 0n: Inflate{stream, codes}
301	    case 1n+d: inflate.cl.byte(bits.read(stream, 3), codes, index, input => output => inflate.cl(d, U32.inc(index), input, output))
302	
303	def inflate.length.repeat(read: BitRead, +base: U32, +value: U32, +remaining: U32, +lengths: Bytes) -> Inflate:
304	  BitRead{extra, stream} = read
305	  +count = (base + extra : U32)
306	  +input = stream
307	  U.branch(Inflate, bits.valid(input) && U32.is_le(count, remaining), _ => Inflate{input, bytes.repeat(U32.to_nat(count), value, lengths)}, _ => Inflate{bits.invalid(input), lengths})
308	
309	def inflate.length.code(read: BitRead, +remaining: U32, +lengths: Bytes) -> Inflate:
310	  BitRead{symbol, stream} = read
311	  +codeword = symbol
312	  +input = stream
313	  U.branch(Inflate, Bool.not(bits.valid(input)) || U32.is_gt(codeword, 18), _ => Inflate{bits.invalid(input), lengths},
314	    _ => U.branch(Inflate, U32.is_lt(codeword, 16), _ => Inflate{input, bytes.push(lengths, codeword)},
315	      _ => U.branch(Inflate, U32.is_eq(codeword, 16) && U32.is_eq(bytes.size(lengths), 0), _ => Inflate{bits.invalid(input), lengths},
316	        _ => inflate.length.repeat(bits.read(input, U.choose(U32, U32.is_eq(codeword, 16), 2, U.choose(U32, U32.is_eq(codeword, 17), 3, 7))), U.choose(U32, U32.is_eq(codeword, 18), 11, 3), U.choose(U32, U32.is_eq(codeword, 16), bytes.get(lengths, (bytes.size(lengths) - 1 : U32)), 0), remaining, lengths))))
317	
318	def inflate.lengths.next(+result: Inflate, remaining: U32, oldSize: U32, next: U32 -> BitStream -> Bytes -> Inflate) -> Inflate:
319	  Inflate{stream, lengths} = result
320	  U.branch(Inflate, bits.valid(stream), _ => next((remaining - bytes.size(lengths) + oldSize : U32))(stream)(lengths), _ => result)
321	
322	@unsafe
323	def inflate.lengths(+remaining: U32, +codes: Huffman, +stream: BitStream, +lengths: Bytes) -> Inflate:
324	  U.branch(Inflate, U32.is_eq(remaining, 0), _ => Inflate{stream, lengths},
325	    _ => inflate.lengths.next(inflate.length.code(huff.read(codes, stream), remaining, lengths), remaining, bytes.size(lengths), n => input => output => inflate.lengths(n, codes, input, output)))
326	
327	def inflate.trees(result: Inflate, +litCount: U32, distCount: U32) -> DeflateTrees:
328	  Inflate{stream, lengths} = result
329	  +ls = lengths
330	  +input = stream
331	  DeflateTrees{huff.build(bytes.slice(U32.to_nat(litCount), ls, 0, bytes.empty())), huff.build(bytes.slice(U32.to_nat(distCount), ls, litCount, bytes.empty())), U.choose(BitStream, U32.is_gt(bytes.get(ls, 256), 0), input, bits.invalid(input))}
332	
333	def inflate.dynamic.codes(result: Inflate, +litCount: U32, +distCount: U32) -> DeflateTrees:
334	  Inflate{stream, codes} = result
335	  inflate.trees(inflate.lengths((litCount + distCount : U32), huff.build(codes), stream, bytes.empty()), litCount, distCount)
336	
337	def inflate.dynamic.header(read: BitRead) -> DeflateTrees:
338	  BitRead{header, stream} = read
339	  +word = header
340	  +litCount = (U32.and(word, 31) + 257 : U32)
341	  +distCount = (U32.and(U32.shrn(word, 5n), 31) + 1 : U32)
342	  inflate.dynamic.codes(inflate.cl(U32.to_nat((U32.and(U32.shrn(word, 10n), 15) + 4 : U32)), 0, stream, Bytes{ByteFlat{0}, 19, 32}), litCount, distCount)
343	
344	def inflate.dynamic(trees: DeflateTrees, out: Bytes, limit: U32) -> Inflate:
345	  DeflateTrees{literal, distance, stream} = trees
346	  inflate.codes(literal, distance, stream, out, limit)
347	
348	def inflate.block(+kind: U32, +stream: BitStream, +out: Bytes, +limit: U32) -> Inflate:
349	  U.branch(Inflate, U32.is_eq(kind, 0), _ => inflate.stored.len(bits.read(bits.align(stream), 16), out, limit),
350	    _ => U.branch(Inflate, U32.is_eq(kind, 1), _ => inflate.codes(huff.build(huff.fixed.lengths(288n, 0, bytes.empty())), huff.build(bytes.repeat(32n, 5, bytes.empty())), stream, out, limit),
351	      _ => U.branch(Inflate, U32.is_eq(kind, 2), _ => inflate.dynamic(inflate.dynamic.header(bits.read(stream, 14)), out, limit), _ => Inflate{bits.invalid(stream), out})))
352	
353	def inflate.block.done(+result: Inflate, last: Bool, next: BitStream -> Bytes -> Inflate) -> Inflate:
354	  Inflate{stream, output} = result
355	  U.branch(Inflate, last || Bool.not(bits.valid(stream)), _ => result, _ => next(stream)(output))
356	
357	def inflate.header(read: BitRead, out: Bytes, limit: U32, next: BitStream -> Bytes -> Inflate) -> Inflate:
358	  BitRead{header, stream} = read
359	  +word = header
360	  inflate.block.done(inflate.block(U32.shr(word), stream, out, limit), U32.is_eq(U32.and(word, 1), 1), next)
361	
362	@unsafe
363	def inflate.blocks(stream: BitStream, out: Bytes, +limit: U32) -> Inflate:
364	  inflate.header(bits.read(stream, 3), out, limit, input => output => inflate.blocks(input, output, limit))
365	
366	def checksum.adler.loop(n: Nat, +src: Bytes, +index: U32, +a: U32, b: U32) -> U32:
367	  match n:
368	    case 0n: (b * 65536 + a : U32)
369	    case 1n+d:
370	      +aa = ((a + bytes.get(src, index)) % 65521 : U32)
371	      checksum.adler.loop(d, src, U32.inc(index), aa, ((b + aa) % 65521 : U32))
372	
373	def checksum.adler(+src: Bytes) -> U32:
374	  checksum.adler.loop(U32.to_nat(bytes.size(src)), src, 0, 1, 0)
375	
376	def checksum.crc.word(n: Nat, +word: U32) -> U32:
377	  match n:
378	    case 0n: word
379	    case 1n+d: checksum.crc.word(d, U32.xor(U32.shr(word), U.choose(U32, U32.is_eq(U32.and(word, 1), 1), 3988292384, 0)))
380	
381	def checksum.crc.table(n: Nat, +index: U32, out: Bytes) -> Bytes:
382	  match n:
383	    case 0n: out
384	    case 1n+d: checksum.crc.table(d, U32.inc(index), bytes.push(out, checksum.crc.word(8n, index)))
385	
386	def checksum.crc.loop(n: Nat, +src: Bytes, +index: U32, +table: Bytes, +crc: U32) -> U32:
387	  match n:
388	    case 0n: U32.xor(crc, 4294967295)
389	    case 1n+d: checksum.crc.loop(d, src, U32.inc(index), table, U32.xor(U32.shrn(crc, 8n), bytes.get(table, U32.and(U32.xor(crc, bytes.get(src, index)), 255))))
390	
391	def zlib.result(result: Inflate, +expected: U32, checksum: U32) -> Maybe<&2, Bytes>:
392	  Inflate{stream, output} = result
393	  +out = output
394	  U.choose(Maybe<&2, Bytes>, bits.valid(stream) && U32.is_eq(bytes.size(out), expected) && U32.is_eq(checksum.adler(out), checksum), Some{out}, None{})
395	
396	def zlib(+src: Bytes, +expected: U32) -> Maybe<&2, Bytes>:
397	  +n = bytes.size(src)
398	  +cmf = bytes.get(src, 0)
399	  +flg = bytes.get(src, 1)
400	  U.branch(Maybe<&2, Bytes>, U32.is_ge(n, 6) && U32.is_eq(U32.and(cmf, 15), 8) && U32.is_le(U32.shrn(cmf, 4n), 7) && U32.is_eq(U32.and(flg, 32), 0) && U32.is_eq(((cmf * 256 + flg) % 31 : U32), 0),
401	    _ => zlib.result(inflate.blocks(BitStream{src, 16, ((n - 4) * 8 : U32), True{}}, bytes.empty(), expected), expected, bytes.be(src, (n - 4 : U32), 4n, 0)), _ => None{})
402	
403	def uri.hex.valid(+c: U32) -> Bool:
404	  U.digit(c) || (U32.is_ge(c, 65) && U32.is_le(c, 70)) || (U32.is_ge(c, 97) && U32.is_le(c, 102))
405	
406	def uri.bytes(+s: String, +out: Bytes) -> Bytes:
407	  match s:
408	    case SNil{}: out
409	    case SCon{Chr{37}, SCon{Chr{a}, SCon{Chr{b}, rest}}}:
410	      U.branch(Bytes, uri.hex.valid(a) && uri.hex.valid(b), _ => uri.bytes(rest, bytes.push(out, (U.hex.digit(a) * 16 + U.hex.digit(b) : U32))), _ => bytes.empty())
411	    case SCon{Chr{c}, rest}:
412	      U.branch(Bytes, U32.is_lt(c, 128) && Bool.not(U32.is_eq(c, 37)), _ => uri.bytes(rest, bytes.push(out, c)), _ => bytes.empty())
413	
414	@unsafe
415	def bytes.depth(+size: U32, +side: U32, +depth: Nat) -> Nat:
416	  U.branch(Nat, U32.is_ge(side, size), _ => depth, _ => bytes.depth(size, (side * 2 : U32), 1n+depth))
417	
418	def bytes.zero(+size: U32) -> Bytes:
419	  Bytes{ByteFlat{0}, size, U32.shln(1, bytes.depth(size, 1, 0n))}
420	
421	# ---- files ----
422	
423	# A file's bytes, read straight into a byte tree by the effect (File.read
424	# decodes UTF-8, and building the tree in Bend from a byte string costs a
425	# cons cell per byte); Fail carries the errno and its message.
426	def bytes.read.raw(path: String) -> IO(Result<&1, &1, U32 & String, Bytes>):
427	  import "./effs/bytes_read.c"
428	  import "./effs/bytes_read.js"
429	
430	def bytes.read(path: String) -> IO(Result<&1, &1, U32 & String, Bytes>):
431	  bytes.read.raw(path)