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