http.bend
bend-kit-http@0.25.0.2 · 5,782 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, -zlib@0.2.0.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.5.0.0/dns.bend as Dns
16import bend-kit-zlib@0.2.0.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.22.0.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
346
347def parse.headers.scan.line(acc: String, fields: Fields) -> Fields:
348 match acc:
349 case SCon{Chr{13}, t}:
350 fields_put(fields, String.reverse(t))
351 case other:
352 fields_put(fields, String.reverse(other))
353
354def parse.headers.scan(s: String, acc: String, fields: Fields) -> Fields:
355 match s:
356 case SNil{}:
357 parse.headers.scan.line(acc, fields)
358 case SCon{Chr{10}, t}:
359 parse.headers.scan(t, SNil{}, parse.headers.scan.line(acc, fields))
360 case SCon{c, t}:
361 parse.headers.scan(t, SCon{c, acc}, fields)
362
363def parse.headers.raw(s: String) -> Maybe<&2, Map<&2, List<&2, String>>>:
364 parse.headers.done(parse.headers.scan(s, SNil{}, FieldsOk{empty()}))
365
366def parse.first(s: String, acc: String) -> String & String:
367 match s:
368 case SNil{}:
369 (String.reverse(acc), SNil{})
370 case SCon{Chr{10}, t}:
371 (String.reverse(acc), t)
372 case SCon{c, t}:
373 parse.first(t, SCon{c, acc})
374
375def parse_u32.digit(+c: U32) -> Bool:
376 Bool.and(U32.is_le(48, c), U32.is_le(c, 57))
377
378def parse_u32.add(acc: U32, c: U32) -> U32:
379 (acc * 10 + (c - 48 : U32) : U32)
380
381def parse_u32.done(acc: U32, bad: Bool) -> Maybe<&2, U32>:
382 match bad:
383 case True{}:
384 None{}
385 case False{}:
386 Some{acc}
387
388def parse_u32.go(s: String, acc: U32, bad: Bool) -> Maybe<&2, U32>:
389 match s:
390 case SNil{}:
391 parse_u32.done(acc, bad)
392 case SCon{Chr{+c}, t}:
393 parse_u32.go(t, parse_u32.add(acc, c), Bool.or(bad, Bool.not(parse_u32.digit(c))))
394
395def parse_u32(s: String) -> Maybe<&2, U32>:
396 match s:
397 case SNil{}:
398 None{}
399 case SCon{Chr{+c}, t}:
400 parse_u32.go(t, parse_u32.add(0, c), Bool.not(parse_u32.digit(c)))
401
402# More: a valid prefix. Bad: cannot become a body. Body: a whole chunked body.
403type Hold is Data:
404 HoldMore{}
405 HoldBad{}
406 HoldBody{b: String}
407 HoldUntil{b: String}
408
409def is_hex(+c: U32) -> Bool:
410 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))))
411
412def hexv(+c: U32) -> U32:
413 Bool.pick(U32, parse_u32.digit(c), (c - 48 : U32), Bool.pick(U32, U32.is_le(c, 70), (c - 55 : U32), (c - 87 : U32)))
414
415# A chunked body decoder that reads each byte once, so a body fed in pieces
416# costs O(bytes) in total. Tr{j}: j bytes of the closing CRLF CRLF matched.
417type Dc is Data:
418 DcSize{acc: U32, seen: Bool}
419 DcExt{n: U32}
420 DcSizeLf{n: U32}
421 DcData{k: U32}
422 DcDataCr{}
423 DcDataLf{}
424 DcTr{j: U32}
425 DcDone{}
426 DcBad{}
427
428# st: where the decoder is. racc: the body so far, reversed. rest: bytes after a Done body.
429type Dco is Data:
430 Dco{st: Dc, racc: String, rest: String}
431
432def dc.start() -> Dc:
433 DcSize{0, False{}}
434
435def dc.size.semi(+n: U32, semi: Bool) -> Dc:
436 match semi:
437 case True{}:
438 DcExt{n}
439 case False{}:
440 DcBad{}
441
442def dc.size.cr(+n: U32, +c: U32, cr: Bool) -> Dc:
443 match cr:
444 case True{}:
445 DcSizeLf{n}
446 case False{}:
447 dc.size.semi(n, U32.is_eq(c, 59))
448
449def dc.size.end(+n: U32, +c: U32, seen: Bool) -> Dc:
450 match seen:
451 case False{}:
452 DcBad{}
453 case True{}:
454 dc.size.cr(n, c, U32.is_eq(c, 13))
455
456# A size that would overflow 32 bits ends the digits, and size.end then refuses it.
457def dc.size(+acc: U32, seen: Bool, +c: U32, digit: Bool) -> Dc:
458 match digit:
459 case True{}:
460 DcSize{(acc * 16 + hexv(c) : U32), True{}}
461 case False{}:
462 dc.size.end(acc, c, seen)
463
464# RFC 9112 §7.1.1: recipients ignore unknown chunk extensions; a bare LF is not CRLF.
465def dc.ext.lf(+n: U32, lf: Bool) -> Dc:
466 match lf:
467 case True{}:
468 DcBad{}
469 case False{}:
470 DcExt{n}
471
472def dc.ext(+n: U32, +c: U32, cr: Bool) -> Dc:
473 match cr:
474 case True{}:
475 DcSizeLf{n}
476 case False{}:
477 dc.ext.lf(n, U32.is_eq(c, 10))
478
479def dc.sized(+n: U32, zero: Bool) -> Dc:
480 match zero:
481 case True{}:
482 DcTr{2}
483 case False{}:
484 DcData{n}
485
486def dc.size.lf(+n: U32, lf: Bool) -> Dc:
487 match lf:
488 case True{}:
489 dc.sized(n, U32.is_eq(n, 0))
490 case False{}:
491 DcBad{}
492
493# k data bytes are left and m of them were just read.
494def dc.data(+k: U32, +m: U32) -> Dc:
495 Bool.pick(Dc, U32.is_le(k, m), DcDataCr{}, DcData{(k - m : U32)})
496
497def dc.pick(ok: Bool, next: Dc) -> Dc:
498 match ok:
499 case True{}:
500 next
501 case False{}:
502 DcBad{}
503
504# ponytail: trailer fields are dropped unparsed (§7.1.2 allows discarding)
505def dc.tr.hit(+j: U32) -> Dc:
506 Bool.pick(Dc, U32.is_eq(j, 3), DcDone{}, DcTr{(j + 1 : U32)})
507
508def dc.tr(+j: U32, +c: U32, hit: Bool) -> Dc:
509 match hit:
510 case True{}:
511 dc.tr.hit(j)
512 case False{}:
513 Bool.pick(Dc, U32.is_eq(c, 13), DcTr{1}, DcTr{0})
514
515def dc.tr.want(+j: U32) -> U32:
516 Bool.pick(U32, U32.is_eq(U32.mod(j, 2), 0), 13, 10)
517
518def dc.byte(h: Char) -> U32:
519 Chr{c} = h
520 c
521
522# One byte c. Done and Bad never look at it, and a data byte is not inspected.
523def dc.step(st: Dc, +c: U32) -> Dc:
524 match st:
525 case DcBad{}:
526 DcBad{}
527 case DcSize{+acc, seen}:
528 dc.size(acc, seen, c, Bool.and(is_hex(c), U32.is_le(acc, 268435455)))
529 case DcExt{+n}:
530 dc.ext(n, c, U32.is_eq(c, 13))
531 case DcSizeLf{+n}:
532 dc.size.lf(n, U32.is_eq(c, 10))
533 case DcDataCr{}:
534 dc.pick(U32.is_eq(c, 13), DcDataLf{})
535 case DcDataLf{}:
536 dc.pick(U32.is_eq(c, 10), dc.start())
537 case DcTr{+j}:
538 dc.tr(j, c, U32.is_eq(c, dc.tr.want(j)))
539 case DcData{+k}:
540 dc.data(k, 1)
541 case DcDone{}:
542 DcDone{}
543
544def dc.live(st: Dc) -> Bool:
545 match st:
546 case DcDone{}:
547 False{}
548 case DcBad{}:
549 False{}
550 case DcSize{a, b}:
551 True{}
552 case DcExt{n}:
553 True{}
554 case DcSizeLf{n}:
555 True{}
556 case DcData{k}:
557 True{}
558 case DcDataCr{}:
559 True{}
560 case DcDataLf{}:
561 True{}
562 case DcTr{j}:
563 True{}
564
565def dc.feed(s: String, st: Dc, racc: String) -> Dco:
566 match s:
567 case SNil{}:
568 Dco{st, racc, ""}
569 case SCon{h, t}:
570 match st:
571 case DcBad{}:
572 Dco{DcBad{}, racc, ""}
573 case DcDone{}:
574 Dco{DcDone{}, racc, SCon{h, t}}
575 case DcData{+k}:
576 dc.feed(t, dc.data(k, 1), SCon{h, racc})
577 case DcSize{+acc, seen}:
578 dc.feed(t, dc.step(DcSize{acc, seen}, dc.byte(h)), racc)
579 case DcExt{+n}:
580 dc.feed(t, dc.step(DcExt{n}, dc.byte(h)), racc)
581 case DcSizeLf{+n}:
582 dc.feed(t, dc.step(DcSizeLf{n}, dc.byte(h)), racc)
583 case DcDataCr{}:
584 dc.feed(t, dc.step(DcDataCr{}, dc.byte(h)), racc)
585 case DcDataLf{}:
586 dc.feed(t, dc.step(DcDataLf{}, dc.byte(h)), racc)
587 case DcTr{+j}:
588 dc.feed(t, dc.step(DcTr{j}, dc.byte(h)), racc)
589
590def chunk.hold(o: Dco) -> Hold:
591 Dco{st, racc, rest} = o
592 match st:
593 case DcDone{}:
594 HoldBody{String.reverse(racc)}
595 case DcBad{}:
596 HoldBad{}
597 case DcSize{a, b}:
598 HoldMore{}
599 case DcExt{n}:
600 HoldMore{}
601 case DcSizeLf{n}:
602 HoldMore{}
603 case DcData{k}:
604 HoldMore{}
605 case DcDataCr{}:
606 HoldMore{}
607 case DcDataLf{}:
608 HoldMore{}
609 case DcTr{j}:
610 HoldMore{}
611
612def chunk.live(s: String) -> Hold:
613 chunk.hold(dc.feed(s, dc.start(), ""))
614
615def chunk.rest(o: Dco) -> Maybe<&2, String>:
616 Dco{st, racc, rest} = o
617 match st:
618 case DcDone{}:
619 Some{rest}
620 case DcBad{}:
621 None{}
622 case DcSize{a, b}:
623 None{}
624 case DcExt{n}:
625 None{}
626 case DcSizeLf{n}:
627 None{}
628 case DcData{k}:
629 None{}
630 case DcDataCr{}:
631 None{}
632 case DcDataLf{}:
633 None{}
634 case DcTr{j}:
635 None{}
636
637def chunk.suffix(s: String) -> Maybe<&2, String>:
638 chunk.rest(dc.feed(s, dc.start(), ""))
639
640def chunk.decode.hold(h: Hold) -> Maybe<&2, String>:
641 match h:
642 case HoldMore{}:
643 None{}
644 case HoldBad{}:
645 None{}
646 case HoldUntil{b}:
647 None{}
648 case HoldBody{b}:
649 Some{b}
650
651def chunk.decode(s: String) -> Maybe<&2, String>:
652 chunk.decode.hold(chunk.live(s))
653
654def bytes.snd(r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes:
655 (a, b) = r
656 b
657
658def found.at(+from: U32, m: Maybe<&2, U32>) -> Maybe<&2, U32>:
659 match m:
660 case None{}:
661 None{}
662 case Some{+j}:
663 Some{(from + j : U32)}
664
665# A chunked body decoded from piece[i..]: a data run is sliced whole, and every other byte steps dc.
666type Cs is Type:
667 Cs{piece: Bytes.Bytes, i: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
668
669# st: where the decoder stopped. parts: the data so far, newest first. rest: the bytes after a Done body.
670type Ck is Type:
671 Ck{st: Dc, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
672
673def ck.next(+len: U32, +i: U32, +st: Dc, piece: Bytes.Bytes, parts: List<&1, Bytes.Bytes>) -> Bool & Cs:
674 (Bool.and(U32.is_lt(i, len), dc.live(st)), Cs{piece, i, st, parts})
675
676def ck.data(+len: U32, +i: U32, +k: U32, +m: U32, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Bool & Cs:
677 (piece, run) = r
678 ck.next(len, (i + m : U32), dc.data(k, m), piece, Con{run, parts})
679
680def ck.byte(+len: U32, +i: U32, st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Maybe<&2, U32>) -> Bool & Cs:
681 (piece, m) = r
682 match m:
683 case None{}:
684 ck.next(len, i, DcBad{}, piece, parts)
685 case Some{+c}:
686 ck.next(len, (i + 1 : U32), dc.step(st, c), piece, parts)
687
688def ck.step(+len: U32, cs: Cs) -> Bool & Cs:
689 Cs{piece, +i, st, parts} = cs
690 match st:
691 case DcData{+k}:
692 +m = U32.min(k, (len - i : U32))
693 ck.data(len, i, k, m, parts, Bytes.slice(piece, i, m))
694 case DcDone{}:
695 (False{}, Cs{piece, i, DcDone{}, parts})
696 case DcBad{}:
697 (False{}, Cs{piece, i, DcBad{}, parts})
698 case DcSize{+acc, seen}:
699 ck.byte(len, i, DcSize{acc, seen}, parts, Bytes.get(piece, i))
700 case DcExt{+n}:
701 ck.byte(len, i, DcExt{n}, parts, Bytes.get(piece, i))
702 case DcSizeLf{+n}:
703 ck.byte(len, i, DcSizeLf{n}, parts, Bytes.get(piece, i))
704 case DcDataCr{}:
705 ck.byte(len, i, DcDataCr{}, parts, Bytes.get(piece, i))
706 case DcDataLf{}:
707 ck.byte(len, i, DcDataLf{}, parts, Bytes.get(piece, i))
708 case DcTr{+j}:
709 ck.byte(len, i, DcTr{j}, parts, Bytes.get(piece, i))
710
711def ck.rest(st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Ck:
712 (piece, rest) = r
713 Ck{st, parts, rest}
714
715def ck.end(+len: U32, cs: Cs) -> Ck:
716 Cs{piece, +i, st, parts} = cs
717 ck.rest(st, parts, Bytes.slice(piece, i, (len - i : U32)))
718
719# Each step reads at least one byte, so len steps are enough.
720def ck.feed(f: Nat, +len: U32, r: Bool & Cs) -> Ck:
721 match f:
722 case 0n:
723 (go, cs) = r
724 ck.end(len, cs)
725 case 1n+p:
726 (go, cs) = r
727 match go:
728 case False{}:
729 ck.end(len, cs)
730 case True{}:
731 ck.feed(p, len, ck.step(len, cs))
732
733def ck(piece: Bytes.Bytes, +st: Dc, parts: List<&1, Bytes.Bytes>) -> Ck:
734 Bytes.Bytes{+len, buf} = piece
735 ck.feed(U32.to_nat(len), len, ck.next(len, 0, st, Bytes.Bytes{len, buf}, parts))
736
737def parse.res.cl.have(+rest: String, +k: Nat, short: Bool) -> Hold:
738 match short:
739 case True{}:
740 HoldMore{}
741 case False{}:
742 HoldBody{String.take(rest, k)}
743
744def parse.res.cl.k(+rest: String, +k: Nat) -> Hold:
745 parse.res.cl.have(rest, k, Nat.is_lt(String.length(rest), k))
746
747def parse.res.cl.n(rest: String, n: Maybe<&2, U32>) -> Hold:
748 match n:
749 case None{}:
750 HoldBad{}
751 case Some{k}:
752 parse.res.cl.k(rest, U32.to_nat(k))
753
754def parse.body.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
755 match hascl:
756 case False{}:
757 HoldBody{""}
758 case True{}:
759 parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
760
761# RFC 9112 §6.3 (4): a request coding other than chunked cannot be framed.
762def parse.body.chunked.eq(rest: String, ok: Bool) -> Hold:
763 match ok:
764 case False{}:
765 HoldBad{}
766 case True{}:
767 chunk.live(rest)
768
769def parse.body.chunked.val(te: String, rest: String) -> Hold:
770 parse.body.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
771
772def parse.body.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
773 match hascl:
774 case True{}:
775 HoldBad{}
776 case False{}:
777 parse.body.chunked.val(header.last(h, "transfer-encoding"), rest)
778
779def parse.body.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
780 match te:
781 case True{}:
782 parse.body.chunked(h, rest, has_header(h, "content-length"))
783 case False{}:
784 parse.body.cl(h, rest, has_header(h, "content-length"))
785
786def parse.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
787 parse.body.te(h, rest, has_header(h, "transfer-encoding"))
788
789# Bad: never a request. More: the head is not whole; read on. Head: the head is whole
790# and valid, and the body is still coming (req.body is empty). Req: a whole request.
791type Got is Type:
792 GotBad{}
793 GotMore{}
794 GotHead{req: Req}
795 GotReq{req: Req}
796
797def parse.finish(method: String, path: String, h: Map<&2, List<&2, String>>, body: Hold) -> Got:
798 match body:
799 case HoldBad{}:
800 GotBad{}
801 case HoldMore{}:
802 GotHead{Req{method, path, h, Bytes.new(0)}}
803 case HoldUntil{b}:
804 GotBad{}
805 case HoldBody{b}:
806 GotReq{Req{method, path, h, Bytes.from_string(b)}}
807
808def parse.host(method: String, path: String, +h: Map<&2, List<&2, String>>, rest: String, has: Bool) -> Got:
809 match has:
810 case False{}:
811 GotBad{}
812 case True{}:
813 parse.finish(method, path, h, parse.body(h, rest))
814
815# RFC 9112 §3.2: only HTTP/1.1 requires Host.
816def parse.fields(method: String, path: String, rest: String, v11: Bool, fs: Maybe<&2, Map<&2, List<&2, String>>>) -> Got:
817 match fs:
818 case None{}:
819 GotBad{}
820 case Some{+h}:
821 parse.host(method, path, h, rest, Bool.or(Bool.not(v11), has_header(h, "host")))
822
823def target_ok(+p: String) -> Bool:
824 Bool.or(String.starts_with(p, "/"), Bool.or(String.eq(p, "*"), String.starts_with(p, "http://")))
825
826def parse.target(method: String, +path: String, headers: String, rest: String, v11: Bool, ok: Bool) -> Got:
827 match ok:
828 case False{}:
829 GotBad{}
830 case True{}:
831 parse.fields(method, path, rest, v11, parse.headers.raw(headers))
832
833def parse.ver(method: String, +path: String, +v: String, headers: String, rest: String, ok: Bool) -> Got:
834 match ok:
835 case False{}:
836 GotBad{}
837 case True{}:
838 parse.target(method, path, headers, rest, String.eq(v, "HTTP/1.1"), target_ok(path))
839
840def parse.empty_method(method: String, path: String, +v: String, headers: String, rest: String, empty: Bool) -> Got:
841 match empty:
842 case True{}:
843 GotBad{}
844 case False{}:
845 parse.ver(method, path, v, headers, rest, Bool.or(String.eq(v, "HTTP/1.1"), String.eq(v, "HTTP/1.0")))
846
847def parse.start3(mpv: String & String & String, headers: String, rest: String) -> Got:
848 (+method, path, v) = mpv
849 parse.empty_method(method, path, v, headers, rest, String.is_empty(method))
850
851def parse.lines(lr: String & String, rest: String) -> Got:
852 (line, headers) = lr
853 parse.start3(start_line(line), headers, rest)
854
855
856def parse.head(+head: String, rest: String, whole: Bool) -> Got:
857 match whole:
858 case False{}:
859 GotMore{}
860 case True{}:
861 parse.lines(parse.first(head, SNil{}), rest)
862
863def parse.of(hb: String & String & Bool) -> Got:
864 (head, rest, whole) = hb
865 parse.head(head, rest, whole)
866
867# serve reads until this is not GotMore.
868def parse.got(+raw: String) -> Got:
869 parse.of(split_at_blank.flag.go(raw, raw, 0n, 0, False{}))
870
871
872def parse.req(g: Got) -> Maybe<&1, Req>:
873 match g:
874 case GotReq{req}:
875 Some{req}
876 case GotBad{}:
877 None{}
878 case GotMore{}:
879 None{}
880 case GotHead{req}:
881 None{}
882
883def parse(raw: String) -> Maybe<&1, Req>:
884 parse.req(parse.got(raw))
885
886def parse.res.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
887 match hascl:
888 case False{}:
889 HoldBody{rest}
890 case True{}:
891 parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
892
893def parse.res.chunked.eq(rest: String, ok: Bool) -> Hold:
894 match ok:
895 case False{}:
896 HoldUntil{rest}
897 case True{}:
898 chunk.live(rest)
899
900def parse.res.chunked.val(te: String, rest: String) -> Hold:
901 parse.res.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
902
903def parse.res.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
904 match hascl:
905 case True{}:
906 HoldBad{}
907 case False{}:
908 parse.res.chunked.val(header.last(h, "transfer-encoding"), rest)
909
910def parse.res.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
911 match te:
912 case True{}:
913 parse.res.chunked(h, rest, has_header(h, "content-length"))
914 case False{}:
915 parse.res.cl(h, rest, has_header(h, "content-length"))
916
917def parse.res.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
918 parse.res.te(h, rest, has_header(h, "transfer-encoding"))
919
920# Bad: never a message. More: a valid prefix; read on. Done: a whole response.
921type Frame is Type:
922 FrameBad{}
923 FrameMore{}
924 FrameDone{res: Res}
925
926# RFC 9112 §8: a message cut short by close is incomplete, not valid.
927def frame.cut(closed: Bool) -> Frame:
928 match closed:
929 case True{}:
930 FrameBad{}
931 case False{}:
932 FrameMore{}
933
934def frame.wait(res: Res, wait: Bool) -> Frame:
935 match wait:
936 case True{}:
937 FrameMore{}
938 case False{}:
939 FrameDone{res}
940
941def frame.done(status: U32, h: Map<&2, List<&2, String>>, body: Hold, +closed: Bool, open: Bool) -> Frame:
942 match body:
943 case HoldBad{}:
944 FrameBad{}
945 case HoldMore{}:
946 frame.cut(closed)
947 case HoldUntil{b}:
948 frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.not(closed))
949 case HoldBody{b}:
950 frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.and(open, Bool.not(closed)))
951
952# RFC 9112 §6.3 (8): no TE and no CL ⇒ the body runs until the server closes.
953def frame.open(+h: Map<&2, List<&2, String>>) -> Bool:
954 Bool.not(Bool.or(has_header(h, "transfer-encoding"), has_header(h, "content-length")))
955
956# RFC 9112 §6.3 (1): HEAD, 1xx, 204 and 304 responses end at the blank line.
957def frame.nobody(+status: U32, head: Bool) -> Bool:
958 Bool.or(head, Bool.or(U32.is_lt(status, 200), Bool.or(U32.is_eq(status, 204), U32.is_eq(status, 304))))
959
960# 101 is the final response. Other 1xx are interim; a final response follows.
961def frame.interim(+status: U32) -> Bool:
962 Bool.and(U32.is_lt(status, 200), Bool.not(U32.is_eq(status, 101)))
963
964def frame.status(status: U32, +h: Map<&2, List<&2, String>>, rest: String, closed: Bool, nobody: Bool) -> Frame:
965 match nobody:
966 case True{}:
967 FrameDone{Res{status, h, Bytes.new(0)}}
968 case False{}:
969 frame.done(status, h, parse.res.body(h, rest), closed, frame.open(h))
970
971def parse.res.fields(+status: U32, rest: String, fs: Maybe<&2, Map<&2, List<&2, String>>>, closed: Bool, head: Bool) -> Frame:
972 match fs:
973 case None{}:
974 FrameBad{}
975 case Some{h}:
976 frame.status(status, h, rest, closed, frame.nobody(status, head))
977
978def parse.res.num(code: Maybe<&2, U32>, headers: String, rest: String, closed: Bool, head: Bool) -> Frame:
979 match code:
980 case None{}:
981 FrameBad{}
982 case Some{n}:
983 parse.res.fields(n, rest, parse.headers.raw(headers), closed, head)
984
985def parse.res.ver(code: String, headers: String, rest: String, closed: Bool, head: Bool, ok: Bool) -> Frame:
986 match ok:
987 case False{}:
988 FrameBad{}
989 case True{}:
990 parse.res.num(parse_u32(code), headers, rest, closed, head)
991
992def parse.res.start3(mpv: String & String & String, headers: String, rest: String, closed: Bool, head: Bool) -> Frame:
993 (+ver, code, reason) = mpv
994 parse.res.ver(code, headers, rest, closed, head, Bool.or(String.eq(ver, "HTTP/1.1"), String.eq(ver, "HTTP/1.0")))
995
996def parse.res.lines(lr: String & String, rest: String, closed: Bool, head: Bool) -> Frame:
997 (line, headers) = lr
998 parse.res.start3(start_line(line), headers, rest, closed, head)
999
1000def parse.res.blank(hd: String, rest: String, +closed: Bool, head: Bool, ok: Bool) -> Frame:
1001 match ok:
1002 case False{}:
1003 frame.cut(closed)
1004 case True{}:
1005 parse.res.lines(parse.first(hd, SNil{}), rest, closed, head)
1006
1007def parse.res.of(hb: String & String, closed: Bool, head: Bool) -> Frame:
1008 (+hd, rest) = hb
1009 parse.res.blank(hd, rest, closed, head, blank_end(hd))
1010
1011type Lead is Data:
1012 LeadCut{}
1013 LeadFinal{}
1014 LeadSkip{+rest: String}
1015
1016def frame.lead.if(rest: String, interim: Bool) -> Lead:
1017 match interim:
1018 case True{}:
1019 LeadSkip{rest}
1020 case False{}:
1021 LeadFinal{}
1022
1023def frame.lead.num(n: Maybe<&2, U32>, rest: String) -> Lead:
1024 match n:
1025 case None{}:
1026 LeadFinal{}
1027 case Some{s}:
1028 frame.lead.if(rest, frame.interim(s))
1029
1030def frame.lead.code(mpv: String & String & String, rest: String) -> Lead:
1031 (ver, code, reason) = mpv
1032 frame.lead.num(parse_u32(code), rest)
1033
1034def frame.lead.lines(xs: List<&2, String>, rest: String) -> Lead:
1035 match xs:
1036 case Nil{}:
1037 LeadFinal{}
1038 case Con{line, headers}:
1039 frame.lead.code(start_line(line), rest)
1040
1041def frame.lead.blank(+hd: String, rest: String, ok: Bool) -> Lead:
1042 match ok:
1043 case False{}:
1044 LeadCut{}
1045 case True{}:
1046 frame.lead.lines(String.lines(hd), rest)
1047
1048def frame.lead(hb: String & String) -> Lead:
1049 (+hd, rest) = hb
1050 frame.lead.blank(hd, rest, blank_end(hd))
1051
1052def frame.at.cont(+raw: String, lead: Lead) -> String:
1053 match lead:
1054 case LeadCut{}:
1055 raw
1056 case LeadFinal{}:
1057 raw
1058 case LeadSkip{rest}:
1059 rest
1060
1061def frame.at.zero.go(+raw: String, closed: Bool, head: Bool, lead: Lead) -> Frame:
1062 match lead:
1063 case LeadCut{}:
1064 frame.cut(closed)
1065 case LeadFinal{}:
1066 parse.res.of(split_at_blank(raw), closed, head)
1067 case LeadSkip{rest}:
1068 FrameBad{}
1069
1070def frame.at.zero.of(+raw: String, closed: Bool, head: Bool) -> Frame:
1071 frame.at.zero.go(raw, closed, head, frame.lead(split_at_blank(raw)))
1072
1073def frame.at.pos.do(f: Nat, +raw: String, closed: Bool, head: Bool, hb: String & String, lead: Lead) -> Frame:
1074 match f:
1075 case 0n:
1076 match lead:
1077 case LeadCut{}:
1078 frame.cut(closed)
1079 case LeadFinal{}:
1080 parse.res.of(hb, closed, head)
1081 case LeadSkip{+rest}:
1082 frame.at.zero.of(rest, closed, head)
1083 case 1n+g:
1084 match lead:
1085 case LeadCut{}:
1086 frame.cut(closed)
1087 case LeadFinal{}:
1088 parse.res.of(hb, closed, head)
1089 case LeadSkip{+rest}:
1090 frame.at.pos.do(g, rest, closed, head, split_at_blank(rest), frame.lead(split_at_blank(rest)))
1091
1092def frame.at.zero(+raw: String, closed: Bool, head: Bool) -> Frame:
1093 frame.at.zero.of(raw, closed, head)
1094
1095# ponytail: 8 interim responses; raise the fuel if a server sends more
1096def frame.at(fuel: Nat, +raw: String, closed: Bool, head: Bool) -> Frame:
1097 match fuel:
1098 case 0n:
1099 frame.at.zero(raw, closed, head)
1100 case 1n+f:
1101 frame.at.pos.do(f, raw, closed, head, split_at_blank(raw), frame.lead(split_at_blank(raw)))
1102
1103# frame(bytes so far, server closed?, request was HEAD?)
1104def frame(raw: String, closed: Bool, head: Bool) -> Frame:
1105 frame.at(8n, raw, closed, head)
1106
1107def frame.res(f: Frame) -> Maybe<&1, Res>:
1108 match f:
1109 case FrameDone{res}:
1110 Some{res}
1111 case FrameBad{}:
1112 None{}
1113 case FrameMore{}:
1114 None{}
1115
1116def parse_res(raw: String) -> Maybe<&1, Res>:
1117 frame.res(frame(raw, True{}, False{}))
1118
1119def res_fields.res(res: Res, k: String) -> List<&2, String>:
1120 Res{status, headers, body} = res
1121 fields(headers, k)
1122
1123def res_fields(m: Maybe<&1, Res>, k: String) -> List<&2, String>:
1124 match m:
1125 case None{}:
1126 Nil{}
1127 case Some{res}:
1128 res_fields.res(res, k)
1129
1130# The response body as it arrives. Len: bytes left. Chunk: the decoder. Close: until the
1131# server closes. Done: the body is whole. Bad: it cannot become a body.
1132type Rb is Data:
1133 RbLen{left: U32}
1134 RbChunk{st: Dc}
1135 RbClose{}
1136 RbDone{}
1137 RbBad{}
1138
1139def rb.cl(n: Maybe<&2, U32>) -> Maybe<&2, Rb>:
1140 match n:
1141 case None{}:
1142 None{}
1143 case Some{+k}:
1144 Some{Bool.pick(Rb, U32.is_zero(k), RbDone{}, RbLen{k})}
1145
1146def rb.te(+h: Map<&2, List<&2, String>>, cl: Bool) -> Maybe<&2, Rb>:
1147 match cl:
1148 case True{}:
1149 None{}
1150 case False{}:
1151 Some{Bool.pick(Rb, String.eq(String.to_lower(header.last(h, "transfer-encoding")), "chunked"), RbChunk{dc.start()}, RbClose{})}
1152
1153def rb.len(+h: Map<&2, List<&2, String>>, te: Bool) -> Maybe<&2, Rb>:
1154 match te:
1155 case True{}:
1156 rb.te(h, has_header(h, "content-length"))
1157 case False{}:
1158 Bool.pick(Maybe<&2, Rb>, has_header(h, "content-length"), rb.cl(parse_u32(header(h, "content-length"))), Some{RbClose{}})
1159
1160# RFC 9112 §6.3: how the body of this response ends. None: it cannot be framed.
1161def rb.of(+h: Map<&2, List<&2, String>>, nobody: Bool) -> Maybe<&2, Rb>:
1162 match nobody:
1163 case True{}:
1164 Some{RbDone{}}
1165 case False{}:
1166 rb.len(h, has_header(h, "transfer-encoding"))
1167
1168# rb: how the body goes on. parts: body bytes so far, newest first. rest: bytes past a Done body.
1169type Bf is Type:
1170 Bf{rb: Rb, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
1171
1172def rb.len.cut(parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Bf:
1173 (piece, data) = r
1174 Bf{RbDone{}, Con{data, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32)))}
1175
1176def rb.len.have(short: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Bf:
1177 match short:
1178 case True{}:
1179 Bf{RbLen{(left - len : U32)}, Con{piece, parts}, Bytes.new(0)}
1180 case False{}:
1181 rb.len.cut(parts, len, left, Bytes.slice(piece, 0, left))
1182
1183def rb.chunk(c: Ck) -> Bf:
1184 Ck{st, parts, rest} = c
1185 match st:
1186 case DcDone{}:
1187 Bf{RbDone{}, parts, rest}
1188 case DcBad{}:
1189 Bf{RbBad{}, parts, rest}
1190 case DcSize{a, b}:
1191 Bf{RbChunk{DcSize{a, b}}, parts, rest}
1192 case DcExt{x}:
1193 Bf{RbChunk{DcExt{x}}, parts, rest}
1194 case DcSizeLf{x}:
1195 Bf{RbChunk{DcSizeLf{x}}, parts, rest}
1196 case DcData{k}:
1197 Bf{RbChunk{DcData{k}}, parts, rest}
1198 case DcDataCr{}:
1199 Bf{RbChunk{DcDataCr{}}, parts, rest}
1200 case DcDataLf{}:
1201 Bf{RbChunk{DcDataLf{}}, parts, rest}
1202 case DcTr{j}:
1203 Bf{RbChunk{DcTr{j}}, parts, rest}
1204
1205# The body bytes in piece, added to parts.
1206def rb.feed(rb: Rb, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Bf:
1207 match rb:
1208 case RbLen{+left}:
1209 Bytes.Bytes{+len, buf} = piece
1210 rb.len.have(U32.is_lt(len, left), left, parts, len, Bytes.Bytes{len, buf})
1211 case RbChunk{st}:
1212 rb.chunk(ck(piece, st, parts))
1213 case RbClose{}:
1214 Bf{RbClose{}, Con{piece, parts}, Bytes.new(0)}
1215 case RbDone{}:
1216 Bf{RbDone{}, parts, piece}
1217 case RbBad{}:
1218 Bf{RbBad{}, parts, piece}
1219
1220# RFC 9112 §8: only a close-delimited body may end at close.
1221def rb.eof(rb: Rb) -> Bool:
1222 match rb:
1223 case RbClose{}:
1224 True{}
1225 case RbDone{}:
1226 True{}
1227 case RbLen{n}:
1228 False{}
1229 case RbChunk{st}:
1230 False{}
1231 case RbBad{}:
1232 False{}
1233
1234def rb.body(parts: List<&1, Bytes.Bytes>) -> Bytes.Bytes:
1235 Bytes.concat(List.reverse(&1, Bytes.Bytes, parts))
1236
1237# The head scan. Seek: look for the blank line from byte from; k interim heads are behind.
1238# Wait: no blank line yet. Res: the final head, how its body ends, and the bytes after it.
1239type Hs is Type:
1240 HsSeek{buf: Bytes.Bytes, from: U32, k: U32}
1241 HsWait{buf: Bytes.Bytes, k: U32}
1242 HsBad{}
1243 HsRes{res: Res, rb: Rb, rest: Bytes.Bytes}
1244
1245def hs.final(+status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes, m: Maybe<&2, Rb>) -> Hs:
1246 match m:
1247 case None{}:
1248 HsBad{}
1249 case Some{rb}:
1250 HsRes{Res{status, h, Bytes.new(0)}, rb, rest}
1251
1252def hs.skip(more: Bool, +k: U32, rest: Bytes.Bytes) -> Hs:
1253 match more:
1254 case True{}:
1255 HsSeek{rest, 0, (k + 1 : U32)}
1256 case False{}:
1257 HsBad{}
1258
1259def hs.pick(interim: Bool, +head: Bool, +k: U32, +status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes) -> Hs:
1260 match interim:
1261 case True{}:
1262 hs.skip(U32.is_lt(k, 8), k, rest)
1263 case False{}:
1264 hs.final(status, h, rest, rb.of(h, frame.nobody(status, head)))
1265
1266def hs.res(+head: Bool, +k: U32, rest: Bytes.Bytes, res: Res) -> Hs:
1267 Res{+status, +h, body} = res
1268 hs.pick(frame.interim(status), head, k, status, h, rest)
1269
1270# The head alone, framed as a HEAD response so it stops at the blank line.
1271def hs.parsed(+head: Bool, +k: U32, rest: Bytes.Bytes, f: Frame) -> Hs:
1272 match f:
1273 case FrameDone{res}:
1274 hs.res(head, k, rest, res)
1275 case FrameBad{}:
1276 HsBad{}
1277 case FrameMore{}:
1278 HsBad{}
1279
1280def hs.split(+head: Bool, +k: U32, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1281 (buf, hb) = r
1282 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{}))
1283
1284def hs.hit(+head: Bool, +k: U32, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Hs:
1285 match at:
1286 case None{}:
1287 HsWait{buf, k}
1288 case Some{+i}:
1289 +hlen = (i + 4 : U32)
1290 hs.split(head, k, hlen, len, Bytes.slice(buf, 0, hlen))
1291
1292def hs.seek.of(+head: Bool, +k: U32, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Hs:
1293 (tail, m) = r
1294 hs.hit(head, k, len, buf, found.at(from, m))
1295
1296def hs.seek(+head: Bool, +k: U32, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1297 (buf, tail) = r
1298 hs.seek.of(head, k, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
1299
1300def hs.step(+head: Bool, st: Hs) -> Hs:
1301 match st:
1302 case HsSeek{buf, +from, +k}:
1303 Bytes.Bytes{+len, b} = buf
1304 hs.seek(head, k, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
1305 case HsWait{buf, k}:
1306 HsWait{buf, k}
1307 case HsBad{}:
1308 HsBad{}
1309 case HsRes{res, rb, rest}:
1310 HsRes{res, rb, rest}
1311
1312# Each step ends the scan or passes one interim head, and at most 8 interim heads pass.
1313def hs.scan(fuel: Nat, +head: Bool, st: Hs) -> Hs:
1314 match fuel:
1315 case 0n:
1316 match st:
1317 case HsSeek{buf, from, k}:
1318 HsBad{}
1319 case HsWait{buf, k}:
1320 HsWait{buf, k}
1321 case HsBad{}:
1322 HsBad{}
1323 case HsRes{res, rb, rest}:
1324 HsRes{res, rb, rest}
1325 case 1n+f:
1326 hs.scan(f, head, hs.step(head, st))
1327
1328# piece joins buf; only the new bytes, and the 3 before them, can finish the blank line.
1329def hs.more(+head: Bool, +k: U32, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Hs:
1330 Bytes.Bytes{+ol, ob} = buf
1331 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})
1332
1333# Untrusted servers must not grow the buffer without bound.
1334def fetch.max() -> Nat:
1335 U32.to_nat(16777216)
1336
1337# A response read in pieces. Head: the head is not whole yet. Body: it is, and parts is the body so far.
1338# Len: a Content-Length body in one buffer of that size, with left bytes still to come.
1339type Rv is Type:
1340 RvHead{buf: Bytes.Bytes, k: U32}
1341 RvBody{res: Res, rb: Rb, parts: List<&1, Bytes.Bytes>}
1342 RvLen{res: Res, left: U32, body: Bytes.Bytes}
1343
1344# More: read on. Done: the response, and the bytes after it when the body is self-delimited.
1345type Rt is Type:
1346 RtMore{rv: Rv}
1347 RtBad{}
1348 RtDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1349
1350def rv.start() -> Rv:
1351 RvHead{Bytes.new(0), 0}
1352
1353def rv.whole(res: Res, b: Bytes.Bytes, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1354 Res{status, headers, body} = res
1355 RtDone{Res{status, headers, b}, rest}
1356
1357def rv.done(res: Res, parts: List<&1, Bytes.Bytes>, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1358 rv.whole(res, rb.body(parts), rest)
1359
1360def rl.put.of(+total: U32, +len: U32, r: Array<U32> & Array<U32>) -> Bytes.Bytes & Bytes.Bytes:
1361 (src, dst) = r
1362 (Bytes.Bytes{total, dst}, Bytes.Bytes{len, src})
1363
1364# The first m bytes of piece, written into body after the total - left bytes already there.
1365def rl.put(+m: U32, +left: U32, body: Bytes.Bytes, piece: Bytes.Bytes) -> Bytes.Bytes & Bytes.Bytes:
1366 Bytes.Bytes{+total, dst} = body
1367 Bytes.Bytes{+len, src} = piece
1368 rl.put.of(total, len, Bytes.copy(m, src, dst, 0, (total - left : U32)))
1369
1370def rl.fed(short: Bool, res: Res, +left: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Rt:
1371 match short:
1372 case True{}:
1373 (body, piece) = r
1374 RtMore{RvLen{res, (left - len : U32), body}}
1375 case False{}:
1376 (body, piece) = r
1377 rv.whole(res, body, Some{bytes.snd(Bytes.slice(piece, left, (len - left : U32)))})
1378
1379def rl.feed(res: Res, +left: U32, body: Bytes.Bytes, piece: Bytes.Bytes) -> Rt:
1380 Bytes.Bytes{+len, buf} = piece
1381 rl.fed(U32.is_lt(len, left), res, left, len, rl.put(U32.min(len, left), left, body, Bytes.Bytes{len, buf}))
1382
1383def rv.fed(res: Res, bf: Bf) -> Rt:
1384 Bf{rb, parts, rest} = bf
1385 match rb:
1386 case RbDone{}:
1387 rv.done(res, parts, Some{rest})
1388 case RbBad{}:
1389 RtBad{}
1390 case RbLen{n}:
1391 RtMore{RvBody{res, RbLen{n}, parts}}
1392 case RbChunk{st}:
1393 RtMore{RvBody{res, RbChunk{st}, parts}}
1394 case RbClose{}:
1395 RtMore{RvBody{res, RbClose{}, parts}}
1396
1397# Some{left}: a Content-Length body small enough to allocate up front. Larger ones fail at the fetch cap.
1398def rb.buf(rb: Rb) -> Maybe<&2, U32>:
1399 match rb:
1400 case RbLen{+left}:
1401 Bool.pick(Maybe<&2, U32>, Nat.is_lt(fetch.max(), U32.to_nat(left)), None{}, Some{left})
1402 case RbChunk{st}:
1403 None{}
1404 case RbClose{}:
1405 None{}
1406 case RbDone{}:
1407 None{}
1408 case RbBad{}:
1409 None{}
1410
1411def rv.body(m: Maybe<&2, U32>, res: Res, rb: Rb, rest: Bytes.Bytes) -> Rt:
1412 match m:
1413 case None{}:
1414 rv.fed(res, rb.feed(rb, Nil{}, rest))
1415 case Some{+left}:
1416 rl.feed(res, left, Bytes.new(left), rest)
1417
1418def rv.head(hs: Hs) -> Rt:
1419 match hs:
1420 case HsWait{buf, k}:
1421 RtMore{RvHead{buf, k}}
1422 case HsBad{}:
1423 RtBad{}
1424 case HsSeek{buf, from, k}:
1425 RtBad{}
1426 case HsRes{res, +rb, rest}:
1427 rv.body(rb.buf(rb), res, rb, rest)
1428
1429def rv.eof(res: Res, parts: List<&1, Bytes.Bytes>, ok: Bool) -> Rt:
1430 match ok:
1431 case True{}:
1432 rv.done(res, parts, None{})
1433 case False{}:
1434 RtBad{}
1435
1436# One read: piece, or the server closed (RFC 9112 §8: a message cut short is not a message).
1437def rv.step(closed: Bool, +head: Bool, rv: Rv, piece: Bytes.Bytes) -> Rt:
1438 match closed:
1439 case True{}:
1440 match rv:
1441 case RvHead{buf, k}:
1442 RtBad{}
1443 case RvBody{res, rb, parts}:
1444 rv.eof(res, parts, rb.eof(rb))
1445 case RvLen{res, left, body}:
1446 RtBad{}
1447 case False{}:
1448 match rv:
1449 case RvHead{buf, +k}:
1450 rv.head(hs.more(head, k, buf, piece))
1451 case RvBody{res, rb, parts}:
1452 rv.fed(res, rb.feed(rb, parts, piece))
1453 case RvLen{res, +left, body}:
1454 rl.feed(res, left, body, piece)
1455
1456def rv.end(closed: Bool, +head: Bool, t: Rt) -> Rt:
1457 match closed:
1458 case False{}:
1459 t
1460 case True{}:
1461 match t:
1462 case RtMore{rv}:
1463 rv.step(True{}, head, rv, Bytes.new(0))
1464 case RtBad{}:
1465 RtBad{}
1466 case RtDone{res, rest}:
1467 RtDone{res, rest}
1468
1469def rv.go(xs: List<&2, String>, closed: Bool, +head: Bool, t: Rt) -> Rt:
1470 match xs:
1471 case Nil{}:
1472 rv.end(closed, head, t)
1473 case Con{+x, rest}:
1474 match t:
1475 case RtMore{rv}:
1476 rv.go(rest, closed, head, rv.step(False{}, head, rv, Bytes.from_string(x)))
1477 case RtBad{}:
1478 RtBad{}
1479 case RtDone{res, r}:
1480 RtDone{res, r}
1481
1482def rt.frame(t: Rt) -> Frame:
1483 match t:
1484 case RtMore{rv}:
1485 FrameMore{}
1486 case RtBad{}:
1487 FrameBad{}
1488 case RtDone{res, rest}:
1489 FrameDone{res}
1490
1491# What the read loop makes of these pieces, then a close when closed is set.
1492def res.frame(xs: List<&2, String>, closed: Bool, +head: Bool) -> Frame:
1493 rt.frame(rv.go(xs, closed, head, RtMore{rv.start()}))
1494
1495def rt.rest(t: Rt) -> Maybe<&1, Bytes.Bytes>:
1496 match t:
1497 case RtMore{rv}:
1498 None{}
1499 case RtBad{}:
1500 None{}
1501 case RtDone{res, rest}:
1502 rest
1503
1504def after.of(m: Maybe<&1, Bytes.Bytes>) -> Maybe<&2, String>:
1505 match m:
1506 case None{}:
1507 None{}
1508 case Some{b}:
1509 Some{Bytes.to_string(b)}
1510
1511# Bytes after a complete self-delimited message. None if it is not one yet.
1512def after(+raw: String, +head: Bool) -> Maybe<&2, String>:
1513 after.of(rt.rest(rv.go([raw], False{}, head, RtMore{rv.start()})))
1514
1515def req.v11.ver(mpv: String & String & String) -> Bool:
1516 (+method, path, v) = mpv
1517 String.eq(v, "HTTP/1.1")
1518
1519def req.v11.line(+line: String) -> Bool:
1520 req.v11.ver(start_line(line))
1521
1522def req.v11.lines(xs: List<&2, String>) -> Bool:
1523 match xs:
1524 case Nil{}:
1525 False{}
1526 case Con{line, headers}:
1527 req.v11.line(line)
1528
1529def req.v11.pick(+head: String, ok: Bool) -> Bool:
1530 match ok:
1531 case False{}:
1532 False{}
1533 case True{}:
1534 req.v11.lines(String.lines(head))
1535
1536def req.v11.of(hb: String & String) -> Bool:
1537 (+head, rest) = hb
1538 req.v11.pick(head, blank_end(head))
1539
1540def req.v11(+raw: String) -> Bool:
1541 req.v11.of(split_at_blank(raw))
1542
1543def req.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1544 String.eq(String.to_lower(header(headers, "connection")), "close")
1545
1546def res.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1547 String.eq(String.to_lower(header(headers, "connection")), "close")
1548
1549def serve.fail_close(+status: U32) -> Bool:
1550 Bool.or(U32.is_eq(status, 400), Bool.or(U32.is_eq(status, 413), U32.is_eq(status, 431)))
1551
1552def serve.keep.ok(fail: Bool, res_close: Bool) -> Bool:
1553 match fail:
1554 case True{}:
1555 False{}
1556 case False{}:
1557 Bool.not(res_close)
1558
1559def serve.keep.v11(v11: Bool, +req_close: Bool, +status: U32, res_close: Bool) -> Bool:
1560 match v11:
1561 case False{}:
1562 False{}
1563 case True{}:
1564 match req_close:
1565 case True{}:
1566 False{}
1567 case False{}:
1568 serve.keep.ok(serve.fail_close(status), res_close)
1569
1570def serve.keep(+headers: Map<&2, List<&2, String>>, v11: Bool, +status: U32, +res: Map<&2, List<&2, String>>) -> Bool:
1571 serve.keep.v11(v11, req.conn_close(headers), status, res.conn_close(res))
1572
1573
1574def again.keep(close: Bool, x: Bytes.Bytes) -> Maybe<&1, Bytes.Bytes>:
1575 match close:
1576 case True{}:
1577 None{}
1578 case False{}:
1579 Some{x}
1580
1581def again.rest(close: Bool, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1582 match rest:
1583 case None{}:
1584 None{}
1585 case Some{x}:
1586 again.keep(close, x)
1587
1588# The bytes past the response when the socket can take another request: the request did not
1589# ask to close, the response is self-delimited, and the peer did not say close.
1590def again(close: Bool, +h: Map<&2, List<&2, String>>, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1591 match close:
1592 case True{}:
1593 None{}
1594 case False{}:
1595 again.rest(String.eq(String.to_lower(header(h, "connection")), "close"), rest)
1596
1597def res_body.res(res: Res) -> Bytes.Bytes:
1598 Res{status, headers, body} = res
1599 body
1600
1601def res_body(m: Maybe<&1, Res>) -> Bytes.Bytes:
1602 match m:
1603 case None{}:
1604 Bytes.new(0)
1605 case Some{res}:
1606 res_body.res(res)
1607
1608def text(res: Res) -> String:
1609 Enc.utf8.decode(res_body.res(res))
1610
1611# UTF-8 is checked, not repaired: bad UTF-8 in a string gives None (RFC 8259 §8.1).
1612def json(res: Res) -> Maybe<&1, Json.Val>:
1613 Json.parse.bytes(res_body.res(res))
1614
1615def got_body.req(req: Req) -> Bytes.Bytes:
1616 Req{method, path, headers, body} = req
1617 body
1618
1619def got_body(m: Maybe<&1, Req>) -> Bytes.Bytes:
1620 match m:
1621 case None{}:
1622 Bytes.new(0)
1623 case Some{req}:
1624 got_body.req(req)
1625
1626def body.of(hb: String & String) -> String:
1627 (h, b) = hb
1628 b
1629
1630def body(s: String) -> String:
1631 body.of(split_at_blank.go(s, False{}, 0, SNil{}))
1632
1633def headers_lines(+k: String, vs: List<&2, String>, acc: String) -> String:
1634 match vs:
1635 case Nil{}:
1636 acc
1637 case Con{v, t}:
1638 headers_lines(k, t, acc ++ ("\r\n" ++ sanitize(k) ++ ": " ++ sanitize(v)))
1639
1640def headers_block.go(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, acc: String) -> String:
1641 match xs:
1642 case Nil{}:
1643 acc
1644 case (k, vs) <> t:
1645 headers_block.go(t, headers_lines(k, vs, acc))
1646
1647def headers_block(h: Map<&2, List<&2, String>>) -> String:
1648 headers_block.go(Map.to_list(&2, List<&2, String>, h), "")
1649
1650# RFC 9110 §15. An unknown code gets an empty reason, which RFC 9112 §4 allows.
1651type Reason is Data:
1652 Reason{code: U32, text: String}
1653
1654def reasons() -> List<&2, Reason>:
1655 [Reason{100, "Continue"}, Reason{101, "Switching Protocols"}, Reason{103, "Early Hints"},
1656 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"},
1657 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"},
1658 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"},
1659 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"}]
1660
1661def reason.go(xs: List<&2, Reason>, +status: U32) -> String:
1662 match xs:
1663 case Nil{}:
1664 ""
1665 case Con{Reason{k, v}, t}:
1666 Bool.pick(String, U32.is_eq(k, status), v, reason.go(t, status))
1667
1668def reason(+status: U32) -> String:
1669 reason.go(reasons(), status)
1670
1671def response(+status: U32, headers: Map<&2, List<&2, String>>, body: String) -> String:
1672 ("HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1673
1674def encode.body(head: Bool, top: Bytes.Bytes, body: Bytes.Bytes) -> Bytes.Bytes:
1675 match head:
1676 case True{}:
1677 top
1678 case False{}:
1679 Bytes.append(top, body)
1680
1681def encode.len(+status: U32, headers: Map<&2, List<&2, String>>, head: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1682 Bytes.Bytes{+len, buf} = body
1683 encode.body(head, Bytes.from_string(response(status, set(headers, "content-length", U32.show(len)), "")), Bytes.Bytes{len, buf})
1684
1685# RFC 9110 §6.4.1, §8.6: 1xx, 204 and 304 have no body; HEAD gets the length but no body.
1686def encode.pick(+status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, head: Bool, nobody: Bool) -> Bytes.Bytes:
1687 match nobody:
1688 case True{}:
1689 Bytes.from_string(response(status, headers, ""))
1690 case False{}:
1691 encode.len(status, headers, head, body)
1692
1693def encode.on(r: Res, head: Bool) -> Bytes.Bytes:
1694 Res{+status, headers, body} = r
1695 encode.pick(status, headers, body, head, frame.nobody(status, False{}))
1696
1697def encode(r: Res) -> Bytes.Bytes:
1698 encode.on(r, False{})
1699
1700def request(method: String, path: String, headers: Map<&2, List<&2, String>>, body: String) -> String:
1701 (method ++ " " ++ path ++ " HTTP/1.1" ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1702
1703def req.reserved(+k: String) -> Bool:
1704 Bool.or(Bool.or(String.eq(k, "host"), String.eq(k, "connection")), Bool.or(String.eq(k, "content-length"), String.eq(k, "transfer-encoding")))
1705
1706def req.put.one(m: Map<&2, List<&2, String>>, +k: String, vs: List<&2, String>, skip: Bool) -> Map<&2, List<&2, String>>:
1707 match skip:
1708 case True{}:
1709 m
1710 case False{}:
1711 Map.set(&2, List<&2, String>, m, k, vs)
1712
1713def req.put(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1714 match xs:
1715 case Nil{}:
1716 m
1717 case (k, vs) <> t:
1718 +lk = String.to_lower(k)
1719 req.put(t, req.put.one(m, lk, vs, req.reserved(lk)))
1720
1721# RFC 9110 §8.6: no Content-Length on a bodiless request whose method gives a body no meaning.
1722def req.cl(+m: Map<&2, List<&2, String>>, +method: String, +len: U32) -> Map<&2, List<&2, String>>:
1723 +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"))))
1724 Bool.pick(Map<&2, List<&2, String>>, bodied, set(m, "content-length", U32.show(len)), m)
1725
1726# Caller headers are lowercased so they cannot duplicate ours; host, connection,
1727# content-length and transfer-encoding are always ours (no smuggling through them).
1728def encode_req.word(close: Bool) -> String:
1729 match close:
1730 case True{}:
1731 "close"
1732 case False{}:
1733 "keep-alive"
1734
1735def encode_req.on(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, close: Bool) -> Bytes.Bytes:
1736 Bytes.Bytes{+len, buf} = body
1737 +h = set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", host), "connection", encode_req.word(close))
1738 Bytes.append(Bytes.from_string(request(method, target, req.cl(h, method, len), "")), Bytes.Bytes{len, buf})
1739
1740def encode_req(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Bytes.Bytes:
1741 encode_req.on(method, target, host, headers, body, True{})
1742
1743# Redirects (RFC 9110 §15.4, as WHATWG fetch applies them)
1744# --------------------------------------------------------
1745
1746# One request to make: headers are already lowercased (see req.put).
1747type Hop is Type:
1748 Hop{method: String, url: Url.Abs, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
1749
1750def redirect.code(+s: U32) -> Bool:
1751 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))))
1752
1753def redirect.origin(a: Url.Abs) -> String:
1754 Url.Abs{scheme, host, port, target} = a
1755 scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1756
1757def redirect.del(ks: List<&2, String>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1758 match ks:
1759 case Nil{}:
1760 m
1761 case Con{k, t}:
1762 redirect.del(t, Map.del(&2, List<&2, String>, m, k))
1763
1764def redirect.hdrs(+h: Map<&2, List<&2, String>>, drop: Bool, cross: Bool) -> Map<&2, List<&2, String>>:
1765 +h2 = Bool.pick(Map<&2, List<&2, String>>, drop, redirect.del(["content-type", "content-encoding", "content-language", "content-location"], h), h)
1766 Bool.pick(Map<&2, List<&2, String>>, cross, redirect.del(["authorization", "cookie", "proxy-authorization"], h2), h2)
1767
1768# 303 turns any method but HEAD into GET; 301 and 302 turn POST into GET;
1769# 307 and 308 keep method and body. A GET carries no body or body headers.
1770# Credentials do not follow a hop to another origin.
1771def redirect.body(drop: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1772 match drop:
1773 case True{}:
1774 Bytes.new(0)
1775 case False{}:
1776 body
1777
1778def 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>:
1779 match next:
1780 case None{}:
1781 None{}
1782 case Some{+to}:
1783 +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")))
1784 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)}}
1785
1786def redirect.hop(status: U32, h: Hop, loc: String) -> Maybe<&1, Hop>:
1787 Hop{method, +url, headers, body} = h
1788 redirect.to(status, method, url, headers, body, Url.resolve(url, loc))
1789
1790def redirect.if(status: U32, h: Hop, loc: String, ok: Bool) -> Maybe<&1, Hop>:
1791 match ok:
1792 case False{}:
1793 None{}
1794 case True{}:
1795 redirect.hop(status, h, loc)
1796
1797# The next request after a response, or None when it is not a redirect we follow.
1798def redirect(+status: U32, +headers: Map<&2, List<&2, String>>, h: Hop) -> Maybe<&1, Hop>:
1799 redirect.if(status, h, header(headers, "location"), Bool.and(redirect.code(status), has_header(headers, "location")))
1800
1801# Cookies (RFC 6265bis §5)
1802# ------------------------
1803
1804# A stored cookie. domain is lowercase, with no leading dot; host_only sends it to that host alone.
1805# expiry None is a session cookie. http_only and same_site ("strict", "lax", "none" or "default")
1806# are kept, not enforced: fetch has no browsing client, so its requests are same-site (§5.2).
1807type Cookie is Data:
1808 Cookie{name: String, value: String, domain: String, host_only: Bool, path: String, secure: Bool, http_only: Bool, same_site: String, expiry: Maybe<&2, Time.Instant>}
1809
1810# The cookies, oldest first, and the caller's clock. No cookie in it has expired by now.
1811type Jar is Data:
1812 Jar{now: Time.Instant, cookies: List<&2, Cookie>}
1813
1814def jar.new(now: Time.Instant) -> Jar:
1815 Jar{now, Nil{}}
1816
1817def jar.cookies(j: Jar) -> List<&2, Cookie>:
1818 Jar{now, cs} = j
1819 cs
1820
1821def cookie.live.at(+now: Time.Instant, e: Maybe<&2, Time.Instant>) -> Bool:
1822 match e:
1823 case None{}:
1824 True{}
1825 case Some{t}:
1826 Cmp.is_lt(Time.Instant.cmp(now, t))
1827
1828# Alive at now: no expiry, or an expiry after now.
1829def cookie.live(+now: Time.Instant, c: Cookie) -> Bool:
1830 Cookie{name, value, domain, host_only, path, secure, http_only, same_site, expiry} = c
1831 cookie.live.at(now, expiry)
1832
1833def jar.live(cs: List<&2, Cookie>, +now: Time.Instant) -> List<&2, Cookie>:
1834 match cs:
1835 case Nil{}:
1836 Nil{}
1837 case Con{+c, t}:
1838 List.filter.put(Cookie, c, jar.live(t, now), cookie.live(now, c))
1839
1840# The jar at a later time: cookies expired by now are evicted (§5.7).
1841def jar.at(j: Jar, +now: Time.Instant) -> Jar:
1842 Jar{old, cs} = j
1843 Jar{now, jar.live(cs, now)}
1844
1845def cookie.cut.found(r: String & String) -> String & String & Bool:
1846 (a, b) = r
1847 (a, b, True{})
1848
1849# hit: the last char pushed onto acc was c.
1850def cookie.cut.go(s: String, +c: U32, acc: String, hit: Bool) -> String & String & Bool:
1851 match s:
1852 case SNil{}:
1853 match hit:
1854 case True{}:
1855 cookie.cut.found(take.cut(acc, SNil{}))
1856 case False{}:
1857 (String.reverse(acc), SNil{}, False{})
1858 case SCon{Chr{+x}, t}:
1859 match hit:
1860 case True{}:
1861 cookie.cut.found(take.cut(acc, SCon{Chr{x}, t}))
1862 case False{}:
1863 cookie.cut.go(t, c, SCon{Chr{x}, acc}, U32.is_eq(x, c))
1864
1865# s split at its first c: before, after, and whether c was there.
1866def cookie.cut(s: String, +c: U32) -> String & String & Bool:
1867 cookie.cut.go(s, c, SNil{}, False{})
1868
1869def cookie.fst(r: String & String & Bool) -> String:
1870 (a, b, found) = r
1871 a
1872
1873# The path of an origin-form target: the part before "?".
1874def cookie.target_path(t: String) -> String:
1875 cookie.fst(cookie.cut(t, 63))
1876
1877# Longer than n octets.
1878def cookie.over(s: String, +n: U32) -> Bool:
1879 match s:
1880 case SNil{}:
1881 False{}
1882 case SCon{c, t}:
1883 Bool.or(U32.is_eq(n, 0), cookie.over(t, (n - 1 : U32)))
1884
1885# %x00-08 / %x0A-1F / %x7F: control characters other than HTAB.
1886def cookie.ctl(s: String) -> Bool:
1887 match s:
1888 case SNil{}:
1889 False{}
1890 case SCon{Chr{+c}, t}:
1891 Bool.or(Bool.or(U32.is_lt(c, 9), Bool.and(U32.is_gt(c, 9), U32.is_lt(c, 32))), Bool.or(U32.is_eq(c, 127), cookie.ctl(t)))
1892
1893def cookie.ascii(s: String) -> Bool:
1894 match s:
1895 case SNil{}:
1896 True{}
1897 case SCon{Chr{+c}, t}:
1898 Bool.and(U32.is_lt(c, 128), cookie.ascii(t))
1899
1900def cookie.ip4(s: String) -> Bool:
1901 match s:
1902 case SNil{}:
1903 True{}
1904 case SCon{Chr{+c}, t}:
1905 Bool.and(Bool.or(parse_u32.digit(c), U32.is_eq(c, 46)), cookie.ip4(t))
1906
1907# An IP literal rather than a host name: IPv6 has a colon, IPv4 is digits and dots.
1908def cookie.ip(+h: String) -> Bool:
1909 Bool.or(String.contains(h, ":"), cookie.ip4(h))
1910
1911# §5.1.3: s is d, or a host name under d on a label boundary.
1912def cookie.domain_match(+s: String, +d: String) -> Bool:
1913 Bool.or(String.eq(s, d), Bool.and(String.ends_with(s, "." ++ d), Bool.not(cookie.ip(s))))
1914
1915# A reversed path with its last segment and slash dropped.
1916def cookie.up(rs: String) -> String:
1917 match rs:
1918 case SNil{}:
1919 SNil{}
1920 case SCon{Chr{47}, t}:
1921 t
1922 case SCon{Chr{c}, t}:
1923 cookie.up(t)
1924
1925# §5.1.4: the request path up to its last "/", or "/".
1926def cookie.default_path(+p: String) -> String:
1927 +up = String.reverse(cookie.up(String.reverse(p)))
1928 Bool.pick(String, Bool.or(Bool.not(String.starts_with(p, "/")), String.is_empty(up)), "/", up)
1929
1930# §5.1.4: request path p path-matches cookie path c.
1931def cookie.path_match(+p: String, +c: String) -> Bool:
1932 Bool.or(String.eq(p, c), Bool.and(String.starts_with(p, c), Bool.or(String.ends_with(c, "/"), String.starts_with(String.drop(p, String.length(c)), "/"))))
1933
1934type Hms is Data:
1935 Hms{h: U32, m: U32, s: U32}
1936
1937# §5.1.1 cookie-date: the first time, day, month and year tokens found.
1938type Cdate is Data:
1939 Cdate{time: Maybe<&2, Hms>, day: Maybe<&2, U32>, month: Maybe<&2, U32>, year: Maybe<&2, U32>}
1940
1941def cookie.date.delim(+c: U32) -> Bool:
1942 Bool.or(U32.is_eq(c, 9), Bool.or(Bool.and(U32.is_ge(c, 32), U32.is_le(c, 47)), Bool.or(Bool.and(U32.is_ge(c, 59), U32.is_le(c, 64)), Bool.or(Bool.and(U32.is_ge(c, 91), U32.is_le(c, 96)), Bool.and(U32.is_ge(c, 123), U32.is_le(c, 126))))))
1943
1944def cookie.date.push(acc: String, ts: List<&2, String>) -> List<&2, String>:
1945 match acc:
1946 case SNil{}:
1947 ts
1948 case SCon{h, t}:
1949 Con{String.reverse(SCon{h, t}), ts}
1950
1951def cookie.date.step(d: Bool, +c: U32, acc: String, ts: List<&2, String>) -> String & List<&2, String>:
1952 match d:
1953 case True{}:
1954 (SNil{}, cookie.date.push(acc, ts))
1955 case False{}:
1956 (SCon{Chr{c}, acc}, ts)
1957
1958# The date-tokens, last first. st: the token so far (reversed) and the tokens before it.
1959def cookie.date.tokens(s: String, st: String & List<&2, String>) -> List<&2, String>:
1960 match s:
1961 case SNil{}:
1962 (acc, ts) = st
1963 cookie.date.push(acc, ts)
1964 case SCon{Chr{+c}, t}:
1965 (acc, ts) = st
1966 cookie.date.tokens(t, cookie.date.step(cookie.date.delim(c), c, acc, ts))
1967
1968def cookie.date.head(+s: String) -> Bool:
1969 match s:
1970 case SNil{}:
1971 False{}
1972 case SCon{Chr{+c}, t}:
1973 parse_u32.digit(c)
1974
1975# The digits at the start of s: (count, value, rest). d: s starts with a digit.
1976def cookie.date.run(s: String, d: Bool, +n: U32, +acc: U32) -> U32 & U32 & String:
1977 match s:
1978 case SNil{}:
1979 (n, acc, SNil{})
1980 case SCon{Chr{+c}, +t}:
1981 match d:
1982 case True{}:
1983 cookie.date.run(t, cookie.date.head(t), (n + 1 : U32), (acc * 10 + (c - 48 : U32) : U32))
1984 case False{}:
1985 (n, acc, SCon{Chr{c}, t})
1986
1987def cookie.date.within(r: U32 & U32 & String, +lo: U32, +hi: U32) -> Maybe<&1, U32 & String>:
1988 (+n, v, rest) = r
1989 Bool.pick(Maybe<&1, U32 & String>, Bool.and(U32.is_ge(n, lo), U32.is_le(n, hi)), Some{(v, rest)}, None{})
1990
1991# lo to hi digits and what follows them, which does not start with a digit.
1992def cookie.date.num(+s: String, +lo: U32, +hi: U32) -> Maybe<&1, U32 & String>:
1993 cookie.date.within(cookie.date.run(s, cookie.date.head(s), 0, 0), lo, hi)
1994
1995def cookie.date.val(m: Maybe<&1, U32 & String>) -> Maybe<&2, U32>:
1996 match m:
1997 case None{}:
1998 None{}
1999 case Some{(v, t)}:
2000 Some{v}
2001
2002def cookie.date.colon(s: String) -> Maybe<&2, String>:
2003 match s:
2004 case SNil{}:
2005 None{}
2006 case SCon{Chr{58}, t}:
2007 Some{t}
2008 case SCon{Chr{c}, t}:
2009 None{}
2010
2011def cookie.date.sec(+h: U32, +m: U32, r: Maybe<&1, U32 & String>) -> Maybe<&2, Hms>:
2012 match r:
2013 case None{}:
2014 None{}
2015 case Some{(s, t)}:
2016 Some{Hms{h, m, s}}
2017
2018def cookie.date.min.c(+h: U32, +m: U32, c: Maybe<&2, String>) -> Maybe<&2, Hms>:
2019 match c:
2020 case None{}:
2021 None{}
2022 case Some{+t}:
2023 cookie.date.sec(h, m, cookie.date.num(t, 1, 2))
2024
2025def cookie.date.min(+h: U32, r: Maybe<&1, U32 & String>) -> Maybe<&2, Hms>:
2026 match r:
2027 case None{}:
2028 None{}
2029 case Some{(m, t)}:
2030 cookie.date.min.c(h, m, cookie.date.colon(t))
2031
2032def cookie.date.hour.c(+h: U32, c: Maybe<&2, String>) -> Maybe<&2, Hms>:
2033 match c:
2034 case None{}:
2035 None{}
2036 case Some{+t}:
2037 cookie.date.min(h, cookie.date.num(t, 1, 2))
2038
2039def cookie.date.hour(r: Maybe<&1, U32 & String>) -> Maybe<&2, Hms>:
2040 match r:
2041 case None{}:
2042 None{}
2043 case Some{(h, t)}:
2044 cookie.date.hour.c(h, cookie.date.colon(t))
2045
2046# hms-time: 1*2DIGIT ":" 1*2DIGIT ":" 1*2DIGIT, then anything but a digit.
2047def cookie.date.time(+tok: String) -> Maybe<&2, Hms>:
2048 cookie.date.hour(cookie.date.num(tok, 1, 2))
2049
2050def cookie.date.month.go(xs: List<&2, String>, +w: String, +i: U32) -> Maybe<&2, U32>:
2051 match xs:
2052 case Nil{}:
2053 None{}
2054 case Con{x, t}:
2055 Bool.pick(Maybe<&2, U32>, String.eq(x, w), Some{i}, cookie.date.month.go(t, w, (i + 1 : U32)))
2056
2057# The month named by the first three letters, from 1.
2058def cookie.date.month(+tok: String) -> Maybe<&2, U32>:
2059 cookie.date.month.go(["jan", "feb", "mar", "apr", "may", "jun", "jul", "aug", "sep", "oct", "nov", "dec"], String.to_lower(String.take(tok, 3n)), 1)
2060
2061# Each try* below: the flag is set, so go on; or the token matches, so stop; or go on.
2062def cookie.date.year(y: Maybe<&2, U32>, +tok: String, t: Maybe<&2, Hms>, d: Maybe<&2, U32>, m: Maybe<&2, U32>) -> Cdate:
2063 match y:
2064 case None{}:
2065 Cdate{t, d, m, cookie.date.val(cookie.date.num(tok, 2, 4))}
2066 case Some{v}:
2067 Cdate{t, d, m, Some{v}}
2068
2069def cookie.date.month.got(g: Maybe<&2, U32>, +tok: String, t: Maybe<&2, Hms>, d: Maybe<&2, U32>, y: Maybe<&2, U32>) -> Cdate:
2070 match g:
2071 case None{}:
2072 cookie.date.year(y, tok, t, d, None{})
2073 case Some{v}:
2074 Cdate{t, d, Some{v}, y}
2075
2076def cookie.date.month.try(m: Maybe<&2, U32>, +tok: String, t: Maybe<&2, Hms>, d: Maybe<&2, U32>, y: Maybe<&2, U32>) -> Cdate:
2077 match m:
2078 case None{}:
2079 cookie.date.month.got(cookie.date.month(tok), tok, t, d, y)
2080 case Some{v}:
2081 cookie.date.year(y, tok, t, d, Some{v})
2082
2083def cookie.date.day.got(g: Maybe<&2, U32>, +tok: String, t: Maybe<&2, Hms>, m: Maybe<&2, U32>, y: Maybe<&2, U32>) -> Cdate:
2084 match g:
2085 case None{}:
2086 cookie.date.month.try(m, tok, t, None{}, y)
2087 case Some{v}:
2088 Cdate{t, Some{v}, m, y}
2089
2090def cookie.date.day.try(d: Maybe<&2, U32>, +tok: String, t: Maybe<&2, Hms>, m: Maybe<&2, U32>, y: Maybe<&2, U32>) -> Cdate:
2091 match d:
2092 case None{}:
2093 cookie.date.day.got(cookie.date.val(cookie.date.num(tok, 1, 2)), tok, t, m, y)
2094 case Some{v}:
2095 cookie.date.month.try(m, tok, t, Some{v}, y)
2096
2097def cookie.date.time.got(g: Maybe<&2, Hms>, +tok: String, d: Maybe<&2, U32>, m: Maybe<&2, U32>, y: Maybe<&2, U32>) -> Cdate:
2098 match g:
2099 case None{}:
2100 cookie.date.day.try(d, tok, None{}, m, y)
2101 case Some{v}:
2102 Cdate{Some{v}, d, m, y}
2103
2104def cookie.date.time.try(t: Maybe<&2, Hms>, +tok: String, d: Maybe<&2, U32>, m: Maybe<&2, U32>, y: Maybe<&2, U32>) -> Cdate:
2105 match t:
2106 case None{}:
2107 cookie.date.time.got(cookie.date.time(tok), tok, d, m, y)
2108 case Some{v}:
2109 cookie.date.day.try(d, tok, Some{v}, m, y)
2110
2111def cookie.date.fold(ts: List<&2, String>, st: Cdate) -> Cdate:
2112 match ts:
2113 case Nil{}:
2114 st
2115 case Con{+tok, rest}:
2116 Cdate{t, d, m, y} = st
2117 cookie.date.fold(rest, cookie.date.time.try(t, tok, d, m, y))
2118
2119# 70–99 are 19xx, 0–69 are 20xx.
2120def cookie.date.fix(+y: U32) -> U32:
2121 Bool.pick(U32, U32.is_le(y, 69), (y + 2000 : U32), Bool.pick(U32, U32.is_le(y, 99), (y + 1900 : U32), y))
2122
2123def cookie.date.at(+y: U32, +d: U32, mo: U32, h: U32, mi: U32, s: U32) -> Maybe<&2, Time.Instant>:
2124 Bool.pick(Maybe<&2, Time.Instant>, Bool.and(U32.is_ge(y, 1601), Bool.and(U32.is_ge(d, 1), U32.is_le(d, 31))), Time.mk(Time.DateTime{Time.Date{y, mo, d}, h, mi, s, 0}), None{})
2125
2126def cookie.date.fin(st: Cdate) -> Maybe<&2, Time.Instant>:
2127 match st:
2128 case Cdate{Some{Hms{h, mi, s}}, Some{d}, Some{mo}, Some{y}}:
2129 cookie.date.at(cookie.date.fix(y), d, mo, h, mi, s)
2130 case _:
2131 None{}
2132
2133# §5.1.1: a cookie-date such as "Sun, 06 Nov 1994 08:49:37 GMT" or "Thu, 01-Jan-70 00:00:01 GMT".
2134# Time.mk refuses a day past the month's end and a time past 23:59:59.
2135def cookie.date(s: String) -> Maybe<&2, Time.Instant>:
2136 cookie.date.fin(cookie.date.fold(List.reverse(&2, String, cookie.date.tokens(s, (SNil{}, Nil{}))), Cdate{None{}, None{}, None{}, None{}}))
2137
2138# §5.6.1–§5.6.7: the last of each attribute. expires is the date as sent; max_age is capped seconds.
2139# Neither is a time from now yet: a Cav with a Time.Instant and now beside it is too wide (bendlang/bend#1069).
2140type Cav is Data:
2141 Cav{expires: Maybe<&2, Time.Instant>, max_age: Maybe<&2, U32>, domain: String, path: Maybe<&2, String>, secure: Bool, http_only: Bool, same_site: String}
2142
2143def cookie.cav() -> Cav:
2144 Cav{None{}, None{}, "", None{}, False{}, False{}, "default"}
2145
2146# §5.5: 400 days, the longest a cookie lives.
2147def cookie.limit() -> U32:
2148 34560000
2149
2150def cookie.later(+now: Time.Instant, +secs: U32) -> Time.Instant:
2151 Time.Instant.add(now, Time.Duration.of_secs(Int.I64.from_u32(secs)))
2152
2153def cookie.expires.cap(+now: Time.Instant, m: Maybe<&2, Time.Instant>) -> Maybe<&2, Time.Instant>:
2154 match m:
2155 case None{}:
2156 None{}
2157 case Some{+t}:
2158 +lim = cookie.later(now, cookie.limit())
2159 Some{Bool.pick(Time.Instant, Cmp.is_lt(Time.Instant.cmp(lim, t)), lim, t)}
2160
2161def cookie.max_age.zero(m: Maybe<&2, U32>) -> Maybe<&2, U32>:
2162 match m:
2163 case None{}:
2164 None{}
2165 case Some{s}:
2166 Some{0}
2167
2168def cookie.max_age.nz(s: String) -> String:
2169 match s:
2170 case SNil{}:
2171 SNil{}
2172 case SCon{Chr{48}, t}:
2173 cookie.max_age.nz(t)
2174 case SCon{Chr{c}, t}:
2175 SCon{Chr{c}, t}
2176
2177# More than 9 significant digits is past the limit (and would overflow parse_u32).
2178def cookie.max_age.cap(long: Bool, m: Maybe<&2, U32>) -> Maybe<&2, U32>:
2179 match m:
2180 case None{}:
2181 None{}
2182 case Some{s}:
2183 Some{Bool.pick(U32, long, cookie.limit(), s)}
2184
2185def cookie.max_age.secs(+v: String, neg: Bool) -> Maybe<&2, U32>:
2186 match neg:
2187 case True{}:
2188 cookie.max_age.zero(parse_u32(String.drop(v, 1n)))
2189 case False{}:
2190 cookie.max_age.cap(cookie.over(cookie.max_age.nz(v), 9), parse_u32(v))
2191
2192# Zero or less is the earliest time, so the cookie is already expired.
2193def cookie.max_age.at(+now: Time.Instant, m: Maybe<&2, U32>) -> Maybe<&2, Time.Instant>:
2194 match m:
2195 case None{}:
2196 None{}
2197 case Some{+s}:
2198 Some{Bool.pick(Time.Instant, U32.is_eq(s, 0), Time.Instant.epoch(), cookie.later(now, U32.min(s, cookie.limit())))}
2199
2200# §5.6.2: DIGIT*, or "-" and DIGIT*. Anything else is ignored.
2201def cookie.max_age(+v: String) -> Maybe<&2, U32>:
2202 cookie.max_age.secs(v, String.starts_with(v, "-"))
2203
2204def cookie.same_site(+v: String) -> String:
2205 +l = String.to_lower(v)
2206 Bool.pick(String, Bool.or(String.eq(l, "strict"), Bool.or(String.eq(l, "lax"), String.eq(l, "none"))), l, "default")
2207
2208type Av is Data:
2209 AvExpires{}
2210 AvMaxAge{}
2211 AvDomain{}
2212 AvPath{}
2213 AvSecure{}
2214 AvHttpOnly{}
2215 AvSameSite{}
2216 AvOther{}
2217
2218def cookie.av.kind(+k: String) -> Av:
2219 Bool.pick(Av, String.eq(k, "expires"), AvExpires{}, Bool.pick(Av, String.eq(k, "max-age"), AvMaxAge{}, Bool.pick(Av, String.eq(k, "domain"), AvDomain{}, Bool.pick(Av, String.eq(k, "path"), AvPath{}, Bool.pick(Av, String.eq(k, "secure"), AvSecure{}, Bool.pick(Av, String.eq(k, "httponly"), AvHttpOnly{}, Bool.pick(Av, String.eq(k, "samesite"), AvSameSite{}, AvOther{})))))))
2220
2221# An Expires or Max-Age that does not parse leaves the earlier one. A leading dot of Domain is dropped.
2222def cookie.av.put(k: Av, a: Cav, +v: String) -> Cav:
2223 match k a:
2224 case AvExpires{} Cav{e, m, d, p, s, h, ss}:
2225 Cav{Maybe.or(&2, Time.Instant, cookie.date(v), e), m, d, p, s, h, ss}
2226 case AvMaxAge{} Cav{e, m, d, p, s, h, ss}:
2227 Cav{e, Maybe.or(&2, U32, cookie.max_age(v), m), d, p, s, h, ss}
2228 case AvDomain{} Cav{e, m, d, p, s, h, ss}:
2229 Cav{e, m, String.to_lower(Bool.pick(String, String.starts_with(v, "."), String.drop(v, 1n), v)), p, s, h, ss}
2230 case AvPath{} Cav{e, m, d, p, s, h, ss}:
2231 Cav{e, m, d, Some{v}, s, h, ss}
2232 case AvSecure{} Cav{e, m, d, p, s, h, ss}:
2233 Cav{e, m, d, p, True{}, h, ss}
2234 case AvHttpOnly{} Cav{e, m, d, p, s, h, ss}:
2235 Cav{e, m, d, p, s, True{}, ss}
2236 case AvSameSite{} Cav{e, m, d, p, s, h, ss}:
2237 Cav{e, m, d, p, s, h, cookie.same_site(v)}
2238 case AvOther{} Cav{e, m, d, p, s, h, ss}:
2239 Cav{e, m, d, p, s, h, ss}
2240
2241# §5.6: name and value trimmed; a value over 1024 octets drops the attribute.
2242def cookie.av(+a: Cav, kv: String & String & Bool) -> Cav:
2243 (k, v, found) = kv
2244 +tv = trim(v)
2245 Bool.pick(Cav, cookie.over(tv, 1024), a, cookie.av.put(cookie.av.kind(String.to_lower(trim(k))), a, tv))
2246
2247def cookie.avs(xs: List<&2, String>, a: Cav) -> Cav:
2248 match xs:
2249 case Nil{}:
2250 a
2251 case Con{x, t}:
2252 cookie.avs(t, cookie.av(a, cookie.cut(x, 61)))
2253
2254# §5.6: with no "=", the name is empty and the pair is the value.
2255def cookie.nv(r: String & String & Bool) -> String & String:
2256 (a, b, found) = r
2257 match found:
2258 case True{}:
2259 (trim(a), trim(b))
2260 case False{}:
2261 ("", trim(a))
2262
2263def cookie.prefixed(+s: String, +p: String) -> Bool:
2264 String.starts_with(String.to_lower(s), p)
2265
2266# §5.7 steps 8–10: (domain, host-only), or None to ignore the cookie.
2267# ponytail: the public-suffix check knows single-label suffixes only (com, org, localhost). Multi-label
2268# ones (co.uk, github.io) need the publicsuffix.org list; ship it as data when a caller needs it.
2269def cookie.domain.of(+host: String, +d: String) -> Maybe<&1, String & Bool>:
2270 +suffix = Bool.and(Bool.not(String.is_empty(d)), Bool.not(String.contains(d, ".")))
2271 +d2 = Bool.pick(String, Bool.and(suffix, String.eq(d, host)), "", d)
2272 Bool.pick(Maybe<&1, String & Bool>, Bool.or(Bool.and(suffix, Bool.not(String.eq(d, host))), Bool.not(cookie.ascii(d))), None{},
2273 Bool.pick(Maybe<&1, String & Bool>, String.is_empty(d2), Some{(host, True{})},
2274 Bool.pick(Maybe<&1, String & Bool>, cookie.domain_match(host, d2), Some{(d2, False{})}, None{})))
2275
2276def cookie.path.of(p: Maybe<&2, String>, +req: String) -> String:
2277 match p:
2278 case None{}:
2279 cookie.default_path(req)
2280 case Some{+v}:
2281 Bool.pick(String, String.starts_with(v, "/"), v, cookie.default_path(req))
2282
2283# §5.7 steps 12–20: Secure needs https; SameSite=None needs Secure; the __Secure- and __Host- prefixes.
2284def cookie.make.dm(dm: Maybe<&1, String & Bool>, +name: String, +value: String, +path: String, has_path: Bool, +secure: Bool, http_only: Bool, +same_site: String, expiry: Maybe<&2, Time.Instant>, https: Bool) -> Maybe<&2, Cookie>:
2285 match dm:
2286 case None{}:
2287 None{}
2288 case Some{(domain, +host_only)}:
2289 +host = Bool.and(Bool.and(secure, host_only), Bool.and(has_path, String.eq(path, "/")))
2290 +bad = Bool.or(Bool.or(Bool.and(secure, Bool.not(https)), Bool.and(String.eq(same_site, "none"), Bool.not(secure))),
2291 Bool.or(Bool.or(Bool.and(cookie.prefixed(name, "__secure-"), Bool.not(secure)), Bool.and(cookie.prefixed(name, "__host-"), Bool.not(host))),
2292 Bool.and(String.is_empty(name), Bool.or(cookie.prefixed(value, "__secure-"), cookie.prefixed(value, "__host-")))))
2293 Bool.pick(Maybe<&2, Cookie>, bad, None{}, Some{Cookie{name, value, domain, host_only, path, secure, http_only, same_site, expiry}})
2294
2295# Max-Age wins over Expires, whatever their order (§5.7 step 6). Both count from now.
2296def cookie.expiry(+now: Time.Instant, m: Maybe<&2, U32>, e: Maybe<&2, Time.Instant>) -> Maybe<&2, Time.Instant>:
2297 Maybe.or(&2, Time.Instant, cookie.max_age.at(now, m), cookie.expires.cap(now, e))
2298
2299def cookie.make(+now: Time.Instant, a: Url.Abs, +name: String, +value: String, c: Cav) -> Maybe<&2, Cookie>:
2300 Url.Abs{scheme, host, port, target} = a
2301 Cav{e, m, d, +p, secure, http_only, same_site} = c
2302 cookie.make.dm(cookie.domain.of(host, d), name, value, cookie.path.of(p, cookie.target_path(target)), Maybe.is_some(&2, String, p), secure, http_only, same_site, cookie.expiry(now, m, e), String.eq(scheme, "https"))
2303
2304# An empty name and value, or more than 4096 octets of them, is ignored.
2305def cookie.parse.nv(+now: Time.Instant, a: Url.Abs, nv: String & String, avs: List<&2, String>) -> Maybe<&2, Cookie>:
2306 (+name, +value) = nv
2307 Bool.pick(Maybe<&2, Cookie>, Bool.or(Bool.and(String.is_empty(name), String.is_empty(value)), cookie.over(name ++ value, 4096)), None{}, cookie.make(now, a, name, value, cookie.avs(avs, cookie.cav())))
2308
2309def cookie.parse.go(+now: Time.Instant, a: Url.Abs, xs: List<&2, String>) -> Maybe<&2, Cookie>:
2310 match xs:
2311 case Nil{}:
2312 None{}
2313 case Con{first, avs}:
2314 cookie.parse.nv(now, a, cookie.nv(cookie.cut(first, 61)), avs)
2315
2316# §5.6 and §5.7: one Set-Cookie value received from a at now, or None when it is ignored.
2317def cookie.parse(+now: Time.Instant, a: Url.Abs, +line: String) -> Maybe<&2, Cookie>:
2318 Bool.pick(Maybe<&2, Cookie>, cookie.ctl(line), None{}, cookie.parse.go(now, a, String.split(line, ';')))
2319
2320def cookie.https(a: Url.Abs) -> Bool:
2321 Url.Abs{scheme, host, port, target} = a
2322 String.eq(scheme, "https")
2323
2324def cookie.secure(c: Cookie) -> Bool:
2325 Cookie{name, value, domain, host_only, path, secure, http_only, same_site, expiry} = c
2326 secure
2327
2328# Same name, domain, host-only flag and path: the new cookie replaces the old one.
2329def cookie.same(+a: Cookie, +b: Cookie) -> Bool:
2330 Cookie{n1, v1, d1, h1, p1, s1, o1, ss1, e1} = a
2331 Cookie{n2, v2, d2, h2, p2, s2, o2, ss2, e2} = b
2332 Bool.and(Bool.and(String.eq(n1, n2), String.eq(d1, d2)), Bool.and(Bool.not(Bool.xor(h1, h2)), String.eq(p1, p2)))
2333
2334# §5.7 step 16: a secure cookie that a new cookie from plain http must not overlay.
2335def cookie.shadows(+old: Cookie, +c: Cookie) -> Bool:
2336 Cookie{n1, v1, +d1, h1, p1, s1, o1, ss1, e1} = old
2337 Cookie{n2, v2, +d2, h2, p2, s2, o2, ss2, e2} = c
2338 Bool.and(Bool.and(String.eq(n1, n2), s1), Bool.and(Bool.or(cookie.domain_match(d1, d2), cookie.domain_match(d2, d1)), cookie.path_match(p2, p1)))
2339
2340def cookie.shadowed(cs: List<&2, Cookie>, +c: Cookie) -> Bool:
2341 match cs:
2342 case Nil{}:
2343 False{}
2344 case Con{+o, t}:
2345 Bool.or(cookie.shadows(o, c), cookie.shadowed(t, c))
2346
2347# cs with the cookie c replaces swapped for c (keeping its place, so its creation order), or c last.
2348# A c that is not live only removes the old one: that is how a server deletes a cookie.
2349def cookie.put(cs: List<&2, Cookie>, +c: Cookie, +live: Bool) -> List<&2, Cookie>:
2350 match cs:
2351 case Nil{}:
2352 Bool.pick(List<&2, Cookie>, live, [c], Nil{})
2353 case Con{+o, +t}:
2354 Bool.pick(List<&2, Cookie>, cookie.same(o, c), Bool.pick(List<&2, Cookie>, live, Con{c, t}, t), Con{o, cookie.put(t, c, live)})
2355
2356def jar.put.c(m: Maybe<&2, Cookie>, j: Jar, +https: Bool) -> Jar:
2357 match m:
2358 case None{}:
2359 Jar{now, cs} = j
2360 Jar{now, cs}
2361 case Some{+c}:
2362 Jar{+now, +cs} = j
2363 Jar{now, Bool.pick(List<&2, Cookie>, Bool.and(Bool.not(Bool.or(https, cookie.secure(c))), cookie.shadowed(cs, c)), cs, cookie.put(cs, c, cookie.live(now, c)))}
2364
2365def jar.put.one(j: Jar, +a: Url.Abs, x: String) -> Jar:
2366 Jar{+now, cs} = j
2367 jar.put.c(cookie.parse(now, a, x), Jar{now, cs}, cookie.https(a))
2368
2369def jar.put.all(xs: List<&2, String>, j: Jar, +a: Url.Abs) -> Jar:
2370 match xs:
2371 case Nil{}:
2372 j
2373 case Con{x, t}:
2374 jar.put.all(t, jar.put.one(j, a, x), a)
2375
2376# Every set-cookie field of h, in order, as received from a.
2377def jar.store.abs(j: Jar, +a: Url.Abs, +h: Map<&2, List<&2, String>>) -> Jar:
2378 jar.put.all(fields(h, "set-cookie"), j, a)
2379
2380def jar.store.url(j: Jar, u: Maybe<&2, Url.Abs>, +h: Map<&2, List<&2, String>>) -> Jar:
2381 match u:
2382 case None{}:
2383 j
2384 case Some{+a}:
2385 jar.store.abs(j, a, h)
2386
2387# The jar after res came from url, and res as it was. Header names are lowercase, as parse gives them.
2388# An unparsable url stores nothing.
2389def jar.store(j: Jar, url: String, res: Res) -> Jar & Res:
2390 Res{status, +headers, body} = res
2391 (jar.store.url(j, Url.absolute(url), headers), Res{status, headers, body})
2392
2393# §5.8.3: domain (exact when host-only), path, and Secure only over https.
2394def cookie.sends(+host: String, +path: String, +https: Bool, +c: Cookie) -> Bool:
2395 Cookie{n, v, +d, +ho, +p, s, o, ss, e} = c
2396 Bool.and(Bool.pick(Bool, ho, String.eq(host, d), cookie.domain_match(host, d)), Bool.and(cookie.path_match(path, p), Bool.or(Bool.not(s), https)))
2397
2398def cookie.pick(cs: List<&2, Cookie>, +host: String, +path: String, +https: Bool) -> List<&2, Cookie>:
2399 match cs:
2400 case Nil{}:
2401 Nil{}
2402 case Con{+c, t}:
2403 List.filter.put(Cookie, c, cookie.pick(t, host, path, https), cookie.sends(host, path, https, c))
2404
2405# The sort order of §5.8.3: longer paths first; the stable sort keeps creation order among equals.
2406def cookie.longer(a: Cookie, b: Cookie) -> Bool:
2407 Cookie{n1, v1, d1, h1, p1, s1, o1, ss1, e1} = a
2408 Cookie{n2, v2, d2, h2, p2, s2, o2, ss2, e2} = b
2409 Bool.not(Nat.is_lt(String.length(p1), String.length(p2)))
2410
2411def cookie.pair(c: Cookie) -> String:
2412 Cookie{+n, +v, d, h, p, s, o, ss, e} = c
2413 Bool.pick(String, String.is_empty(n), v, n ++ "=" ++ v)
2414
2415def cookie.pairs(cs: List<&2, Cookie>) -> List<&2, String>:
2416 match cs:
2417 case Nil{}:
2418 Nil{}
2419 case Con{c, t}:
2420 Con{cookie.pair(c), cookie.pairs(t)}
2421
2422# §5.8.3: the cookie-string for a request to a, or "" when no cookie matches.
2423def jar.string(j: Jar, a: Url.Abs) -> String:
2424 Jar{now, cs} = j
2425 Url.Abs{scheme, +host, port, target} = a
2426 String.join(cookie.pairs(List.sort(~Cookie, ~cookie.longer, cookie.pick(cs, host, cookie.target_path(target), String.eq(scheme, "https")))), "; ")
2427
2428# One cookie field: the caller's own cookie values first, then the jar's.
2429def jar.header(+h: Map<&2, List<&2, String>>, +s: String) -> Map<&2, List<&2, String>>:
2430 +old = String.join(fields(h, "cookie"), "; ")
2431 Bool.pick(Map<&2, List<&2, String>>, String.is_empty(s), h, set(h, "cookie", Bool.pick(String, String.is_empty(old), s, old ++ "; " ++ s)))
2432
2433def jar.apply.url(j: Jar, u: Maybe<&2, Url.Abs>, +h: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
2434 match u:
2435 case None{}:
2436 h
2437 case Some{a}:
2438 jar.header(h, jar.string(j, a))
2439
2440# The headers with the jar's cookies for a request to url in their cookie field (lowercase, as fetch
2441# sends names). An unparsable url adds nothing.
2442def jar.apply(j: Jar, url: String, +h: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
2443 jar.apply.url(j, Url.absolute(url), h)
2444
2445# The jar, if any, that a fetch threads through its hops.
2446def jar.opt.apply(m: Maybe<&2, Jar>, a: Url.Abs, +h: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
2447 match m:
2448 case None{}:
2449 h
2450 case Some{j}:
2451 jar.header(h, jar.string(j, a))
2452
2453def jar.opt.res(j: Jar, +a: Url.Abs, r: Result<&1, &1, Err, Res>) -> Maybe<&2, Jar> & Result<&1, &1, Err, Res>:
2454 match r:
2455 case Fail{e}:
2456 (Some{j}, Fail{e})
2457 case Done{res}:
2458 Res{status, +headers, body} = res
2459 (Some{jar.store.abs(j, a, headers)}, Done{Res{status, headers, body}})
2460
2461def jar.opt.store(m: Maybe<&2, Jar>, +a: Url.Abs, r: Result<&1, &1, Err, Res>) -> Maybe<&2, Jar> & Result<&1, &1, Err, Res>:
2462 match m:
2463 case None{}:
2464 (None{}, r)
2465 case Some{j}:
2466 jar.opt.res(j, a, r)
2467
2468def io.recv.words(tls: Bool, s: Socket, max: U32, ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>):
2469 match tls:
2470 case True{}:
2471 Wire.tls.recv.words(s, max, ms)
2472 case False{}:
2473 Wire.recv.words(s, max, ms)
2474
2475def io.send.words(tls: Bool, s: Socket, +len: U32, buf: Array<U32>) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
2476 match tls:
2477 case True{}:
2478 Wire.tls.send.words(s, len, buf)
2479 case False{}:
2480 Wire.send.words(s, len, buf)
2481
2482def io.send.bytes(tls: Bool, s: Socket, b: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
2483 Bytes.Bytes{+len, buf} = b
2484 io.send.words(tls, s, len, buf)
2485
2486def io.close(tls: Bool, s: Socket) -> IO(Unit):
2487 match tls:
2488 case True{}:
2489 Wire.tls.close(s)
2490 case False{}:
2491 Socket.close(s)
2492
2493def fetch.close(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
2494 do IO<Result<&1, &1, Err, Res>>:
2495 io.close(tls, s)
2496 return r
2497
2498# none: no response byte arrived, so an idempotent request may be retried (RFC 9112 §9.3.1).
2499# sock: the socket, when it can take another request.
2500type Out is Type:
2501 OutDone{res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes}
2502 OutFail{e: Err, none: Bool}
2503
2504def fetch.boxed(r: Result<&1, &1, Err, Res>, none: Bool) -> Out:
2505 match r:
2506 case Done{res}:
2507 OutDone{res, None{}, Bytes.new(0)}
2508 case Fail{e}:
2509 OutFail{e, none}
2510
2511def fetch.bad(tls: Bool, s: Socket, e: Maybe<&2, Err>) -> IO(Result<&1, &1, Err, Res>):
2512 match e:
2513 case None{}:
2514 fetch.close(tls, s, Fail{ErrBad{}})
2515 case Some{err}:
2516 fetch.close(tls, s, Fail{err})
2517
2518def fetch.shut(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>, none: Bool) -> IO(Out):
2519 do IO<Out>:
2520 x : Result<&1, &1, Err, Res> <- fetch.close(tls, s, r)
2521 return fetch.boxed(x, none)
2522
2523def fetch.hold.go(tls: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
2524 match left:
2525 case Some{x}:
2526 IO.pure(Out, OutDone{res, Some{s}, x})
2527 case None{}:
2528 fetch.shut(tls, s, Done{res}, False{})
2529
2530def fetch.hold(tls: Bool, close: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
2531 Res{status, +headers, body} = res
2532 fetch.hold.go(tls, s, Res{status, headers, body}, again(close, headers, left))
2533
2534def fetch.failout(tls: Bool, s: Socket, e: Maybe<&2, Err>, none: Bool) -> IO(Out):
2535 do IO<Out>:
2536 r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, e)
2537 return fetch.boxed(r, none)
2538
2539# Read state: the response so far and the bytes read, or how it ended.
2540# none: no byte arrived, so an idempotent request may be retried.
2541type Fl is Type:
2542 FlMore{rv: Rv, n: U32}
2543 FlBad{err: Maybe<&2, Err>, none: Bool}
2544 FlDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
2545
2546def fetch.rt(+n: U32, t: Rt) -> Fl:
2547 match t:
2548 case RtMore{rv}:
2549 FlMore{rv, n}
2550 case RtBad{}:
2551 FlBad{None{}, U32.is_zero(n)}
2552 case RtDone{res, rest}:
2553 FlDone{res, rest}
2554
2555# 64 KiB of head past the body cap, as serve allows.
2556def fetch.over(+n: U32) -> Bool:
2557 Nat.is_lt(Nat.add(fetch.max(), 65536n), U32.to_nat(n))
2558
2559def fetch.piece.cap(over: Bool, +head: Bool, rv: Rv, +n2: U32, +len: U32, buf: Array<U32>) -> Fl:
2560 match over:
2561 case True{}:
2562 FlBad{None{}, False{}}
2563 case False{}:
2564 fetch.rt(n2, rv.step(U32.is_zero(len), head, rv, Bytes.Bytes{len, buf}))
2565
2566def fetch.piece(+head: Bool, rv: Rv, +n: U32, p: U32 & Array<U32>) -> Fl:
2567 (+len, buf) = p
2568 +n2 = (n + len : U32)
2569 fetch.piece.cap(fetch.over(n2), head, rv, n2, len, buf)
2570
2571def fetch.next(+head: Bool, rv: Rv, +n: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Fl:
2572 (s, r) = m
2573 match r:
2574 case Fail{(+code, why)}:
2575 (s, FlBad{Some{err.or_late(code, ErrRead{code, why})}, U32.is_zero(n)})
2576 case Done{p}:
2577 (s, fetch.piece(head, rv, n, p))
2578
2579# Reads until the response is whole or cannot be; an empty read means the server closed.
2580@unsafe
2581def fetch.loop(+close: Bool, +head: Bool, +tls: Bool, +ms: U32, st: Socket & Fl) -> IO(Out):
2582 (s, fl) = st
2583 match fl:
2584 case FlMore{rv, +n}:
2585 do IO<Out>:
2586 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
2587 fetch.loop(close, head, tls, ms, fetch.next(head, rv, n, m))
2588 case FlBad{err, none}:
2589 fetch.failout(tls, s, err, none)
2590 case FlDone{res, rest}:
2591 fetch.hold(tls, close, s, res, rest)
2592
2593def exchange.sent(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Out):
2594 (s, r) = m
2595 match r:
2596 case Fail{(+code, why)}:
2597 fetch.shut(tls, s, Fail{err.or_late(code, ErrWrite{code, why})}, True{})
2598 case Done{u}:
2599 fetch.loop(close, head, tls, ms, (s, FlMore{rv.start(), 0}))
2600
2601def exchange.go(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, s: Socket, wire: Bytes.Bytes) -> IO(Out):
2602 do IO<Out>:
2603 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
2604 exchange.sent(tls, ms, close, head, sent)
2605
2606def exchange.tup(o: Out) -> Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes:
2607 match o:
2608 case OutFail{e, none}:
2609 (None{}, Fail{e}, Bytes.new(0))
2610 case OutDone{res, sock, rest}:
2611 (sock, Done{res}, rest)
2612
2613# One request on an open socket. Some{socket}: it can take another request.
2614def 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):
2615 do IO<Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes>:
2616 o : Out <- exchange.go(tls, ms, close, head, s, wire)
2617 return exchange.tup(o)
2618
2619# Paths to a PEM client chain and its private key for mutual TLS.
2620type Cert is Data:
2621 Cert{chain: String, key: String}
2622
2623type Proxy is Data:
2624 ProxyDirect{}
2625 ProxyVia{host: String, port: U32, authorization: String}
2626
2627type Route is Data:
2628 RouteDirect{tls: Bool, host: String, port: U32, cert: Maybe<&2, Cert>}
2629 RouteProxy{tls: Bool, host: String, port: U32, sni: String,
2630 authority: String, authorization: String, cert: Maybe<&2, Cert>}
2631
2632# Connection pool: idle sockets by origin and client identity, newest first, at most cap per key.
2633# fetch uses a fresh pool per call.
2634
2635type Conn is Type:
2636 Conn{tls: Bool, s: Socket}
2637 ConnH2{s: Socket, client: H2.Client}
2638
2639type Send is Type:
2640 Send{method: String, target: String, authority: String,
2641 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
2642
2643type H2Step is Type:
2644 H2Reply{s: Socket, reply: H2.Reply}
2645 H2Sent{client: H2.Client, events: List<&1, H2.ClientEvent>,
2646 sent: Result<&1, &1, Err, Socket>}
2647 H2Events{s: Socket, client: H2.Client, result: Result<&1, &1, Err, Maybe<&1, Res>>}
2648 H2Received{client: H2.Client,
2649 answer: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>}
2650
2651type TunnelStep is Type:
2652 TunnelRead{s: Socket, raw: String}
2653 TunnelHead{s: Socket, raw: String, frame: Frame}
2654 TunnelGot{raw: String,
2655 answer: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>}
2656
2657type Pool is Type:
2658 Pool{cap: U32, idle: Map<&1, List<&1, Conn>>}
2659
2660def pool.new.with(+cap: U32) -> Pool:
2661 Pool{cap, Map.new(&1, List<&1, Conn>)}
2662
2663# Up to 8 idle sockets per origin.
2664def pool.new() -> Pool:
2665 pool.new.with(8)
2666
2667def pool.key(+scheme: String, +host: String, +port: U32) -> String:
2668 scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
2669
2670def pool.key.cert(+base: String, cert: Maybe<&2, Cert>) -> String:
2671 match cert:
2672 case None{}:
2673 base
2674 case Some{Cert{+chain, +key}}:
2675 base ++ "|cert:" ++ Nat.show(String.length(chain)) ++ ":" ++ chain
2676 ++ Nat.show(String.length(key)) ++ ":" ++ key
2677
2678def pool.take.of(+cap: U32, +key: String, r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> Pool & Maybe<&1, Conn>:
2679 (m, got) = r
2680 match got:
2681 case None{}:
2682 (Pool{cap, m}, None{})
2683 case Some{xs}:
2684 match xs:
2685 case Nil{}:
2686 (Pool{cap, m}, None{})
2687 case Con{c, t}:
2688 (Pool{cap, Map.set(&1, List<&1, Conn>, m, key, t)}, Some{c})
2689
2690# The socket given back last.
2691def pool.take(p: Pool, +key: String) -> Pool & Maybe<&1, Conn>:
2692 Pool{+cap, idle} = p
2693 pool.take.of(cap, key, Map.pop(&1, List<&1, Conn>, idle, key))
2694
2695def conn.close(c: Conn) -> IO(Unit):
2696 match c:
2697 case Conn{tls, s}:
2698 io.close(tls, s)
2699 case ConnH2{s, client}:
2700 Wire.tls.close(s)
2701
2702# The first n sockets; the rest are closed.
2703def conns.cut(xs: List<&1, Conn>, n: Nat) -> IO(List<&1, Conn>):
2704 match xs:
2705 case Nil{}:
2706 IO.pure(List<&1, Conn>, Nil{})
2707 case Con{c, t}:
2708 match n:
2709 case 0n:
2710 do IO<List<&1, Conn>>:
2711 conn.close(c)
2712 conns.cut(t, 0n)
2713 case 1n+k:
2714 do IO<List<&1, Conn>>:
2715 r : List<&1, Conn> <- conns.cut(t, k)
2716 return c <> r
2717
2718def pool.give.of(+cap: U32, +key: String, c: Conn, limit: Nat,
2719 r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> IO(Pool):
2720 (m, old) = r
2721 do IO<Pool>:
2722 xs : List<&1, Conn> <- conns.cut(c <> Maybe.default(&1, List<&1, Conn>, old, Nil{}), limit)
2723 return Pool{cap, Map.set(&1, List<&1, Conn>, m, key, xs)}
2724
2725# Past the limit (cap for HTTP/1.1, one session for HTTP/2), close the oldest idle connection.
2726def pool.give(p: Pool, +key: String, c: Conn) -> IO(Pool):
2727 Pool{+cap, idle} = p
2728 match c:
2729 case Conn{tls, s}:
2730 pool.give.of(cap, key, Conn{tls, s}, U32.to_nat(cap), Map.pop(&1, List<&1, Conn>, idle, key))
2731 case ConnH2{s, client}:
2732 pool.give.of(cap, key, ConnH2{s, client}, Bool.pick(Nat, U32.is_zero(cap), 0n, 1n),
2733 Map.pop(&1, List<&1, Conn>, idle, key))
2734
2735def pool.close.go(xs: List<&1, List<&1, Conn>>) -> IO(Unit):
2736 match xs:
2737 case Nil{}:
2738 IO.pure(Unit, Unit{})
2739 case Con{cs, t}:
2740 do IO<Unit>:
2741 none : List<&1, Conn> <- conns.cut(cs, 0n)
2742 pool.close.go(t)
2743
2744def pool.close(p: Pool) -> IO(Unit):
2745 Pool{cap, idle} = p
2746 pool.close.go(Map.values(&1, List<&1, Conn>, idle))
2747
2748# RFC 9110 §9.2.2
2749def pool.idempotent(+method: String) -> Bool:
2750 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"))))))
2751
2752def conn.tls(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2753 (s, r) = m
2754 match r:
2755 case Fail{(+code, why)}:
2756 do IO<Result<&1, &1, Err, Conn>>:
2757 Wire.tls.close(s)
2758 return Fail{err.or_late(code, ErrTls{code, why})}
2759 case Done{u}:
2760 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2761
2762def conn.h2.sent(client: H2.Client, r: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2763 (s, sent) = r
2764 match sent:
2765 case Fail{(+code, why)}:
2766 do IO<Result<&1, &1, Err, Conn>>:
2767 Wire.tls.close(s)
2768 return Fail{err.or_late(code, ErrWrite{code, why})}
2769 case Done{u}:
2770 IO.pure(Result<&1, &1, Err, Conn>, Done{ConnH2{s, client}})
2771
2772def conn.h2.start(s: Socket, r: H2.Client & HBytes.Bytes) -> IO(Result<&1, &1, Err, Conn>):
2773 (client, HBytes.Bytes{len, buf}) = r
2774 do IO<Result<&1, &1, Err, Conn>>:
2775 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.send.words(s, len, buf)
2776 conn.h2.sent(client, sent)
2777
2778def conn.tls.protocol(proto: String, s: Socket) -> IO(Result<&1, &1, Err, Conn>):
2779 match proto:
2780 case "h2":
2781 conn.h2.start(s, H2.client.start())
2782 case "http/1.1":
2783 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2784 case "":
2785 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2786 case other:
2787 do IO<Result<&1, &1, Err, Conn>>:
2788 Wire.tls.close(s)
2789 return Fail{ErrTls{71, "unsupported ALPN: " ++ other}}
2790
2791def conn.tls.alpn(m: Socket & Result<&1, &1, U32 & String, String>) -> IO(Result<&1, &1, Err, Conn>):
2792 (s, r) = m
2793 match r:
2794 case Fail{(+code, why)}:
2795 do IO<Result<&1, &1, Err, Conn>>:
2796 Wire.tls.close(s)
2797 return Fail{err.or_late(code, ErrTls{code, why})}
2798 case Done{proto}:
2799 conn.tls.protocol(proto, s)
2800
2801def conn.secure.no.cert(offer: Bool, s: Socket, host: String, +ms: U32) ->
2802 IO(Result<&1, &1, Err, Conn>):
2803 match offer:
2804 case True{}:
2805 do IO<Result<&1, &1, Err, Conn>>:
2806 hs : Socket & Result<&1, &1, U32 & String, String> <-
2807 Wire.tls.connect.alpn(s, host, ms, "h2,http/1.1")
2808 conn.tls.alpn(hs)
2809 case False{}:
2810 do IO<Result<&1, &1, Err, Conn>>:
2811 hs : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.connect(s, host, ms)
2812 conn.tls(hs)
2813
2814def conn.secure.tls(cert: Maybe<&2, Cert>, s: Socket, host: String, +ms: U32,
2815 offer: Bool) -> IO(Result<&1, &1, Err, Conn>):
2816 match cert:
2817 case None{}:
2818 conn.secure.no.cert(offer, s, host, ms)
2819 case Some{Cert{chain, key}}:
2820 do IO<Result<&1, &1, Err, Conn>>:
2821 hs : Socket & Result<&1, &1, U32 & String, Unit> <-
2822 Wire.tls.connect.cert(s, host, ms, chain, key)
2823 conn.tls(hs)
2824
2825# A failed handshake is an error, never plaintext.
2826def conn.secure(+ms: U32, sni: String, s: Socket, tls: Bool,
2827 cert: Maybe<&2, Cert>, offer: Bool) -> IO(Result<&1, &1, Err, Conn>):
2828 match tls:
2829 case False{}:
2830 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{False{}, s}})
2831 case True{}:
2832 conn.secure.tls(cert, s, sni, ms, offer)
2833
2834def conn.made(+ms: U32, sni: String, tls: Bool, cert: Maybe<&2, Cert>,
2835 offer: Bool, r: Result<&1, &1, U32 & String, Socket>) ->
2836 IO(Result<&1, &1, Err, Conn>):
2837 match r:
2838 case Fail{(+code, why)}:
2839 IO.pure(Result<&1, &1, Err, Conn>, Fail{err.or_late(code, ErrConnect{code, why})})
2840 case Done{s}:
2841 conn.secure(ms, sni, s, tls, cert, offer)
2842
2843def conn.open(+tls: Bool, +ms: U32, sni: String, ip: String, port: U32) ->
2844 IO(Result<&1, &1, Err, Conn>):
2845 do IO<Result<&1, &1, Err, Conn>>:
2846 c : Result<&1, &1, U32 & String, Socket> <- Wire.connect(ip, port, ms)
2847 conn.made(ms, sni, tls, None{}, False{}, c)
2848
2849# ponytail: addresses are tried in order, not raced; a broken first route can consume the step timeout.
2850type Dial is Type:
2851 Dial{port: U32, ms: U32, deadline: Nat, action: IO(Result<&1, &1, U32 & String, Socket>)}
2852
2853def conn.dial.time(+ip: String, +port: U32, +deadline: Nat, now: Nat, expired: Bool) ->
2854 IO(Result<&1, &1, U32 & String, Socket>):
2855 match expired:
2856 case True{}:
2857 IO.pure(Result<&1, &1, U32 & String, Socket>, Fail{(60, "connect timeout")})
2858 case False{}:
2859 Wire.connect(ip, port, U32.from_nat(Nat.sub(deadline, now)))
2860
2861def conn.dial.with(+ip: String, +port: U32, +ms: U32, +deadline: Nat, +now: Nat, unlimited: Bool) ->
2862 IO(Result<&1, &1, U32 & String, Socket>):
2863 match unlimited:
2864 case True{}:
2865 Wire.connect(ip, port, 0)
2866 case False{}:
2867 conn.dial.time(ip, port, deadline, now, Nat.is_le(deadline, now))
2868
2869def conn.dial.try(+ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2870 IO(Result<&1, &1, U32 & String, Socket>):
2871 do IO<Result<&1, &1, U32 & String, Socket>>:
2872 now : Nat <- IO.now()
2873 conn.dial.with(ip, port, ms, deadline, now, U32.is_zero(ms))
2874
2875def conn.dial.after(r: Result<&1, &1, U32 & String, Socket>, ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2876 IO(Result<&1, &1, U32 & String, Socket>):
2877 match r:
2878 case Done{s}:
2879 IO.pure(Result<&1, &1, U32 & String, Socket>, Done{s})
2880 case Fail{e}:
2881 conn.dial.try(ip, port, ms, deadline)
2882
2883def conn.dial.more(prev: IO(Result<&1, &1, U32 & String, Socket>), ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2884 IO(Result<&1, &1, U32 & String, Socket>):
2885 do IO<Result<&1, &1, U32 & String, Socket>>:
2886 r : Result<&1, &1, U32 & String, Socket> <- prev
2887 conn.dial.after(r, ip, port, ms, deadline)
2888
2889def conn.dial.fold(d: Dial, ip: String) -> Dial:
2890 Dial{+port, +ms, +deadline, action} = d
2891 Dial{port, ms, deadline, conn.dial.more(action, ip, port, ms, deadline)}
2892
2893def conn.dial.run(d: Dial) -> IO(Result<&1, &1, U32 & String, Socket>):
2894 Dial{port, ms, deadline, action} = d
2895 action
2896
2897def conn.dial.all(+port: U32, +ms: U32, +start: Nat, first: String, rest: List<&2, String>) ->
2898 IO(Result<&1, &1, U32 & String, Socket>):
2899 match rest:
2900 case Nil{}:
2901 Wire.connect(first, port, ms)
2902 case Con{ip, tail}:
2903 +deadline = Nat.add(start, U32.to_nat(ms))
2904 conn.dial.run(List.foldl(~&2, ~String, ~Dial, ~conn.dial.fold, Con{ip, tail},
2905 Dial{port, ms, deadline, Wire.connect(first, port, ms)}))
2906
2907def conn.open.all(+tls: Bool, +ms: U32, +host: String, +port: U32,
2908 ips: List<&2, String>, cert: Maybe<&2, Cert>, offer: Bool) ->
2909 IO(Result<&1, &1, Err, Conn>):
2910 match ips:
2911 case Nil{}:
2912 IO.pure(Result<&1, &1, Err, Conn>, Fail{ErrDns{}})
2913 case Con{addr, rest}:
2914 do IO<Result<&1, &1, Err, Conn>>:
2915 start : Nat <- IO.now()
2916 r : Result<&1, &1, U32 & String, Socket> <- conn.dial.all(port, ms, start, addr, rest)
2917 conn.made(ms, host, tls, cert, offer, r)
2918
2919def proxy.auth.safe(s: String) -> Bool:
2920 match s:
2921 case SNil{}:
2922 True{}
2923 case SCon{Chr{+c}, rest}:
2924 Bool.and(U32.is_ge(c, 32), Bool.and(U32.is_ne(c, 127), proxy.auth.safe(rest)))
2925
2926def proxy.auth.checked(+decoded: String, valid: Bool) -> Maybe<&2, String>:
2927 match valid:
2928 case False{}:
2929 None{}
2930 case True{}:
2931 Some{"Basic " ++ Bytes.to_base64(Bytes.from_string(decoded))}
2932
2933def proxy.auth.value(m: Maybe<&2, String>) -> Maybe<&2, String>:
2934 match m:
2935 case None{}:
2936 None{}
2937 case Some{+decoded}:
2938 proxy.auth.checked(decoded, Bool.and(Url.has(decoded, 58), proxy.auth.safe(decoded)))
2939
2940def proxy.from.abs(authorization: String, m: Maybe<&2, Url.Abs>) -> Maybe<&2, Proxy>:
2941 match m:
2942 case None{}:
2943 None{}
2944 case Some{Url.Abs{scheme, host, port, target}}:
2945 Some{ProxyVia{host, port, authorization}}
2946
2947def proxy.from.user(user: String, host: String) -> Maybe<&2, Proxy>:
2948 do Maybe<&2, Proxy>:
2949 authorization : String <- proxy.auth.value(Url.pct.decode(user))
2950 proxy.from.abs(authorization, Url.absolute("http://" ++ host))
2951
2952def proxy.from.authority(has_user: Bool, authority: String, split: String & String) ->
2953 Maybe<&2, Proxy>:
2954 match has_user:
2955 case False{}:
2956 proxy.from.abs("", Url.absolute("http://" ++ authority))
2957 case True{}:
2958 (user, host) = split
2959 proxy.from.user(user, host)
2960
2961def proxy.from.parts(parts: String & String) -> Maybe<&2, Proxy>:
2962 (+authority, path) = parts
2963 match path:
2964 case SNil{}:
2965 proxy.from.authority(Url.has(authority, 64), authority, Url.take_to(authority, 64))
2966 case other:
2967 None{}
2968
2969def proxy.from.url.if(valid: Bool, raw: String) -> Maybe<&2, Proxy>:
2970 match valid:
2971 case False{}:
2972 None{}
2973 case True{}:
2974 proxy.from.parts(Url.take_to(String.drop(raw, 7n), 47))
2975
2976def proxy.from.url(+raw: String) -> Maybe<&2, Proxy>:
2977 proxy.from.url.if(String.starts_with(String.to_lower(raw), "http://"), raw)
2978
2979def proxy.no.domain(+host: String, +suffix: String) -> Bool:
2980 Bool.or(String.eq(host, suffix), String.ends_with(host, "." ++ suffix))
2981
2982def proxy.no.suffix(+host: String, +raw: String) -> Bool:
2983 match raw:
2984 case SCon{Chr{46}, +suffix}:
2985 proxy.no.domain(host, suffix)
2986 case other:
2987 proxy.no.domain(host, raw)
2988
2989def proxy.no.port(valid: Bool, +host: String, suffix: String) -> Bool:
2990 match valid:
2991 case False{}:
2992 False{}
2993 case True{}:
2994 proxy.no.suffix(host, suffix)
2995
2996def proxy.no.named(+host: String, +port: U32, parts: String & String) -> Bool:
2997 (suffix, port_text) = parts
2998 match port_text:
2999 case SNil{}:
3000 proxy.no.suffix(host, suffix)
3001 case other:
3002 proxy.no.port(String.eq(port_text, U32.show(port)), host, suffix)
3003
3004def proxy.no.literal(+host: String, +port: U32, +name: String) -> Bool:
3005 Bool.or(String.eq(name, host), Bool.or(String.eq(name, "[" ++ host ++ "]"),
3006 Bool.or(String.eq(name, host ++ ":" ++ U32.show(port)),
3007 String.eq(name, "[" ++ host ++ "]:" ++ U32.show(port)))))
3008
3009def proxy.no.token(+host: String, +port: U32, token: String) -> Bool:
3010 +name = String.to_lower(trim(token))
3011 Bool.or(String.eq(name, "*"),
3012 Bool.or(proxy.no.literal(host, port, name),
3013 Bool.and(Bool.not(Url.has(host, 58)),
3014 proxy.no.named(host, port, Url.take_to(name, 58)))))
3015
3016def proxy.no.list(xs: List<&2, String>, +host: String, +port: U32) -> Bool:
3017 match xs:
3018 case Nil{}:
3019 False{}
3020 case Con{token, rest}:
3021 Bool.or(proxy.no.token(host, port, token), proxy.no.list(rest, host, port))
3022
3023def proxy.no_match(+host: String, +port: U32, no_proxy: String) -> Bool:
3024 proxy.no.list(String.split(no_proxy, ','), String.to_lower(host), port)
3025
3026def proxy.env.value(r: Result<&1, &1, U32 & String, String>) -> String:
3027 match r:
3028 case Fail{e}:
3029 ""
3030 case Done{value}:
3031 value
3032
3033def proxy.env.lower(r: Result<&1, &1, U32 & String, String>, upper: String) ->
3034 IO(String):
3035 match r:
3036 case Done{value}:
3037 IO.pure(String, value)
3038 case Fail{e}:
3039 do IO<String>:
3040 got : Result<&1, &1, U32 & String, String> <- IO.get_env(upper)
3041 return proxy.env.value(got)
3042
3043def proxy.env(lower: String, upper: String) -> IO(String):
3044 do IO<String>:
3045 got : Result<&1, &1, U32 & String, String> <- IO.get_env(lower)
3046 proxy.env.lower(got, upper)
3047
3048def proxy.from.env(value: String) -> Maybe<&2, Proxy>:
3049 match value:
3050 case SNil{}:
3051 Some{ProxyDirect{}}
3052 case other:
3053 proxy.from.url(value)
3054
3055def proxy.choose(bypass: Bool, value: String) -> Maybe<&2, Proxy>:
3056 match bypass:
3057 case True{}:
3058 Some{ProxyDirect{}}
3059 case False{}:
3060 proxy.from.env(value)
3061
3062def proxy.select(+scheme: String, +host: String, +port: U32) ->
3063 IO(Maybe<&2, Proxy>):
3064 +secure = String.eq(scheme, "https")
3065 do IO<Maybe<&2, Proxy>>:
3066 bypass : String <- proxy.env("no_proxy", "NO_PROXY")
3067 value : String <- proxy.env(Bool.pick(String, secure, "https_proxy", "http_proxy"),
3068 Bool.pick(String, secure, "HTTPS_PROXY", "HTTP_PROXY"))
3069 return proxy.choose(proxy.no_match(host, port, bypass), value)
3070
3071def h2.header.skip(+name: String) -> Bool:
3072 match name:
3073 case SCon{Chr{58}, rest}:
3074 True{}
3075 case other:
3076 Bool.or(req.reserved(name),
3077 Bool.or(String.eq(name, "keep-alive"),
3078 Bool.or(String.eq(name, "proxy-connection"),
3079 Bool.or(String.eq(name, "upgrade"), String.eq(name, "te")))))
3080
3081def h2.header.mode(+name: String) -> U32:
3082 Bool.pick(U32,
3083 Bool.or(String.eq(name, "authorization"),
3084 Bool.or(String.eq(name, "cookie"), String.eq(name, "proxy-authorization"))),
3085 2, 0)
3086
3087def h2.header.values(+name: String, +mode: U32, vs: List<&2, String>) -> List<&2, Hpack.Field>:
3088 match vs:
3089 case Nil{}:
3090 Nil{}
3091 case Con{v, tail}:
3092 Hpack.Field{name, sanitize(v), mode} <> h2.header.values(name, mode, tail)
3093
3094def h2.header.tokens(vs: List<&2, String>) -> List<&2, String>:
3095 match vs:
3096 case Nil{}:
3097 Nil{}
3098 case Con{value, rest}:
3099 List.append(&2, String, String.split(value, ','), h2.header.tokens(rest))
3100
3101def h2.header.nominated.one(enabled: Bool, vs: List<&2, String>,
3102 rest: List<&2, String>) -> List<&2, String>:
3103 match enabled:
3104 case True{}:
3105 List.append(&2, String, h2.header.tokens(vs), rest)
3106 case False{}:
3107 rest
3108
3109def h2.header.nominated(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>) ->
3110 List<&2, String>:
3111 match xs:
3112 case Nil{}:
3113 Nil{}
3114 case (name, values) <> tail:
3115 h2.header.nominated.one(String.eq(String.to_lower(name), "connection"),
3116 values, h2.header.nominated(tail))
3117
3118def h2.header.has(xs: List<&2, String>, +key: String) -> Bool:
3119 match xs:
3120 case Nil{}:
3121 False{}
3122 case Con{value, rest}:
3123 Bool.or(String.eq(String.to_lower(trim(value)), key), h2.header.has(rest, key))
3124
3125def h2.header.item(skip: Bool, +name: String, vs: List<&2, String>,
3126 tail: List<&2, Hpack.Field>) -> List<&2, Hpack.Field>:
3127 match skip:
3128 case True{}:
3129 tail
3130 case False{}:
3131 List.append(&2, Hpack.Field, h2.header.values(name, h2.header.mode(name), vs), tail)
3132
3133def h2.header.items(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>,
3134 +nominated: List<&2, String>) -> List<&2, Hpack.Field>:
3135 match xs:
3136 case Nil{}:
3137 Nil{}
3138 case (name, values) <> tail:
3139 +key = String.to_lower(name)
3140 h2.header.item(Bool.or(h2.header.skip(key), h2.header.has(nominated, key)),
3141 key, values, h2.header.items(tail, nominated))
3142
3143def h2.request.fields(+method: String, target: String, authority: String,
3144 headers: Map<&2, List<&2, String>>) -> List<&2, Hpack.Field>:
3145 +xs = Map.to_list(&2, List<&2, String>, headers)
3146 List.append(&2, Hpack.Field,
3147 [Hpack.Field{":method", method, 0}, Hpack.Field{":scheme", "https", 0},
3148 Hpack.Field{":authority", authority, 0}, Hpack.Field{":path", target, 0}],
3149 h2.header.items(xs, h2.header.nominated(xs)))
3150
3151def h2.response.status.value(+value: String, valid: Bool) -> Maybe<&2, U32>:
3152 match valid:
3153 case False{}:
3154 None{}
3155 case True{}:
3156 parse_u32(value)
3157
3158def h2.response.status(xs: List<&2, Hpack.Field>) -> Maybe<&2, U32>:
3159 match xs:
3160 case Nil{}:
3161 None{}
3162 case Con{Hpack.Field{name, +value, mode}, tail}:
3163 match name:
3164 case ":status":
3165 h2.response.status.value(value, Nat.is_eq(String.length(value), 3n))
3166 case other:
3167 h2.response.status(tail)
3168
3169def h2.response.headers(xs: List<&2, Hpack.Field>, acc: Map<&2, List<&2, String>>) ->
3170 Map<&2, List<&2, String>>:
3171 match xs:
3172 case Nil{}:
3173 acc
3174 case Con{Hpack.Field{name, value, mode}, tail}:
3175 match name:
3176 case SCon{Chr{58}, rest}:
3177 h2.response.headers(tail, acc)
3178 case other:
3179 h2.response.headers(tail, add(acc, String.to_lower(name), value))
3180
3181def h2.response.final(interim: Bool, +status: U32, headers: List<&2, Hpack.Field>,
3182 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
3183 match interim:
3184 case True{}:
3185 Done{None{}}
3186 case False{}:
3187 HBytes.Bytes{len, buf} = body
3188 Done{Some{Res{status, h2.response.headers(headers, empty()), Bytes.Bytes{len, buf}}}}
3189
3190def h2.response.valid(valid: Bool, +status: U32, headers: List<&2, Hpack.Field>,
3191 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
3192 match valid:
3193 case False{}:
3194 Fail{ErrBad{}}
3195 case True{}:
3196 h2.response.final(U32.is_lt(status, 200), status, headers, body)
3197
3198def h2.response.parsed(m: Maybe<&2, U32>, headers: List<&2, Hpack.Field>,
3199 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
3200 match m:
3201 case None{}:
3202 Fail{ErrBad{}}
3203 case Some{+status}:
3204 h2.response.valid(Bool.and(U32.is_ge(status, 100), U32.is_lt(status, 600)),
3205 status, headers, body)
3206
3207def h2.response(+fields: List<&2, Hpack.Field>, body: HBytes.Bytes) ->
3208 Result<&1, &1, Err, Maybe<&1, Res>>:
3209 h2.response.parsed(h2.response.status(fields), fields, body)
3210
3211def h2.event.fold(acc: Result<&1, &1, Err, Maybe<&1, Res>>,
3212 event: H2.ClientEvent) -> Result<&1, &1, Err, Maybe<&1, Res>>:
3213 match acc:
3214 case Fail{e}:
3215 Fail{e}
3216 case Done{Some{res}}:
3217 Done{Some{res}}
3218 case Done{None{}}:
3219 match event:
3220 case H2.Response{id, headers, body}:
3221 h2.response(headers, body)
3222 case H2.Reset{id, code}:
3223 Fail{ErrBad{}}
3224 case H2.Shutdown{last, code}:
3225 Done{None{}}
3226 case H2.Pong{data}:
3227 Done{None{}}
3228
3229def h2.send.report(r: Socket & Result<&1, &1, U32 & String, Unit>) ->
3230 IO(Result<&1, &1, Err, Socket>):
3231 (s, sent) = r
3232 match sent:
3233 case Fail{(+code, why)}:
3234 do IO<Result<&1, &1, Err, Socket>>:
3235 Wire.tls.close(s)
3236 return Fail{err.or_late(code, ErrWrite{code, why})}
3237 case Done{unit}:
3238 IO.pure(Result<&1, &1, Err, Socket>, Done{s})
3239
3240def h2.send.one(prev: Result<&1, &1, Err, Socket>, b: HBytes.Bytes) ->
3241 IO(Result<&1, &1, Err, Socket>):
3242 match prev:
3243 case Fail{e}:
3244 IO.pure(Result<&1, &1, Err, Socket>, Fail{e})
3245 case Done{s}:
3246 HBytes.Bytes{len, buf} = b
3247 do IO<Result<&1, &1, Err, Socket>>:
3248 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.send.words(s, len, buf)
3249 h2.send.report(sent)
3250
3251def h2.send.fold(prev: IO(Result<&1, &1, Err, Socket>), b: HBytes.Bytes) ->
3252 IO(Result<&1, &1, Err, Socket>):
3253 do IO<Result<&1, &1, Err, Socket>>:
3254 r : Result<&1, &1, Err, Socket> <- prev
3255 h2.send.one(r, b)
3256
3257def h2.send(xs: List<&1, HBytes.Bytes>, s: Socket) -> IO(Result<&1, &1, Err, Socket>):
3258 List.foldl(~&1, ~HBytes.Bytes, ~IO(Result<&1, &1, Err, Socket>), ~h2.send.fold,
3259 xs, IO.pure(Result<&1, &1, Err, Socket>, Done{s}))
3260
3261def h2.received.step(over: Bool, s: Socket, client: H2.Client,
3262 +len: U32, buf: Array<U32>) -> H2Step:
3263 match over:
3264 case True{}:
3265 H2Reply{s, H2.Failed{H2.Error{1, True{}, 0}}}
3266 case False{}:
3267 H2Reply{s, H2.client.receive(client, HBytes.Bytes{len, buf})}
3268
3269def h2.fail(s: Socket, e: Err) -> IO(Result<&1, &1, Err, Conn & Res>):
3270 do IO<Result<&1, &1, Err, Conn & Res>>:
3271 Wire.tls.close(s)
3272 return Fail{e}
3273
3274def h2.loop(n: Nat, step: H2Step, +ms: U32, +used: U32) ->
3275 IO(Result<&1, &1, Err, Conn & Res>):
3276 match n:
3277 case 0n:
3278 match step:
3279 case H2Reply{s, reply}:
3280 h2.fail(s, ErrBad{})
3281 case H2Sent{client, events, sent}:
3282 match sent:
3283 case Fail{e}:
3284 IO.pure(Result<&1, &1, Err, Conn & Res>, Fail{e})
3285 case Done{s}:
3286 h2.fail(s, ErrBad{})
3287 case H2Events{s, client, result}:
3288 h2.fail(s, ErrBad{})
3289 case H2Received{client, answer}:
3290 (s, r) = answer
3291 h2.fail(s, ErrBad{})
3292 case 1n+p:
3293 match step:
3294 case H2Reply{s, reply}:
3295 match reply:
3296 case H2.Failed{error}:
3297 h2.fail(s, ErrBad{})
3298 case H2.Ready{client, writes, events}:
3299 do IO<Result<&1, &1, Err, Conn & Res>>:
3300 sent : Result<&1, &1, Err, Socket> <- h2.send(writes, s)
3301 h2.loop(p, H2Sent{client, events, sent}, ms, used)
3302 case H2Sent{client, events, sent}:
3303 match sent:
3304 case Fail{e}:
3305 IO.pure(Result<&1, &1, Err, Conn & Res>, Fail{e})
3306 case Done{s}:
3307 h2.loop(p, H2Events{s, client,
3308 List.foldl(~&1, ~H2.ClientEvent,
3309 ~Result<&1, &1, Err, Maybe<&1, Res>>, ~h2.event.fold,
3310 events, Done{None{}})}, ms, used)
3311 case H2Events{s, client, result}:
3312 match result:
3313 case Fail{e}:
3314 h2.fail(s, e)
3315 case Done{Some{res}}:
3316 IO.pure(Result<&1, &1, Err, Conn & Res>,
3317 Done{(ConnH2{s, client}, res)})
3318 case Done{None{}}:
3319 do IO<Result<&1, &1, Err, Conn & Res>>:
3320 r : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
3321 Wire.tls.recv.words(s, 16384, ms)
3322 h2.loop(p, H2Received{client, r}, ms, used)
3323 case H2Received{client, answer}:
3324 match answer:
3325 case (s, Fail{(+code, why)}):
3326 h2.fail(s, err.or_late(code, ErrRead{code, why}))
3327 case (s, Done{(0, buf)}):
3328 h2.fail(s, ErrBad{})
3329 case (s, Done{(+len, buf)}):
3330 +total = (used + len : U32)
3331 h2.loop(p, h2.received.step(fetch.over(total), s, client, len, buf), ms, total)
3332
3333def h2.exchange(s: Socket, client: H2.Client, +ms: U32, request: Send) ->
3334 IO(Result<&1, &1, Err, Conn & Res>):
3335 Send{method, target, authority, headers, Bytes.Bytes{len, buf}} = request
3336 h2.loop(Nat.mul(4n, Nat.add(fetch.max(), 65536n)),
3337 H2Reply{s, H2.client.request(client,
3338 h2.request.fields(method, target, authority, headers), HBytes.Bytes{len, buf})},
3339 ms, 0)
3340
3341def proxy.connect.fail(s: Socket, e: Err) -> IO(Result<&1, &1, Err, Conn>):
3342 do IO<Result<&1, &1, Err, Conn>>:
3343 io.close(False{}, s)
3344 return Fail{e}
3345
3346def proxy.connect.extra(m: Maybe<&2, String>, s: Socket, +ms: U32,
3347 sni: String, cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
3348 match m:
3349 case None{}:
3350 proxy.connect.fail(s, ErrBad{})
3351 case Some{rest}:
3352 match rest:
3353 case SNil{}:
3354 conn.secure(ms, sni, s, True{}, cert, True{})
3355 case other:
3356 proxy.connect.fail(s, ErrBad{})
3357
3358def proxy.connect.status(ok: Bool, +status: U32, raw: String, s: Socket,
3359 +ms: U32, sni: String, cert: Maybe<&2, Cert>) ->
3360 IO(Result<&1, &1, Err, Conn>):
3361 match ok:
3362 case False{}:
3363 proxy.connect.fail(s, ErrConnect{status, "proxy CONNECT refused"})
3364 case True{}:
3365 proxy.connect.extra(after(raw, True{}), s, ms, sni, cert)
3366
3367def proxy.connect.finish(res: Res, raw: String, s: Socket, +ms: U32,
3368 sni: String, cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
3369 Res{+status, headers, body} = res
3370 proxy.connect.status(Bool.and(U32.is_ge(status, 200), U32.is_lt(status, 300)),
3371 status, raw, s, ms, sni, cert)
3372
3373def proxy.connect.frame(raw: String, over: Bool) -> Frame:
3374 match over:
3375 case True{}:
3376 FrameBad{}
3377 case False{}:
3378 frame(raw, False{}, True{})
3379
3380def proxy.connect.chunk(empty: Bool, s: Socket, raw: String,
3381 +len: U32, buf: Array<U32>) -> TunnelStep:
3382 match empty:
3383 case True{}:
3384 TunnelHead{s, raw, FrameBad{}}
3385 case False{}:
3386 TunnelRead{s, raw ++ Bytes.to_string(Bytes.Bytes{len, buf})}
3387
3388def proxy.connect.loop(n: Nat, step: TunnelStep, +ms: U32, +sni: String,
3389 +cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
3390 match n:
3391 case 0n:
3392 match step:
3393 case TunnelRead{s, raw}:
3394 proxy.connect.fail(s, ErrBad{})
3395 case TunnelHead{s, raw, result}:
3396 proxy.connect.fail(s, ErrBad{})
3397 case TunnelGot{raw, answer}:
3398 (s, result) = answer
3399 proxy.connect.fail(s, ErrBad{})
3400 case 1n+p:
3401 match step:
3402 case TunnelRead{s, +raw}:
3403 proxy.connect.loop(p, TunnelHead{s, raw,
3404 proxy.connect.frame(raw, Nat.is_gt(String.length(raw), 65536n))},
3405 ms, sni, cert)
3406 case TunnelHead{s, raw, result}:
3407 match result:
3408 case FrameBad{}:
3409 proxy.connect.fail(s, ErrBad{})
3410 case FrameMore{}:
3411 do IO<Result<&1, &1, Err, Conn>>:
3412 answer : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
3413 io.recv.words(False{}, s, 4096, ms)
3414 proxy.connect.loop(p, TunnelGot{raw, answer}, ms, sni, cert)
3415 case FrameDone{res}:
3416 proxy.connect.finish(res, raw, s, ms, sni, cert)
3417 case TunnelGot{raw, answer}:
3418 match answer:
3419 case (s, Fail{(+code, why)}):
3420 proxy.connect.fail(s, err.or_late(code, ErrRead{code, why}))
3421 case (s, Done{(+len, buf)}):
3422 proxy.connect.loop(p,
3423 proxy.connect.chunk(U32.is_zero(len), s, raw, len, buf),
3424 ms, sni, cert)
3425
3426def proxy.connect.header(+authority: String, authorization: String) -> String:
3427 match authorization:
3428 case SNil{}:
3429 "CONNECT " ++ authority ++ " HTTP/1.1\r\nHost: " ++ authority ++ "\r\n\r\n"
3430 case other:
3431 "CONNECT " ++ authority ++ " HTTP/1.1\r\nHost: " ++ authority
3432 ++ "\r\nProxy-Authorization: " ++ authorization ++ "\r\n\r\n"
3433
3434def proxy.connect.sent(r: Socket & Result<&1, &1, U32 & String, Unit>,
3435 +ms: U32, sni: String, cert: Maybe<&2, Cert>) ->
3436 IO(Result<&1, &1, Err, Conn>):
3437 (s, sent) = r
3438 match sent:
3439 case Fail{(+code, why)}:
3440 proxy.connect.fail(s, err.or_late(code, ErrWrite{code, why}))
3441 case Done{unit}:
3442 proxy.connect.loop(Nat.mul(3n, 65536n), TunnelRead{s, ""}, ms, sni, cert)
3443
3444def proxy.connect(s: Socket, +ms: U32, sni: String, authority: String,
3445 authorization: String, cert: Maybe<&2, Cert>) ->
3446 IO(Result<&1, &1, Err, Conn>):
3447 do IO<Result<&1, &1, Err, Conn>>:
3448 sent : Socket & Result<&1, &1, U32 & String, Unit> <-
3449 io.send.bytes(False{}, s, Bytes.from_string(proxy.connect.header(authority, authorization)))
3450 proxy.connect.sent(sent, ms, sni, cert)
3451
3452def proxy.route.tls(tls: Bool, s: Socket, +ms: U32, sni: String,
3453 authority: String, authorization: String, cert: Maybe<&2, Cert>) ->
3454 IO(Result<&1, &1, Err, Conn>):
3455 match tls:
3456 case False{}:
3457 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{False{}, s}})
3458 case True{}:
3459 proxy.connect(s, ms, sni, authority, authorization, cert)
3460
3461def proxy.route.connected(tls: Bool, +ms: U32, sni: String, authority: String,
3462 authorization: String, cert: Maybe<&2, Cert>,
3463 r: Result<&1, &1, Err, Conn>) -> IO(Result<&1, &1, Err, Conn>):
3464 match r:
3465 case Fail{e}:
3466 IO.pure(Result<&1, &1, Err, Conn>, Fail{e})
3467 case Done{c}:
3468 match c:
3469 case Conn{plain, s}:
3470 proxy.route.tls(tls, s, ms, sni, authority, authorization, cert)
3471 case ConnH2{s, client}:
3472 do IO<Result<&1, &1, Err, Conn>>:
3473 Wire.tls.close(s)
3474 return Fail{ErrBad{}}
3475
3476def proxy.route.open(+ms: U32, +tls: Bool, +host: String, +port: U32,
3477 +sni: String, +authority: String, +authorization: String,
3478 cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
3479 do IO<Result<&1, &1, Err, Conn>>:
3480 ips : List<&2, String> <- Dns.resolve.all(host)
3481 conn : Result<&1, &1, Err, Conn> <-
3482 conn.open.all(False{}, ms, host, port, ips, None{}, False{})
3483 proxy.route.connected(tls, ms, sni, authority, authorization, cert, conn)
3484
3485def route.open(+ms: U32, route: Route) -> IO(Result<&1, &1, Err, Conn>):
3486 match route:
3487 case RouteDirect{tls, +host, port, cert}:
3488 do IO<Result<&1, &1, Err, Conn>>:
3489 ips : List<&2, String> <- Dns.resolve.all(host)
3490 conn.open.all(tls, ms, host, port, ips, cert, True{})
3491 case RouteProxy{tls, host, port, sni, authority, authorization, cert}:
3492 proxy.route.open(ms, tls, host, port, sni, authority, authorization, cert)
3493
3494def conn.ex.h1(+tls: Bool, s: Socket, +ms: U32, request: Send) -> IO(Out):
3495 Send{+method, target, authority, headers, body} = request
3496 exchange.go(tls, ms, False{}, String.eq(method, "HEAD"), s,
3497 encode_req.on(method, target, authority, headers, body, False{}))
3498
3499# A socket with bytes past the response is out of step with the server, so it is closed.
3500def pool.keep.s(p: Pool, +key: String, +tls: Bool, res: Res, s: Socket, clean: Bool) -> IO(Pool & Result<&1, &1, Err, Res>):
3501 match clean:
3502 case True{}:
3503 do IO<Pool & Result<&1, &1, Err, Res>>:
3504 p2 : Pool <- pool.give(p, key, Conn{tls, s})
3505 return (p2, Done{res})
3506 case False{}:
3507 do IO<Pool & Result<&1, &1, Err, Res>>:
3508 io.close(tls, s)
3509 return (p, Done{res})
3510
3511def pool.keep.m(p: Pool, +key: String, +tls: Bool, res: Res, +clean: Bool, sock: Maybe<&1, Socket>) -> IO(Pool & Result<&1, &1, Err, Res>):
3512 match sock:
3513 case None{}:
3514 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Done{res}))
3515 case Some{s}:
3516 pool.keep.s(p, key, tls, res, s, clean)
3517
3518def pool.keep(p: Pool, +key: String, +tls: Bool, res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
3519 Bytes.Bytes{+len, buf} = rest
3520 pool.keep.m(p, key, tls, res, U32.is_zero(len), sock)
3521
3522def pool.after(p: Pool, +key: String, +tls: Bool, o: Out) -> IO(Pool & Result<&1, &1, Err, Res>):
3523 match o:
3524 case OutFail{e, none}:
3525 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
3526 case OutDone{res, sock, rest}:
3527 pool.keep(p, key, tls, res, sock, rest)
3528
3529def pool.h2.reusable(c: Conn) -> Bool & Conn:
3530 match c:
3531 case Conn{tls, s}:
3532 (True{}, Conn{tls, s})
3533 case ConnH2{s, H2.Client{input, streams, encoder, decoder, +control}}:
3534 H2.Control{next, active, frame_max, initial, max_streams, send_window,
3535 recv_window, first, ack, continuation, +goaway} = control
3536 (Maybe.is_none(&2, U32, goaway),
3537 ConnH2{s, H2.Client{input, streams, encoder, decoder, control}})
3538
3539def pool.h2.keep(p: Pool, +key: String, res: Res, state: Bool & Conn) ->
3540 IO(Pool & Result<&1, &1, Err, Res>):
3541 (reusable, c) = state
3542 match reusable:
3543 case True{}:
3544 do IO<Pool & Result<&1, &1, Err, Res>>:
3545 next : Pool <- pool.give(p, key, c)
3546 return (next, Done{res})
3547 case False{}:
3548 do IO<Pool & Result<&1, &1, Err, Res>>:
3549 conn.close(c)
3550 return (p, Done{res})
3551
3552def pool.h2.result(p: Pool, +key: String, r: Result<&1, &1, Err, Conn & Res>) ->
3553 IO(Pool & Result<&1, &1, Err, Res>):
3554 match r:
3555 case Fail{e}:
3556 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
3557 case Done{(c, res)}:
3558 pool.h2.keep(p, key, res, pool.h2.reusable(c))
3559
3560def pool.h2.ex(p: Pool, +key: String, +ms: U32, request: Send,
3561 s: Socket, client: H2.Client) -> IO(Pool & Result<&1, &1, Err, Res>):
3562 do IO<Pool & Result<&1, &1, Err, Res>>:
3563 r : Result<&1, &1, Err, Conn & Res> <- h2.exchange(s, client, ms, request)
3564 pool.h2.result(p, key, r)
3565
3566def pool.fresh.conn(p: Pool, +key: String, +ms: U32, request: Send,
3567 r: Result<&1, &1, Err, Conn>) -> IO(Pool & Result<&1, &1, Err, Res>):
3568 match r:
3569 case Fail{e}:
3570 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
3571 case Done{c}:
3572 match c:
3573 case Conn{+tls, s}:
3574 do IO<Pool & Result<&1, &1, Err, Res>>:
3575 o : Out <- conn.ex.h1(tls, s, ms, request)
3576 pool.after(p, key, tls, o)
3577 case ConnH2{s, client}:
3578 pool.h2.ex(p, key, ms, request, s, client)
3579
3580def pool.fresh(p: Pool, +key: String, +ms: U32, request: Send, route: Route) ->
3581 IO(Pool & Result<&1, &1, Err, Res>):
3582 do IO<Pool & Result<&1, &1, Err, Res>>:
3583 c : Result<&1, &1, Err, Conn> <- route.open(ms, route)
3584 pool.fresh.conn(p, key, ms, request, c)
3585
3586# A reused socket the server already closed fails before any response byte.
3587def pool.retry(+none: Bool, +idem: Bool) -> Bool:
3588 Bool.and(none, idem)
3589
3590def pool.stale(p: Pool, +key: String, +ms: U32, request: Send,
3591 e: Err, again: Bool, route: Route) ->
3592 IO(Pool & Result<&1, &1, Err, Res>):
3593 match again:
3594 case True{}:
3595 pool.fresh(p, key, ms, request, route)
3596 case False{}:
3597 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
3598
3599def pool.reused(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
3600 spare: Send, o: Out, route: Route) ->
3601 IO(Pool & Result<&1, &1, Err, Res>):
3602 match o:
3603 case OutFail{e, +none}:
3604 pool.stale(p, key, ms, spare, e, pool.retry(none, idem), route)
3605 case OutDone{res, sock, rest}:
3606 pool.keep(p, key, tls, res, sock, rest)
3607
3608# Copy only the reused HTTP/1.1 request body, for a stale-socket retry.
3609def pool.idle.h1.bodies(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
3610 s: Socket, +method: String, +target: String, +authority: String,
3611 +headers: Map<&2, List<&2, String>>, r: Bytes.Bytes & Bytes.Bytes,
3612 route: Route) -> IO(Pool & Result<&1, &1, Err, Res>):
3613 (wire, spare) = r
3614 do IO<Pool & Result<&1, &1, Err, Res>>:
3615 o : Out <- conn.ex.h1(tls, s, ms, Send{method, target, authority, headers, wire})
3616 pool.reused(p, key, tls, ms, idem,
3617 Send{method, target, authority, headers, spare}, o, route)
3618
3619def pool.idle.h1(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
3620 s: Socket, request: Send, route: Route) ->
3621 IO(Pool & Result<&1, &1, Err, Res>):
3622 Send{+method, +target, +authority, +headers, body} = request
3623 pool.idle.h1.bodies(p, key, tls, ms, idem, s, method, target,
3624 authority, headers, Bytes.slice(body, 0, 4294967295), route)
3625
3626def pool.idle.reuse(p: Pool, +key: String, +ms: U32, +idem: Bool,
3627 c: Conn, request: Send, route: Route) ->
3628 IO(Pool & Result<&1, &1, Err, Res>):
3629 match c:
3630 case Conn{tls, s}:
3631 pool.idle.h1(p, key, tls, ms, idem, s, request, route)
3632 case ConnH2{s, client}:
3633 pool.h2.ex(p, key, ms, request, s, client)
3634
3635def pool.idle(taken: Pool & Maybe<&1, Conn>, +key: String, +ms: U32,
3636 +idem: Bool, request: Send, route: Route) ->
3637 IO(Pool & Result<&1, &1, Err, Res>):
3638 (p, m) = taken
3639 match m:
3640 case None{}:
3641 pool.fresh(p, key, ms, request, route)
3642 case Some{c}:
3643 pool.idle.reuse(p, key, ms, idem, c, request, route)
3644
3645def proxy.http.headers(headers: Map<&2, List<&2, String>>,
3646 authorization: String) -> Map<&2, List<&2, String>>:
3647 match authorization:
3648 case SNil{}:
3649 headers
3650 case other:
3651 set(headers, "proxy-authorization", authorization)
3652
3653def proxy.absolute(scheme: String, host_field: String, target: String) -> String:
3654 scheme ++ "://" ++ host_field ++ target
3655
3656def proxy.request(secure: Bool, +scheme: String, method: String,
3657 +target: String, +hf: String, headers: Map<&2, List<&2, String>>,
3658 body: Bytes.Bytes, authorization: String) -> Send:
3659 match secure:
3660 case True{}:
3661 Send{method, target, hf, Map.del(&2, List<&2, String>, headers,
3662 "proxy-authorization"), body}
3663 case False{}:
3664 Send{method, proxy.absolute(scheme, hf, target), hf,
3665 proxy.http.headers(headers, authorization), body}
3666
3667def pool.origin.proxy(p: Pool, +method: String, +ms: U32,
3668 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +hf: String,
3669 +scheme: String, +host: String, +port: U32, +target: String,
3670 +cert: Maybe<&2, Cert>, proxy: Proxy) ->
3671 IO(Pool & Result<&1, &1, Err, Res>):
3672 match proxy:
3673 case ProxyDirect{}:
3674 +key = pool.key.cert(pool.key(scheme, host, port), cert)
3675 pool.idle(pool.take(p, key), key, ms, pool.idempotent(method),
3676 Send{method, target, hf, headers, body},
3677 RouteDirect{String.eq(scheme, "https"), host, port, cert})
3678 case ProxyVia{+proxy_host, +proxy_port, +authorization}:
3679 +secure = String.eq(scheme, "https")
3680 +key = pool.key.cert(pool.key(scheme, host, port)
3681 ++ "|proxy:" ++ proxy_host ++ ":" ++ U32.show(proxy_port)
3682 ++ "|auth:" ++ authorization, cert)
3683 pool.idle(pool.take(p, key), key, ms, pool.idempotent(method),
3684 proxy.request(secure, scheme, method, target, hf, headers, body, authorization),
3685 RouteProxy{secure, proxy_host, proxy_port, host,
3686 Url.host_field.wrap(host, Url.has(host, 58)) ++ ":" ++ U32.show(port),
3687 authorization, cert})
3688
3689def pool.origin.choice(p: Pool, method: String, ms: U32,
3690 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, hf: String,
3691 scheme: String, host: String, port: U32, target: String,
3692 cert: Maybe<&2, Cert>, choice: Maybe<&2, Proxy>) ->
3693 IO(Pool & Result<&1, &1, Err, Res>):
3694 match choice:
3695 case None{}:
3696 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrUrl{}}))
3697 case Some{proxy}:
3698 pool.origin.proxy(p, method, ms, headers, body, hf, scheme, host, port,
3699 target, cert, proxy)
3700
3701def pool.origin(p: Pool, method: String, ms: U32,
3702 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, hf: String,
3703 a: Url.Abs, known: Bool, cert: Maybe<&2, Cert>,
3704 choice: Maybe<&2, Proxy>) ->
3705 IO(Pool & Result<&1, &1, Err, Res>):
3706 Url.Abs{scheme, host, port, target} = a
3707 match known:
3708 case False{}:
3709 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrUrl{}}))
3710 case True{}:
3711 pool.origin.choice(p, method, ms, headers, body, hf, scheme, host,
3712 port, target, cert, choice)
3713
3714def pool.scheme.ok(a: Url.Abs) -> Bool:
3715 Url.Abs{+scheme, host, port, target} = a
3716 Bool.or(String.eq(scheme, "http"), String.eq(scheme, "https"))
3717
3718def pool.one.back(h: Hop, pr: Pool & Result<&1, &1, Err, Res>) -> Pool & Result<&1, &1, Err, Res> & Hop:
3719 (p, r) = pr
3720 (p, r, h)
3721
3722# sent is headers plus any jar cookies; the hop keeps headers, so cookies never pile up across hops.
3723def pool.one.of(p: Pool, +method: String, +url: Url.Abs,
3724 headers: Map<&2, List<&2, String>>, sent: Map<&2, List<&2, String>>,
3725 +ms: U32, r: Bytes.Bytes & Bytes.Bytes, cert: Maybe<&2, Cert>) ->
3726 IO(Pool & Result<&1, &1, Err, Res> & Hop):
3727 Url.Abs{+scheme, +host, +port, target} = url
3728 (body, wire) = r
3729 do IO<Pool & Result<&1, &1, Err, Res> & Hop>:
3730 choice : Maybe<&2, Proxy> <- proxy.select(scheme, host, port)
3731 pr : Pool & Result<&1, &1, Err, Res> <-
3732 pool.origin(p, method, ms, sent, wire, Url.host_field(url),
3733 url, pool.scheme.ok(url), cert, choice)
3734 return pool.one.back(Hop{method, url, headers, body}, pr)
3735
3736# One request, on an idle socket to its origin when the pool has one. The hop comes back for the redirect.
3737def pool.one(p: Pool, h: Hop, +ms: U32, cert: Maybe<&2, Cert>, jar: Maybe<&2, Jar>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
3738 Hop{+method, +url, +headers, body} = h
3739 pool.one.of(p, method, url, headers, jar.opt.apply(jar, url, headers), ms, Bytes.slice(body, 0, 4294967295), cert)
3740
3741type Next is Type:
3742 NDone{res: Result<&1, &1, Err, Res>}
3743 NStop{}
3744 NGo{left: Nat, hop: Hop}
3745
3746type Mode is Data:
3747 ModeFollow{}
3748 ModeManual{}
3749 ModeError{}
3750
3751# left: redirects still allowed after the request we just finished.
3752def fetch.hop(left: Nat, h: Hop) -> Next:
3753 match left:
3754 case 0n:
3755 NStop{}
3756 case 1n+p:
3757 NGo{p, h}
3758
3759def fetch.decide.r(left: Nat, r: Res, next: Maybe<&1, Hop>) -> Next:
3760 match next:
3761 case None{}:
3762 NDone{Done{r}}
3763 case Some{h}:
3764 fetch.hop(left, h)
3765
3766def fetch.decide.res(left: Nat, h: Hop, r: Res) -> Next:
3767 Res{+status, +headers, body} = r
3768 fetch.decide.r(left, Res{status, headers, body}, redirect(status, headers, h))
3769
3770def fetch.decide(left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
3771 match m:
3772 case Fail{e}:
3773 NDone{Fail{e}}
3774 case Done{r}:
3775 fetch.decide.res(left, h, r)
3776
3777def fetch.error.res(r: Res, bad: Bool) -> Next:
3778 match bad:
3779 case True{}:
3780 NDone{Fail{ErrRedirect{}}}
3781 case False{}:
3782 NDone{Done{r}}
3783
3784def fetch.error(h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
3785 match m:
3786 case Fail{e}:
3787 NDone{Fail{e}}
3788 case Done{r}:
3789 Res{+status, +headers, body} = r
3790 fetch.error.res(Res{status, headers, body}, Bool.and(redirect.code(status), has_header(headers, "location")))
3791
3792def fetch.policy(mode: Mode, left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
3793 match mode:
3794 case ModeFollow{}:
3795 fetch.decide(left, h, m)
3796 case ModeManual{}:
3797 NDone{m}
3798 case ModeError{}:
3799 fetch.error(h, m)
3800
3801# A caller's own Accept-Encoding wins; enc is the codings fetch can undo.
3802def accept.enc(+h: Map<&2, List<&2, String>>, +enc: String) -> Map<&2, List<&2, String>>:
3803 Bool.pick(Map<&2, List<&2, String>>, has_header(h, "accept-encoding"), h, set(h, "accept-encoding", enc))
3804
3805def fetch.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>, +enc: String) -> Next:
3806 match u:
3807 case None{}:
3808 NDone{Fail{ErrUrl{}}}
3809 case Some{a}:
3810 NGo{20n, Hop{method, a, accept.enc(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), enc), body}}
3811
3812# The redirect loop's state: the pool, what to do next, the client identity, and the jar if any.
3813type Hops is Type:
3814 Hops{p: Pool, next: Next, cert: Maybe<&2, Cert>, jar: Maybe<&2, Jar>}
3815
3816def pool.next.move(p: Pool, +old: String, cert: Maybe<&2, Cert>, jar: Maybe<&2, Jar>, n: Next) -> Hops:
3817 match n:
3818 case NGo{left, h}:
3819 Hop{method, +url, headers, body} = h
3820 Hops{p, NGo{left, Hop{method, url, headers, body}},
3821 Bool.pick(Maybe<&2, Cert>, String.eq(old, redirect.origin(url)), cert, None{}), jar}
3822 case NDone{r}:
3823 Hops{p, NDone{r}, None{}, jar}
3824 case NStop{}:
3825 Hops{p, NStop{}, None{}, jar}
3826
3827def pool.next.of(+mode: Mode, left: Nat, cert: Maybe<&2, Cert>, p: Pool, +url: Url.Abs, h: Hop, r: Maybe<&2, Jar> & Result<&1, &1, Err, Res>) -> Hops:
3828 (jar, m) = r
3829 pool.next.move(p, redirect.origin(url), cert, jar, fetch.policy(mode, left, h, m))
3830
3831# The jar takes the response's Set-Cookie fields first, redirect or not.
3832def pool.next(+mode: Mode, left: Nat, cert: Maybe<&2, Cert>, jar: Maybe<&2, Jar>, x: Pool & Result<&1, &1, Err, Res> & Hop) -> Hops:
3833 (p, m, h) = x
3834 Hop{method, +url, headers, body} = h
3835 pool.next.of(mode, left, cert, p, url, Hop{method, url, headers, body}, jar.opt.store(jar, url, m))
3836
3837def pool.hops.one(+mode: Mode, +ms: U32, +cert: Maybe<&2, Cert>, +jar: Maybe<&2, Jar>, p: Pool, h: Hop, left: Nat) -> IO(Hops):
3838 do IO<Hops>:
3839 x : Pool & Result<&1, &1, Err, Res> & Hop <- pool.one(p, h, ms, cert, jar)
3840 return pool.next(mode, left, cert, jar, x)
3841
3842# NGo.left is how many redirects may follow this request. 20 is WHATWG's limit.
3843# The jar, when there is one, gives cookies to every hop and takes them from every response.
3844@unsafe
3845def pool.hops(+mode: Mode, +ms: U32, st: Hops) -> IO(Pool & Result<&1, &1, Err, Res> & Maybe<&2, Jar>):
3846 Hops{p, n, cert, cj} = st
3847 match n:
3848 case NDone{m}:
3849 IO.pure(Pool & Result<&1, &1, Err, Res> & Maybe<&2, Jar>, (p, m, cj))
3850 case NStop{}:
3851 IO.pure(Pool & Result<&1, &1, Err, Res> & Maybe<&2, Jar>, (p, Fail{ErrRedirect{}}, cj))
3852 case NGo{+left, h}:
3853 do IO<Pool & Result<&1, &1, Err, Res> & Maybe<&2, Jar>>:
3854 next : Hops <- pool.hops.one(mode, ms, cert, cj, p, h, left)
3855 pool.hops(mode, ms, next)
3856
3857# Content-Encoding (RFC 9110 §8.4): each value, trimmed and lowercased, in the order applied.
3858def ce.keep(+w: String, +rest: List<&2, String>) -> List<&2, String>:
3859 Bool.pick(List<&2, String>, String.is_empty(w), rest, Con{w, rest})
3860
3861def ce.norm(xs: List<&2, String>) -> List<&2, String>:
3862 match xs:
3863 case Nil{}:
3864 Nil{}
3865 case Con{v, t}:
3866 ce.keep(String.to_lower(trim(v)), ce.norm(t))
3867
3868def ce.split(xs: List<&2, String>) -> List<&2, String>:
3869 match xs:
3870 case Nil{}:
3871 Nil{}
3872 case Con{v, t}:
3873 List.append(&2, String, ce.norm(String.split(v, ',')), ce.split(t))
3874
3875# Ok: decoded so far. Bad: a coding failed. Skip: a coding we cannot decode, so the body stays as sent.
3876type Dec is Data:
3877 DecOk{b: String}
3878 DecBad{}
3879 DecSkip{}
3880
3881def ce.of(m: Maybe<&2, String>) -> Dec:
3882 match m:
3883 case None{}:
3884 DecBad{}
3885 case Some{b}:
3886 DecOk{b}
3887
3888# Servers send deflate both with and without the zlib wrapper.
3889def ce.deflate(+b: String, m: Maybe<&2, String>) -> Dec:
3890 match m:
3891 case Some{out}:
3892 DecOk{out}
3893 case None{}:
3894 ce.of(Zlib.inflate(b))
3895
3896def ce.apply(+c: String, +b: String) -> Dec:
3897 Bool.pick(Dec, Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), ce.of(Zlib.gunzip(b)),
3898 Bool.pick(Dec, String.eq(c, "deflate"), ce.deflate(b, Zlib.unzlib(b)),
3899 Bool.pick(Dec, String.eq(c, "identity"), DecOk{b}, DecSkip{})))
3900
3901def ce.go(cs: List<&2, String>, d: Dec) -> Dec:
3902 match cs:
3903 case Nil{}:
3904 d
3905 case Con{+c, t}:
3906 match d:
3907 case DecOk{+b}:
3908 ce.go(t, ce.apply(c, b))
3909 case DecBad{}:
3910 DecBad{}
3911 case DecSkip{}:
3912 DecSkip{}
3913
3914def decoded.pick(d: Dec, +status: U32, headers: Map<&2, List<&2, String>>, body: String) -> Result<&1, &1, Err, Res>:
3915 match d:
3916 case DecOk{b}:
3917 Done{Res{status, headers, Bytes.from_string(b)}}
3918 case DecBad{}:
3919 Fail{ErrBad{}}
3920 case DecSkip{}:
3921 Done{Res{status, headers, Bytes.from_string(body)}}
3922
3923# ponytail: the codings run on a String copy of the body; give zlib a Bytes input if gzip bodies get big.
3924def decoded.cs(+status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, cs: List<&2, String>) -> Result<&1, &1, Err, Res>:
3925 match cs:
3926 case Nil{}:
3927 Done{Res{status, headers, body}}
3928 case Con{c, t}:
3929 +s = Bytes.to_string(body)
3930 decoded.pick(ce.go(Con{c, t}, DecOk{s}), status, headers, s)
3931
3932def decoded.go(empty: Bool, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Result<&1, &1, Err, Res>:
3933 match empty:
3934 case True{}:
3935 Done{Res{status, headers, body}}
3936 case False{}:
3937 decoded.cs(status, headers, body, List.reverse(&2, String, ce.split(fields(headers, "content-encoding"))))
3938
3939# The body decoded per Content-Encoding; the headers stay as sent. A corrupt body is ErrBad.
3940def decoded(res: Res) -> Result<&1, &1, Err, Res>:
3941 Res{+status, +headers, body} = res
3942 Bytes.Bytes{+len, buf} = body
3943 decoded.go(U32.is_zero(len), status, headers, Bytes.Bytes{len, buf})
3944
3945def decoded.m(r: Result<&1, &1, Err, Res>) -> Maybe<&1, Res>:
3946 match r:
3947 case Done{x}:
3948 Some{x}
3949 case Fail{e}:
3950 None{}
3951
3952def decoded.some(res: Res) -> Maybe<&1, Res>:
3953 decoded.m(decoded(res))
3954
3955def ce.words(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Maybe<&1, Bytes.Bytes>:
3956 match r:
3957 case Fail{e}:
3958 None{}
3959 case Done{(+len, buf)}:
3960 Some{Bytes.Bytes{len, buf}}
3961
3962# A decoded body stops at 16 MiB, like a received one.
3963def ce.eff(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3964 Bytes.Bytes{+len, buf} = b
3965 do IO<Maybe<&1, Bytes.Bytes>>:
3966 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(16777216, len, buf)
3967 return ce.words(r)
3968
3969def ce.dec(d: Dec) -> Maybe<&1, Bytes.Bytes>:
3970 match d:
3971 case DecOk{b}:
3972 Some{Bytes.from_string(b)}
3973 case DecBad{}:
3974 None{}
3975 case DecSkip{}:
3976 None{}
3977
3978# ponytail: deflate runs on the pure decoder, which also takes raw DEFLATE; servers rarely send it.
3979def ce.io.deflate(on: Bool, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3980 match on:
3981 case True{}:
3982 +s = Bytes.to_string(b)
3983 IO.pure(Maybe<&1, Bytes.Bytes>, ce.dec(ce.deflate(s, Zlib.unzlib(s))))
3984 case False{}:
3985 IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
3986
3987def ce.io.zstd(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3988 match on:
3989 case True{}:
3990 ce.eff(~Zlib.zstd.words, b)
3991 case False{}:
3992 ce.io.deflate(String.eq(c, "deflate"), b)
3993
3994def ce.io.br(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3995 match on:
3996 case True{}:
3997 ce.eff(~Zlib.brotli.words, b)
3998 case False{}:
3999 ce.io.zstd(String.eq(c, "zstd"), c, b)
4000
4001# One known coding undone: gzip, x-gzip, br, zstd, deflate, or identity.
4002def ce.io.gz(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
4003 match on:
4004 case True{}:
4005 ce.eff(~Zlib.inflate.words, b)
4006 case False{}:
4007 ce.io.br(String.eq(c, "br"), c, b)
4008
4009def ce.io.go(cs: List<&2, String>, m: Maybe<&1, Bytes.Bytes>) -> IO(Maybe<&1, Bytes.Bytes>):
4010 match cs:
4011 case Nil{}:
4012 match m:
4013 case None{}:
4014 IO.pure(Maybe<&1, Bytes.Bytes>, None{})
4015 case Some{b}:
4016 IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
4017 case Con{+c, t}:
4018 match m:
4019 case None{}:
4020 IO.pure(Maybe<&1, Bytes.Bytes>, None{})
4021 case Some{b}:
4022 do IO<Maybe<&1, Bytes.Bytes>>:
4023 n : Maybe<&1, Bytes.Bytes> <- ce.io.gz(Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), c, b)
4024 ce.io.go(t, n)
4025
4026def ce.has(xs: List<&2, String>, +c: String) -> Bool:
4027 match xs:
4028 case Nil{}:
4029 False{}
4030 case Con{x, t}:
4031 Bool.or(String.eq(c, x), ce.has(t, c))
4032
4033def ce.known(cs: List<&2, String>, +ok: List<&2, String>) -> Bool:
4034 match cs:
4035 case Nil{}:
4036 True{}
4037 case Con{c, t}:
4038 Bool.and(ce.has(ok, c), ce.known(t, ok))
4039
4040def decoded.io.pick(m: Maybe<&1, Bytes.Bytes>, +status: U32, headers: Map<&2, List<&2, String>>) -> Result<&1, &1, Err, Res>:
4041 match m:
4042 case Some{b}:
4043 Done{Res{status, headers, b}}
4044 case None{}:
4045 Fail{ErrBad{}}
4046
4047def 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>):
4048 match known:
4049 case True{}:
4050 do IO<Result<&1, &1, Err, Res>>:
4051 m : Maybe<&1, Bytes.Bytes> <- ce.io.go(cs, Some{body})
4052 return decoded.io.pick(m, status, headers)
4053 case False{}:
4054 IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
4055
4056def decoded.io.go(empty: Bool, +enc: String, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
4057 match empty:
4058 case True{}:
4059 IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
4060 case False{}:
4061 +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
4062 decoded.io.run(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}), status, headers, body, cs)
4063
4064# decoded through the C libraries, for the codings in enc. A body with any other coding stays as sent.
4065def decoded.io(+enc: String, res: Res) -> IO(Result<&1, &1, Err, Res>):
4066 Res{+status, +headers, body} = res
4067 Bytes.Bytes{+len, buf} = body
4068 decoded.io.go(U32.is_zero(len), enc, status, headers, Bytes.Bytes{len, buf})
4069
4070# An effect on empty input fails with ENOENT only when its library does not load.
4071def codings.ok(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Bool:
4072 match r:
4073 case Fail{(+c, why)}:
4074 Bool.not(U32.is_eq(c, 2))
4075 case Done{p}:
4076 True{}
4077
4078def codings.has(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Bool):
4079 Bytes.Bytes{+len, buf} = b
4080 do IO<Bool>:
4081 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(0, len, buf)
4082 return codings.ok(r)
4083
4084def codings.add(has: Bool, +enc: String, +c: String) -> String:
4085 Bool.pick(String, has, enc ++ ", " ++ c, enc)
4086
4087# gzip and deflate, then br and zstd when their C library loads.
4088def codings() -> IO(String):
4089 do IO<String>:
4090 b : Bool <- codings.has(~Zlib.brotli.words, Bytes.new(0))
4091 z : Bool <- codings.has(~Zlib.zstd.words, Bytes.new(0))
4092 return codings.add(z, codings.add(b, "gzip, deflate", "br"), "zstd")
4093
4094# The final response of a fetch, after redirects.
4095def fetch.final(+enc: String, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
4096 match r:
4097 case Done{res}:
4098 decoded.io(enc, res)
4099 case Fail{e}:
4100 IO.pure(Result<&1, &1, Err, Res>, Fail{e})
4101
4102def pool.final(+enc: String, pr: Pool & Result<&1, &1, Err, Res> & Maybe<&2, Jar>) -> IO(Pool & Result<&1, &1, Err, Res>):
4103 (p, r, jar) = pr
4104 do IO<Pool & Result<&1, &1, Err, Res>>:
4105 d : Result<&1, &1, Err, Res> <- fetch.final(enc, r)
4106 return (p, d)
4107
4108def 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>):
4109 do IO<Pool & Result<&1, &1, Err, Res>>:
4110 pr : Pool & Result<&1, &1, Err, Res> & Maybe<&2, Jar> <- pool.hops(mode, ms, Hops{p, fetch.start(method, headers, body, Url.absolute(url), enc), cert, None{}})
4111 pool.final(enc, pr)
4112
4113def 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>):
4114 do IO<Pool & Result<&1, &1, Err, Res>>:
4115 enc : String <- codings()
4116 pool.how.enc(enc, p, method, url, headers, body, ms, mode, cert)
4117
4118# pool.how(p, "GET", "https://example.com/x?y=1", headers, body, ms, mode) follows redirects
4119# on p's idle sockets. Fail is a bad URL, a failed lookup, connect, handshake, send, read,
4120# a malformed response, more than 20 redirects, or a step past ms. Bodies are bytes.
4121def 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>):
4122 pool.how.cert(p, method, url, headers, body, ms, mode, None{})
4123
4124def 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>):
4125 pool.how(p, method, url, headers, body, ms, ModeFollow{})
4126
4127def pool.fetch(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
4128 pool.fetch.with(p, method, url, headers, body, 30000)
4129
4130def 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>):
4131 pool.how.cert(p, method, url, headers, body, ms, ModeFollow{}, Some{Cert{chain, key}})
4132
4133def 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>):
4134 pool.fetch.cert.with(p, method, url, headers, body, chain, key, 30000)
4135
4136# One request for fetch.all: the arguments of fetch, as a record.
4137type Fetch is Type:
4138 Fetch{method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
4139
4140def fetch.all.job(p: Pool, f: Fetch) -> IO(Pool & Result<&1, &1, Err, Res>):
4141 Fetch{method, url, headers, body} = f
4142 pool.fetch(p, method, url, headers, body)
4143
4144def fetch.all.pools(n: Nat) -> List<Pool>:
4145 match n:
4146 case 0n:
4147 Nil{}
4148 case 1n+p:
4149 pool.new() <> fetch.all.pools(p)
4150
4151def fetch.all.close(ps: List<Pool>) -> IO(Unit):
4152 match ps:
4153 case Nil{}:
4154 IO.pure(Unit, Unit{})
4155 case p <> rest:
4156 do IO<Unit>:
4157 pool.close(p)
4158 fetch.all.close(rest)
4159
4160def fetch.all.done(r: List<Pool> & List<Result<&1, &1, Err, Res>>) -> IO(List<Result<&1, &1, Err, Res>>):
4161 (ps, rs) = r
4162 do IO<List<Result<&1, &1, Err, Res>>>:
4163 fetch.all.close(ps)
4164 return rs
4165
4166# No requests start no workers, since Conc.pool needs at least one.
4167def fetch.all.go(xs: List<Fetch>, +workers: Nat) -> IO(List<Result<&1, &1, Err, Res>>):
4168 match xs:
4169 case Nil{}:
4170 IO.pure(List<Result<&1, &1, Err, Res>>, Nil{})
4171 case x <> rest:
4172 do IO<List<Result<&1, &1, Err, Res>>>:
4173 r : List<Pool> & List<Result<&1, &1, Err, Res>> <-
4174 Conc.pool(~Pool, ~Fetch, ~Result<&1, &1, Err, Res>, ~fetch.all.job, fetch.all.pools(workers), x <> rest)
4175 fetch.all.done(r)
4176
4177def fetch.all.of(+n: U32, nx: Nat & List<Fetch>) -> IO(List<Result<&1, &1, Err, Res>>):
4178 (+len, xs) = nx
4179 fetch.all.go(xs, Nat.min(len, Nat.max(1n, U32.to_nat(n))))
4180
4181# Each request as fetch would make it, on at most n workers (0 counts as 1, and
4182# never more workers than requests). Each worker owns its own Pool, so an idle
4183# socket is reused only by the worker that opened it; every pool is closed at the
4184# end. Results come back in the order of reqs.
4185def fetch.all(reqs: List<Fetch>, +n: U32) -> IO(List<Result<&1, &1, Err, Res>>):
4186 fetch.all.of(n, Conc.count(Fetch, reqs))
4187
4188# The hops always hand the jar back; j is only the type's fallback.
4189def pool.jar.final(+enc: String, j: Jar, pr: Pool & Result<&1, &1, Err, Res> & Maybe<&2, Jar>) -> IO(Pool & Jar & Result<&1, &1, Err, Res>):
4190 (p, r, jar) = pr
4191 do IO<Pool & Jar & Result<&1, &1, Err, Res>>:
4192 d : Result<&1, &1, Err, Res> <- fetch.final(enc, r)
4193 return (p, Maybe.default(&2, Jar, jar, j), d)
4194
4195def pool.jar.enc(+enc: String, p: Pool, +j: Jar, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Pool & Jar & Result<&1, &1, Err, Res>):
4196 do IO<Pool & Jar & Result<&1, &1, Err, Res>>:
4197 pr : Pool & Result<&1, &1, Err, Res> & Maybe<&2, Jar> <- pool.hops(ModeFollow{}, 30000, Hops{p, fetch.start(method, headers, body, Url.absolute(url), enc), None{}, Some{j}})
4198 pool.jar.final(enc, j, pr)
4199
4200# pool.fetch with a cookie jar (RFC 6265bis). Before every hop, redirects included, the jar's
4201# cookies for that URL join the request's cookie field; after every response, redirects included,
4202# its Set-Cookie fields go into the jar. The jar's clock is the caller's: advance it with jar.at.
4203def pool.fetch.jar(p: Pool, j: Jar, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Pool & Jar & Result<&1, &1, Err, Res>):
4204 do IO<Pool & Jar & Result<&1, &1, Err, Res>>:
4205 enc : String <- codings()
4206 pool.jar.enc(enc, p, j, method, url, headers, body)
4207def fetch.end(pr: Pool & Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
4208 (p, r) = pr
4209 do IO<Result<&1, &1, Err, Res>>:
4210 pool.close(p)
4211 return r
4212
4213# fetch is pool.how on a fresh pool that closes afterwards.
4214def 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>):
4215 do IO<Result<&1, &1, Err, Res>>:
4216 pr : Pool & Result<&1, &1, Err, Res> <- pool.how(pool.new(), method, url, headers, body, ms, mode)
4217 fetch.end(pr)
4218
4219def fetch.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32) -> IO(Result<&1, &1, Err, Res>):
4220 fetch.how(method, url, headers, body, ms, ModeFollow{})
4221
4222def 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>):
4223 do IO<Result<&1, &1, Err, Res>>:
4224 pr : Pool & Result<&1, &1, Err, Res> <- pool.fetch.cert.with(pool.new(), method, url, headers, body, chain, key, ms)
4225 fetch.end(pr)
4226
4227def 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>):
4228 fetch.cert.with(method, url, headers, body, chain, key, 30000)
4229
4230# fetch.with and a 30 s step timeout.
4231def fetch(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
4232 fetch.with(method, url, headers, body, 30000)
4233
4234def get(url: String) -> IO(Result<&1, &1, Err, Res>):
4235 fetch("GET", url, empty(), Bytes.new(0))
4236
4237# POST v as compact JSON, with content-type: application/json.
4238def post.json(url: String, v: Json.Val) -> IO(Result<&1, &1, Err, Res>):
4239 fetch("POST", url, set(empty(), "content-type", "application/json"), Json.encode.bytes(v))
4240
4241# Base URLs: resolve(base, ref) is ref against the absolute http(s) URL base (RFC 3986 §5.2),
4242# written back as a URL for fetch. None when base is not absolute or ref has another scheme.
4243def resolve.show(a: Url.Abs) -> String:
4244 Url.Abs{+scheme, host, port, +target} = a
4245 scheme ++ "://" ++ Url.host_field(Url.Abs{scheme, host, port, target}) ++ target
4246
4247def resolve.to(m: Maybe<&2, Url.Abs>) -> Maybe<&2, String>:
4248 match m:
4249 case None{}:
4250 None{}
4251 case Some{a}:
4252 Some{resolve.show(a)}
4253
4254def resolve.base(m: Maybe<&2, Url.Abs>, +ref: String) -> Maybe<&2, String>:
4255 match m:
4256 case None{}:
4257 None{}
4258 case Some{b}:
4259 resolve.to(Url.resolve(b, ref))
4260
4261def resolve(base: String, +ref: String) -> Maybe<&2, String>:
4262 resolve.base(Url.absolute(base), ref)
4263
4264# Retry. The wait before retry n (0 first) is 500 ms doubled n times, at most 30 s;
4265# its upper half is jitter r: backoff(n, r) = half + r mod (half + 1).
4266def retry.cap() -> U32:
4267 30000
4268
4269def retry.base(n: Nat) -> U32:
4270 match n:
4271 case 0n:
4272 500
4273 case 1n+p:
4274 U32.min((retry.base(p) * 2 : U32), retry.cap())
4275
4276def retry.backoff.half(+half: U32, +r: U32) -> U32:
4277 (half + (r % (half + 1)) : U32)
4278
4279def retry.backoff(n: Nat, +r: U32) -> U32:
4280 retry.backoff.half((retry.base(n) / 2 : U32), r)
4281
4282# ms clamped to 0 .. retry.cap().
4283def retry.after.ms(+ms: Int.I64) -> U32:
4284 Bool.pick(U32, Int.I64.is_neg(ms), 0,
4285 Bool.pick(U32, Int.I64.is_lt(ms, Int.I64.from_u32(retry.cap())), Int.I64.to_u32(ms), retry.cap()))
4286
4287def retry.after.date(m: Maybe<&2, Time.Instant>, now: Time.Instant) -> Maybe<&2, U32>:
4288 match m:
4289 case None{}:
4290 None{}
4291 case Some{date}:
4292 Some{retry.after.ms(Time.Duration.to_ms(Time.Instant.since(date, now)))}
4293
4294# More than 5 digits is past the cap, and would overflow parse_u32.
4295def retry.after.secs(+v: String, now: Time.Instant, n: Maybe<&2, U32>) -> Maybe<&2, U32>:
4296 match n:
4297 case None{}:
4298 retry.after.date(Time.http_date.parse(v), now)
4299 case Some{s}:
4300 Some{Bool.pick(U32, Nat.is_lt(5n, String.length(v)), retry.cap(), U32.min((s * 1000 : U32), retry.cap()))}
4301
4302# Retry-After (RFC 9110 §10.2.3) as ms from now, at most retry.cap(): delay-seconds, or an
4303# HTTP-date (a past date is 0). None when v is empty or neither form.
4304def retry.after(+v: String, now: Time.Instant) -> Maybe<&2, U32>:
4305 retry.after.secs(v, now, parse_u32(v))
4306
4307def retry.wait(m: Maybe<&2, U32>, n: Nat, +r: U32) -> U32:
4308 match m:
4309 case None{}:
4310 retry.backoff(n, r)
4311 case Some{ms}:
4312 ms
4313
4314# The wait before retry n: Retry-After v when it reads as a delay, else backoff with jitter r.
4315def retry.delay(+v: String, now: Time.Instant, n: Nat, +r: U32) -> U32:
4316 retry.wait(retry.after(v, now), n, r)
4317
4318# Statuses a later try may clear.
4319def retry.status(+s: U32) -> Bool:
4320 Bool.or(Bool.or(U32.is_eq(s, 408), U32.is_eq(s, 429)),
4321 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))))
4322
4323# A refused connect or a timeout may clear; any other error would repeat.
4324def retry.fail(e: Err) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
4325 match e:
4326 case ErrConnect{code, why}:
4327 (Fail{ErrConnect{code, why}}, Some{""})
4328 case ErrTimeout{}:
4329 (Fail{ErrTimeout{}}, Some{""})
4330 case other:
4331 (Fail{other}, None{})
4332
4333def retry.res(res: Res) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
4334 Res{+status, +headers, body} = res
4335 (Done{Res{status, headers, body}}, Bool.pick(Maybe<&2, String>, retry.status(status), Some{header(headers, "retry-after")}, None{}))
4336
4337def retry.judge.try(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
4338 match r:
4339 case Fail{e}:
4340 retry.fail(e)
4341 case Done{res}:
4342 retry.res(res)
4343
4344# One try, judged: the result as it came, and Some{Retry-After value} ("" when absent)
4345# when an idempotent request may try again.
4346def retry.judge(idem: Bool, r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
4347 match idem:
4348 case False{}:
4349 (r, None{})
4350 case True{}:
4351 retry.judge.try(r)
4352
4353# ponytail: a failed random source gives jitter 0, so the wait is the lower half.
4354def retry.jitter(r: Result<&1, &1, U32 & String, U32>) -> U32:
4355 match r:
4356 case Fail{e}:
4357 0
4358 case Done{x}:
4359 x
4360
4361def retry.sleep(+v: String, n: Nat) -> IO(Unit):
4362 do IO<Unit>:
4363 now : Time.Instant <- Time.now()
4364 rnd : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
4365 IO.sleep(retry.delay(v, now, n, retry.jitter(rnd)))
4366
4367def retry.kept(body: Bytes.Bytes, j: Result<&1, &1, Err, Res> & Maybe<&2, String>) -> Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>:
4368 (r, m) = j
4369 (body, r, m)
4370
4371# One fetch of the copy; the body comes back for the next try.
4372def retry.one(+idem: Bool, +method: String, +url: String, +headers: Map<&2, List<&2, String>>,
4373 r: Bytes.Bytes & Bytes.Bytes) -> IO(Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>):
4374 (body, spare) = r
4375 do IO<Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>>:
4376 got : Result<&1, &1, Err, Res> <- fetch(method, url, headers, spare)
4377 return retry.kept(body, retry.judge(idem, got))
4378
4379# left: retries still allowed. n: the retry to wait for next, 0 first.
4380def retry.go(left: Nat, +n: Nat, +idem: Bool, +method: String, +url: String,
4381 +headers: Map<&2, List<&2, String>>,
4382 t: Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>) -> IO(Result<&1, &1, Err, Res>):
4383 match left:
4384 case 0n:
4385 (body, r, m) = t
4386 IO.pure(Result<&1, &1, Err, Res>, r)
4387 case 1n+p:
4388 (body, r, m) = t
4389 match m:
4390 case None{}:
4391 IO.pure(Result<&1, &1, Err, Res>, r)
4392 case Some{v}:
4393 do IO<Result<&1, &1, Err, Res>>:
4394 retry.sleep(v, n)
4395 tried : Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String> <-
4396 retry.one(idem, method, url, headers, Bytes.slice(body, 0, 4294967295))
4397 retry.go(p, 1n+n, idem, method, url, headers, tried)
4398
4399# fetch.retry(n, method, url, headers, body) is fetch, tried again up to n times while an
4400# idempotent method (GET, HEAD, OPTIONS, TRACE, PUT, DELETE) gets a connect error, a timeout,
4401# or 408, 429, 500, 502, 503, or 504. POST, PATCH and other methods get one try. It waits
4402# Retry-After (seconds or HTTP-date, at most 30 s) when given, else the backoff. When retries
4403# run out, the last response or error comes back as it was.
4404def retry.start(enabled: Bool, n: U32, +method: String, +url: String,
4405 +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) ->
4406 IO(Result<&1, &1, Err, Res>):
4407 match enabled:
4408 case False{}:
4409 fetch(method, url, headers, body)
4410 case True{}:
4411 do IO<Result<&1, &1, Err, Res>>:
4412 first : Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String> <-
4413 retry.one(True{}, method, url, headers, Bytes.slice(body, 0, 4294967295))
4414 retry.go(U32.to_nat(n), 0n, True{}, method, url, headers, first)
4415
4416def fetch.retry(+n: U32, +method: String, +url: String,
4417 +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) ->
4418 IO(Result<&1, &1, Err, Res>):
4419 retry.start(Bool.and(U32.is_ne(n, 0), pool.idempotent(method)),
4420 n, method, url, headers, body)
4421
4422# Streaming (a body read or sent in pieces). A decoded stream owns its decoders.
4423# What the next read returns: read more, a raw piece, a decoded piece, the end, or an error.
4424type Po is Type:
4425 PoNone{}
4426 PoPiece{b: Bytes.Bytes}
4427 PoReady{b: Bytes.Bytes}
4428 PoEnd{}
4429 PoBad{e: Err}
4430
4431type Stream is Type:
4432 Stream{tls: Bool, s: Socket, ms: U32, res: Res, rb: Rb, out: Po, decs: List<&1, Zlib.Decoder>}
4433
4434type Pc is Type:
4435 Pc{rb: Rb, out: Po}
4436
4437# A body piece, or none when empty: more reads the next piece, and not more is the end.
4438def pc.po(more: Bool, empty: Bool, b: Bytes.Bytes) -> Po:
4439 match empty:
4440 case True{}:
4441 Bool.pick(Po, more, PoNone{}, PoEnd{})
4442 case False{}:
4443 PoPiece{b}
4444
4445def pc.piece(more: Bool, +rb: Rb, b: Bytes.Bytes) -> Pc:
4446 Bytes.Bytes{+len, buf} = b
4447 Pc{rb, pc.po(more, U32.is_zero(len), Bytes.Bytes{len, buf})}
4448
4449def pc.fed.of(b: Bytes.Bytes, st: Rb) -> Pc:
4450 match st:
4451 case RbDone{}:
4452 pc.piece(False{}, RbDone{}, b)
4453 case RbBad{}:
4454 Pc{RbDone{}, PoBad{ErrBad{}}}
4455 case RbLen{n}:
4456 pc.piece(True{}, RbLen{n}, b)
4457 case RbChunk{st}:
4458 pc.piece(True{}, RbChunk{st}, b)
4459 case RbClose{}:
4460 pc.piece(True{}, RbClose{}, b)
4461
4462def pc.fed(bf: Bf) -> Pc:
4463 Bf{st, parts, rest} = bf
4464 pc.fed.of(rb.body(parts), st)
4465
4466# The body bytes that just arrived: what they add to the body, and how it ends.
4467def pc.of(rb: Rb, piece: Bytes.Bytes) -> Pc:
4468 pc.fed(rb.feed(rb, Nil{}, piece))
4469
4470# The server closed. Only a close-delimited body may end this way (RFC 9112 §8).
4471def pc.end(ok: Bool) -> Pc:
4472 match ok:
4473 case True{}:
4474 Pc{RbDone{}, PoEnd{}}
4475 case False{}:
4476 Pc{RbDone{}, PoBad{ErrBad{}}}
4477
4478def pc.eof(st: Rb) -> Pc:
4479 pc.end(rb.eof(st))
4480
4481def stream.mk(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, pc: Pc) -> Stream:
4482 Pc{rb, out} = pc
4483 Stream{tls, s, ms, res, rb, out, decs}
4484
4485def stream.got.piece(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, +rb: Rb, p: U32 & Array<U32>) -> Stream:
4486 (+len, buf) = p
4487 stream.mk(tls, s, ms, res, decs, Bool.pick(Pc, U32.is_zero(len), pc.eof(rb), pc.of(rb, Bytes.Bytes{len, buf})))
4488
4489def 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:
4490 (s, r) = m
4491 match r:
4492 case Fail{(+code, why)}:
4493 Stream{tls, s, ms, res, RbDone{}, PoBad{err.or_late(code, ErrRead{code, why})}, decs}
4494 case Done{p}:
4495 stream.got.piece(tls, s, ms, res, decs, rb, p)
4496
4497def stream.after(+rb: Rb) -> Po:
4498 match rb:
4499 case RbDone{}:
4500 PoEnd{}
4501 case RbBad{}:
4502 PoEnd{}
4503 case RbLen{n}:
4504 PoNone{}
4505 case RbChunk{st}:
4506 PoNone{}
4507 case RbClose{}:
4508 PoNone{}
4509
4510type Fed is Type:
4511 Fed{decs: List<&1, Zlib.Decoder>, body: Result<&1, &1, Err, Bytes.Bytes>}
4512
4513def stream.feed.received(done: List<&1, Zlib.Decoder>, m: Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Fed:
4514 (d, r) = m
4515 match r:
4516 case Fail{e}:
4517 Fed{d <> done, Fail{ErrBad{}}}
4518 case Done{(+len, buf)}:
4519 Fed{d <> done, Done{Bytes.Bytes{len, buf}}}
4520
4521def stream.feed.step(st: Fed, d: Zlib.Decoder) -> IO(Fed):
4522 Fed{done, body} = st
4523 match body:
4524 case Fail{e}:
4525 IO.pure(Fed, Fed{d <> done, Fail{e}})
4526 case Done{b}:
4527 Bytes.Bytes{+len, buf} = b
4528 do IO<Fed>:
4529 m : Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
4530 Zlib.dec.feed.words(d, 16777216, len, buf)
4531 return stream.feed.received(done, m)
4532
4533def stream.feed.one(prev: IO(Fed), d: Zlib.Decoder) -> IO(Fed):
4534 do IO<Fed>:
4535 st : Fed <- prev
4536 stream.feed.step(st, d)
4537
4538def stream.feed.reverse(st: Fed) -> Fed:
4539 Fed{done, body} = st
4540 Fed{List.reverse(&1, Zlib.Decoder, done), body}
4541
4542def stream.feed.all(decs: List<&1, Zlib.Decoder>, b: Bytes.Bytes) -> IO(Fed):
4543 do IO<Fed>:
4544 st : Fed <- List.foldl(~&1, ~Zlib.Decoder, ~IO(Fed), ~stream.feed.one, decs,
4545 IO.pure(Fed, Fed{Nil{}, Done{b}}))
4546 return stream.feed.reverse(st)
4547
4548def stream.ready(empty: Bool, +rb: Rb, b: Bytes.Bytes) -> Po:
4549 match empty:
4550 case True{}:
4551 stream.after(rb)
4552 case False{}:
4553 PoReady{b}
4554
4555def stream.feed.got(+tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb, st: Fed) -> Stream:
4556 Fed{decs, body} = st
4557 match body:
4558 case Fail{e}:
4559 Stream{tls, s, ms, res, rb, PoBad{e}, decs}
4560 case Done{b}:
4561 Bytes.Bytes{+len, buf} = b
4562 Stream{tls, s, ms, res, rb, stream.ready(U32.is_zero(len), rb, Bytes.Bytes{len, buf}), decs}
4563
4564def stream.feed.st(st: Stream, b: Bytes.Bytes) -> IO(Stream):
4565 Stream{+tls, s, +ms, res, +rb, out, decs} = st
4566 match decs:
4567 case Nil{}:
4568 IO.pure(Stream, Stream{tls, s, ms, res, rb, PoReady{b}, Nil{}})
4569 case Con{d, rest}:
4570 do IO<Stream>:
4571 fed : Fed <- stream.feed.all(Con{d, rest}, b)
4572 return stream.feed.got(tls, s, ms, res, rb, fed)
4573
4574def stream.finish.ok(r: Result<&1, &1, U32 & String, Unit>) -> Bool:
4575 match r:
4576 case Fail{e}:
4577 False{}
4578 case Done{u}:
4579 True{}
4580
4581def stream.finish(decs: List<&1, Zlib.Decoder>) -> IO(Bool):
4582 match decs:
4583 case Nil{}:
4584 IO.pure(Bool, True{})
4585 case Con{d, rest}:
4586 do IO<Bool>:
4587 r : Result<&1, &1, U32 & String, Unit> <- Zlib.dec.finish(d)
4588 tail : Bool <- stream.finish(rest)
4589 return Bool.and(stream.finish.ok(r), tail)
4590
4591def stream.ended(good: Bool, +tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb) ->
4592 Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>:
4593 match good:
4594 case True{}:
4595 (Stream{tls, s, ms, res, rb, PoEnd{}, Nil{}}, Done{None{}})
4596 case False{}:
4597 (Stream{tls, s, ms, res, rb, PoBad{ErrBad{}}, Nil{}}, Fail{ErrBad{}})
4598
4599# The next piece of the body; None at the end. A piece is never empty.
4600@unsafe
4601def stream.read(st: Stream) -> IO(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>):
4602 Stream{+tls, s, +ms, res, +rb, out, decs} = st
4603 match out:
4604 case PoPiece{b}:
4605 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
4606 next : Stream <- stream.feed.st(Stream{tls, s, ms, res, rb, PoNone{}, decs}, b)
4607 stream.read(next)
4608 case PoReady{b}:
4609 IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
4610 (Stream{tls, s, ms, res, rb, stream.after(rb), decs}, Done{Some{b}}))
4611 case PoEnd{}:
4612 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
4613 good : Bool <- stream.finish(decs)
4614 return stream.ended(good, tls, s, ms, res, rb)
4615 case PoBad{+e}:
4616 IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
4617 (Stream{tls, s, ms, res, rb, PoBad{e}, decs}, Fail{e}))
4618 case PoNone{}:
4619 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
4620 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
4621 stream.read(stream.got(tls, ms, res, decs, rb, m))
4622
4623# Status and headers. Its body is empty: read the body with stream.read.
4624def stream.res(st: Stream) -> Stream & Res:
4625 Stream{tls, s, ms, res, rb, out, decs} = st
4626 Res{+status, +headers, body} = res
4627 (Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, Res{status, headers, Bytes.new(0)})
4628
4629def stream.close(st: Stream) -> IO(Unit):
4630 Stream{tls, s, ms, res, rb, out, decs} = st
4631 do IO<Unit>:
4632 good : Bool <- stream.finish(decs)
4633 io.close(tls, s)
4634
4635# Head read state: still scanning, cut short or bad, or the head with the bytes after it.
4636type Sh is Type:
4637 ShMore{buf: Bytes.Bytes, k: U32}
4638 ShBad{err: Maybe<&2, Err>}
4639 ShRes{res: Res, rb: Rb, rest: Bytes.Bytes}
4640
4641def sh.of(hs: Hs) -> Sh:
4642 match hs:
4643 case HsWait{buf, k}:
4644 ShMore{buf, k}
4645 case HsBad{}:
4646 ShBad{None{}}
4647 case HsSeek{buf, from, k}:
4648 ShBad{None{}}
4649 case HsRes{res, rb, rest}:
4650 ShRes{res, rb, rest}
4651
4652def sh.piece(+head: Bool, buf: Bytes.Bytes, +k: U32, p: U32 & Array<U32>) -> Sh:
4653 (+len, b) = p
4654 Bool.pick(Sh, U32.is_zero(len), ShBad{None{}}, sh.of(hs.more(head, k, buf, Bytes.Bytes{len, b})))
4655
4656def sh.next(+head: Bool, buf: Bytes.Bytes, +k: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Sh:
4657 (s, r) = m
4658 match r:
4659 case Fail{(+code, why)}:
4660 (s, ShBad{Some{err.or_late(code, ErrRead{code, why})}})
4661 case Done{p}:
4662 (s, sh.piece(head, buf, k, p))
4663
4664def fetch.fail.of(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Stream>:
4665 match r:
4666 case Fail{e}:
4667 Fail{e}
4668 case Done{res}:
4669 Fail{ErrBad{}}
4670
4671# Reads until the final head is in; the body bytes that came with it are the first piece.
4672@unsafe
4673def stream.head(+tls: Bool, +ms: U32, +head: Bool, st: Socket & Sh) -> IO(Result<&1, &1, Err, Stream>):
4674 (s, sh) = st
4675 match sh:
4676 case ShMore{buf, +k}:
4677 do IO<Result<&1, &1, Err, Stream>>:
4678 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
4679 stream.head(tls, ms, head, sh.next(head, buf, k, m))
4680 case ShBad{err}:
4681 do IO<Result<&1, &1, Err, Stream>>:
4682 r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, err)
4683 return fetch.fail.of(r)
4684 case ShRes{res, rb, rest}:
4685 IO.pure(Result<&1, &1, Err, Stream>, Done{stream.mk(tls, s, ms, res, Nil{}, pc.of(rb, rest))})
4686
4687def stream.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Stream>):
4688 (s, r) = m
4689 match r:
4690 case Fail{(+code, why)}:
4691 do IO<Result<&1, &1, Err, Stream>>:
4692 io.close(tls, s)
4693 return Fail{err.or_late(code, ErrWrite{code, why})}
4694 case Done{u}:
4695 stream.head(tls, ms, head, (s, ShMore{Bytes.new(0), 0}))
4696
4697def stream.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
4698 match r:
4699 case Fail{e}:
4700 IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
4701 case Done{c}:
4702 match c:
4703 case Conn{+tls, s}:
4704 do IO<Result<&1, &1, Err, Stream>>:
4705 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
4706 stream.sent(tls, ms, head, sent)
4707 case ConnH2{s, client}:
4708 do IO<Result<&1, &1, Err, Stream>>:
4709 Wire.tls.close(s)
4710 return Fail{ErrBad{}}
4711
4712# One connection per stream; the request says close.
4713def stream.origin(+ms: U32, +head: Bool, wire: Bytes.Bytes, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Stream>):
4714 Url.Abs{+scheme, +host, +port, target} = a
4715 match known:
4716 case False{}:
4717 IO.pure(Result<&1, &1, Err, Stream>, Fail{ErrUrl{}})
4718 case True{}:
4719 do IO<Result<&1, &1, Err, Stream>>:
4720 ips : List<&2, String> <- Dns.resolve.all(host)
4721 c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{}, False{})
4722 stream.conn(c, ms, head, wire)
4723
4724def 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>):
4725 Url.Abs{scheme, host, port, +target} = url
4726 (body, wire) = r
4727 do IO<Hop & Result<&1, &1, Err, Stream>>:
4728 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))
4729 return (Hop{method, url, headers, body}, got)
4730
4731# One request on its own connection. The hop comes back for the redirect.
4732def stream.one(h: Hop, +ms: U32) -> IO(Hop & Result<&1, &1, Err, Stream>):
4733 Hop{+method, +url, +headers, body} = h
4734 stream.one.of(method, url, headers, ms, Bytes.slice(body, 0, 4294967295))
4735
4736# Go: the next request. Drop: close this stream, then go on. Done: the answer.
4737type Sn is Type:
4738 SnGo{left: Nat, hop: Hop}
4739 SnDrop{st: Stream, next: Next}
4740 SnDone{r: Result<&1, &1, Err, Stream>}
4741
4742def sn.of(n: Next) -> Sn:
4743 match n:
4744 case NGo{l, h}:
4745 SnGo{l, h}
4746 case NStop{}:
4747 SnDone{Fail{ErrRedirect{}}}
4748 case NDone{m}:
4749 match m:
4750 case Fail{e}:
4751 SnDone{Fail{e}}
4752 case Done{r}:
4753 SnDone{Fail{ErrBad{}}}
4754
4755def stream.decide.n(st: Stream, n: Next) -> Sn:
4756 match n:
4757 case NDone{m}:
4758 SnDone{Done{st}}
4759 case NGo{l, h}:
4760 SnDrop{st, NGo{l, h}}
4761 case NStop{}:
4762 SnDrop{st, NStop{}}
4763
4764def stream.decide.of(+left: Nat, hop: Hop, sr: Stream & Res) -> Sn:
4765 (st, res) = sr
4766 stream.decide.n(st, fetch.decide(left, hop, Done{res}))
4767
4768def stream.decide(+left: Nat, x: Hop & Result<&1, &1, Err, Stream>) -> Sn:
4769 (hop, r) = x
4770 match r:
4771 case Fail{e}:
4772 SnDone{Fail{e}}
4773 case Done{st}:
4774 stream.decide.of(left, hop, stream.res(st))
4775
4776@unsafe
4777def stream.hops(+ms: U32, sn: Sn) -> IO(Result<&1, &1, Err, Stream>):
4778 match sn:
4779 case SnDone{r}:
4780 IO.pure(Result<&1, &1, Err, Stream>, r)
4781 case SnGo{+left, hop}:
4782 do IO<Result<&1, &1, Err, Stream>>:
4783 x : Hop & Result<&1, &1, Err, Stream> <- stream.one(hop, ms)
4784 stream.hops(ms, stream.decide(left, x))
4785 case SnDrop{st, next}:
4786 do IO<Result<&1, &1, Err, Stream>>:
4787 stream.close(st)
4788 stream.hops(ms, sn.of(next))
4789
4790type Opened is Type:
4791 Opened{decs: List<&1, Zlib.Decoder>, bad: Bool}
4792
4793def stream.open.got(st: Opened, r: Result<&1, &1, U32 & String, Zlib.Decoder>) -> Opened:
4794 Opened{decs, bad} = st
4795 match r:
4796 case Fail{e}:
4797 Opened{decs, True{}}
4798 case Done{d}:
4799 Opened{d <> decs, bad}
4800
4801def stream.open.add(st: Opened, m: IO(Result<&1, &1, U32 & String, Zlib.Decoder>)) -> IO(Opened):
4802 do IO<Opened>:
4803 r : Result<&1, &1, U32 & String, Zlib.Decoder> <- m
4804 return stream.open.got(st, r)
4805
4806def stream.open.zstd(zstd: Bool, st: Opened) -> IO(Opened):
4807 match zstd:
4808 case True{}:
4809 stream.open.add(st, Zlib.zstd.new())
4810 case False{}:
4811 IO.pure(Opened, st)
4812
4813def stream.open.br(br: Bool, +c: String, st: Opened) -> IO(Opened):
4814 match br:
4815 case True{}:
4816 stream.open.add(st, Zlib.brotli.new())
4817 case False{}:
4818 stream.open.zstd(String.eq(c, "zstd"), st)
4819
4820def stream.open.gz(gz: Bool, +c: String, st: Opened) -> IO(Opened):
4821 match gz:
4822 case True{}:
4823 stream.open.add(st, Zlib.inflate.new())
4824 case False{}:
4825 stream.open.br(String.eq(c, "br"), c, st)
4826
4827def stream.open.step(+c: String, st: Opened) -> IO(Opened):
4828 Opened{decs, bad} = st
4829 match bad:
4830 case True{}:
4831 IO.pure(Opened, Opened{decs, True{}})
4832 case False{}:
4833 stream.open.gz(Bool.or(String.eq(c, "gzip"), Bool.or(String.eq(c, "x-gzip"), String.eq(c, "deflate"))),
4834 c, Opened{decs, False{}})
4835
4836def stream.open.one(prev: IO(Opened), c: String) -> IO(Opened):
4837 do IO<Opened>:
4838 st : Opened <- prev
4839 stream.open.step(c, st)
4840
4841def stream.open.all(cs: List<&2, String>) -> IO(Opened):
4842 List.foldl(~&2, ~String, ~IO(Opened), ~stream.open.one, cs, IO.pure(Opened, Opened{Nil{}, False{}}))
4843
4844def stream.put.decs(st: Stream, decs: List<&1, Zlib.Decoder>) -> Stream:
4845 Stream{tls, s, ms, res, rb, out, old} = st
4846 Stream{tls, s, ms, res, rb, out, decs}
4847
4848def stream.init.opened(st: Stream, opened: Opened) -> IO(Result<&1, &1, Err, Stream>):
4849 Opened{decs, bad} = opened
4850 match bad:
4851 case True{}:
4852 do IO<Result<&1, &1, Err, Stream>>:
4853 stream.close(stream.put.decs(st, decs))
4854 return Fail{ErrBad{}}
4855 case False{}:
4856 IO.pure(Result<&1, &1, Err, Stream>, Done{stream.put.decs(st, List.reverse(&1, Zlib.Decoder, decs))})
4857
4858def stream.init.known(known: Bool, st: Stream, cs: List<&2, String>) -> IO(Result<&1, &1, Err, Stream>):
4859 match known:
4860 case False{}:
4861 IO.pure(Result<&1, &1, Err, Stream>, Done{st})
4862 case True{}:
4863 do IO<Result<&1, &1, Err, Stream>>:
4864 opened : Opened <- stream.open.all(cs)
4865 stream.init.opened(st, opened)
4866
4867def stream.init.st(+enc: String, st: Stream) -> IO(Result<&1, &1, Err, Stream>):
4868 Stream{tls, s, ms, res, rb, out, decs} = st
4869 Res{+status, +headers, body} = res
4870 +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
4871 stream.init.known(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}),
4872 Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, cs)
4873
4874def stream.init(+enc: String, r: Result<&1, &1, Err, Stream>) -> IO(Result<&1, &1, Err, Stream>):
4875 match r:
4876 case Fail{e}:
4877 IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
4878 case Done{st}:
4879 stream.init.st(enc, st)
4880
4881def stream.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>) -> Sn:
4882 match u:
4883 case None{}:
4884 SnDone{Fail{ErrUrl{}}}
4885 case Some{a}:
4886 SnGo{20n, Hop{method, a, req.put(Map.to_list(&2, List<&2, String>, headers), empty()), body}}
4887
4888# Open a raw stream. Its body bytes and headers remain as sent.
4889def open.raw.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
4890 stream.hops(ms, stream.start(method, headers, body, Url.absolute(url)))
4891
4892def open.raw(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
4893 open.raw.with(method, url, headers, body, 30000)
4894
4895def 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>):
4896 do IO<Result<&1, &1, Err, Stream>>:
4897 r : Result<&1, &1, Err, Stream> <-
4898 stream.hops(ms, stream.start(method, accept.enc(headers, enc), body, Url.absolute(url)))
4899 stream.init(enc, r)
4900
4901# Follow redirects, then decode each body piece by Content-Encoding. Unknown codings stay raw.
4902def open.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
4903 do IO<Result<&1, &1, Err, Stream>>:
4904 enc : String <- codings()
4905 open.with.enc(enc, method, url, headers, body, ms)
4906
4907def open(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
4908 open.with(method, url, headers, body, 30000)
4909
4910# Upload: the request body sent in chunks (RFC 9112 §7.1). err: the first failed write.
4911type Up is Type:
4912 Up{tls: Bool, s: Socket, ms: U32, head: Bool, err: Maybe<&2, Err>}
4913
4914def hex.digit(+n: U32) -> Char:
4915 Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))}
4916
4917def hex.go(k: Nat, +n: U32, acc: String) -> String:
4918 match k:
4919 case 0n:
4920 acc
4921 case 1n+p:
4922 hex.go(p, U32.shrn(n, 4n), SCon{hex.digit(U32.and(n, 15)), acc})
4923
4924def hex.trim(+s: String) -> String:
4925 match s:
4926 case SNil{}:
4927 SNil{}
4928 case SCon{Chr{+c}, +t}:
4929 Bool.pick(String, Bool.and(U32.is_eq(c, 48), Bool.not(String.is_empty(t))), hex.trim(t), SCon{Chr{c}, t})
4930
4931def hex(+n: U32) -> String:
4932 hex.trim(hex.go(8n, n, ""))
4933
4934def up.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up:
4935 (s, r) = m
4936 match r:
4937 case Fail{(+code, why)}:
4938 Up{tls, s, ms, head, Some{err.or_late(code, ErrWrite{code, why})}}
4939 case Done{u}:
4940 Up{tls, s, ms, head, None{}}
4941
4942def up.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: String) -> IO(Result<&1, &1, Err, Up>):
4943 match r:
4944 case Fail{e}:
4945 IO.pure(Result<&1, &1, Err, Up>, Fail{e})
4946 case Done{c}:
4947 match c:
4948 case Conn{+tls, s}:
4949 do IO<Result<&1, &1, Err, Up>>:
4950 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, Bytes.from_string(wire))
4951 return Done{up.sent(tls, ms, head, sent)}
4952 case ConnH2{s, client}:
4953 do IO<Result<&1, &1, Err, Up>>:
4954 Wire.tls.close(s)
4955 return Fail{ErrBad{}}
4956
4957def up.head(+method: String, +target: String, +hf: String, +headers: Map<&2, List<&2, String>>) -> String:
4958 request(method, target, set(set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", hf), "connection", "close"), "transfer-encoding", "chunked"), "")
4959
4960def up.origin(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Up>):
4961 Url.Abs{+scheme, +host, +port, +target} = a
4962 match known:
4963 case False{}:
4964 IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
4965 case True{}:
4966 do IO<Result<&1, &1, Err, Up>>:
4967 ips : List<&2, String> <- Dns.resolve.all(host)
4968 c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{}, False{})
4969 up.conn(c, ms, String.eq(method, "HEAD"), up.head(method, target, Url.host_field(a), headers))
4970
4971def up.url(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, u: Maybe<&2, Url.Abs>) -> IO(Result<&1, &1, Err, Up>):
4972 match u:
4973 case None{}:
4974 IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
4975 case Some{+a}:
4976 up.origin(method, ms, headers, a, pool.scheme.ok(a))
4977
4978# Http.upload(method, url, headers) sends the head. A streamed body cannot be replayed, so redirects are not followed.
4979def upload.with(+method: String, url: String, headers: Map<&2, List<&2, String>>, +ms: U32) -> IO(Result<&1, &1, Err, Up>):
4980 up.url(method, ms, headers, Url.absolute(url))
4981
4982def upload(+method: String, url: String, headers: Map<&2, List<&2, String>>) -> IO(Result<&1, &1, Err, Up>):
4983 upload.with(method, url, headers, 30000)
4984
4985def up.wrote(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up & Result<&2, &2, Err, Unit>:
4986 (s, r) = m
4987 match r:
4988 case Fail{(+code, why)}:
4989 +e = err.or_late(code, ErrWrite{code, why})
4990 (Up{tls, s, ms, head, Some{e}}, Fail{e})
4991 case Done{u}:
4992 (Up{tls, s, ms, head, None{}}, Done{Unit{}})
4993
4994# One write per chunk, so the size line and the data do not wait on each other (Nagle).
4995def up.put(+tls: Bool, s: Socket, +ms: U32, +head: Bool, +len: U32, piece: Bytes.Bytes, skip: Bool) -> IO(Up & Result<&2, &2, Err, Unit>):
4996 match skip:
4997 case True{}:
4998 IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, None{}}, Done{Unit{}}))
4999 case False{}:
5000 do IO<Up & Result<&2, &2, Err, Unit>>:
5001 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{}}}}))
5002 return up.wrote(tls, ms, head, sent)
5003
5004def up.chunk(+tls: Bool, s: Socket, +ms: U32, +head: Bool, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
5005 Bytes.Bytes{+len, buf} = piece
5006 up.put(tls, s, ms, head, len, Bytes.Bytes{len, buf}, U32.is_zero(len))
5007
5008# One chunk. An empty piece sends nothing, since an empty chunk would end the body.
5009def upload.write(up: Up, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
5010 Up{+tls, s, +ms, +head, err} = up
5011 match err:
5012 case Some{+e}:
5013 IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, Some{e}}, Fail{e}))
5014 case None{}:
5015 up.chunk(tls, s, ms, head, piece)
5016
5017# Ends the body and returns the response as a stream.
5018def upload.finish(up: Up) -> IO(Result<&1, &1, Err, Stream>):
5019 Up{+tls, s, +ms, +head, err} = up
5020 match err:
5021 case Some{e}:
5022 do IO<Result<&1, &1, Err, Stream>>:
5023 io.close(tls, s)
5024 return Fail{e}
5025 case None{}:
5026 do IO<Result<&1, &1, Err, Stream>>:
5027 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, Bytes.from_string("0\r\n\r\n"))
5028 stream.sent(tls, ms, head, sent)
5029
5030def reply.bytes(res: Res, head: Bool, close: Bool) -> Bytes.Bytes:
5031 Res{+status, +headers, body} = res
5032 encode.on(Res{status, Bool.pick(Map<&2, List<&2, String>>, close, set(headers, "connection", "close"), headers), body}, head)
5033
5034def reply.fail.bytes(+status: U32) -> Res:
5035 Res{status, set(empty(), "connection", "close"), Bytes.from_string(reason(status))}
5036
5037def reply.drain.of(m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Bool:
5038 (s, r) = m
5039 match r:
5040 case Fail{e}:
5041 (s, False{})
5042 case Done{data}:
5043 (len, words) = data
5044 (s, Bool.not(U32.is_zero(len)))
5045
5046# ponytail: cap drain at 32 MiB and 2.55 s; use socket half-close if larger peers need guaranteed delivery.
5047def reply.drain(n: Nat, alive: Bool, +until: Time.Duration, st: Socket & Bool) -> IO(Unit):
5048 match n:
5049 case 0n:
5050 (s, more) = st
5051 Socket.close(s)
5052 case 1n+p:
5053 match alive:
5054 case False{}:
5055 (s, more) = st
5056 Socket.close(s)
5057 case True{}:
5058 (s, more) = st
5059 match more:
5060 case False{}:
5061 Socket.close(s)
5062 case True{}:
5063 do IO<Unit>:
5064 got : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- Wire.recv.words(s, 65536, 50)
5065 now : Time.Duration <- Time.mono()
5066 reply.drain(p, Cmp.is_lt(Time.Duration.cmp(now, until)), until, reply.drain.of(got))
5067
5068def reply.sent.close(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Unit):
5069 (s, r) = m
5070 match r:
5071 case Fail{e}:
5072 Socket.close(s)
5073 case Done{u}:
5074 do IO<Unit>:
5075 now : Time.Duration <- Time.mono()
5076 reply.drain(U32.to_nat(512), True{}, Time.Duration.add(now, Time.Duration.of_ms(2500)), (s, True{}))
5077
5078def reply_fail(s: Socket, +status: U32) -> IO(Unit):
5079 do IO<Unit>:
5080 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, encode(reply.fail.bytes(status)))
5081 reply.sent.close(sent)
5082
5083
5084# The head is parsed once, when it is whole. Body pieces are kept as they come and joined once.
5085type Sv is Type:
5086 SvHead{buf: Bytes.Bytes}
5087 SvLen{req: Req, v11: Bool, left: U32, parts: List<&1, Bytes.Bytes>}
5088 SvChunk{req: Req, v11: Bool, n: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
5089
5090# More: read on, first answering 100 Continue when cont is set.
5091type Turn is Type:
5092 TurnClose{}
5093 TurnFail{status: U32}
5094 TurnReq{req: Req, rest: Bytes.Bytes, v11: Bool}
5095 TurnMore{sv: Sv, cont: Bool}
5096
5097def serve.max() -> Nat:
5098 fetch.max()
5099
5100def sv.none() -> Sv:
5101 SvHead{Bytes.new(0)}
5102
5103def sv.body(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes) -> Turn:
5104 Req{method, path, headers, body} = req
5105 TurnReq{Req{method, path, headers, rb.body(parts)}, rest, v11}
5106
5107def sv.len.cut(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
5108 (piece, last) = r
5109 sv.body(req, v11, Con{last, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32))))
5110
5111def sv.len.have(short: Bool, req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Turn:
5112 match short:
5113 case True{}:
5114 TurnMore{SvLen{req, v11, (left - len : U32), Con{piece, parts}}, False{}}
5115 case False{}:
5116 sv.len.cut(req, v11, parts, len, left, Bytes.slice(piece, 0, left))
5117
5118def sv.len(req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
5119 Bytes.Bytes{+len, buf} = piece
5120 sv.len.have(U32.is_lt(len, left), req, v11, left, parts, len, Bytes.Bytes{len, buf})
5121
5122def sv.chunk.of(req: Req, +v11: Bool, +n: U32, c: Ck) -> Turn:
5123 Ck{st, parts, rest} = c
5124 match st:
5125 case DcDone{}:
5126 sv.body(req, v11, parts, rest)
5127 case DcBad{}:
5128 TurnFail{400}
5129 case DcSize{a, b}:
5130 TurnMore{SvChunk{req, v11, n, DcSize{a, b}, parts}, False{}}
5131 case DcExt{x}:
5132 TurnMore{SvChunk{req, v11, n, DcExt{x}, parts}, False{}}
5133 case DcSizeLf{x}:
5134 TurnMore{SvChunk{req, v11, n, DcSizeLf{x}, parts}, False{}}
5135 case DcData{k}:
5136 TurnMore{SvChunk{req, v11, n, DcData{k}, parts}, False{}}
5137 case DcDataCr{}:
5138 TurnMore{SvChunk{req, v11, n, DcDataCr{}, parts}, False{}}
5139 case DcDataLf{}:
5140 TurnMore{SvChunk{req, v11, n, DcDataLf{}, parts}, False{}}
5141 case DcTr{j}:
5142 TurnMore{SvChunk{req, v11, n, DcTr{j}, parts}, False{}}
5143
5144def sv.chunk.cap(big: Bool, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
5145 match big:
5146 case True{}:
5147 TurnFail{413}
5148 case False{}:
5149 sv.chunk.of(req, v11, n, ck(piece, st, parts))
5150
5151def sv.chunk(+max: Nat, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
5152 Bytes.Bytes{+len, buf} = piece
5153 +n2 = (n + len : U32)
5154 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})
5155
5156# RFC 9110 §10.1.1: answer 100 Continue only when the body is still to come.
5157def sv.cont(want: Bool, t: Turn) -> Turn:
5158 match t:
5159 case TurnMore{sv, c}:
5160 TurnMore{sv, want}
5161 case TurnClose{}:
5162 TurnClose{}
5163 case TurnFail{s}:
5164 TurnFail{s}
5165 case TurnReq{req, rest, v11}:
5166 TurnReq{req, rest, v11}
5167
5168def sv.cl.k(big: Bool, req: Req, +v11: Bool, +k: U32, rest: Bytes.Bytes) -> Turn:
5169 match big:
5170 case True{}:
5171 TurnFail{413}
5172 case False{}:
5173 sv.len(req, v11, k, Nil{}, rest)
5174
5175def sv.cl(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, n: Maybe<&2, U32>) -> Turn:
5176 match n:
5177 case None{}:
5178 TurnFail{400}
5179 case Some{+k}:
5180 sv.cl.k(Nat.is_lt(max, U32.to_nat(k)), req, v11, k, rest)
5181
5182def sv.frame(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, te: Bool) -> Turn:
5183 Req{method, path, +headers, body} = req
5184 match te:
5185 case True{}:
5186 sv.chunk(max, Req{method, path, headers, body}, v11, 0, dc.start(), Nil{}, rest)
5187 case False{}:
5188 sv.cl(max, Req{method, path, headers, body}, v11, rest, parse_u32(header(headers, "content-length")))
5189
5190def sv.expects(+v11: Bool, +headers: Map<&2, List<&2, String>>) -> Bool:
5191 Bool.and(v11, String.eq(String.to_lower(header(headers, "expect")), "100-continue"))
5192
5193def sv.got.head(+max: Nat, +v11: Bool, rest: Bytes.Bytes, req: Req) -> Turn:
5194 Req{method, path, +headers, body} = req
5195 sv.cont(sv.expects(v11, headers), sv.frame(max, Req{method, path, headers, body}, v11, rest, has_header(headers, "transfer-encoding")))
5196
5197def sv.parsed(+max: Nat, +v11: Bool, rest: Bytes.Bytes, g: Got) -> Turn:
5198 match g:
5199 case GotBad{}:
5200 TurnFail{400}
5201 case GotMore{}:
5202 TurnFail{400}
5203 case GotReq{req}:
5204 TurnReq{req, rest, v11}
5205 case GotHead{req}:
5206 sv.got.head(max, v11, rest, req)
5207
5208def sv.split(+max: Nat, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
5209 (buf, hb) = r
5210 +head = Bytes.to_string(hb)
5211 sv.parsed(max, req.v11(head), bytes.snd(Bytes.slice(buf, hlen, (len - hlen : U32))), parse.got(head))
5212
5213def sv.hit.none(big: Bool, buf: Bytes.Bytes) -> Turn:
5214 match big:
5215 case True{}:
5216 TurnFail{431}
5217 case False{}:
5218 TurnMore{SvHead{buf}, False{}}
5219
5220def sv.hit.some(big: Bool, +max: Nat, +hlen: U32, +len: U32, buf: Bytes.Bytes) -> Turn:
5221 match big:
5222 case True{}:
5223 TurnFail{431}
5224 case False{}:
5225 sv.split(max, hlen, len, Bytes.slice(buf, 0, hlen))
5226
5227# RFC 6585 §5: a head over 64 KiB is refused.
5228def sv.hit(+max: Nat, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Turn:
5229 match at:
5230 case None{}:
5231 sv.hit.none(U32.is_lt(65536, len), buf)
5232 case Some{+i}:
5233 +hlen = (i + 4 : U32)
5234 sv.hit.some(U32.is_lt(65536, hlen), max, hlen, len, buf)
5235
5236def sv.seek.of(+max: Nat, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Turn:
5237 (tail, m) = r
5238 sv.hit(max, len, buf, found.at(from, m))
5239
5240def sv.seek(+max: Nat, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
5241 (buf, tail) = r
5242 sv.seek.of(max, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
5243
5244# Only the new bytes, and the 3 before them, can finish the blank line.
5245def sv.head.at(+max: Nat, +from: U32, buf: Bytes.Bytes) -> Turn:
5246 Bytes.Bytes{+len, b} = buf
5247 sv.seek(max, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
5248
5249def sv.head(+max: Nat, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Turn:
5250 Bytes.Bytes{+ol, ob} = buf
5251 sv.head.at(max, Bool.pick(U32, U32.is_lt(ol, 3), 0, (ol - 3 : U32)), Bytes.append(Bytes.Bytes{ol, ob}, piece))
5252
5253def sv.closed.pick(empty: Bool) -> Turn:
5254 match empty:
5255 case True{}:
5256 TurnClose{}
5257 case False{}:
5258 TurnFail{400}
5259
5260def sv.closed.head(buf: Bytes.Bytes) -> Turn:
5261 Bytes.Bytes{+len, b} = buf
5262 sv.closed.pick(U32.is_eq(len, 0))
5263
5264# A close mid-request is a request cut short (RFC 9112 §8).
5265def sv.step(closed: Bool, +max: Nat, sv: Sv, piece: Bytes.Bytes) -> Turn:
5266 match closed:
5267 case True{}:
5268 match sv:
5269 case SvHead{buf}:
5270 sv.closed.head(buf)
5271 case SvLen{req, v11, left, parts}:
5272 TurnFail{400}
5273 case SvChunk{req, v11, n, st, parts}:
5274 TurnFail{400}
5275 case False{}:
5276 match sv:
5277 case SvHead{buf}:
5278 sv.head(max, buf, piece)
5279 case SvLen{req, +v11, +left, parts}:
5280 sv.len(req, v11, left, parts, piece)
5281 case SvChunk{req, +v11, +n, st, parts}:
5282 sv.chunk(max, req, v11, n, st, parts, piece)
5283
5284def sv.frame.req(t: Turn) -> Maybe<&1, String & String>:
5285 match t:
5286 case TurnReq{req, rest, v11}:
5287 Req{method, path, headers, body} = req
5288 Some{(Bytes.to_string(body), Bytes.to_string(rest))}
5289 case TurnMore{sv, c}:
5290 None{}
5291 case TurnFail{s}:
5292 None{}
5293 case TurnClose{}:
5294 None{}
5295
5296def sv.frame.go(xs: List<&2, String>, t: Turn) -> Maybe<&1, String & String>:
5297 match xs:
5298 case Nil{}:
5299 sv.frame.req(t)
5300 case Con{+x, rest}:
5301 match t:
5302 case TurnMore{sv, c}:
5303 sv.frame.go(rest, sv.step(False{}, serve.max(), sv, Bytes.from_string(x)))
5304 case TurnReq{req, r, v11}:
5305 sv.frame.req(TurnReq{req, r, v11})
5306 case TurnFail{s}:
5307 None{}
5308 case TurnClose{}:
5309 None{}
5310
5311# The body and the bytes after it, once the pieces make a whole request; None otherwise.
5312def serve.frame(xs: List<&2, String>) -> Maybe<&1, String & String>:
5313 sv.frame.go(xs, TurnMore{sv.none(), False{}})
5314
5315def talk.piece(+max: Nat, sv: Sv, p: U32 & Array<U32>) -> Turn:
5316 (+len, buf) = p
5317 sv.step(U32.is_eq(len, 0), max, sv, Bytes.Bytes{len, buf})
5318
5319def talk.next(+max: Nat, sv: Sv, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Turn:
5320 (s, r) = m
5321 match r:
5322 case Fail{e}:
5323 (s, TurnClose{})
5324 case Done{p}:
5325 (s, talk.piece(max, sv, p))
5326
5327def talk.after.pick(empty: Bool, +max: Nat, rest: Bytes.Bytes) -> Turn:
5328 match empty:
5329 case True{}:
5330 TurnMore{sv.none(), False{}}
5331 case False{}:
5332 sv.step(False{}, max, sv.none(), rest)
5333
5334def talk.after.rest(+max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
5335 Bytes.Bytes{+len, buf} = rest
5336 (s, talk.after.pick(U32.is_eq(len, 0), max, Bytes.Bytes{len, buf}))
5337
5338def talk.after.keep(keep: Bool, +max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
5339 match keep:
5340 case False{}:
5341 (s, TurnClose{})
5342 case True{}:
5343 talk.after.rest(max, rest, s)
5344
5345def talk.after(+max: Nat, keep: Bool, rest: Bytes.Bytes, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket & Turn:
5346 (s, r) = m
5347 match r:
5348 case Fail{e}:
5349 (s, TurnClose{})
5350 case Done{u}:
5351 talk.after.keep(keep, max, rest, s)
5352
5353def talk.send(+max: Nat, s: Socket, rest: Bytes.Bytes, +headers: Map<&2, List<&2, String>>, v11: Bool, +head: Bool, res: Res) -> IO(Socket & Turn):
5354 Res{+status, +rh, body} = res
5355 +keep = serve.keep(headers, v11, status, rh)
5356 do IO<Socket & Turn>:
5357 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, reply.bytes(Res{status, rh, body}, head, Bool.not(keep)))
5358 return talk.after(max, keep, rest, sent)
5359
5360def talk.cont.sent(m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket:
5361 (s, r) = m
5362 s
5363
5364def talk.cont(cont: Bool, s: Socket) -> IO(Socket):
5365 match cont:
5366 case False{}:
5367 IO.pure(Socket, s)
5368 case True{}:
5369 do IO<Socket>:
5370 sent : Socket & Result<&1, &1, U32 & String, Unit> <-
5371 io.send.bytes(False{}, s, Bytes.from_string("HTTP/1.1 100 Continue\r\n\r\n"))
5372 return talk.cont.sent(sent)
5373
5374@unsafe
5375def talk(~h: Req -> IO(Res), +max: Nat, st: Socket & Turn) -> IO(Unit):
5376 (s, t) = st
5377 match t:
5378 case TurnMore{sv, cont}:
5379 do IO<Unit>:
5380 s2 : Socket <- talk.cont(cont, s)
5381 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- Wire.recv.words(s2, 65536, 30000)
5382 talk(~h, max, talk.next(max, sv, m))
5383 case TurnReq{req, rest, v11}:
5384 Req{+method, path, +headers, body} = req
5385 do IO<Unit>:
5386 res : Res <- h(Req{method, path, headers, body})
5387 next : Socket & Turn <- talk.send(max, s, rest, headers, v11, String.eq(method, "HEAD"), res)
5388 talk(~h, max, next)
5389 case TurnFail{status}:
5390 reply_fail(s, status)
5391 case TurnClose{}:
5392 Socket.close(s)
5393
5394def conn(~h: Req -> IO(Res), +max: Nat, m: Listener & Result<&1, &1, U32 & String, Socket>) -> IO(Listener):
5395 (l, r) = m
5396 do IO<Listener>:
5397 s : Socket <- IO.pass(Socket, r)
5398 IO.spawn(Unit, talk(~h, max, (s, TurnMore{sv.none(), False{}})))
5399 return l
5400
5401@unsafe
5402def loop(~h: Req -> IO(Res), +max: Nat, l: Listener) -> IO(Unit):
5403 do IO<Unit>:
5404 m : Listener & Result<&1, &1, U32 & String, Socket> <- TCP.accept(l)
5405 l2 : Listener <- conn(~h, max, m)
5406 loop(~h, max, l2)
5407
5408def serve.on.with(~h: Req -> IO(Res), host: String, +port: U32, +max: Nat) -> IO(Unit):
5409 do IO<Unit>:
5410 l : Listener <- IO.try(Listener, TCP.listen(host, port))
5411 loop(~h, max, l)
5412
5413def serve.on(~h: Req -> IO(Res), host: String, +port: U32) -> IO(Unit):
5414 serve.on.with(~h, host, port, serve.max())
5415
5416def serve.with(~h: Req -> IO(Res), +port: U32, +max: Nat) -> IO(Unit):
5417 serve.on.with(~h, "0.0.0.0", port, max)
5418
5419def serve(~h: Req -> IO(Res), +port: U32) -> IO(Unit):
5420 serve.with(~h, port, serve.max())
5421
5422def serve.stream.nonempty(~S: Type, ~piece: S -> Bytes.Bytes -> IO(S & Bool), empty: Bool, state: S, b: Bytes.Bytes) -> IO(S & Bool):
5423 match empty:
5424 case True{}:
5425 IO.pure(S & Bool, (state, False{}))
5426 case False{}:
5427 piece(state, b)
5428
5429# The piece callback returns True to discard the rest of this request body.
5430def serve.stream.one(~S: Type, ~piece: S -> Bytes.Bytes -> IO(S & Bool), drop: Bool, state: S, b: Bytes.Bytes) -> IO(S & Bool):
5431 match drop:
5432 case True{}:
5433 IO.pure(S & Bool, (state, True{}))
5434 case False{}:
5435 Bytes.Bytes{+len, buf} = b
5436 serve.stream.nonempty(~S, ~piece, U32.is_eq(len, 0), state, Bytes.Bytes{len, buf})
5437
5438def serve.stream.parts(~S: Type, ~piece: S -> Bytes.Bytes -> IO(S & Bool), xs: List<&1, Bytes.Bytes>, st: S & Bool) -> IO(S & Bool):
5439 match xs:
5440 case Nil{}:
5441 IO.pure(S & Bool, st)
5442 case Con{b, rest}:
5443 (state, drop) = st
5444 do IO<S & Bool>:
5445 next : S & Bool <- serve.stream.one(~S, ~piece, drop, state, b)
5446 serve.stream.parts(~S, ~piece, rest, next)
5447
5448def serve.stream.feed(~S: Type, ~start: Req -> IO(S), ~piece: S -> Bytes.Bytes -> IO(S & Bool), req: Req, m: Maybe<&1, S & Bool>, parts: List<&1, Bytes.Bytes>) -> IO(S & Bool):
5449 match m:
5450 case None{}:
5451 do IO<S & Bool>:
5452 state : S <- start(req)
5453 serve.stream.parts(~S, ~piece, parts, (state, False{}))
5454 case Some{st}:
5455 serve.stream.parts(~S, ~piece, parts, st)
5456
5457def serve.stream.recv(+max: Nat, s: Socket, sv: Sv, cont: Bool) -> IO(Socket & Turn):
5458 do IO<Socket & Turn>:
5459 s2 : Socket <- talk.cont(cont, s)
5460 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- Wire.recv.words(s2, 65536, 30000)
5461 return talk.next(max, sv, m)
5462
5463def serve.stream.respond(~S: Type, ~finish: S -> IO(Res), +max: Nat, s: Socket, rest: Bytes.Bytes, +headers: Map<&2, List<&2, String>>, v11: Bool, +method: String, st: S & Bool) -> IO(Socket & Turn):
5464 (state, dropped) = st
5465 do IO<Socket & Turn>:
5466 res : Res <- finish(state)
5467 talk.send(max, s, rest, headers, v11, String.eq(method, "HEAD"), res)
5468
5469@unsafe
5470def serve.stream.talk(
5471 ~S: Type, ~start: Req -> IO(S), ~piece: S -> Bytes.Bytes -> IO(S & Bool),
5472 ~finish: S -> IO(Res), +max: Nat, st: Socket & Turn, m: Maybe<&1, S & Bool>
5473) -> IO(Unit):
5474 (s, t) = st
5475 match t:
5476 case TurnClose{}:
5477 Socket.close(s)
5478 case TurnFail{status}:
5479 reply_fail(s, status)
5480 case TurnReq{req, rest, v11}:
5481 Req{+method, path, +headers, body} = req
5482 do IO<Unit>:
5483 next : S & Bool <- serve.stream.feed(~S, ~start, ~piece,
5484 Req{method, path, headers, Bytes.new(0)}, m, [body])
5485 after : Socket & Turn <- serve.stream.respond(~S, ~finish, max, s, rest, headers, v11, method, next)
5486 serve.stream.talk(~S, ~start, ~piece, ~finish, max, after, None{})
5487 case TurnMore{sv, cont}:
5488 match sv:
5489 case SvHead{buf}:
5490 do IO<Unit>:
5491 next : Socket & Turn <- serve.stream.recv(max, s, SvHead{buf}, cont)
5492 serve.stream.talk(~S, ~start, ~piece, ~finish, max, next, m)
5493 case SvLen{req, +v11, +left, parts}:
5494 Req{+method, +path, +headers, body} = req
5495 do IO<Unit>:
5496 next : S & Bool <- serve.stream.feed(~S, ~start, ~piece,
5497 Req{method, path, headers, body}, m, List.reverse(&1, Bytes.Bytes, parts))
5498 more : Socket & Turn <- serve.stream.recv(max, s,
5499 SvLen{Req{method, path, headers, Bytes.new(0)}, v11, left, Nil{}}, cont)
5500 serve.stream.talk(~S, ~start, ~piece, ~finish, max, more, Some{next})
5501 case SvChunk{req, +v11, +n, st, parts}:
5502 Req{+method, +path, +headers, body} = req
5503 do IO<Unit>:
5504 next : S & Bool <- serve.stream.feed(~S, ~start, ~piece,
5505 Req{method, path, headers, body}, m, List.reverse(&1, Bytes.Bytes, parts))
5506 more : Socket & Turn <- serve.stream.recv(max, s,
5507 SvChunk{Req{method, path, headers, Bytes.new(0)}, v11, n, st, Nil{}}, cont)
5508 serve.stream.talk(~S, ~start, ~piece, ~finish, max, more, Some{next})
5509
5510
5511def serve.stream.conn(
5512 ~S: Type, ~start: Req -> IO(S), ~piece: S -> Bytes.Bytes -> IO(S & Bool),
5513 ~finish: S -> IO(Res), +max: Nat, m: Listener & Result<&1, &1, U32 & String, Socket>
5514) -> IO(Listener):
5515 (l, r) = m
5516 do IO<Listener>:
5517 s : Socket <- IO.pass(Socket, r)
5518 IO.spawn(Unit, serve.stream.talk(~S, ~start, ~piece, ~finish, max,
5519 (s, TurnMore{sv.none(), False{}}), None{}))
5520 return l
5521
5522@unsafe
5523def serve.stream.loop(
5524 ~S: Type, ~start: Req -> IO(S), ~piece: S -> Bytes.Bytes -> IO(S & Bool),
5525 ~finish: S -> IO(Res), +max: Nat, l: Listener
5526) -> IO(Unit):
5527 do IO<Unit>:
5528 m : Listener & Result<&1, &1, U32 & String, Socket> <- TCP.accept(l)
5529 l2 : Listener <- serve.stream.conn(~S, ~start, ~piece, ~finish, max, m)
5530 serve.stream.loop(~S, ~start, ~piece, ~finish, max, l2)
5531
5532def serve.stream.on.with(
5533 ~S: Type, ~start: Req -> IO(S), ~piece: S -> Bytes.Bytes -> IO(S & Bool),
5534 ~finish: S -> IO(Res), host: String, +port: U32, +max: Nat
5535) -> IO(Unit):
5536 do IO<Unit>:
5537 l : Listener <- IO.try(Listener, TCP.listen(host, port))
5538 serve.stream.loop(~S, ~start, ~piece, ~finish, max, l)
5539
5540def serve.stream.with(
5541 ~S: Type, ~start: Req -> IO(S), ~piece: S -> Bytes.Bytes -> IO(S & Bool),
5542 ~finish: S -> IO(Res), +port: U32, +max: Nat
5543) -> IO(Unit):
5544 serve.stream.on.with(~S, ~start, ~piece, ~finish, "0.0.0.0", port, max)
5545
5546type WriterMode is Data:
5547 WriteKnown{left: U32}
5548 WriteChunk{}
5549 WriteNone{}
5550
5551type Writer is Type:
5552 Writer{s: Socket, mode: WriterMode, failed: Bool}
5553
5554type WriteHead<-S: Type> is Type:
5555 WriteHead{status: U32, headers: Map<&2, List<&2, String>>, length: Maybe<&2, U32>, state: S}
5556
5557def writer.sent(+mode: WriterMode, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Writer:
5558 (s, r) = m
5559 match r:
5560 case Fail{e}:
5561 Writer{s, mode, True{}}
5562 case Done{u}:
5563 Writer{s, mode, False{}}
5564
5565def writer.raw(w: Writer, b: Bytes.Bytes) -> IO(Writer):
5566 Writer{s, +mode, failed} = w
5567 match failed:
5568 case True{}:
5569 IO.pure(Writer, Writer{s, mode, True{}})
5570 case False{}:
5571 do IO<Writer>:
5572 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, b)
5573 return writer.sent(mode, sent)
5574
5575def writer.chunk(s: Socket, b: Bytes.Bytes, +len: U32) -> IO(Writer):
5576 do IO<Writer>:
5577 head : Writer <- writer.raw(Writer{s, WriteChunk{}, False{}}, Bytes.from_string(hex(len) ++ "\r\n"))
5578 data : Writer <- writer.raw(head, b)
5579 writer.raw(data, Bytes.from_string("\r\n"))
5580
5581def writer.known(ok: Bool, s: Socket, +left: U32, +len: U32, b: Bytes.Bytes) -> IO(Writer):
5582 match ok:
5583 case False{}:
5584 IO.pure(Writer, Writer{s, WriteKnown{left}, True{}})
5585 case True{}:
5586 writer.raw(Writer{s, WriteKnown{(left - len : U32)}, False{}}, b)
5587
5588def writer.chunk.go(empty: Bool, s: Socket, b: Bytes.Bytes, +len: U32) -> IO(Writer):
5589 match empty:
5590 case True{}:
5591 IO.pure(Writer, Writer{s, WriteChunk{}, False{}})
5592 case False{}:
5593 writer.chunk(s, b, len)
5594
5595def writer.write.mode(s: Socket, mode: WriterMode, b: Bytes.Bytes) -> IO(Writer):
5596 match mode:
5597 case WriteNone{}:
5598 IO.pure(Writer, Writer{s, WriteNone{}, False{}})
5599 case WriteKnown{+left}:
5600 Bytes.Bytes{+len, buf} = b
5601 writer.known(U32.is_le(len, left), s, left, len, Bytes.Bytes{len, buf})
5602 case WriteChunk{}:
5603 Bytes.Bytes{+len, buf} = b
5604 writer.chunk.go(U32.is_zero(len), s, Bytes.Bytes{len, buf}, len)
5605
5606def writer.write(w: Writer, b: Bytes.Bytes) -> IO(Writer):
5607 Writer{s, mode, failed} = w
5608 match failed:
5609 case True{}:
5610 IO.pure(Writer, Writer{s, mode, True{}})
5611 case False{}:
5612 writer.write.mode(s, mode, b)
5613
5614
5615def writer.result(w: Writer) -> Socket & Bool:
5616 Writer{s, mode, failed} = w
5617 (s, Bool.not(failed))
5618
5619def writer.finish.mode(s: Socket, mode: WriterMode) -> IO(Socket & Bool):
5620 match mode:
5621 case WriteNone{}:
5622 IO.pure(Socket & Bool, (s, True{}))
5623 case WriteKnown{+left}:
5624 IO.pure(Socket & Bool, (s, U32.is_zero(left)))
5625 case WriteChunk{}:
5626 do IO<Socket & Bool>:
5627 end : Writer <- writer.raw(Writer{s, WriteChunk{}, False{}}, Bytes.from_string("0\r\n\r\n"))
5628 return writer.result(end)
5629
5630def writer.finish(w: Writer) -> IO(Socket & Bool):
5631 Writer{s, mode, failed} = w
5632 match failed:
5633 case True{}:
5634 IO.pure(Socket & Bool, (s, False{}))
5635 case False{}:
5636 writer.finish.mode(s, mode)
5637
5638def writer.header.one(m: Map<&2, List<&2, String>>, +key: String, vs: List<&2, String>, framing: Bool) -> Map<&2, List<&2, String>>:
5639 match framing:
5640 case True{}:
5641 m
5642 case False{}:
5643 Map.set(&2, List<&2, String>, m, key, vs)
5644
5645def writer.headers(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
5646 match xs:
5647 case Nil{}:
5648 m
5649 case (k, vs) <> rest:
5650 +key = String.to_lower(k)
5651 +framing = Bool.or(String.eq(key, "content-length"), String.eq(key, "transfer-encoding"))
5652 writer.headers(rest, writer.header.one(m, key, vs, framing))
5653
5654def writer.plan.body(headers: Map<&2, List<&2, String>>, length: Maybe<&2, U32>) -> WriterMode & Map<&2, List<&2, String>>:
5655 match length:
5656 case Some{+n}:
5657 (WriteKnown{n}, set(headers, "content-length", U32.show(n)))
5658 case None{}:
5659 (WriteChunk{}, set(headers, "transfer-encoding", "chunked"))
5660
5661def writer.plan(nobody: Bool, headers: Map<&2, List<&2, String>>, length: Maybe<&2, U32>) -> WriterMode & Map<&2, List<&2, String>>:
5662 match nobody:
5663 case True{}:
5664 (WriteNone{}, headers)
5665 case False{}:
5666 writer.plan.body(headers, length)
5667
5668def serve.write.after(+max: Nat, keep: Bool, rest: Bytes.Bytes, m: Socket & Bool) -> Socket & Turn:
5669 (s, ok) = m
5670 match ok:
5671 case False{}:
5672 (s, TurnClose{})
5673 case True{}:
5674 talk.after.keep(keep, max, rest, s)
5675
5676def serve.write.finish(+max: Nat, keep: Bool, rest: Bytes.Bytes, w: Writer) -> IO(Socket & Turn):
5677 do IO<Socket & Turn>:
5678 done : Socket & Bool <- writer.finish(w)
5679 return serve.write.after(max, keep, rest, done)
5680
5681def serve.write.body(~S: Type, ~write: S -> Writer -> IO(Writer), +max: Nat, +keep: Bool, rest: Bytes.Bytes, state: S, s: Socket, mode: WriterMode, suppress: Bool) -> IO(Socket & Turn):
5682 match suppress:
5683 case True{}:
5684 serve.write.finish(max, keep, rest, Writer{s, WriteNone{}, False{}})
5685 case False{}:
5686 do IO<Socket & Turn>:
5687 w : Writer <- write(state, Writer{s, mode, False{}})
5688 serve.write.finish(max, keep, rest, w)
5689
5690def serve.write.open(~S: Type, ~write: S -> Writer -> IO(Writer), +max: Nat, +keep: Bool, rest: Bytes.Bytes, state: S, mode: WriterMode, suppress: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Socket & Turn):
5691 (s, r) = m
5692 match r:
5693 case Fail{e}:
5694 IO.pure(Socket & Turn, (s, TurnClose{}))
5695 case Done{u}:
5696 serve.write.body(~S, ~write, max, keep, rest, state, s, mode, suppress)
5697
5698def writer.connection(keep: Bool, headers: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
5699 match keep:
5700 case True{}:
5701 headers
5702 case False{}:
5703 set(headers, "connection", "close")
5704
5705def serve.write.send.plan(
5706 ~S: Type, ~write: S -> Writer -> IO(Writer), +max: Nat, s: Socket, rest: Bytes.Bytes,
5707 +keep: Bool, +head: Bool, +status: U32, state: S, plan: WriterMode & Map<&2, List<&2, String>>
5708) -> IO(Socket & Turn):
5709 (mode, headers) = plan
5710 sent_headers = writer.connection(keep, headers)
5711 do IO<Socket & Turn>:
5712 sent : Socket & Result<&1, &1, U32 & String, Unit> <-
5713 io.send.bytes(False{}, s, Bytes.from_string(response(status, sent_headers, "")))
5714 serve.write.open(~S, ~write, max, keep, rest, state, mode,
5715 frame.nobody(status, head), sent)
5716
5717def serve.write.send(
5718 ~S: Type, ~write: S -> Writer -> IO(Writer), +max: Nat, s: Socket, rest: Bytes.Bytes,
5719 +headers: Map<&2, List<&2, String>>, v11: Bool, +head: Bool, out: WriteHead<S>
5720) -> IO(Socket & Turn):
5721 WriteHead{+status, rh, length, state} = out
5722 +normalized = writer.headers(Map.to_list(&2, List<&2, String>, rh), empty())
5723 +keep = serve.keep(headers, v11, status, normalized)
5724 serve.write.send.plan(~S, ~write, max, s, rest, keep, head, status, state,
5725 writer.plan(frame.nobody(status, False{}), normalized, length))
5726
5727@unsafe
5728def serve.write.talk(
5729 ~S: Type, ~start: Req -> IO(WriteHead<S>), ~write: S -> Writer -> IO(Writer),
5730 +max: Nat, st: Socket & Turn
5731) -> IO(Unit):
5732 (s, t) = st
5733 match t:
5734 case TurnMore{sv, cont}:
5735 do IO<Unit>:
5736 more : Socket & Turn <- serve.stream.recv(max, s, sv, cont)
5737 serve.write.talk(~S, ~start, ~write, max, more)
5738 case TurnReq{req, rest, v11}:
5739 Req{+method, path, +headers, body} = req
5740 do IO<Unit>:
5741 out : WriteHead<S> <- start(Req{method, path, headers, body})
5742 after : Socket & Turn <- serve.write.send(~S, ~write, max, s, rest, headers, v11, String.eq(method, "HEAD"), out)
5743 serve.write.talk(~S, ~start, ~write, max, after)
5744 case TurnFail{status}:
5745 reply_fail(s, status)
5746 case TurnClose{}:
5747 Socket.close(s)
5748
5749def serve.write.conn(
5750 ~S: Type, ~start: Req -> IO(WriteHead<S>), ~write: S -> Writer -> IO(Writer),
5751 +max: Nat, m: Listener & Result<&1, &1, U32 & String, Socket>
5752) -> IO(Listener):
5753 (l, r) = m
5754 do IO<Listener>:
5755 s : Socket <- IO.pass(Socket, r)
5756 IO.spawn(Unit, serve.write.talk(~S, ~start, ~write, max,
5757 (s, TurnMore{sv.none(), False{}})))
5758 return l
5759
5760@unsafe
5761def serve.write.loop(
5762 ~S: Type, ~start: Req -> IO(WriteHead<S>), ~write: S -> Writer -> IO(Writer),
5763 +max: Nat, l: Listener
5764) -> IO(Unit):
5765 do IO<Unit>:
5766 m : Listener & Result<&1, &1, U32 & String, Socket> <- TCP.accept(l)
5767 l2 : Listener <- serve.write.conn(~S, ~start, ~write, max, m)
5768 serve.write.loop(~S, ~start, ~write, max, l2)
5769
5770def serve.write.on.with(
5771 ~S: Type, ~start: Req -> IO(WriteHead<S>), ~write: S -> Writer -> IO(Writer),
5772 host: String, +port: U32, +max: Nat
5773) -> IO(Unit):
5774 do IO<Unit>:
5775 l : Listener <- IO.try(Listener, TCP.listen(host, port))
5776 serve.write.loop(~S, ~start, ~write, max, l)
5777
5778def serve.write.with(
5779 ~S: Type, ~start: Req -> IO(WriteHead<S>), ~write: S -> Writer -> IO(Writer),
5780 +port: U32, +max: Nat
5781) -> IO(Unit):
5782 serve.write.on.with(~S, ~start, ~write, "0.0.0.0", port, max)