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. 10 import Base 11 import ./http.bend as Http 12 import ./url.bend as Url 13 import ./body.bend as Body 14 import ./pct.bend as Pct 15 import ./qs.bend as Qs 16 17 # --- the deadline --- 18 19 # the deadline of an exchange with no timeout: 60 s, in milliseconds 20 def wire.ms.dflt() -> U32: 21 60000 22 23 # a timeout once it is known whether it is 0 24 def 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 33 def 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) 38 def 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) 49 def 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 54 def 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 62 def 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 70 def 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) 78 type 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 83 def 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 90 def 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 98 def 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 109 def 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) 121 def 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 132 def 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 140 def 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 144 def 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 152 def wire.text(raw: String) -> String: 153 wire.text.of(Http.divide(raw, "\n")) 154 155 # whether a status is success (0) 156 def 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 164 def wire.ok(raw: String) -> Bool: 165 wire.ok.of(wire.code(raw)) 166 167 # the text a list of pieces, newest first, stands for 168 def 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 176 def 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 184 def 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 189 def 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 194 type Read is Data: 195 Again{hear: Http.Hear} 196 Heard{} 197 198 # where the response stands after a read, judged 199 def 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 207 def 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 211 def 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) 220 def 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 224 def 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 232 def 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) 242 def 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 246 def 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) 250 def 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) 256 def 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 265 def wire.phrase(raw: String) -> String: 266 Http.phrase.to(wire.text(raw)) 267 268 # the response an exchange's answer holds 269 def 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 275 def 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) 284 def 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 290 type 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) 298 def wire.etimedout() -> U32: 299 110 300 301 # the Linux errno symbols this table names 302 def 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 319 def 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) 327 def 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: ` ()` 331 def 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 336 def 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 344 def 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 362 def 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 379 def 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) 389 def 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()))