1 # ezhttp/src/wirespec: the text the wire effect reads, and what its answer 2 # means, pure. Kept apart from wire.bend (the effect) so the proof gate can 3 # import it. What the client sends for a URL (wire.exchange) and when it has 4 # heard a whole answer (wire.read.next) are decided here; wire.bend and 5 # client.bend act on them. 6 # 7 # Spec: scheme, host, port each on their own line; everything after the third 8 # newline is the request verbatim. The scheme line may carry a timeout after a 9 # space: 32 binary digits, least significant first, in milliseconds. A scheme 10 # line with no timeout means 60000 ms. SPEC.md HTTP-CLI lists what is 11 # guaranteed. 12 import Base 13 import ./http.bend as Http 14 import ./url.bend as Url 15 import ./body.bend as Body 16 17 # the word the effect reads for a scheme that wants TLS 18 def wire.scheme(secure: Bool) -> String: 19 match secure: 20 case True{}: 21 "tls" 22 case False{}: 23 "tcp" 24 25 # the spec the effect reads 26 def wire.spec(secure: Bool, host: String, port: U32, req: String) -> String: 27 wire.scheme(secure) ++ "\n" ++ host ++ "\n" ++ U32.show(port) ++ "\n" ++ req 28 29 # --- the timeout --- 30 31 # the timeout a spec with none carries: 60 s, in milliseconds 32 def wire.ms.dflt() -> U32: 33 60000 34 35 # one bit as a binary digit 36 def wire.bit(b: Bool) -> Char: 37 match b: 38 case True{}: 39 '1' 40 case False{}: 41 '0' 42 43 # a word as binary digits, least significant first 44 def wire.bits(n: Nat, w: Word(n)) -> String: 45 match n: 46 case 0n: 47 SNil{} 48 case 1n+p: 49 match w: 50 case WCon{b, t}: 51 SCon{wire.bit(b), wire.bits(p, t)} 52 53 # binary digits, least significant first, as a word; a missing digit is 0 54 def wire.bits.read(n: Nat, s: String) -> Word(n): 55 match n: 56 case 0n: 57 WNil{} 58 case 1n+p: 59 match s: 60 case SNil{}: 61 WCon{False{}, wire.bits.read(p, SNil{})} 62 case SCon{c, t}: 63 WCon{Char.is_eq(c, '1'), wire.bits.read(p, t)} 64 65 # a timeout as the scheme line carries it 66 def wire.ms.text(ms: U32) -> String: 67 match ms: 68 case U32{w}: 69 wire.bits(32n, w) 70 71 # the first line of a timed spec: the scheme, a space, the timeout 72 def wire.head(secure: Bool, ms: U32) -> String: 73 wire.scheme(secure) ++ " " ++ wire.ms.text(ms) 74 75 # the lines after the first: host, port, then the request verbatim 76 def wire.rest(host: String, port: U32, req: String) -> String: 77 host ++ "\n" ++ U32.show(port) ++ "\n" ++ req 78 79 # the spec the effect reads, with a timeout in milliseconds 80 def wire.spec.timed(secure: Bool, ms: U32, host: String, port: U32, 81 req: String) -> String: 82 wire.head(secure, ms) ++ "\n" ++ wire.rest(host, port, req) 83 84 # the timeout after the scheme word, or the default when there is none 85 def wire.ms.words(ws: List<&2, String>) -> U32: 86 match ws: 87 case []: 88 wire.ms.dflt() 89 case _ <> []: 90 wire.ms.dflt() 91 case _ <> (bits <> _): 92 U32{wire.bits.read(32n, bits)} 93 94 # the first line of a spec 95 def wire.line(ls: List<&2, String>) -> String: 96 match ls: 97 case []: 98 "" 99 case l <> _: 100 l 101 102 # the timeout the effect reads from a spec, in milliseconds 103 def wire.ms(spec: String) -> U32: 104 wire.ms.words(String.split(wire.line(String.split(spec, '\n')), ' ')) 105 106 # --- the answer --- 107 108 # the wire status for an exchange that ran out of time (curl's 109 # CURLE_OPERATION_TIMEDOUT) 110 def wire.late() -> U32: 111 28 112 113 # what a failed exchange is reported as: a timeout is marked, any other 114 # failure's reason is kept as it is 115 def wire.why.of(why: String, late: Bool) -> String: 116 match late: 117 case True{}: 118 "timed out: " ++ why 119 case False{}: 120 why 121 122 # a failed exchange's status and reason as the reason the client reports 123 def wire.why(code: Maybe<&2, U32>, why: String) -> String: 124 match code: 125 case None{}: 126 why 127 case Some{n}: 128 wire.why.of(why, U32.is_eq(n, wire.late())) 129 130 # whether a reported reason is a timeout 131 def wire.timed_out(why: String) -> Bool: 132 String.starts_with(why, "timed out: ") 133 134 # --- what is sent --- 135 136 # what a request to a URL becomes: nothing when the URL did not parse, else 137 # the scheme (secure or not), host, port, method and request text the effect 138 # is given; the answer is read by that method (wire.read.next) 139 type Exchange is Data: 140 NoUrl{why: String} 141 Exchange{secure: Bool, host: String, port: U32, method: String, req: String} 142 143 # the exchange once it is known whether the scheme wants TLS 144 def wire.exchange.at(+method: String, +secure: Bool, +host: String, 145 +port: U32, path: String, headers: List<&2, Http.Header>, body: String) 146 -> Exchange: 147 Exchange{secure, host, port, method, 148 Http.request.at(method, secure, host, port, path, headers, body)} 149 150 # the method an exchange is sent and read by, none when nothing is sent 151 def wire.exchange.method(ex: Exchange) -> Maybe<&2, String>: 152 match ex: 153 case NoUrl{why}: 154 None{} 155 case Exchange{secure, host, port, method, req}: 156 Some{method} 157 158 # a request with this method, headers and body to a URL that came apart 159 def wire.exchange(method: String, l: Url.Loc, headers: List<&2, Http.Header>, 160 body: String) -> Exchange: 161 match l: 162 case Url.Bad{why}: 163 NoUrl{why} 164 case Url.Loc{scheme, host, port, path}: 165 +secure = String.eq(scheme, "https") 166 wire.exchange.at(method, secure, host, port, path, headers, body) 167 168 # a request with n octets of body to a URL that came apart: the request text 169 # ends at the blank line, and the octets go after it as the tail (wire.tail) 170 def wire.exchange.octets(+method: String, l: Url.Loc, 171 headers: List<&2, Http.Header>, n: Nat) -> Exchange: 172 match l: 173 case Url.Bad{why}: 174 NoUrl{why} 175 case Url.Loc{scheme, +host, +port, path}: 176 +secure = String.eq(scheme, "https") 177 Exchange{secure, host, port, method, 178 Http.request.head.at(method, secure, host, port, path, headers, n)} 179 180 # a request with this body to a URL that came apart: text inside the request 181 # text as UTF-8, octets after it (SPEC.md HTTP-CLI-10) 182 def wire.exchange.body(method: String, l: Url.Loc, 183 headers: List<&2, Http.Header>, b: Body.Body) -> Exchange: 184 match b: 185 case Body.Empty{}: 186 wire.exchange(method, l, headers, "") 187 case Body.Plain{text}: 188 wire.exchange(method, l, headers, text) 189 case Body.Octets{bytes}: 190 wire.exchange.octets(method, l, headers, List.length(&2, U32, bytes)) 191 192 # the octets sent after the request text: an octet body's, else none 193 def wire.tail(b: Body.Body) -> List<&2, U32>: 194 match b: 195 case Body.Empty{}: 196 [] 197 case Body.Plain{text}: 198 [] 199 case Body.Octets{bytes}: 200 bytes 201 202 # --- what is heard --- 203 204 # an answer's status: the number on its first line, if it is one 205 def wire.code.of(c: Http.Cut, raw: String) -> Maybe<&2, U32>: 206 match c: 207 case Http.NoCut{}: 208 U32.read(raw) 209 case Http.Cut{before, after}: 210 U32.read(before) 211 212 # an answer's status line as a number 213 def wire.code(+raw: String) -> Maybe<&2, U32>: 214 wire.code.of(Http.divide(raw, "\n"), raw) 215 216 # the text after an answer's first newline 217 def wire.text.of(c: Http.Cut) -> String: 218 match c: 219 case Http.NoCut{}: 220 "" 221 case Http.Cut{before, after}: 222 after 223 224 # the text after an answer's first newline 225 def wire.text(raw: String) -> String: 226 wire.text.of(Http.divide(raw, "\n")) 227 228 # whether a status is success (0) 229 def wire.ok.of(m: Maybe<&2, U32>) -> Bool: 230 match m: 231 case None{}: 232 False{} 233 case Some{n}: 234 U32.is_eq(n, 0) 235 236 # whether an answer has status 0 237 def wire.ok(raw: String) -> Bool: 238 wire.ok.of(wire.code(raw)) 239 240 # what an open answered: a connection to read from, or the answer itself 241 type Opened is Data: 242 Refused{answer: String} 243 Open{conn: U32} 244 245 # a connection number that read, or a malformed answer when it did not 246 def wire.opened.conn(m: Maybe<&2, U32>) -> Opened: 247 match m: 248 case None{}: 249 Refused{"22\na malformed connection number"} 250 case Some{n}: 251 Open{n} 252 253 # an open's answer once it is known whether it succeeded 254 def wire.opened.of(+got: String, ok: Bool) -> Opened: 255 match ok: 256 case False{}: 257 Refused{got} 258 case True{}: 259 wire.opened.conn(U32.read(wire.text(got))) 260 261 # what an open's answer means 262 def wire.opened(+got: String) -> Opened: 263 wire.opened.of(got, wire.ok(got)) 264 265 # what has been received so far: its pieces, the newest first, and where 266 # the response stands (Http.hear) 267 type Got is Data: 268 Got{pieces: List<&2, String>, hear: Http.Hear} 269 270 # the text a list of pieces, newest first, stands for 271 def wire.joined(ps: List<&2, String>) -> String: 272 match ps: 273 case []: 274 "" 275 case p <> rest: 276 wire.joined(rest) ++ p 277 278 # the pieces put together onto what follows them, each copied once 279 def wire.join.go(ps: List<&2, String>, acc: String) -> String: 280 match ps: 281 case []: 282 acc 283 case p <> rest: 284 wire.join.go(rest, p ++ acc) 285 286 # the text a list of pieces, newest first, stands for, built in one pass 287 def wire.join(ps: List<&2, String>) -> String: 288 wire.join.go(ps, "") 289 290 # what has been received as these pieces, for a request with this method 291 def wire.got(+method: String, +ps: List<&2, String>) -> Got: 292 Got{ps, Http.hear.of(method, wire.joined(ps))} 293 294 # after a read: read again with what has arrived, or answer 295 type Read is Data: 296 Again{acc: Got} 297 Heard{answer: String} 298 299 # everything received, once it is known whether it is a whole response 300 def wire.read.whole(+ps: List<&2, String>, h: Http.Hear, done: Bool) -> Read: 301 match done: 302 case True{}: 303 Heard{"0\n" ++ wire.join(ps)} 304 case False{}: 305 Again{Got{ps, h}} 306 307 # a read that brought text, judged with where the response now stands 308 def wire.read.add(text: String, ps: List<&2, String>, +h: Http.Hear) -> Read: 309 wire.read.whole(text <> ps, h, Http.hear.done(h)) 310 311 # a read that brought text, or found the connection closed 312 def wire.read.got(st: Got, +text: String, closed: Bool) -> Read: 313 match st closed: 314 case Got{ps, h} True{}: 315 Heard{"0\n" ++ wire.join(ps)} 316 case Got{ps, h} False{}: 317 wire.read.add(text, ps, Http.hear.more(h, text)) 318 319 # a read's answer once it is known whether it succeeded 320 def wire.read.of(st: Got, +got: String, ok: Bool) -> Read: 321 match ok: 322 case False{}: 323 Heard{got} 324 case True{}: 325 +text = wire.text(got) 326 wire.read.got(st, text, String.is_empty(text)) 327 328 # what to do after a read answered `got`, with what was received before it 329 # (SPEC.md HTTP-CLI-6) 330 def wire.read.next(st: Got, +got: String) -> Read: 331 wire.read.of(st, got, wire.ok(got)) 332 333 # the answer when the reads run out before the response ends 334 def wire.spent() -> String: 335 "56\nthe answer did not end within 65536 reads" 336 337 # the response an exchange's answer holds, read by the request's method 338 # (SPEC.md HTTP-CLI-9); a failed exchange is torn with the reason it is 339 # reported with (wire.why) 340 def wire.heard.of(+method: String, +raw: String, ok: Bool) -> Http.Reply: 341 match ok: 342 case False{}: 343 Http.Torn{wire.why(wire.code(raw), wire.text(raw))} 344 case True{}: 345 Http.parse.to(method, wire.text(raw)) 346 347 # the reason phrase of the response an exchange's answer holds (SPEC.md 348 # HTTP-CLI-11); a failed exchange's is read from its reason and not used 349 def wire.phrase(raw: String) -> String: 350 Http.phrase.to(wire.text(raw)) 351 352 # the response an exchange's answer holds 353 def wire.heard(+method: String, +raw: String) -> Http.Reply: 354 wire.heard.of(method, raw, wire.ok(raw))