src/wirespec.bend
emerging-ezhttp@0.21.0.0 · 391 lines · 0 definitions
1# ezhttp/src/wirespec: what the client sends, when it has heard a whole
2# answer, and what a failed socket call is reported as, pure. Kept apart from
3# wire.bend (bend-kit-wire's effects) so the proof gate can import it.
4# wire.bend and client.bend act on what is decided here.
5#
6# A failed exchange's answer is a non-zero status on its first line, then the
7# reason (wire.fail); a successful one is the response's octets, which
8# wire.bend keeps packed and packed.bend reads. SPEC.md HTTP-CLI lists what is
9# guaranteed.
10import Base
11import emerging-ezhttp@0.21.0.0/src/http.bend as Http
12import emerging-ezhttp@0.21.0.0/src/url.bend as Url
13import emerging-ezhttp@0.21.0.0/src/body.bend as Body
14import emerging-ezhttp@0.21.0.0/src/pct.bend as Pct
15import emerging-ezhttp@0.21.0.0/src/qs.bend as Qs
16
17# --- the deadline ---
18
19# the deadline of an exchange with no timeout: 60 s, in milliseconds
20def wire.ms.dflt() -> U32:
21 60000
22
23# a timeout once it is known whether it is 0
24def wire.ms.pick(ms: U32, zero: Bool) -> U32:
25 match zero:
26 case True{}:
27 1
28 case False{}:
29 ms
30
31# a timeout as a deadline bend-kit-wire reads: 0 would be none there, so it
32# is 1 ms
33def wire.ms.at(+ms: U32) -> U32:
34 wire.ms.pick(ms, U32.is_eq(ms, 0))
35
36# the deadline every socket call of an exchange gets: the timeout it was made
37# with, or the default (SPEC.md HTTP-CLI-1, 2)
38def wire.ms.of(m: Maybe<&2, U32>) -> U32:
39 match m:
40 case None{}:
41 wire.ms.dflt()
42 case Some{ms}:
43 wire.ms.at(ms)
44
45# --- the answer ---
46
47# the wire status for an exchange that ran out of time (curl's
48# CURLE_OPERATION_TIMEDOUT)
49def wire.late() -> U32:
50 28
51
52# what a failed exchange is reported as: a timeout is marked, any other
53# failure's reason is kept as it is
54def wire.why.of(why: String, late: Bool) -> String:
55 match late:
56 case True{}:
57 "timed out: " ++ why
58 case False{}:
59 why
60
61# a failed exchange's status and reason as the reason the client reports
62def wire.why(code: Maybe<&2, U32>, why: String) -> String:
63 match code:
64 case None{}:
65 why
66 case Some{n}:
67 wire.why.of(why, U32.is_eq(n, wire.late()))
68
69# whether a reported reason is a timeout
70def wire.timed_out(why: String) -> Bool:
71 String.starts_with(why, "timed out: ")
72
73# --- what is sent ---
74
75# what a request to a URL becomes: nothing when the URL did not parse, else
76# the scheme (secure or not), host, port, method and request text the effect
77# is given; the answer is read by that method (wire.read.next)
78type Exchange is Data:
79 NoUrl{why: String}
80 Exchange{secure: Bool, host: String, port: U32, method: String, req: String}
81
82# the exchange once it is known whether the scheme wants TLS
83def wire.exchange.at(+method: String, +secure: Bool, +host: String,
84 +port: U32, path: String, headers: List<&2, Http.Header>, body: String)
85 -> Exchange:
86 Exchange{secure, host, port, method,
87 Http.request.at(method, secure, host, port, path, headers, body)}
88
89# the method an exchange is sent and read by, none when nothing is sent
90def wire.exchange.method(ex: Exchange) -> Maybe<&2, String>:
91 match ex:
92 case NoUrl{why}:
93 None{}
94 case Exchange{secure, host, port, method, req}:
95 Some{method}
96
97# a request with this method, headers and body to a URL that came apart
98def wire.exchange(method: String, l: Url.Loc, headers: List<&2, Http.Header>,
99 body: String) -> Exchange:
100 match l:
101 case Url.Bad{why}:
102 NoUrl{why}
103 case Url.Loc{scheme, host, port, path}:
104 +secure = String.eq(scheme, "https")
105 wire.exchange.at(method, secure, host, port, path, headers, body)
106
107# a request with n octets of body to a URL that came apart: the request text
108# ends at the blank line, and the octets go after it
109def wire.exchange.octets(+method: String, l: Url.Loc,
110 headers: List<&2, Http.Header>, n: Nat) -> Exchange:
111 match l:
112 case Url.Bad{why}:
113 NoUrl{why}
114 case Url.Loc{scheme, +host, +port, path}:
115 +secure = String.eq(scheme, "https")
116 Exchange{secure, host, port, method,
117 Http.request.head.at(method, secure, host, port, path, headers, n)}
118
119# a request with a body of this shape to a URL that came apart: text inside
120# the request text as UTF-8, octets after it (SPEC.md HTTP-CLI-10)
121def wire.exchange.body(method: String, l: Url.Loc,
122 headers: List<&2, Http.Header>, b: Body.Shape) -> Exchange:
123 match b:
124 case Body.ShapeText{text}:
125 wire.exchange(method, l, headers, text)
126 case Body.ShapeOctets{n}:
127 wire.exchange.octets(method, l, headers, U32.to_nat(n))
128
129# --- what is heard ---
130
131# an answer's status: the number on its first line, if it is one
132def wire.code.of(c: Http.Cut, raw: String) -> Maybe<&2, U32>:
133 match c:
134 case Http.NoCut{}:
135 U32.read(raw)
136 case Http.Cut{before, after}:
137 U32.read(before)
138
139# an answer's status line as a number
140def wire.code(+raw: String) -> Maybe<&2, U32>:
141 wire.code.of(Http.divide(raw, "\n"), raw)
142
143# the text after an answer's first newline
144def wire.text.of(c: Http.Cut) -> String:
145 match c:
146 case Http.NoCut{}:
147 ""
148 case Http.Cut{before, after}:
149 after
150
151# the text after an answer's first newline
152def wire.text(raw: String) -> String:
153 wire.text.of(Http.divide(raw, "\n"))
154
155# whether a status is success (0)
156def wire.ok.of(m: Maybe<&2, U32>) -> Bool:
157 match m:
158 case None{}:
159 False{}
160 case Some{n}:
161 U32.is_eq(n, 0)
162
163# whether an answer has status 0
164def wire.ok(raw: String) -> Bool:
165 wire.ok.of(wire.code(raw))
166
167# the text a list of pieces, newest first, stands for
168def wire.joined(ps: List<&2, String>) -> String:
169 match ps:
170 case []:
171 ""
172 case p <> rest:
173 wire.joined(rest) ++ p
174
175# the pieces put together onto what follows them, each copied once
176def wire.join.go(ps: List<&2, String>, acc: String) -> String:
177 match ps:
178 case []:
179 acc
180 case p <> rest:
181 wire.join.go(rest, p ++ acc)
182
183# the text a list of pieces, newest first, stands for, built in one pass
184def wire.join(ps: List<&2, String>) -> String:
185 wire.join.go(ps, "")
186
187# where a response to a request with this method stands before anything has
188# been received
189def wire.got(+method: String) -> Http.Hear:
190 Http.hear.of(method, "")
191
192# after a read: read again from where the response now stands, or it has all
193# been received
194type Read is Data:
195 Again{hear: Http.Hear}
196 Heard{}
197
198# where the response stands after a read, judged
199def wire.read.done(+h: Http.Hear, done: Bool) -> Read:
200 match done:
201 case True{}:
202 Heard{}
203 case False{}:
204 Again{h}
205
206# where the response stands after a read, judged
207def wire.read.with(+h: Http.Hear) -> Read:
208 wire.read.done(h, Http.hear.done(h))
209
210# a read that brought text, or found the connection closed
211def wire.read.got(h: Http.Hear, +text: String, closed: Bool) -> Read:
212 match closed:
213 case True{}:
214 Heard{}
215 case False{}:
216 wire.read.with(Http.hear.more(h, text))
217
218# what to do after a read brought this text, judged from where the response
219# stood (SPEC.md HTTP-CLI-6)
220def wire.read.next(h: Http.Hear, +text: String) -> Read:
221 wire.read.got(h, text, String.is_empty(text))
222
223# a read of m octets judged by its count, when that is enough to judge it
224def wire.read.counted(+h: Http.Hear, +m: Nat, counts: Bool) -> Maybe<&2, Read>:
225 match counts:
226 case True{}:
227 Some{wire.read.with(Http.hear.more.n(h, m))}
228 case False{}:
229 None{}
230
231# a read of m octets: none is the close
232def wire.read.count.at(+h: Http.Hear, +m: Nat, closed: Bool)
233 -> Maybe<&2, Read>:
234 match closed:
235 case True{}:
236 Some{Heard{}}
237 case False{}:
238 wire.read.counted(h, m, Http.hear.counts(h, m))
239
240# what to do after a read of m octets, when their count alone decides it;
241# none when their text is needed (wire.read.next) (SPEC.md HTTP-CLI-6)
242def wire.read.count(+h: Http.Hear, +m: Nat) -> Maybe<&2, Read>:
243 wire.read.count.at(h, m, Nat.is_eq(m, 0n))
244
245# the answer when the reads run out before the response ends
246def wire.spent() -> String:
247 "56\nthe answer did not end within 65536 reads"
248
249# the reason a failed exchange's answer is reported with (wire.why)
250def wire.failed(+raw: String) -> String:
251 wire.why(wire.code(raw), wire.text(raw))
252
253# the response an exchange's answer holds, read by the request's method
254# (SPEC.md HTTP-CLI-9); a failed exchange is torn with the reason it is
255# reported with (wire.why)
256def wire.heard.of(+method: String, +raw: String, ok: Bool) -> Http.Reply:
257 match ok:
258 case False{}:
259 Http.Torn{wire.failed(raw)}
260 case True{}:
261 Http.parse.to(method, wire.text(raw))
262
263# the reason phrase of the response an exchange's answer holds (SPEC.md
264# HTTP-CLI-11); a failed exchange's is read from its reason and not used
265def wire.phrase(raw: String) -> String:
266 Http.phrase.to(wire.text(raw))
267
268# the response an exchange's answer holds
269def wire.heard(+method: String, +raw: String) -> Http.Reply:
270 wire.heard.of(method, raw, wire.ok(raw))
271
272# --- what goes on the wire (SPEC.md HTTP-CLI-10) ---
273
274# a request text's UTF-8 octets, one character each, onto the octets after it
275def wire.payload.text(s: String, rest: String) -> String:
276 match s:
277 case SNil{}:
278 rest
279 case SCon{Chr{+cp}, t}:
280 Body.octets.chars(Pct.utf8(cp)) ++ wire.payload.text(t, rest)
281
282# the octets of a request text, one character each: its UTF-8 (the body's
283# octets go after them)
284def wire.payload(req: String) -> String:
285 wire.payload.text(req, "")
286
287# --- what a failed socket call is reported as (SPEC.md HTTP-CLI-13, 14) ---
288
289# where in an exchange a call failed
290type Phase is Data:
291 Resolve{}
292 Connect{}
293 Handshake{}
294 Send{}
295 Receive{}
296
297# the error number a call that ran out of time fails with (Linux ETIMEDOUT)
298def wire.etimedout() -> U32:
299 110
300
301# the Linux errno symbols this table names
302def wire.errnos() -> List<&2, Http.Phrase>:
303 [Http.P{1, "EPERM"}, Http.P{2, "ENOENT"}, Http.P{4, "EINTR"},
304 Http.P{5, "EIO"}, Http.P{9, "EBADF"}, Http.P{11, "EAGAIN"},
305 Http.P{12, "ENOMEM"}, Http.P{13, "EACCES"}, Http.P{22, "EINVAL"},
306 Http.P{23, "ENFILE"}, Http.P{24, "EMFILE"}, Http.P{32, "EPIPE"},
307 Http.P{71, "EPROTO"}, Http.P{88, "ENOTSOCK"},
308 Http.P{93, "EPROTONOSUPPORT"}, Http.P{97, "EAFNOSUPPORT"},
309 Http.P{98, "EADDRINUSE"}, Http.P{99, "EADDRNOTAVAIL"},
310 Http.P{100, "ENETDOWN"}, Http.P{101, "ENETUNREACH"},
311 Http.P{103, "ECONNABORTED"}, Http.P{104, "ECONNRESET"},
312 Http.P{105, "ENOBUFS"}, Http.P{106, "EISCONN"},
313 Http.P{107, "ENOTCONN"}, Http.P{110, "ETIMEDOUT"},
314 Http.P{111, "ECONNREFUSED"}, Http.P{112, "EHOSTDOWN"},
315 Http.P{113, "EHOSTUNREACH"}, Http.P{114, "EALREADY"},
316 Http.P{115, "EINPROGRESS"}]
317
318# a name from the table, or `errno` when it has none
319def wire.errno.or(name: String) -> String:
320 match name:
321 case SNil{}:
322 "errno"
323 case SCon{h, t}:
324 SCon{h, t}
325
326# an error number's name (SPEC.md HTTP-CLI-14)
327def wire.errno.name(+n: U32) -> String:
328 wire.errno.or(Http.reason.in(wire.errnos(), n))
329
330# an error number as a reason names it: `<name> (<n>)`
331def wire.cause(+n: U32) -> String:
332 wire.errno.name(n) ++ " (" ++ U32.show(n) ++ ")"
333
334# a resolve's failure: bend-kit-dns reports a name with no address as
335# ENOENT, whose name would read as a missing file, so only the host is named
336def wire.fail.resolve(host: String, +n: U32, none: Bool) -> String:
337 match none:
338 case True{}:
339 "6\ncould not resolve " ++ host
340 case False{}:
341 "6\ncould not resolve " ++ host ++ ": " ++ wire.cause(n)
342
343# a call that ran out of time, by its phase
344def wire.fail.late(p: Phase, host: String, +port: U32, +ms: U32, +n: U32)
345 -> String:
346 match p:
347 case Resolve{}:
348 wire.fail.resolve(host, n, U32.is_eq(n, 2))
349 case Connect{}:
350 "28\nconnecting to " ++ host ++ " port " ++ U32.show(port)
351 ++ " took over " ++ U32.show(ms) ++ " ms"
352 case Handshake{}:
353 "28\nthe TLS handshake with " ++ host ++ " took over " ++ U32.show(ms)
354 ++ " ms"
355 case Send{}:
356 "28\nsending the request to " ++ host ++ " took over " ++ U32.show(ms)
357 ++ " ms"
358 case Receive{}:
359 "28\n" ++ host ++ " sent nothing for " ++ U32.show(ms) ++ " ms"
360
361# a call that failed for another reason, by its phase
362def wire.fail.other(p: Phase, host: String, +port: U32, +n: U32, why: String)
363 -> String:
364 match p:
365 case Resolve{}:
366 wire.fail.resolve(host, n, U32.is_eq(n, 2))
367 case Connect{}:
368 "7\ncould not reach " ++ host ++ " port " ++ U32.show(port) ++ ": "
369 ++ wire.cause(n)
370 case Handshake{}:
371 "35\nthe TLS handshake with " ++ host ++ " failed: " ++ wire.cause(n)
372 ++ ": " ++ why
373 case Send{}:
374 "55\nthe request to " ++ host ++ " could not be sent: " ++ wire.cause(n)
375 case Receive{}:
376 "56\nthe answer from " ++ host ++ " was cut short: " ++ wire.cause(n)
377
378# a failure once it is known whether it ran out of time
379def wire.fail.of(p: Phase, host: String, +port: U32, +ms: U32, +n: U32,
380 why: String, late: Bool) -> String:
381 match late:
382 case True{}:
383 wire.fail.late(p, host, port, ms, n)
384 case False{}:
385 wire.fail.other(p, host, port, n, why)
386
387# the exchange's answer when a call in this phase failed with error number n
388# and reason why, with deadline ms (SPEC.md HTTP-CLI-13)
389def wire.fail(p: Phase, host: String, +port: U32, +ms: U32, +n: U32,
390 why: String) -> String:
391 wire.fail.of(p, host, port, ms, n, why, U32.is_eq(n, wire.etimedout()))