http.bend

bend-kit-http@0.20.1.0 · 4,238 lines · 0 definitions

1# HTTP/1.1 and HTTP/2 client, with an HTTP/1.1 server. Source: https://github.com/paymog/bend-kit/tree/main/http
2import Base
3# By hash: bend-kit-url@0.4.1.0, -encoding@0.3.0.0, -json@0.5.0.1, -bytes@0.3.0.0, -dns@0.4.0.1, -zlib@0.1.5.0.
4import bend-kit-wire@0.4.2.0/wire.bend as Wire
5import bend-kit-http2@0.1.2.0/http2.bend as H2
6import bend-kit-http2@0.1.2.0/hpack.bend as Hpack
7import bend-kit-bytes@0.3.1.0/bytes.bend as HBytes
8import bend-kit-time@0.1.0.0/time.bend as Time
9import bend-kit-int@0.2.0.0/int.bend as Int
10import bend-kit-url@0.4.1.0/url.bend as Url
11import bend-kit-encoding@0.3.0.0/encoding.bend as Enc
12import bend-kit-json@0.5.0.1/json.bend as Json
13import bend-kit-bytes@0.3.0.0/bytes.bend as Bytes
14import bend-kit-dns@0.4.0.1/dns.bend as Dns
15import bend-kit-zlib@0.1.5.0/zlib.bend as Zlib
16
17# HTTP/1.1 codec and client (RFC 9112) for http:// and https:// (OpenSSL 3 at run time).
18# parse: start-line → field lines → blank → body length (§6.3); chunked (§7.1).
19# Bodies are Bytes. The String parsers below are the spec: one Char per octet.
20# fetch reads until frame() says the response is whole. It returns Result, not Maybe.
21# Build with -o for big bodies: the `bend file.bend` runner overflows on ~30 KB strings; native binaries do not.
22#   import bend-kit-http@0.20.1.0/http.bend as Http
23
24type Req is Type:
25  Req{method: String, path: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
26
27type Res is Type:
28  Res{status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
29
30# The body type and its conversions, so a caller needs no bytes import.
31def Body() -> Type:
32  Bytes.Bytes
33
34# A byte string (one Char per octet) to a body, and back.
35def from_string(+s: String) -> Bytes.Bytes:
36  Bytes.from_string(s)
37
38def to_string(b: Bytes.Bytes) -> String:
39  Bytes.to_string(b)
40
41def length(b: Bytes.Bytes) -> Bytes.Bytes & U32:
42  Bytes.length(b)
43
44# Why fetch failed. Wire errors keep the errno and the text the effect already had.
45# ponytail: 60 and 110 are ETIMEDOUT on macOS and Linux. Windows is out of scope.
46type Err is Data:
47  ErrUrl{}
48  ErrDns{}
49  ErrConnect{code: U32, why: String}
50  ErrTls{code: U32, why: String}
51  ErrRead{code: U32, why: String}
52  ErrWrite{code: U32, why: String}
53  ErrTimeout{}
54  ErrRedirect{}
55  ErrBad{}
56
57def err.late(+code: U32) -> Bool:
58  Bool.or(U32.is_eq(code, 60), U32.is_eq(code, 110))
59
60def err.pick(e: Err, late: Bool) -> Err:
61  match late:
62    case True{}:
63      ErrTimeout{}
64    case False{}:
65      e
66
67def err.or_late(code: U32, e: Err) -> Err:
68  err.pick(e, err.late(code))
69
70type Fields is Data:
71  FieldsBad{}
72  FieldsOk{m: Map<&2, List<&2, String>>}
73
74# One list per field name, in arrival order. header() is the first value.
75# Set-Cookie is never joined. Encode writes one line per value.
76def empty() -> Map<&2, List<&2, String>>:
77  Map.new(&2, List<&2, String>)
78
79def fields.of(r: Map<&2, List<&2, String>> & List<&2, String>) -> List<&2, String>:
80  (h, xs) = r
81  xs
82
83def fields(+h: Map<&2, List<&2, String>>, k: String) -> List<&2, String>:
84  fields.of(Map.get(List<&2, String>, Nil{}, h, k))
85
86def header.first(xs: List<&2, String>) -> String:
87  match xs:
88    case Nil{}:
89      ""
90    case Con{v, t}:
91      v
92
93def header(+h: Map<&2, List<&2, String>>, k: String) -> String:
94  header.first(fields(h, k))
95
96def field.last(xs: List<&2, String>) -> String:
97  match xs:
98    case Nil{}:
99      ""
100    case Con{v, Nil{}}:
101      v
102    case Con{v, t}:
103      field.last(t)
104
105# Transfer-Encoding is a list; chunked, when present, is the last coding.
106def header.last(+h: Map<&2, List<&2, String>>, k: String) -> String:
107  field.last(fields(h, k))
108
109def snoc(xs: List<&2, String>, v: String) -> List<&2, String>:
110  match xs:
111    case Nil{}:
112      [v]
113    case Con{h, t}:
114      Con{h, snoc(t, v)}
115
116def set(m: Map<&2, List<&2, String>>, k: String, v: String) -> Map<&2, List<&2, String>>:
117  Map.set(&2, List<&2, String>, m, k, [v])
118
119def add(+m: Map<&2, List<&2, String>>, +k: String, v: String) -> Map<&2, List<&2, String>>:
120  Map.set(&2, List<&2, String>, m, k, snoc(fields(m, k), v))
121
122def sanitize.cons(ch: Char, rest: String, drop: Bool) -> String:
123  match drop:
124    case True{}:
125      rest
126    case False{}:
127      SCon{ch, rest}
128
129def sanitize(s: String) -> String:
130  match s:
131    case SNil{}:
132      SNil{}
133    case SCon{Chr{+c}, t}:
134      sanitize.cons(Chr{c}, sanitize(t), Bool.or(U32.is_eq(c, 13), U32.is_eq(c, 10)))
135
136def drop_cr.last.if(cr: Bool, c: U32) -> String:
137  match cr:
138    case True{}:
139      SNil{}
140    case False{}:
141      SCon{Chr{c}, SNil{}}
142
143def drop_cr.last(+c: U32) -> String:
144  drop_cr.last.if(U32.is_eq(c, 13), c)
145
146# prev is the char before s; it is kept unless it is a final CR.
147def drop_cr.go(s: String, prev: U32) -> String:
148  match s:
149    case SNil{}:
150      drop_cr.last(prev)
151    case SCon{Chr{c}, t}:
152      SCon{Chr{prev}, drop_cr.go(t, c)}
153
154def drop_cr(s: String) -> String:
155  match s:
156    case SNil{}:
157      SNil{}
158    case SCon{Chr{c}, t}:
159      drop_cr.go(t, c)
160
161# w holds the last four octets; a char past 255 clears it.
162def blank_end.go(s: String, w: U32) -> Bool:
163  match s:
164    case SNil{}:
165      U32.is_eq(w, 218762506)
166    case SCon{Chr{+c}, t}:
167      blank_end.go(t, Bool.pick(U32, U32.is_lt(c, 256), (w * 256 + c : U32), 0))
168
169# String.ends_with(s, "\r\n\r\n") in one pass, with no reversed copy.
170def blank_end(s: String) -> Bool:
171  blank_end.go(s, 0)
172
173def trim_end.cons(h: Char, r: String, space: Bool) -> String:
174  match r:
175    case SNil{}:
176      match space:
177        case True{}:
178          SNil{}
179        case False{}:
180          SCon{h, SNil{}}
181    case SCon{a, t}:
182      SCon{h, SCon{a, t}}
183
184# String.trim_end without the two reversed copies.
185def trim_end(s: String) -> String:
186  match s:
187    case SNil{}:
188      SNil{}
189    case SCon{+h, t}:
190      trim_end.cons(h, trim_end(t), Char.is_space(h))
191
192def trim(s: String) -> String:
193  trim_end(String.trim_start(s))
194
195# Bool.pick evaluates both arms; a split that recursed inside it would reverse acc at every byte.
196def take.cut(acc: String, rest: String) -> String & String:
197  (String.reverse(String.drop(acc, 1n)), rest)
198
199# hit: the last char pushed onto acc was the stop char.
200def take_sp.go(s: String, acc: String, hit: Bool) -> String & String:
201  match s:
202    case SNil{}:
203      match hit:
204        case True{}:
205          take.cut(acc, SNil{})
206        case False{}:
207          (String.reverse(acc), SNil{})
208    case SCon{Chr{+c}, t}:
209      match hit:
210        case True{}:
211          take.cut(acc, SCon{Chr{c}, t})
212        case False{}:
213          take_sp.go(t, SCon{Chr{c}, acc}, U32.is_eq(c, 32))
214
215def take_sp(s: String) -> String & String:
216  take_sp.go(s, SNil{}, False{})
217
218def start_line.ver(m: String, pv: String & String) -> String & String & String:
219  (p, v) = pv
220  (m, p, drop_cr(v))
221
222def start_line.rest(mr: String & String) -> String & String & String:
223  (m, r) = mr
224  start_line.ver(m, take_sp(r))
225
226def start_line(s: String) -> String & String & String:
227  start_line.rest(take_sp(s))
228
229def split_at_blank.go(s: String, e: Bool, w: U32, acc: String) -> String & String:
230  match s:
231    case SNil{}:
232      (String.reverse(acc), SNil{})
233    case SCon{Chr{+a}, t}:
234      match e:
235        case True{}:
236          (String.reverse(acc), SCon{Chr{a}, t})
237        case False{}:
238          +w2 = (w * 256 + a : U32)
239          split_at_blank.go(t, U32.is_eq(w2, 218762506), w2, SCon{Chr{a}, acc})
240
241# split_at_blank, plus whether the head ends in the blank line.
242def split_at_blank.flag.go(+raw: String, s: String, off: Nat, w: U32, e: Bool) -> String & String & Bool:
243  match s:
244    case SNil{}:
245      (String.take(raw, off), SNil{}, e)
246    case SCon{Chr{+a}, t}:
247      match e:
248        case True{}:
249          (String.take(raw, off), SCon{Chr{a}, t}, True{})
250        case False{}:
251          +w2 = (w * 256 + a : U32)
252          +off1 = (1n + off : Nat)
253          split_at_blank.flag.go(raw, t, off1, w2, U32.is_eq(w2, 218762506))
254
255def split_at_blank.pair(r: String & String & Bool) -> String & String:
256  (head, rest, whole) = r
257  (head, rest)
258
259def split_at_blank(+s: String) -> String & String:
260  split_at_blank.pair(split_at_blank.flag.go(s, s, 0n, 0, False{}))
261
262def split_colon.go(s: String, acc: String, hit: Bool) -> String & String:
263  match s:
264    case SNil{}:
265      match hit:
266        case True{}:
267          take.cut(acc, SNil{})
268        case False{}:
269          (String.reverse(acc), SNil{})
270    case SCon{Chr{+c}, t}:
271      match hit:
272        case True{}:
273          take.cut(acc, SCon{Chr{c}, t})
274        case False{}:
275          split_colon.go(t, SCon{Char.to_lower(Chr{c}), acc}, U32.is_eq(c, 58))
276
277def split_colon(+s: String) -> String & String:
278  split_colon.go(s, SNil{}, False{})
279
280def has_header.of(r: Map<&2, List<&2, String>> & Bool) -> Bool:
281  (h, b) = r
282  b
283
284def has_header(+h: Map<&2, List<&2, String>>, k: String) -> Bool:
285  has_header.of(Map.has(&2, List<&2, String>, h, k))
286
287def folded(+line: String) -> Bool:
288  Bool.or(String.starts_with(line, " "), String.starts_with(line, "\t"))
289
290def tracked(+k: String) -> Bool:
291  Bool.or(String.eq(k, "host"), String.eq(k, "content-length"))
292
293def fields_put.dup(m: Map<&2, List<&2, String>>, k: String, v: String, bad: Bool) -> Fields:
294  match bad:
295    case True{}:
296      FieldsBad{}
297    case False{}:
298      FieldsOk{add(m, k, v)}
299
300def fields_put.tracked(+m: Map<&2, List<&2, String>>, +k: String, v: String, t: Bool) -> Fields:
301  match t:
302    case True{}:
303      fields_put.dup(m, k, v, has_header(m, k))
304    case False{}:
305      FieldsOk{add(m, k, v)}
306
307def fields_put.key(+m: Map<&2, List<&2, String>>, +k: String, v: String) -> Fields:
308  fields_put.tracked(m, k, v, tracked(k))
309
310def fields_put.kv(m: Map<&2, List<&2, String>>, kv: String & String) -> Fields:
311  (k, v) = kv
312  fields_put.key(m, k, trim(v))
313
314def fields_put.fold(m: Map<&2, List<&2, String>>, line: String, fold: Bool) -> Fields:
315  match fold:
316    case True{}:
317      FieldsBad{}
318    case False{}:
319      fields_put.kv(m, split_colon(line))
320
321def fields_put.empty(m: Map<&2, List<&2, String>>, +line: String, e: Bool) -> Fields:
322  match e:
323    case True{}:
324      FieldsOk{m}
325    case False{}:
326      fields_put.fold(m, line, folded(line))
327
328def fields_put.ok(m: Map<&2, List<&2, String>>, +line: String) -> Fields:
329  fields_put.empty(m, line, String.is_empty(line))
330
331def fields_put(acc: Fields, line: String) -> Fields:
332  match acc:
333    case FieldsBad{}:
334      FieldsBad{}
335    case FieldsOk{m}:
336      fields_put.ok(m, line)
337
338def parse.headers.done(acc: Fields) -> Maybe<&2, Map<&2, List<&2, String>>>:
339  match acc:
340    case FieldsBad{}:
341      None{}
342    case FieldsOk{m}:
343      Some{m}
344
345def parse.headers(xs: List<&2, String>, acc: Fields) -> Maybe<&2, Map<&2, List<&2, String>>>:
346  match xs:
347    case Nil{}:
348      parse.headers.done(acc)
349    case Con{line, rest}:
350      parse.headers(rest, fields_put(acc, drop_cr(line)))
351
352def parse_u32.digit(+c: U32) -> Bool:
353  Bool.and(U32.is_le(48, c), U32.is_le(c, 57))
354
355def parse_u32.add(acc: U32, c: U32) -> U32:
356  (acc * 10 + (c - 48 : U32) : U32)
357
358def parse_u32.done(acc: U32, bad: Bool) -> Maybe<&2, U32>:
359  match bad:
360    case True{}:
361      None{}
362    case False{}:
363      Some{acc}
364
365def parse_u32.go(s: String, acc: U32, bad: Bool) -> Maybe<&2, U32>:
366  match s:
367    case SNil{}:
368      parse_u32.done(acc, bad)
369    case SCon{Chr{+c}, t}:
370      parse_u32.go(t, parse_u32.add(acc, c), Bool.or(bad, Bool.not(parse_u32.digit(c))))
371
372def parse_u32(s: String) -> Maybe<&2, U32>:
373  match s:
374    case SNil{}:
375      None{}
376    case SCon{Chr{+c}, t}:
377      parse_u32.go(t, parse_u32.add(0, c), Bool.not(parse_u32.digit(c)))
378
379# More: a valid prefix. Bad: cannot become a body. Body: a whole chunked body.
380type Hold is Data:
381  HoldMore{}
382  HoldBad{}
383  HoldBody{b: String}
384  HoldUntil{b: String}
385
386def is_hex(+c: U32) -> Bool:
387  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))))
388
389def hexv(+c: U32) -> U32:
390  Bool.pick(U32, parse_u32.digit(c), (c - 48 : U32), Bool.pick(U32, U32.is_le(c, 70), (c - 55 : U32), (c - 87 : U32)))
391
392# A chunked body decoder that reads each byte once, so a body fed in pieces
393# costs O(bytes) in total. Tr{j}: j bytes of the closing CRLF CRLF matched.
394type Dc is Data:
395  DcSize{acc: U32, seen: Bool}
396  DcExt{n: U32}
397  DcSizeLf{n: U32}
398  DcData{k: U32}
399  DcDataCr{}
400  DcDataLf{}
401  DcTr{j: U32}
402  DcDone{}
403  DcBad{}
404
405# st: where the decoder is. racc: the body so far, reversed. rest: bytes after a Done body.
406type Dco is Data:
407  Dco{st: Dc, racc: String, rest: String}
408
409def dc.start() -> Dc:
410  DcSize{0, False{}}
411
412def dc.size.semi(+n: U32, semi: Bool) -> Dc:
413  match semi:
414    case True{}:
415      DcExt{n}
416    case False{}:
417      DcBad{}
418
419def dc.size.cr(+n: U32, +c: U32, cr: Bool) -> Dc:
420  match cr:
421    case True{}:
422      DcSizeLf{n}
423    case False{}:
424      dc.size.semi(n, U32.is_eq(c, 59))
425
426def dc.size.end(+n: U32, +c: U32, seen: Bool) -> Dc:
427  match seen:
428    case False{}:
429      DcBad{}
430    case True{}:
431      dc.size.cr(n, c, U32.is_eq(c, 13))
432
433# A size that would overflow 32 bits ends the digits, and size.end then refuses it.
434def dc.size(+acc: U32, seen: Bool, +c: U32, digit: Bool) -> Dc:
435  match digit:
436    case True{}:
437      DcSize{(acc * 16 + hexv(c) : U32), True{}}
438    case False{}:
439      dc.size.end(acc, c, seen)
440
441# RFC 9112 §7.1.1: recipients ignore unknown chunk extensions; a bare LF is not CRLF.
442def dc.ext.lf(+n: U32, lf: Bool) -> Dc:
443  match lf:
444    case True{}:
445      DcBad{}
446    case False{}:
447      DcExt{n}
448
449def dc.ext(+n: U32, +c: U32, cr: Bool) -> Dc:
450  match cr:
451    case True{}:
452      DcSizeLf{n}
453    case False{}:
454      dc.ext.lf(n, U32.is_eq(c, 10))
455
456def dc.sized(+n: U32, zero: Bool) -> Dc:
457  match zero:
458    case True{}:
459      DcTr{2}
460    case False{}:
461      DcData{n}
462
463def dc.size.lf(+n: U32, lf: Bool) -> Dc:
464  match lf:
465    case True{}:
466      dc.sized(n, U32.is_eq(n, 0))
467    case False{}:
468      DcBad{}
469
470# k data bytes are left and m of them were just read.
471def dc.data(+k: U32, +m: U32) -> Dc:
472  Bool.pick(Dc, U32.is_le(k, m), DcDataCr{}, DcData{(k - m : U32)})
473
474def dc.pick(ok: Bool, next: Dc) -> Dc:
475  match ok:
476    case True{}:
477      next
478    case False{}:
479      DcBad{}
480
481# ponytail: trailer fields are dropped unparsed (§7.1.2 allows discarding)
482def dc.tr.hit(+j: U32) -> Dc:
483  Bool.pick(Dc, U32.is_eq(j, 3), DcDone{}, DcTr{(j + 1 : U32)})
484
485def dc.tr(+j: U32, +c: U32, hit: Bool) -> Dc:
486  match hit:
487    case True{}:
488      dc.tr.hit(j)
489    case False{}:
490      Bool.pick(Dc, U32.is_eq(c, 13), DcTr{1}, DcTr{0})
491
492def dc.tr.want(+j: U32) -> U32:
493  Bool.pick(U32, U32.is_eq(U32.mod(j, 2), 0), 13, 10)
494
495def dc.byte(h: Char) -> U32:
496  Chr{c} = h
497  c
498
499# One byte c. Done and Bad never look at it, and a data byte is not inspected.
500def dc.step(st: Dc, +c: U32) -> Dc:
501  match st:
502    case DcBad{}:
503      DcBad{}
504    case DcSize{+acc, seen}:
505      dc.size(acc, seen, c, Bool.and(is_hex(c), U32.is_le(acc, 268435455)))
506    case DcExt{+n}:
507      dc.ext(n, c, U32.is_eq(c, 13))
508    case DcSizeLf{+n}:
509      dc.size.lf(n, U32.is_eq(c, 10))
510    case DcDataCr{}:
511      dc.pick(U32.is_eq(c, 13), DcDataLf{})
512    case DcDataLf{}:
513      dc.pick(U32.is_eq(c, 10), dc.start())
514    case DcTr{+j}:
515      dc.tr(j, c, U32.is_eq(c, dc.tr.want(j)))
516    case DcData{+k}:
517      dc.data(k, 1)
518    case DcDone{}:
519      DcDone{}
520
521def dc.live(st: Dc) -> Bool:
522  match st:
523    case DcDone{}:
524      False{}
525    case DcBad{}:
526      False{}
527    case DcSize{a, b}:
528      True{}
529    case DcExt{n}:
530      True{}
531    case DcSizeLf{n}:
532      True{}
533    case DcData{k}:
534      True{}
535    case DcDataCr{}:
536      True{}
537    case DcDataLf{}:
538      True{}
539    case DcTr{j}:
540      True{}
541
542def dc.feed(s: String, st: Dc, racc: String) -> Dco:
543  match s:
544    case SNil{}:
545      Dco{st, racc, ""}
546    case SCon{h, t}:
547      match st:
548        case DcBad{}:
549          Dco{DcBad{}, racc, ""}
550        case DcDone{}:
551          Dco{DcDone{}, racc, SCon{h, t}}
552        case DcData{+k}:
553          dc.feed(t, dc.data(k, 1), SCon{h, racc})
554        case DcSize{+acc, seen}:
555          dc.feed(t, dc.step(DcSize{acc, seen}, dc.byte(h)), racc)
556        case DcExt{+n}:
557          dc.feed(t, dc.step(DcExt{n}, dc.byte(h)), racc)
558        case DcSizeLf{+n}:
559          dc.feed(t, dc.step(DcSizeLf{n}, dc.byte(h)), racc)
560        case DcDataCr{}:
561          dc.feed(t, dc.step(DcDataCr{}, dc.byte(h)), racc)
562        case DcDataLf{}:
563          dc.feed(t, dc.step(DcDataLf{}, dc.byte(h)), racc)
564        case DcTr{+j}:
565          dc.feed(t, dc.step(DcTr{j}, dc.byte(h)), racc)
566
567def chunk.hold(o: Dco) -> Hold:
568  Dco{st, racc, rest} = o
569  match st:
570    case DcDone{}:
571      HoldBody{String.reverse(racc)}
572    case DcBad{}:
573      HoldBad{}
574    case DcSize{a, b}:
575      HoldMore{}
576    case DcExt{n}:
577      HoldMore{}
578    case DcSizeLf{n}:
579      HoldMore{}
580    case DcData{k}:
581      HoldMore{}
582    case DcDataCr{}:
583      HoldMore{}
584    case DcDataLf{}:
585      HoldMore{}
586    case DcTr{j}:
587      HoldMore{}
588
589def chunk.live(s: String) -> Hold:
590  chunk.hold(dc.feed(s, dc.start(), ""))
591
592def chunk.rest(o: Dco) -> Maybe<&2, String>:
593  Dco{st, racc, rest} = o
594  match st:
595    case DcDone{}:
596      Some{rest}
597    case DcBad{}:
598      None{}
599    case DcSize{a, b}:
600      None{}
601    case DcExt{n}:
602      None{}
603    case DcSizeLf{n}:
604      None{}
605    case DcData{k}:
606      None{}
607    case DcDataCr{}:
608      None{}
609    case DcDataLf{}:
610      None{}
611    case DcTr{j}:
612      None{}
613
614def chunk.suffix(s: String) -> Maybe<&2, String>:
615  chunk.rest(dc.feed(s, dc.start(), ""))
616
617def chunk.decode.hold(h: Hold) -> Maybe<&2, String>:
618  match h:
619    case HoldMore{}:
620      None{}
621    case HoldBad{}:
622      None{}
623    case HoldUntil{b}:
624      None{}
625    case HoldBody{b}:
626      Some{b}
627
628def chunk.decode(s: String) -> Maybe<&2, String>:
629  chunk.decode.hold(chunk.live(s))
630
631def bytes.snd(r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes:
632  (a, b) = r
633  b
634
635def found.at(+from: U32, m: Maybe<&2, U32>) -> Maybe<&2, U32>:
636  match m:
637    case None{}:
638      None{}
639    case Some{+j}:
640      Some{(from + j : U32)}
641
642# A chunked body decoded from piece[i..]: a data run is sliced whole, and every other byte steps dc.
643type Cs is Type:
644  Cs{piece: Bytes.Bytes, i: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
645
646# st: where the decoder stopped. parts: the data so far, newest first. rest: the bytes after a Done body.
647type Ck is Type:
648  Ck{st: Dc, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
649
650def ck.next(+len: U32, +i: U32, +st: Dc, piece: Bytes.Bytes, parts: List<&1, Bytes.Bytes>) -> Bool & Cs:
651  (Bool.and(U32.is_lt(i, len), dc.live(st)), Cs{piece, i, st, parts})
652
653def ck.data(+len: U32, +i: U32, +k: U32, +m: U32, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Bool & Cs:
654  (piece, run) = r
655  ck.next(len, (i + m : U32), dc.data(k, m), piece, Con{run, parts})
656
657def ck.byte(+len: U32, +i: U32, st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Maybe<&2, U32>) -> Bool & Cs:
658  (piece, m) = r
659  match m:
660    case None{}:
661      ck.next(len, i, DcBad{}, piece, parts)
662    case Some{+c}:
663      ck.next(len, (i + 1 : U32), dc.step(st, c), piece, parts)
664
665def ck.step(+len: U32, cs: Cs) -> Bool & Cs:
666  Cs{piece, +i, st, parts} = cs
667  match st:
668    case DcData{+k}:
669      +m = U32.min(k, (len - i : U32))
670      ck.data(len, i, k, m, parts, Bytes.slice(piece, i, m))
671    case DcDone{}:
672      (False{}, Cs{piece, i, DcDone{}, parts})
673    case DcBad{}:
674      (False{}, Cs{piece, i, DcBad{}, parts})
675    case DcSize{+acc, seen}:
676      ck.byte(len, i, DcSize{acc, seen}, parts, Bytes.get(piece, i))
677    case DcExt{+n}:
678      ck.byte(len, i, DcExt{n}, parts, Bytes.get(piece, i))
679    case DcSizeLf{+n}:
680      ck.byte(len, i, DcSizeLf{n}, parts, Bytes.get(piece, i))
681    case DcDataCr{}:
682      ck.byte(len, i, DcDataCr{}, parts, Bytes.get(piece, i))
683    case DcDataLf{}:
684      ck.byte(len, i, DcDataLf{}, parts, Bytes.get(piece, i))
685    case DcTr{+j}:
686      ck.byte(len, i, DcTr{j}, parts, Bytes.get(piece, i))
687
688def ck.rest(st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Ck:
689  (piece, rest) = r
690  Ck{st, parts, rest}
691
692def ck.end(+len: U32, cs: Cs) -> Ck:
693  Cs{piece, +i, st, parts} = cs
694  ck.rest(st, parts, Bytes.slice(piece, i, (len - i : U32)))
695
696# Each step reads at least one byte, so len steps are enough.
697def ck.feed(f: Nat, +len: U32, r: Bool & Cs) -> Ck:
698  match f:
699    case 0n:
700      (go, cs) = r
701      ck.end(len, cs)
702    case 1n+p:
703      (go, cs) = r
704      match go:
705        case False{}:
706          ck.end(len, cs)
707        case True{}:
708          ck.feed(p, len, ck.step(len, cs))
709
710def ck(piece: Bytes.Bytes, +st: Dc, parts: List<&1, Bytes.Bytes>) -> Ck:
711  Bytes.Bytes{+len, buf} = piece
712  ck.feed(U32.to_nat(len), len, ck.next(len, 0, st, Bytes.Bytes{len, buf}, parts))
713
714def parse.res.cl.have(+rest: String, +k: Nat, short: Bool) -> Hold:
715  match short:
716    case True{}:
717      HoldMore{}
718    case False{}:
719      HoldBody{String.take(rest, k)}
720
721def parse.res.cl.k(+rest: String, +k: Nat) -> Hold:
722  parse.res.cl.have(rest, k, Nat.is_lt(String.length(rest), k))
723
724def parse.res.cl.n(rest: String, n: Maybe<&2, U32>) -> Hold:
725  match n:
726    case None{}:
727      HoldBad{}
728    case Some{k}:
729      parse.res.cl.k(rest, U32.to_nat(k))
730
731def parse.body.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
732  match hascl:
733    case False{}:
734      HoldBody{""}
735    case True{}:
736      parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
737
738# RFC 9112 §6.3 (4): a request coding other than chunked cannot be framed.
739def parse.body.chunked.eq(rest: String, ok: Bool) -> Hold:
740  match ok:
741    case False{}:
742      HoldBad{}
743    case True{}:
744      chunk.live(rest)
745
746def parse.body.chunked.val(te: String, rest: String) -> Hold:
747  parse.body.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
748
749def parse.body.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
750  match hascl:
751    case True{}:
752      HoldBad{}
753    case False{}:
754      parse.body.chunked.val(header.last(h, "transfer-encoding"), rest)
755
756def parse.body.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
757  match te:
758    case True{}:
759      parse.body.chunked(h, rest, has_header(h, "content-length"))
760    case False{}:
761      parse.body.cl(h, rest, has_header(h, "content-length"))
762
763def parse.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
764  parse.body.te(h, rest, has_header(h, "transfer-encoding"))
765
766# Bad: never a request. More: the head is not whole; read on. Head: the head is whole
767# and valid, and the body is still coming (req.body is empty). Req: a whole request.
768type Got is Type:
769  GotBad{}
770  GotMore{}
771  GotHead{req: Req}
772  GotReq{req: Req}
773
774def parse.finish(method: String, path: String, h: Map<&2, List<&2, String>>, body: Hold) -> Got:
775  match body:
776    case HoldBad{}:
777      GotBad{}
778    case HoldMore{}:
779      GotHead{Req{method, path, h, Bytes.new(0)}}
780    case HoldUntil{b}:
781      GotBad{}
782    case HoldBody{b}:
783      GotReq{Req{method, path, h, Bytes.from_string(b)}}
784
785def parse.host(method: String, path: String, +h: Map<&2, List<&2, String>>, rest: String, has: Bool) -> Got:
786  match has:
787    case False{}:
788      GotBad{}
789    case True{}:
790      parse.finish(method, path, h, parse.body(h, rest))
791
792# RFC 9112 §3.2: only HTTP/1.1 requires Host.
793def parse.fields(method: String, path: String, rest: String, v11: Bool, fs: Maybe<&2, Map<&2, List<&2, String>>>) -> Got:
794  match fs:
795    case None{}:
796      GotBad{}
797    case Some{+h}:
798      parse.host(method, path, h, rest, Bool.or(Bool.not(v11), has_header(h, "host")))
799
800def target_ok(+p: String) -> Bool:
801  Bool.or(String.starts_with(p, "/"), Bool.or(String.eq(p, "*"), String.starts_with(p, "http://")))
802
803def parse.target(method: String, +path: String, headers: List<&2, String>, rest: String, v11: Bool, ok: Bool) -> Got:
804  match ok:
805    case False{}:
806      GotBad{}
807    case True{}:
808      parse.fields(method, path, rest, v11, parse.headers(headers, FieldsOk{empty()}))
809
810def parse.ver(method: String, +path: String, +v: String, headers: List<&2, String>, rest: String, ok: Bool) -> Got:
811  match ok:
812    case False{}:
813      GotBad{}
814    case True{}:
815      parse.target(method, path, headers, rest, String.eq(v, "HTTP/1.1"), target_ok(path))
816
817def parse.empty_method(method: String, path: String, +v: String, headers: List<&2, String>, rest: String, empty: Bool) -> Got:
818  match empty:
819    case True{}:
820      GotBad{}
821    case False{}:
822      parse.ver(method, path, v, headers, rest, Bool.or(String.eq(v, "HTTP/1.1"), String.eq(v, "HTTP/1.0")))
823
824def parse.start3(mpv: String & String & String, headers: List<&2, String>, rest: String) -> Got:
825  (+method, path, v) = mpv
826  parse.empty_method(method, path, v, headers, rest, String.is_empty(method))
827
828def parse.lines(xs: List<&2, String>, rest: String) -> Got:
829  match xs:
830    case Nil{}:
831      GotBad{}
832    case Con{line, headers}:
833      parse.start3(start_line(line), headers, rest)
834
835
836def parse.head(+head: String, rest: String, whole: Bool) -> Got:
837  match whole:
838    case False{}:
839      GotMore{}
840    case True{}:
841      parse.lines(String.lines(head), rest)
842
843def parse.of(hb: String & String & Bool) -> Got:
844  (head, rest, whole) = hb
845  parse.head(head, rest, whole)
846
847# serve reads until this is not GotMore.
848def parse.got(+raw: String) -> Got:
849  parse.of(split_at_blank.flag.go(raw, raw, 0n, 0, False{}))
850
851
852def parse.req(g: Got) -> Maybe<&1, Req>:
853  match g:
854    case GotReq{req}:
855      Some{req}
856    case GotBad{}:
857      None{}
858    case GotMore{}:
859      None{}
860    case GotHead{req}:
861      None{}
862
863def parse(raw: String) -> Maybe<&1, Req>:
864  parse.req(parse.got(raw))
865
866def parse.res.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
867  match hascl:
868    case False{}:
869      HoldBody{rest}
870    case True{}:
871      parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
872
873def parse.res.chunked.eq(rest: String, ok: Bool) -> Hold:
874  match ok:
875    case False{}:
876      HoldUntil{rest}
877    case True{}:
878      chunk.live(rest)
879
880def parse.res.chunked.val(te: String, rest: String) -> Hold:
881  parse.res.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
882
883def parse.res.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
884  match hascl:
885    case True{}:
886      HoldBad{}
887    case False{}:
888      parse.res.chunked.val(header.last(h, "transfer-encoding"), rest)
889
890def parse.res.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
891  match te:
892    case True{}:
893      parse.res.chunked(h, rest, has_header(h, "content-length"))
894    case False{}:
895      parse.res.cl(h, rest, has_header(h, "content-length"))
896
897def parse.res.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
898  parse.res.te(h, rest, has_header(h, "transfer-encoding"))
899
900# Bad: never a message. More: a valid prefix; read on. Done: a whole response.
901type Frame is Type:
902  FrameBad{}
903  FrameMore{}
904  FrameDone{res: Res}
905
906# RFC 9112 §8: a message cut short by close is incomplete, not valid.
907def frame.cut(closed: Bool) -> Frame:
908  match closed:
909    case True{}:
910      FrameBad{}
911    case False{}:
912      FrameMore{}
913
914def frame.wait(res: Res, wait: Bool) -> Frame:
915  match wait:
916    case True{}:
917      FrameMore{}
918    case False{}:
919      FrameDone{res}
920
921def frame.done(status: U32, h: Map<&2, List<&2, String>>, body: Hold, +closed: Bool, open: Bool) -> Frame:
922  match body:
923    case HoldBad{}:
924      FrameBad{}
925    case HoldMore{}:
926      frame.cut(closed)
927    case HoldUntil{b}:
928      frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.not(closed))
929    case HoldBody{b}:
930      frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.and(open, Bool.not(closed)))
931
932# RFC 9112 §6.3 (8): no TE and no CL ⇒ the body runs until the server closes.
933def frame.open(+h: Map<&2, List<&2, String>>) -> Bool:
934  Bool.not(Bool.or(has_header(h, "transfer-encoding"), has_header(h, "content-length")))
935
936# RFC 9112 §6.3 (1): HEAD, 1xx, 204 and 304 responses end at the blank line.
937def frame.nobody(+status: U32, head: Bool) -> Bool:
938  Bool.or(head, Bool.or(U32.is_lt(status, 200), Bool.or(U32.is_eq(status, 204), U32.is_eq(status, 304))))
939
940# 101 is the final response. Other 1xx are interim; a final response follows.
941def frame.interim(+status: U32) -> Bool:
942  Bool.and(U32.is_lt(status, 200), Bool.not(U32.is_eq(status, 101)))
943
944def frame.status(status: U32, +h: Map<&2, List<&2, String>>, rest: String, closed: Bool, nobody: Bool) -> Frame:
945  match nobody:
946    case True{}:
947      FrameDone{Res{status, h, Bytes.new(0)}}
948    case False{}:
949      frame.done(status, h, parse.res.body(h, rest), closed, frame.open(h))
950
951def parse.res.fields(+status: U32, rest: String, fs: Maybe<&2, Map<&2, List<&2, String>>>, closed: Bool, head: Bool) -> Frame:
952  match fs:
953    case None{}:
954      FrameBad{}
955    case Some{h}:
956      frame.status(status, h, rest, closed, frame.nobody(status, head))
957
958def parse.res.num(code: Maybe<&2, U32>, headers: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
959  match code:
960    case None{}:
961      FrameBad{}
962    case Some{n}:
963      parse.res.fields(n, rest, parse.headers(headers, FieldsOk{empty()}), closed, head)
964
965def parse.res.ver(code: String, headers: List<&2, String>, rest: String, closed: Bool, head: Bool, ok: Bool) -> Frame:
966  match ok:
967    case False{}:
968      FrameBad{}
969    case True{}:
970      parse.res.num(parse_u32(code), headers, rest, closed, head)
971
972def parse.res.start3(mpv: String & String & String, headers: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
973  (+ver, code, reason) = mpv
974  parse.res.ver(code, headers, rest, closed, head, Bool.or(String.eq(ver, "HTTP/1.1"), String.eq(ver, "HTTP/1.0")))
975
976def parse.res.lines(xs: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
977  match xs:
978    case Nil{}:
979      FrameBad{}
980    case Con{line, headers}:
981      parse.res.start3(start_line(line), headers, rest, closed, head)
982
983def parse.res.blank(hd: String, rest: String, +closed: Bool, head: Bool, ok: Bool) -> Frame:
984  match ok:
985    case False{}:
986      frame.cut(closed)
987    case True{}:
988      parse.res.lines(String.lines(hd), rest, closed, head)
989
990def parse.res.of(hb: String & String, closed: Bool, head: Bool) -> Frame:
991  (+hd, rest) = hb
992  parse.res.blank(hd, rest, closed, head, blank_end(hd))
993
994type Lead is Data:
995  LeadCut{}
996  LeadFinal{}
997  LeadSkip{+rest: String}
998
999def frame.lead.if(rest: String, interim: Bool) -> Lead:
1000  match interim:
1001    case True{}:
1002      LeadSkip{rest}
1003    case False{}:
1004      LeadFinal{}
1005
1006def frame.lead.num(n: Maybe<&2, U32>, rest: String) -> Lead:
1007  match n:
1008    case None{}:
1009      LeadFinal{}
1010    case Some{s}:
1011      frame.lead.if(rest, frame.interim(s))
1012
1013def frame.lead.code(mpv: String & String & String, rest: String) -> Lead:
1014  (ver, code, reason) = mpv
1015  frame.lead.num(parse_u32(code), rest)
1016
1017def frame.lead.lines(xs: List<&2, String>, rest: String) -> Lead:
1018  match xs:
1019    case Nil{}:
1020      LeadFinal{}
1021    case Con{line, headers}:
1022      frame.lead.code(start_line(line), rest)
1023
1024def frame.lead.blank(+hd: String, rest: String, ok: Bool) -> Lead:
1025  match ok:
1026    case False{}:
1027      LeadCut{}
1028    case True{}:
1029      frame.lead.lines(String.lines(hd), rest)
1030
1031def frame.lead(hb: String & String) -> Lead:
1032  (+hd, rest) = hb
1033  frame.lead.blank(hd, rest, blank_end(hd))
1034
1035def frame.at.cont(+raw: String, lead: Lead) -> String:
1036  match lead:
1037    case LeadCut{}:
1038      raw
1039    case LeadFinal{}:
1040      raw
1041    case LeadSkip{rest}:
1042      rest
1043
1044def frame.at.zero.go(+raw: String, closed: Bool, head: Bool, lead: Lead) -> Frame:
1045  match lead:
1046    case LeadCut{}:
1047      frame.cut(closed)
1048    case LeadFinal{}:
1049      parse.res.of(split_at_blank(raw), closed, head)
1050    case LeadSkip{rest}:
1051      FrameBad{}
1052
1053def frame.at.zero.of(+raw: String, closed: Bool, head: Bool) -> Frame:
1054  frame.at.zero.go(raw, closed, head, frame.lead(split_at_blank(raw)))
1055
1056def frame.at.pos.do(f: Nat, +raw: String, closed: Bool, head: Bool, hb: String & String, lead: Lead) -> Frame:
1057  match f:
1058    case 0n:
1059      match lead:
1060        case LeadCut{}:
1061          frame.cut(closed)
1062        case LeadFinal{}:
1063          parse.res.of(hb, closed, head)
1064        case LeadSkip{+rest}:
1065          frame.at.zero.of(rest, closed, head)
1066    case 1n+g:
1067      match lead:
1068        case LeadCut{}:
1069          frame.cut(closed)
1070        case LeadFinal{}:
1071          parse.res.of(hb, closed, head)
1072        case LeadSkip{+rest}:
1073          frame.at.pos.do(g, rest, closed, head, split_at_blank(rest), frame.lead(split_at_blank(rest)))
1074
1075def frame.at.zero(+raw: String, closed: Bool, head: Bool) -> Frame:
1076  frame.at.zero.of(raw, closed, head)
1077
1078# ponytail: 8 interim responses; raise the fuel if a server sends more
1079def frame.at(fuel: Nat, +raw: String, closed: Bool, head: Bool) -> Frame:
1080  match fuel:
1081    case 0n:
1082      frame.at.zero(raw, closed, head)
1083    case 1n+f:
1084      frame.at.pos.do(f, raw, closed, head, split_at_blank(raw), frame.lead(split_at_blank(raw)))
1085
1086# frame(bytes so far, server closed?, request was HEAD?)
1087def frame(raw: String, closed: Bool, head: Bool) -> Frame:
1088  frame.at(8n, raw, closed, head)
1089
1090def frame.res(f: Frame) -> Maybe<&1, Res>:
1091  match f:
1092    case FrameDone{res}:
1093      Some{res}
1094    case FrameBad{}:
1095      None{}
1096    case FrameMore{}:
1097      None{}
1098
1099def parse_res(raw: String) -> Maybe<&1, Res>:
1100  frame.res(frame(raw, True{}, False{}))
1101
1102def res_fields.res(res: Res, k: String) -> List<&2, String>:
1103  Res{status, headers, body} = res
1104  fields(headers, k)
1105
1106def res_fields(m: Maybe<&1, Res>, k: String) -> List<&2, String>:
1107  match m:
1108    case None{}:
1109      Nil{}
1110    case Some{res}:
1111      res_fields.res(res, k)
1112
1113# The response body as it arrives. Len: bytes left. Chunk: the decoder. Close: until the
1114# server closes. Done: the body is whole. Bad: it cannot become a body.
1115type Rb is Data:
1116  RbLen{left: U32}
1117  RbChunk{st: Dc}
1118  RbClose{}
1119  RbDone{}
1120  RbBad{}
1121
1122def rb.cl(n: Maybe<&2, U32>) -> Maybe<&2, Rb>:
1123  match n:
1124    case None{}:
1125      None{}
1126    case Some{+k}:
1127      Some{Bool.pick(Rb, U32.is_zero(k), RbDone{}, RbLen{k})}
1128
1129def rb.te(+h: Map<&2, List<&2, String>>, cl: Bool) -> Maybe<&2, Rb>:
1130  match cl:
1131    case True{}:
1132      None{}
1133    case False{}:
1134      Some{Bool.pick(Rb, String.eq(String.to_lower(header.last(h, "transfer-encoding")), "chunked"), RbChunk{dc.start()}, RbClose{})}
1135
1136def rb.len(+h: Map<&2, List<&2, String>>, te: Bool) -> Maybe<&2, Rb>:
1137  match te:
1138    case True{}:
1139      rb.te(h, has_header(h, "content-length"))
1140    case False{}:
1141      Bool.pick(Maybe<&2, Rb>, has_header(h, "content-length"), rb.cl(parse_u32(header(h, "content-length"))), Some{RbClose{}})
1142
1143# RFC 9112 §6.3: how the body of this response ends. None: it cannot be framed.
1144def rb.of(+h: Map<&2, List<&2, String>>, nobody: Bool) -> Maybe<&2, Rb>:
1145  match nobody:
1146    case True{}:
1147      Some{RbDone{}}
1148    case False{}:
1149      rb.len(h, has_header(h, "transfer-encoding"))
1150
1151# rb: how the body goes on. parts: body bytes so far, newest first. rest: bytes past a Done body.
1152type Bf is Type:
1153  Bf{rb: Rb, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
1154
1155def rb.len.cut(parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Bf:
1156  (piece, data) = r
1157  Bf{RbDone{}, Con{data, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32)))}
1158
1159def rb.len.have(short: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Bf:
1160  match short:
1161    case True{}:
1162      Bf{RbLen{(left - len : U32)}, Con{piece, parts}, Bytes.new(0)}
1163    case False{}:
1164      rb.len.cut(parts, len, left, Bytes.slice(piece, 0, left))
1165
1166def rb.chunk(c: Ck) -> Bf:
1167  Ck{st, parts, rest} = c
1168  match st:
1169    case DcDone{}:
1170      Bf{RbDone{}, parts, rest}
1171    case DcBad{}:
1172      Bf{RbBad{}, parts, rest}
1173    case DcSize{a, b}:
1174      Bf{RbChunk{DcSize{a, b}}, parts, rest}
1175    case DcExt{x}:
1176      Bf{RbChunk{DcExt{x}}, parts, rest}
1177    case DcSizeLf{x}:
1178      Bf{RbChunk{DcSizeLf{x}}, parts, rest}
1179    case DcData{k}:
1180      Bf{RbChunk{DcData{k}}, parts, rest}
1181    case DcDataCr{}:
1182      Bf{RbChunk{DcDataCr{}}, parts, rest}
1183    case DcDataLf{}:
1184      Bf{RbChunk{DcDataLf{}}, parts, rest}
1185    case DcTr{j}:
1186      Bf{RbChunk{DcTr{j}}, parts, rest}
1187
1188# The body bytes in piece, added to parts.
1189def rb.feed(rb: Rb, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Bf:
1190  match rb:
1191    case RbLen{+left}:
1192      Bytes.Bytes{+len, buf} = piece
1193      rb.len.have(U32.is_lt(len, left), left, parts, len, Bytes.Bytes{len, buf})
1194    case RbChunk{st}:
1195      rb.chunk(ck(piece, st, parts))
1196    case RbClose{}:
1197      Bf{RbClose{}, Con{piece, parts}, Bytes.new(0)}
1198    case RbDone{}:
1199      Bf{RbDone{}, parts, piece}
1200    case RbBad{}:
1201      Bf{RbBad{}, parts, piece}
1202
1203# RFC 9112 §8: only a close-delimited body may end at close.
1204def rb.eof(rb: Rb) -> Bool:
1205  match rb:
1206    case RbClose{}:
1207      True{}
1208    case RbDone{}:
1209      True{}
1210    case RbLen{n}:
1211      False{}
1212    case RbChunk{st}:
1213      False{}
1214    case RbBad{}:
1215      False{}
1216
1217def rb.body(parts: List<&1, Bytes.Bytes>) -> Bytes.Bytes:
1218  Bytes.concat(List.reverse(&1, Bytes.Bytes, parts))
1219
1220# The head scan. Seek: look for the blank line from byte from; k interim heads are behind.
1221# Wait: no blank line yet. Res: the final head, how its body ends, and the bytes after it.
1222type Hs is Type:
1223  HsSeek{buf: Bytes.Bytes, from: U32, k: U32}
1224  HsWait{buf: Bytes.Bytes, k: U32}
1225  HsBad{}
1226  HsRes{res: Res, rb: Rb, rest: Bytes.Bytes}
1227
1228def hs.final(+status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes, m: Maybe<&2, Rb>) -> Hs:
1229  match m:
1230    case None{}:
1231      HsBad{}
1232    case Some{rb}:
1233      HsRes{Res{status, h, Bytes.new(0)}, rb, rest}
1234
1235def hs.skip(more: Bool, +k: U32, rest: Bytes.Bytes) -> Hs:
1236  match more:
1237    case True{}:
1238      HsSeek{rest, 0, (k + 1 : U32)}
1239    case False{}:
1240      HsBad{}
1241
1242def hs.pick(interim: Bool, +head: Bool, +k: U32, +status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes) -> Hs:
1243  match interim:
1244    case True{}:
1245      hs.skip(U32.is_lt(k, 8), k, rest)
1246    case False{}:
1247      hs.final(status, h, rest, rb.of(h, frame.nobody(status, head)))
1248
1249def hs.res(+head: Bool, +k: U32, rest: Bytes.Bytes, res: Res) -> Hs:
1250  Res{+status, +h, body} = res
1251  hs.pick(frame.interim(status), head, k, status, h, rest)
1252
1253# The head alone, framed as a HEAD response so it stops at the blank line.
1254def hs.parsed(+head: Bool, +k: U32, rest: Bytes.Bytes, f: Frame) -> Hs:
1255  match f:
1256    case FrameDone{res}:
1257      hs.res(head, k, rest, res)
1258    case FrameBad{}:
1259      HsBad{}
1260    case FrameMore{}:
1261      HsBad{}
1262
1263def hs.split(+head: Bool, +k: U32, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1264  (buf, hb) = r
1265  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{}))
1266
1267def hs.hit(+head: Bool, +k: U32, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Hs:
1268  match at:
1269    case None{}:
1270      HsWait{buf, k}
1271    case Some{+i}:
1272      +hlen = (i + 4 : U32)
1273      hs.split(head, k, hlen, len, Bytes.slice(buf, 0, hlen))
1274
1275def hs.seek.of(+head: Bool, +k: U32, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Hs:
1276  (tail, m) = r
1277  hs.hit(head, k, len, buf, found.at(from, m))
1278
1279def hs.seek(+head: Bool, +k: U32, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1280  (buf, tail) = r
1281  hs.seek.of(head, k, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
1282
1283def hs.step(+head: Bool, st: Hs) -> Hs:
1284  match st:
1285    case HsSeek{buf, +from, +k}:
1286      Bytes.Bytes{+len, b} = buf
1287      hs.seek(head, k, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
1288    case HsWait{buf, k}:
1289      HsWait{buf, k}
1290    case HsBad{}:
1291      HsBad{}
1292    case HsRes{res, rb, rest}:
1293      HsRes{res, rb, rest}
1294
1295# Each step ends the scan or passes one interim head, and at most 8 interim heads pass.
1296def hs.scan(fuel: Nat, +head: Bool, st: Hs) -> Hs:
1297  match fuel:
1298    case 0n:
1299      match st:
1300        case HsSeek{buf, from, k}:
1301          HsBad{}
1302        case HsWait{buf, k}:
1303          HsWait{buf, k}
1304        case HsBad{}:
1305          HsBad{}
1306        case HsRes{res, rb, rest}:
1307          HsRes{res, rb, rest}
1308    case 1n+f:
1309      hs.scan(f, head, hs.step(head, st))
1310
1311# piece joins buf; only the new bytes, and the 3 before them, can finish the blank line.
1312def hs.more(+head: Bool, +k: U32, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Hs:
1313  Bytes.Bytes{+ol, ob} = buf
1314  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})
1315
1316# Untrusted servers must not grow the buffer without bound.
1317def fetch.max() -> Nat:
1318  U32.to_nat(16777216)
1319
1320# A response read in pieces. Head: the head is not whole yet. Body: it is, and parts is the body so far.
1321# Len: a Content-Length body in one buffer of that size, with left bytes still to come.
1322type Rv is Type:
1323  RvHead{buf: Bytes.Bytes, k: U32}
1324  RvBody{res: Res, rb: Rb, parts: List<&1, Bytes.Bytes>}
1325  RvLen{res: Res, left: U32, body: Bytes.Bytes}
1326
1327# More: read on. Done: the response, and the bytes after it when the body is self-delimited.
1328type Rt is Type:
1329  RtMore{rv: Rv}
1330  RtBad{}
1331  RtDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1332
1333def rv.start() -> Rv:
1334  RvHead{Bytes.new(0), 0}
1335
1336def rv.whole(res: Res, b: Bytes.Bytes, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1337  Res{status, headers, body} = res
1338  RtDone{Res{status, headers, b}, rest}
1339
1340def rv.done(res: Res, parts: List<&1, Bytes.Bytes>, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1341  rv.whole(res, rb.body(parts), rest)
1342
1343def rl.put.of(+total: U32, +len: U32, r: Array<U32> & Array<U32>) -> Bytes.Bytes & Bytes.Bytes:
1344  (src, dst) = r
1345  (Bytes.Bytes{total, dst}, Bytes.Bytes{len, src})
1346
1347# The first m bytes of piece, written into body after the total - left bytes already there.
1348def rl.put(+m: U32, +left: U32, body: Bytes.Bytes, piece: Bytes.Bytes) -> Bytes.Bytes & Bytes.Bytes:
1349  Bytes.Bytes{+total, dst} = body
1350  Bytes.Bytes{+len, src} = piece
1351  rl.put.of(total, len, Bytes.copy(m, src, dst, 0, (total - left : U32)))
1352
1353def rl.fed(short: Bool, res: Res, +left: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Rt:
1354  match short:
1355    case True{}:
1356      (body, piece) = r
1357      RtMore{RvLen{res, (left - len : U32), body}}
1358    case False{}:
1359      (body, piece) = r
1360      rv.whole(res, body, Some{bytes.snd(Bytes.slice(piece, left, (len - left : U32)))})
1361
1362def rl.feed(res: Res, +left: U32, body: Bytes.Bytes, piece: Bytes.Bytes) -> Rt:
1363  Bytes.Bytes{+len, buf} = piece
1364  rl.fed(U32.is_lt(len, left), res, left, len, rl.put(U32.min(len, left), left, body, Bytes.Bytes{len, buf}))
1365
1366def rv.fed(res: Res, bf: Bf) -> Rt:
1367  Bf{rb, parts, rest} = bf
1368  match rb:
1369    case RbDone{}:
1370      rv.done(res, parts, Some{rest})
1371    case RbBad{}:
1372      RtBad{}
1373    case RbLen{n}:
1374      RtMore{RvBody{res, RbLen{n}, parts}}
1375    case RbChunk{st}:
1376      RtMore{RvBody{res, RbChunk{st}, parts}}
1377    case RbClose{}:
1378      RtMore{RvBody{res, RbClose{}, parts}}
1379
1380# Some{left}: a Content-Length body small enough to allocate up front. Larger ones fail at the fetch cap.
1381def rb.buf(rb: Rb) -> Maybe<&2, U32>:
1382  match rb:
1383    case RbLen{+left}:
1384      Bool.pick(Maybe<&2, U32>, Nat.is_lt(fetch.max(), U32.to_nat(left)), None{}, Some{left})
1385    case RbChunk{st}:
1386      None{}
1387    case RbClose{}:
1388      None{}
1389    case RbDone{}:
1390      None{}
1391    case RbBad{}:
1392      None{}
1393
1394def rv.body(m: Maybe<&2, U32>, res: Res, rb: Rb, rest: Bytes.Bytes) -> Rt:
1395  match m:
1396    case None{}:
1397      rv.fed(res, rb.feed(rb, Nil{}, rest))
1398    case Some{+left}:
1399      rl.feed(res, left, Bytes.new(left), rest)
1400
1401def rv.head(hs: Hs) -> Rt:
1402  match hs:
1403    case HsWait{buf, k}:
1404      RtMore{RvHead{buf, k}}
1405    case HsBad{}:
1406      RtBad{}
1407    case HsSeek{buf, from, k}:
1408      RtBad{}
1409    case HsRes{res, +rb, rest}:
1410      rv.body(rb.buf(rb), res, rb, rest)
1411
1412def rv.eof(res: Res, parts: List<&1, Bytes.Bytes>, ok: Bool) -> Rt:
1413  match ok:
1414    case True{}:
1415      rv.done(res, parts, None{})
1416    case False{}:
1417      RtBad{}
1418
1419# One read: piece, or the server closed (RFC 9112 §8: a message cut short is not a message).
1420def rv.step(closed: Bool, +head: Bool, rv: Rv, piece: Bytes.Bytes) -> Rt:
1421  match closed:
1422    case True{}:
1423      match rv:
1424        case RvHead{buf, k}:
1425          RtBad{}
1426        case RvBody{res, rb, parts}:
1427          rv.eof(res, parts, rb.eof(rb))
1428        case RvLen{res, left, body}:
1429          RtBad{}
1430    case False{}:
1431      match rv:
1432        case RvHead{buf, +k}:
1433          rv.head(hs.more(head, k, buf, piece))
1434        case RvBody{res, rb, parts}:
1435          rv.fed(res, rb.feed(rb, parts, piece))
1436        case RvLen{res, +left, body}:
1437          rl.feed(res, left, body, piece)
1438
1439def rv.end(closed: Bool, +head: Bool, t: Rt) -> Rt:
1440  match closed:
1441    case False{}:
1442      t
1443    case True{}:
1444      match t:
1445        case RtMore{rv}:
1446          rv.step(True{}, head, rv, Bytes.new(0))
1447        case RtBad{}:
1448          RtBad{}
1449        case RtDone{res, rest}:
1450          RtDone{res, rest}
1451
1452def rv.go(xs: List<&2, String>, closed: Bool, +head: Bool, t: Rt) -> Rt:
1453  match xs:
1454    case Nil{}:
1455      rv.end(closed, head, t)
1456    case Con{+x, rest}:
1457      match t:
1458        case RtMore{rv}:
1459          rv.go(rest, closed, head, rv.step(False{}, head, rv, Bytes.from_string(x)))
1460        case RtBad{}:
1461          RtBad{}
1462        case RtDone{res, r}:
1463          RtDone{res, r}
1464
1465def rt.frame(t: Rt) -> Frame:
1466  match t:
1467    case RtMore{rv}:
1468      FrameMore{}
1469    case RtBad{}:
1470      FrameBad{}
1471    case RtDone{res, rest}:
1472      FrameDone{res}
1473
1474# What the read loop makes of these pieces, then a close when closed is set.
1475def res.frame(xs: List<&2, String>, closed: Bool, +head: Bool) -> Frame:
1476  rt.frame(rv.go(xs, closed, head, RtMore{rv.start()}))
1477
1478def rt.rest(t: Rt) -> Maybe<&1, Bytes.Bytes>:
1479  match t:
1480    case RtMore{rv}:
1481      None{}
1482    case RtBad{}:
1483      None{}
1484    case RtDone{res, rest}:
1485      rest
1486
1487def after.of(m: Maybe<&1, Bytes.Bytes>) -> Maybe<&2, String>:
1488  match m:
1489    case None{}:
1490      None{}
1491    case Some{b}:
1492      Some{Bytes.to_string(b)}
1493
1494# Bytes after a complete self-delimited message. None if it is not one yet.
1495def after(+raw: String, +head: Bool) -> Maybe<&2, String>:
1496  after.of(rt.rest(rv.go([raw], False{}, head, RtMore{rv.start()})))
1497
1498def req.v11.ver(mpv: String & String & String) -> Bool:
1499  (+method, path, v) = mpv
1500  String.eq(v, "HTTP/1.1")
1501
1502def req.v11.line(+line: String) -> Bool:
1503  req.v11.ver(start_line(line))
1504
1505def req.v11.lines(xs: List<&2, String>) -> Bool:
1506  match xs:
1507    case Nil{}:
1508      False{}
1509    case Con{line, headers}:
1510      req.v11.line(line)
1511
1512def req.v11.pick(+head: String, ok: Bool) -> Bool:
1513  match ok:
1514    case False{}:
1515      False{}
1516    case True{}:
1517      req.v11.lines(String.lines(head))
1518
1519def req.v11.of(hb: String & String) -> Bool:
1520  (+head, rest) = hb
1521  req.v11.pick(head, blank_end(head))
1522
1523def req.v11(+raw: String) -> Bool:
1524  req.v11.of(split_at_blank(raw))
1525
1526def req.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1527  String.eq(String.to_lower(header(headers, "connection")), "close")
1528
1529def res.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1530  String.eq(String.to_lower(header(headers, "connection")), "close")
1531
1532def serve.fail_close(+status: U32) -> Bool:
1533  Bool.or(U32.is_eq(status, 400), Bool.or(U32.is_eq(status, 413), U32.is_eq(status, 431)))
1534
1535def serve.keep.ok(fail: Bool, res_close: Bool) -> Bool:
1536  match fail:
1537    case True{}:
1538      False{}
1539    case False{}:
1540      Bool.not(res_close)
1541
1542def serve.keep.v11(v11: Bool, +req_close: Bool, +status: U32, res_close: Bool) -> Bool:
1543  match v11:
1544    case False{}:
1545      False{}
1546    case True{}:
1547      match req_close:
1548        case True{}:
1549          False{}
1550        case False{}:
1551          serve.keep.ok(serve.fail_close(status), res_close)
1552
1553def serve.keep(+headers: Map<&2, List<&2, String>>, v11: Bool, +status: U32, +res: Map<&2, List<&2, String>>) -> Bool:
1554  serve.keep.v11(v11, req.conn_close(headers), status, res.conn_close(res))
1555
1556
1557def again.keep(close: Bool, x: Bytes.Bytes) -> Maybe<&1, Bytes.Bytes>:
1558  match close:
1559    case True{}:
1560      None{}
1561    case False{}:
1562      Some{x}
1563
1564def again.rest(close: Bool, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1565  match rest:
1566    case None{}:
1567      None{}
1568    case Some{x}:
1569      again.keep(close, x)
1570
1571# The bytes past the response when the socket can take another request: the request did not
1572# ask to close, the response is self-delimited, and the peer did not say close.
1573def again(close: Bool, +h: Map<&2, List<&2, String>>, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1574  match close:
1575    case True{}:
1576      None{}
1577    case False{}:
1578      again.rest(String.eq(String.to_lower(header(h, "connection")), "close"), rest)
1579
1580def res_body.res(res: Res) -> Bytes.Bytes:
1581  Res{status, headers, body} = res
1582  body
1583
1584def res_body(m: Maybe<&1, Res>) -> Bytes.Bytes:
1585  match m:
1586    case None{}:
1587      Bytes.new(0)
1588    case Some{res}:
1589      res_body.res(res)
1590
1591def text(res: Res) -> String:
1592  Enc.utf8.decode(res_body.res(res))
1593
1594# UTF-8 is checked, not repaired: bad UTF-8 in a string gives None (RFC 8259 §8.1).
1595def json(res: Res) -> Maybe<&1, Json.Val>:
1596  Json.parse.bytes(res_body.res(res))
1597
1598def got_body.req(req: Req) -> Bytes.Bytes:
1599  Req{method, path, headers, body} = req
1600  body
1601
1602def got_body(m: Maybe<&1, Req>) -> Bytes.Bytes:
1603  match m:
1604    case None{}:
1605      Bytes.new(0)
1606    case Some{req}:
1607      got_body.req(req)
1608
1609def body.of(hb: String & String) -> String:
1610  (h, b) = hb
1611  b
1612
1613def body(s: String) -> String:
1614  body.of(split_at_blank.go(s, False{}, 0, SNil{}))
1615
1616def headers_lines(+k: String, vs: List<&2, String>, acc: String) -> String:
1617  match vs:
1618    case Nil{}:
1619      acc
1620    case Con{v, t}:
1621      headers_lines(k, t, acc ++ ("\r\n" ++ sanitize(k) ++ ": " ++ sanitize(v)))
1622
1623def headers_block.go(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, acc: String) -> String:
1624  match xs:
1625    case Nil{}:
1626      acc
1627    case (k, vs) <> t:
1628      headers_block.go(t, headers_lines(k, vs, acc))
1629
1630def headers_block(h: Map<&2, List<&2, String>>) -> String:
1631  headers_block.go(Map.to_list(&2, List<&2, String>, h), "")
1632
1633# RFC 9110 §15. An unknown code gets an empty reason, which RFC 9112 §4 allows.
1634type Reason is Data:
1635  Reason{code: U32, text: String}
1636
1637def reasons() -> List<&2, Reason>:
1638  [Reason{100, "Continue"}, Reason{101, "Switching Protocols"}, Reason{103, "Early Hints"},
1639   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"},
1640   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"},
1641   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"},
1642   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"}]
1643
1644def reason.go(xs: List<&2, Reason>, +status: U32) -> String:
1645  match xs:
1646    case Nil{}:
1647      ""
1648    case Con{Reason{k, v}, t}:
1649      Bool.pick(String, U32.is_eq(k, status), v, reason.go(t, status))
1650
1651def reason(+status: U32) -> String:
1652  reason.go(reasons(), status)
1653
1654def response(+status: U32, headers: Map<&2, List<&2, String>>, body: String) -> String:
1655  ("HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1656
1657def encode.body(head: Bool, top: Bytes.Bytes, body: Bytes.Bytes) -> Bytes.Bytes:
1658  match head:
1659    case True{}:
1660      top
1661    case False{}:
1662      Bytes.append(top, body)
1663
1664def encode.len(+status: U32, headers: Map<&2, List<&2, String>>, head: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1665  Bytes.Bytes{+len, buf} = body
1666  encode.body(head, Bytes.from_string(response(status, set(headers, "content-length", U32.show(len)), "")), Bytes.Bytes{len, buf})
1667
1668# RFC 9110 §6.4.1, §8.6: 1xx, 204 and 304 have no body; HEAD gets the length but no body.
1669def encode.pick(+status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, head: Bool, nobody: Bool) -> Bytes.Bytes:
1670  match nobody:
1671    case True{}:
1672      Bytes.from_string(response(status, headers, ""))
1673    case False{}:
1674      encode.len(status, headers, head, body)
1675
1676def encode.on(r: Res, head: Bool) -> Bytes.Bytes:
1677  Res{+status, headers, body} = r
1678  encode.pick(status, headers, body, head, frame.nobody(status, False{}))
1679
1680def encode(r: Res) -> Bytes.Bytes:
1681  encode.on(r, False{})
1682
1683def request(method: String, path: String, headers: Map<&2, List<&2, String>>, body: String) -> String:
1684  (method ++ " " ++ path ++ " HTTP/1.1" ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1685
1686def req.reserved(+k: String) -> Bool:
1687  Bool.or(Bool.or(String.eq(k, "host"), String.eq(k, "connection")), Bool.or(String.eq(k, "content-length"), String.eq(k, "transfer-encoding")))
1688
1689def req.put.one(m: Map<&2, List<&2, String>>, +k: String, vs: List<&2, String>, skip: Bool) -> Map<&2, List<&2, String>>:
1690  match skip:
1691    case True{}:
1692      m
1693    case False{}:
1694      Map.set(&2, List<&2, String>, m, k, vs)
1695
1696def req.put(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1697  match xs:
1698    case Nil{}:
1699      m
1700    case (k, vs) <> t:
1701      +lk = String.to_lower(k)
1702      req.put(t, req.put.one(m, lk, vs, req.reserved(lk)))
1703
1704# RFC 9110 §8.6: no Content-Length on a bodiless request whose method gives a body no meaning.
1705def req.cl(+m: Map<&2, List<&2, String>>, +method: String, +len: U32) -> Map<&2, List<&2, String>>:
1706  +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"))))
1707  Bool.pick(Map<&2, List<&2, String>>, bodied, set(m, "content-length", U32.show(len)), m)
1708
1709# Caller headers are lowercased so they cannot duplicate ours; host, connection,
1710# content-length and transfer-encoding are always ours (no smuggling through them).
1711def encode_req.word(close: Bool) -> String:
1712  match close:
1713    case True{}:
1714      "close"
1715    case False{}:
1716      "keep-alive"
1717
1718def encode_req.on(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, close: Bool) -> Bytes.Bytes:
1719  Bytes.Bytes{+len, buf} = body
1720  +h = set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", host), "connection", encode_req.word(close))
1721  Bytes.append(Bytes.from_string(request(method, target, req.cl(h, method, len), "")), Bytes.Bytes{len, buf})
1722
1723def encode_req(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Bytes.Bytes:
1724  encode_req.on(method, target, host, headers, body, True{})
1725
1726# Redirects (RFC 9110 §15.4, as WHATWG fetch applies them)
1727# --------------------------------------------------------
1728
1729# One request to make: headers are already lowercased (see req.put).
1730type Hop is Type:
1731  Hop{method: String, url: Url.Abs, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
1732
1733def redirect.code(+s: U32) -> Bool:
1734  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))))
1735
1736def redirect.origin(a: Url.Abs) -> String:
1737  Url.Abs{scheme, host, port, target} = a
1738  scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1739
1740def redirect.del(ks: List<&2, String>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1741  match ks:
1742    case Nil{}:
1743      m
1744    case Con{k, t}:
1745      redirect.del(t, Map.del(&2, List<&2, String>, m, k))
1746
1747def redirect.hdrs(+h: Map<&2, List<&2, String>>, drop: Bool, cross: Bool) -> Map<&2, List<&2, String>>:
1748  +h2 = Bool.pick(Map<&2, List<&2, String>>, drop, redirect.del(["content-type", "content-encoding", "content-language", "content-location"], h), h)
1749  Bool.pick(Map<&2, List<&2, String>>, cross, redirect.del(["authorization", "cookie", "proxy-authorization"], h2), h2)
1750
1751# 303 turns any method but HEAD into GET; 301 and 302 turn POST into GET;
1752# 307 and 308 keep method and body. A GET carries no body or body headers.
1753# Credentials do not follow a hop to another origin.
1754def redirect.body(drop: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1755  match drop:
1756    case True{}:
1757      Bytes.new(0)
1758    case False{}:
1759      body
1760
1761def 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>:
1762  match next:
1763    case None{}:
1764      None{}
1765    case Some{+to}:
1766      +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")))
1767      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)}}
1768
1769def redirect.hop(status: U32, h: Hop, loc: String) -> Maybe<&1, Hop>:
1770  Hop{method, +url, headers, body} = h
1771  redirect.to(status, method, url, headers, body, Url.resolve(url, loc))
1772
1773def redirect.if(status: U32, h: Hop, loc: String, ok: Bool) -> Maybe<&1, Hop>:
1774  match ok:
1775    case False{}:
1776      None{}
1777    case True{}:
1778      redirect.hop(status, h, loc)
1779
1780# The next request after a response, or None when it is not a redirect we follow.
1781def redirect(+status: U32, +headers: Map<&2, List<&2, String>>, h: Hop) -> Maybe<&1, Hop>:
1782  redirect.if(status, h, header(headers, "location"), Bool.and(redirect.code(status), has_header(headers, "location")))
1783
1784def io.recv.words(tls: Bool, s: Socket, max: U32, ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>):
1785  match tls:
1786    case True{}:
1787      Wire.tls.recv.words(s, max, ms)
1788    case False{}:
1789      Wire.recv.words(s, max, ms)
1790
1791def io.send(tls: Bool, s: Socket, data: String) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1792  match tls:
1793    case True{}:
1794      Wire.tls.send(s, data)
1795    case False{}:
1796      Wire.send(s, data)
1797
1798def io.send.words(tls: Bool, s: Socket, +len: U32, buf: Array<U32>) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1799  match tls:
1800    case True{}:
1801      Wire.tls.send.words(s, len, buf)
1802    case False{}:
1803      Wire.send.words(s, len, buf)
1804
1805def io.send.bytes(tls: Bool, s: Socket, b: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1806  Bytes.Bytes{+len, buf} = b
1807  io.send.words(tls, s, len, buf)
1808
1809def io.close(tls: Bool, s: Socket) -> IO(Unit):
1810  match tls:
1811    case True{}:
1812      Wire.tls.close(s)
1813    case False{}:
1814      Socket.close(s)
1815
1816def fetch.close(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
1817  do IO<Result<&1, &1, Err, Res>>:
1818    io.close(tls, s)
1819    return r
1820
1821# none: no response byte arrived, so an idempotent request may be retried (RFC 9112 §9.3.1).
1822# sock: the socket, when it can take another request.
1823type Out is Type:
1824  OutDone{res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes}
1825  OutFail{e: Err, none: Bool}
1826
1827def fetch.boxed(r: Result<&1, &1, Err, Res>, none: Bool) -> Out:
1828  match r:
1829    case Done{res}:
1830      OutDone{res, None{}, Bytes.new(0)}
1831    case Fail{e}:
1832      OutFail{e, none}
1833
1834def fetch.bad(tls: Bool, s: Socket, e: Maybe<&2, Err>) -> IO(Result<&1, &1, Err, Res>):
1835  match e:
1836    case None{}:
1837      fetch.close(tls, s, Fail{ErrBad{}})
1838    case Some{err}:
1839      fetch.close(tls, s, Fail{err})
1840
1841def fetch.shut(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>, none: Bool) -> IO(Out):
1842  do IO<Out>:
1843    x : Result<&1, &1, Err, Res> <- fetch.close(tls, s, r)
1844    return fetch.boxed(x, none)
1845
1846def fetch.hold.go(tls: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
1847  match left:
1848    case Some{x}:
1849      IO.pure(Out, OutDone{res, Some{s}, x})
1850    case None{}:
1851      fetch.shut(tls, s, Done{res}, False{})
1852
1853def fetch.hold(tls: Bool, close: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
1854  Res{status, +headers, body} = res
1855  fetch.hold.go(tls, s, Res{status, headers, body}, again(close, headers, left))
1856
1857def fetch.failout(tls: Bool, s: Socket, e: Maybe<&2, Err>, none: Bool) -> IO(Out):
1858  do IO<Out>:
1859    r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, e)
1860    return fetch.boxed(r, none)
1861
1862# Read state: the response so far and the bytes read, or how it ended.
1863# none: no byte arrived, so an idempotent request may be retried.
1864type Fl is Type:
1865  FlMore{rv: Rv, n: U32}
1866  FlBad{err: Maybe<&2, Err>, none: Bool}
1867  FlDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1868
1869def fetch.rt(+n: U32, t: Rt) -> Fl:
1870  match t:
1871    case RtMore{rv}:
1872      FlMore{rv, n}
1873    case RtBad{}:
1874      FlBad{None{}, U32.is_zero(n)}
1875    case RtDone{res, rest}:
1876      FlDone{res, rest}
1877
1878# 64 KiB of head past the body cap, as serve allows.
1879def fetch.over(+n: U32) -> Bool:
1880  Nat.is_lt(Nat.add(fetch.max(), 65536n), U32.to_nat(n))
1881
1882def fetch.piece.cap(over: Bool, +head: Bool, rv: Rv, +n2: U32, +len: U32, buf: Array<U32>) -> Fl:
1883  match over:
1884    case True{}:
1885      FlBad{None{}, False{}}
1886    case False{}:
1887      fetch.rt(n2, rv.step(U32.is_zero(len), head, rv, Bytes.Bytes{len, buf}))
1888
1889def fetch.piece(+head: Bool, rv: Rv, +n: U32, p: U32 & Array<U32>) -> Fl:
1890  (+len, buf) = p
1891  +n2 = (n + len : U32)
1892  fetch.piece.cap(fetch.over(n2), head, rv, n2, len, buf)
1893
1894def fetch.next(+head: Bool, rv: Rv, +n: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Fl:
1895  (s, r) = m
1896  match r:
1897    case Fail{(+code, why)}:
1898      (s, FlBad{Some{err.or_late(code, ErrRead{code, why})}, U32.is_zero(n)})
1899    case Done{p}:
1900      (s, fetch.piece(head, rv, n, p))
1901
1902# Reads until the response is whole or cannot be; an empty read means the server closed.
1903@unsafe
1904def fetch.loop(+close: Bool, +head: Bool, +tls: Bool, +ms: U32, st: Socket & Fl) -> IO(Out):
1905  (s, fl) = st
1906  match fl:
1907    case FlMore{rv, +n}:
1908      do IO<Out>:
1909        m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
1910        fetch.loop(close, head, tls, ms, fetch.next(head, rv, n, m))
1911    case FlBad{err, none}:
1912      fetch.failout(tls, s, err, none)
1913    case FlDone{res, rest}:
1914      fetch.hold(tls, close, s, res, rest)
1915
1916def exchange.sent(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Out):
1917  (s, r) = m
1918  match r:
1919    case Fail{(+code, why)}:
1920      fetch.shut(tls, s, Fail{err.or_late(code, ErrWrite{code, why})}, True{})
1921    case Done{u}:
1922      fetch.loop(close, head, tls, ms, (s, FlMore{rv.start(), 0}))
1923
1924def exchange.go(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, s: Socket, wire: Bytes.Bytes) -> IO(Out):
1925  do IO<Out>:
1926    sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
1927    exchange.sent(tls, ms, close, head, sent)
1928
1929def exchange.tup(o: Out) -> Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes:
1930  match o:
1931    case OutFail{e, none}:
1932      (None{}, Fail{e}, Bytes.new(0))
1933    case OutDone{res, sock, rest}:
1934      (sock, Done{res}, rest)
1935
1936# One request on an open socket. Some{socket}: it can take another request.
1937def 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):
1938  do IO<Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes>:
1939    o : Out <- exchange.go(tls, ms, close, head, s, wire)
1940    return exchange.tup(o)
1941
1942# Paths to a PEM client chain and its private key for mutual TLS.
1943type Cert is Data:
1944  Cert{chain: String, key: String}
1945
1946# Connection pool: idle sockets by origin and client identity, newest first, at most cap per key.
1947# fetch uses a fresh pool per call.
1948
1949type Conn is Type:
1950  Conn{tls: Bool, s: Socket}
1951  ConnH2{s: Socket, client: H2.Client}
1952
1953type Send is Type:
1954  Send{method: String, target: String, authority: String,
1955    headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
1956
1957type H2Step is Type:
1958  H2Reply{s: Socket, reply: H2.Reply}
1959  H2Sent{client: H2.Client, events: List<&1, H2.ClientEvent>,
1960    sent: Result<&1, &1, Err, Socket>}
1961  H2Events{s: Socket, client: H2.Client, result: Result<&1, &1, Err, Maybe<&1, Res>>}
1962  H2Received{client: H2.Client,
1963    answer: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>}
1964
1965type Pool is Type:
1966  Pool{cap: U32, idle: Map<&1, List<&1, Conn>>}
1967
1968def pool.new.with(+cap: U32) -> Pool:
1969  Pool{cap, Map.new(&1, List<&1, Conn>)}
1970
1971# Up to 8 idle sockets per origin.
1972def pool.new() -> Pool:
1973  pool.new.with(8)
1974
1975def pool.key(+scheme: String, +host: String, +port: U32) -> String:
1976  scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1977
1978def pool.key.cert(+base: String, cert: Maybe<&2, Cert>) -> String:
1979  match cert:
1980    case None{}:
1981      base
1982    case Some{Cert{+chain, +key}}:
1983      base ++ "|cert:" ++ Nat.show(String.length(chain)) ++ ":" ++ chain
1984        ++ Nat.show(String.length(key)) ++ ":" ++ key
1985
1986def pool.take.of(+cap: U32, +key: String, r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> Pool & Maybe<&1, Conn>:
1987  (m, got) = r
1988  match got:
1989    case None{}:
1990      (Pool{cap, m}, None{})
1991    case Some{xs}:
1992      match xs:
1993        case Nil{}:
1994          (Pool{cap, m}, None{})
1995        case Con{c, t}:
1996          (Pool{cap, Map.set(&1, List<&1, Conn>, m, key, t)}, Some{c})
1997
1998# The socket given back last.
1999def pool.take(p: Pool, +key: String) -> Pool & Maybe<&1, Conn>:
2000  Pool{+cap, idle} = p
2001  pool.take.of(cap, key, Map.pop(&1, List<&1, Conn>, idle, key))
2002
2003def conn.close(c: Conn) -> IO(Unit):
2004  match c:
2005    case Conn{tls, s}:
2006      io.close(tls, s)
2007    case ConnH2{s, client}:
2008      Wire.tls.close(s)
2009
2010# The first n sockets; the rest are closed.
2011def conns.cut(xs: List<&1, Conn>, n: Nat) -> IO(List<&1, Conn>):
2012  match xs:
2013    case Nil{}:
2014      IO.pure(List<&1, Conn>, Nil{})
2015    case Con{c, t}:
2016      match n:
2017        case 0n:
2018          do IO<List<&1, Conn>>:
2019            conn.close(c)
2020            conns.cut(t, 0n)
2021        case 1n+k:
2022          do IO<List<&1, Conn>>:
2023            r : List<&1, Conn> <- conns.cut(t, k)
2024            return c <> r
2025
2026def pool.give.of(+cap: U32, +key: String, c: Conn, limit: Nat,
2027    r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> IO(Pool):
2028  (m, old) = r
2029  do IO<Pool>:
2030    xs : List<&1, Conn> <- conns.cut(c <> Maybe.default(&1, List<&1, Conn>, old, Nil{}), limit)
2031    return Pool{cap, Map.set(&1, List<&1, Conn>, m, key, xs)}
2032
2033# Past the limit (cap for HTTP/1.1, one session for HTTP/2), close the oldest idle connection.
2034def pool.give(p: Pool, +key: String, c: Conn) -> IO(Pool):
2035  Pool{+cap, idle} = p
2036  match c:
2037    case Conn{tls, s}:
2038      pool.give.of(cap, key, Conn{tls, s}, U32.to_nat(cap), Map.pop(&1, List<&1, Conn>, idle, key))
2039    case ConnH2{s, client}:
2040      pool.give.of(cap, key, ConnH2{s, client}, Bool.pick(Nat, U32.is_zero(cap), 0n, 1n),
2041        Map.pop(&1, List<&1, Conn>, idle, key))
2042
2043def pool.close.go(xs: List<&1, List<&1, Conn>>) -> IO(Unit):
2044  match xs:
2045    case Nil{}:
2046      IO.pure(Unit, Unit{})
2047    case Con{cs, t}:
2048      do IO<Unit>:
2049        none : List<&1, Conn> <- conns.cut(cs, 0n)
2050        pool.close.go(t)
2051
2052def pool.close(p: Pool) -> IO(Unit):
2053  Pool{cap, idle} = p
2054  pool.close.go(Map.values(&1, List<&1, Conn>, idle))
2055
2056# RFC 9110 §9.2.2
2057def pool.idempotent(+method: String) -> Bool:
2058  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"))))))
2059
2060def conn.tls(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2061  (s, r) = m
2062  match r:
2063    case Fail{(+code, why)}:
2064      do IO<Result<&1, &1, Err, Conn>>:
2065        Wire.tls.close(s)
2066        return Fail{err.or_late(code, ErrTls{code, why})}
2067    case Done{u}:
2068      IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2069
2070def conn.h2.sent(client: H2.Client, r: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2071  (s, sent) = r
2072  match sent:
2073    case Fail{(+code, why)}:
2074      do IO<Result<&1, &1, Err, Conn>>:
2075        Wire.tls.close(s)
2076        return Fail{err.or_late(code, ErrWrite{code, why})}
2077    case Done{u}:
2078      IO.pure(Result<&1, &1, Err, Conn>, Done{ConnH2{s, client}})
2079
2080def conn.h2.start(s: Socket, r: H2.Client & HBytes.Bytes) -> IO(Result<&1, &1, Err, Conn>):
2081  (client, HBytes.Bytes{len, buf}) = r
2082  do IO<Result<&1, &1, Err, Conn>>:
2083    sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.send.words(s, len, buf)
2084    conn.h2.sent(client, sent)
2085
2086def conn.tls.protocol(proto: String, s: Socket) -> IO(Result<&1, &1, Err, Conn>):
2087  match proto:
2088    case "h2":
2089      conn.h2.start(s, H2.client.start())
2090    case "http/1.1":
2091      IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2092    case "":
2093      IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2094    case other:
2095      do IO<Result<&1, &1, Err, Conn>>:
2096        Wire.tls.close(s)
2097        return Fail{ErrTls{71, "unsupported ALPN: " ++ other}}
2098
2099def conn.tls.alpn(m: Socket & Result<&1, &1, U32 & String, String>) -> IO(Result<&1, &1, Err, Conn>):
2100  (s, r) = m
2101  match r:
2102    case Fail{(+code, why)}:
2103      do IO<Result<&1, &1, Err, Conn>>:
2104        Wire.tls.close(s)
2105        return Fail{err.or_late(code, ErrTls{code, why})}
2106    case Done{proto}:
2107      conn.tls.protocol(proto, s)
2108
2109def conn.secure.no.cert(offer: Bool, s: Socket, host: String, +ms: U32) ->
2110    IO(Result<&1, &1, Err, Conn>):
2111  match offer:
2112    case True{}:
2113      do IO<Result<&1, &1, Err, Conn>>:
2114        hs : Socket & Result<&1, &1, U32 & String, String> <-
2115          Wire.tls.connect.alpn(s, host, ms, "h2,http/1.1")
2116        conn.tls.alpn(hs)
2117    case False{}:
2118      do IO<Result<&1, &1, Err, Conn>>:
2119        hs : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.connect(s, host, ms)
2120        conn.tls(hs)
2121
2122def conn.secure.tls(cert: Maybe<&2, Cert>, s: Socket, host: String, +ms: U32,
2123    offer: Bool) -> IO(Result<&1, &1, Err, Conn>):
2124  match cert:
2125    case None{}:
2126      conn.secure.no.cert(offer, s, host, ms)
2127    case Some{Cert{chain, key}}:
2128      do IO<Result<&1, &1, Err, Conn>>:
2129        hs : Socket & Result<&1, &1, U32 & String, Unit> <-
2130          Wire.tls.connect.cert(s, host, ms, chain, key)
2131        conn.tls(hs)
2132
2133# A failed handshake is an error, never plaintext.
2134def conn.secure(+ms: U32, sni: String, s: Socket, tls: Bool,
2135    cert: Maybe<&2, Cert>, offer: Bool) -> IO(Result<&1, &1, Err, Conn>):
2136  match tls:
2137    case False{}:
2138      IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{False{}, s}})
2139    case True{}:
2140      conn.secure.tls(cert, s, sni, ms, offer)
2141
2142def conn.made(+ms: U32, sni: String, tls: Bool, cert: Maybe<&2, Cert>,
2143    offer: Bool, r: Result<&1, &1, U32 & String, Socket>) ->
2144    IO(Result<&1, &1, Err, Conn>):
2145  match r:
2146    case Fail{(+code, why)}:
2147      IO.pure(Result<&1, &1, Err, Conn>, Fail{err.or_late(code, ErrConnect{code, why})})
2148    case Done{s}:
2149      conn.secure(ms, sni, s, tls, cert, offer)
2150
2151def conn.open(+tls: Bool, +ms: U32, sni: String, ip: String, port: U32) ->
2152    IO(Result<&1, &1, Err, Conn>):
2153  do IO<Result<&1, &1, Err, Conn>>:
2154    c : Result<&1, &1, U32 & String, Socket> <- Wire.connect(ip, port, ms)
2155    conn.made(ms, sni, tls, None{}, False{}, c)
2156
2157# ponytail: addresses are tried in order, not raced; a broken first route can consume the step timeout.
2158type Dial is Type:
2159  Dial{port: U32, ms: U32, deadline: Nat, action: IO(Result<&1, &1, U32 & String, Socket>)}
2160
2161def conn.dial.time(+ip: String, +port: U32, +deadline: Nat, now: Nat, expired: Bool) ->
2162  IO(Result<&1, &1, U32 & String, Socket>):
2163  match expired:
2164    case True{}:
2165      IO.pure(Result<&1, &1, U32 & String, Socket>, Fail{(60, "connect timeout")})
2166    case False{}:
2167      Wire.connect(ip, port, U32.from_nat(Nat.sub(deadline, now)))
2168
2169def conn.dial.with(+ip: String, +port: U32, +ms: U32, +deadline: Nat, +now: Nat, unlimited: Bool) ->
2170  IO(Result<&1, &1, U32 & String, Socket>):
2171  match unlimited:
2172    case True{}:
2173      Wire.connect(ip, port, 0)
2174    case False{}:
2175      conn.dial.time(ip, port, deadline, now, Nat.is_le(deadline, now))
2176
2177def conn.dial.try(+ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2178  IO(Result<&1, &1, U32 & String, Socket>):
2179  do IO<Result<&1, &1, U32 & String, Socket>>:
2180    now : Nat <- IO.now()
2181    conn.dial.with(ip, port, ms, deadline, now, U32.is_zero(ms))
2182
2183def conn.dial.after(r: Result<&1, &1, U32 & String, Socket>, ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2184  IO(Result<&1, &1, U32 & String, Socket>):
2185  match r:
2186    case Done{s}:
2187      IO.pure(Result<&1, &1, U32 & String, Socket>, Done{s})
2188    case Fail{e}:
2189      conn.dial.try(ip, port, ms, deadline)
2190
2191def conn.dial.more(prev: IO(Result<&1, &1, U32 & String, Socket>), ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2192  IO(Result<&1, &1, U32 & String, Socket>):
2193  do IO<Result<&1, &1, U32 & String, Socket>>:
2194    r : Result<&1, &1, U32 & String, Socket> <- prev
2195    conn.dial.after(r, ip, port, ms, deadline)
2196
2197def conn.dial.fold(d: Dial, ip: String) -> Dial:
2198  Dial{+port, +ms, +deadline, action} = d
2199  Dial{port, ms, deadline, conn.dial.more(action, ip, port, ms, deadline)}
2200
2201def conn.dial.run(d: Dial) -> IO(Result<&1, &1, U32 & String, Socket>):
2202  Dial{port, ms, deadline, action} = d
2203  action
2204
2205def conn.dial.all(+port: U32, +ms: U32, +start: Nat, first: String, rest: List<&2, String>) ->
2206  IO(Result<&1, &1, U32 & String, Socket>):
2207  match rest:
2208    case Nil{}:
2209      Wire.connect(first, port, ms)
2210    case Con{ip, tail}:
2211      +deadline = Nat.add(start, U32.to_nat(ms))
2212      conn.dial.run(List.foldl(~&2, ~String, ~Dial, ~conn.dial.fold, Con{ip, tail},
2213        Dial{port, ms, deadline, Wire.connect(first, port, ms)}))
2214
2215def conn.open.all(+tls: Bool, +ms: U32, +host: String, +port: U32,
2216    ips: List<&2, String>, cert: Maybe<&2, Cert>, offer: Bool) ->
2217    IO(Result<&1, &1, Err, Conn>):
2218  match ips:
2219    case Nil{}:
2220      IO.pure(Result<&1, &1, Err, Conn>, Fail{ErrDns{}})
2221    case Con{addr, rest}:
2222      do IO<Result<&1, &1, Err, Conn>>:
2223        start : Nat <- IO.now()
2224        r : Result<&1, &1, U32 & String, Socket> <- conn.dial.all(port, ms, start, addr, rest)
2225        conn.made(ms, host, tls, cert, offer, r)
2226
2227def h2.header.skip(+name: String) -> Bool:
2228  match name:
2229    case SCon{Chr{58}, rest}:
2230      True{}
2231    case other:
2232      Bool.or(req.reserved(name),
2233        Bool.or(String.eq(name, "keep-alive"),
2234          Bool.or(String.eq(name, "proxy-connection"),
2235            Bool.or(String.eq(name, "upgrade"), String.eq(name, "te")))))
2236
2237def h2.header.mode(+name: String) -> U32:
2238  Bool.pick(U32,
2239    Bool.or(String.eq(name, "authorization"),
2240      Bool.or(String.eq(name, "cookie"), String.eq(name, "proxy-authorization"))),
2241    2, 0)
2242
2243def h2.header.values(+name: String, +mode: U32, vs: List<&2, String>) -> List<&2, Hpack.Field>:
2244  match vs:
2245    case Nil{}:
2246      Nil{}
2247    case Con{v, tail}:
2248      Hpack.Field{name, sanitize(v), mode} <> h2.header.values(name, mode, tail)
2249
2250def h2.header.tokens(vs: List<&2, String>) -> List<&2, String>:
2251  match vs:
2252    case Nil{}:
2253      Nil{}
2254    case Con{value, rest}:
2255      List.append(&2, String, String.split(value, ','), h2.header.tokens(rest))
2256
2257def h2.header.nominated.one(enabled: Bool, vs: List<&2, String>,
2258    rest: List<&2, String>) -> List<&2, String>:
2259  match enabled:
2260    case True{}:
2261      List.append(&2, String, h2.header.tokens(vs), rest)
2262    case False{}:
2263      rest
2264
2265def h2.header.nominated(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>) ->
2266    List<&2, String>:
2267  match xs:
2268    case Nil{}:
2269      Nil{}
2270    case (name, values) <> tail:
2271      h2.header.nominated.one(String.eq(String.to_lower(name), "connection"),
2272        values, h2.header.nominated(tail))
2273
2274def h2.header.has(xs: List<&2, String>, +key: String) -> Bool:
2275  match xs:
2276    case Nil{}:
2277      False{}
2278    case Con{value, rest}:
2279      Bool.or(String.eq(String.to_lower(trim(value)), key), h2.header.has(rest, key))
2280
2281def h2.header.item(skip: Bool, +name: String, vs: List<&2, String>,
2282    tail: List<&2, Hpack.Field>) -> List<&2, Hpack.Field>:
2283  match skip:
2284    case True{}:
2285      tail
2286    case False{}:
2287      List.append(&2, Hpack.Field, h2.header.values(name, h2.header.mode(name), vs), tail)
2288
2289def h2.header.items(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>,
2290    +nominated: List<&2, String>) -> List<&2, Hpack.Field>:
2291  match xs:
2292    case Nil{}:
2293      Nil{}
2294    case (name, values) <> tail:
2295      +key = String.to_lower(name)
2296      h2.header.item(Bool.or(h2.header.skip(key), h2.header.has(nominated, key)),
2297        key, values, h2.header.items(tail, nominated))
2298
2299def h2.request.fields(+method: String, target: String, authority: String,
2300    headers: Map<&2, List<&2, String>>) -> List<&2, Hpack.Field>:
2301  +xs = Map.to_list(&2, List<&2, String>, headers)
2302  List.append(&2, Hpack.Field,
2303    [Hpack.Field{":method", method, 0}, Hpack.Field{":scheme", "https", 0},
2304      Hpack.Field{":authority", authority, 0}, Hpack.Field{":path", target, 0}],
2305    h2.header.items(xs, h2.header.nominated(xs)))
2306
2307def h2.response.status.value(+value: String, valid: Bool) -> Maybe<&2, U32>:
2308  match valid:
2309    case False{}:
2310      None{}
2311    case True{}:
2312      parse_u32(value)
2313
2314def h2.response.status(xs: List<&2, Hpack.Field>) -> Maybe<&2, U32>:
2315  match xs:
2316    case Nil{}:
2317      None{}
2318    case Con{Hpack.Field{name, +value, mode}, tail}:
2319      match name:
2320        case ":status":
2321          h2.response.status.value(value, Nat.is_eq(String.length(value), 3n))
2322        case other:
2323          h2.response.status(tail)
2324
2325def h2.response.headers(xs: List<&2, Hpack.Field>, acc: Map<&2, List<&2, String>>) ->
2326    Map<&2, List<&2, String>>:
2327  match xs:
2328    case Nil{}:
2329      acc
2330    case Con{Hpack.Field{name, value, mode}, tail}:
2331      match name:
2332        case SCon{Chr{58}, rest}:
2333          h2.response.headers(tail, acc)
2334        case other:
2335          h2.response.headers(tail, add(acc, String.to_lower(name), value))
2336
2337def h2.response.final(interim: Bool, +status: U32, headers: List<&2, Hpack.Field>,
2338    body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2339  match interim:
2340    case True{}:
2341      Done{None{}}
2342    case False{}:
2343      HBytes.Bytes{len, buf} = body
2344      Done{Some{Res{status, h2.response.headers(headers, empty()), Bytes.Bytes{len, buf}}}}
2345
2346def h2.response.valid(valid: Bool, +status: U32, headers: List<&2, Hpack.Field>,
2347    body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2348  match valid:
2349    case False{}:
2350      Fail{ErrBad{}}
2351    case True{}:
2352      h2.response.final(U32.is_lt(status, 200), status, headers, body)
2353
2354def h2.response.parsed(m: Maybe<&2, U32>, headers: List<&2, Hpack.Field>,
2355    body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2356  match m:
2357    case None{}:
2358      Fail{ErrBad{}}
2359    case Some{+status}:
2360      h2.response.valid(Bool.and(U32.is_ge(status, 100), U32.is_lt(status, 600)),
2361        status, headers, body)
2362
2363def h2.response(+fields: List<&2, Hpack.Field>, body: HBytes.Bytes) ->
2364    Result<&1, &1, Err, Maybe<&1, Res>>:
2365  h2.response.parsed(h2.response.status(fields), fields, body)
2366
2367def h2.event.fold(acc: Result<&1, &1, Err, Maybe<&1, Res>>,
2368    event: H2.ClientEvent) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2369  match acc:
2370    case Fail{e}:
2371      Fail{e}
2372    case Done{Some{res}}:
2373      Done{Some{res}}
2374    case Done{None{}}:
2375      match event:
2376        case H2.Response{id, headers, body}:
2377          h2.response(headers, body)
2378        case H2.Reset{id, code}:
2379          Fail{ErrBad{}}
2380        case H2.Shutdown{last, code}:
2381          Done{None{}}
2382        case H2.Pong{data}:
2383          Done{None{}}
2384
2385def h2.send.report(r: Socket & Result<&1, &1, U32 & String, Unit>) ->
2386    IO(Result<&1, &1, Err, Socket>):
2387  (s, sent) = r
2388  match sent:
2389    case Fail{(+code, why)}:
2390      do IO<Result<&1, &1, Err, Socket>>:
2391        Wire.tls.close(s)
2392        return Fail{err.or_late(code, ErrWrite{code, why})}
2393    case Done{unit}:
2394      IO.pure(Result<&1, &1, Err, Socket>, Done{s})
2395
2396def h2.send.one(prev: Result<&1, &1, Err, Socket>, b: HBytes.Bytes) ->
2397    IO(Result<&1, &1, Err, Socket>):
2398  match prev:
2399    case Fail{e}:
2400      IO.pure(Result<&1, &1, Err, Socket>, Fail{e})
2401    case Done{s}:
2402      HBytes.Bytes{len, buf} = b
2403      do IO<Result<&1, &1, Err, Socket>>:
2404        sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.send.words(s, len, buf)
2405        h2.send.report(sent)
2406
2407def h2.send.fold(prev: IO(Result<&1, &1, Err, Socket>), b: HBytes.Bytes) ->
2408    IO(Result<&1, &1, Err, Socket>):
2409  do IO<Result<&1, &1, Err, Socket>>:
2410    r : Result<&1, &1, Err, Socket> <- prev
2411    h2.send.one(r, b)
2412
2413def h2.send(xs: List<&1, HBytes.Bytes>, s: Socket) -> IO(Result<&1, &1, Err, Socket>):
2414  List.foldl(~&1, ~HBytes.Bytes, ~IO(Result<&1, &1, Err, Socket>), ~h2.send.fold,
2415    xs, IO.pure(Result<&1, &1, Err, Socket>, Done{s}))
2416
2417def h2.received.step(over: Bool, s: Socket, client: H2.Client,
2418    +len: U32, buf: Array<U32>) -> H2Step:
2419  match over:
2420    case True{}:
2421      H2Reply{s, H2.Failed{H2.Error{1, True{}, 0}}}
2422    case False{}:
2423      H2Reply{s, H2.client.receive(client, HBytes.Bytes{len, buf})}
2424
2425def h2.fail(s: Socket, e: Err) -> IO(Result<&1, &1, Err, Conn & Res>):
2426  do IO<Result<&1, &1, Err, Conn & Res>>:
2427    Wire.tls.close(s)
2428    return Fail{e}
2429
2430def h2.loop(n: Nat, step: H2Step, +ms: U32, +used: U32) ->
2431    IO(Result<&1, &1, Err, Conn & Res>):
2432  match n:
2433    case 0n:
2434      match step:
2435        case H2Reply{s, reply}:
2436          h2.fail(s, ErrBad{})
2437        case H2Sent{client, events, sent}:
2438          match sent:
2439            case Fail{e}:
2440              IO.pure(Result<&1, &1, Err, Conn & Res>, Fail{e})
2441            case Done{s}:
2442              h2.fail(s, ErrBad{})
2443        case H2Events{s, client, result}:
2444          h2.fail(s, ErrBad{})
2445        case H2Received{client, answer}:
2446          (s, r) = answer
2447          h2.fail(s, ErrBad{})
2448    case 1n+p:
2449      match step:
2450        case H2Reply{s, reply}:
2451          match reply:
2452            case H2.Failed{error}:
2453              h2.fail(s, ErrBad{})
2454            case H2.Ready{client, writes, events}:
2455              do IO<Result<&1, &1, Err, Conn & Res>>:
2456                sent : Result<&1, &1, Err, Socket> <- h2.send(writes, s)
2457                h2.loop(p, H2Sent{client, events, sent}, ms, used)
2458        case H2Sent{client, events, sent}:
2459          match sent:
2460            case Fail{e}:
2461              IO.pure(Result<&1, &1, Err, Conn & Res>, Fail{e})
2462            case Done{s}:
2463              h2.loop(p, H2Events{s, client,
2464                List.foldl(~&1, ~H2.ClientEvent,
2465                  ~Result<&1, &1, Err, Maybe<&1, Res>>, ~h2.event.fold,
2466                  events, Done{None{}})}, ms, used)
2467        case H2Events{s, client, result}:
2468          match result:
2469            case Fail{e}:
2470              h2.fail(s, e)
2471            case Done{Some{res}}:
2472              IO.pure(Result<&1, &1, Err, Conn & Res>,
2473                Done{(ConnH2{s, client}, res)})
2474            case Done{None{}}:
2475              do IO<Result<&1, &1, Err, Conn & Res>>:
2476                r : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
2477                  Wire.tls.recv.words(s, 16384, ms)
2478                h2.loop(p, H2Received{client, r}, ms, used)
2479        case H2Received{client, answer}:
2480          match answer:
2481            case (s, Fail{(+code, why)}):
2482              h2.fail(s, err.or_late(code, ErrRead{code, why}))
2483            case (s, Done{(0, buf)}):
2484              h2.fail(s, ErrBad{})
2485            case (s, Done{(+len, buf)}):
2486              +total = (used + len : U32)
2487              h2.loop(p, h2.received.step(fetch.over(total), s, client, len, buf), ms, total)
2488
2489def h2.exchange(s: Socket, client: H2.Client, +ms: U32, request: Send) ->
2490    IO(Result<&1, &1, Err, Conn & Res>):
2491  Send{method, target, authority, headers, Bytes.Bytes{len, buf}} = request
2492  h2.loop(Nat.mul(4n, Nat.add(fetch.max(), 65536n)),
2493    H2Reply{s, H2.client.request(client,
2494      h2.request.fields(method, target, authority, headers), HBytes.Bytes{len, buf})},
2495    ms, 0)
2496
2497def conn.ex.h1(+tls: Bool, s: Socket, +ms: U32, request: Send) -> IO(Out):
2498  Send{+method, target, authority, headers, body} = request
2499  exchange.go(tls, ms, False{}, String.eq(method, "HEAD"), s,
2500    encode_req.on(method, target, authority, headers, body, False{}))
2501
2502# A socket with bytes past the response is out of step with the server, so it is closed.
2503def pool.keep.s(p: Pool, +key: String, +tls: Bool, res: Res, s: Socket, clean: Bool) -> IO(Pool & Result<&1, &1, Err, Res>):
2504  match clean:
2505    case True{}:
2506      do IO<Pool & Result<&1, &1, Err, Res>>:
2507        p2 : Pool <- pool.give(p, key, Conn{tls, s})
2508        return (p2, Done{res})
2509    case False{}:
2510      do IO<Pool & Result<&1, &1, Err, Res>>:
2511        io.close(tls, s)
2512        return (p, Done{res})
2513
2514def pool.keep.m(p: Pool, +key: String, +tls: Bool, res: Res, +clean: Bool, sock: Maybe<&1, Socket>) -> IO(Pool & Result<&1, &1, Err, Res>):
2515  match sock:
2516    case None{}:
2517      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Done{res}))
2518    case Some{s}:
2519      pool.keep.s(p, key, tls, res, s, clean)
2520
2521def pool.keep(p: Pool, +key: String, +tls: Bool, res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
2522  Bytes.Bytes{+len, buf} = rest
2523  pool.keep.m(p, key, tls, res, U32.is_zero(len), sock)
2524
2525def pool.after(p: Pool, +key: String, +tls: Bool, o: Out) -> IO(Pool & Result<&1, &1, Err, Res>):
2526  match o:
2527    case OutFail{e, none}:
2528      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2529    case OutDone{res, sock, rest}:
2530      pool.keep(p, key, tls, res, sock, rest)
2531
2532def pool.h2.reusable(c: Conn) -> Bool & Conn:
2533  match c:
2534    case Conn{tls, s}:
2535      (True{}, Conn{tls, s})
2536    case ConnH2{s, H2.Client{input, streams, encoder, decoder, +control}}:
2537      H2.Control{next, active, frame_max, initial, max_streams, send_window,
2538        recv_window, first, ack, continuation, +goaway} = control
2539      (Maybe.is_none(&2, U32, goaway),
2540        ConnH2{s, H2.Client{input, streams, encoder, decoder, control}})
2541
2542def pool.h2.keep(p: Pool, +key: String, res: Res, state: Bool & Conn) ->
2543    IO(Pool & Result<&1, &1, Err, Res>):
2544  (reusable, c) = state
2545  match reusable:
2546    case True{}:
2547      do IO<Pool & Result<&1, &1, Err, Res>>:
2548        next : Pool <- pool.give(p, key, c)
2549        return (next, Done{res})
2550    case False{}:
2551      do IO<Pool & Result<&1, &1, Err, Res>>:
2552        conn.close(c)
2553        return (p, Done{res})
2554
2555def pool.h2.result(p: Pool, +key: String, r: Result<&1, &1, Err, Conn & Res>) ->
2556    IO(Pool & Result<&1, &1, Err, Res>):
2557  match r:
2558    case Fail{e}:
2559      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2560    case Done{(c, res)}:
2561      pool.h2.keep(p, key, res, pool.h2.reusable(c))
2562
2563def pool.h2.ex(p: Pool, +key: String, +ms: U32, request: Send,
2564    s: Socket, client: H2.Client) -> IO(Pool & Result<&1, &1, Err, Res>):
2565  do IO<Pool & Result<&1, &1, Err, Res>>:
2566    r : Result<&1, &1, Err, Conn & Res> <- h2.exchange(s, client, ms, request)
2567    pool.h2.result(p, key, r)
2568
2569def pool.fresh.conn(p: Pool, +key: String, +ms: U32, request: Send,
2570    r: Result<&1, &1, Err, Conn>) -> IO(Pool & Result<&1, &1, Err, Res>):
2571  match r:
2572    case Fail{e}:
2573      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2574    case Done{c}:
2575      match c:
2576        case Conn{+tls, s}:
2577          do IO<Pool & Result<&1, &1, Err, Res>>:
2578            o : Out <- conn.ex.h1(tls, s, ms, request)
2579            pool.after(p, key, tls, o)
2580        case ConnH2{s, client}:
2581          pool.h2.ex(p, key, ms, request, s, client)
2582
2583def pool.fresh(p: Pool, +key: String, +tls: Bool, +ms: U32, +host: String,
2584    +port: U32, request: Send, cert: Maybe<&2, Cert>) ->
2585    IO(Pool & Result<&1, &1, Err, Res>):
2586  do IO<Pool & Result<&1, &1, Err, Res>>:
2587    ips : List<&2, String> <- Dns.resolve.all(host)
2588    c : Result<&1, &1, Err, Conn> <- conn.open.all(tls, ms, host, port, ips, cert, True{})
2589    pool.fresh.conn(p, key, ms, request, c)
2590
2591# A reused socket the server already closed fails before any response byte.
2592def pool.retry(+none: Bool, +idem: Bool) -> Bool:
2593  Bool.and(none, idem)
2594
2595def pool.stale(p: Pool, +key: String, +tls: Bool, +ms: U32, +host: String,
2596    +port: U32, request: Send, e: Err, again: Bool, cert: Maybe<&2, Cert>) ->
2597    IO(Pool & Result<&1, &1, Err, Res>):
2598  match again:
2599    case True{}:
2600      pool.fresh(p, key, tls, ms, host, port, request, cert)
2601    case False{}:
2602      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2603
2604def pool.reused(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2605    +host: String, +port: U32, spare: Send, o: Out, cert: Maybe<&2, Cert>) ->
2606    IO(Pool & Result<&1, &1, Err, Res>):
2607  match o:
2608    case OutFail{e, +none}:
2609      pool.stale(p, key, tls, ms, host, port, spare, e, pool.retry(none, idem), cert)
2610    case OutDone{res, sock, rest}:
2611      pool.keep(p, key, tls, res, sock, rest)
2612
2613# Copy only the reused HTTP/1.1 request body, for a stale-socket retry.
2614def pool.idle.h1.bodies(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2615    +host: String, +port: U32, s: Socket, +method: String, +target: String,
2616    +authority: String, +headers: Map<&2, List<&2, String>>,
2617    r: Bytes.Bytes & Bytes.Bytes, cert: Maybe<&2, Cert>) ->
2618    IO(Pool & Result<&1, &1, Err, Res>):
2619  (wire, spare) = r
2620  do IO<Pool & Result<&1, &1, Err, Res>>:
2621    o : Out <- conn.ex.h1(tls, s, ms, Send{method, target, authority, headers, wire})
2622    pool.reused(p, key, tls, ms, idem, host, port,
2623      Send{method, target, authority, headers, spare}, o, cert)
2624
2625def pool.idle.h1(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2626    +host: String, +port: U32, s: Socket, request: Send, cert: Maybe<&2, Cert>) ->
2627    IO(Pool & Result<&1, &1, Err, Res>):
2628  Send{+method, +target, +authority, +headers, body} = request
2629  pool.idle.h1.bodies(p, key, tls, ms, idem, host, port, s, method, target,
2630    authority, headers, Bytes.slice(body, 0, 4294967295), cert)
2631
2632def pool.idle.reuse(p: Pool, +key: String, +ms: U32, +idem: Bool,
2633    +host: String, +port: U32, c: Conn, request: Send,
2634    cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2635  match c:
2636    case Conn{tls, s}:
2637      pool.idle.h1(p, key, tls, ms, idem, host, port, s, request, cert)
2638    case ConnH2{s, client}:
2639      pool.h2.ex(p, key, ms, request, s, client)
2640
2641def pool.idle(taken: Pool & Maybe<&1, Conn>, +key: String, +tls: Bool, +ms: U32,
2642    +idem: Bool, +host: String, +port: U32, request: Send, cert: Maybe<&2, Cert>) ->
2643    IO(Pool & Result<&1, &1, Err, Res>):
2644  (p, m) = taken
2645  match m:
2646    case None{}:
2647      pool.fresh(p, key, tls, ms, host, port, request, cert)
2648    case Some{c}:
2649      pool.idle.reuse(p, key, ms, idem, host, port, c, request, cert)
2650
2651def pool.origin(p: Pool, +method: String, +ms: U32,
2652    headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +hf: String,
2653    a: Url.Abs, known: Bool, +cert: Maybe<&2, Cert>) ->
2654    IO(Pool & Result<&1, &1, Err, Res>):
2655  Url.Abs{+scheme, +host, +port, target} = a
2656  match known:
2657    case False{}:
2658      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrUrl{}}))
2659    case True{}:
2660      +key = pool.key.cert(pool.key(scheme, host, port), cert)
2661      pool.idle(pool.take(p, key), key, String.eq(scheme, "https"), ms,
2662        pool.idempotent(method), host, port, Send{method, target, hf, headers, body}, cert)
2663
2664def pool.scheme.ok(a: Url.Abs) -> Bool:
2665  Url.Abs{+scheme, host, port, target} = a
2666  Bool.or(String.eq(scheme, "http"), String.eq(scheme, "https"))
2667
2668def pool.one.back(h: Hop, pr: Pool & Result<&1, &1, Err, Res>) -> Pool & Result<&1, &1, Err, Res> & Hop:
2669  (p, r) = pr
2670  (p, r, h)
2671
2672def pool.one.of(p: Pool, +method: String, +url: Url.Abs, +headers: Map<&2, List<&2, String>>, +ms: U32, r: Bytes.Bytes & Bytes.Bytes, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
2673  (body, wire) = r
2674  do IO<Pool & Result<&1, &1, Err, Res> & Hop>:
2675    pr : Pool & Result<&1, &1, Err, Res> <- pool.origin(p, method, ms, headers, wire, Url.host_field(url), url, pool.scheme.ok(url), cert)
2676    return pool.one.back(Hop{method, url, headers, body}, pr)
2677
2678# One request, on an idle socket to its origin when the pool has one. The hop comes back for the redirect.
2679def pool.one(p: Pool, h: Hop, +ms: U32, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
2680  Hop{+method, +url, +headers, body} = h
2681  pool.one.of(p, method, url, headers, ms, Bytes.slice(body, 0, 4294967295), cert)
2682
2683type Next is Type:
2684  NDone{res: Result<&1, &1, Err, Res>}
2685  NStop{}
2686  NGo{left: Nat, hop: Hop}
2687
2688type Mode is Data:
2689  ModeFollow{}
2690  ModeManual{}
2691  ModeError{}
2692
2693# left: redirects still allowed after the request we just finished.
2694def fetch.hop(left: Nat, h: Hop) -> Next:
2695  match left:
2696    case 0n:
2697      NStop{}
2698    case 1n+p:
2699      NGo{p, h}
2700
2701def fetch.decide.r(left: Nat, r: Res, next: Maybe<&1, Hop>) -> Next:
2702  match next:
2703    case None{}:
2704      NDone{Done{r}}
2705    case Some{h}:
2706      fetch.hop(left, h)
2707
2708def fetch.decide.res(left: Nat, h: Hop, r: Res) -> Next:
2709  Res{+status, +headers, body} = r
2710  fetch.decide.r(left, Res{status, headers, body}, redirect(status, headers, h))
2711
2712def fetch.decide(left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2713  match m:
2714    case Fail{e}:
2715      NDone{Fail{e}}
2716    case Done{r}:
2717      fetch.decide.res(left, h, r)
2718
2719def fetch.error.res(r: Res, bad: Bool) -> Next:
2720  match bad:
2721    case True{}:
2722      NDone{Fail{ErrRedirect{}}}
2723    case False{}:
2724      NDone{Done{r}}
2725
2726def fetch.error(h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2727  match m:
2728    case Fail{e}:
2729      NDone{Fail{e}}
2730    case Done{r}:
2731      Res{+status, +headers, body} = r
2732      fetch.error.res(Res{status, headers, body}, Bool.and(redirect.code(status), has_header(headers, "location")))
2733
2734def fetch.policy(mode: Mode, left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2735  match mode:
2736    case ModeFollow{}:
2737      fetch.decide(left, h, m)
2738    case ModeManual{}:
2739      NDone{m}
2740    case ModeError{}:
2741      fetch.error(h, m)
2742
2743# A caller's own Accept-Encoding wins; enc is the codings fetch can undo.
2744def accept.enc(+h: Map<&2, List<&2, String>>, +enc: String) -> Map<&2, List<&2, String>>:
2745  Bool.pick(Map<&2, List<&2, String>>, has_header(h, "accept-encoding"), h, set(h, "accept-encoding", enc))
2746
2747def fetch.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>, +enc: String) -> Next:
2748  match u:
2749    case None{}:
2750      NDone{Fail{ErrUrl{}}}
2751    case Some{a}:
2752      NGo{20n, Hop{method, a, accept.enc(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), enc), body}}
2753
2754def pool.next.move(p: Pool, +old: String, cert: Maybe<&2, Cert>, n: Next) -> Pool & Next & Maybe<&2, Cert>:
2755  match n:
2756    case NGo{left, h}:
2757      Hop{method, +url, headers, body} = h
2758      (p, NGo{left, Hop{method, url, headers, body}},
2759        Bool.pick(Maybe<&2, Cert>, String.eq(old, redirect.origin(url)), cert, None{}))
2760    case NDone{r}:
2761      (p, NDone{r}, None{})
2762    case NStop{}:
2763      (p, NStop{}, None{})
2764
2765def pool.next(+mode: Mode, left: Nat, cert: Maybe<&2, Cert>, x: Pool & Result<&1, &1, Err, Res> & Hop) -> Pool & Next & Maybe<&2, Cert>:
2766  (p, m, h) = x
2767  Hop{method, +url, headers, body} = h
2768  pool.next.move(p, redirect.origin(url), cert, fetch.policy(mode, left, Hop{method, url, headers, body}, m))
2769
2770def pool.hops.one(+mode: Mode, +ms: U32, +cert: Maybe<&2, Cert>, p: Pool, h: Hop, left: Nat) -> IO(Pool & Next & Maybe<&2, Cert>):
2771  do IO<Pool & Next & Maybe<&2, Cert>>:
2772    x : Pool & Result<&1, &1, Err, Res> & Hop <- pool.one(p, h, ms, cert)
2773    return pool.next(mode, left, cert, x)
2774
2775# NGo.left is how many redirects may follow this request. 20 is WHATWG's limit.
2776@unsafe
2777def pool.hops(+mode: Mode, +ms: U32, st: Pool & Next & Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2778  (p, n, cert) = st
2779  match n:
2780    case NDone{m}:
2781      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, m))
2782    case NStop{}:
2783      IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrRedirect{}}))
2784    case NGo{+left, h}:
2785      do IO<Pool & Result<&1, &1, Err, Res>>:
2786        next : Pool & Next & Maybe<&2, Cert> <- pool.hops.one(mode, ms, cert, p, h, left)
2787        pool.hops(mode, ms, next)
2788
2789# Content-Encoding (RFC 9110 §8.4): each value, trimmed and lowercased, in the order applied.
2790def ce.keep(+w: String, +rest: List<&2, String>) -> List<&2, String>:
2791  Bool.pick(List<&2, String>, String.is_empty(w), rest, Con{w, rest})
2792
2793def ce.norm(xs: List<&2, String>) -> List<&2, String>:
2794  match xs:
2795    case Nil{}:
2796      Nil{}
2797    case Con{v, t}:
2798      ce.keep(String.to_lower(trim(v)), ce.norm(t))
2799
2800def ce.split(xs: List<&2, String>) -> List<&2, String>:
2801  match xs:
2802    case Nil{}:
2803      Nil{}
2804    case Con{v, t}:
2805      List.append(&2, String, ce.norm(String.split(v, ',')), ce.split(t))
2806
2807# Ok: decoded so far. Bad: a coding failed. Skip: a coding we cannot decode, so the body stays as sent.
2808type Dec is Data:
2809  DecOk{b: String}
2810  DecBad{}
2811  DecSkip{}
2812
2813def ce.of(m: Maybe<&2, String>) -> Dec:
2814  match m:
2815    case None{}:
2816      DecBad{}
2817    case Some{b}:
2818      DecOk{b}
2819
2820# Servers send deflate both with and without the zlib wrapper.
2821def ce.deflate(+b: String, m: Maybe<&2, String>) -> Dec:
2822  match m:
2823    case Some{out}:
2824      DecOk{out}
2825    case None{}:
2826      ce.of(Zlib.inflate(b))
2827
2828def ce.apply(+c: String, +b: String) -> Dec:
2829  Bool.pick(Dec, Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), ce.of(Zlib.gunzip(b)),
2830    Bool.pick(Dec, String.eq(c, "deflate"), ce.deflate(b, Zlib.unzlib(b)),
2831      Bool.pick(Dec, String.eq(c, "identity"), DecOk{b}, DecSkip{})))
2832
2833def ce.go(cs: List<&2, String>, d: Dec) -> Dec:
2834  match cs:
2835    case Nil{}:
2836      d
2837    case Con{+c, t}:
2838      match d:
2839        case DecOk{+b}:
2840          ce.go(t, ce.apply(c, b))
2841        case DecBad{}:
2842          DecBad{}
2843        case DecSkip{}:
2844          DecSkip{}
2845
2846def decoded.pick(d: Dec, +status: U32, headers: Map<&2, List<&2, String>>, body: String) -> Result<&1, &1, Err, Res>:
2847  match d:
2848    case DecOk{b}:
2849      Done{Res{status, headers, Bytes.from_string(b)}}
2850    case DecBad{}:
2851      Fail{ErrBad{}}
2852    case DecSkip{}:
2853      Done{Res{status, headers, Bytes.from_string(body)}}
2854
2855# ponytail: the codings run on a String copy of the body; give zlib a Bytes input if gzip bodies get big.
2856def decoded.cs(+status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, cs: List<&2, String>) -> Result<&1, &1, Err, Res>:
2857  match cs:
2858    case Nil{}:
2859      Done{Res{status, headers, body}}
2860    case Con{c, t}:
2861      +s = Bytes.to_string(body)
2862      decoded.pick(ce.go(Con{c, t}, DecOk{s}), status, headers, s)
2863
2864def decoded.go(empty: Bool, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Result<&1, &1, Err, Res>:
2865  match empty:
2866    case True{}:
2867      Done{Res{status, headers, body}}
2868    case False{}:
2869      decoded.cs(status, headers, body, List.reverse(&2, String, ce.split(fields(headers, "content-encoding"))))
2870
2871# The body decoded per Content-Encoding; the headers stay as sent. A corrupt body is ErrBad.
2872def decoded(res: Res) -> Result<&1, &1, Err, Res>:
2873  Res{+status, +headers, body} = res
2874  Bytes.Bytes{+len, buf} = body
2875  decoded.go(U32.is_zero(len), status, headers, Bytes.Bytes{len, buf})
2876
2877def decoded.m(r: Result<&1, &1, Err, Res>) -> Maybe<&1, Res>:
2878  match r:
2879    case Done{x}:
2880      Some{x}
2881    case Fail{e}:
2882      None{}
2883
2884def decoded.some(res: Res) -> Maybe<&1, Res>:
2885  decoded.m(decoded(res))
2886
2887def ce.words(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Maybe<&1, Bytes.Bytes>:
2888  match r:
2889    case Fail{e}:
2890      None{}
2891    case Done{(+len, buf)}:
2892      Some{Bytes.Bytes{len, buf}}
2893
2894# A decoded body stops at 16 MiB, like a received one.
2895def ce.eff(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2896  Bytes.Bytes{+len, buf} = b
2897  do IO<Maybe<&1, Bytes.Bytes>>:
2898    r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(16777216, len, buf)
2899    return ce.words(r)
2900
2901def ce.dec(d: Dec) -> Maybe<&1, Bytes.Bytes>:
2902  match d:
2903    case DecOk{b}:
2904      Some{Bytes.from_string(b)}
2905    case DecBad{}:
2906      None{}
2907    case DecSkip{}:
2908      None{}
2909
2910# ponytail: deflate runs on the pure decoder, which also takes raw DEFLATE; servers rarely send it.
2911def ce.io.deflate(on: Bool, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2912  match on:
2913    case True{}:
2914      +s = Bytes.to_string(b)
2915      IO.pure(Maybe<&1, Bytes.Bytes>, ce.dec(ce.deflate(s, Zlib.unzlib(s))))
2916    case False{}:
2917      IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
2918
2919def ce.io.zstd(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2920  match on:
2921    case True{}:
2922      ce.eff(~Zlib.zstd.words, b)
2923    case False{}:
2924      ce.io.deflate(String.eq(c, "deflate"), b)
2925
2926def ce.io.br(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2927  match on:
2928    case True{}:
2929      ce.eff(~Zlib.brotli.words, b)
2930    case False{}:
2931      ce.io.zstd(String.eq(c, "zstd"), c, b)
2932
2933# One known coding undone: gzip, x-gzip, br, zstd, deflate, or identity.
2934def ce.io.gz(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2935  match on:
2936    case True{}:
2937      ce.eff(~Zlib.inflate.words, b)
2938    case False{}:
2939      ce.io.br(String.eq(c, "br"), c, b)
2940
2941def ce.io.go(cs: List<&2, String>, m: Maybe<&1, Bytes.Bytes>) -> IO(Maybe<&1, Bytes.Bytes>):
2942  match cs:
2943    case Nil{}:
2944      match m:
2945        case None{}:
2946          IO.pure(Maybe<&1, Bytes.Bytes>, None{})
2947        case Some{b}:
2948          IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
2949    case Con{+c, t}:
2950      match m:
2951        case None{}:
2952          IO.pure(Maybe<&1, Bytes.Bytes>, None{})
2953        case Some{b}:
2954          do IO<Maybe<&1, Bytes.Bytes>>:
2955            n : Maybe<&1, Bytes.Bytes> <- ce.io.gz(Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), c, b)
2956            ce.io.go(t, n)
2957
2958def ce.has(xs: List<&2, String>, +c: String) -> Bool:
2959  match xs:
2960    case Nil{}:
2961      False{}
2962    case Con{x, t}:
2963      Bool.or(String.eq(c, x), ce.has(t, c))
2964
2965def ce.known(cs: List<&2, String>, +ok: List<&2, String>) -> Bool:
2966  match cs:
2967    case Nil{}:
2968      True{}
2969    case Con{c, t}:
2970      Bool.and(ce.has(ok, c), ce.known(t, ok))
2971
2972def decoded.io.pick(m: Maybe<&1, Bytes.Bytes>, +status: U32, headers: Map<&2, List<&2, String>>) -> Result<&1, &1, Err, Res>:
2973  match m:
2974    case Some{b}:
2975      Done{Res{status, headers, b}}
2976    case None{}:
2977      Fail{ErrBad{}}
2978
2979def decoded.io.run(known: Bool, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, cs: List<&2, String>) -> IO(Result<&1, &1, Err, Res>):
2980  match known:
2981    case True{}:
2982      do IO<Result<&1, &1, Err, Res>>:
2983        m : Maybe<&1, Bytes.Bytes> <- ce.io.go(cs, Some{body})
2984        return decoded.io.pick(m, status, headers)
2985    case False{}:
2986      IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
2987
2988def decoded.io.go(empty: Bool, +enc: String, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
2989  match empty:
2990    case True{}:
2991      IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
2992    case False{}:
2993      +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
2994      decoded.io.run(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}), status, headers, body, cs)
2995
2996# decoded through the C libraries, for the codings in enc. A body with any other coding stays as sent.
2997def decoded.io(+enc: String, res: Res) -> IO(Result<&1, &1, Err, Res>):
2998  Res{+status, +headers, body} = res
2999  Bytes.Bytes{+len, buf} = body
3000  decoded.io.go(U32.is_zero(len), enc, status, headers, Bytes.Bytes{len, buf})
3001
3002# An effect on empty input fails with ENOENT only when its library does not load.
3003def codings.ok(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Bool:
3004  match r:
3005    case Fail{(+c, why)}:
3006      Bool.not(U32.is_eq(c, 2))
3007    case Done{p}:
3008      True{}
3009
3010def codings.has(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Bool):
3011  Bytes.Bytes{+len, buf} = b
3012  do IO<Bool>:
3013    r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(0, len, buf)
3014    return codings.ok(r)
3015
3016def codings.add(has: Bool, +enc: String, +c: String) -> String:
3017  Bool.pick(String, has, enc ++ ", " ++ c, enc)
3018
3019# gzip and deflate, then br and zstd when their C library loads.
3020def codings() -> IO(String):
3021  do IO<String>:
3022    b : Bool <- codings.has(~Zlib.brotli.words, Bytes.new(0))
3023    z : Bool <- codings.has(~Zlib.zstd.words, Bytes.new(0))
3024    return codings.add(z, codings.add(b, "gzip, deflate", "br"), "zstd")
3025
3026# The final response of a fetch, after redirects.
3027def fetch.final(+enc: String, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
3028  match r:
3029    case Done{res}:
3030      decoded.io(enc, res)
3031    case Fail{e}:
3032      IO.pure(Result<&1, &1, Err, Res>, Fail{e})
3033
3034def pool.final(+enc: String, pr: Pool & Result<&1, &1, Err, Res>) -> IO(Pool & Result<&1, &1, Err, Res>):
3035  (p, r) = pr
3036  do IO<Pool & Result<&1, &1, Err, Res>>:
3037    d : Result<&1, &1, Err, Res> <- fetch.final(enc, r)
3038    return (p, d)
3039
3040def pool.how.enc(+enc: String, p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32, mode: Mode, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
3041  do IO<Pool & Result<&1, &1, Err, Res>>:
3042    pr : Pool & Result<&1, &1, Err, Res> <- pool.hops(mode, ms, (p, fetch.start(method, headers, body, Url.absolute(url), enc), cert))
3043    pool.final(enc, pr)
3044
3045def pool.how.cert(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32, mode: Mode, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
3046  do IO<Pool & Result<&1, &1, Err, Res>>:
3047    enc : String <- codings()
3048    pool.how.enc(enc, p, method, url, headers, body, ms, mode, cert)
3049
3050# pool.how(p, "GET", "https://example.com/x?y=1", headers, body, ms, mode) follows redirects
3051# on p's idle sockets. Fail is a bad URL, a failed lookup, connect, handshake, send, read,
3052# a malformed response, more than 20 redirects, or a step past ms. Bodies are bytes.
3053def pool.how(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32, mode: Mode) -> IO(Pool & Result<&1, &1, Err, Res>):
3054  pool.how.cert(p, method, url, headers, body, ms, mode, None{})
3055
3056def pool.fetch.with(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32) -> IO(Pool & Result<&1, &1, Err, Res>):
3057  pool.how(p, method, url, headers, body, ms, ModeFollow{})
3058
3059def pool.fetch(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
3060  pool.fetch.with(p, method, url, headers, body, 30000)
3061
3062def pool.fetch.cert.with(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, chain: String, key: String, ms: U32) -> IO(Pool & Result<&1, &1, Err, Res>):
3063  pool.how.cert(p, method, url, headers, body, ms, ModeFollow{}, Some{Cert{chain, key}})
3064
3065def pool.fetch.cert(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, chain: String, key: String) -> IO(Pool & Result<&1, &1, Err, Res>):
3066  pool.fetch.cert.with(p, method, url, headers, body, chain, key, 30000)
3067
3068def fetch.end(pr: Pool & Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
3069  (p, r) = pr
3070  do IO<Result<&1, &1, Err, Res>>:
3071    pool.close(p)
3072    return r
3073
3074# fetch is pool.how on a fresh pool that closes afterwards.
3075def fetch.how(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32, mode: Mode) -> IO(Result<&1, &1, Err, Res>):
3076  do IO<Result<&1, &1, Err, Res>>:
3077    pr : Pool & Result<&1, &1, Err, Res> <- pool.how(pool.new(), method, url, headers, body, ms, mode)
3078    fetch.end(pr)
3079
3080def fetch.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32) -> IO(Result<&1, &1, Err, Res>):
3081  fetch.how(method, url, headers, body, ms, ModeFollow{})
3082
3083def fetch.cert.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, chain: String, key: String, ms: U32) -> IO(Result<&1, &1, Err, Res>):
3084  do IO<Result<&1, &1, Err, Res>>:
3085    pr : Pool & Result<&1, &1, Err, Res> <- pool.fetch.cert.with(pool.new(), method, url, headers, body, chain, key, ms)
3086    fetch.end(pr)
3087
3088def fetch.cert(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, chain: String, key: String) -> IO(Result<&1, &1, Err, Res>):
3089  fetch.cert.with(method, url, headers, body, chain, key, 30000)
3090
3091# fetch.with and a 30 s step timeout.
3092def fetch(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
3093  fetch.with(method, url, headers, body, 30000)
3094
3095def get(url: String) -> IO(Result<&1, &1, Err, Res>):
3096  fetch("GET", url, empty(), Bytes.new(0))
3097
3098# POST v as compact JSON, with content-type: application/json.
3099def post.json(url: String, v: Json.Val) -> IO(Result<&1, &1, Err, Res>):
3100  fetch("POST", url, set(empty(), "content-type", "application/json"), Json.encode.bytes(v))
3101
3102# Base URLs: resolve(base, ref) is ref against the absolute http(s) URL base (RFC 3986 §5.2),
3103# written back as a URL for fetch. None when base is not absolute or ref has another scheme.
3104def resolve.show(a: Url.Abs) -> String:
3105  Url.Abs{+scheme, host, port, +target} = a
3106  scheme ++ "://" ++ Url.host_field(Url.Abs{scheme, host, port, target}) ++ target
3107
3108def resolve.to(m: Maybe<&2, Url.Abs>) -> Maybe<&2, String>:
3109  match m:
3110    case None{}:
3111      None{}
3112    case Some{a}:
3113      Some{resolve.show(a)}
3114
3115def resolve.base(m: Maybe<&2, Url.Abs>, +ref: String) -> Maybe<&2, String>:
3116  match m:
3117    case None{}:
3118      None{}
3119    case Some{b}:
3120      resolve.to(Url.resolve(b, ref))
3121
3122def resolve(base: String, +ref: String) -> Maybe<&2, String>:
3123  resolve.base(Url.absolute(base), ref)
3124
3125# Retry. The wait before retry n (0 first) is 500 ms doubled n times, at most 30 s;
3126# its upper half is jitter r: backoff(n, r) = half + r mod (half + 1).
3127def retry.cap() -> U32:
3128  30000
3129
3130def retry.base(n: Nat) -> U32:
3131  match n:
3132    case 0n:
3133      500
3134    case 1n+p:
3135      U32.min((retry.base(p) * 2 : U32), retry.cap())
3136
3137def retry.backoff.half(+half: U32, +r: U32) -> U32:
3138  (half + (r % (half + 1)) : U32)
3139
3140def retry.backoff(n: Nat, +r: U32) -> U32:
3141  retry.backoff.half((retry.base(n) / 2 : U32), r)
3142
3143# ms clamped to 0 .. retry.cap().
3144def retry.after.ms(+ms: Int.I64) -> U32:
3145  Bool.pick(U32, Int.I64.is_neg(ms), 0,
3146    Bool.pick(U32, Int.I64.is_lt(ms, Int.I64.from_u32(retry.cap())), Int.I64.to_u32(ms), retry.cap()))
3147
3148def retry.after.date(m: Maybe<&2, Time.Instant>, now: Time.Instant) -> Maybe<&2, U32>:
3149  match m:
3150    case None{}:
3151      None{}
3152    case Some{date}:
3153      Some{retry.after.ms(Time.Duration.to_ms(Time.Instant.since(date, now)))}
3154
3155# More than 5 digits is past the cap, and would overflow parse_u32.
3156def retry.after.secs(+v: String, now: Time.Instant, n: Maybe<&2, U32>) -> Maybe<&2, U32>:
3157  match n:
3158    case None{}:
3159      retry.after.date(Time.http_date.parse(v), now)
3160    case Some{s}:
3161      Some{Bool.pick(U32, Nat.is_lt(5n, String.length(v)), retry.cap(), U32.min((s * 1000 : U32), retry.cap()))}
3162
3163# Retry-After (RFC 9110 §10.2.3) as ms from now, at most retry.cap(): delay-seconds, or an
3164# HTTP-date (a past date is 0). None when v is empty or neither form.
3165def retry.after(+v: String, now: Time.Instant) -> Maybe<&2, U32>:
3166  retry.after.secs(v, now, parse_u32(v))
3167
3168def retry.wait(m: Maybe<&2, U32>, n: Nat, +r: U32) -> U32:
3169  match m:
3170    case None{}:
3171      retry.backoff(n, r)
3172    case Some{ms}:
3173      ms
3174
3175# The wait before retry n: Retry-After v when it reads as a delay, else backoff with jitter r.
3176def retry.delay(+v: String, now: Time.Instant, n: Nat, +r: U32) -> U32:
3177  retry.wait(retry.after(v, now), n, r)
3178
3179# Statuses a later try may clear.
3180def retry.status(+s: U32) -> Bool:
3181  Bool.or(Bool.or(U32.is_eq(s, 408), U32.is_eq(s, 429)),
3182    Bool.or(Bool.or(U32.is_eq(s, 500), U32.is_eq(s, 502)), Bool.or(U32.is_eq(s, 503), U32.is_eq(s, 504))))
3183
3184# A refused connect or a timeout may clear; any other error would repeat.
3185def retry.fail(e: Err) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3186  match e:
3187    case ErrConnect{code, why}:
3188      (Fail{ErrConnect{code, why}}, Some{""})
3189    case ErrTimeout{}:
3190      (Fail{ErrTimeout{}}, Some{""})
3191    case other:
3192      (Fail{other}, None{})
3193
3194def retry.res(res: Res) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3195  Res{+status, +headers, body} = res
3196  (Done{Res{status, headers, body}}, Bool.pick(Maybe<&2, String>, retry.status(status), Some{header(headers, "retry-after")}, None{}))
3197
3198def retry.judge.try(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3199  match r:
3200    case Fail{e}:
3201      retry.fail(e)
3202    case Done{res}:
3203      retry.res(res)
3204
3205# One try, judged: the result as it came, and Some{Retry-After value} ("" when absent)
3206# when an idempotent request may try again.
3207def retry.judge(idem: Bool, r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3208  match idem:
3209    case False{}:
3210      (r, None{})
3211    case True{}:
3212      retry.judge.try(r)
3213
3214# ponytail: a failed random source gives jitter 0, so the wait is the lower half.
3215def retry.jitter(r: Result<&1, &1, U32 & String, U32>) -> U32:
3216  match r:
3217    case Fail{e}:
3218      0
3219    case Done{x}:
3220      x
3221
3222def retry.sleep(+v: String, n: Nat) -> IO(Unit):
3223  do IO<Unit>:
3224    now : Time.Instant <- Time.now()
3225    rnd : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
3226    IO.sleep(retry.delay(v, now, n, retry.jitter(rnd)))
3227
3228def retry.kept(body: Bytes.Bytes, j: Result<&1, &1, Err, Res> & Maybe<&2, String>) -> Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>:
3229  (r, m) = j
3230  (body, r, m)
3231
3232# One fetch of the copy; the body comes back for the next try.
3233def retry.one(+idem: Bool, +method: String, +url: String, +headers: Map<&2, List<&2, String>>,
3234    r: Bytes.Bytes & Bytes.Bytes) -> IO(Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>):
3235  (body, spare) = r
3236  do IO<Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>>:
3237    got : Result<&1, &1, Err, Res> <- fetch(method, url, headers, spare)
3238    return retry.kept(body, retry.judge(idem, got))
3239
3240# left: retries still allowed. n: the retry to wait for next, 0 first.
3241def retry.go(left: Nat, +n: Nat, +idem: Bool, +method: String, +url: String,
3242    +headers: Map<&2, List<&2, String>>,
3243    t: Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>) -> IO(Result<&1, &1, Err, Res>):
3244  match left:
3245    case 0n:
3246      (body, r, m) = t
3247      IO.pure(Result<&1, &1, Err, Res>, r)
3248    case 1n+p:
3249      (body, r, m) = t
3250      match m:
3251        case None{}:
3252          IO.pure(Result<&1, &1, Err, Res>, r)
3253        case Some{v}:
3254          do IO<Result<&1, &1, Err, Res>>:
3255            retry.sleep(v, n)
3256            tried : Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String> <-
3257              retry.one(idem, method, url, headers, Bytes.slice(body, 0, 4294967295))
3258            retry.go(p, 1n+n, idem, method, url, headers, tried)
3259
3260# fetch.retry(n, method, url, headers, body) is fetch, tried again up to n times while an
3261# idempotent method (GET, HEAD, OPTIONS, TRACE, PUT, DELETE) gets a connect error, a timeout,
3262# or 408, 429, 500, 502, 503, or 504. POST, PATCH and other methods get one try. It waits
3263# Retry-After (seconds or HTTP-date, at most 30 s) when given, else the backoff. When retries
3264# run out, the last response or error comes back as it was.
3265def retry.start(enabled: Bool, n: U32, +method: String, +url: String,
3266    +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) ->
3267    IO(Result<&1, &1, Err, Res>):
3268  match enabled:
3269    case False{}:
3270      fetch(method, url, headers, body)
3271    case True{}:
3272      do IO<Result<&1, &1, Err, Res>>:
3273        first : Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String> <-
3274          retry.one(True{}, method, url, headers, Bytes.slice(body, 0, 4294967295))
3275        retry.go(U32.to_nat(n), 0n, True{}, method, url, headers, first)
3276
3277def fetch.retry(+n: U32, +method: String, +url: String,
3278    +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) ->
3279    IO(Result<&1, &1, Err, Res>):
3280  retry.start(Bool.and(U32.is_ne(n, 0), pool.idempotent(method)),
3281    n, method, url, headers, body)
3282
3283# Streaming (a body read or sent in pieces). A decoded stream owns its decoders.
3284# What the next read returns: read more, a raw piece, a decoded piece, the end, or an error.
3285type Po is Type:
3286  PoNone{}
3287  PoPiece{b: Bytes.Bytes}
3288  PoReady{b: Bytes.Bytes}
3289  PoEnd{}
3290  PoBad{e: Err}
3291
3292type Stream is Type:
3293  Stream{tls: Bool, s: Socket, ms: U32, res: Res, rb: Rb, out: Po, decs: List<&1, Zlib.Decoder>}
3294
3295type Pc is Type:
3296  Pc{rb: Rb, out: Po}
3297
3298# A body piece, or none when empty: more reads the next piece, and not more is the end.
3299def pc.po(more: Bool, empty: Bool, b: Bytes.Bytes) -> Po:
3300  match empty:
3301    case True{}:
3302      Bool.pick(Po, more, PoNone{}, PoEnd{})
3303    case False{}:
3304      PoPiece{b}
3305
3306def pc.piece(more: Bool, +rb: Rb, b: Bytes.Bytes) -> Pc:
3307  Bytes.Bytes{+len, buf} = b
3308  Pc{rb, pc.po(more, U32.is_zero(len), Bytes.Bytes{len, buf})}
3309
3310def pc.fed.of(b: Bytes.Bytes, st: Rb) -> Pc:
3311  match st:
3312    case RbDone{}:
3313      pc.piece(False{}, RbDone{}, b)
3314    case RbBad{}:
3315      Pc{RbDone{}, PoBad{ErrBad{}}}
3316    case RbLen{n}:
3317      pc.piece(True{}, RbLen{n}, b)
3318    case RbChunk{st}:
3319      pc.piece(True{}, RbChunk{st}, b)
3320    case RbClose{}:
3321      pc.piece(True{}, RbClose{}, b)
3322
3323def pc.fed(bf: Bf) -> Pc:
3324  Bf{st, parts, rest} = bf
3325  pc.fed.of(rb.body(parts), st)
3326
3327# The body bytes that just arrived: what they add to the body, and how it ends.
3328def pc.of(rb: Rb, piece: Bytes.Bytes) -> Pc:
3329  pc.fed(rb.feed(rb, Nil{}, piece))
3330
3331# The server closed. Only a close-delimited body may end this way (RFC 9112 §8).
3332def pc.end(ok: Bool) -> Pc:
3333  match ok:
3334    case True{}:
3335      Pc{RbDone{}, PoEnd{}}
3336    case False{}:
3337      Pc{RbDone{}, PoBad{ErrBad{}}}
3338
3339def pc.eof(st: Rb) -> Pc:
3340  pc.end(rb.eof(st))
3341
3342def stream.mk(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, pc: Pc) -> Stream:
3343  Pc{rb, out} = pc
3344  Stream{tls, s, ms, res, rb, out, decs}
3345
3346def stream.got.piece(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, +rb: Rb, p: U32 & Array<U32>) -> Stream:
3347  (+len, buf) = p
3348  stream.mk(tls, s, ms, res, decs, Bool.pick(Pc, U32.is_zero(len), pc.eof(rb), pc.of(rb, Bytes.Bytes{len, buf})))
3349
3350def stream.got(+tls: Bool, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, +rb: Rb, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Stream:
3351  (s, r) = m
3352  match r:
3353    case Fail{(+code, why)}:
3354      Stream{tls, s, ms, res, RbDone{}, PoBad{err.or_late(code, ErrRead{code, why})}, decs}
3355    case Done{p}:
3356      stream.got.piece(tls, s, ms, res, decs, rb, p)
3357
3358def stream.after(+rb: Rb) -> Po:
3359  match rb:
3360    case RbDone{}:
3361      PoEnd{}
3362    case RbBad{}:
3363      PoEnd{}
3364    case RbLen{n}:
3365      PoNone{}
3366    case RbChunk{st}:
3367      PoNone{}
3368    case RbClose{}:
3369      PoNone{}
3370
3371type Fed is Type:
3372  Fed{decs: List<&1, Zlib.Decoder>, body: Result<&1, &1, Err, Bytes.Bytes>}
3373
3374def stream.feed.received(done: List<&1, Zlib.Decoder>, m: Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Fed:
3375  (d, r) = m
3376  match r:
3377    case Fail{e}:
3378      Fed{d <> done, Fail{ErrBad{}}}
3379    case Done{(+len, buf)}:
3380      Fed{d <> done, Done{Bytes.Bytes{len, buf}}}
3381
3382def stream.feed.step(st: Fed, d: Zlib.Decoder) -> IO(Fed):
3383  Fed{done, body} = st
3384  match body:
3385    case Fail{e}:
3386      IO.pure(Fed, Fed{d <> done, Fail{e}})
3387    case Done{b}:
3388      Bytes.Bytes{+len, buf} = b
3389      do IO<Fed>:
3390        m : Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
3391          Zlib.dec.feed.words(d, 16777216, len, buf)
3392        return stream.feed.received(done, m)
3393
3394def stream.feed.one(prev: IO(Fed), d: Zlib.Decoder) -> IO(Fed):
3395  do IO<Fed>:
3396    st : Fed <- prev
3397    stream.feed.step(st, d)
3398
3399def stream.feed.reverse(st: Fed) -> Fed:
3400  Fed{done, body} = st
3401  Fed{List.reverse(&1, Zlib.Decoder, done), body}
3402
3403def stream.feed.all(decs: List<&1, Zlib.Decoder>, b: Bytes.Bytes) -> IO(Fed):
3404  do IO<Fed>:
3405    st : Fed <- List.foldl(~&1, ~Zlib.Decoder, ~IO(Fed), ~stream.feed.one, decs,
3406      IO.pure(Fed, Fed{Nil{}, Done{b}}))
3407    return stream.feed.reverse(st)
3408
3409def stream.ready(empty: Bool, +rb: Rb, b: Bytes.Bytes) -> Po:
3410  match empty:
3411    case True{}:
3412      stream.after(rb)
3413    case False{}:
3414      PoReady{b}
3415
3416def stream.feed.got(+tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb, st: Fed) -> Stream:
3417  Fed{decs, body} = st
3418  match body:
3419    case Fail{e}:
3420      Stream{tls, s, ms, res, rb, PoBad{e}, decs}
3421    case Done{b}:
3422      Bytes.Bytes{+len, buf} = b
3423      Stream{tls, s, ms, res, rb, stream.ready(U32.is_zero(len), rb, Bytes.Bytes{len, buf}), decs}
3424
3425def stream.feed.st(st: Stream, b: Bytes.Bytes) -> IO(Stream):
3426  Stream{+tls, s, +ms, res, +rb, out, decs} = st
3427  match decs:
3428    case Nil{}:
3429      IO.pure(Stream, Stream{tls, s, ms, res, rb, PoReady{b}, Nil{}})
3430    case Con{d, rest}:
3431      do IO<Stream>:
3432        fed : Fed <- stream.feed.all(Con{d, rest}, b)
3433        return stream.feed.got(tls, s, ms, res, rb, fed)
3434
3435def stream.finish.ok(r: Result<&1, &1, U32 & String, Unit>) -> Bool:
3436  match r:
3437    case Fail{e}:
3438      False{}
3439    case Done{u}:
3440      True{}
3441
3442def stream.finish(decs: List<&1, Zlib.Decoder>) -> IO(Bool):
3443  match decs:
3444    case Nil{}:
3445      IO.pure(Bool, True{})
3446    case Con{d, rest}:
3447      do IO<Bool>:
3448        r : Result<&1, &1, U32 & String, Unit> <- Zlib.dec.finish(d)
3449        tail : Bool <- stream.finish(rest)
3450        return Bool.and(stream.finish.ok(r), tail)
3451
3452def stream.ended(good: Bool, +tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb) ->
3453  Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>:
3454  match good:
3455    case True{}:
3456      (Stream{tls, s, ms, res, rb, PoEnd{}, Nil{}}, Done{None{}})
3457    case False{}:
3458      (Stream{tls, s, ms, res, rb, PoBad{ErrBad{}}, Nil{}}, Fail{ErrBad{}})
3459
3460# The next piece of the body; None at the end. A piece is never empty.
3461@unsafe
3462def stream.read(st: Stream) -> IO(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>):
3463  Stream{+tls, s, +ms, res, +rb, out, decs} = st
3464  match out:
3465    case PoPiece{b}:
3466      do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3467        next : Stream <- stream.feed.st(Stream{tls, s, ms, res, rb, PoNone{}, decs}, b)
3468        stream.read(next)
3469    case PoReady{b}:
3470      IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
3471        (Stream{tls, s, ms, res, rb, stream.after(rb), decs}, Done{Some{b}}))
3472    case PoEnd{}:
3473      do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3474        good : Bool <- stream.finish(decs)
3475        return stream.ended(good, tls, s, ms, res, rb)
3476    case PoBad{+e}:
3477      IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
3478        (Stream{tls, s, ms, res, rb, PoBad{e}, decs}, Fail{e}))
3479    case PoNone{}:
3480      do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3481        m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
3482        stream.read(stream.got(tls, ms, res, decs, rb, m))
3483
3484# Status and headers. Its body is empty: read the body with stream.read.
3485def stream.res(st: Stream) -> Stream & Res:
3486  Stream{tls, s, ms, res, rb, out, decs} = st
3487  Res{+status, +headers, body} = res
3488  (Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, Res{status, headers, Bytes.new(0)})
3489
3490def stream.close(st: Stream) -> IO(Unit):
3491  Stream{tls, s, ms, res, rb, out, decs} = st
3492  do IO<Unit>:
3493    good : Bool <- stream.finish(decs)
3494    io.close(tls, s)
3495
3496# Head read state: still scanning, cut short or bad, or the head with the bytes after it.
3497type Sh is Type:
3498  ShMore{buf: Bytes.Bytes, k: U32}
3499  ShBad{err: Maybe<&2, Err>}
3500  ShRes{res: Res, rb: Rb, rest: Bytes.Bytes}
3501
3502def sh.of(hs: Hs) -> Sh:
3503  match hs:
3504    case HsWait{buf, k}:
3505      ShMore{buf, k}
3506    case HsBad{}:
3507      ShBad{None{}}
3508    case HsSeek{buf, from, k}:
3509      ShBad{None{}}
3510    case HsRes{res, rb, rest}:
3511      ShRes{res, rb, rest}
3512
3513def sh.piece(+head: Bool, buf: Bytes.Bytes, +k: U32, p: U32 & Array<U32>) -> Sh:
3514  (+len, b) = p
3515  Bool.pick(Sh, U32.is_zero(len), ShBad{None{}}, sh.of(hs.more(head, k, buf, Bytes.Bytes{len, b})))
3516
3517def sh.next(+head: Bool, buf: Bytes.Bytes, +k: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Sh:
3518  (s, r) = m
3519  match r:
3520    case Fail{(+code, why)}:
3521      (s, ShBad{Some{err.or_late(code, ErrRead{code, why})}})
3522    case Done{p}:
3523      (s, sh.piece(head, buf, k, p))
3524
3525def fetch.fail.of(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Stream>:
3526  match r:
3527    case Fail{e}:
3528      Fail{e}
3529    case Done{res}:
3530      Fail{ErrBad{}}
3531
3532# Reads until the final head is in; the body bytes that came with it are the first piece.
3533@unsafe
3534def stream.head(+tls: Bool, +ms: U32, +head: Bool, st: Socket & Sh) -> IO(Result<&1, &1, Err, Stream>):
3535  (s, sh) = st
3536  match sh:
3537    case ShMore{buf, +k}:
3538      do IO<Result<&1, &1, Err, Stream>>:
3539        m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
3540        stream.head(tls, ms, head, sh.next(head, buf, k, m))
3541    case ShBad{err}:
3542      do IO<Result<&1, &1, Err, Stream>>:
3543        r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, err)
3544        return fetch.fail.of(r)
3545    case ShRes{res, rb, rest}:
3546      IO.pure(Result<&1, &1, Err, Stream>, Done{stream.mk(tls, s, ms, res, Nil{}, pc.of(rb, rest))})
3547
3548def stream.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Stream>):
3549  (s, r) = m
3550  match r:
3551    case Fail{(+code, why)}:
3552      do IO<Result<&1, &1, Err, Stream>>:
3553        io.close(tls, s)
3554        return Fail{err.or_late(code, ErrWrite{code, why})}
3555    case Done{u}:
3556      stream.head(tls, ms, head, (s, ShMore{Bytes.new(0), 0}))
3557
3558def stream.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3559  match r:
3560    case Fail{e}:
3561      IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
3562    case Done{c}:
3563      match c:
3564        case Conn{+tls, s}:
3565          do IO<Result<&1, &1, Err, Stream>>:
3566            sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
3567            stream.sent(tls, ms, head, sent)
3568        case ConnH2{s, client}:
3569          do IO<Result<&1, &1, Err, Stream>>:
3570            Wire.tls.close(s)
3571            return Fail{ErrBad{}}
3572
3573# One connection per stream; the request says close.
3574def stream.origin(+ms: U32, +head: Bool, wire: Bytes.Bytes, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Stream>):
3575  Url.Abs{+scheme, +host, +port, target} = a
3576  match known:
3577    case False{}:
3578      IO.pure(Result<&1, &1, Err, Stream>, Fail{ErrUrl{}})
3579    case True{}:
3580      do IO<Result<&1, &1, Err, Stream>>:
3581        ips : List<&2, String> <- Dns.resolve.all(host)
3582        c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{}, False{})
3583        stream.conn(c, ms, head, wire)
3584
3585def stream.one.of(+method: String, +url: Url.Abs, +headers: Map<&2, List<&2, String>>, +ms: U32, r: Bytes.Bytes & Bytes.Bytes) -> IO(Hop & Result<&1, &1, Err, Stream>):
3586  Url.Abs{scheme, host, port, +target} = url
3587  (body, wire) = r
3588  do IO<Hop & Result<&1, &1, Err, Stream>>:
3589    got : Result<&1, &1, Err, Stream> <- stream.origin(ms, String.eq(method, "HEAD"), encode_req.on(method, target, Url.host_field(url), headers, wire, True{}), url, pool.scheme.ok(url))
3590    return (Hop{method, url, headers, body}, got)
3591
3592# One request on its own connection. The hop comes back for the redirect.
3593def stream.one(h: Hop, +ms: U32) -> IO(Hop & Result<&1, &1, Err, Stream>):
3594  Hop{+method, +url, +headers, body} = h
3595  stream.one.of(method, url, headers, ms, Bytes.slice(body, 0, 4294967295))
3596
3597# Go: the next request. Drop: close this stream, then go on. Done: the answer.
3598type Sn is Type:
3599  SnGo{left: Nat, hop: Hop}
3600  SnDrop{st: Stream, next: Next}
3601  SnDone{r: Result<&1, &1, Err, Stream>}
3602
3603def sn.of(n: Next) -> Sn:
3604  match n:
3605    case NGo{l, h}:
3606      SnGo{l, h}
3607    case NStop{}:
3608      SnDone{Fail{ErrRedirect{}}}
3609    case NDone{m}:
3610      match m:
3611        case Fail{e}:
3612          SnDone{Fail{e}}
3613        case Done{r}:
3614          SnDone{Fail{ErrBad{}}}
3615
3616def stream.decide.n(st: Stream, n: Next) -> Sn:
3617  match n:
3618    case NDone{m}:
3619      SnDone{Done{st}}
3620    case NGo{l, h}:
3621      SnDrop{st, NGo{l, h}}
3622    case NStop{}:
3623      SnDrop{st, NStop{}}
3624
3625def stream.decide.of(+left: Nat, hop: Hop, sr: Stream & Res) -> Sn:
3626  (st, res) = sr
3627  stream.decide.n(st, fetch.decide(left, hop, Done{res}))
3628
3629def stream.decide(+left: Nat, x: Hop & Result<&1, &1, Err, Stream>) -> Sn:
3630  (hop, r) = x
3631  match r:
3632    case Fail{e}:
3633      SnDone{Fail{e}}
3634    case Done{st}:
3635      stream.decide.of(left, hop, stream.res(st))
3636
3637@unsafe
3638def stream.hops(+ms: U32, sn: Sn) -> IO(Result<&1, &1, Err, Stream>):
3639  match sn:
3640    case SnDone{r}:
3641      IO.pure(Result<&1, &1, Err, Stream>, r)
3642    case SnGo{+left, hop}:
3643      do IO<Result<&1, &1, Err, Stream>>:
3644        x : Hop & Result<&1, &1, Err, Stream> <- stream.one(hop, ms)
3645        stream.hops(ms, stream.decide(left, x))
3646    case SnDrop{st, next}:
3647      do IO<Result<&1, &1, Err, Stream>>:
3648        stream.close(st)
3649        stream.hops(ms, sn.of(next))
3650
3651type Opened is Type:
3652  Opened{decs: List<&1, Zlib.Decoder>, bad: Bool}
3653
3654def stream.open.got(st: Opened, r: Result<&1, &1, U32 & String, Zlib.Decoder>) -> Opened:
3655  Opened{decs, bad} = st
3656  match r:
3657    case Fail{e}:
3658      Opened{decs, True{}}
3659    case Done{d}:
3660      Opened{d <> decs, bad}
3661
3662def stream.open.add(st: Opened, m: IO(Result<&1, &1, U32 & String, Zlib.Decoder>)) -> IO(Opened):
3663  do IO<Opened>:
3664    r : Result<&1, &1, U32 & String, Zlib.Decoder> <- m
3665    return stream.open.got(st, r)
3666
3667def stream.open.zstd(zstd: Bool, st: Opened) -> IO(Opened):
3668  match zstd:
3669    case True{}:
3670      stream.open.add(st, Zlib.zstd.new())
3671    case False{}:
3672      IO.pure(Opened, st)
3673
3674def stream.open.br(br: Bool, +c: String, st: Opened) -> IO(Opened):
3675  match br:
3676    case True{}:
3677      stream.open.add(st, Zlib.brotli.new())
3678    case False{}:
3679      stream.open.zstd(String.eq(c, "zstd"), st)
3680
3681def stream.open.gz(gz: Bool, +c: String, st: Opened) -> IO(Opened):
3682  match gz:
3683    case True{}:
3684      stream.open.add(st, Zlib.inflate.new())
3685    case False{}:
3686      stream.open.br(String.eq(c, "br"), c, st)
3687
3688def stream.open.step(+c: String, st: Opened) -> IO(Opened):
3689  Opened{decs, bad} = st
3690  match bad:
3691    case True{}:
3692      IO.pure(Opened, Opened{decs, True{}})
3693    case False{}:
3694      stream.open.gz(Bool.or(String.eq(c, "gzip"), Bool.or(String.eq(c, "x-gzip"), String.eq(c, "deflate"))),
3695        c, Opened{decs, False{}})
3696
3697def stream.open.one(prev: IO(Opened), c: String) -> IO(Opened):
3698  do IO<Opened>:
3699    st : Opened <- prev
3700    stream.open.step(c, st)
3701
3702def stream.open.all(cs: List<&2, String>) -> IO(Opened):
3703  List.foldl(~&2, ~String, ~IO(Opened), ~stream.open.one, cs, IO.pure(Opened, Opened{Nil{}, False{}}))
3704
3705def stream.put.decs(st: Stream, decs: List<&1, Zlib.Decoder>) -> Stream:
3706  Stream{tls, s, ms, res, rb, out, old} = st
3707  Stream{tls, s, ms, res, rb, out, decs}
3708
3709def stream.init.opened(st: Stream, opened: Opened) -> IO(Result<&1, &1, Err, Stream>):
3710  Opened{decs, bad} = opened
3711  match bad:
3712    case True{}:
3713      do IO<Result<&1, &1, Err, Stream>>:
3714        stream.close(stream.put.decs(st, decs))
3715        return Fail{ErrBad{}}
3716    case False{}:
3717      IO.pure(Result<&1, &1, Err, Stream>, Done{stream.put.decs(st, List.reverse(&1, Zlib.Decoder, decs))})
3718
3719def stream.init.known(known: Bool, st: Stream, cs: List<&2, String>) -> IO(Result<&1, &1, Err, Stream>):
3720  match known:
3721    case False{}:
3722      IO.pure(Result<&1, &1, Err, Stream>, Done{st})
3723    case True{}:
3724      do IO<Result<&1, &1, Err, Stream>>:
3725        opened : Opened <- stream.open.all(cs)
3726        stream.init.opened(st, opened)
3727
3728def stream.init.st(+enc: String, st: Stream) -> IO(Result<&1, &1, Err, Stream>):
3729  Stream{tls, s, ms, res, rb, out, decs} = st
3730  Res{+status, +headers, body} = res
3731  +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
3732  stream.init.known(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}),
3733    Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, cs)
3734
3735def stream.init(+enc: String, r: Result<&1, &1, Err, Stream>) -> IO(Result<&1, &1, Err, Stream>):
3736  match r:
3737    case Fail{e}:
3738      IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
3739    case Done{st}:
3740      stream.init.st(enc, st)
3741
3742def stream.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>) -> Sn:
3743  match u:
3744    case None{}:
3745      SnDone{Fail{ErrUrl{}}}
3746    case Some{a}:
3747      SnGo{20n, Hop{method, a, req.put(Map.to_list(&2, List<&2, String>, headers), empty()), body}}
3748
3749# Open a raw stream. Its body bytes and headers remain as sent.
3750def open.raw.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
3751  stream.hops(ms, stream.start(method, headers, body, Url.absolute(url)))
3752
3753def open.raw(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3754  open.raw.with(method, url, headers, body, 30000)
3755
3756def open.with.enc(+enc: String, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
3757  do IO<Result<&1, &1, Err, Stream>>:
3758    r : Result<&1, &1, Err, Stream> <-
3759      stream.hops(ms, stream.start(method, accept.enc(headers, enc), body, Url.absolute(url)))
3760    stream.init(enc, r)
3761
3762# Follow redirects, then decode each body piece by Content-Encoding. Unknown codings stay raw.
3763def open.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
3764  do IO<Result<&1, &1, Err, Stream>>:
3765    enc : String <- codings()
3766    open.with.enc(enc, method, url, headers, body, ms)
3767
3768def open(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3769  open.with(method, url, headers, body, 30000)
3770
3771# Upload: the request body sent in chunks (RFC 9112 §7.1). err: the first failed write.
3772type Up is Type:
3773  Up{tls: Bool, s: Socket, ms: U32, head: Bool, err: Maybe<&2, Err>}
3774
3775def hex.digit(+n: U32) -> Char:
3776  Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))}
3777
3778def hex.go(k: Nat, +n: U32, acc: String) -> String:
3779  match k:
3780    case 0n:
3781      acc
3782    case 1n+p:
3783      hex.go(p, U32.shrn(n, 4n), SCon{hex.digit(U32.and(n, 15)), acc})
3784
3785def hex.trim(+s: String) -> String:
3786  match s:
3787    case SNil{}:
3788      SNil{}
3789    case SCon{Chr{+c}, +t}:
3790      Bool.pick(String, Bool.and(U32.is_eq(c, 48), Bool.not(String.is_empty(t))), hex.trim(t), SCon{Chr{c}, t})
3791
3792def hex(+n: U32) -> String:
3793  hex.trim(hex.go(8n, n, ""))
3794
3795def up.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up:
3796  (s, r) = m
3797  match r:
3798    case Fail{(+code, why)}:
3799      Up{tls, s, ms, head, Some{err.or_late(code, ErrWrite{code, why})}}
3800    case Done{u}:
3801      Up{tls, s, ms, head, None{}}
3802
3803def up.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: String) -> IO(Result<&1, &1, Err, Up>):
3804  match r:
3805    case Fail{e}:
3806      IO.pure(Result<&1, &1, Err, Up>, Fail{e})
3807    case Done{c}:
3808      match c:
3809        case Conn{+tls, s}:
3810          do IO<Result<&1, &1, Err, Up>>:
3811            sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(tls, s, wire)
3812            return Done{up.sent(tls, ms, head, sent)}
3813        case ConnH2{s, client}:
3814          do IO<Result<&1, &1, Err, Up>>:
3815            Wire.tls.close(s)
3816            return Fail{ErrBad{}}
3817
3818def up.head(+method: String, +target: String, +hf: String, +headers: Map<&2, List<&2, String>>) -> String:
3819  request(method, target, set(set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", hf), "connection", "close"), "transfer-encoding", "chunked"), "")
3820
3821def up.origin(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Up>):
3822  Url.Abs{+scheme, +host, +port, +target} = a
3823  match known:
3824    case False{}:
3825      IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
3826    case True{}:
3827      do IO<Result<&1, &1, Err, Up>>:
3828        ips : List<&2, String> <- Dns.resolve.all(host)
3829        c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{}, False{})
3830        up.conn(c, ms, String.eq(method, "HEAD"), up.head(method, target, Url.host_field(a), headers))
3831
3832def up.url(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, u: Maybe<&2, Url.Abs>) -> IO(Result<&1, &1, Err, Up>):
3833  match u:
3834    case None{}:
3835      IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
3836    case Some{+a}:
3837      up.origin(method, ms, headers, a, pool.scheme.ok(a))
3838
3839# Http.upload(method, url, headers) sends the head. A streamed body cannot be replayed, so redirects are not followed.
3840def upload.with(+method: String, url: String, headers: Map<&2, List<&2, String>>, +ms: U32) -> IO(Result<&1, &1, Err, Up>):
3841  up.url(method, ms, headers, Url.absolute(url))
3842
3843def upload(+method: String, url: String, headers: Map<&2, List<&2, String>>) -> IO(Result<&1, &1, Err, Up>):
3844  upload.with(method, url, headers, 30000)
3845
3846def up.wrote(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up & Result<&2, &2, Err, Unit>:
3847  (s, r) = m
3848  match r:
3849    case Fail{(+code, why)}:
3850      +e = err.or_late(code, ErrWrite{code, why})
3851      (Up{tls, s, ms, head, Some{e}}, Fail{e})
3852    case Done{u}:
3853      (Up{tls, s, ms, head, None{}}, Done{Unit{}})
3854
3855# One write per chunk, so the size line and the data do not wait on each other (Nagle).
3856def up.put(+tls: Bool, s: Socket, +ms: U32, +head: Bool, +len: U32, piece: Bytes.Bytes, skip: Bool) -> IO(Up & Result<&2, &2, Err, Unit>):
3857  match skip:
3858    case True{}:
3859      IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, None{}}, Done{Unit{}}))
3860    case False{}:
3861      do IO<Up & Result<&2, &2, Err, Unit>>:
3862        sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, Bytes.concat(Con{Bytes.from_string(hex(len) ++ "\r\n"), Con{piece, Con{Bytes.from_string("\r\n"), Nil{}}}}))
3863        return up.wrote(tls, ms, head, sent)
3864
3865def up.chunk(+tls: Bool, s: Socket, +ms: U32, +head: Bool, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
3866  Bytes.Bytes{+len, buf} = piece
3867  up.put(tls, s, ms, head, len, Bytes.Bytes{len, buf}, U32.is_zero(len))
3868
3869# One chunk. An empty piece sends nothing, since an empty chunk would end the body.
3870def upload.write(up: Up, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
3871  Up{+tls, s, +ms, +head, err} = up
3872  match err:
3873    case Some{+e}:
3874      IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, Some{e}}, Fail{e}))
3875    case None{}:
3876      up.chunk(tls, s, ms, head, piece)
3877
3878# Ends the body and returns the response as a stream.
3879def upload.finish(up: Up) -> IO(Result<&1, &1, Err, Stream>):
3880  Up{+tls, s, +ms, +head, err} = up
3881  match err:
3882    case Some{e}:
3883      do IO<Result<&1, &1, Err, Stream>>:
3884        io.close(tls, s)
3885        return Fail{e}
3886    case None{}:
3887      do IO<Result<&1, &1, Err, Stream>>:
3888        sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(tls, s, "0\r\n\r\n")
3889        stream.sent(tls, ms, head, sent)
3890
3891def reply.bytes(res: Res, head: Bool, close: Bool) -> Bytes.Bytes:
3892  Res{+status, +headers, body} = res
3893  encode.on(Res{status, Bool.pick(Map<&2, List<&2, String>>, close, set(headers, "connection", "close"), headers), body}, head)
3894
3895def reply.fail.bytes(+status: U32) -> Res:
3896  Res{status, empty(), Bytes.from_string(reason(status))}
3897
3898def reply.sent.close(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Unit):
3899  (s, r) = m
3900  Socket.close(s)
3901
3902def reply_fail(s: Socket, +status: U32) -> IO(Unit):
3903  do IO<Unit>:
3904    sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, encode(reply.fail.bytes(status)))
3905    reply.sent.close(sent)
3906
3907
3908# The head is parsed once, when it is whole. Body pieces are kept as they come and joined once.
3909type Sv is Type:
3910  SvHead{buf: Bytes.Bytes}
3911  SvLen{req: Req, v11: Bool, left: U32, parts: List<&1, Bytes.Bytes>}
3912  SvChunk{req: Req, v11: Bool, n: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
3913
3914# More: read on, first answering 100 Continue when cont is set.
3915type Turn is Type:
3916  TurnClose{}
3917  TurnFail{status: U32}
3918  TurnReq{req: Req, rest: Bytes.Bytes, v11: Bool}
3919  TurnMore{sv: Sv, cont: Bool}
3920
3921def serve.max() -> Nat:
3922  fetch.max()
3923
3924def sv.none() -> Sv:
3925  SvHead{Bytes.new(0)}
3926
3927def sv.body(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes) -> Turn:
3928  Req{method, path, headers, body} = req
3929  TurnReq{Req{method, path, headers, rb.body(parts)}, rest, v11}
3930
3931def sv.len.cut(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
3932  (piece, last) = r
3933  sv.body(req, v11, Con{last, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32))))
3934
3935def sv.len.have(short: Bool, req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Turn:
3936  match short:
3937    case True{}:
3938      TurnMore{SvLen{req, v11, (left - len : U32), Con{piece, parts}}, False{}}
3939    case False{}:
3940      sv.len.cut(req, v11, parts, len, left, Bytes.slice(piece, 0, left))
3941
3942def sv.len(req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3943  Bytes.Bytes{+len, buf} = piece
3944  sv.len.have(U32.is_lt(len, left), req, v11, left, parts, len, Bytes.Bytes{len, buf})
3945
3946def sv.chunk.of(req: Req, +v11: Bool, +n: U32, c: Ck) -> Turn:
3947  Ck{st, parts, rest} = c
3948  match st:
3949    case DcDone{}:
3950      sv.body(req, v11, parts, rest)
3951    case DcBad{}:
3952      TurnFail{400}
3953    case DcSize{a, b}:
3954      TurnMore{SvChunk{req, v11, n, DcSize{a, b}, parts}, False{}}
3955    case DcExt{x}:
3956      TurnMore{SvChunk{req, v11, n, DcExt{x}, parts}, False{}}
3957    case DcSizeLf{x}:
3958      TurnMore{SvChunk{req, v11, n, DcSizeLf{x}, parts}, False{}}
3959    case DcData{k}:
3960      TurnMore{SvChunk{req, v11, n, DcData{k}, parts}, False{}}
3961    case DcDataCr{}:
3962      TurnMore{SvChunk{req, v11, n, DcDataCr{}, parts}, False{}}
3963    case DcDataLf{}:
3964      TurnMore{SvChunk{req, v11, n, DcDataLf{}, parts}, False{}}
3965    case DcTr{j}:
3966      TurnMore{SvChunk{req, v11, n, DcTr{j}, parts}, False{}}
3967
3968def sv.chunk.cap(big: Bool, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3969  match big:
3970    case True{}:
3971      TurnFail{413}
3972    case False{}:
3973      sv.chunk.of(req, v11, n, ck(piece, st, parts))
3974
3975def sv.chunk(+max: Nat, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3976  Bytes.Bytes{+len, buf} = piece
3977  +n2 = (n + len : U32)
3978  sv.chunk.cap(Bool.or(U32.is_lt(n2, n), Nat.is_lt(max, U32.to_nat(n2))), req, v11, n2, st, parts, Bytes.Bytes{len, buf})
3979
3980# RFC 9110 §10.1.1: answer 100 Continue only when the body is still to come.
3981def sv.cont(want: Bool, t: Turn) -> Turn:
3982  match t:
3983    case TurnMore{sv, c}:
3984      TurnMore{sv, want}
3985    case TurnClose{}:
3986      TurnClose{}
3987    case TurnFail{s}:
3988      TurnFail{s}
3989    case TurnReq{req, rest, v11}:
3990      TurnReq{req, rest, v11}
3991
3992def sv.cl.k(big: Bool, req: Req, +v11: Bool, +k: U32, rest: Bytes.Bytes) -> Turn:
3993  match big:
3994    case True{}:
3995      TurnFail{413}
3996    case False{}:
3997      sv.len(req, v11, k, Nil{}, rest)
3998
3999def sv.cl(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, n: Maybe<&2, U32>) -> Turn:
4000  match n:
4001    case None{}:
4002      TurnFail{400}
4003    case Some{+k}:
4004      sv.cl.k(Nat.is_lt(max, U32.to_nat(k)), req, v11, k, rest)
4005
4006def sv.frame(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, te: Bool) -> Turn:
4007  Req{method, path, +headers, body} = req
4008  match te:
4009    case True{}:
4010      sv.chunk(max, Req{method, path, headers, body}, v11, 0, dc.start(), Nil{}, rest)
4011    case False{}:
4012      sv.cl(max, Req{method, path, headers, body}, v11, rest, parse_u32(header(headers, "content-length")))
4013
4014def sv.expects(+v11: Bool, +headers: Map<&2, List<&2, String>>) -> Bool:
4015  Bool.and(v11, String.eq(String.to_lower(header(headers, "expect")), "100-continue"))
4016
4017def sv.got.head(+max: Nat, +v11: Bool, rest: Bytes.Bytes, req: Req) -> Turn:
4018  Req{method, path, +headers, body} = req
4019  sv.cont(sv.expects(v11, headers), sv.frame(max, Req{method, path, headers, body}, v11, rest, has_header(headers, "transfer-encoding")))
4020
4021def sv.parsed(+max: Nat, +v11: Bool, rest: Bytes.Bytes, g: Got) -> Turn:
4022  match g:
4023    case GotBad{}:
4024      TurnFail{400}
4025    case GotMore{}:
4026      TurnFail{400}
4027    case GotReq{req}:
4028      TurnReq{req, rest, v11}
4029    case GotHead{req}:
4030      sv.got.head(max, v11, rest, req)
4031
4032def sv.split(+max: Nat, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
4033  (buf, hb) = r
4034  +head = Bytes.to_string(hb)
4035  sv.parsed(max, req.v11(head), bytes.snd(Bytes.slice(buf, hlen, (len - hlen : U32))), parse.got(head))
4036
4037def sv.hit.none(big: Bool, buf: Bytes.Bytes) -> Turn:
4038  match big:
4039    case True{}:
4040      TurnFail{431}
4041    case False{}:
4042      TurnMore{SvHead{buf}, False{}}
4043
4044def sv.hit.some(big: Bool, +max: Nat, +hlen: U32, +len: U32, buf: Bytes.Bytes) -> Turn:
4045  match big:
4046    case True{}:
4047      TurnFail{431}
4048    case False{}:
4049      sv.split(max, hlen, len, Bytes.slice(buf, 0, hlen))
4050
4051# RFC 6585 §5: a head over 64 KiB is refused.
4052def sv.hit(+max: Nat, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Turn:
4053  match at:
4054    case None{}:
4055      sv.hit.none(U32.is_lt(65536, len), buf)
4056    case Some{+i}:
4057      +hlen = (i + 4 : U32)
4058      sv.hit.some(U32.is_lt(65536, hlen), max, hlen, len, buf)
4059
4060def sv.seek.of(+max: Nat, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Turn:
4061  (tail, m) = r
4062  sv.hit(max, len, buf, found.at(from, m))
4063
4064def sv.seek(+max: Nat, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
4065  (buf, tail) = r
4066  sv.seek.of(max, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
4067
4068# Only the new bytes, and the 3 before them, can finish the blank line.
4069def sv.head.at(+max: Nat, +from: U32, buf: Bytes.Bytes) -> Turn:
4070  Bytes.Bytes{+len, b} = buf
4071  sv.seek(max, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
4072
4073def sv.head(+max: Nat, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Turn:
4074  Bytes.Bytes{+ol, ob} = buf
4075  sv.head.at(max, Bool.pick(U32, U32.is_lt(ol, 3), 0, (ol - 3 : U32)), Bytes.append(Bytes.Bytes{ol, ob}, piece))
4076
4077def sv.closed.pick(empty: Bool) -> Turn:
4078  match empty:
4079    case True{}:
4080      TurnClose{}
4081    case False{}:
4082      TurnFail{400}
4083
4084def sv.closed.head(buf: Bytes.Bytes) -> Turn:
4085  Bytes.Bytes{+len, b} = buf
4086  sv.closed.pick(U32.is_eq(len, 0))
4087
4088# A close mid-request is a request cut short (RFC 9112 §8).
4089def sv.step(closed: Bool, +max: Nat, sv: Sv, piece: Bytes.Bytes) -> Turn:
4090  match closed:
4091    case True{}:
4092      match sv:
4093        case SvHead{buf}:
4094          sv.closed.head(buf)
4095        case SvLen{req, v11, left, parts}:
4096          TurnFail{400}
4097        case SvChunk{req, v11, n, st, parts}:
4098          TurnFail{400}
4099    case False{}:
4100      match sv:
4101        case SvHead{buf}:
4102          sv.head(max, buf, piece)
4103        case SvLen{req, +v11, +left, parts}:
4104          sv.len(req, v11, left, parts, piece)
4105        case SvChunk{req, +v11, +n, st, parts}:
4106          sv.chunk(max, req, v11, n, st, parts, piece)
4107
4108def sv.frame.req(t: Turn) -> Maybe<&1, String & String>:
4109  match t:
4110    case TurnReq{req, rest, v11}:
4111      Req{method, path, headers, body} = req
4112      Some{(Bytes.to_string(body), Bytes.to_string(rest))}
4113    case TurnMore{sv, c}:
4114      None{}
4115    case TurnFail{s}:
4116      None{}
4117    case TurnClose{}:
4118      None{}
4119
4120def sv.frame.go(xs: List<&2, String>, t: Turn) -> Maybe<&1, String & String>:
4121  match xs:
4122    case Nil{}:
4123      sv.frame.req(t)
4124    case Con{+x, rest}:
4125      match t:
4126        case TurnMore{sv, c}:
4127          sv.frame.go(rest, sv.step(False{}, serve.max(), sv, Bytes.from_string(x)))
4128        case TurnReq{req, r, v11}:
4129          sv.frame.req(TurnReq{req, r, v11})
4130        case TurnFail{s}:
4131          None{}
4132        case TurnClose{}:
4133          None{}
4134
4135# The body and the bytes after it, once the pieces make a whole request; None otherwise.
4136def serve.frame(xs: List<&2, String>) -> Maybe<&1, String & String>:
4137  sv.frame.go(xs, TurnMore{sv.none(), False{}})
4138
4139def talk.piece(+max: Nat, sv: Sv, p: U32 & Array<U32>) -> Turn:
4140  (+len, buf) = p
4141  sv.step(U32.is_eq(len, 0), max, sv, Bytes.Bytes{len, buf})
4142
4143def talk.next(+max: Nat, sv: Sv, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Turn:
4144  (s, r) = m
4145  match r:
4146    case Fail{e}:
4147      (s, TurnClose{})
4148    case Done{p}:
4149      (s, talk.piece(max, sv, p))
4150
4151def talk.after.pick(empty: Bool, +max: Nat, rest: Bytes.Bytes) -> Turn:
4152  match empty:
4153    case True{}:
4154      TurnMore{sv.none(), False{}}
4155    case False{}:
4156      sv.step(False{}, max, sv.none(), rest)
4157
4158def talk.after.rest(+max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
4159  Bytes.Bytes{+len, buf} = rest
4160  (s, talk.after.pick(U32.is_eq(len, 0), max, Bytes.Bytes{len, buf}))
4161
4162def talk.after.keep(keep: Bool, +max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
4163  match keep:
4164    case False{}:
4165      (s, TurnClose{})
4166    case True{}:
4167      talk.after.rest(max, rest, s)
4168
4169def talk.after(+max: Nat, keep: Bool, rest: Bytes.Bytes, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket & Turn:
4170  (s, r) = m
4171  match r:
4172    case Fail{e}:
4173      (s, TurnClose{})
4174    case Done{u}:
4175      talk.after.keep(keep, max, rest, s)
4176
4177def talk.send(+max: Nat, s: Socket, rest: Bytes.Bytes, +headers: Map<&2, List<&2, String>>, v11: Bool, +head: Bool, res: Res) -> IO(Socket & Turn):
4178  Res{+status, +rh, body} = res
4179  +keep = serve.keep(headers, v11, status, rh)
4180  do IO<Socket & Turn>:
4181    sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, reply.bytes(Res{status, rh, body}, head, Bool.not(keep)))
4182    return talk.after(max, keep, rest, sent)
4183
4184def talk.cont.sent(m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket:
4185  (s, r) = m
4186  s
4187
4188def talk.cont(cont: Bool, s: Socket) -> IO(Socket):
4189  match cont:
4190    case False{}:
4191      IO.pure(Socket, s)
4192    case True{}:
4193      do IO<Socket>:
4194        sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send(s, "HTTP/1.1 100 Continue\r\n\r\n")
4195        return talk.cont.sent(sent)
4196
4197@unsafe
4198def talk(~h: Req -> IO(Res), +max: Nat, st: Socket & Turn) -> IO(Unit):
4199  (s, t) = st
4200  match t:
4201    case TurnMore{sv, cont}:
4202      do IO<Unit>:
4203        s2 : Socket <- talk.cont(cont, s)
4204        m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- Wire.recv.words(s2, 65536, 30000)
4205        talk(~h, max, talk.next(max, sv, m))
4206    case TurnReq{req, rest, v11}:
4207      Req{+method, path, +headers, body} = req
4208      do IO<Unit>:
4209        res : Res <- h(Req{method, path, headers, body})
4210        next : Socket & Turn <- talk.send(max, s, rest, headers, v11, String.eq(method, "HEAD"), res)
4211        talk(~h, max, next)
4212    case TurnFail{status}:
4213      reply_fail(s, status)
4214    case TurnClose{}:
4215      Socket.close(s)
4216
4217def conn(~h: Req -> IO(Res), +max: Nat, m: Listener & Result<&1, &1, U32 & String, Socket>) -> IO(Listener):
4218  (l, r) = m
4219  do IO<Listener>:
4220    s : Socket <- IO.pass(Socket, r)
4221    IO.spawn(Unit, talk(~h, max, (s, TurnMore{sv.none(), False{}})))
4222    return l
4223
4224@unsafe
4225def loop(~h: Req -> IO(Res), +max: Nat, l: Listener) -> IO(Unit):
4226  do IO<Unit>:
4227    m  : Listener & Result<&1, &1, U32 & String, Socket> <- TCP.accept(l)
4228    l2 : Listener <- conn(~h, max, m)
4229    loop(~h, max, l2)
4230
4231def serve.with(~h: Req -> IO(Res), +port: U32, +max: Nat) -> IO(Unit):
4232  do IO<Unit>:
4233    l : Listener <- IO.try(Listener, TCP.listen(port))
4234    IO.print("http://127.0.0.1:" ++ U32.show(port))
4235    loop(~h, max, l)
4236
4237def serve(~h: Req -> IO(Res), +port: U32) -> IO(Unit):
4238  serve.with(~h, port, serve.max())