src/wirespec.bend
emerging-ezhttp@0.18.0.0 · 447 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.18.0.0/src/http.bend as Http
11import emerging-ezhttp@0.18.0.0/src/url.bend as Url
12import emerging-ezhttp@0.18.0.0/src/body.bend as Body
13import emerging-ezhttp@0.18.0.0/src/pct.bend as Pct
14import emerging-ezhttp@0.18.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 as the tail (wire.tail)
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 this body to a URL that came apart: text inside the request
119# 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.Body) -> Exchange:
122 match b:
123 case Body.Empty{}:
124 wire.exchange(method, l, headers, "")
125 case Body.Plain{text}:
126 wire.exchange(method, l, headers, text)
127 case Body.Octets{bytes}:
128 wire.exchange.octets(method, l, headers, List.length(&2, U32, bytes))
129
130# the octets sent after the request text: an octet body's, else none
131def wire.tail(b: Body.Body) -> List<&2, U32>:
132 match b:
133 case Body.Empty{}:
134 []
135 case Body.Plain{text}:
136 []
137 case Body.Octets{bytes}:
138 bytes
139
140# --- what is heard ---
141
142# an answer's status: the number on its first line, if it is one
143def wire.code.of(c: Http.Cut, raw: String) -> Maybe<&2, U32>:
144 match c:
145 case Http.NoCut{}:
146 U32.read(raw)
147 case Http.Cut{before, after}:
148 U32.read(before)
149
150# an answer's status line as a number
151def wire.code(+raw: String) -> Maybe<&2, U32>:
152 wire.code.of(Http.divide(raw, "\n"), raw)
153
154# the text after an answer's first newline
155def wire.text.of(c: Http.Cut) -> String:
156 match c:
157 case Http.NoCut{}:
158 ""
159 case Http.Cut{before, after}:
160 after
161
162# the text after an answer's first newline
163def wire.text(raw: String) -> String:
164 wire.text.of(Http.divide(raw, "\n"))
165
166# whether a status is success (0)
167def wire.ok.of(m: Maybe<&2, U32>) -> Bool:
168 match m:
169 case None{}:
170 False{}
171 case Some{n}:
172 U32.is_eq(n, 0)
173
174# whether an answer has status 0
175def wire.ok(raw: String) -> Bool:
176 wire.ok.of(wire.code(raw))
177
178# what has been received so far: its pieces, the newest first, and where
179# the response stands (Http.hear)
180type Got is Data:
181 Got{pieces: List<&2, String>, hear: Http.Hear}
182
183# the text a list of pieces, newest first, stands for
184def wire.joined(ps: List<&2, String>) -> String:
185 match ps:
186 case []:
187 ""
188 case p <> rest:
189 wire.joined(rest) ++ p
190
191# the pieces put together onto what follows them, each copied once
192def wire.join.go(ps: List<&2, String>, acc: String) -> String:
193 match ps:
194 case []:
195 acc
196 case p <> rest:
197 wire.join.go(rest, p ++ acc)
198
199# the text a list of pieces, newest first, stands for, built in one pass
200def wire.join(ps: List<&2, String>) -> String:
201 wire.join.go(ps, "")
202
203# what has been received as these pieces, for a request with this method
204def wire.got(+method: String, +ps: List<&2, String>) -> Got:
205 Got{ps, Http.hear.of(method, wire.joined(ps))}
206
207# after a read: read again with what has arrived, or answer
208type Read is Data:
209 Again{acc: Got}
210 Heard{answer: String}
211
212# everything received, once it is known whether it is a whole response
213def wire.read.whole(+ps: List<&2, String>, h: Http.Hear, done: Bool) -> Read:
214 match done:
215 case True{}:
216 Heard{"0\n" ++ wire.join(ps)}
217 case False{}:
218 Again{Got{ps, h}}
219
220# a read that brought text, judged with where the response now stands
221def wire.read.add(text: String, ps: List<&2, String>, +h: Http.Hear) -> Read:
222 wire.read.whole(text <> ps, h, Http.hear.done(h))
223
224# a read that brought text, or found the connection closed
225def wire.read.got(st: Got, +text: String, closed: Bool) -> Read:
226 match st closed:
227 case Got{ps, h} True{}:
228 Heard{"0\n" ++ wire.join(ps)}
229 case Got{ps, h} False{}:
230 wire.read.add(text, ps, Http.hear.more(h, text))
231
232# a read's answer once it is known whether it succeeded
233def wire.read.of(st: Got, +got: String, ok: Bool) -> Read:
234 match ok:
235 case False{}:
236 Heard{got}
237 case True{}:
238 +text = wire.text(got)
239 wire.read.got(st, text, String.is_empty(text))
240
241# what to do after a read answered `got`, with what was received before it
242# (SPEC.md HTTP-CLI-6)
243def wire.read.next(st: Got, +got: String) -> Read:
244 wire.read.of(st, got, wire.ok(got))
245
246# the answer when the reads run out before the response ends
247def wire.spent() -> String:
248 "56\nthe answer did not end within 65536 reads"
249
250# the response an exchange's answer holds, read by the request's method
251# (SPEC.md HTTP-CLI-9); a failed exchange is torn with the reason it is
252# reported with (wire.why)
253def wire.heard.of(+method: String, +raw: String, ok: Bool) -> Http.Reply:
254 match ok:
255 case False{}:
256 Http.Torn{wire.why(wire.code(raw), wire.text(raw))}
257 case True{}:
258 Http.parse.to(method, wire.text(raw))
259
260# the reason phrase of the response an exchange's answer holds (SPEC.md
261# HTTP-CLI-11); a failed exchange's is read from its reason and not used
262def wire.phrase(raw: String) -> String:
263 Http.phrase.to(wire.text(raw))
264
265# the response an exchange's answer holds
266def wire.heard(+method: String, +raw: String) -> Http.Reply:
267 wire.heard.of(method, raw, wire.ok(raw))
268
269# --- what goes on the wire (SPEC.md HTTP-CLI-10) ---
270
271# a request text's UTF-8 octets, one character each, onto the octets after it
272def wire.payload.text(s: String, rest: String) -> String:
273 match s:
274 case SNil{}:
275 rest
276 case SCon{Chr{+cp}, t}:
277 Body.octets.chars(Pct.utf8(cp)) ++ wire.payload.text(t, rest)
278
279# the octets an exchange sends, one character each: the request text as
280# UTF-8, then the body's tail
281def wire.payload(req: String, tail: List<&2, U32>) -> String:
282 wire.payload.text(req, Body.octets.chars(tail))
283
284# --- what a failed socket call is reported as (SPEC.md HTTP-CLI-13, 14) ---
285
286# where in an exchange a call failed
287type Phase is Data:
288 Resolve{}
289 Connect{}
290 Handshake{}
291 Send{}
292 Receive{}
293
294# the error number a call that ran out of time fails with (Linux ETIMEDOUT)
295def wire.etimedout() -> U32:
296 110
297
298# the Linux errno symbols this table names
299def wire.errnos() -> List<&2, Http.Phrase>:
300 [Http.P{1, "EPERM"}, Http.P{2, "ENOENT"}, Http.P{4, "EINTR"},
301 Http.P{5, "EIO"}, Http.P{9, "EBADF"}, Http.P{11, "EAGAIN"},
302 Http.P{12, "ENOMEM"}, Http.P{13, "EACCES"}, Http.P{22, "EINVAL"},
303 Http.P{23, "ENFILE"}, Http.P{24, "EMFILE"}, Http.P{32, "EPIPE"},
304 Http.P{71, "EPROTO"}, Http.P{88, "ENOTSOCK"},
305 Http.P{93, "EPROTONOSUPPORT"}, Http.P{97, "EAFNOSUPPORT"},
306 Http.P{98, "EADDRINUSE"}, Http.P{99, "EADDRNOTAVAIL"},
307 Http.P{100, "ENETDOWN"}, Http.P{101, "ENETUNREACH"},
308 Http.P{103, "ECONNABORTED"}, Http.P{104, "ECONNRESET"},
309 Http.P{105, "ENOBUFS"}, Http.P{106, "EISCONN"},
310 Http.P{107, "ENOTCONN"}, Http.P{110, "ETIMEDOUT"},
311 Http.P{111, "ECONNREFUSED"}, Http.P{112, "EHOSTDOWN"},
312 Http.P{113, "EHOSTUNREACH"}, Http.P{114, "EALREADY"},
313 Http.P{115, "EINPROGRESS"}]
314
315# a name from the table, or `errno` when it has none
316def wire.errno.or(name: String) -> String:
317 match name:
318 case SNil{}:
319 "errno"
320 case SCon{h, t}:
321 SCon{h, t}
322
323# an error number's name (SPEC.md HTTP-CLI-14)
324def wire.errno.name(+n: U32) -> String:
325 wire.errno.or(Http.reason.in(wire.errnos(), n))
326
327# an error number as a reason names it: `<name> (<n>)`
328def wire.cause(+n: U32) -> String:
329 wire.errno.name(n) ++ " (" ++ U32.show(n) ++ ")"
330
331# a call that ran out of time, by its phase
332def wire.fail.late(p: Phase, host: String, +port: U32, +ms: U32, +n: U32)
333 -> String:
334 match p:
335 case Resolve{}:
336 "6\ncould not resolve " ++ host ++ ": " ++ wire.cause(n)
337 case Connect{}:
338 "28\nconnecting to " ++ host ++ " port " ++ U32.show(port)
339 ++ " took over " ++ U32.show(ms) ++ " ms"
340 case Handshake{}:
341 "28\nthe TLS handshake with " ++ host ++ " took over " ++ U32.show(ms)
342 ++ " ms"
343 case Send{}:
344 "28\nsending the request to " ++ host ++ " took over " ++ U32.show(ms)
345 ++ " ms"
346 case Receive{}:
347 "28\n" ++ host ++ " sent nothing for " ++ U32.show(ms) ++ " ms"
348
349# a call that failed for another reason, by its phase
350def wire.fail.other(p: Phase, host: String, +port: U32, +n: U32, why: String)
351 -> String:
352 match p:
353 case Resolve{}:
354 "6\ncould not resolve " ++ host ++ ": " ++ wire.cause(n)
355 case Connect{}:
356 "7\ncould not reach " ++ host ++ " port " ++ U32.show(port) ++ ": "
357 ++ wire.cause(n)
358 case Handshake{}:
359 "35\nthe TLS handshake with " ++ host ++ " failed: " ++ wire.cause(n)
360 ++ ": " ++ why
361 case Send{}:
362 "55\nthe request to " ++ host ++ " could not be sent: " ++ wire.cause(n)
363 case Receive{}:
364 "56\nthe answer from " ++ host ++ " was cut short: " ++ wire.cause(n)
365
366# a failure once it is known whether it ran out of time
367def wire.fail.of(p: Phase, host: String, +port: U32, +ms: U32, +n: U32,
368 why: String, late: Bool) -> String:
369 match late:
370 case True{}:
371 wire.fail.late(p, host, port, ms, n)
372 case False{}:
373 wire.fail.other(p, host, port, n, why)
374
375# the exchange's answer when a call in this phase failed with error number n
376# and reason why, with deadline ms (SPEC.md HTTP-CLI-13)
377def wire.fail(p: Phase, host: String, +port: U32, +ms: U32, +n: U32,
378 why: String) -> String:
379 wire.fail.of(p, host, port, ms, n, why, U32.is_eq(n, wire.etimedout()))
380
381# --- received octets as text (SPEC.md HTTP-TRUST-5) ---
382
383# how many continuation octets a lead octet asks for (RFC 3629 §3); 0 for an
384# octet that opens no sequence
385def wire.utf8.wants(+b: U32) -> Nat:
386 Bool.pick(Nat, U32.is_lt(b, 194), 0n,
387 Bool.pick(Nat, U32.is_lt(b, 224), 1n,
388 Bool.pick(Nat, U32.is_lt(b, 240), 2n,
389 Bool.pick(Nat, U32.is_lt(b, 245), 3n, 0n))))
390
391# whether an octet continues a sequence (10xxxxxx)
392def wire.utf8.cont(+b: U32) -> Bool:
393 Bool.and(U32.is_le(128, b), U32.is_lt(b, 192))
394
395# the octet before k continuation octets: hold the k + 1 when it opens a
396# sequence that wants more than k
397def wire.utf8.lead(+b: U32, +k: Nat) -> Nat:
398 Bool.pick(Nat, Nat.is_lt(k, wire.utf8.wants(b)), 1n+k, 0n)
399
400# one octet from the end: another continuation octet, or the one before them
401def wire.utf8.back(+b: U32, +k: Nat, more: Bool, rest: Unit -> Nat) -> Nat:
402 match more:
403 case True{}:
404 rest(Unit{})
405 case False{}:
406 wire.utf8.lead(b, k)
407
408# how many octets at the end of a list, given newest first, are a sequence
409# still waiting for octets; k continuation octets have been passed
410def wire.utf8.open(r: List<&2, U32>, +k: Nat) -> Nat:
411 match r:
412 case []:
413 0n
414 case +b <> t:
415 wire.utf8.back(b, k, Bool.and(wire.utf8.cont(b), Nat.is_lt(k, 3n)),
416 _u => wire.utf8.open(t, 1n+k))
417
418# octets as the pieces Qs.utf.dec reads
419def wire.utf8.toks(bs: List<&2, U32>) -> List<&2, Qs.Tok>:
420 match bs:
421 case []:
422 []
423 case b <> t:
424 Qs.B{b} <> wire.utf8.toks(t)
425
426# octets, one character each, as a list
427def wire.utf8.bytes(s: String) -> List<&2, U32>:
428 match s:
429 case SNil{}:
430 []
431 case SCon{c, t}:
432 Char.to_u32(c) <> wire.utf8.bytes(t)
433
434# the octets held from before and a receive's octets: the text of all but a
435# sequence still open at the end, and that sequence, held for the next
436def wire.utf8.feed(held: List<&2, U32>, got: String)
437 -> String & List<&2, U32>:
438 +bs = List.append(&2, U32, held, wire.utf8.bytes(got))
439 +n = List.length(&2, U32, bs)
440 +m = wire.utf8.open(List.reverse(&2, U32, bs), 0n)
441 +k = Nat.sub(n, m)
442 (Qs.utf.dec(wire.utf8.toks(List.take(&2, U32, bs, k)), Qs.Idle{}),
443 List.drop(&2, U32, bs, k))
444
445# what was held once the server has closed: decoded as it is
446def wire.utf8.flush(held: List<&2, U32>) -> String:
447 Qs.utf.dec(wire.utf8.toks(held), Qs.Idle{})