src/packed.bend

emerging-ezhttp@0.21.0.0 · 211 lines · 23 definitions

1# ezhttp/src/packed: a response read off its packed octets (bend-kit-bytes),
2# so its body is never turned into text. Only the heads and the chunk-size
3# lines are read as text, a few octets each; every decision is
4# src/http.bend's, the same one its text parse makes (SPEC.md HTTP-CLI-15):
5# which head is final and what its plan is (head.final), its reason phrase
6# (phrase.line), and what each chunk-size line says (chunk.size). This module
7# only finds those lines and copies the body's octets out (SPEC.md
8# HTTP-TRUST-9).
9import Base
10import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
11import emerging-ezhttp@0.21.0.0/src/http.bend as Http
12
13# a response read off its octets: torn, or its status, its header fields and
14# reason phrase as octet text, and its body's octets
15type Got is Type:  # noqa: L001 holds packed Bytes, which no law reaches (HTTP-TRUST-9)
16  Torn{why: String}
17  Got{status: U32, headers: List<&2, Http.Header>, reason: String,
18    body: Bytes.Bytes}
19
20# a chunked body's octets so far, newest first, or why it was torn
21type Parts is Type:  # noqa: L001 holds packed Bytes, which no law reaches (HTTP-TRUST-9)
22  Bad{why: String}
23  Parts{parts: List<&1, Bytes.Bytes>}
24
25# a slice's copy as text, the buffer kept
26def packed.text.of(r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes & String:
27  (b, piece) = r
28  (b, Bytes.to_string(piece))
29
30# n octets from `at` as text (a head or a chunk-size line), the buffer kept
31def packed.text(b: Bytes.Bytes, +at: U32, +n: U32) -> Bytes.Bytes & String:
32  packed.text.of(Bytes.slice(b, at, n))
33
34# n octets from `at`, the buffer dropped
35def packed.copy(b: Bytes.Bytes, +at: U32, +n: U32) -> Bytes.Bytes:
36  Bytes.snd(Bytes.slice(b, at, n))
37
38# --- a chunked body (RFC 9112 §7.1), as chunk.size decides ---
39
40# a chunk's octets copied out, then on to the chunk-size line after its CRLF
41def packed.chunk.take(r: Bytes.Bytes & Bytes.Bytes, +next: U32,
42  acc: List<&1, Bytes.Bytes>,
43  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
44  (b, part) = r
45  go(b)(next)(part <> acc)
46
47# a chunk of k octets from d, ready when its CRLF follows them
48def packed.chunk.ready.is(b: Bytes.Bytes, +d: U32, +k: U32,
49  acc: List<&1, Bytes.Bytes>, ready: Bool,
50  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
51  match ready:
52    case False{}:
53      Bad{Http.chunk.short()}
54    case True{}:
55      packed.chunk.take(Bytes.slice(b, d, k), (d + k + 2 : U32), acc, go)
56
57# a chunk of k octets from d whose CRLF has been looked for (chunks.ready)
58def packed.chunk.ready(r: Bytes.Bytes & String, +d: U32, +k: U32,
59  acc: List<&1, Bytes.Bytes>,
60  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
61  (b, crlf) = r
62  packed.chunk.ready.is(b, d, k, acc, String.eq(crlf, "\r\n"), go)
63
64# a chunk of n octets from d: its octets must all be there, and a CRLF after
65# them
66def packed.chunk.data(b: Bytes.Bytes, +d: U32, +n: Nat,
67  acc: List<&1, Bytes.Bytes>, fits: Bool,
68  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
69  match fits:
70    case False{}:
71      Bad{Http.chunk.short()}
72    case True{}:
73      +k = U32.from_nat(n)
74      packed.chunk.ready(packed.text(b, (d + k : U32), 2), d, k, acc, go)
75
76# what a chunk-size line says, acted on with the octets after it
77def packed.chunk.size(b: Bytes.Bytes, +d: U32, +len: U32,
78  acc: List<&1, Bytes.Bytes>, z: Http.Size,
79  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
80  match z:
81    case Http.SizeBad{why}:
82      Bad{why}
83    case Http.SizeLast{}:
84      Parts{acc}
85    case Http.SizeData{+n}:
86      packed.chunk.data(b, d, n, acc,
87        Bool.not(Nat.is_lt(U32.to_nat((len - d : U32)), Nat.add(n, 2n))), go)
88
89# a chunk-size line read, its octets after its CRLF
90def packed.chunk.line(r: Bytes.Bytes & String, +d: U32, +len: U32,
91  acc: List<&1, Bytes.Bytes>,
92  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
93  (b, line) = r
94  packed.chunk.size(b, d, len, acc, Http.chunk.size(line), go)
95
96# a chunk-size line that ends at i, or none ends: the body ends there
97def packed.chunk.at(r: Bytes.Bytes & Maybe<&2, U32>, +p: U32,
98  +len: U32, acc: List<&1, Bytes.Bytes>,
99  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
100  (b, at) = r
101  match at:
102    case None{}:
103      Parts{acc}
104    case Some{+i}:
105      packed.chunk.line(packed.text(b, p, (i - p : U32)), (i + 2 : U32),
106        len, acc, go)
107
108# the chunks from the chunk-size line at p, at most `fuel` of them
109def packed.chunks(fuel: Nat, b: Bytes.Bytes, +p: U32, +len: U32,
110  acc: List<&1, Bytes.Bytes>) -> Parts:
111  match fuel:
112    case 0n:
113      Bad{"the chunked body is truncated"}
114    case 1n+f:
115      packed.chunk.at(Bytes.find.from(b, "\r\n", p), p, len, acc,
116        b2 => q => a2 => packed.chunks(f, b2, q, len, a2))
117
118# a chunked body's octets in order, or why it was torn
119def packed.chunked(st: U32, hs: List<&2, Http.Header>, reason: String,
120  r: Parts) -> Got:
121  match r:
122    case Bad{why}:
123      Torn{why}
124    case Parts{ps}:
125      Got{st, hs, reason, Bytes.concat(List.reverse(&1, Bytes.Bytes, ps))}
126
127# --- the body under its framing (RFC 9112 §6.3) ---
128
129# a body framed by Content-Length: torn when fewer octets arrived
130def packed.sized(st: U32, hs: List<&2, Http.Header>, reason: String,
131  b: Bytes.Bytes, +q: U32, +n: Nat, short: Bool) -> Got:
132  match short:
133    case True{}:
134      Torn{"the response body stopped before its Content-Length"}
135    case False{}:
136      Got{st, hs, reason, packed.copy(b, q, U32.from_nat(n))}
137
138# the octets after the final head, as its framing says
139def packed.body(st: U32, hs: List<&2, Http.Header>, reason: String,
140  f: Http.Frame, b: Bytes.Bytes, +q: U32, +len: U32) -> Got:
141  match f:
142    case Http.Bare{}:
143      Got{st, hs, reason, Bytes.new(0)}
144    case Http.Sized{+n}:
145      packed.sized(st, hs, reason, b, q, n,
146        Nat.is_lt(U32.to_nat((len - q : U32)), n))
147    case Http.Chunked{}:
148      packed.chunked(st, hs, reason,
149        packed.chunks(U32.to_nat((len - q : U32)), b, q, len, []))
150    case Http.Closed{}:
151      Got{st, hs, reason, packed.copy(b, q, (len - q : U32))}
152
153# the final head's plan carried out on the octets after it
154def packed.final(p: Http.Plan, reason: String, b: Bytes.Bytes, +q: U32,
155  +len: U32) -> Got:
156  match p:
157    case Http.Unplanned{why}:
158      Torn{why}
159    case Http.Planned{st, hs, f}:
160      packed.body(st, hs, reason, f, b, q, len)
161
162# --- the heads (RFC 9112 §2.1, RFC 9110 §15.2) ---
163
164# an interim head is skipped, any other is the final one
165def packed.step(+asked: Bool, b: Bytes.Bytes, +q: U32, +len: U32,
166  +ls: List<&2, String>, skip: Bool, rest: Bytes.Bytes -> U32 -> Got) -> Got:
167  match skip:
168    case True{}:
169      rest(b)(q)
170    case False{}:
171      packed.final(Http.head.final(asked, ls), Http.phrase.line(Http.first(ls)),
172        b, q, len)
173
174# a head read as text, and the octets after its blank line from q
175def packed.head.text(+asked: Bool, r: Bytes.Bytes & String, +q: U32,
176  +len: U32, rest: Bytes.Bytes -> U32 -> Got) -> Got:
177  (b, before) = r
178  +ls = String.lines(before)
179  packed.step(asked, b, q, len, ls,
180    Http.interim.skip.of(Http.status.of(ls), U32.is_lt(q, len)), rest)
181
182# a head that ends at i, or none ends
183def packed.head(+asked: Bool, r: Bytes.Bytes & Maybe<&2, U32>, +p: U32,
184  +len: U32, rest: Bytes.Bytes -> U32 -> Got) -> Got:
185  (b, at) = r
186  match at:
187    case None{}:
188      Torn{"the response head has no blank line after it"}
189    case Some{+i}:
190      packed.head.text(asked, packed.text(b, p, (i - p : U32)), (i + 4 : U32),
191        len, rest)
192
193# the heads in turn from p, at most `fuel` of them
194def packed.heads(fuel: Nat, +asked: Bool, b: Bytes.Bytes, +p: U32, +len: U32)
195  -> Got:
196  match fuel:
197    case 0n:
198      Torn{"the response head has no blank line after it"}
199    case 1n+f:
200      packed.head(asked, Bytes.find.from(b, "\r\n\r\n", p), p, len,
201        b2 => q => packed.heads(f, asked, b2, q, len))
202
203# the response to a request with this method, its octets counted
204def packed.reply.of(+method: String, r: Bytes.Bytes & U32) -> Got:
205  (b, +len) = r
206  packed.heads(U32.to_nat(len), String.eq(method, "HEAD"), b, 0, len)
207
208# the response to a request with this method, read off its octets as
209# parse.to reads its text (SPEC.md HTTP-CLI-9, HTTP-CLI-15, HTTP-TRUST-9)
210def packed.reply(+method: String, b: Bytes.Bytes) -> Got:
211  packed.reply.of(method, Bytes.length(b))