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. 9 import Base 10 import ./http.bend as Http 11 import ./url.bend as Url 12 import ./body.bend as Body 13 import ./pct.bend as Pct 14 import ./qs.bend as Qs 15 16 # --- the deadline --- 17 18 # the deadline of an exchange with no timeout: 60 s, in milliseconds 19 def wire.ms.dflt() -> U32: 20 60000 21 22 # a timeout once it is known whether it is 0 23 def 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 32 def 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) 37 def 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) 48 def 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 53 def 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 61 def 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 69 def 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) 77 type 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 82 def 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 89 def 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 97 def 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) 108 def 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) 120 def 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 131 def 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 143 def 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 151 def 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 155 def 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 163 def wire.text(raw: String) -> String: 164 wire.text.of(Http.divide(raw, "\n")) 165 166 # whether a status is success (0) 167 def 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 175 def 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) 180 type Got is Data: 181 Got{pieces: List<&2, String>, hear: Http.Hear} 182 183 # the text a list of pieces, newest first, stands for 184 def 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 192 def 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 200 def 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 204 def 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 208 type 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 213 def 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 221 def 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 225 def 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 233 def 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) 243 def 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 247 def 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) 253 def 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 262 def wire.phrase(raw: String) -> String: 263 Http.phrase.to(wire.text(raw)) 264 265 # the response an exchange's answer holds 266 def 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 272 def 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 281 def 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 287 type 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) 295 def wire.etimedout() -> U32: 296 110 297 298 # the Linux errno symbols this table names 299 def 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 316 def 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) 324 def 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: ` ()` 328 def 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 332 def 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 350 def 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 367 def 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) 377 def 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 385 def 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) 392 def 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 397 def 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 401 def 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 410 def 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 419 def 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 427 def 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 436 def 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 446 def wire.utf8.flush(held: List<&2, U32>) -> String: 447 Qs.utf.dec(wire.utf8.toks(held), Qs.Idle{})