1	# ezhttp/src/http: HTTP/1.1 message text for client and server — request and
2	# response formatting/parsing — with no sockets. Semantics follow RFC 9110;
3	# message syntax and framing follow RFC 9112. TLS is outside this module.
4	import Base
5	import ./body.bend as Body
6	
7	# a string divided at the first occurrence of a pattern, or not divided at all
8	type Cut is Data:
9	  NoCut{}
10	  Cut{before: String, after: String}
11	
12	# one header field name and value (RFC 9110 §5 / RFC 9112 §5)
13	type Header is Data:
14	  H{name: String, value: String}
15	
16	# what a response turned out to be: status, headers, framed body — or why not
17	type Reply is Data:
18	  Torn{why: String}
19	  Reply{status: U32, headers: List<&2, Header>, body: String}
20	
21	# the first of a list of pieces, "" when there are none
22	def first(ps: List<&2, String>) -> String:
23	  match ps:
24	    case []:
25	      ""
26	    case h <> t:
27	      h
28	
29	# the second of a list of pieces, "" when there is no second
30	def second(ps: List<&2, String>) -> String:
31	  match ps:
32	    case []:
33	      ""
34	    case h <> t:
35	      first(t)
36	
37	# one char of the divide, put back on the front of what the rest found
38	def divide.push(h: Char, r: Cut) -> Cut:
39	  match r:
40	    case NoCut{}:
41	      NoCut{}
42	    case Cut{before, after}:
43	      Cut{SCon{h, before}, after}
44	
45	# one step of the walk; rest is a thunk so Bool.pick does not force recursion
46	def divide.step(here: Bool, h: Char, t: String, n: Nat,
47	  rest: Unit -> Cut) -> Cut:
48	  match here:
49	    case True{}:
50	      Cut{"", String.drop(SCon{h, t}, n)}
51	    case False{}:
52	      divide.push(h, rest(Unit{}))
53	
54	# the walk: stop at the first hit
55	def divide.go(s: String, +pat: String, +n: Nat) -> Cut:
56	  match s:
57	    case SNil{}:
58	      NoCut{}
59	    case SCon{+h, +t}:
60	      divide.step(String.starts_with(SCon{h, t}, pat), h, t, n,
61	        _u => divide.go(t, pat, n))
62	
63	# a string in two halves around the first occurrence of a pattern
64	def divide(s: String, +pat: String) -> Cut:
65	  divide.go(s, pat, String.length(pat))
66	
67	# the value of one hex digit's code point, or 16 when it is not one
68	def hex.of(+u: U32) -> U32:
69	  Bool.pick(U32, Bool.and(U32.is_ge(u, 48), U32.is_le(u, 57)), U32.sub(u, 48),
70	    Bool.pick(U32, Bool.and(U32.is_ge(u, 97), U32.is_le(u, 102)), U32.sub(u, 87),
71	      Bool.pick(U32, Bool.and(U32.is_ge(u, 65), U32.is_le(u, 70)), U32.sub(u, 55),
72	        16)))
73	
74	# the value of one hex digit, or 16 when the char is not one
75	def hex.val(c: Char) -> U32:
76	  hex.of(Char.to_u32(c))
77	
78	# one step of the hex read
79	def hex.step(done: Bool, acc: Nat, rest: Unit -> Nat) -> Nat:
80	  match done:
81	    case True{}:
82	      acc
83	    case False{}:
84	      rest(Unit{})
85	
86	# the hex digits at the front of a string, read until one is not a digit
87	def hex.go(s: String, +acc: Nat) -> Nat:
88	  match s:
89	    case SNil{}:
90	      acc
91	    case SCon{+h, t}:
92	      +v = hex.val(h)
93	      hex.step(U32.is_ge(v, 16), acc,
94	        _u => hex.go(t, Nat.add(Nat.mul(acc, 16n), U32.to_nat(v))))
95	
96	# chunk-size from a chunk header (RFC 9112 §7.1); extensions after `;` ignored
97	def hexlen(s: String) -> Nat:
98	  hex.go(String.trim(first(String.split(s, ';'))), 0n)
99	
100	# whether a character is a hex digit
101	def hex.digit(c: Char) -> Bool:
102	  U32.is_lt(hex.val(c), 16)
103	
104	# the rest of a hex token once the first digit is known
105	def hex.rest(token: String, good: Bool) -> Bool:
106	  match token good:
107	    case _ False{}:
108	      False{}
109	    case SNil{} True{}:
110	      True{}
111	    case SCon{h, t} True{}:
112	      hex.rest(t, hex.digit(h))
113	
114	# a chunk-size token is one or more hex digits (RFC 9112 §7.1)
115	def hex.well(token: String) -> Bool:
116	  match token:
117	    case SNil{}:
118	      False{}
119	    case SCon{h, t}:
120	      hex.rest(t, hex.digit(h))
121	
122	# the chunk-size token, extensions after `;` removed
123	def chunks.token(before: String) -> String:
124	  String.trim(first(String.split(before, ';')))
125	
126	# bytes one code point takes in UTF-8. Content-Length counts octets
127	# (RFC 9110 §8.6); a Bend String counts code points.
128	def utf8.width(+u: U32) -> Nat:
129	  Bool.pick(Nat, U32.is_lt(u, 128), 1n,
130	    Bool.pick(Nat, U32.is_lt(u, 2048), 2n,
131	      Bool.pick(Nat, U32.is_lt(u, 65536), 3n, 4n)))
132	
133	# how many bytes of UTF-8 a string is
134	def utf8.len(s: String) -> Nat:
135	  match s:
136	    case SNil{}:
137	      0n
138	    case SCon{h, t}:
139	      Nat.add(utf8.width(Char.to_u32(h)), utf8.len(t))
140	
141	# one step of the take
142	def utf8.take.step(short: Bool, h: Char, rest: Unit -> String) -> String:
143	  match short:
144	    case True{}:
145	      SNil{}
146	    case False{}:
147	      SCon{h, rest(Unit{})}
148	
149	# the front of a string that is this many bytes of UTF-8
150	def utf8.take(s: String, +n: Nat) -> String:
151	  match s:
152	    case SNil{}:
153	      SNil{}
154	    case SCon{+h, t}:
155	      +w = utf8.width(Char.to_u32(h))
156	      utf8.take.step(Nat.is_lt(n, w), h, _u => utf8.take(t, Nat.sub(n, w)))
157	
158	# one step of the drop
159	def utf8.drop.step(short: Bool, h: Char, t: String,
160	  rest: Unit -> String) -> String:
161	  match short:
162	    case True{}:
163	      SCon{h, t}
164	    case False{}:
165	      rest(Unit{})
166	
167	# the rest of a string after this many bytes of UTF-8
168	def utf8.drop(s: String, +n: Nat) -> String:
169	  match s:
170	    case SNil{}:
171	      SNil{}
172	    case SCon{+h, +t}:
173	      +w = utf8.width(Char.to_u32(h))
174	      utf8.drop.step(Nat.is_lt(n, w), h, t, _u => utf8.drop(t, Nat.sub(n, w)))
175	
176	# a decimal digit's value, or 10 when the character is not a digit
177	def digits.val.of(+u: U32) -> U32:
178	  Bool.pick(U32, Bool.and(U32.is_ge(u, 48), U32.is_le(u, 57)), U32.sub(u, 48), 10)
179	
180	# a decimal digit's value, or 10 when the character is not a digit
181	def digits.val(c: Char) -> U32:
182	  digits.val.of(Char.to_u32(c))
183	
184	# accept one digit and keep reading, or stop when it is not a digit
185	def digits.step(ok: Bool, next: Unit -> Maybe<&2, Nat>) -> Maybe<&2, Nat>:
186	  match ok:
187	    case False{}:
188	      None{}
189	    case True{}:
190	      next(Unit{})
191	
192	# read a decimal token without building Base's Nat.read ceiling
193	def digits.go(s: String, +acc: Nat, left: Nat) -> Maybe<&2, Nat>:
194	  match s left:
195	    case _ 0n:
196	      None{}
197	    case SNil{} 1n+k:
198	      Some{acc}
199	    case SCon{+h, t} 1n+k:
200	      +d = digits.val(h)
201	      digits.step(U32.is_lt(d, 10),
202	        _u => digits.go(t, Nat.add(Nat.mul(acc, 10n), U32.to_nat(d)), k))
203	
204	# a short decimal (Content-Length, max-age). Empty is none. At most 9 digits.
205	def digits.read(s: String) -> Maybe<&2, Nat>:
206	  match s:
207	    case SNil{}:
208	      None{}
209	    case SCon{h, t}:
210	      digits.go(SCon{h, t}, 0n, 9n)
211	
212	# one step of the count: a character wider than what is still asked for
213	# means the string is longer
214	def utf8.has.step(short: Bool, rest: Unit -> Bool) -> Bool:
215	  match short:
216	    case True{}:
217	      True{}
218	    case False{}:
219	      rest(Unit{})
220	
221	# whether a string is at least this many bytes of UTF-8, walking no further
222	# than that many (utf8.len walks all of it)
223	def utf8.has(s: String, +n: Nat) -> Bool:
224	  match s:
225	    case SNil{}:
226	      Bool.not(Nat.is_lt(0n, n))
227	    case SCon{+h, t}:
228	      +w = utf8.width(Char.to_u32(h))
229	      utf8.has.step(Nat.is_lt(n, w), _u => utf8.has(t, Nat.sub(n, w)))
230	
231	# a non-zero chunk has its data and the following CRLF
232	def chunks.ready(+after: String, +n: Nat) -> Bool:
233	  Bool.and(utf8.has(after, Nat.add(n, 2n)),
234	    String.starts_with(utf8.drop(after, n), "\r\n"))
235	
236	# the next scan step, or why this chunk header is not usable
237	type Next is Data:
238	  Stop{}
239	  Go{cut: Cut}
240	  Reject{why: String}
241	
242	# one chunk header: reject non-hex sizes, stop on the 0 chunk, else continue
243	def chunks.next.of(zero: Bool, ready: Bool, +after: String, +n: Nat) -> Next:
244	  match zero ready:
245	    case True{} _:
246	      Stop{}
247	    case False{} False{}:
248	      Reject{"the chunked body stopped short"}
249	    case False{} True{}:
250	      Go{divide(utf8.drop(after, Nat.add(n, 2n)), "\r\n")}
251	
252	# hex check, then the length
253	def chunks.next.hex(+before: String, +after: String, ok: Bool) -> Next:
254	  match ok:
255	    case False{}:
256	      Reject{"chunk size is not hexadecimal"}
257	    case True{}:
258	      +n = hexlen(before)
259	      chunks.next.of(Nat.is_eq(n, 0n), chunks.ready(after, n), after, n)
260	
261	# classify one chunk header (RFC 9112 §7.1)
262	def chunks.next(+before: String, +after: String) -> Next:
263	  chunks.next.hex(before, after, hex.well(chunks.token(before)))
264	
265	# apply one scan step
266	def chunks.scan.step(step: Next, rest: Cut -> Maybe<&2, String>)
267	  -> Maybe<&2, String>:
268	  match step:
269	    case Stop{}:
270	      None{}
271	    case Reject{why}:
272	      Some{why}
273	    case Go{cut}:
274	      rest(cut)
275	
276	# None when every chunk size is hex and the 0 chunk is reached
277	def chunks.scan(fuel: Nat, c: Cut) -> Maybe<&2, String>:
278	  match fuel c:
279	    case 0n _:
280	      Some{"the chunked body is truncated"}
281	    case 1n+f NoCut{}:
282	      None{}
283	    case 1n+f Cut{before, +after}:
284	      chunks.scan.step(chunks.next(before, after), cut => chunks.scan(f, cut))
285	
286	# a zero chunk ends the body; anything after it is a trailer (RFC 9112 §7.1)
287	def chunks.more(+n: Nat, +after: String, rest: Unit -> String, zero: Bool)
288	  -> String:
289	  match zero:
290	    case True{}:
291	      ""
292	    case False{}:
293	      utf8.take(after, n)
294	        ++ rest(Unit{})
295	
296	# a chunked body put back together (RFC 9112 §7.1)
297	def chunks(fuel: Nat, c: Cut) -> String:
298	  match fuel c:
299	    case 0n _:
300	      ""
301	    case 1n+f NoCut{}:
302	      ""
303	    case 1n+f Cut{before, +after}:
304	      +n = hexlen(before)
305	      chunks.more(n, after,
306	        _u => chunks(f, divide(utf8.drop(after, Nat.add(n, 2n)), "\r\n")),
307	        Nat.is_eq(n, 0n))
308	
309	# a Transfer-Encoding: chunked body as the octets it stands for
310	def dechunk(+s: String) -> String:
311	  chunks(String.length(s), divide(s, "\r\n"))
312	
313	# whether a head line names this header (field names are case-insensitive:
314	# RFC 9110 §5.1)
315	def head.hit(h: String, +name: String) -> Bool:
316	  String.starts_with(String.to_lower(h), name ++ ":")
317	
318	# this line's value when it is the header asked for
319	def head.pick(hit: Bool, h: String, name: String, rest: String) -> String:
320	  match hit:
321	    case True{}:
322	      String.trim(String.drop(h, Nat.add(String.length(name), 1n)))
323	    case False{}:
324	      rest
325	
326	# the value a head gave a header, "" when it gave none
327	def head.go(ls: List<&2, String>, +name: String) -> String:
328	  match ls:
329	    case []:
330	      ""
331	    case +h <> t:
332	      head.pick(head.hit(h, name), h, name, head.go(t, name))
333	
334	# this line's trimmed field value
335	def head.value(h: String, name: String) -> String:
336	  String.trim(String.drop(h, Nat.add(String.length(name), 1n)))
337	
338	# cons a value when the line is the header asked for
339	def head.values.cons(hit: Bool, value: String, rest: Unit -> List<&2, String>)
340	  -> List<&2, String>:
341	  match hit:
342	    case False{}:
343	      rest(Unit{})
344	    case True{}:
345	      value <> rest(Unit{})
346	
347	# every value a head gave a header, in order (RFC 9112 §6.3 lists Content-Length)
348	def head.values(ls: List<&2, String>, +name: String) -> List<&2, String>:
349	  match ls:
350	    case []:
351	      []
352	    case +h <> t:
353	      head.values.cons(head.hit(h, name), head.value(h, name),
354	        _u => head.values(t, name))
355	
356	# a field value still holding a line break is obs-fold, which we refuse
357	def field.folded(+value: String) -> Bool:
358	  Bool.or(String.contains(value, "\n"), String.contains(value, "\r"))
359	
360	# a trimmed field value, or none when it still contains obs-fold
361	def field.keep(name: String, +value: String, folded: Bool) -> Maybe<&2, Header>:
362	  match folded:
363	    case True{}:
364	      None{}
365	    case False{}:
366	      Some{H{name, value}}
367	
368	# name and trimmed value from a cut at the first colon
369	def head.from_kept(before: String, +after: String) -> Maybe<&2, Header>:
370	  +value = String.trim(after)
371	  field.keep(before, value, field.folded(value))
372	
373	# one header line as a Header, or none when it has no colon
374	def head.from_cut(c: Cut) -> Maybe<&2, Header>:
375	  match c:
376	    case NoCut{}:
377	      None{}
378	    case Cut{before, after}:
379	      head.from_kept(before, after)
380	
381	# one header line as a Header, or none when it has no colon
382	def head.line(h: String) -> Maybe<&2, Header>:
383	  head.from_cut(divide(h, ":"))
384	
385	# prepend a parsed header when present
386	def head.cons(m: Maybe<&2, Header>, rest: List<&2, Header>) -> List<&2, Header>:
387	  match m:
388	    case None{}:
389	      rest
390	    case Some{hdr}:
391	      hdr <> rest
392	
393	# header lines after the status line as a list of fields
394	def head.list(ls: List<&2, String>) -> List<&2, Header>:
395	  match ls:
396	    case []:
397	      []
398	    case h <> t:
399	      head.cons(head.line(h), head.list(t))
400	
401	# one request header line
402	def header.line(h: Header) -> String:
403	  match h:
404	    case H{name, value}:
405	      name ++ ": " ++ value ++ "\r\n"
406	
407	# the value when this field is the one asked for
408	def headers.find.pick(value: String, hit: Bool, rest: Unit -> String) -> String:
409	  match hit:
410	    case True{}:
411	      value
412	    case False{}:
413	      rest(Unit{})
414	
415	# case-insensitive field lookup (RFC 9110 §5.1)
416	def headers.find.go(hs: List<&2, Header>, +name: String) -> String:
417	  match hs:
418	    case []:
419	      ""
420	    case H{n, v} <> t:
421	      headers.find.pick(v, String.eq(String.to_lower(n), name),
422	        _u => headers.find.go(t, name))
423	
424	# the value of a field, "" when it is absent
425	def headers.find(hs: List<&2, Header>, +name: String) -> String:
426	  headers.find.go(hs, String.to_lower(name))
427	
428	# extra headers rendered in order
429	def headers.lines(hs: List<&2, Header>) -> String:
430	  match hs:
431	    case []:
432	      ""
433	    case h <> t:
434	      header.line(h) ++ headers.lines(t)
435	
436	# the Content-Length field when the body is not empty (RFC 9110 §8.6)
437	def clen.field(+n: Nat, empty: Bool) -> List<&2, Header>:
438	  match empty:
439	    case True{}:
440	      []
441	    case False{}:
442	      [H{"Content-Length", Nat.show(n)}]
443	
444	# Content-Length line when the body is not empty (RFC 9110 §8.6)
445	def clen.line(+n: Nat, empty: Bool) -> String:
446	  headers.lines(clen.field(n, empty))
447	
448	# the fields a request names: the ones ezhttp writes a default for, the ones
449	# it always computes, and every other (SPEC.md HTTP-CLI-8)
450	type Field is Data:
451	  FHost{}
452	  FAgent{}
453	  FAccept{}
454	  FConn{}
455	  FClen{}
456	  FOther{}
457	
458	# a field's place in the order above
459	def field.rank(f: Field) -> U32:
460	  match f:
461	    case FHost{}:
462	      0
463	    case FAgent{}:
464	      1
465	    case FAccept{}:
466	      2
467	    case FConn{}:
468	      3
469	    case FClen{}:
470	      4
471	    case FOther{}:
472	      5
473	
474	# whether two fields are the same one
475	def field.same(a: Field, b: Field) -> Bool:
476	  U32.is_eq(field.rank(a), field.rank(b))
477	
478	# a lower-case name that is not content-length
479	def field.of.clen(hit: Bool) -> Field:
480	  match hit:
481	    case True{}:
482	      FClen{}
483	    case False{}:
484	      FOther{}
485	
486	# a lower-case name that is not connection
487	def field.of.conn(hit: Bool, +l: String) -> Field:
488	  match hit:
489	    case True{}:
490	      FConn{}
491	    case False{}:
492	      field.of.clen(String.eq(l, "content-length"))
493	
494	# a lower-case name that is not accept
495	def field.of.accept(hit: Bool, +l: String) -> Field:
496	  match hit:
497	    case True{}:
498	      FAccept{}
499	    case False{}:
500	      field.of.conn(String.eq(l, "connection"), l)
501	
502	# a lower-case name that is not user-agent
503	def field.of.agent(hit: Bool, +l: String) -> Field:
504	  match hit:
505	    case True{}:
506	      FAgent{}
507	    case False{}:
508	      field.of.accept(String.eq(l, "accept"), l)
509	
510	# a lower-case name that is not host
511	def field.of.host(hit: Bool, +l: String) -> Field:
512	  match hit:
513	    case True{}:
514	      FHost{}
515	    case False{}:
516	      field.of.agent(String.eq(l, "user-agent"), l)
517	
518	# the field a lower-case name names
519	def field.of(+l: String) -> Field:
520	  field.of.host(String.eq(l, "host"), l)
521	
522	# the field a name names, compared case-insensitively (RFC 9110 §5.1)
523	def field.name(name: String) -> Field:
524	  field.of(String.to_lower(name))
525	
526	# the field a header line names
527	def header.field(h: Header) -> Field:
528	  match h:
529	    case H{name, value}:
530	      field.name(name)
531	
532	# keep a header in front of the rest, or not
533	def fields.put(keep: Bool, h: Header, rest: List<&2, Header>)
534	  -> List<&2, Header>:
535	  match keep:
536	    case True{}:
537	      h <> rest
538	    case False{}:
539	      rest
540	
541	# the headers that name one field, in order
542	def fields.of(+f: Field, hs: List<&2, Header>) -> List<&2, Header>:
543	  match hs:
544	    case []:
545	      []
546	    case +h <> t:
547	      fields.put(field.same(f, header.field(h)), h, fields.of(f, t))
548	
549	# the caller's fields of a name, or the default when it gave none
550	def fields.or(given: List<&2, Header>, dflt: List<&2, Header>)
551	  -> List<&2, Header>:
552	  match given:
553	    case []:
554	      dflt
555	    case h <> t:
556	      h <> t
557	
558	# a request's header fields for a body of n octets: Host, User-Agent and
559	# Accept (the caller's, or the default), Connection: close, the caller's other
560	# fields, Content-Length.
561	# A caller's Connection or Content-Length is not sent: Connection: close lets
562	# the connection end frame the body when no Content-Length / chunked framing
563	# applies (RFC 9112 §9.6 / §6.3), and the body's length is computed.
564	def request.fields.n(host: String, +hs: List<&2, Header>, +n: Nat)
565	  -> List<&2, Header>:
566	  List.append(&2, Header, fields.or(fields.of(FHost{}, hs), [H{"Host", host}]),
567	    List.append(&2, Header,
568	      fields.or(fields.of(FAgent{}, hs), [H{"User-Agent", "ezhttp"}]),
569	      List.append(&2, Header,
570	        fields.or(fields.of(FAccept{}, hs), [H{"Accept", "*/*"}]),
571	        H{"Connection", "close"}
572	          <> List.append(&2, Header, fields.of(FOther{}, hs),
573	            clen.field(n, Nat.is_eq(n, 0n))))))
574	
575	# a request's header fields for a text body: the fields for its UTF-8 octets
576	def request.fields(host: String, +hs: List<&2, Header>, +body: String)
577	  -> List<&2, Header>:
578	  request.fields.n(host, hs, utf8.len(body))
579	
580	# a request-line and headers (RFC 9112 §3, §5). Absolute-path request-target
581	# (RFC 9112 §3.2.1); the fields are request.fields'.
582	def request(method: String, host: String, path: String,
583	  headers: List<&2, Header>, +body: String) -> String:
584	  method ++ " " ++ path ++ " HTTP/1.1\r\n"
585	    ++ headers.lines(request.fields(host, headers, body))
586	    ++ "\r\n"
587	    ++ body
588	
589	# the port a scheme implies: 443 for a secure one, 80 otherwise (RFC 9110
590	# §4.2.1, §4.2.2)
591	def port.dflt(secure: Bool) -> U32:
592	  match secure:
593	    case True{}:
594	      443
595	    case False{}:
596	      80
597	
598	# the Host field value once it is known whether the port is the default
599	def authority.of(host: String, +port: U32, dflt: Bool) -> String:
600	  match dflt:
601	    case True{}:
602	      host
603	    case False{}:
604	      host ++ ":" ++ U32.show(port)
605	
606	# the Host field value: the host, and the port after a colon unless it is the
607	# scheme's default (RFC 9110 §7.2)
608	def authority(secure: Bool, host: String, +port: U32) -> String:
609	  authority.of(host, port, U32.is_eq(port, port.dflt(secure)))
610	
611	# the request a client sends to host and port, over TLS when secure
612	def request.at(method: String, secure: Bool, host: String, port: U32,
613	  path: String, headers: List<&2, Header>, body: String) -> String:
614	  request(method, authority(secure, host, port), path, headers, body)
615	
616	# the request text for a body of n octets that is sent after it as its own
617	# octets: the request line, the fields for n octets, and the blank line
618	def request.head(method: String, host: String, path: String,
619	  headers: List<&2, Header>, +n: Nat) -> String:
620	  method ++ " " ++ path ++ " HTTP/1.1\r\n"
621	    ++ headers.lines(request.fields.n(host, headers, n))
622	    ++ "\r\n"
623	
624	# the request text a client sends to host and port ahead of n octets
625	def request.head.at(method: String, secure: Bool, host: String, port: U32,
626	  path: String, headers: List<&2, Header>, n: Nat) -> String:
627	  request.head(method, authority(secure, host, port), path, headers, n)
628	
629	# GET with optional headers
630	def get_req(host: String, path: String, headers: List<&2, Header>) -> String:
631	  request("GET", host, path, headers, "")
632	
633	# HEAD with optional headers (RFC 9110 §9.3.2): same as GET, no body
634	def head_req(host: String, path: String, headers: List<&2, Header>) -> String:
635	  request("HEAD", host, path, headers, "")
636	
637	# POST with body and optional headers
638	def post_req(host: String, path: String, headers: List<&2, Header>,
639	  body: Body.Body) -> String:
640	  request("POST", host, path, headers, Body.body.payload(body))
641	
642	# PUT with body and optional headers (RFC 9110 §9.3.4)
643	def put_req(host: String, path: String, headers: List<&2, Header>,
644	  body: Body.Body) -> String:
645	  request("PUT", host, path, headers, Body.body.payload(body))
646	
647	# DELETE with body and optional headers (RFC 9110 §9.3.5)
648	def delete_req(host: String, path: String, headers: List<&2, Header>,
649	  body: Body.Body) -> String:
650	  request("DELETE", host, path, headers, Body.body.payload(body))
651	
652	# OPTIONS with optional headers (RFC 9110 §9.3.7). No request body.
653	def options_req(host: String, path: String, headers: List<&2, Header>) -> String:
654	  request("OPTIONS", host, path, headers, "")
655	
656	# GET, HEAD, and OPTIONS are safe (RFC 9110 §9.2.1). Tokens are case-sensitive.
657	def method.safe(+method: String) -> Bool:
658	  Bool.or(String.eq(method, "GET"),
659	    Bool.or(String.eq(method, "HEAD"), String.eq(method, "OPTIONS")))
660	
661	# safe methods, plus PUT and DELETE, are idempotent (RFC 9110 §9.2.2)
662	def method.idempotent(+method: String) -> Bool:
663	  Bool.or(method.safe(method),
664	    Bool.or(String.eq(method, "PUT"), String.eq(method, "DELETE")))
665	
666	# the rest of a token once this character is known
667	def token.ok.step(space: Bool, rest: Unit -> Bool) -> Bool:
668	  match space:
669	    case True{}:
670	      False{}
671	    case False{}:
672	      rest(Unit{})
673	
674	# a bearer token has no whitespace (RFC 6750 §2.1)
675	def token.ok(s: String) -> Bool:
676	  match s:
677	    case SNil{}:
678	      True{}
679	    case SCon{h, t}:
680	      token.ok.step(Char.is_space(h), _u => token.ok(t))
681	
682	# origin-form request-target: absolute-path, optional query (RFC 9112 §3.2.1)
683	def target.origin(path: String) -> Bool:
684	  String.starts_with(path, "/")
685	
686	# asterisk-form is only `*` and only for OPTIONS (RFC 9112 §3.2.4)
687	def target.asterisk(method: String, star: Bool) -> Bool:
688	  match star:
689	    case False{}:
690	      False{}
691	    case True{}:
692	      String.eq(method, "OPTIONS")
693	
694	# origin-form, or OPTIONS asterisk-form
695	def target.form(method: String, path: String, absolute: Bool) -> Bool:
696	  match absolute:
697	    case True{}:
698	      True{}
699	    case False{}:
700	      target.asterisk(method, String.eq(path, "*"))
701	
702	# a body against the length its head promised
703	def parse.short(status: U32, headers: List<&2, Header>, n: Nat, body: String,
704	  short: Bool) -> Reply:
705	  match short:
706	    case True{}:
707	      Torn{"the response body stopped before its Content-Length"}
708	    case False{}:
709	      Reply{status, headers, utf8.take(body, n)}
710	
711	# a body framed by Content-Length (RFC 9110 §8.6 / RFC 9112 §6.3)
712	def parse.clen(status: U32, headers: List<&2, Header>, +n: Nat, +body: String)
713	  -> Reply:
714	  parse.short(status, headers, n, body, Nat.is_lt(utf8.len(body), n))
715	
716	# Content-Length when present; else the rest of the connection is the body
717	def parse.len(status: U32, headers: List<&2, Header>, m: Maybe<&2, Nat>,
718	  body: String) -> Reply:
719	  match m:
720	    case None{}:
721	      Reply{status, headers, body}
722	    case Some{n}:
723	      parse.clen(status, headers, n, body)
724	
725	# every Content-Length text equals the first
726	def clen.agree.step(same: Bool, rest: Unit -> Bool) -> Bool:
727	  match same:
728	    case False{}:
729	      False{}
730	    case True{}:
731	      rest(Unit{})
732	
733	# the tail of a Content-Length list against the first value
734	def clen.agree.go(rest: List<&2, String>, +h: String) -> Bool:
735	  match rest:
736	    case []:
737	      True{}
738	    case x <> r:
739	      clen.agree.step(String.eq(x, h), _u => clen.agree.go(r, h))
740	
741	# duplicate Content-Length fields must be the same digits (RFC 9112 §6.3)
742	def clen.agree(vs: List<&2, String>) -> Bool:
743	  match vs:
744	    case []:
745	      True{}
746	    case h <> t:
747	      clen.agree.go(t, h)
748	
749	# whether any Content-Length field was present
750	def clen.any(vs: List<&2, String>) -> Bool:
751	  match vs:
752	    case []:
753	      False{}
754	    case h <> t:
755	      True{}
756	
757	# a chunked body, or why the chunk framing was rejected
758	def parse.chunked(status: U32, headers: List<&2, Header>, body: String,
759	  bad: Maybe<&2, String>) -> Reply:
760	  match bad:
761	    case None{}:
762	      Reply{status, headers, dechunk(body)}
763	    case Some{why}:
764	      Torn{why}
765	
766	# scan chunk sizes, then decode when they are hex and closed by 0
767	def parse.chunks(status: U32, headers: List<&2, Header>, +body: String) -> Reply:
768	  parse.chunked(status, headers, body,
769	    chunks.scan(String.length(body), divide(body, "\r\n")))
770	
771	# Transfer-Encoding together with Content-Length is a bad message
772	def parse.te.clash(status: U32, headers: List<&2, Header>, body: String,
773	  present: Bool) -> Reply:
774	  match present:
775	    case True{}:
776	      Torn{"Content-Length and Transfer-Encoding conflict"}
777	    case False{}:
778	      parse.chunks(status, headers, body)
779	
780	# chunked framing, or Content-Length, or the rest of the connection
781	def parse.te(status: U32, headers: List<&2, Header>, +lens: List<&2, String>,
782	  +body: String, chunked: Bool) -> Reply:
783	  match chunked:
784	    case False{}:
785	      parse.len(status, headers, digits.read(first(lens)), body)
786	    case True{}:
787	      parse.te.clash(status, headers, body, clen.any(lens))
788	
789	# disagreeing Content-Length values are torn before framing
790	def parse.agree(status: U32, headers: List<&2, Header>, te: String,
791	  +lens: List<&2, String>, body: String, ok: Bool) -> Reply:
792	  match ok:
793	    case False{}:
794	      Torn{"Content-Length values disagree"}
795	    case True{}:
796	      parse.te(status, headers, lens, body,
797	        String.contains(String.to_lower(te), "chunked"))
798	
799	# the headers that decide the framing (RFC 9112 §6.3)
800	def parse.frame(status: U32, headers: List<&2, Header>, te: String,
801	  +lens: List<&2, String>, body: String) -> Reply:
802	  parse.agree(status, headers, te, lens, body, clen.agree(lens))
803	
804	# a head whose status line has been read (RFC 9112 §4)
805	def parse.status(m: Maybe<&2, U32>, +ls: List<&2, String>, body: String)
806	  -> Reply:
807	  match m:
808	    case None{}:
809	      Torn{"the response has no status line"}
810	    case Some{n}:
811	      +hs = head.list(ls)
812	      parse.frame(n, hs, head.go(ls, "transfer-encoding"),
813	        head.values(ls, "content-length"), body)
814	
815	# the status code a head's first line names, if it names one (RFC 9112 §4)
816	def status.of(ls: List<&2, String>) -> Maybe<&2, U32>:
817	  U32.read(second(String.split(first(ls), ' ')))
818	
819	# the head's lines, with the status line read off the first
820	def parse.head(+ls: List<&2, String>, body: String) -> Reply:
821	  parse.status(status.of(ls), ls, body)
822	
823	# a response divided into its head and everything after the blank line
824	# (RFC 9112 §2.1: header section ends at empty line)
825	def parse.cut(c: Cut) -> Reply:
826	  match c:
827	    case NoCut{}:
828	      Torn{"the response head has no blank line after it"}
829	    case Cut{before, after}:
830	      parse.head(String.lines(before), after)
831	
832	# the status, headers, and body of a raw response
833	def parse(raw: String) -> Reply:
834	  parse.cut(divide(raw, "\r\n\r\n"))
835	
836	# a parsed response on one line, for a test to read
837	def show(r: Reply) -> String:
838	  match r:
839	    case Torn{why}:
840	      "torn " ++ why
841	    case Reply{status, headers, body}:
842	      U32.show(status) ++ " " ++ body
843	
844	# --- inbound request (server) and outbound response (server) ---
845	
846	# a request that came apart, or the reason it would not (RFC 9112 §3)
847	type Request is Data:
848	  Bad{why: String}
849	  Request{method: String, target: String, headers: List<&2, Header>,
850	    body: String}
851	
852	# a status code and its reason-phrase
853	type Phrase is Data:
854	  P{code: U32, text: String}
855	
856	# the reason-phrases RFC 9110 §15 names (RFC 6585 §4 for 429)
857	def reasons() -> List<&2, Phrase>:
858	  [P{200, "OK"}, P{201, "Created"}, P{202, "Accepted"}, P{204, "No Content"},
859	    P{301, "Moved Permanently"}, P{302, "Found"}, P{303, "See Other"},
860	    P{304, "Not Modified"}, P{307, "Temporary Redirect"},
861	    P{308, "Permanent Redirect"}, P{400, "Bad Request"},
862	    P{401, "Unauthorized"}, P{403, "Forbidden"}, P{404, "Not Found"},
863	    P{405, "Method Not Allowed"}, P{409, "Conflict"}, P{410, "Gone"},
864	    P{413, "Content Too Large"}, P{415, "Unsupported Media Type"},
865	    P{422, "Unprocessable Content"}, P{429, "Too Many Requests"},
866	    P{500, "Internal Server Error"}, P{501, "Not Implemented"},
867	    P{502, "Bad Gateway"}, P{503, "Service Unavailable"},
868	    P{504, "Gateway Timeout"}]
869	
870	# this phrase when its code is the one asked for, else the rest's
871	def reason.pick(text: String, hit: Bool, rest: Unit -> String) -> String:
872	  match hit:
873	    case True{}:
874	      text
875	    case False{}:
876	      rest(Unit{})
877	
878	# the phrase a list gives a code, "" when it gives none
879	def reason.in(ps: List<&2, Phrase>, +code: U32) -> String:
880	  match ps:
881	    case []:
882	      ""
883	    case P{c, text} <> t:
884	      reason.pick(text, U32.is_eq(code, c), _u => reason.in(t, code))
885	
886	# the reason-phrase for a status code (RFC 9112 §4); "" for one not listed
887	def reason(+code: U32) -> String:
888	  reason.in(reasons(), code)
889	
890	# status-line + headers + body (RFC 9112 §4, §5). Connection: close ends the
891	# exchange after one response.
892	def respond(+status: U32, headers: List<&2, Header>, +body: String) -> String:
893	  +n = utf8.len(body)
894	  "HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ "\r\n"
895	    ++ "Connection: close\r\n"
896	    ++ headers.lines(headers)
897	    ++ clen.line(n, Nat.is_eq(n, 0n))
898	    ++ "\r\n"
899	    ++ body
900	
901	# 204 and 304 are terminated by the header section (RFC 9110 §15.3.5, §15.4.5)
902	def status.nocontent(+code: U32) -> Bool:
903	  Bool.or(U32.is_eq(code, 204), U32.is_eq(code, 304))
904	
905	# drop a 204/304 body; any other status keeps it
906	def respond.of.body(+status: U32, headers: List<&2, Header>, body: String,
907	  drop: Bool) -> String:
908	  match drop:
909	    case True{}:
910	      respond(status, headers, "")
911	    case False{}:
912	      respond(status, headers, body)
913	
914	# format a structured Reply as a response message
915	def respond.of(r: Reply) -> String:
916	  match r:
917	    case Torn{why}:
918	      respond(500, [], why)
919	    case Reply{+status, headers, body}:
920	      respond.of.body(status, headers, body, status.nocontent(status))
921	
922	# HEAD carries no message body; any other method keeps the body (RFC 9110 §9.3.2)
923	def reply.for.pick(reply: Reply, head: Bool) -> Reply:
924	  match reply head:
925	    case Torn{why} _:
926	      Torn{why}
927	    case Reply{status, headers, body} False{}:
928	      Reply{status, headers, body}
929	    case Reply{status, headers, body} True{}:
930	      Reply{status, headers, ""}
931	
932	# drop a HEAD response body before it is written
933	def reply.for(method: String, reply: Reply) -> Reply:
934	  reply.for.pick(reply, String.eq(method, "HEAD"))
935	
936	# the method token, or "" when the request did not parse
937	def method.of(req: Request) -> String:
938	  match req:
939	    case Bad{why}:
940	      ""
941	    case Request{method, target, headers, body}:
942	      method
943	
944	# request body against Content-Length
945	def ask.short(method: String, target: String, headers: List<&2, Header>,
946	  n: Nat, body: String, short: Bool) -> Request:
947	  match short:
948	    case True{}:
949	      Bad{"the request body stopped before its Content-Length"}
950	    case False{}:
951	      Request{method, target, headers, utf8.take(body, n)}
952	
953	# a request body framed by Content-Length (RFC 9110 §8.6 / RFC 9112 §6.3)
954	def ask.clen(method: String, target: String, headers: List<&2, Header>,
955	  +n: Nat, +body: String) -> Request:
956	  ask.short(method, target, headers, n, body, Nat.is_lt(utf8.len(body), n))
957	
958	# Content-Length when present; else the rest of the connection is the body
959	def ask.len(method: String, target: String, headers: List<&2, Header>,
960	  m: Maybe<&2, Nat>, body: String) -> Request:
961	  match m:
962	    case None{}:
963	      Request{method, target, headers, body}
964	    case Some{n}:
965	      ask.clen(method, target, headers, n, body)
966	
967	# a chunked request body, or why the chunk framing was rejected
968	def ask.chunked(method: String, target: String, headers: List<&2, Header>,
969	  body: String, bad: Maybe<&2, String>) -> Request:
970	  match bad:
971	    case None{}:
972	      Request{method, target, headers, dechunk(body)}
973	    case Some{why}:
974	      Bad{why}
975	
976	# scan chunk sizes, then decode when they are hex and closed by 0
977	def ask.chunks(method: String, target: String, headers: List<&2, Header>,
978	  +body: String) -> Request:
979	  ask.chunked(method, target, headers, body,
980	    chunks.scan(String.length(body), divide(body, "\r\n")))
981	
982	# Transfer-Encoding together with Content-Length is a bad request
983	def ask.te.clash(method: String, target: String, headers: List<&2, Header>,
984	  body: String, present: Bool) -> Request:
985	  match present:
986	    case True{}:
987	      Bad{"Content-Length and Transfer-Encoding conflict"}
988	    case False{}:
989	      ask.chunks(method, target, headers, body)
990	
991	# chunked framing, or Content-Length, or the rest of the connection
992	def ask.te(method: String, target: String, headers: List<&2, Header>,
993	  +lens: List<&2, String>, +body: String, chunked: Bool) -> Request:
994	  match chunked:
995	    case False{}:
996	      ask.len(method, target, headers, digits.read(first(lens)), body)
997	    case True{}:
998	      ask.te.clash(method, target, headers, body, clen.any(lens))
999	
1000	# disagreeing Content-Length values are bad before framing
1001	def ask.agree(method: String, target: String, headers: List<&2, Header>,
1002	  te: String, +lens: List<&2, String>, body: String, ok: Bool) -> Request:
1003	  match ok:
1004	    case False{}:
1005	      Bad{"Content-Length values disagree"}
1006	    case True{}:
1007	      ask.te(method, target, headers, lens, body,
1008	        String.contains(String.to_lower(te), "chunked"))
1009	
1010	# the headers that decide request framing (RFC 9112 §6.3)
1011	def ask.frame(method: String, target: String, headers: List<&2, Header>,
1012	  te: String, +lens: List<&2, String>, body: String) -> Request:
1013	  ask.agree(method, target, headers, te, lens, body, clen.agree(lens))
1014	
1015	# origin-form, or a bad request when the target is not an absolute-path
1016	def ask.origin(method: String, target: String, +ls: List<&2, String>,
1017	  body: String, ok: Bool) -> Request:
1018	  match ok:
1019	    case False{}:
1020	      Bad{"the request-target is not in origin-form"}
1021	    case True{}:
1022	      +hs = head.list(ls)
1023	      ask.frame(method, target, hs, head.go(ls, "transfer-encoding"),
1024	        head.values(ls, "content-length"), body)
1025	
1026	# request-line: method SP request-target SP HTTP-version (RFC 9112 §3)
1027	def ask.line(+method: String, +target: String, +ls: List<&2, String>,
1028	  body: String) -> Request:
1029	  ask.origin(method, target, ls, body,
1030	    target.form(method, target, target.origin(target)))
1031	
1032	# three fields of the request-line, or torn
1033	def ask.parts(ps: List<&2, String>, +ls: List<&2, String>, body: String)
1034	  -> Request:
1035	  match ps:
1036	    case []:
1037	      Bad{"the request has no request line"}
1038	    case m <> rest:
1039	      match rest:
1040	        case []:
1041	          Bad{"the request line has no target"}
1042	        case t <> _ver:
1043	          ask.line(m, t, ls, body)
1044	
1045	# the head's lines, with the request-line read off the first
1046	def ask.head(+ls: List<&2, String>, body: String) -> Request:
1047	  match ls:
1048	    case []:
1049	      Bad{"the request has no request line"}
1050	    case _:
1051	      ask.parts(String.split(first(ls), ' '), ls, body)
1052	
1053	# a request divided into its head and everything after the blank line
1054	def ask.cut(c: Cut) -> Request:
1055	  match c:
1056	    case NoCut{}:
1057	      Bad{"the request head has no blank line after it"}
1058	    case Cut{before, after}:
1059	      ask.head(String.lines(before), after)
1060	
1061	# the method, target, headers, and body of a raw request
1062	def ask(raw: String) -> Request:
1063	  ask.cut(divide(raw, "\r\n\r\n"))
1064	
1065	# a parsed request on one line, for a test to read
1066	def ask.show(r: Request) -> String:
1067	  match r:
1068	    case Bad{why}:
1069	      "bad " ++ why
1070	    case Request{method, target, headers, body}:
1071	      method ++ " " ++ target ++ " " ++ body
1072	
1073	# --- when a response has all arrived (RFC 9112 §6.3) ---
1074	
1075	# how a response's body is framed
1076	type Frame is Data:
1077	  Bare{}
1078	  Sized{n: Nat}
1079	  Chunked{}
1080	  Closed{}
1081	
1082	# 204 and 304 carry no body; a status line that did not parse is framed by
1083	# its headers
1084	def status.bare(m: Maybe<&2, U32>) -> Bool:
1085	  match m:
1086	    case None{}:
1087	      False{}
1088	    case Some{n}:
1089	      status.nocontent(n)
1090	
1091	# a 1xx status is an interim response (RFC 9110 §15.2); a status line that
1092	# did not parse is not
1093	def status.interim(m: Maybe<&2, U32>) -> Bool:
1094	  match m:
1095	    case None{}:
1096	      False{}
1097	    case Some{+n}:
1098	      Bool.and(U32.is_le(100, n), U32.is_lt(n, 200))
1099	
1100	# a Content-Length that reads as a number, or the close when none does
1101	def frame.sized(m: Maybe<&2, Nat>) -> Frame:
1102	  match m:
1103	    case None{}:
1104	      Closed{}
1105	    case Some{n}:
1106	      Sized{n}
1107	
1108	# Content-Length values that agree frame the body; any others leave the close
1109	def frame.agree(+lens: List<&2, String>, ok: Bool) -> Frame:
1110	  match ok:
1111	    case False{}:
1112	      Closed{}
1113	    case True{}:
1114	      frame.sized(digits.read(first(lens)))
1115	
1116	# chunked framing wins over Content-Length (RFC 9112 §6.3 item 4)
1117	def frame.te(+lens: List<&2, String>, chunked: Bool) -> Frame:
1118	  match chunked:
1119	    case True{}:
1120	      Chunked{}
1121	    case False{}:
1122	      frame.agree(lens, clen.agree(lens))
1123	
1124	# the framing of a response: none when bare (a reply to HEAD, a 204 or a 304),
1125	# else Transfer-Encoding chunked, else Content-Length, else the close
1126	def frame(bare: Bool, te: String, +lens: List<&2, String>) -> Frame:
1127	  match bare:
1128	    case True{}:
1129	      Bare{}
1130	    case False{}:
1131	      frame.te(lens, String.contains(String.to_lower(te), "chunked"))
1132	
1133	# a zero chunk's trailer section has ended: at once, or after its fields
1134	def chunks.trailer(+after: String) -> Bool:
1135	  Bool.or(String.starts_with(after, "\r\n"), String.contains(after, "\r\n\r\n"))
1136	
1137	# a chunk that has all arrived: on to the next chunk header, else not yet
1138	def chunks.ended.data(+after: String, +n: Nat, ready: Bool,
1139	  rest: Cut -> Bool) -> Bool:
1140	  match ready:
1141	    case False{}:
1142	      False{}
1143	    case True{}:
1144	      rest(divide(utf8.drop(after, Nat.add(n, 2n)), "\r\n"))
1145	
1146	# a chunk of size n: the last one when n is 0
1147	def chunks.ended.size(+after: String, +n: Nat, zero: Bool,
1148	  rest: Cut -> Bool) -> Bool:
1149	  match zero:
1150	    case True{}:
1151	      chunks.trailer(after)
1152	    case False{}:
1153	      chunks.ended.data(after, n, chunks.ready(after, n), rest)
1154	
1155	# a chunk header: a size that is not hex ends the read (the parse rejects it)
1156	def chunks.ended.hex(+before: String, +after: String, ok: Bool,
1157	  rest: Cut -> Bool) -> Bool:
1158	  match ok:
1159	    case False{}:
1160	      True{}
1161	    case True{}:
1162	      +n = hexlen(before)
1163	      chunks.ended.size(after, n, Nat.is_eq(n, 0n), rest)
1164	
1165	# a chunk header that has arrived, or not yet
1166	def chunks.ended.at(c: Cut, rest: Cut -> Bool) -> Bool:
1167	  match c:
1168	    case NoCut{}:
1169	      False{}
1170	    case Cut{+before, +after}:
1171	      chunks.ended.hex(before, after, hex.well(chunks.token(before)), rest)
1172	
1173	# whether a chunked body has reached the end of its last chunk
1174	def chunks.ended(fuel: Nat, c: Cut) -> Bool:
1175	  match fuel:
1176	    case 0n:
1177	      False{}
1178	    case 1n+f:
1179	      chunks.ended.at(c, cut => chunks.ended(f, cut))
1180	
1181	# whether a body has all arrived under its framing
1182	def whole.of(f: Frame, +body: String) -> Bool:
1183	  match f:
1184	    case Bare{}:
1185	      True{}
1186	    case Sized{n}:
1187	      Bool.not(Nat.is_lt(utf8.len(body), n))
1188	    case Chunked{}:
1189	      chunks.ended(String.length(body), divide(body, "\r\n"))
1190	    case Closed{}:
1191	      False{}
1192	
1193	# a head that is interim: whole when what follows is; else whole under the
1194	# framing it gives
1195	def whole.step(asked: Bool, +ls: List<&2, String>, +after: String,
1196	  interim: Bool, rest: Cut -> Bool) -> Bool:
1197	  match interim:
1198	    case True{}:
1199	      rest(divide(after, "\r\n\r\n"))
1200	    case False{}:
1201	      whole.of(frame(Bool.or(asked, status.bare(status.of(ls))),
1202	        head.go(ls, "transfer-encoding"), head.values(ls, "content-length")),
1203	        after)
1204	
1205	# a response whose head has ended, or not yet
1206	def whole.at(asked: Bool, c: Cut, rest: Cut -> Bool) -> Bool:
1207	  match c:
1208	    case NoCut{}:
1209	      False{}
1210	    case Cut{before, after}:
1211	      +ls = String.lines(before)
1212	      whole.step(asked, ls, after, status.interim(status.of(ls)), rest)
1213	
1214	# the heads in turn, at most `fuel` of them
1215	def whole.go(fuel: Nat, +asked: Bool, c: Cut) -> Bool:
1216	  match fuel:
1217	    case 0n:
1218	      False{}
1219	    case 1n+f:
1220	      whole.at(asked, c, cut => whole.go(f, asked, cut))
1221	
1222	# whether the text received so far is a whole response to a request with
1223	# this method (RFC 9112 §6.3), interim 1xx heads read past (RFC 9110 §15.2);
1224	# a response framed by the close never is
1225	def whole(+method: String, +raw: String) -> Bool:
1226	  whole.go(String.length(raw), String.eq(method, "HEAD"),
1227	    divide(raw, "\r\n\r\n"))
1228	
1229	# --- a response read by the request's method (RFC 9110 §15.2, §6.4.1) ---
1230	
1231	# a 1xx, 204 or 304 response has no body (RFC 9110 §6.4.1)
1232	def status.empty(+m: Maybe<&2, U32>) -> Bool:
1233	  Bool.or(status.interim(m), status.bare(m))
1234	
1235	# an interim head is skipped when more text follows it
1236	def interim.skip(m: Maybe<&2, U32>, after: String) -> Bool:
1237	  Bool.and(status.interim(m), Bool.not(String.is_empty(after)))
1238	
1239	# the final head with no body: its status and fields, an empty body
1240	def parse.to.bare(m: Maybe<&2, U32>, ls: List<&2, String>) -> Reply:
1241	  match m:
1242	    case None{}:
1243	      Torn{"the response has no status line"}
1244	    case Some{n}:
1245	      Reply{n, head.list(ls), ""}
1246	
1247	# the final head: with no body, or framed as parse frames it
1248	def parse.to.final(m: Maybe<&2, U32>, +ls: List<&2, String>, after: String,
1249	  bare: Bool) -> Reply:
1250	  match bare:
1251	    case True{}:
1252	      parse.to.bare(m, ls)
1253	    case False{}:
1254	      parse.status(m, ls, after)
1255	
1256	# an interim head is skipped, any other is the final one
1257	def parse.to.step(head: Bool, +ls: List<&2, String>, +m: Maybe<&2, U32>,
1258	  +after: String, skip: Bool, rest: Cut -> Reply) -> Reply:
1259	  match skip:
1260	    case True{}:
1261	      rest(divide(after, "\r\n\r\n"))
1262	    case False{}:
1263	      parse.to.final(m, ls, after, Bool.or(head, status.empty(m)))
1264	
1265	# a head that has ended, or the reason it has not
1266	def parse.to.at(head: Bool, c: Cut, rest: Cut -> Reply) -> Reply:
1267	  match c:
1268	    case NoCut{}:
1269	      Torn{"the response head has no blank line after it"}
1270	    case Cut{before, +after}:
1271	      +ls = String.lines(before)
1272	      +m = status.of(ls)
1273	      parse.to.step(head, ls, m, after, interim.skip(m, after), rest)
1274	
1275	# the heads in turn, at most `fuel` of them
1276	def parse.to.go(fuel: Nat, +head: Bool, c: Cut) -> Reply:
1277	  match fuel:
1278	    case 0n:
1279	      Torn{"the response head has no blank line after it"}
1280	    case 1n+f:
1281	      parse.to.at(head, c, cut => parse.to.go(f, head, cut))
1282	
1283	# the response to a request with this method (RFC 9112 §6.3): interim 1xx
1284	# heads skipped, and no body for HEAD or a 1xx, 204 or 304 final status
1285	def parse.to(+method: String, +raw: String) -> Reply:
1286	  parse.to.go(String.length(raw), String.eq(method, "HEAD"),
1287	    divide(raw, "\r\n\r\n"))
1288	
1289	# --- when a response has all arrived, judged read by read (SPEC.md HTTP-CLI-12) ---
1290	#
1291	# The client judges the text it has received after every read. Judging the
1292	# whole text each time (whole) costs the whole text each time; the state
1293	# below carries the judgement from one read to the next, so a read costs what
1294	# it brought (and the head, while no final head has ended). hear.more(
1295	# hear.of(method, a), b) is hear.of(method, a ++ b), and hear.done of it is
1296	# whole(method, a ++ b).
1297	
1298	# bytes of UTF-8 walked off the front of a string: all of it, with this many
1299	# still owed, or a stop at the first character that does not fit in what was
1300	# left, with what was left and the text from that character on
1301	type Skip is Data:
1302	  Short{owed: Nat}
1303	  Over{left: Nat, rest: String}
1304	
1305	# one step of the skip: a character wider than what is left stops it
1306	def utf8.skip.step(short: Bool, +n: Nat, h: Char, t: String,
1307	  rest: Unit -> Skip) -> Skip:
1308	  match short:
1309	    case True{}:
1310	      Over{n, SCon{h, t}}
1311	    case False{}:
1312	      rest(Unit{})
1313	
1314	# walk n bytes of UTF-8 off a string, as utf8.drop does, saying how it ended
1315	def utf8.skip(s: String, +n: Nat) -> Skip:
1316	  match s:
1317	    case SNil{}:
1318	      Short{n}
1319	    case SCon{+h, +t}:
1320	      +w = utf8.width(Char.to_u32(h))
1321	      utf8.skip.step(Nat.is_lt(n, w), n, h, t, _u => utf8.skip(t, Nat.sub(n, w)))
1322	
1323	# where a chunked body's walk stands: ended; waiting at a chunk header (or the
1324	# last chunk's trailer) that has not all arrived; inside a chunk's data with
1325	# octets still owed; or at the end of a chunk's data, at what should be its
1326	# CRLF. `fuel` is what chunks.ended would have left there.
1327	type Walk is Data:
1328	  Ended{}
1329	  Hold{fuel: Nat, rest: String}
1330	  Owed{fuel: Nat, owed: Nat}
1331	  Tail{fuel: Nat, left: Nat, rest: String}
1332	
1333	# a chunk's data skipped: whether its CRLF has arrived, and on to the next
1334	# chunk header when it has
1335	def walk.crlf(g: Nat, +left: Nat, +rest: String, ready: Bool,
1336	  go: String -> Walk) -> Walk:
1337	  match ready:
1338	    case True{}:
1339	      go(utf8.drop(rest, Nat.add(left, 2n)))
1340	    case False{}:
1341	      Tail{g, left, rest}
1342	
1343	# a chunk's data: all of what arrived, with octets still owed, or its end
1344	def walk.data(+g: Nat, s: Skip, go: String -> Walk) -> Walk:
1345	  match s:
1346	    case Short{owed}:
1347	      Owed{g, owed}
1348	    case Over{+left, +rest}:
1349	      walk.crlf(g, left, rest, Bool.and(utf8.has(rest, Nat.add(left, 2n)),
1350	        String.starts_with(rest, "\r\n")), go)
1351	
1352	# the last chunk: ended once its trailer section has
1353	def walk.trail(g: Nat, rest: String, ended: Bool) -> Walk:
1354	  match ended:
1355	    case True{}:
1356	      Ended{}
1357	    case False{}:
1358	      Hold{1n+g, rest}
1359	
1360	# a chunk of size n: the last one when n is 0
1361	def walk.size(+g: Nat, rest: String, +after: String, +n: Nat, zero: Bool,
1362	  go: String -> Walk) -> Walk:
1363	  match zero:
1364	    case True{}:
1365	      walk.trail(g, rest, chunks.trailer(after))
1366	    case False{}:
1367	      walk.data(g, utf8.skip(after, n), go)
1368	
1369	# a chunk header: a size that is not hex ends the walk (the parse rejects it)
1370	def walk.hex(+g: Nat, rest: String, +before: String, +after: String, ok: Bool,
1371	  go: String -> Walk) -> Walk:
1372	  match ok:
1373	    case False{}:
1374	      Ended{}
1375	    case True{}:
1376	      +n = hexlen(before)
1377	      walk.size(g, rest, after, n, Nat.is_eq(n, 0n), go)
1378	
1379	# a chunk header that has arrived, or not yet
1380	def walk.at(+g: Nat, rest: String, c: Cut, go: String -> Walk) -> Walk:
1381	  match c:
1382	    case NoCut{}:
1383	      Hold{1n+g, rest}
1384	    case Cut{+before, +after}:
1385	      walk.hex(g, rest, before, after, hex.well(chunks.token(before)), go)
1386	
1387	# the walk of chunks.ended from the chunk header at the front of a text
1388	def walk(fuel: Nat, +rest: String) -> Walk:
1389	  match fuel:
1390	    case 0n:
1391	      Hold{0n, rest}
1392	    case 1n+f:
1393	      +g = f
1394	      walk.at(g, rest, divide(rest, "\r\n"), s => walk(g, s))
1395	
1396	# whether the walk has ended
1397	def walk.done(w: Walk) -> Bool:
1398	  match w:
1399	    case Ended{}:
1400	      True{}
1401	    case Hold{fuel, rest}:
1402	      False{}
1403	    case Owed{fuel, owed}:
1404	      False{}
1405	    case Tail{fuel, left, rest}:
1406	      False{}
1407	
1408	# the walk once m more characters, b, have arrived
1409	def walk.more(w: Walk, +m: Nat, b: String) -> Walk:
1410	  match w:
1411	    case Ended{}:
1412	      Ended{}
1413	    case Hold{fuel, rest}:
1414	      walk(Nat.add(fuel, m), rest ++ b)
1415	    case Owed{g, owed}:
1416	      +f = Nat.add(g, m)
1417	      walk.data(f, utf8.skip(b, owed), s => walk(f, s))
1418	    case Tail{g, left, rest}:
1419	      +f = Nat.add(g, m)
1420	      walk.data(f, Over{left, rest ++ b}, s => walk(f, s))
1421	
1422	# where a response stands: no final head yet (with the text from the head
1423	# being read on, and the fuel whole.go would have there); no body, so whole;
1424	# framed by the close, so never whole; sized, with the octets that have
1425	# arrived; or chunked, with its walk
1426	type Hear is Data:
1427	  Heads{fuel: Nat, asked: Bool, raw: String}
1428	  Whole{}
1429	  Never{}
1430	  Count{n: Nat, have: Nat}
1431	  Walking{w: Walk}
1432	
1433	# a final head's body under its framing
1434	def hear.body(f: Frame, +after: String) -> Hear:
1435	  match f:
1436	    case Bare{}:
1437	      Whole{}
1438	    case Sized{n}:
1439	      Count{n, utf8.len(after)}
1440	    case Chunked{}:
1441	      Walking{walk(String.length(after), after)}
1442	    case Closed{}:
1443	      Never{}
1444	
1445	# an interim head: on to the next; a final one: its body
1446	def hear.step(asked: Bool, +ls: List<&2, String>, +after: String,
1447	  interim: Bool, go: String -> Hear) -> Hear:
1448	  match interim:
1449	    case True{}:
1450	      go(after)
1451	    case False{}:
1452	      hear.body(frame(Bool.or(asked, status.bare(status.of(ls))),
1453	        head.go(ls, "transfer-encoding"), head.values(ls, "content-length")),
1454	        after)
1455	
1456	# a head that has ended, or not yet
1457	def hear.at(+g: Nat, +asked: Bool, raw: String, c: Cut, go: String -> Hear)
1458	  -> Hear:
1459	  match c:
1460	    case NoCut{}:
1461	      Heads{1n+g, asked, raw}
1462	    case Cut{before, after}:
1463	      +ls = String.lines(before)
1464	      hear.step(asked, ls, after, status.interim(status.of(ls)), go)
1465	
1466	# the heads in turn, as whole.go reads them
1467	def hear.go(fuel: Nat, +asked: Bool, +raw: String) -> Hear:
1468	  match fuel:
1469	    case 0n:
1470	      Heads{0n, asked, raw}
1471	    case 1n+f:
1472	      +g = f
1473	      hear.at(g, asked, raw, divide(raw, "\r\n\r\n"), s => hear.go(g, asked, s))
1474	
1475	# where a response to a request with this method stands, read from the
1476	# whole text received so far
1477	def hear.of(+method: String, +raw: String) -> Hear:
1478	  hear.go(String.length(raw), String.eq(method, "HEAD"), raw)
1479	
1480	# whether the response has all arrived
1481	def hear.done(h: Hear) -> Bool:
1482	  match h:
1483	    case Heads{fuel, asked, raw}:
1484	      False{}
1485	    case Whole{}:
1486	      True{}
1487	    case Never{}:
1488	      False{}
1489	    case Count{n, have}:
1490	      Bool.not(Nat.is_lt(have, n))
1491	    case Walking{w}:
1492	      walk.done(w)
1493	
1494	# where a response stands once more text, b, has arrived
1495	def hear.more(h: Hear, +b: String) -> Hear:
1496	  match h:
1497	    case Heads{fuel, asked, raw}:
1498	      hear.go(Nat.add(fuel, String.length(b)), asked, raw ++ b)
1499	    case Whole{}:
1500	      Whole{}
1501	    case Never{}:
1502	      Never{}
1503	    case Count{n, have}:
1504	      Count{n, Nat.add(have, utf8.len(b))}
1505	    case Walking{w}:
1506	      Walking{walk.more(w, String.length(b), b)}