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