1	# HTTP/1.1 client and server for http and https, with DNS and TLS. Source: https://github.com/paymog/bend-kit/tree/main/http
2	import Base
3	# By hash: bend-kit-wire@0.4.0.3, -url@0.4.0.0, -encoding@0.3.0.0, -json@0.3.0.0, -bytes@0.3.0.0, -dns@0.3.2.1, -zlib@0.1.0.0.
4	import 0x096635686408886b7d907f16c4550317/wire.bend as Wire
5	import 0xd248560355ba8929ae030bc9c72f40be/url.bend as Url
6	import 0xcfc8be7b076f41f95c8e118383892d55/encoding.bend as Enc
7	import 0xaaa10a97bf5ac6990143da2c863f8a3f/json.bend as Json
8	import 0x49814d83de8f70993a43e1002be29ecd/bytes.bend as Bytes
9	import 0xc10a5eaaa9c896e1570e279945f4241e/dns.bend as Dns
10	import 0xe01785b64266bf3ba0068183b9f9f5e3/zlib.bend as Zlib
11	
12	# HTTP/1.1 codec and client (RFC 9112) for http:// and https:// (OpenSSL 3 at run time).
13	# parse: start-line → field lines → blank → body length (§6.3); chunked (§7.1).
14	# Bodies are Bytes. The String parsers below are the spec: one Char per octet.
15	# fetch reads until frame() says the response is whole. It returns Result, not Maybe.
16	# Build with -o for big bodies: the `bend file.bend` runner overflows on ~30 KB strings; native binaries do not.
17	#   import bend-kit-http@0.15.0.0/http.bend as Http
18	
19	type Req is Type:
20	  Req{method: String, path: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
21	
22	type Res is Type:
23	  Res{status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
24	
25	# The body type and its conversions, so a caller needs no bytes import.
26	def Body() -> Type:
27	  Bytes.Bytes
28	
29	# A byte string (one Char per octet) to a body, and back.
30	def from_string(+s: String) -> Bytes.Bytes:
31	  Bytes.from_string(s)
32	
33	def to_string(b: Bytes.Bytes) -> String:
34	  Bytes.to_string(b)
35	
36	def length(b: Bytes.Bytes) -> Bytes.Bytes & U32:
37	  Bytes.length(b)
38	
39	# Why fetch failed. Wire errors keep the errno and the text the effect already had.
40	# ponytail: 60 and 110 are ETIMEDOUT on macOS and Linux. Windows is out of scope.
41	type Err is Data:
42	  ErrUrl{}
43	  ErrDns{}
44	  ErrConnect{code: U32, why: String}
45	  ErrTls{code: U32, why: String}
46	  ErrRead{code: U32, why: String}
47	  ErrWrite{code: U32, why: String}
48	  ErrTimeout{}
49	  ErrRedirect{}
50	  ErrBad{}
51	
52	def err.late(+code: U32) -> Bool:
53	  Bool.or(U32.is_eq(code, 60), U32.is_eq(code, 110))
54	
55	def err.pick(e: Err, late: Bool) -> Err:
56	  match late:
57	    case True{}:
58	      ErrTimeout{}
59	    case False{}:
60	      e
61	
62	def err.or_late(code: U32, e: Err) -> Err:
63	  err.pick(e, err.late(code))
64	
65	type Fields is Data:
66	  FieldsBad{}
67	  FieldsOk{m: Map<&2, List<&2, String>>}
68	
69	# One list per field name, in arrival order. header() is the first value.
70	# Set-Cookie is never joined. Encode writes one line per value.
71	def empty() -> Map<&2, List<&2, String>>:
72	  Map.new(&2, List<&2, String>)
73	
74	def fields.of(r: Map<&2, List<&2, String>> & List<&2, String>) -> List<&2, String>:
75	  (h, xs) = r
76	  xs
77	
78	def fields(+h: Map<&2, List<&2, String>>, k: String) -> List<&2, String>:
79	  fields.of(Map.get(List<&2, String>, Nil{}, h, k))
80	
81	def header.first(xs: List<&2, String>) -> String:
82	  match xs:
83	    case Nil{}:
84	      ""
85	    case Con{v, t}:
86	      v
87	
88	def header(+h: Map<&2, List<&2, String>>, k: String) -> String:
89	  header.first(fields(h, k))
90	
91	def field.last(xs: List<&2, String>) -> String:
92	  match xs:
93	    case Nil{}:
94	      ""
95	    case Con{v, Nil{}}:
96	      v
97	    case Con{v, t}:
98	      field.last(t)
99	
100	# Transfer-Encoding is a list; chunked, when present, is the last coding.
101	def header.last(+h: Map<&2, List<&2, String>>, k: String) -> String:
102	  field.last(fields(h, k))
103	
104	def snoc(xs: List<&2, String>, v: String) -> List<&2, String>:
105	  match xs:
106	    case Nil{}:
107	      [v]
108	    case Con{h, t}:
109	      Con{h, snoc(t, v)}
110	
111	def set(m: Map<&2, List<&2, String>>, k: String, v: String) -> Map<&2, List<&2, String>>:
112	  Map.set(&2, List<&2, String>, m, k, [v])
113	
114	def add(+m: Map<&2, List<&2, String>>, +k: String, v: String) -> Map<&2, List<&2, String>>:
115	  Map.set(&2, List<&2, String>, m, k, snoc(fields(m, k), v))
116	
117	def sanitize.cons(ch: Char, rest: String, drop: Bool) -> String:
118	  match drop:
119	    case True{}:
120	      rest
121	    case False{}:
122	      SCon{ch, rest}
123	
124	def sanitize(s: String) -> String:
125	  match s:
126	    case SNil{}:
127	      SNil{}
128	    case SCon{Chr{+c}, t}:
129	      sanitize.cons(Chr{c}, sanitize(t), Bool.or(U32.is_eq(c, 13), U32.is_eq(c, 10)))
130	
131	def drop_cr.if(+s: String, cr: Bool) -> String:
132	  match cr:
133	    case True{}:
134	      String.take(s, (String.length(s) - 1n : Nat))
135	    case False{}:
136	      s
137	
138	def drop_cr(+s: String) -> String:
139	  drop_cr.if(s, String.ends_with(s, "\r"))
140	
141	# Bool.pick evaluates both arms; a split that recursed inside it would reverse acc at every byte.
142	def take.cut(acc: String, rest: String) -> String & String:
143	  (String.reverse(String.drop(acc, 1n)), rest)
144	
145	# hit: the last char pushed onto acc was the stop char.
146	def take_sp.go(s: String, acc: String, hit: Bool) -> String & String:
147	  match s:
148	    case SNil{}:
149	      match hit:
150	        case True{}:
151	          take.cut(acc, SNil{})
152	        case False{}:
153	          (String.reverse(acc), SNil{})
154	    case SCon{Chr{+c}, t}:
155	      match hit:
156	        case True{}:
157	          take.cut(acc, SCon{Chr{c}, t})
158	        case False{}:
159	          take_sp.go(t, SCon{Chr{c}, acc}, U32.is_eq(c, 32))
160	
161	def take_sp(s: String) -> String & String:
162	  take_sp.go(s, SNil{}, False{})
163	
164	def start_line.ver(m: String, pv: String & String) -> String & String & String:
165	  (p, v) = pv
166	  (m, p, drop_cr(v))
167	
168	def start_line.rest(mr: String & String) -> String & String & String:
169	  (m, r) = mr
170	  start_line.ver(m, take_sp(r))
171	
172	def start_line(s: String) -> String & String & String:
173	  start_line.rest(take_sp(s))
174	
175	def split_at_blank.go(s: String, e: Bool, w: U32, acc: String) -> String & String:
176	  match s:
177	    case SNil{}:
178	      (String.reverse(acc), SNil{})
179	    case SCon{Chr{+a}, t}:
180	      match e:
181	        case True{}:
182	          (String.reverse(acc), SCon{Chr{a}, t})
183	        case False{}:
184	          +w2 = (w * 256 + a : U32)
185	          split_at_blank.go(t, U32.is_eq(w2, 218762506), w2, SCon{Chr{a}, acc})
186	
187	def split_at_blank.scan.go(+raw: String, s: String, off: Nat, w: U32, e: Bool) -> String & String:
188	  match s:
189	    case SNil{}:
190	      (String.take(raw, off), SNil{})
191	    case SCon{Chr{+a}, t}:
192	      match e:
193	        case True{}:
194	          (String.take(raw, off), SCon{Chr{a}, t})
195	        case False{}:
196	          +w2 = (w * 256 + a : U32)
197	          +off1 = (1n + off : Nat)
198	          split_at_blank.scan.go(raw, t, off1, w2, U32.is_eq(w2, 218762506))
199	
200	def split_at_blank(+s: String) -> String & String:
201	  split_at_blank.scan.go(s, s, 0n, 0, False{})
202	
203	def split_colon.go(s: String, acc: String, hit: Bool) -> String & String:
204	  match s:
205	    case SNil{}:
206	      match hit:
207	        case True{}:
208	          take.cut(acc, SNil{})
209	        case False{}:
210	          (String.reverse(acc), SNil{})
211	    case SCon{Chr{+c}, t}:
212	      match hit:
213	        case True{}:
214	          take.cut(acc, SCon{Chr{c}, t})
215	        case False{}:
216	          split_colon.go(t, SCon{Char.to_lower(Chr{c}), acc}, U32.is_eq(c, 58))
217	
218	def split_colon(+s: String) -> String & String:
219	  split_colon.go(s, SNil{}, False{})
220	
221	def has_header.of(r: Map<&2, List<&2, String>> & Bool) -> Bool:
222	  (h, b) = r
223	  b
224	
225	def has_header(+h: Map<&2, List<&2, String>>, k: String) -> Bool:
226	  has_header.of(Map.has(&2, List<&2, String>, h, k))
227	
228	def folded(+line: String) -> Bool:
229	  Bool.or(String.starts_with(line, " "), String.starts_with(line, "\t"))
230	
231	def tracked(+k: String) -> Bool:
232	  Bool.or(String.eq(k, "host"), String.eq(k, "content-length"))
233	
234	def fields_put.dup(m: Map<&2, List<&2, String>>, k: String, v: String, bad: Bool) -> Fields:
235	  match bad:
236	    case True{}:
237	      FieldsBad{}
238	    case False{}:
239	      FieldsOk{add(m, k, v)}
240	
241	def fields_put.key(+m: Map<&2, List<&2, String>>, +k: String, v: String) -> Fields:
242	  fields_put.dup(m, k, v, Bool.and(tracked(k), has_header(m, k)))
243	
244	def fields_put.kv(m: Map<&2, List<&2, String>>, kv: String & String) -> Fields:
245	  (k, v) = kv
246	  fields_put.key(m, k, String.trim(v))
247	
248	def fields_put.fold(m: Map<&2, List<&2, String>>, line: String, fold: Bool) -> Fields:
249	  match fold:
250	    case True{}:
251	      FieldsBad{}
252	    case False{}:
253	      fields_put.kv(m, split_colon(line))
254	
255	def fields_put.empty(m: Map<&2, List<&2, String>>, +line: String, e: Bool) -> Fields:
256	  match e:
257	    case True{}:
258	      FieldsOk{m}
259	    case False{}:
260	      fields_put.fold(m, line, folded(line))
261	
262	def fields_put.ok(m: Map<&2, List<&2, String>>, +line: String) -> Fields:
263	  fields_put.empty(m, line, String.is_empty(line))
264	
265	def fields_put(acc: Fields, line: String) -> Fields:
266	  match acc:
267	    case FieldsBad{}:
268	      FieldsBad{}
269	    case FieldsOk{m}:
270	      fields_put.ok(m, line)
271	
272	def parse.headers.done(acc: Fields) -> Maybe<&2, Map<&2, List<&2, String>>>:
273	  match acc:
274	    case FieldsBad{}:
275	      None{}
276	    case FieldsOk{m}:
277	      Some{m}
278	
279	def parse.headers(xs: List<&2, String>, acc: Fields) -> Maybe<&2, Map<&2, List<&2, String>>>:
280	  match xs:
281	    case Nil{}:
282	      parse.headers.done(acc)
283	    case Con{line, rest}:
284	      parse.headers(rest, fields_put(acc, drop_cr(line)))
285	
286	def parse_u32.digit(+c: U32) -> Bool:
287	  Bool.and(U32.is_le(48, c), U32.is_le(c, 57))
288	
289	def parse_u32.add(acc: U32, c: U32) -> U32:
290	  (acc * 10 + (c - 48 : U32) : U32)
291	
292	def parse_u32.done(acc: U32, bad: Bool) -> Maybe<&2, U32>:
293	  match bad:
294	    case True{}:
295	      None{}
296	    case False{}:
297	      Some{acc}
298	
299	def parse_u32.go(s: String, acc: U32, bad: Bool) -> Maybe<&2, U32>:
300	  match s:
301	    case SNil{}:
302	      parse_u32.done(acc, bad)
303	    case SCon{Chr{+c}, t}:
304	      parse_u32.go(t, parse_u32.add(acc, c), Bool.or(bad, Bool.not(parse_u32.digit(c))))
305	
306	def parse_u32(s: String) -> Maybe<&2, U32>:
307	  match s:
308	    case SNil{}:
309	      None{}
310	    case SCon{Chr{+c}, t}:
311	      parse_u32.go(t, parse_u32.add(0, c), Bool.not(parse_u32.digit(c)))
312	
313	# More: a valid prefix. Bad: cannot become a body. Body: a whole chunked body.
314	type Hold is Data:
315	  HoldMore{}
316	  HoldBad{}
317	  HoldBody{b: String}
318	  HoldUntil{b: String}
319	
320	def is_hex(+c: U32) -> Bool:
321	  Bool.or(parse_u32.digit(c), Bool.or(Bool.and(U32.is_le(97, c), U32.is_le(c, 102)), Bool.and(U32.is_le(65, c), U32.is_le(c, 70))))
322	
323	def hexv(+c: U32) -> U32:
324	  Bool.pick(U32, parse_u32.digit(c), (c - 48 : U32), Bool.pick(U32, U32.is_le(c, 70), (c - 55 : U32), (c - 87 : U32)))
325	
326	# A chunked body decoder that reads each byte once, so a body fed in pieces
327	# costs O(bytes) in total. Tr{j}: j bytes of the closing CRLF CRLF matched.
328	type Dc is Data:
329	  DcSize{acc: U32, seen: Bool}
330	  DcExt{n: U32}
331	  DcSizeLf{n: U32}
332	  DcData{k: U32}
333	  DcDataCr{}
334	  DcDataLf{}
335	  DcTr{j: U32}
336	  DcDone{}
337	  DcBad{}
338	
339	# st: where the decoder is. racc: the body so far, reversed. rest: bytes after a Done body.
340	type Dco is Data:
341	  Dco{st: Dc, racc: String, rest: String}
342	
343	def dc.start() -> Dc:
344	  DcSize{0, False{}}
345	
346	def dc.size.semi(+n: U32, semi: Bool) -> Dc:
347	  match semi:
348	    case True{}:
349	      DcExt{n}
350	    case False{}:
351	      DcBad{}
352	
353	def dc.size.cr(+n: U32, +c: U32, cr: Bool) -> Dc:
354	  match cr:
355	    case True{}:
356	      DcSizeLf{n}
357	    case False{}:
358	      dc.size.semi(n, U32.is_eq(c, 59))
359	
360	def dc.size.end(+n: U32, +c: U32, seen: Bool) -> Dc:
361	  match seen:
362	    case False{}:
363	      DcBad{}
364	    case True{}:
365	      dc.size.cr(n, c, U32.is_eq(c, 13))
366	
367	# A size that would overflow 32 bits ends the digits, and size.end then refuses it.
368	def dc.size(+acc: U32, seen: Bool, +c: U32, digit: Bool) -> Dc:
369	  match digit:
370	    case True{}:
371	      DcSize{(acc * 16 + hexv(c) : U32), True{}}
372	    case False{}:
373	      dc.size.end(acc, c, seen)
374	
375	# RFC 9112 §7.1.1: recipients ignore unknown chunk extensions; a bare LF is not CRLF.
376	def dc.ext.lf(+n: U32, lf: Bool) -> Dc:
377	  match lf:
378	    case True{}:
379	      DcBad{}
380	    case False{}:
381	      DcExt{n}
382	
383	def dc.ext(+n: U32, +c: U32, cr: Bool) -> Dc:
384	  match cr:
385	    case True{}:
386	      DcSizeLf{n}
387	    case False{}:
388	      dc.ext.lf(n, U32.is_eq(c, 10))
389	
390	def dc.sized(+n: U32, zero: Bool) -> Dc:
391	  match zero:
392	    case True{}:
393	      DcTr{2}
394	    case False{}:
395	      DcData{n}
396	
397	def dc.size.lf(+n: U32, lf: Bool) -> Dc:
398	  match lf:
399	    case True{}:
400	      dc.sized(n, U32.is_eq(n, 0))
401	    case False{}:
402	      DcBad{}
403	
404	# k data bytes are left and m of them were just read.
405	def dc.data(+k: U32, +m: U32) -> Dc:
406	  Bool.pick(Dc, U32.is_le(k, m), DcDataCr{}, DcData{(k - m : U32)})
407	
408	def dc.pick(ok: Bool, next: Dc) -> Dc:
409	  match ok:
410	    case True{}:
411	      next
412	    case False{}:
413	      DcBad{}
414	
415	# ponytail: trailer fields are dropped unparsed (§7.1.2 allows discarding)
416	def dc.tr.hit(+j: U32) -> Dc:
417	  Bool.pick(Dc, U32.is_eq(j, 3), DcDone{}, DcTr{(j + 1 : U32)})
418	
419	def dc.tr(+j: U32, +c: U32, hit: Bool) -> Dc:
420	  match hit:
421	    case True{}:
422	      dc.tr.hit(j)
423	    case False{}:
424	      Bool.pick(Dc, U32.is_eq(c, 13), DcTr{1}, DcTr{0})
425	
426	def dc.tr.want(+j: U32) -> U32:
427	  Bool.pick(U32, U32.is_eq(U32.mod(j, 2), 0), 13, 10)
428	
429	def dc.byte(h: Char) -> U32:
430	  Chr{c} = h
431	  c
432	
433	# One byte c. Done and Bad never look at it, and a data byte is not inspected.
434	def dc.step(st: Dc, +c: U32) -> Dc:
435	  match st:
436	    case DcBad{}:
437	      DcBad{}
438	    case DcSize{+acc, seen}:
439	      dc.size(acc, seen, c, Bool.and(is_hex(c), U32.is_le(acc, 268435455)))
440	    case DcExt{+n}:
441	      dc.ext(n, c, U32.is_eq(c, 13))
442	    case DcSizeLf{+n}:
443	      dc.size.lf(n, U32.is_eq(c, 10))
444	    case DcDataCr{}:
445	      dc.pick(U32.is_eq(c, 13), DcDataLf{})
446	    case DcDataLf{}:
447	      dc.pick(U32.is_eq(c, 10), dc.start())
448	    case DcTr{+j}:
449	      dc.tr(j, c, U32.is_eq(c, dc.tr.want(j)))
450	    case DcData{+k}:
451	      dc.data(k, 1)
452	    case DcDone{}:
453	      DcDone{}
454	
455	def dc.live(st: Dc) -> Bool:
456	  match st:
457	    case DcDone{}:
458	      False{}
459	    case DcBad{}:
460	      False{}
461	    case DcSize{a, b}:
462	      True{}
463	    case DcExt{n}:
464	      True{}
465	    case DcSizeLf{n}:
466	      True{}
467	    case DcData{k}:
468	      True{}
469	    case DcDataCr{}:
470	      True{}
471	    case DcDataLf{}:
472	      True{}
473	    case DcTr{j}:
474	      True{}
475	
476	def dc.feed(s: String, st: Dc, racc: String) -> Dco:
477	  match s:
478	    case SNil{}:
479	      Dco{st, racc, ""}
480	    case SCon{h, t}:
481	      match st:
482	        case DcBad{}:
483	          Dco{DcBad{}, racc, ""}
484	        case DcDone{}:
485	          Dco{DcDone{}, racc, SCon{h, t}}
486	        case DcData{+k}:
487	          dc.feed(t, dc.data(k, 1), SCon{h, racc})
488	        case DcSize{+acc, seen}:
489	          dc.feed(t, dc.step(DcSize{acc, seen}, dc.byte(h)), racc)
490	        case DcExt{+n}:
491	          dc.feed(t, dc.step(DcExt{n}, dc.byte(h)), racc)
492	        case DcSizeLf{+n}:
493	          dc.feed(t, dc.step(DcSizeLf{n}, dc.byte(h)), racc)
494	        case DcDataCr{}:
495	          dc.feed(t, dc.step(DcDataCr{}, dc.byte(h)), racc)
496	        case DcDataLf{}:
497	          dc.feed(t, dc.step(DcDataLf{}, dc.byte(h)), racc)
498	        case DcTr{+j}:
499	          dc.feed(t, dc.step(DcTr{j}, dc.byte(h)), racc)
500	
501	def chunk.hold(o: Dco) -> Hold:
502	  Dco{st, racc, rest} = o
503	  match st:
504	    case DcDone{}:
505	      HoldBody{String.reverse(racc)}
506	    case DcBad{}:
507	      HoldBad{}
508	    case DcSize{a, b}:
509	      HoldMore{}
510	    case DcExt{n}:
511	      HoldMore{}
512	    case DcSizeLf{n}:
513	      HoldMore{}
514	    case DcData{k}:
515	      HoldMore{}
516	    case DcDataCr{}:
517	      HoldMore{}
518	    case DcDataLf{}:
519	      HoldMore{}
520	    case DcTr{j}:
521	      HoldMore{}
522	
523	def chunk.live(s: String) -> Hold:
524	  chunk.hold(dc.feed(s, dc.start(), ""))
525	
526	def chunk.rest(o: Dco) -> Maybe<&2, String>:
527	  Dco{st, racc, rest} = o
528	  match st:
529	    case DcDone{}:
530	      Some{rest}
531	    case DcBad{}:
532	      None{}
533	    case DcSize{a, b}:
534	      None{}
535	    case DcExt{n}:
536	      None{}
537	    case DcSizeLf{n}:
538	      None{}
539	    case DcData{k}:
540	      None{}
541	    case DcDataCr{}:
542	      None{}
543	    case DcDataLf{}:
544	      None{}
545	    case DcTr{j}:
546	      None{}
547	
548	def chunk.suffix(s: String) -> Maybe<&2, String>:
549	  chunk.rest(dc.feed(s, dc.start(), ""))
550	
551	def chunk.decode.hold(h: Hold) -> Maybe<&2, String>:
552	  match h:
553	    case HoldMore{}:
554	      None{}
555	    case HoldBad{}:
556	      None{}
557	    case HoldUntil{b}:
558	      None{}
559	    case HoldBody{b}:
560	      Some{b}
561	
562	def chunk.decode(s: String) -> Maybe<&2, String>:
563	  chunk.decode.hold(chunk.live(s))
564	
565	def bytes.snd(r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes:
566	  (a, b) = r
567	  b
568	
569	def found.at(+from: U32, m: Maybe<&2, U32>) -> Maybe<&2, U32>:
570	  match m:
571	    case None{}:
572	      None{}
573	    case Some{+j}:
574	      Some{(from + j : U32)}
575	
576	# A chunked body decoded from piece[i..]: a data run is sliced whole, and every other byte steps dc.
577	type Cs is Type:
578	  Cs{piece: Bytes.Bytes, i: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
579	
580	# st: where the decoder stopped. parts: the data so far, newest first. rest: the bytes after a Done body.
581	type Ck is Type:
582	  Ck{st: Dc, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
583	
584	def ck.next(+len: U32, +i: U32, +st: Dc, piece: Bytes.Bytes, parts: List<&1, Bytes.Bytes>) -> Bool & Cs:
585	  (Bool.and(U32.is_lt(i, len), dc.live(st)), Cs{piece, i, st, parts})
586	
587	def ck.data(+len: U32, +i: U32, +k: U32, +m: U32, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Bool & Cs:
588	  (piece, run) = r
589	  ck.next(len, (i + m : U32), dc.data(k, m), piece, Con{run, parts})
590	
591	def ck.byte(+len: U32, +i: U32, st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Maybe<&2, U32>) -> Bool & Cs:
592	  (piece, m) = r
593	  match m:
594	    case None{}:
595	      ck.next(len, i, DcBad{}, piece, parts)
596	    case Some{+c}:
597	      ck.next(len, (i + 1 : U32), dc.step(st, c), piece, parts)
598	
599	def ck.step(+len: U32, cs: Cs) -> Bool & Cs:
600	  Cs{piece, +i, st, parts} = cs
601	  match st:
602	    case DcData{+k}:
603	      +m = U32.min(k, (len - i : U32))
604	      ck.data(len, i, k, m, parts, Bytes.slice(piece, i, m))
605	    case DcDone{}:
606	      (False{}, Cs{piece, i, DcDone{}, parts})
607	    case DcBad{}:
608	      (False{}, Cs{piece, i, DcBad{}, parts})
609	    case DcSize{+acc, seen}:
610	      ck.byte(len, i, DcSize{acc, seen}, parts, Bytes.get(piece, i))
611	    case DcExt{+n}:
612	      ck.byte(len, i, DcExt{n}, parts, Bytes.get(piece, i))
613	    case DcSizeLf{+n}:
614	      ck.byte(len, i, DcSizeLf{n}, parts, Bytes.get(piece, i))
615	    case DcDataCr{}:
616	      ck.byte(len, i, DcDataCr{}, parts, Bytes.get(piece, i))
617	    case DcDataLf{}:
618	      ck.byte(len, i, DcDataLf{}, parts, Bytes.get(piece, i))
619	    case DcTr{+j}:
620	      ck.byte(len, i, DcTr{j}, parts, Bytes.get(piece, i))
621	
622	def ck.rest(st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Ck:
623	  (piece, rest) = r
624	  Ck{st, parts, rest}
625	
626	def ck.end(+len: U32, cs: Cs) -> Ck:
627	  Cs{piece, +i, st, parts} = cs
628	  ck.rest(st, parts, Bytes.slice(piece, i, (len - i : U32)))
629	
630	# Each step reads at least one byte, so len steps are enough.
631	def ck.feed(f: Nat, +len: U32, r: Bool & Cs) -> Ck:
632	  match f:
633	    case 0n:
634	      (go, cs) = r
635	      ck.end(len, cs)
636	    case 1n+p:
637	      (go, cs) = r
638	      match go:
639	        case False{}:
640	          ck.end(len, cs)
641	        case True{}:
642	          ck.feed(p, len, ck.step(len, cs))
643	
644	def ck(piece: Bytes.Bytes, +st: Dc, parts: List<&1, Bytes.Bytes>) -> Ck:
645	  Bytes.Bytes{+len, buf} = piece
646	  ck.feed(U32.to_nat(len), len, ck.next(len, 0, st, Bytes.Bytes{len, buf}, parts))
647	
648	def parse.res.cl.have(+rest: String, +k: Nat, short: Bool) -> Hold:
649	  match short:
650	    case True{}:
651	      HoldMore{}
652	    case False{}:
653	      HoldBody{String.take(rest, k)}
654	
655	def parse.res.cl.k(+rest: String, +k: Nat) -> Hold:
656	  parse.res.cl.have(rest, k, Nat.is_lt(String.length(rest), k))
657	
658	def parse.res.cl.n(rest: String, n: Maybe<&2, U32>) -> Hold:
659	  match n:
660	    case None{}:
661	      HoldBad{}
662	    case Some{k}:
663	      parse.res.cl.k(rest, U32.to_nat(k))
664	
665	def parse.body.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
666	  match hascl:
667	    case False{}:
668	      HoldBody{""}
669	    case True{}:
670	      parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
671	
672	# RFC 9112 §6.3 (4): a request coding other than chunked cannot be framed.
673	def parse.body.chunked.eq(rest: String, ok: Bool) -> Hold:
674	  match ok:
675	    case False{}:
676	      HoldBad{}
677	    case True{}:
678	      chunk.live(rest)
679	
680	def parse.body.chunked.val(te: String, rest: String) -> Hold:
681	  parse.body.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
682	
683	def parse.body.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
684	  match hascl:
685	    case True{}:
686	      HoldBad{}
687	    case False{}:
688	      parse.body.chunked.val(header.last(h, "transfer-encoding"), rest)
689	
690	def parse.body.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
691	  match te:
692	    case True{}:
693	      parse.body.chunked(h, rest, has_header(h, "content-length"))
694	    case False{}:
695	      parse.body.cl(h, rest, has_header(h, "content-length"))
696	
697	def parse.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
698	  parse.body.te(h, rest, has_header(h, "transfer-encoding"))
699	
700	# Bad: never a request. More: the head is not whole; read on. Head: the head is whole
701	# and valid, and the body is still coming (req.body is empty). Req: a whole request.
702	type Got is Type:
703	  GotBad{}
704	  GotMore{}
705	  GotHead{req: Req}
706	  GotReq{req: Req}
707	
708	def parse.finish(method: String, path: String, h: Map<&2, List<&2, String>>, body: Hold) -> Got:
709	  match body:
710	    case HoldBad{}:
711	      GotBad{}
712	    case HoldMore{}:
713	      GotHead{Req{method, path, h, Bytes.new(0)}}
714	    case HoldUntil{b}:
715	      GotBad{}
716	    case HoldBody{b}:
717	      GotReq{Req{method, path, h, Bytes.from_string(b)}}
718	
719	def parse.host(method: String, path: String, +h: Map<&2, List<&2, String>>, rest: String, has: Bool) -> Got:
720	  match has:
721	    case False{}:
722	      GotBad{}
723	    case True{}:
724	      parse.finish(method, path, h, parse.body(h, rest))
725	
726	# RFC 9112 §3.2: only HTTP/1.1 requires Host.
727	def parse.fields(method: String, path: String, rest: String, v11: Bool, fs: Maybe<&2, Map<&2, List<&2, String>>>) -> Got:
728	  match fs:
729	    case None{}:
730	      GotBad{}
731	    case Some{+h}:
732	      parse.host(method, path, h, rest, Bool.or(Bool.not(v11), has_header(h, "host")))
733	
734	def target_ok(+p: String) -> Bool:
735	  Bool.or(String.starts_with(p, "/"), Bool.or(String.eq(p, "*"), String.starts_with(p, "http://")))
736	
737	def parse.target(method: String, +path: String, headers: List<&2, String>, rest: String, v11: Bool, ok: Bool) -> Got:
738	  match ok:
739	    case False{}:
740	      GotBad{}
741	    case True{}:
742	      parse.fields(method, path, rest, v11, parse.headers(headers, FieldsOk{empty()}))
743	
744	def parse.ver(method: String, +path: String, +v: String, headers: List<&2, String>, rest: String, ok: Bool) -> Got:
745	  match ok:
746	    case False{}:
747	      GotBad{}
748	    case True{}:
749	      parse.target(method, path, headers, rest, String.eq(v, "HTTP/1.1"), target_ok(path))
750	
751	def parse.empty_method(method: String, path: String, +v: String, headers: List<&2, String>, rest: String, empty: Bool) -> Got:
752	  match empty:
753	    case True{}:
754	      GotBad{}
755	    case False{}:
756	      parse.ver(method, path, v, headers, rest, Bool.or(String.eq(v, "HTTP/1.1"), String.eq(v, "HTTP/1.0")))
757	
758	def parse.start3(mpv: String & String & String, headers: List<&2, String>, rest: String) -> Got:
759	  (+method, path, v) = mpv
760	  parse.empty_method(method, path, v, headers, rest, String.is_empty(method))
761	
762	def parse.lines(xs: List<&2, String>, rest: String) -> Got:
763	  match xs:
764	    case Nil{}:
765	      GotBad{}
766	    case Con{line, headers}:
767	      parse.start3(start_line(line), headers, rest)
768	
769	
770	def parse.head(+head: String, rest: String, whole: Bool) -> Got:
771	  match whole:
772	    case False{}:
773	      GotMore{}
774	    case True{}:
775	      parse.lines(String.lines(head), rest)
776	
777	def parse.of(hb: String & String) -> Got:
778	  (+head, rest) = hb
779	  parse.head(head, rest, String.ends_with(head, "\r\n\r\n"))
780	
781	# serve reads until this is not GotMore.
782	def parse.got(raw: String) -> Got:
783	  parse.of(split_at_blank(raw))
784	
785	
786	def parse.req(g: Got) -> Maybe<&1, Req>:
787	  match g:
788	    case GotReq{req}:
789	      Some{req}
790	    case GotBad{}:
791	      None{}
792	    case GotMore{}:
793	      None{}
794	    case GotHead{req}:
795	      None{}
796	
797	def parse(raw: String) -> Maybe<&1, Req>:
798	  parse.req(parse.got(raw))
799	
800	def parse.res.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
801	  match hascl:
802	    case False{}:
803	      HoldBody{rest}
804	    case True{}:
805	      parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
806	
807	def parse.res.chunked.eq(rest: String, ok: Bool) -> Hold:
808	  match ok:
809	    case False{}:
810	      HoldUntil{rest}
811	    case True{}:
812	      chunk.live(rest)
813	
814	def parse.res.chunked.val(te: String, rest: String) -> Hold:
815	  parse.res.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
816	
817	def parse.res.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
818	  match hascl:
819	    case True{}:
820	      HoldBad{}
821	    case False{}:
822	      parse.res.chunked.val(header.last(h, "transfer-encoding"), rest)
823	
824	def parse.res.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
825	  match te:
826	    case True{}:
827	      parse.res.chunked(h, rest, has_header(h, "content-length"))
828	    case False{}:
829	      parse.res.cl(h, rest, has_header(h, "content-length"))
830	
831	def parse.res.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
832	  parse.res.te(h, rest, has_header(h, "transfer-encoding"))
833	
834	# Bad: never a message. More: a valid prefix; read on. Done: a whole response.
835	type Frame is Type:
836	  FrameBad{}
837	  FrameMore{}
838	  FrameDone{res: Res}
839	
840	# RFC 9112 §8: a message cut short by close is incomplete, not valid.
841	def frame.cut(closed: Bool) -> Frame:
842	  match closed:
843	    case True{}:
844	      FrameBad{}
845	    case False{}:
846	      FrameMore{}
847	
848	def frame.wait(res: Res, wait: Bool) -> Frame:
849	  match wait:
850	    case True{}:
851	      FrameMore{}
852	    case False{}:
853	      FrameDone{res}
854	
855	def frame.done(status: U32, h: Map<&2, List<&2, String>>, body: Hold, +closed: Bool, open: Bool) -> Frame:
856	  match body:
857	    case HoldBad{}:
858	      FrameBad{}
859	    case HoldMore{}:
860	      frame.cut(closed)
861	    case HoldUntil{b}:
862	      frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.not(closed))
863	    case HoldBody{b}:
864	      frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.and(open, Bool.not(closed)))
865	
866	# RFC 9112 §6.3 (8): no TE and no CL ⇒ the body runs until the server closes.
867	def frame.open(+h: Map<&2, List<&2, String>>) -> Bool:
868	  Bool.not(Bool.or(has_header(h, "transfer-encoding"), has_header(h, "content-length")))
869	
870	# RFC 9112 §6.3 (1): HEAD, 1xx, 204 and 304 responses end at the blank line.
871	def frame.nobody(+status: U32, head: Bool) -> Bool:
872	  Bool.or(head, Bool.or(U32.is_lt(status, 200), Bool.or(U32.is_eq(status, 204), U32.is_eq(status, 304))))
873	
874	# 101 is the final response. Other 1xx are interim; a final response follows.
875	def frame.interim(+status: U32) -> Bool:
876	  Bool.and(U32.is_lt(status, 200), Bool.not(U32.is_eq(status, 101)))
877	
878	def frame.status(status: U32, +h: Map<&2, List<&2, String>>, rest: String, closed: Bool, nobody: Bool) -> Frame:
879	  match nobody:
880	    case True{}:
881	      FrameDone{Res{status, h, Bytes.new(0)}}
882	    case False{}:
883	      frame.done(status, h, parse.res.body(h, rest), closed, frame.open(h))
884	
885	def parse.res.fields(+status: U32, rest: String, fs: Maybe<&2, Map<&2, List<&2, String>>>, closed: Bool, head: Bool) -> Frame:
886	  match fs:
887	    case None{}:
888	      FrameBad{}
889	    case Some{h}:
890	      frame.status(status, h, rest, closed, frame.nobody(status, head))
891	
892	def parse.res.num(code: Maybe<&2, U32>, headers: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
893	  match code:
894	    case None{}:
895	      FrameBad{}
896	    case Some{n}:
897	      parse.res.fields(n, rest, parse.headers(headers, FieldsOk{empty()}), closed, head)
898	
899	def parse.res.ver(code: String, headers: List<&2, String>, rest: String, closed: Bool, head: Bool, ok: Bool) -> Frame:
900	  match ok:
901	    case False{}:
902	      FrameBad{}
903	    case True{}:
904	      parse.res.num(parse_u32(code), headers, rest, closed, head)
905	
906	def parse.res.start3(mpv: String & String & String, headers: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
907	  (+ver, code, reason) = mpv
908	  parse.res.ver(code, headers, rest, closed, head, Bool.or(String.eq(ver, "HTTP/1.1"), String.eq(ver, "HTTP/1.0")))
909	
910	def parse.res.lines(xs: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
911	  match xs:
912	    case Nil{}:
913	      FrameBad{}
914	    case Con{line, headers}:
915	      parse.res.start3(start_line(line), headers, rest, closed, head)
916	
917	def parse.res.blank(hd: String, rest: String, +closed: Bool, head: Bool, ok: Bool) -> Frame:
918	  match ok:
919	    case False{}:
920	      frame.cut(closed)
921	    case True{}:
922	      parse.res.lines(String.lines(hd), rest, closed, head)
923	
924	def parse.res.of(hb: String & String, closed: Bool, head: Bool) -> Frame:
925	  (+hd, rest) = hb
926	  parse.res.blank(hd, rest, closed, head, String.ends_with(hd, "\r\n\r\n"))
927	
928	type Lead is Data:
929	  LeadCut{}
930	  LeadFinal{}
931	  LeadSkip{+rest: String}
932	
933	def frame.lead.if(rest: String, interim: Bool) -> Lead:
934	  match interim:
935	    case True{}:
936	      LeadSkip{rest}
937	    case False{}:
938	      LeadFinal{}
939	
940	def frame.lead.num(n: Maybe<&2, U32>, rest: String) -> Lead:
941	  match n:
942	    case None{}:
943	      LeadFinal{}
944	    case Some{s}:
945	      frame.lead.if(rest, frame.interim(s))
946	
947	def frame.lead.code(mpv: String & String & String, rest: String) -> Lead:
948	  (ver, code, reason) = mpv
949	  frame.lead.num(parse_u32(code), rest)
950	
951	def frame.lead.lines(xs: List<&2, String>, rest: String) -> Lead:
952	  match xs:
953	    case Nil{}:
954	      LeadFinal{}
955	    case Con{line, headers}:
956	      frame.lead.code(start_line(line), rest)
957	
958	def frame.lead.blank(+hd: String, rest: String, ok: Bool) -> Lead:
959	  match ok:
960	    case False{}:
961	      LeadCut{}
962	    case True{}:
963	      frame.lead.lines(String.lines(hd), rest)
964	
965	def frame.lead(hb: String & String) -> Lead:
966	  (+hd, rest) = hb
967	  frame.lead.blank(hd, rest, String.ends_with(hd, "\r\n\r\n"))
968	
969	def frame.at.cont(+raw: String, lead: Lead) -> String:
970	  match lead:
971	    case LeadCut{}:
972	      raw
973	    case LeadFinal{}:
974	      raw
975	    case LeadSkip{rest}:
976	      rest
977	
978	def frame.at.zero.go(+raw: String, closed: Bool, head: Bool, lead: Lead) -> Frame:
979	  match lead:
980	    case LeadCut{}:
981	      frame.cut(closed)
982	    case LeadFinal{}:
983	      parse.res.of(split_at_blank(raw), closed, head)
984	    case LeadSkip{rest}:
985	      FrameBad{}
986	
987	def frame.at.zero.of(+raw: String, closed: Bool, head: Bool) -> Frame:
988	  frame.at.zero.go(raw, closed, head, frame.lead(split_at_blank(raw)))
989	
990	def frame.at.pos.do(f: Nat, +raw: String, closed: Bool, head: Bool, hb: String & String, lead: Lead) -> Frame:
991	  match f:
992	    case 0n:
993	      match lead:
994	        case LeadCut{}:
995	          frame.cut(closed)
996	        case LeadFinal{}:
997	          parse.res.of(hb, closed, head)
998	        case LeadSkip{+rest}:
999	          frame.at.zero.of(rest, closed, head)
1000	    case 1n+g:
1001	      match lead:
1002	        case LeadCut{}:
1003	          frame.cut(closed)
1004	        case LeadFinal{}:
1005	          parse.res.of(hb, closed, head)
1006	        case LeadSkip{+rest}:
1007	          frame.at.pos.do(g, rest, closed, head, split_at_blank(rest), frame.lead(split_at_blank(rest)))
1008	
1009	def frame.at.zero(+raw: String, closed: Bool, head: Bool) -> Frame:
1010	  frame.at.zero.of(raw, closed, head)
1011	
1012	# ponytail: 8 interim responses; raise the fuel if a server sends more
1013	def frame.at(fuel: Nat, +raw: String, closed: Bool, head: Bool) -> Frame:
1014	  match fuel:
1015	    case 0n:
1016	      frame.at.zero(raw, closed, head)
1017	    case 1n+f:
1018	      frame.at.pos.do(f, raw, closed, head, split_at_blank(raw), frame.lead(split_at_blank(raw)))
1019	
1020	# frame(bytes so far, server closed?, request was HEAD?)
1021	def frame(raw: String, closed: Bool, head: Bool) -> Frame:
1022	  frame.at(8n, raw, closed, head)
1023	
1024	def frame.res(f: Frame) -> Maybe<&1, Res>:
1025	  match f:
1026	    case FrameDone{res}:
1027	      Some{res}
1028	    case FrameBad{}:
1029	      None{}
1030	    case FrameMore{}:
1031	      None{}
1032	
1033	def parse_res(raw: String) -> Maybe<&1, Res>:
1034	  frame.res(frame(raw, True{}, False{}))
1035	
1036	def res_fields.res(res: Res, k: String) -> List<&2, String>:
1037	  Res{status, headers, body} = res
1038	  fields(headers, k)
1039	
1040	def res_fields(m: Maybe<&1, Res>, k: String) -> List<&2, String>:
1041	  match m:
1042	    case None{}:
1043	      Nil{}
1044	    case Some{res}:
1045	      res_fields.res(res, k)
1046	
1047	# The response body as it arrives. Len: bytes left. Chunk: the decoder. Close: until the
1048	# server closes. Done: the body is whole. Bad: it cannot become a body.
1049	type Rb is Data:
1050	  RbLen{left: U32}
1051	  RbChunk{st: Dc}
1052	  RbClose{}
1053	  RbDone{}
1054	  RbBad{}
1055	
1056	def rb.cl(n: Maybe<&2, U32>) -> Maybe<&2, Rb>:
1057	  match n:
1058	    case None{}:
1059	      None{}
1060	    case Some{+k}:
1061	      Some{Bool.pick(Rb, U32.is_zero(k), RbDone{}, RbLen{k})}
1062	
1063	def rb.te(+h: Map<&2, List<&2, String>>, cl: Bool) -> Maybe<&2, Rb>:
1064	  match cl:
1065	    case True{}:
1066	      None{}
1067	    case False{}:
1068	      Some{Bool.pick(Rb, String.eq(String.to_lower(header.last(h, "transfer-encoding")), "chunked"), RbChunk{dc.start()}, RbClose{})}
1069	
1070	def rb.len(+h: Map<&2, List<&2, String>>, te: Bool) -> Maybe<&2, Rb>:
1071	  match te:
1072	    case True{}:
1073	      rb.te(h, has_header(h, "content-length"))
1074	    case False{}:
1075	      Bool.pick(Maybe<&2, Rb>, has_header(h, "content-length"), rb.cl(parse_u32(header(h, "content-length"))), Some{RbClose{}})
1076	
1077	# RFC 9112 §6.3: how the body of this response ends. None: it cannot be framed.
1078	def rb.of(+h: Map<&2, List<&2, String>>, nobody: Bool) -> Maybe<&2, Rb>:
1079	  match nobody:
1080	    case True{}:
1081	      Some{RbDone{}}
1082	    case False{}:
1083	      rb.len(h, has_header(h, "transfer-encoding"))
1084	
1085	# rb: how the body goes on. parts: body bytes so far, newest first. rest: bytes past a Done body.
1086	type Bf is Type:
1087	  Bf{rb: Rb, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
1088	
1089	def rb.len.cut(parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Bf:
1090	  (piece, data) = r
1091	  Bf{RbDone{}, Con{data, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32)))}
1092	
1093	def rb.len.have(short: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Bf:
1094	  match short:
1095	    case True{}:
1096	      Bf{RbLen{(left - len : U32)}, Con{piece, parts}, Bytes.new(0)}
1097	    case False{}:
1098	      rb.len.cut(parts, len, left, Bytes.slice(piece, 0, left))
1099	
1100	def rb.chunk(c: Ck) -> Bf:
1101	  Ck{st, parts, rest} = c
1102	  match st:
1103	    case DcDone{}:
1104	      Bf{RbDone{}, parts, rest}
1105	    case DcBad{}:
1106	      Bf{RbBad{}, parts, rest}
1107	    case DcSize{a, b}:
1108	      Bf{RbChunk{DcSize{a, b}}, parts, rest}
1109	    case DcExt{x}:
1110	      Bf{RbChunk{DcExt{x}}, parts, rest}
1111	    case DcSizeLf{x}:
1112	      Bf{RbChunk{DcSizeLf{x}}, parts, rest}
1113	    case DcData{k}:
1114	      Bf{RbChunk{DcData{k}}, parts, rest}
1115	    case DcDataCr{}:
1116	      Bf{RbChunk{DcDataCr{}}, parts, rest}
1117	    case DcDataLf{}:
1118	      Bf{RbChunk{DcDataLf{}}, parts, rest}
1119	    case DcTr{j}:
1120	      Bf{RbChunk{DcTr{j}}, parts, rest}
1121	
1122	# The body bytes in piece, added to parts.
1123	def rb.feed(rb: Rb, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Bf:
1124	  match rb:
1125	    case RbLen{+left}:
1126	      Bytes.Bytes{+len, buf} = piece
1127	      rb.len.have(U32.is_lt(len, left), left, parts, len, Bytes.Bytes{len, buf})
1128	    case RbChunk{st}:
1129	      rb.chunk(ck(piece, st, parts))
1130	    case RbClose{}:
1131	      Bf{RbClose{}, Con{piece, parts}, Bytes.new(0)}
1132	    case RbDone{}:
1133	      Bf{RbDone{}, parts, piece}
1134	    case RbBad{}:
1135	      Bf{RbBad{}, parts, piece}
1136	
1137	# RFC 9112 §8: only a close-delimited body may end at close.
1138	def rb.eof(rb: Rb) -> Bool:
1139	  match rb:
1140	    case RbClose{}:
1141	      True{}
1142	    case RbDone{}:
1143	      True{}
1144	    case RbLen{n}:
1145	      False{}
1146	    case RbChunk{st}:
1147	      False{}
1148	    case RbBad{}:
1149	      False{}
1150	
1151	def rb.body(parts: List<&1, Bytes.Bytes>) -> Bytes.Bytes:
1152	  Bytes.concat(List.reverse(&1, Bytes.Bytes, parts))
1153	
1154	# The head scan. Seek: look for the blank line from byte from; k interim heads are behind.
1155	# Wait: no blank line yet. Res: the final head, how its body ends, and the bytes after it.
1156	type Hs is Type:
1157	  HsSeek{buf: Bytes.Bytes, from: U32, k: U32}
1158	  HsWait{buf: Bytes.Bytes, k: U32}
1159	  HsBad{}
1160	  HsRes{res: Res, rb: Rb, rest: Bytes.Bytes}
1161	
1162	def hs.final(+status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes, m: Maybe<&2, Rb>) -> Hs:
1163	  match m:
1164	    case None{}:
1165	      HsBad{}
1166	    case Some{rb}:
1167	      HsRes{Res{status, h, Bytes.new(0)}, rb, rest}
1168	
1169	def hs.skip(more: Bool, +k: U32, rest: Bytes.Bytes) -> Hs:
1170	  match more:
1171	    case True{}:
1172	      HsSeek{rest, 0, (k + 1 : U32)}
1173	    case False{}:
1174	      HsBad{}
1175	
1176	def hs.pick(interim: Bool, +head: Bool, +k: U32, +status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes) -> Hs:
1177	  match interim:
1178	    case True{}:
1179	      hs.skip(U32.is_lt(k, 8), k, rest)
1180	    case False{}:
1181	      hs.final(status, h, rest, rb.of(h, frame.nobody(status, head)))
1182	
1183	def hs.res(+head: Bool, +k: U32, rest: Bytes.Bytes, res: Res) -> Hs:
1184	  Res{+status, +h, body} = res
1185	  hs.pick(frame.interim(status), head, k, status, h, rest)
1186	
1187	# The head alone, framed as a HEAD response so it stops at the blank line.
1188	def hs.parsed(+head: Bool, +k: U32, rest: Bytes.Bytes, f: Frame) -> Hs:
1189	  match f:
1190	    case FrameDone{res}:
1191	      hs.res(head, k, rest, res)
1192	    case FrameBad{}:
1193	      HsBad{}
1194	    case FrameMore{}:
1195	      HsBad{}
1196	
1197	def hs.split(+head: Bool, +k: U32, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1198	  (buf, hb) = r
1199	  hs.parsed(head, k, bytes.snd(Bytes.slice(buf, hlen, (len - hlen : U32))), parse.res.of(split_at_blank(Bytes.to_string(hb)), False{}, True{}))
1200	
1201	def hs.hit(+head: Bool, +k: U32, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Hs:
1202	  match at:
1203	    case None{}:
1204	      HsWait{buf, k}
1205	    case Some{+i}:
1206	      +hlen = (i + 4 : U32)
1207	      hs.split(head, k, hlen, len, Bytes.slice(buf, 0, hlen))
1208	
1209	def hs.seek.of(+head: Bool, +k: U32, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Hs:
1210	  (tail, m) = r
1211	  hs.hit(head, k, len, buf, found.at(from, m))
1212	
1213	def hs.seek(+head: Bool, +k: U32, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1214	  (buf, tail) = r
1215	  hs.seek.of(head, k, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
1216	
1217	def hs.step(+head: Bool, st: Hs) -> Hs:
1218	  match st:
1219	    case HsSeek{buf, +from, +k}:
1220	      Bytes.Bytes{+len, b} = buf
1221	      hs.seek(head, k, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
1222	    case HsWait{buf, k}:
1223	      HsWait{buf, k}
1224	    case HsBad{}:
1225	      HsBad{}
1226	    case HsRes{res, rb, rest}:
1227	      HsRes{res, rb, rest}
1228	
1229	# Each step ends the scan or passes one interim head, and at most 8 interim heads pass.
1230	def hs.scan(fuel: Nat, +head: Bool, st: Hs) -> Hs:
1231	  match fuel:
1232	    case 0n:
1233	      match st:
1234	        case HsSeek{buf, from, k}:
1235	          HsBad{}
1236	        case HsWait{buf, k}:
1237	          HsWait{buf, k}
1238	        case HsBad{}:
1239	          HsBad{}
1240	        case HsRes{res, rb, rest}:
1241	          HsRes{res, rb, rest}
1242	    case 1n+f:
1243	      hs.scan(f, head, hs.step(head, st))
1244	
1245	# piece joins buf; only the new bytes, and the 3 before them, can finish the blank line.
1246	def hs.more(+head: Bool, +k: U32, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Hs:
1247	  Bytes.Bytes{+ol, ob} = buf
1248	  hs.scan(10n, head, HsSeek{Bytes.append(Bytes.Bytes{ol, ob}, piece), Bool.pick(U32, U32.is_lt(ol, 3), 0, (ol - 3 : U32)), k})
1249	
1250	# A response read in pieces. Head: the head is not whole yet. Body: it is, and parts is the body so far.
1251	type Rv is Type:
1252	  RvHead{buf: Bytes.Bytes, k: U32}
1253	  RvBody{res: Res, rb: Rb, parts: List<&1, Bytes.Bytes>}
1254	
1255	# More: read on. Done: the response, and the bytes after it when the body is self-delimited.
1256	type Rt is Type:
1257	  RtMore{rv: Rv}
1258	  RtBad{}
1259	  RtDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1260	
1261	def rv.start() -> Rv:
1262	  RvHead{Bytes.new(0), 0}
1263	
1264	def rv.done(res: Res, parts: List<&1, Bytes.Bytes>, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1265	  Res{status, headers, body} = res
1266	  RtDone{Res{status, headers, rb.body(parts)}, rest}
1267	
1268	def rv.fed(res: Res, bf: Bf) -> Rt:
1269	  Bf{rb, parts, rest} = bf
1270	  match rb:
1271	    case RbDone{}:
1272	      rv.done(res, parts, Some{rest})
1273	    case RbBad{}:
1274	      RtBad{}
1275	    case RbLen{n}:
1276	      RtMore{RvBody{res, RbLen{n}, parts}}
1277	    case RbChunk{st}:
1278	      RtMore{RvBody{res, RbChunk{st}, parts}}
1279	    case RbClose{}:
1280	      RtMore{RvBody{res, RbClose{}, parts}}
1281	
1282	def rv.head(hs: Hs) -> Rt:
1283	  match hs:
1284	    case HsWait{buf, k}:
1285	      RtMore{RvHead{buf, k}}
1286	    case HsBad{}:
1287	      RtBad{}
1288	    case HsSeek{buf, from, k}:
1289	      RtBad{}
1290	    case HsRes{res, rb, rest}:
1291	      rv.fed(res, rb.feed(rb, Nil{}, rest))
1292	
1293	def rv.eof(res: Res, parts: List<&1, Bytes.Bytes>, ok: Bool) -> Rt:
1294	  match ok:
1295	    case True{}:
1296	      rv.done(res, parts, None{})
1297	    case False{}:
1298	      RtBad{}
1299	
1300	# One read: piece, or the server closed (RFC 9112 §8: a message cut short is not a message).
1301	def rv.step(closed: Bool, +head: Bool, rv: Rv, piece: Bytes.Bytes) -> Rt:
1302	  match closed:
1303	    case True{}:
1304	      match rv:
1305	        case RvHead{buf, k}:
1306	          RtBad{}
1307	        case RvBody{res, rb, parts}:
1308	          rv.eof(res, parts, rb.eof(rb))
1309	    case False{}:
1310	      match rv:
1311	        case RvHead{buf, +k}:
1312	          rv.head(hs.more(head, k, buf, piece))
1313	        case RvBody{res, rb, parts}:
1314	          rv.fed(res, rb.feed(rb, parts, piece))
1315	
1316	def rv.end(closed: Bool, +head: Bool, t: Rt) -> Rt:
1317	  match closed:
1318	    case False{}:
1319	      t
1320	    case True{}:
1321	      match t:
1322	        case RtMore{rv}:
1323	          rv.step(True{}, head, rv, Bytes.new(0))
1324	        case RtBad{}:
1325	          RtBad{}
1326	        case RtDone{res, rest}:
1327	          RtDone{res, rest}
1328	
1329	def rv.go(xs: List<&2, String>, closed: Bool, +head: Bool, t: Rt) -> Rt:
1330	  match xs:
1331	    case Nil{}:
1332	      rv.end(closed, head, t)
1333	    case Con{+x, rest}:
1334	      match t:
1335	        case RtMore{rv}:
1336	          rv.go(rest, closed, head, rv.step(False{}, head, rv, Bytes.from_string(x)))
1337	        case RtBad{}:
1338	          RtBad{}
1339	        case RtDone{res, r}:
1340	          RtDone{res, r}
1341	
1342	def rt.frame(t: Rt) -> Frame:
1343	  match t:
1344	    case RtMore{rv}:
1345	      FrameMore{}
1346	    case RtBad{}:
1347	      FrameBad{}
1348	    case RtDone{res, rest}:
1349	      FrameDone{res}
1350	
1351	# What the read loop makes of these pieces, then a close when closed is set.
1352	def res.frame(xs: List<&2, String>, closed: Bool, +head: Bool) -> Frame:
1353	  rt.frame(rv.go(xs, closed, head, RtMore{rv.start()}))
1354	
1355	def rt.rest(t: Rt) -> Maybe<&1, Bytes.Bytes>:
1356	  match t:
1357	    case RtMore{rv}:
1358	      None{}
1359	    case RtBad{}:
1360	      None{}
1361	    case RtDone{res, rest}:
1362	      rest
1363	
1364	def after.of(m: Maybe<&1, Bytes.Bytes>) -> Maybe<&2, String>:
1365	  match m:
1366	    case None{}:
1367	      None{}
1368	    case Some{b}:
1369	      Some{Bytes.to_string(b)}
1370	
1371	# Bytes after a complete self-delimited message. None if it is not one yet.
1372	def after(+raw: String, +head: Bool) -> Maybe<&2, String>:
1373	  after.of(rt.rest(rv.go([raw], False{}, head, RtMore{rv.start()})))
1374	
1375	def req.v11.ver(mpv: String & String & String) -> Bool:
1376	  (+method, path, v) = mpv
1377	  String.eq(v, "HTTP/1.1")
1378	
1379	def req.v11.line(+line: String) -> Bool:
1380	  req.v11.ver(start_line(line))
1381	
1382	def req.v11.lines(xs: List<&2, String>) -> Bool:
1383	  match xs:
1384	    case Nil{}:
1385	      False{}
1386	    case Con{line, headers}:
1387	      req.v11.line(line)
1388	
1389	def req.v11.pick(+head: String, ok: Bool) -> Bool:
1390	  match ok:
1391	    case False{}:
1392	      False{}
1393	    case True{}:
1394	      req.v11.lines(String.lines(head))
1395	
1396	def req.v11.of(hb: String & String) -> Bool:
1397	  (+head, rest) = hb
1398	  req.v11.pick(head, String.ends_with(head, "\r\n\r\n"))
1399	
1400	def req.v11(+raw: String) -> Bool:
1401	  req.v11.of(split_at_blank(raw))
1402	
1403	def req.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1404	  String.eq(String.to_lower(header(headers, "connection")), "close")
1405	
1406	def res.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1407	  String.eq(String.to_lower(header(headers, "connection")), "close")
1408	
1409	def serve.fail_close(+status: U32) -> Bool:
1410	  Bool.or(U32.is_eq(status, 400), Bool.or(U32.is_eq(status, 413), U32.is_eq(status, 431)))
1411	
1412	def serve.keep.ok(fail: Bool, res_close: Bool) -> Bool:
1413	  match fail:
1414	    case True{}:
1415	      False{}
1416	    case False{}:
1417	      Bool.not(res_close)
1418	
1419	def serve.keep.v11(v11: Bool, +req_close: Bool, +status: U32, res_close: Bool) -> Bool:
1420	  match v11:
1421	    case False{}:
1422	      False{}
1423	    case True{}:
1424	      match req_close:
1425	        case True{}:
1426	          False{}
1427	        case False{}:
1428	          serve.keep.ok(serve.fail_close(status), res_close)
1429	
1430	def serve.keep(+headers: Map<&2, List<&2, String>>, v11: Bool, +status: U32, +res: Map<&2, List<&2, String>>) -> Bool:
1431	  serve.keep.v11(v11, req.conn_close(headers), status, res.conn_close(res))
1432	
1433	
1434	def again.keep(close: Bool, x: Bytes.Bytes) -> Maybe<&1, Bytes.Bytes>:
1435	  match close:
1436	    case True{}:
1437	      None{}
1438	    case False{}:
1439	      Some{x}
1440	
1441	def again.rest(close: Bool, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1442	  match rest:
1443	    case None{}:
1444	      None{}
1445	    case Some{x}:
1446	      again.keep(close, x)
1447	
1448	# The bytes past the response when the socket can take another request: the request did not
1449	# ask to close, the response is self-delimited, and the peer did not say close.
1450	def again(close: Bool, +h: Map<&2, List<&2, String>>, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1451	  match close:
1452	    case True{}:
1453	      None{}
1454	    case False{}:
1455	      again.rest(String.eq(String.to_lower(header(h, "connection")), "close"), rest)
1456	
1457	def res_body.res(res: Res) -> Bytes.Bytes:
1458	  Res{status, headers, body} = res
1459	  body
1460	
1461	def res_body(m: Maybe<&1, Res>) -> Bytes.Bytes:
1462	  match m:
1463	    case None{}:
1464	      Bytes.new(0)
1465	    case Some{res}:
1466	      res_body.res(res)
1467	
1468	def text(res: Res) -> String:
1469	  Enc.utf8.decode(res_body.res(res))
1470	
1471	def json(res: Res) -> Maybe<&2, Json.Val>:
1472	  Json.parse(text(res))
1473	
1474	def got_body.req(req: Req) -> Bytes.Bytes:
1475	  Req{method, path, headers, body} = req
1476	  body
1477	
1478	def got_body(m: Maybe<&1, Req>) -> Bytes.Bytes:
1479	  match m:
1480	    case None{}:
1481	      Bytes.new(0)
1482	    case Some{req}:
1483	      got_body.req(req)
1484	
1485	def body.of(hb: String & String) -> String:
1486	  (h, b) = hb
1487	  b
1488	
1489	def body(s: String) -> String:
1490	  body.of(split_at_blank.go(s, False{}, 0, SNil{}))
1491	
1492	def headers_lines(+k: String, vs: List<&2, String>, acc: String) -> String:
1493	  match vs:
1494	    case Nil{}:
1495	      acc
1496	    case Con{v, t}:
1497	      headers_lines(k, t, acc ++ ("\r\n" ++ sanitize(k) ++ ": " ++ sanitize(v)))
1498	
1499	def headers_block.go(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, acc: String) -> String:
1500	  match xs:
1501	    case Nil{}:
1502	      acc
1503	    case (k, vs) <> t:
1504	      headers_block.go(t, headers_lines(k, vs, acc))
1505	
1506	def headers_block(h: Map<&2, List<&2, String>>) -> String:
1507	  headers_block.go(Map.to_list(&2, List<&2, String>, h), "")
1508	
1509	# RFC 9110 §15. An unknown code gets an empty reason, which RFC 9112 §4 allows.
1510	type Reason is Data:
1511	  Reason{code: U32, text: String}
1512	
1513	def reasons() -> List<&2, Reason>:
1514	  [Reason{100, "Continue"}, Reason{101, "Switching Protocols"}, Reason{103, "Early Hints"},
1515	   Reason{200, "OK"}, Reason{201, "Created"}, Reason{202, "Accepted"}, Reason{203, "Non-Authoritative Information"}, Reason{204, "No Content"}, Reason{205, "Reset Content"}, Reason{206, "Partial Content"},
1516	   Reason{300, "Multiple Choices"}, Reason{301, "Moved Permanently"}, Reason{302, "Found"}, Reason{303, "See Other"}, Reason{304, "Not Modified"}, Reason{307, "Temporary Redirect"}, Reason{308, "Permanent Redirect"},
1517	   Reason{400, "Bad Request"}, Reason{401, "Unauthorized"}, Reason{402, "Payment Required"}, Reason{403, "Forbidden"}, Reason{404, "Not Found"}, Reason{405, "Method Not Allowed"}, Reason{406, "Not Acceptable"}, Reason{407, "Proxy Authentication Required"}, Reason{408, "Request Timeout"}, Reason{409, "Conflict"}, Reason{410, "Gone"}, Reason{411, "Length Required"}, Reason{412, "Precondition Failed"}, Reason{413, "Content Too Large"}, Reason{414, "URI Too Long"}, Reason{415, "Unsupported Media Type"}, Reason{416, "Range Not Satisfiable"}, Reason{417, "Expectation Failed"}, Reason{421, "Misdirected Request"}, Reason{422, "Unprocessable Content"}, Reason{426, "Upgrade Required"}, Reason{428, "Precondition Required"}, Reason{429, "Too Many Requests"}, Reason{431, "Request Header Fields Too Large"},
1518	   Reason{500, "Internal Server Error"}, Reason{501, "Not Implemented"}, Reason{502, "Bad Gateway"}, Reason{503, "Service Unavailable"}, Reason{504, "Gateway Timeout"}, Reason{505, "HTTP Version Not Supported"}]
1519	
1520	def reason.go(xs: List<&2, Reason>, +status: U32) -> String:
1521	  match xs:
1522	    case Nil{}:
1523	      ""
1524	    case Con{Reason{k, v}, t}:
1525	      Bool.pick(String, U32.is_eq(k, status), v, reason.go(t, status))
1526	
1527	def reason(+status: U32) -> String:
1528	  reason.go(reasons(), status)
1529	
1530	def response(+status: U32, headers: Map<&2, List<&2, String>>, body: String) -> String:
1531	  ("HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1532	
1533	def encode.body(head: Bool, top: Bytes.Bytes, body: Bytes.Bytes) -> Bytes.Bytes:
1534	  match head:
1535	    case True{}:
1536	      top
1537	    case False{}:
1538	      Bytes.append(top, body)
1539	
1540	def encode.len(+status: U32, headers: Map<&2, List<&2, String>>, head: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1541	  Bytes.Bytes{+len, buf} = body
1542	  encode.body(head, Bytes.from_string(response(status, set(headers, "content-length", U32.show(len)), "")), Bytes.Bytes{len, buf})
1543	
1544	# RFC 9110 §6.4.1, §8.6: 1xx, 204 and 304 have no body; HEAD gets the length but no body.
1545	def encode.pick(+status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, head: Bool, nobody: Bool) -> Bytes.Bytes:
1546	  match nobody:
1547	    case True{}:
1548	      Bytes.from_string(response(status, headers, ""))
1549	    case False{}:
1550	      encode.len(status, headers, head, body)
1551	
1552	def encode.on(r: Res, head: Bool) -> Bytes.Bytes:
1553	  Res{+status, headers, body} = r
1554	  encode.pick(status, headers, body, head, frame.nobody(status, False{}))
1555	
1556	def encode(r: Res) -> Bytes.Bytes:
1557	  encode.on(r, False{})
1558	
1559	def request(method: String, path: String, headers: Map<&2, List<&2, String>>, body: String) -> String:
1560	  (method ++ " " ++ path ++ " HTTP/1.1" ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1561	
1562	def req.reserved(+k: String) -> Bool:
1563	  Bool.or(Bool.or(String.eq(k, "host"), String.eq(k, "connection")), Bool.or(String.eq(k, "content-length"), String.eq(k, "transfer-encoding")))
1564	
1565	def req.put.one(m: Map<&2, List<&2, String>>, +k: String, vs: List<&2, String>, skip: Bool) -> Map<&2, List<&2, String>>:
1566	  match skip:
1567	    case True{}:
1568	      m
1569	    case False{}:
1570	      Map.set(&2, List<&2, String>, m, k, vs)
1571	
1572	def req.put(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1573	  match xs:
1574	    case Nil{}:
1575	      m
1576	    case (k, vs) <> t:
1577	      +lk = String.to_lower(k)
1578	      req.put(t, req.put.one(m, lk, vs, req.reserved(lk)))
1579	
1580	# RFC 9110 §8.6: no Content-Length on a bodiless request whose method gives a body no meaning.
1581	def req.cl(+m: Map<&2, List<&2, String>>, +method: String, +len: U32) -> Map<&2, List<&2, String>>:
1582	  +bodied = Bool.or(Bool.not(U32.is_zero(len)), Bool.or(String.eq(method, "POST"), Bool.or(String.eq(method, "PUT"), String.eq(method, "PATCH"))))
1583	  Bool.pick(Map<&2, List<&2, String>>, bodied, set(m, "content-length", U32.show(len)), m)
1584	
1585	# Caller headers are lowercased so they cannot duplicate ours; host, connection,
1586	# content-length and transfer-encoding are always ours (no smuggling through them).
1587	def encode_req.word(close: Bool) -> String:
1588	  match close:
1589	    case True{}:
1590	      "close"
1591	    case False{}:
1592	      "keep-alive"
1593	
1594	def encode_req.on(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, close: Bool) -> Bytes.Bytes:
1595	  Bytes.Bytes{+len, buf} = body
1596	  +h = set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", host), "connection", encode_req.word(close))
1597	  Bytes.append(Bytes.from_string(request(method, target, req.cl(h, method, len), "")), Bytes.Bytes{len, buf})
1598	
1599	def encode_req(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Bytes.Bytes:
1600	  encode_req.on(method, target, host, headers, body, True{})
1601	
1602	# Redirects (RFC 9110 §15.4, as WHATWG fetch applies them)
1603	# --------------------------------------------------------
1604	
1605	# One request to make: headers are already lowercased (see req.put).
1606	type Hop is Type:
1607	  Hop{method: String, url: Url.Abs, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
1608	
1609	def redirect.code(+s: U32) -> Bool:
1610	  Bool.or(Bool.or(U32.is_eq(s, 301), U32.is_eq(s, 302)), Bool.or(U32.is_eq(s, 303), Bool.or(U32.is_eq(s, 307), U32.is_eq(s, 308))))
1611	
1612	def redirect.origin(a: Url.Abs) -> String:
1613	  Url.Abs{scheme, host, port, target} = a
1614	  scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1615	
1616	def redirect.del(ks: List<&2, String>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1617	  match ks:
1618	    case Nil{}:
1619	      m
1620	    case Con{k, t}:
1621	      redirect.del(t, Map.del(&2, List<&2, String>, m, k))
1622	
1623	def redirect.hdrs(+h: Map<&2, List<&2, String>>, drop: Bool, cross: Bool) -> Map<&2, List<&2, String>>:
1624	  +h2 = Bool.pick(Map<&2, List<&2, String>>, drop, redirect.del(["content-type", "content-encoding", "content-language", "content-location"], h), h)
1625	  Bool.pick(Map<&2, List<&2, String>>, cross, redirect.del(["authorization", "cookie", "proxy-authorization"], h2), h2)
1626	
1627	# 303 turns any method but HEAD into GET; 301 and 302 turn POST into GET;
1628	# 307 and 308 keep method and body. A GET carries no body or body headers.
1629	# Credentials do not follow a hop to another origin.
1630	def redirect.body(drop: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1631	  match drop:
1632	    case True{}:
1633	      Bytes.new(0)
1634	    case False{}:
1635	      body
1636	
1637	def redirect.to(+status: U32, +method: String, +from: Url.Abs, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, next: Maybe<&2, Url.Abs>) -> Maybe<&1, Hop>:
1638	  match next:
1639	    case None{}:
1640	      None{}
1641	    case Some{+to}:
1642	      +drop = Bool.or(Bool.and(U32.is_eq(status, 303), Bool.not(String.eq(method, "HEAD"))), Bool.and(Bool.or(U32.is_eq(status, 301), U32.is_eq(status, 302)), String.eq(method, "POST")))
1643	      Some{Hop{Bool.pick(String, drop, "GET", method), to, redirect.hdrs(headers, drop, Bool.not(String.eq(redirect.origin(from), redirect.origin(to)))), redirect.body(drop, body)}}
1644	
1645	def redirect.hop(status: U32, h: Hop, loc: String) -> Maybe<&1, Hop>:
1646	  Hop{method, +url, headers, body} = h
1647	  redirect.to(status, method, url, headers, body, Url.resolve(url, loc))
1648	
1649	def redirect.if(status: U32, h: Hop, loc: String, ok: Bool) -> Maybe<&1, Hop>:
1650	  match ok:
1651	    case False{}:
1652	      None{}
1653	    case True{}:
1654	      redirect.hop(status, h, loc)
1655	
1656	# The next request after a response, or None when it is not a redirect we follow.
1657	def redirect(+status: U32, +headers: Map<&2, List<&2, String>>, h: Hop) -> Maybe<&1, Hop>:
1658	  redirect.if(status, h, header(headers, "location"), Bool.and(redirect.code(status), has_header(headers, "location")))
1659	
1660	def io.recv.words(tls: Bool, s: Socket, max: U32, ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>):
1661	  match tls:
1662	    case True{}:
1663	      Wire.tls.recv.words(s, max, ms)
1664	    case False{}:
1665	      Wire.recv.words(s, max, ms)
1666	
1667	def io.send(tls: Bool, s: Socket, data: String) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1668	  match tls:
1669	    case True{}:
1670	      Wire.tls.send(s, data)
1671	    case False{}:
1672	      Wire.send(s, data)
1673	
1674	def io.send.words(tls: Bool, s: Socket, +len: U32, buf: Array<U32>) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1675	  match tls:
1676	    case True{}:
1677	      Wire.tls.send.words(s, len, buf)
1678	    case False{}:
1679	      Wire.send.words(s, len, buf)
1680	
1681	def io.send.bytes(tls: Bool, s: Socket, b: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1682	  Bytes.Bytes{+len, buf} = b
1683	  io.send.words(tls, s, len, buf)
1684	
1685	def io.close(tls: Bool, s: Socket) -> IO(Unit):
1686	  match tls:
1687	    case True{}:
1688	      Wire.tls.close(s)
1689	    case False{}:
1690	      Socket.close(s)
1691	
1692	def fetch.close(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
1693	  do IO<Result<&1, &1, Err, Res>>:
1694	    io.close(tls, s)
1695	    return r
1696	
1697	# Untrusted servers must not grow the buffer without bound.
1698	def fetch.max() -> Nat:
1699	  U32.to_nat(16777216)
1700	
1701	# none: no response byte arrived, so an idempotent request may be retried (RFC 9112 §9.3.1).
1702	# sock: the socket, when it can take another request.
1703	type Out is Type:
1704	  OutDone{res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes}
1705	  OutFail{e: Err, none: Bool}
1706	
1707	def fetch.boxed(r: Result<&1, &1, Err, Res>, none: Bool) -> Out:
1708	  match r:
1709	    case Done{res}:
1710	      OutDone{res, None{}, Bytes.new(0)}
1711	    case Fail{e}:
1712	      OutFail{e, none}
1713	
1714	def fetch.bad(tls: Bool, s: Socket, e: Maybe<&2, Err>) -> IO(Result<&1, &1, Err, Res>):
1715	  match e:
1716	    case None{}:
1717	      fetch.close(tls, s, Fail{ErrBad{}})
1718	    case Some{err}:
1719	      fetch.close(tls, s, Fail{err})
1720	
1721	def fetch.shut(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>, none: Bool) -> IO(Out):
1722	  do IO<Out>:
1723	    x : Result<&1, &1, Err, Res> <- fetch.close(tls, s, r)
1724	    return fetch.boxed(x, none)
1725	
1726	def fetch.hold.go(tls: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
1727	  match left:
1728	    case Some{x}:
1729	      IO.pure(Out, OutDone{res, Some{s}, x})
1730	    case None{}:
1731	      fetch.shut(tls, s, Done{res}, False{})
1732	
1733	def fetch.hold(tls: Bool, close: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
1734	  Res{status, +headers, body} = res
1735	  fetch.hold.go(tls, s, Res{status, headers, body}, again(close, headers, left))
1736	
1737	def fetch.failout(tls: Bool, s: Socket, e: Maybe<&2, Err>, none: Bool) -> IO(Out):
1738	  do IO<Out>:
1739	    r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, e)
1740	    return fetch.boxed(r, none)
1741	
1742	# Read state: the response so far and the bytes read, or how it ended.
1743	# none: no byte arrived, so an idempotent request may be retried.
1744	type Fl is Type:
1745	  FlMore{rv: Rv, n: U32}
1746	  FlBad{err: Maybe<&2, Err>, none: Bool}
1747	  FlDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1748	
1749	def fetch.rt(+n: U32, t: Rt) -> Fl:
1750	  match t:
1751	    case RtMore{rv}:
1752	      FlMore{rv, n}
1753	    case RtBad{}:
1754	      FlBad{None{}, U32.is_zero(n)}
1755	    case RtDone{res, rest}:
1756	      FlDone{res, rest}
1757	
1758	# 64 KiB of head past the body cap, as serve allows.
1759	def fetch.over(+n: U32) -> Bool:
1760	  Nat.is_lt(Nat.add(fetch.max(), 65536n), U32.to_nat(n))
1761	
1762	def fetch.piece.cap(over: Bool, +head: Bool, rv: Rv, +n2: U32, +len: U32, buf: Array<U32>) -> Fl:
1763	  match over:
1764	    case True{}:
1765	      FlBad{None{}, False{}}
1766	    case False{}:
1767	      fetch.rt(n2, rv.step(U32.is_zero(len), head, rv, Bytes.Bytes{len, buf}))
1768	
1769	def fetch.piece(+head: Bool, rv: Rv, +n: U32, p: U32 & Array<U32>) -> Fl:
1770	  (+len, buf) = p
1771	  +n2 = (n + len : U32)
1772	  fetch.piece.cap(fetch.over(n2), head, rv, n2, len, buf)
1773	
1774	def fetch.next(+head: Bool, rv: Rv, +n: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Fl:
1775	  (s, r) = m
1776	  match r:
1777	    case Fail{(+code, why)}:
1778	      (s, FlBad{Some{err.or_late(code, ErrRead{code, why})}, U32.is_zero(n)})
1779	    case Done{p}:
1780	      (s, fetch.piece(head, rv, n, p))
1781	
1782	# Reads until the response is whole or cannot be; an empty read means the server closed.
1783	@unsafe
1784	def fetch.loop(+close: Bool, +head: Bool, +tls: Bool, +ms: U32, st: Socket & Fl) -> IO(Out):
1785	  (s, fl) = st
1786	  match fl:
1787	    case FlMore{rv, +n}:
1788	      do IO<Out>:
1789	        m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
1790	        fetch.loop(close, head, tls, ms, fetch.next(head, rv, n, m))
1791	    case FlBad{err, none}:
1792	      fetch.failout(tls, s, err, none)
1793	    case FlDone{res, rest}:
1794	      fetch.hold(tls, close, s, res, rest)
1795	
1796	def exchange.sent(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Out):
1797	  (s, r) = m
1798	  match r:
1799	    case Fail{(+code, why)}:
1800	      fetch.shut(tls, s, Fail{err.or_late(code, ErrWrite{code, why})}, True{})
1801	    case Done{u}:
1802	      fetch.loop(close, head, tls, ms, (s, FlMore{rv.start(), 0}))
1803	
1804	def exchange.go(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, s: Socket, wire: Bytes.Bytes) -> IO(Out):
1805	  do IO<Out>:
1806	    sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
1807	    exchange.sent(tls, ms, close, head, sent)
1808	
1809	def exchange.tup(o: Out) -> Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes:
1810	  match o:
1811	    case OutFail{e, none}:
1812	      (None{}, Fail{e}, Bytes.new(0))
1813	    case OutDone{res, sock, rest}:
1814	      (sock, Done{res}, rest)
1815	
1816	# One request on an open socket. Some{socket}: it can take another request.
1817	def exchange(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, s: Socket, wire: Bytes.Bytes) -> IO(Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes):
1818	  do IO<Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes>:
1819	    o : Out <- exchange.go(tls, ms, close, head, s, wire)
1820	    return exchange.tup(o)
1821	
1822	# Connection pool: idle sockets by scheme, host, and port. fetch uses a fresh pool per call.
1823	type Conn is Type:
1824	  Conn{tls: Bool, s: Socket}
1825	
1826	type Pool is Type:
1827	  Pool{idle: Map<&1, Conn>}
1828	
1829	def pool.new() -> Pool:
1830	  Pool{Map.new(&1, Conn)}
1831	
1832	def pool.key(+scheme: String, +host: String, +port: U32) -> String:
1833	  scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1834	
1835	def pool.take.of(r: Map<&1, Conn> & Maybe<&1, Conn>) -> Pool & Maybe<&1, Conn>:
1836	  (m, c) = r
1837	  (Pool{m}, c)
1838	
1839	def pool.take(p: Pool, +key: String) -> Pool & Maybe<&1, Conn>:
1840	  Pool{idle} = p
1841	  pool.take.of(Map.pop(&1, Conn, idle, key))
1842	
1843	def conn.close(c: Conn) -> IO(Unit):
1844	  Conn{tls, s} = c
1845	  io.close(tls, s)
1846	
1847	def conn.drop(m: Maybe<&1, Conn>) -> IO(Unit):
1848	  match m:
1849	    case None{}:
1850	      IO.pure(Unit, Unit{})
1851	    case Some{c}:
1852	      conn.close(c)
1853	
1854	# ponytail: one idle socket per origin; a second one replaces the first.
1855	def pool.give.of(+key: String, c: Conn, r: Map<&1, Conn> & Maybe<&1, Conn>) -> IO(Pool):
1856	  (m, old) = r
1857	  do IO<Pool>:
1858	    conn.drop(old)
1859	    return Pool{Map.set(&1, Conn, m, key, c)}
1860	
1861	def pool.give(p: Pool, +key: String, c: Conn) -> IO(Pool):
1862	  Pool{idle} = p
1863	  pool.give.of(key, c, Map.pop(&1, Conn, idle, key))
1864	
1865	def pool.close.go(xs: List<&1, Conn>) -> IO(Unit):
1866	  match xs:
1867	    case Nil{}:
1868	      IO.pure(Unit, Unit{})
1869	    case Con{c, t}:
1870	      do IO<Unit>:
1871	        conn.close(c)
1872	        pool.close.go(t)
1873	
1874	def pool.close(p: Pool) -> IO(Unit):
1875	  Pool{idle} = p
1876	  pool.close.go(Map.values(&1, Conn, idle))
1877	
1878	# RFC 9110 §9.2.2
1879	def pool.idempotent(+method: String) -> Bool:
1880	  Bool.or(String.eq(method, "GET"), Bool.or(String.eq(method, "HEAD"), Bool.or(String.eq(method, "OPTIONS"), Bool.or(String.eq(method, "TRACE"), Bool.or(String.eq(method, "PUT"), String.eq(method, "DELETE"))))))
1881	
1882	def conn.tls(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
1883	  (s, r) = m
1884	  match r:
1885	    case Fail{(+code, why)}:
1886	      do IO<Result<&1, &1, Err, Conn>>:
1887	        Wire.tls.close(s)
1888	        return Fail{err.or_late(code, ErrTls{code, why})}
1889	    case Done{u}:
1890	      IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
1891	
1892	# A failed handshake is an error, never plaintext.
1893	def conn.secure(+ms: U32, sni: String, s: Socket, tls: Bool) -> IO(Result<&1, &1, Err, Conn>):
1894	  match tls:
1895	    case False{}:
1896	      IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{False{}, s}})
1897	    case True{}:
1898	      do IO<Result<&1, &1, Err, Conn>>:
1899	        hs : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.connect(s, sni, ms)
1900	        conn.tls(hs)
1901	
1902	def conn.made(+ms: U32, sni: String, tls: Bool, r: Result<&1, &1, U32 & String, Socket>) -> IO(Result<&1, &1, Err, Conn>):
1903	  match r:
1904	    case Fail{(+code, why)}:
1905	      IO.pure(Result<&1, &1, Err, Conn>, Fail{err.or_late(code, ErrConnect{code, why})})
1906	    case Done{s}:
1907	      conn.secure(ms, sni, s, tls)
1908	
1909	def conn.open(+tls: Bool, +ms: U32, sni: String, ip: String, port: U32) -> IO(Result<&1, &1, Err, Conn>):
1910	  do IO<Result<&1, &1, Err, Conn>>:
1911	    c : Result<&1, &1, U32 & String, Socket> <- Wire.connect(ip, port, ms)
1912	    conn.made(ms, sni, tls, c)
1913	
1914	def conn.ex(c: Conn, +ms: U32, +head: Bool, wire: Bytes.Bytes) -> IO(Out):
1915	  Conn{+tls, s} = c
1916	  exchange.go(tls, ms, False{}, head, s, wire)
1917	
1918	# A socket with bytes past the response is out of step with the server, so it is closed.
1919	def pool.keep.s(p: Pool, +key: String, +tls: Bool, res: Res, s: Socket, clean: Bool) -> IO(Pool & Result<&1, &1, Err, Res>):
1920	  match clean:
1921	    case True{}:
1922	      do IO<Pool & Result<&1, &1, Err, Res>>:
1923	        p2 : Pool <- pool.give(p, key, Conn{tls, s})
1924	        return (p2, Done{res})
1925	    case False{}:
1926	      do IO<Pool & Result<&1, &1, Err, Res>>:
1927	        io.close(tls, s)
1928	        return (p, Done{res})
1929	
1930	def pool.keep.m(p: Pool, +key: String, +tls: Bool, res: Res, +clean: Bool, sock: Maybe<&1, Socket>) -> IO(Pool & Result<&1, &1, Err, Res>):
1931	  match sock:
1932	    case None{}:
1933	      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Done{res}))
1934	    case Some{s}:
1935	      pool.keep.s(p, key, tls, res, s, clean)
1936	
1937	def pool.keep(p: Pool, +key: String, +tls: Bool, res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
1938	  Bytes.Bytes{+len, buf} = rest
1939	  pool.keep.m(p, key, tls, res, U32.is_zero(len), sock)
1940	
1941	def pool.after(p: Pool, +key: String, +tls: Bool, o: Out) -> IO(Pool & Result<&1, &1, Err, Res>):
1942	  match o:
1943	    case OutFail{e, none}:
1944	      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
1945	    case OutDone{res, sock, rest}:
1946	      pool.keep(p, key, tls, res, sock, rest)
1947	
1948	def pool.fresh.conn(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, wire: Bytes.Bytes, r: Result<&1, &1, Err, Conn>) -> IO(Pool & Result<&1, &1, Err, Res>):
1949	  match r:
1950	    case Fail{e}:
1951	      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
1952	    case Done{c}:
1953	      do IO<Pool & Result<&1, &1, Err, Res>>:
1954	        o : Out <- conn.ex(c, ms, head, wire)
1955	        pool.after(p, key, tls, o)
1956	
1957	def pool.fresh.ip(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +host: String, +port: U32, wire: Bytes.Bytes, ip: Maybe<&2, String>) -> IO(Pool & Result<&1, &1, Err, Res>):
1958	  match ip:
1959	    case None{}:
1960	      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrDns{}}))
1961	    case Some{addr}:
1962	      do IO<Pool & Result<&1, &1, Err, Res>>:
1963	        c : Result<&1, &1, Err, Conn> <- conn.open(tls, ms, host, addr, port)
1964	        pool.fresh.conn(p, key, tls, ms, head, wire, c)
1965	
1966	def pool.fresh(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +host: String, +port: U32, wire: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
1967	  do IO<Pool & Result<&1, &1, Err, Res>>:
1968	    ip : Maybe<&2, String> <- Dns.resolve(host)
1969	    pool.fresh.ip(p, key, tls, ms, head, host, port, wire, ip)
1970	
1971	# A reused socket the server already closed fails before any response byte.
1972	def pool.retry(+none: Bool, +idem: Bool) -> Bool:
1973	  Bool.and(none, idem)
1974	
1975	def pool.stale(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +host: String, +port: U32, wire: Bytes.Bytes, e: Err, again: Bool) -> IO(Pool & Result<&1, &1, Err, Res>):
1976	  match again:
1977	    case True{}:
1978	      pool.fresh(p, key, tls, ms, head, host, port, wire)
1979	    case False{}:
1980	      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
1981	
1982	def pool.reused(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +idem: Bool, +host: String, +port: U32, wire: Bytes.Bytes, o: Out) -> IO(Pool & Result<&1, &1, Err, Res>):
1983	  match o:
1984	    case OutFail{e, +none}:
1985	      pool.stale(p, key, tls, ms, head, host, port, wire, e, pool.retry(none, idem))
1986	    case OutDone{res, sock, rest}:
1987	      pool.keep(p, key, tls, res, sock, rest)
1988	
1989	# A spare copy of the request, for the retry after a stale socket.
1990	def pool.idle.reuse(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +idem: Bool, +host: String, +port: U32, c: Conn, r: Bytes.Bytes & Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
1991	  (wire, spare) = r
1992	  do IO<Pool & Result<&1, &1, Err, Res>>:
1993	    o : Out <- conn.ex(c, ms, head, wire)
1994	    pool.reused(p, key, tls, ms, head, idem, host, port, spare, o)
1995	
1996	def pool.idle(taken: Pool & Maybe<&1, Conn>, +key: String, +tls: Bool, +ms: U32, +head: Bool, +idem: Bool, +host: String, +port: U32, wire: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
1997	  (p, m) = taken
1998	  match m:
1999	    case None{}:
2000	      pool.fresh(p, key, tls, ms, head, host, port, wire)
Lines 1-2000 of 3023. More: https://jend.leeeet.dev/read.txt?path=bend-kit-http@0.15.0.3/http.bend&start_line=2001