http.bend

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