1	# RFC 7541 HPACK header blocks with a bounded dynamic table.
2	import Base
3	import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
4	import ./huffman.bend as Huff
5	
6	# mode: 0 permits indexing, 1 is without indexing, 2 is never indexed.
7	type Field is Data:
8	  Field{name: String, value: String, mode: U32}
9	
10	type State is Data:
11	  State{entries: List<&2, Field>, size: U32, capacity: U32, allowed: U32, pending: Maybe<&2, U32>, minimum: Maybe<&2, U32>}
12	
13	def new(+max: U32) -> State:
14	  State{Nil{}, 0, max, max, None{}, None{}}
15	
16	# RFC 7541 Appendix A, indexed from 1 to 61.
17	def static(+index: U32) -> Field:
18	  match index:
19	    case 1:
20	      Field{":authority", "", 0}
21	    case 2:
22	      Field{":method", "GET", 0}
23	    case 3:
24	      Field{":method", "POST", 0}
25	    case 4:
26	      Field{":path", "/", 0}
27	    case 5:
28	      Field{":path", "/index.html", 0}
29	    case 6:
30	      Field{":scheme", "http", 0}
31	    case 7:
32	      Field{":scheme", "https", 0}
33	    case 8:
34	      Field{":status", "200", 0}
35	    case 9:
36	      Field{":status", "204", 0}
37	    case 10:
38	      Field{":status", "206", 0}
39	    case 11:
40	      Field{":status", "304", 0}
41	    case 12:
42	      Field{":status", "400", 0}
43	    case 13:
44	      Field{":status", "404", 0}
45	    case 14:
46	      Field{":status", "500", 0}
47	    case 15:
48	      Field{"accept-charset", "", 0}
49	    case 16:
50	      Field{"accept-encoding", "gzip, deflate", 0}
51	    case 17:
52	      Field{"accept-language", "", 0}
53	    case 18:
54	      Field{"accept-ranges", "", 0}
55	    case 19:
56	      Field{"accept", "", 0}
57	    case 20:
58	      Field{"access-control-allow-origin", "", 0}
59	    case 21:
60	      Field{"age", "", 0}
61	    case 22:
62	      Field{"allow", "", 0}
63	    case 23:
64	      Field{"authorization", "", 0}
65	    case 24:
66	      Field{"cache-control", "", 0}
67	    case 25:
68	      Field{"content-disposition", "", 0}
69	    case 26:
70	      Field{"content-encoding", "", 0}
71	    case 27:
72	      Field{"content-language", "", 0}
73	    case 28:
74	      Field{"content-length", "", 0}
75	    case 29:
76	      Field{"content-location", "", 0}
77	    case 30:
78	      Field{"content-range", "", 0}
79	    case 31:
80	      Field{"content-type", "", 0}
81	    case 32:
82	      Field{"cookie", "", 0}
83	    case 33:
84	      Field{"date", "", 0}
85	    case 34:
86	      Field{"etag", "", 0}
87	    case 35:
88	      Field{"expect", "", 0}
89	    case 36:
90	      Field{"expires", "", 0}
91	    case 37:
92	      Field{"from", "", 0}
93	    case 38:
94	      Field{"host", "", 0}
95	    case 39:
96	      Field{"if-match", "", 0}
97	    case 40:
98	      Field{"if-modified-since", "", 0}
99	    case 41:
100	      Field{"if-none-match", "", 0}
101	    case 42:
102	      Field{"if-range", "", 0}
103	    case 43:
104	      Field{"if-unmodified-since", "", 0}
105	    case 44:
106	      Field{"last-modified", "", 0}
107	    case 45:
108	      Field{"link", "", 0}
109	    case 46:
110	      Field{"location", "", 0}
111	    case 47:
112	      Field{"max-forwards", "", 0}
113	    case 48:
114	      Field{"proxy-authenticate", "", 0}
115	    case 49:
116	      Field{"proxy-authorization", "", 0}
117	    case 50:
118	      Field{"range", "", 0}
119	    case 51:
120	      Field{"referer", "", 0}
121	    case 52:
122	      Field{"refresh", "", 0}
123	    case 53:
124	      Field{"retry-after", "", 0}
125	    case 54:
126	      Field{"server", "", 0}
127	    case 55:
128	      Field{"set-cookie", "", 0}
129	    case 56:
130	      Field{"strict-transport-security", "", 0}
131	    case 57:
132	      Field{"transfer-encoding", "", 0}
133	    case 58:
134	      Field{"user-agent", "", 0}
135	    case 59:
136	      Field{"vary", "", 0}
137	    case 60:
138	      Field{"via", "", 0}
139	    case 61:
140	      Field{"www-authenticate", "", 0}
141	    case _:
142	      Field{"", "", 0}
143	
144	type Cursor is Type:
145	  Cursor{bytes: Bytes.Bytes, at: U32, length: U32}
146	
147	def take.of(r: Bytes.Bytes & Maybe<&2, U32>, +at: U32, +length: U32) -> Maybe<&1, Cursor & U32>:
148	  (b, m) = r
149	  match m:
150	    case None{}:
151	      None{}
152	    case Some{value}:
153	      Some{(Cursor{b, (at + 1 : U32), length}, value)}
154	
155	def take(c: Cursor) -> Maybe<&1, Cursor & U32>:
156	  Cursor{b, +at, +length} = c
157	  take.of(Bytes.get(b, at), at, length)
158	
159	def with_pair(-R: Type, r: Cursor & U32, k: Cursor -> U32 -> R) -> R:
160	  (cursor, value) = r
161	  k(cursor, value)
162	
163	def with_taken(-R: Type, m: Maybe<&1, Cursor & U32>, k: Cursor -> U32 -> Maybe<&1, R>) -> Maybe<&1, R>:
164	  match m:
165	    case None{}:
166	      None{}
167	    case Some{pair}:
168	      with_pair(Maybe<&1, R>, pair, k)
169	
170	def within(ok: Bool) -> Maybe<&1, Unit>:
171	  match ok:
172	    case True{}:
173	      Some{Unit{}}
174	    case False{}:
175	      None{}
176	
177	def integer.done(n: Nat, cont: Bool, c: Cursor, +shift: U32, +value: U32) -> Maybe<&1, Cursor & U32>:
178	  match n cont:
179	    case 0n False{}:
180	      Some{(c, value)}
181	    case 0n True{}:
182	      None{}
183	    case 1n+p False{}:
184	      Some{(c, value)}
185	    case 1n+p True{}:
186	      with_taken(Cursor & U32, take(c), cursor => +byte =>
187	        do Maybe<&1, Cursor & U32>:
188	          +part: U32 = (byte .&. 127 : U32)
189	          unused: Unit <- within(U32.is_le(part, ((4294967295 - value : U32) >> U32.to_nat(shift) : U32)))
190	          integer.done(p, U32.is_ne((byte .&. 128 : U32), 0), cursor, (shift + 7 : U32), (value + (part << U32.to_nat(shift) : U32) : U32)))
191	
192	def integer.more(full: Bool, c: Cursor, +value: U32) -> Maybe<&1, Cursor & U32>:
193	  match full:
194	    case True{}:
195	      integer.done(5n, True{}, c, 0, value)
196	    case False{}:
197	      Some{(c, value)}
198	
199	def integer.after(+byte: U32, +mask: U32, c: Cursor) -> Maybe<&1, Cursor & U32>:
200	  +v = (byte .&. mask : U32)
201	  integer.more(U32.is_eq(v, mask), c, v)
202	
203	def table.at(xs: List<&2, Field>, n: Nat) -> Maybe<&2, Field>:
204	  match xs n:
205	    case Nil{} _:
206	      None{}
207	    case Con{+field, tail} 0n:
208	      Some{field}
209	    case Con{field, tail} 1n+p:
210	      table.at(tail, p)
211	
212	
213	def indexed.static(valid: Bool, +i: U32) -> Maybe<&2, Field>:
214	  match valid:
215	    case True{}:
216	      Some{static(i)}
217	    case False{}:
218	      None{}
219	def indexed.choose(s: Bool, +i: U32, xs: List<&2, Field>) -> Maybe<&2, Field>:
220	  match s:
221	    case True{}:
222	      indexed.static(U32.is_ne(i, 0), i)
223	    case False{}:
224	      table.at(xs, U32.to_nat((i - 62 : U32)))
225	def indexed(+i: U32, st: State) -> Maybe<&2, Field>:
226	  State{entries, size, capacity, allowed, pending, minimum} = st
227	  indexed.choose(U32.is_le(i, 61), i, entries)
228	
229	def literal.decoded(huff: Bool, b: Bytes.Bytes) -> Maybe<&2, String>:
230	  match huff:
231	    case True{}:
232	      Huff.decode(b)
233	    case False{}:
234	      Some{Bytes.to_string(b)}
235	
236	def literal.result(m: Maybe<&2, String>, b: Bytes.Bytes, +at: U32, +count: U32, +length: U32) -> Maybe<&1, Cursor & String>:
237	  match m:
238	    case None{}:
239	      None{}
240	    case Some{text}:
241	      Some{(Cursor{b, (at + count : U32), length}, text)}
242	
243	def literal.slice(r: Bytes.Bytes & Bytes.Bytes, huff: Bool, +at: U32, +count: U32, +length: U32) -> Maybe<&1, Cursor & String>:
244	  (b, part) = r
245	  literal.result(literal.decoded(huff, part), b, at, count, length)
246	
247	def literal.fits(ok: Bool, huff: Bool, b: Bytes.Bytes, +at: U32, +count: U32, +length: U32) -> Maybe<&1, Cursor & String>:
248	  match ok:
249	    case False{}:
250	      None{}
251	    case True{}:
252	      literal.slice(Bytes.slice(b, at, count), huff, at, count, length)
253	
254	def literal.bytes(huff: Bool, c: Cursor, +count: U32) -> Maybe<&1, Cursor & String>:
255	  Cursor{b, +at, +length} = c
256	  literal.fits(Bytes.fits(length, at, count), huff, b, at, count, length)
257	
258	def literal(c: Cursor) -> Maybe<&1, Cursor & String>:
259	  with_taken(Cursor & String, take(c), cursor => +first =>
260	    with_taken(Cursor & String, integer.after(first, 127, cursor), cursor => count =>
261	      literal.bytes(U32.is_ne((first .&. 128 : U32), 0), cursor, count)))
262	
263	def field.size(f: Field) -> U32:
264	  Field{+name, +value, mode} = f
265	  (U32.from_nat(String.length(name)) + U32.from_nat(String.length(value)) + 32 : U32)
266	
267	def table.trim.go(xs: List<&2, Field>, +room: U32, keep: Bool, +acc: List<&2, Field>, +used: U32) -> List<&2, Field> & U32:
268	  match xs keep:
269	    case Nil{} _:
270	      (List.reverse(&2, Field, acc), used)
271	    case Con{field, tail} False{}:
272	      (List.reverse(&2, Field, acc), used)
273	    case Con{+field, tail} True{}:
274	      +cost = field.size(field)
275	      +fits = U32.is_le(cost, room)
276	      table.trim.go(tail, Bool.pick(U32, fits, (room - cost : U32), 0), fits,
277	        Bool.pick(List<&2, Field>, fits, Con{field, acc}, acc),
278	        Bool.pick(U32, fits, (used + cost : U32), used))
279	
280	def table.trim(xs: List<&2, Field>, +capacity: U32) -> List<&2, Field> & U32:
281	  table.trim.go(xs, capacity, True{}, Nil{}, 0)
282	
283	def table.trimmed(r: List<&2, Field> & U32, +capacity: U32, +allowed: U32, pending: Maybe<&2, U32>, minimum: Maybe<&2, U32>) -> State:
284	  (entries, size) = r
285	  State{entries, size, capacity, allowed, pending, minimum}
286	
287	def table.add(room: Bool, +field: Field, xs: List<&2, Field>, +used: U32, +capacity: U32, +allowed: U32, pending: Maybe<&2, U32>, minimum: Maybe<&2, U32>) -> State:
288	  match room:
289	    case True{}:
290	      State{Con{field, xs}, (used + field.size(field) : U32), capacity, allowed, pending, minimum}
291	    case False{}:
292	      table.trimmed(table.trim(Con{field, xs}, capacity), capacity, allowed, pending, minimum)
293	
294	def table.oversize(too_big: Bool, +field: Field, xs: List<&2, Field>, +used: U32, +capacity: U32, +allowed: U32, pending: Maybe<&2, U32>, minimum: Maybe<&2, U32>) -> State:
295	  match too_big:
296	    case True{}:
297	      State{Nil{}, 0, capacity, allowed, pending, minimum}
298	    case False{}:
299	      table.add(U32.is_le(used, (capacity - field.size(field) : U32)), field, xs, used, capacity, allowed, pending, minimum)
300	def table.insert(+field: Field, st: State) -> State:
301	  State{xs, +used, +capacity, +allowed, pending, minimum} = st
302	  +cost = field.size(field)
303	  table.oversize(U32.is_gt(cost, capacity), field, xs, used, capacity, allowed, pending, minimum)
304	
305	def field.matches(exact: Bool, f: Field, +name: String, +value: String) -> Bool:
306	  match exact:
307	    case True{}:
308	      Field{n, v, mode} = f
309	      Bool.and(String.eq(n, name), String.eq(v, value))
310	    case False{}:
311	      Field{n, v, mode} = f
312	      String.eq(n, name)
313	
314	def find.static(+exact: Bool, n: Nat, +i: U32, +name: String, +value: String, found: U32) -> U32:
315	  match n found:
316	    case 0n result:
317	      result
318	    case 1n+p 0:
319	      find.static(exact, p, (i + 1 : U32), name, value,
320	        Bool.pick(U32, field.matches(exact, static(i), name, value), i, 0))
321	    case 1n+p result:
322	      result
323	
324	def find.dynamic(+exact: Bool, xs: List<&2, Field>, +i: U32, +name: String, +value: String, found: U32) -> U32:
325	  match xs found:
326	    case Nil{} result:
327	      result
328	    case Con{+field, tail} 0:
329	      find.dynamic(exact, tail, (i + 1 : U32), name, value,
330	        Bool.pick(U32, field.matches(exact, field, name, value), i, 0))
331	    case Con{field, tail} result:
332	      result
333	
334	def find.in_dynamic(exact: Bool, st: State, +name: String, +value: String, found: U32) -> U32:
335	  State{entries, size, capacity, allowed, pending, minimum} = st
336	  find.dynamic(exact, entries, 62, name, value, found)
337	
338	def find.index(+exact: Bool, st: State, +name: String, +value: String) -> U32:
339	  find.in_dynamic(exact, st, name, value, find.static(exact, 61n, 1, name, value, 0))
340	
341	def limit.min(m: Maybe<&2, U32>, +n: U32) -> U32:
342	  match m:
343	    case None{}:
344	      n
345	    case Some{+old}:
346	      Bool.pick(U32, U32.is_lt(n, old), n, old)
347	
348	def set_limit(+n: U32, st: State) -> State:
349	  State{entries, size, capacity, allowed, pending, minimum} = st
350	  State{entries, size, capacity, n, Some{n}, Some{limit.min(minimum, n)}}
351	
352	def table.resize(+n: U32, st: State) -> State:
353	  State{entries, size, capacity, allowed, pending, minimum} = st
354	  table.trimmed(table.trim(entries, n), n, allowed, pending, minimum)
355	
356	type Step is Type:
357	  Step{state: State, cursor: Cursor, field: Maybe<&2, Field>}
358	
359	def with_text.pair(-R: Type, r: Cursor & String, k: Cursor -> String -> R) -> R:
360	  (cursor, text) = r
361	  k(cursor, text)
362	
363	def with_text(-R: Type, m: Maybe<&1, Cursor & String>, k: Cursor -> String -> Maybe<&1, R>) -> Maybe<&1, R>:
364	  match m:
365	    case None{}:
366	      None{}
367	    case Some{pair}:
368	      with_text.pair(Maybe<&1, R>, pair, k)
369	
370	def name.indexed(m: Maybe<&2, Field>, c: Cursor) -> Maybe<&1, Cursor & String>:
371	  match m:
372	    case None{}:
373	      None{}
374	    case Some{Field{name, value, mode}}:
375	      Some{(c, name)}
376	
377	def name.read(+i: U32, st: State, c: Cursor) -> Maybe<&1, Cursor & String>:
378	  match i:
379	    case 0:
380	      literal(c)
381	    case _:
382	      name.indexed(indexed(i, st), c)
383	
384	def decode.indexed.field(m: Maybe<&2, Field>, st: State, c: Cursor) -> Maybe<&1, Step>:
385	  match m:
386	    case None{}:
387	      None{}
388	    case Some{field}:
389	      Some{Step{st, c, Some{field}}}
390	
391	def decode.indexed(+first: U32, +st: State, c: Cursor) -> Maybe<&1, Step>:
392	  with_taken(Step, integer.after(first, 127, c), cursor => index =>
393	    decode.indexed.field(indexed(index, st), st, cursor))
394	
395	def decode.literal.finish(insert: Bool, +field: Field, st: State, c: Cursor) -> Maybe<&1, Step>:
396	  match insert:
397	    case True{}:
398	      Some{Step{table.insert(field, st), c, Some{field}}}
399	    case False{}:
400	      Some{Step{st, c, Some{field}}}
401	
402	def decode.literal(+first: U32, +mask: U32, +mode: U32, +st: State, c: Cursor) -> Maybe<&1, Step>:
403	  with_taken(Step, integer.after(first, mask, c), cursor => index =>
404	    with_text(Step, name.read(index, st, cursor), cursor => +name =>
405	      with_text(Step, literal(cursor), cursor => value =>
406	        decode.literal.finish(U32.is_eq(mode, 0), Field{name, value, mode}, st, cursor))))
407	
408	def decode.min(m: Maybe<&2, U32>, +n: U32) -> Bool:
409	  match m:
410	    case None{}:
411	      True{}
412	    case Some{minimum}:
413	      U32.is_le(n, minimum)
414	
415	def decode.updated.from(st: State, c: Cursor) -> Maybe<&1, Step>:
416	  State{entries, size, capacity, allowed, pending, minimum} = st
417	  Some{Step{State{entries, size, capacity, allowed, None{}, None{}}, c, None{}}}
418	
419	def decode.updated(n: U32, st: State, c: Cursor) -> Maybe<&1, Step>:
420	  decode.updated.from(table.resize(n, st), c)
421	
422	def decode.update.valid(valid: Bool, +n: U32, st: State, c: Cursor) -> Maybe<&1, Step>:
423	  match valid:
424	    case True{}:
425	      decode.updated(n, st, c)
426	    case False{}:
427	      None{}
428	
429	def decode.update.value(+n: U32, st: State, c: Cursor) -> Maybe<&1, Step>:
430	  State{entries, size, capacity, +allowed, pending, +minimum} = st
431	  decode.update.valid(Bool.and(U32.is_le(n, allowed), decode.min(minimum, n)), n,
432	    State{entries, size, capacity, allowed, pending, minimum}, c)
433	
434	def decode.update(+first: U32, st: State, c: Cursor, seen: Bool) -> Maybe<&1, Step>:
435	  do Maybe<&1, Step>:
436	    unused: Unit <- within(Bool.not(seen))
437	    with_taken(Step, integer.after(first, 31, c), cursor => size =>
438	      decode.update.value(size, st, cursor))
439	
440	def decode.ready(st: State) -> Bool:
441	  State{entries, size, capacity, allowed, pending, minimum} = st
442	  Maybe.is_none(&2, U32, pending)
443	
444	def decode.kind(+first: U32) -> U32:
445	  Bool.pick(U32, U32.is_ne((first .&. 128 : U32), 0), 0,
446	    Bool.pick(U32, U32.is_ne((first .&. 64 : U32), 0), 1,
447	      Bool.pick(U32, U32.is_ne((first .&. 32 : U32), 0), 2, 3)))
448	
449	def decode.representation(kind: U32, +first: U32, c: Cursor, +st: State, seen: Bool) -> Maybe<&1, Step>:
450	  match kind:
451	    case 0:
452	      do Maybe<&1, Step>:
453	        unused: Unit <- within(decode.ready(st))
454	        decode.indexed(first, st, c)
455	    case 1:
456	      do Maybe<&1, Step>:
457	        unused: Unit <- within(decode.ready(st))
458	        decode.literal(first, 63, 0, st, c)
459	    case 2:
460	      decode.update(first, st, c, seen)
461	    case _:
462	      do Maybe<&1, Step>:
463	        unused: Unit <- within(decode.ready(st))
464	        decode.literal(first, 15, Bool.pick(U32, U32.is_ne((first .&. 16 : U32), 0), 2, 1), st, c)
465	
466	def decode.one(c: Cursor, +st: State, seen: Bool) -> Maybe<&1, Step>:
467	  with_taken(Step, take(c), cursor => +first =>
468	    decode.representation(decode.kind(first), first, cursor, st, seen))
469	
470	def decode.add(m: Maybe<&2, Field>, acc: List<&2, Field>, seen: Bool) -> List<&2, Field> & Bool:
471	  match m:
472	    case None{}:
473	      (acc, seen)
474	    case Some{field}:
475	      (Con{field, acc}, True{})
476	
477	def with_step(-R: Type, step: Step, k: State -> Cursor -> Maybe<&2, Field> -> R) -> R:
478	  Step{state, cursor, field} = step
479	  k(state, cursor, field)
480	
481	def with_end(-R: Type, c: Cursor, k: Cursor -> Bool -> R) -> R:
482	  Cursor{bytes, +at, +length} = c
483	  k(Cursor{bytes, at, length}, U32.is_eq(at, length))
484	
485	def with_fields(-R: Type, r: List<&2, Field> & Bool, k: List<&2, Field> -> Bool -> R) -> R:
486	  (fields, seen) = r
487	  k(fields, seen)
488	
489	def decode.go(fuel: Nat, ended: Bool, c: Cursor, st: State, acc: List<&2, Field>, +seen: Bool) -> Maybe<&1, State & List<&2, Field>>:
490	  match fuel ended:
491	    case 0n False{}:
492	      None{}
493	    case 0n True{}:
494	      Some{(st, List.reverse(&2, Field, acc))}
495	    case 1n+p True{}:
496	      Some{(st, List.reverse(&2, Field, acc))}
497	    case 1n+p False{}:
498	      Maybe.bind(&1, Step, State & List<&2, Field>, decode.one(c, st, seen), step =>
499	        with_step(Maybe<&1, State & List<&2, Field>>, step, state => cursor => field =>
500	          with_end(Maybe<&1, State & List<&2, Field>>, cursor, cursor => ended =>
501	            with_fields(Maybe<&1, State & List<&2, Field>>, decode.add(field, acc, seen), fields => was_field =>
502	              decode.go(p, ended, cursor, state, fields, was_field)))))
503	
504	def decode(block: Bytes.Bytes, st: State) -> Maybe<&1, State & List<&2, Field>>:
505	  Bytes.Bytes{+length, buf} = block
506	  decode.go(1n+U32.to_nat(length), U32.is_eq(length, 0),
507	    Cursor{Bytes.Bytes{length, buf}, 0, length}, st, Nil{}, False{})
508	
509	def integer.tail(n: Nat, +value: U32, active: Bool) -> String:
510	  match n active:
511	    case 0n _:
512	      SNil{}
513	    case 1n+p False{}:
514	      SNil{}
515	    case 1n+p True{}:
516	      SCon{Chr{((value .&. 127 : U32) .|. Bool.pick(U32, U32.is_ge(value, 128), 128, 0) : U32)},
517	        integer.tail(p, (value >> 7n : U32), U32.is_ge(value, 128))}
518	
519	def integer.encoded(small: Bool, +prefix: U32, +mask: U32, +value: U32) -> Bytes.Bytes:
520	  match small:
521	    case True{}:
522	      Bytes.from_string(SCon{Chr{(prefix .|. value : U32)}, SNil{}})
523	    case False{}:
524	      Bytes.from_string(SCon{Chr{(prefix .|. mask : U32)},
525	        integer.tail(5n, (value - mask : U32), True{})})
526	
527	def integer.encode(+prefix: U32, +mask: U32, +value: U32) -> Bytes.Bytes:
528	  integer.encoded(U32.is_lt(value, mask), prefix, mask, value)
529	
530	def octets.valid(s: String) -> Bool:
531	  match s:
532	    case SNil{}:
533	      True{}
534	    case SCon{Chr{+octet}, tail}:
535	      Bool.and(U32.is_le(octet, 255), octets.valid(tail))
536	
537	def literal.raw(+s: String) -> Maybe<&1, Bytes.Bytes>:
538	  do Maybe<&1, Bytes.Bytes>:
539	    unused: Unit <- within(octets.valid(s))
540	    return Bytes.from_string(s)
541	
542	def literal.pack(b: Bytes.Bytes, huff: Bool) -> Bytes.Bytes:
543	  Bytes.Bytes{+length, buf} = b
544	  Bytes.concat([integer.encode(Bool.pick(U32, huff, 128, 0), 127, length), Bytes.Bytes{length, buf}])
545	
546	def literal.encode(huff: Bool, s: String) -> Maybe<&1, Bytes.Bytes>:
547	  match huff:
548	    case True{}:
549	      Maybe.map(&1, Bytes.Bytes, Bytes.Bytes, b => literal.pack(b, True{}), Huff.encode(s))
550	    case False{}:
551	      Maybe.map(&1, Bytes.Bytes, Bytes.Bytes, b => literal.pack(b, False{}), literal.raw(s))
552	
553	def name.parts(+index: U32, huff: Bool, name: String) -> Maybe<&1, List<&1, Bytes.Bytes>>:
554	  match index:
555	    case 0:
556	      Maybe.map(&1, Bytes.Bytes, List<&1, Bytes.Bytes>, b => [b], literal.encode(huff, name))
557	    case _:
558	      Some{Nil{}}
559	
560	def encode.literal.bytes(+index: U32, +prefix: U32, +mask: U32, +huff: Bool, name: String, value: String) -> Maybe<&1, Bytes.Bytes>:
561	  do Maybe<&1, Bytes.Bytes>:
562	    parts: List<&1, Bytes.Bytes> <- name.parts(index, huff, name)
563	    encoded: Bytes.Bytes <- literal.encode(huff, value)
564	    return Bytes.concat(Con{integer.encode(prefix, mask, index),
565	      List.append(&1, Bytes.Bytes, parts, [encoded])})
566	
567	def encode.literal.done(insert: Bool, field: Field, st: State, b: Bytes.Bytes) -> Maybe<&1, State & Bytes.Bytes>:
568	  match insert:
569	    case True{}:
570	      Some{(table.insert(field, st), b)}
571	    case False{}:
572	      Some{(st, b)}
573	
574	def encode.literal(+mode: U32, +name: String, +value: String, huff: Bool, +st: State) -> Maybe<&1, State & Bytes.Bytes>:
575	  +index = find.index(False{}, st, name, value)
576	  +prefix = Bool.pick(U32, U32.is_eq(mode, 0), 64, Bool.pick(U32, U32.is_eq(mode, 2), 16, 0))
577	  +mask = Bool.pick(U32, U32.is_eq(mode, 0), 63, 15)
578	  Maybe.bind(&1, Bytes.Bytes, State & Bytes.Bytes,
579	    encode.literal.bytes(index, prefix, mask, huff, name, value), b =>
580	      encode.literal.done(U32.is_eq(mode, 0), Field{name, value, mode}, st, b))
581	
582	def encode.exact(found: Bool, +index: U32, +name: String, +value: String, huff: Bool, st: State) -> Maybe<&1, State & Bytes.Bytes>:
583	  match found:
584	    case True{}:
585	      Some{(st, integer.encode(128, 127, index))}
586	    case False{}:
587	      encode.literal(0, name, value, huff, st)
588	
589	def encode.field(f: Field, huff: Bool, +st: State) -> Maybe<&1, State & Bytes.Bytes>:
590	  Field{+name, +value, mode} = f
591	  match mode:
592	    case 0:
593	      +index = find.index(True{}, st, name, value)
594	      encode.exact(U32.is_ne(index, 0), index, name, value, huff, st)
595	    case 1:
596	      encode.literal(1, name, value, huff, st)
597	    case 2:
598	      encode.literal(2, name, value, huff, st)
599	    case _:
600	      None{}
601	
602	
603	def encode.cleared(st: State, pieces: List<&1, Bytes.Bytes>) -> State & List<&1, Bytes.Bytes>:
604	  State{entries, size, capacity, allowed, pending, minimum} = st
605	  (State{entries, size, capacity, allowed, None{}, None{}}, pieces)
606	
607	def encode.emit(smaller: Bool, +minimum: U32, +final: U32, st: State) -> State & List<&1, Bytes.Bytes>:
608	  match smaller:
609	    case True{}:
610	      encode.cleared(table.resize(final, table.resize(minimum, st)),
611	        [integer.encode(32, 31, minimum), integer.encode(32, 31, final)])
612	    case False{}:
613	      encode.cleared(table.resize(final, st), [integer.encode(32, 31, final)])
614	
615	def encode.pending(m: Maybe<&2, U32>, minimum: Maybe<&2, U32>, st: State) -> State & List<&1, Bytes.Bytes>:
616	  match m:
617	    case None{}:
618	      (st, Nil{})
619	    case Some{+final}:
620	      +smallest = limit.min(minimum, final)
621	      encode.emit(U32.is_lt(smallest, final), smallest, final, st)
622	
623	def encode.prepare(st: State) -> State & List<&1, Bytes.Bytes>:
624	  State{entries, size, capacity, allowed, +pending, +minimum} = st
625	  encode.pending(pending, minimum, State{entries, size, capacity, allowed, pending, minimum})
626	
627	def with_encoded(-R: Type, r: State & Bytes.Bytes, k: State -> Bytes.Bytes -> R) -> R:
628	  (st, bytes) = r
629	  k(st, bytes)
630	
631	def encode.go(xs: List<&2, Field>, +huff: Bool, st: State, acc: List<&1, Bytes.Bytes>) -> Maybe<&1, State & List<&1, Bytes.Bytes>>:
632	  match xs:
633	    case Nil{}:
634	      Some{(st, acc)}
635	    case Con{field, tail}:
636	      Maybe.bind(&1, State & Bytes.Bytes, State & List<&1, Bytes.Bytes>, encode.field(field, huff, st), pair =>
637	        with_encoded(Maybe<&1, State & List<&1, Bytes.Bytes>>, pair, state => bytes =>
638	          encode.go(tail, huff, state, Con{bytes, acc})))
639	
640	def encode.finish(r: State & List<&1, Bytes.Bytes>) -> State & Bytes.Bytes:
641	  (st, pieces) = r
642	  (st, Bytes.concat(List.reverse(&1, Bytes.Bytes, pieces)))
643	
644	def encode.from(r: State & List<&1, Bytes.Bytes>, fields: List<&2, Field>, huff: Bool) -> Maybe<&1, State & Bytes.Bytes>:
645	  (st, updates) = r
646	  Maybe.map(&1, State & List<&1, Bytes.Bytes>, State & Bytes.Bytes, encode.finish,
647	    encode.go(fields, huff, st, List.reverse(&1, Bytes.Bytes, updates)))
648	
649	def encode(fields: List<&2, Field>, huff: Bool, st: State) -> Maybe<&1, State & Bytes.Bytes>:
650	  encode.from(encode.prepare(st), fields, huff)
651