src/wirespec.bend

emerging-ezhttp@0.21.0.0 · 391 lines · 50 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()))