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