websocket.bend
bend-kit-websocket@0.1.0.0 · 961 lines · 0 definitions
1# RFC 6455 WebSocket client: opening handshake, frames over packed Bytes, and messages over Wire. Source: https://github.com/paymog/bend-kit/tree/main/websocket
2import Base
3import bend-kit-bytes@0.3.1.0/bytes.bend as Bytes
4import bend-kit-crypto@0.1.0.0/crypto.bend as Crypto
5import bend-kit-wire@0.4.2.0/wire.bend as Wire
6
7# Errors are (code, why). A code of 1000 or more is the RFC 6455 §7.4 close code the
8# peer broke (1002 protocol, 1006 closed early, 1007 bad UTF-8, 1009 too big, 1011 budget);
9# a smaller code is the errno of a socket or crypto effect.
10# Opcodes (§5.2): 0 continuation, 1 text, 2 binary, 8 close, 9 ping, 10 pong.
11
12# Opening handshake (§4.1, §4.2.2).
13
14def guid() -> String:
15 "258EAFA5-E914-47DA-95CA-C5AB0DC85B11"
16
17# The octets SHA-1 hashes for Sec-WebSocket-Accept: the key, then the GUID.
18def accept.input(key: String) -> Bytes.Bytes:
19 Bytes.from_string(key ++ guid())
20
21# Sec-WebSocket-Accept from the SHA-1 digest of accept.input(key).
22def accept.of(digest: Bytes.Bytes) -> String:
23 Bytes.to_base64(digest)
24
25def accept.fin(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Result<&1, &1, U32 & String, String>:
26 match r:
27 case Fail{e}:
28 Fail{e}
29 case Done{(len, buf)}:
30 Done{accept.of(Bytes.Bytes{len, buf})}
31
32def accept.words(b: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>):
33 Bytes.Bytes{len, buf} = b
34 Crypto.sha1.words(len, buf)
35
36# The Sec-WebSocket-Accept a server must answer to key.
37def accept(key: String) -> IO(Result<&1, &1, U32 & String, String>):
38 do IO<Result<&1, &1, U32 & String, String>>:
39 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- accept.words(accept.input(key))
40 return accept.fin(r)
41
42# Sec-WebSocket-Key from a 16-octet nonce.
43def key.of(nonce: Bytes.Bytes) -> String:
44 Bytes.to_base64(nonce)
45
46def key.fin(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Result<&1, &1, U32 & String, String>:
47 match r:
48 case Fail{e}:
49 Fail{e}
50 case Done{(len, buf)}:
51 Done{key.of(Bytes.Bytes{len, buf})}
52
53# A fresh key from 16 octets of the OS secure random source.
54def key() -> IO(Result<&1, &1, U32 & String, String>):
55 do IO<Result<&1, &1, U32 & String, String>>:
56 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.random.words(16)
57 return key.fin(r)
58
59def first(m: Maybe<&1, U32 & String>, n: Maybe<&1, U32 & String>) -> Maybe<&1, U32 & String>:
60 match m:
61 case Some{e}:
62 Some{e}
63 case None{}:
64 n
65
66def reject(bad: Bool, +code: U32, +why: String) -> Maybe<&1, U32 & String>:
67 match bad:
68 case True{}:
69 Some{(code, why)}
70 case False{}:
71 None{}
72
73def verdict(-A: Type, m: Maybe<&1, U32 & String>, v: A) -> Result<&1, &1, U32 & String, A>:
74 match m:
75 case Some{e}:
76 Fail{e}
77 case None{}:
78 Done{v}
79
80# Every char is visible ASCII (0x21-0x7E): no space, CR, LF, or other control.
81def visible(s: String) -> Bool:
82 match s:
83 case SNil{}:
84 True{}
85 case SCon{Chr{+c}, t}:
86 Bool.and(Bool.and(U32.is_ge(c, 33), U32.is_le(c, 126)), visible(t))
87
88# The GET that asks to upgrade. host is the Host header (with :port when not the default);
89# path is the origin-form target ("/" and on, percent-encoded). A char outside visible
90# ASCII could split the head and inject headers, so it fails with EINVAL (22).
91def request(+host: String, +path: String, +key: String) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
92 verdict(Bytes.Bytes,
93 first(reject(Bool.or(String.is_empty(host), Bool.not(visible(host))), 22, "host is not visible ASCII"),
94 first(reject(Bool.or(Bool.not(String.starts_with(path, "/")), Bool.not(visible(path))), 22, "path is not an origin-form target"),
95 reject(Bool.or(String.is_empty(key), Bool.not(visible(key))), 22, "key is not visible ASCII"))),
96 Bytes.from_string("GET " ++ path ++ " HTTP/1.1\r\nHost: " ++ host
97 ++ "\r\nUpgrade: websocket\r\nConnection: Upgrade\r\nSec-WebSocket-Key: " ++ key
98 ++ "\r\nSec-WebSocket-Version: 13\r\n\r\n"))
99
100def fields.line(parts: List<&2, String>, +name: String, +later: List<&2, String>) -> List<&2, String>:
101 match parts:
102 case Nil{}:
103 later
104 case Con{k, v}:
105 Bool.pick(List<&2, String>, String.eq(String.to_lower(k), name),
106 Con{String.trim(String.join(v, ":")), later}, later)
107
108def fields.go(ls: List<&2, String>, +name: String) -> List<&2, String>:
109 match ls:
110 case Nil{}:
111 Nil{}
112 case Con{h, t}:
113 fields.line(String.split(String.trim_end(h), ':'), name, fields.go(t, name))
114
115def after.first(ls: List<&2, String>) -> List<&2, String>:
116 match ls:
117 case Nil{}:
118 Nil{}
119 case Con{h, t}:
120 t
121
122# The header lines of an HTTP head: every line after the start line.
123def headers(head: String) -> List<&2, String>:
124 after.first(String.split(head, '\n'))
125
126# The trimmed values of every header line named name (lowercase), in order.
127def fields(head: String, +name: String) -> List<&2, String>:
128 fields.go(headers(head), name)
129
130def only(xs: List<&2, String>) -> Maybe<&2, String>:
131 match xs:
132 case Con{v, Nil{}}:
133 Some{v}
134 case _:
135 None{}
136
137# The value of the header named name when exactly one line has it.
138def field(head: String, +name: String) -> Maybe<&2, String>:
139 only(fields(head, name))
140
141# A header line is name ":" value, with a non-empty name that holds no space or tab
142# (RFC 9112 §5.1). That rules out obsolete line folding and bare text.
143def line.parts(parts: List<&2, String>) -> Bool:
144 match parts:
145 case Con{+k, Con{v, rest}}:
146 Bool.and(Bool.not(String.is_empty(k)), Bool.not(Bool.or(String.contains(k, " "), String.contains(k, "\t"))))
147 case _:
148 False{}
149
150def lines.ok(ls: List<&2, String>) -> Bool:
151 match ls:
152 case Nil{}:
153 True{}
154 case Con{h, t}:
155 Bool.and(line.parts(String.split(String.trim_end(h), ':')), lines.ok(t))
156
157def status.parts(parts: List<&2, String>) -> Bool:
158 match parts:
159 case Con{v, Con{code, rest}}:
160 Bool.and(String.eq(v, "HTTP/1.1"), String.eq(code, "101"))
161 case _:
162 False{}
163
164# The first line is exactly "HTTP/1.1 101" and a reason, with nothing before it.
165def status(ls: List<&2, String>) -> Bool:
166 match ls:
167 case Nil{}:
168 False{}
169 case Con{l, t}:
170 status.parts(String.split(String.trim_end(l), ' '))
171
172def token(xs: List<&2, String>, +want: String) -> Bool:
173 match xs:
174 case Nil{}:
175 False{}
176 case Con{h, t}:
177 Bool.or(String.eq(String.trim(h), want), token(t, want))
178
179def value.is(m: Maybe<&2, String>, +want: String) -> Bool:
180 match m:
181 case None{}:
182 False{}
183 case Some{v}:
184 String.eq(v, want)
185
186def value.lower(m: Maybe<&2, String>) -> Maybe<&2, String>:
187 match m:
188 case None{}:
189 None{}
190 case Some{v}:
191 Some{String.to_lower(v)}
192
193# Connection is a list header: its lines join into one comma list (RFC 9110 §5.3).
194def tokens(xs: List<&2, String>, +want: String) -> Bool:
195 match xs:
196 case Nil{}:
197 False{}
198 case Con{v, t}:
199 Bool.or(token(String.split(String.to_lower(v), ','), want), tokens(t, want))
200
201def none(xs: List<&2, String>) -> Bool:
202 match xs:
203 case Nil{}:
204 True{}
205 case Con{h, t}:
206 False{}
207
208# Does a server's head (up to its blank line) accept the upgrade? want is accept(key).
209# Upgrade and Sec-WebSocket-Accept must each come once. No extension or subprotocol
210# was asked for, so the server may name none (§4.1).
211def check(+head: String, +want: String) -> Result<&1, &1, U32 & String, Unit>:
212 verdict(Unit,
213 first(reject(Bool.not(status(String.split(head, '\n'))), 1002, "status line is not HTTP/1.1 101"),
214 first(reject(Bool.not(lines.ok(headers(head))), 1002, "malformed header line"),
215 first(reject(Bool.not(value.is(value.lower(field(head, "upgrade")), "websocket")), 1002, "Upgrade is not one websocket"),
216 first(reject(Bool.not(tokens(fields(head, "connection"), "upgrade")), 1002, "Connection lacks Upgrade"),
217 first(reject(Bool.not(value.is(field(head, "sec-websocket-accept"), want)), 1002, "Sec-WebSocket-Accept is not one match for the key"),
218 first(reject(Bool.not(none(fields(head, "sec-websocket-extensions"))), 1002, "unrequested extension"),
219 reject(Bool.not(none(fields(head, "sec-websocket-protocol"))), 1002, "unrequested subprotocol"))))))),
220 Unit{})
221
222def with_number(-R: Type, r: Bytes.Bytes & Maybe<&2, U32>, k: Bytes.Bytes -> U32 -> R) -> R:
223 (b, m) = r
224 match m:
225 case Some{x}:
226 k(b, x)
227 case None{}:
228 k(b, 0)
229
230def with_slice(-R: Type, r: Bytes.Bytes & Bytes.Bytes, k: Bytes.Bytes -> Bytes.Bytes -> R) -> R:
231 (b, part) = r
232 k(b, part)
233
234# An HTTP head cut at its blank line, with the bytes after it.
235type Split is Type:
236 Found{head: String, rest: Bytes.Bytes}
237 Short{acc: Bytes.Bytes}
238 Long{}
239
240def split.long(long: Bool, b: Bytes.Bytes) -> Split:
241 match long:
242 case True{}:
243 Long{}
244 case False{}:
245 Short{b}
246
247def split.short(b: Bytes.Bytes) -> Split:
248 Bytes.Bytes{+n, buf} = b
249 split.long(U32.is_gt(n, 16384), Bytes.Bytes{n, buf})
250
251def split.found(r: Bytes.Bytes & Maybe<&2, U32>) -> Split:
252 (b, m) = r
253 match m:
254 case Some{+i}:
255 with_slice(Split, Bytes.slice(b, 0, i), b => head =>
256 with_slice(Split, Bytes.slice(b, (i + 4 : U32), 4294967295), unused => rest =>
257 Found{Bytes.to_string(head), rest}))
258 case None{}:
259 split.short(b)
260
261# Found once b holds "\r\n\r\n"; Long when 16 KiB came without it.
262def split(b: Bytes.Bytes) -> Split:
263 split.found(Bytes.find(b, "\r\n\r\n"))
264
265# Frames (§5.2).
266
267type Frame is Type:
268 Frame{fin: Bool, op: U32, payload: Bytes.Bytes}
269
270# Need: b does not hold a whole frame yet, and comes back intact.
271type Decode is Type:
272 Need{input: Bytes.Bytes}
273 Got{frame: Frame, rest: Bytes.Bytes}
274 Bad{code: U32, why: String}
275
276def mask.go(n: Nat, r: Array<U32> & U32, +i: U32, +key: U32) -> Array<U32>:
277 match n:
278 case 0n:
279 (a, w) = r
280 a
281 case 1n+p:
282 (a, +w) = r
283 +j = (i + 1 : U32)
284 mask.go(p, Array.get(U32, Array.set(U32, a, i, (w .^. key : U32)), j), j, key)
285
286def mask.trim.word(+k: U32, +m: U32, r: Array<U32> & U32) -> Array<U32>:
287 (a, +w) = r
288 Array.set(U32, a, k, (w .&. m : U32))
289
290def mask.trim.if(whole: Bool, +k: U32, +m: U32, a: Array<U32>) -> Array<U32>:
291 match whole:
292 case True{}:
293 a
294 case False{}:
295 mask.trim.word(k, m, Array.get(U32, a, k))
296
297# Bytes at or past len stay 0, as Bytes requires.
298def mask.trim(+len: U32, a: Array<U32>) -> Array<U32>:
299 +r = (len .&. 3 : U32)
300 mask.trim.if(U32.is_eq(r, 0), (len >> 2n : U32), (U32.shln(1, U32.to_nat((r * 8 : U32))) - 1 : U32), a)
301
302# The payload XOR the mask key (§5.3), a word at a time. key's byte k (low first) is mask octet k.
303# Masking twice gives the payload back.
304def mask(+key: U32, b: Bytes.Bytes) -> Bytes.Bytes:
305 Bytes.Bytes{+len, buf} = b
306 Bytes.Bytes{len, mask.trim(len, mask.go(U32.to_nat(Bytes.words(len)), Array.get(U32, buf, 0), 0, key))}
307
308def known(+op: U32) -> Bool:
309 match op:
310 case 0:
311 True{}
312 case 1:
313 True{}
314 case 2:
315 True{}
316 case 8:
317 True{}
318 case 9:
319 True{}
320 case 10:
321 True{}
322 case _:
323 False{}
324
325# The §5.2 and §5.5 rules on a frame header. No extension is in use, so RSV must be 0.
326def rules(+fin: Bool, +rsv: U32, +op: U32, +len: U32) -> Maybe<&1, U32 & String>:
327 first(reject(U32.is_ne(rsv, 0), 1002, "reserved bits set"),
328 first(reject(Bool.not(known(op)), 1002, "unknown opcode"),
329 first(reject(Bool.and(U32.is_ge(op, 8), Bool.not(fin)), 1002, "fragmented control frame"),
330 reject(Bool.and(U32.is_ge(op, 8), U32.is_gt(len, 125)), 1002, "control frame over 125 bytes"))))
331
332def encode.ext(+ext: U32, +len: U32, b: Bytes.Bytes) -> Bytes.Bytes:
333 match ext:
334 case 0:
335 b
336 case 2:
337 Bytes.set.u16be(b, 2, len)
338 case _:
339 Bytes.set.u32be(b, 6, len)
340
341def encode.mkey(+keylen: U32, +at: U32, +key: U32, b: Bytes.Bytes) -> Bytes.Bytes:
342 match keylen:
343 case 0:
344 b
345 case _:
346 Bytes.set.u32le(b, at, key)
347
348def encode.copy(+len: U32, src: Array<U32>, +hs: U32, b: Bytes.Bytes) -> Bytes.Bytes:
349 Bytes.Bytes{+n, dst} = b
350 Bytes.Bytes{n, Bytes.dst(Bytes.copy(len, src, dst, 0, hs))}
351
352# Payload lengths use the shortest form (§5.2): 7 bits, then 16, then 64.
353def encode.frame(+b0: U32, +mbit: U32, +keylen: U32, +key: U32, p: Bytes.Bytes) -> Bytes.Bytes:
354 Bytes.Bytes{+len, src} = p
355 +ext = Bool.pick(U32, U32.is_le(len, 125), 0, Bool.pick(U32, U32.is_le(len, 65535), 2, 8))
356 +l7 = Bool.pick(U32, U32.is_le(len, 125), len, Bool.pick(U32, U32.is_le(len, 65535), 126, 127))
357 +hs = (2 + ext + keylen : U32)
358 encode.copy(len, src, hs, encode.mkey(keylen, (2 + ext : U32), key, encode.ext(ext, len,
359 Bytes.set(Bytes.set(Bytes.new((hs + len : U32)), 0, b0), 1, (mbit .|. l7 : U32)))))
360
361def encode.key(key: Maybe<&2, U32>, +b0: U32, p: Bytes.Bytes) -> Bytes.Bytes:
362 match key:
363 case Some{+k}:
364 encode.frame(b0, 128, 4, k, mask(k, p))
365 case None{}:
366 encode.frame(b0, 0, 0, 0, p)
367
368def encode.checked(err: Maybe<&1, U32 & String>, +fin: Bool, +op: U32, key: Maybe<&2, U32>, p: Bytes.Bytes) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
369 match err:
370 case Some{e}:
371 Fail{e}
372 case None{}:
373 Done{encode.key(key, (Bool.pick(U32, fin, 128, 0) .|. op : U32), p)}
374
375# A frame's octets. A client passes Some{mask key} and the payload goes masked;
376# None sends it clear, as a server does. Fails on a frame that breaks rules.
377def encode(f: Frame, key: Maybe<&2, U32>) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
378 Frame{+fin, +op, payload} = f
379 Bytes.Bytes{+len, buf} = payload
380 encode.checked(rules(fin, 0, op, len), fin, op, key, Bytes.Bytes{len, buf})
381
382def unmask(m: Bool, +key: U32, p: Bytes.Bytes) -> Bytes.Bytes:
383 match m:
384 case True{}:
385 mask(key, p)
386 case False{}:
387 p
388
389# ponytail: rest is a copy, so a buffer of k frames costs O(k * size); keep an offset if many small frames share one read.
390def parse.done(+b0: U32, +m: Bool, +key: U32, +end: U32, payload: Bytes.Bytes, b: Bytes.Bytes) -> Decode:
391 Bytes.Bytes{+n, buf} = b
392 with_slice(Decode, Bytes.slice(Bytes.Bytes{n, buf}, end, (n - end : U32)), unused => rest =>
393 Got{Frame{U32.is_ne((b0 .&. 128 : U32), 0), (b0 .&. 15 : U32), unmask(m, key, payload)}, rest})
394
395def parse.take(short: Bool, +b0: U32, +m: Bool, +len: U32, +hs: U32, b: Bytes.Bytes) -> Decode:
396 match short:
397 case True{}:
398 Need{b}
399 case False{}:
400 with_number(Decode, Bytes.get.u32le(b, (hs - 4 : U32)), b => +key =>
401 with_slice(Decode, Bytes.slice(b, hs, len), b => payload =>
402 parse.done(b0, m, key, (hs + len : U32), payload, b)))
403
404def parse.body(err: Maybe<&1, U32 & String>, +b0: U32, +m: Bool, +len: U32, +hs: U32, b: Bytes.Bytes) -> Decode:
405 match err:
406 case Some{(code, why)}:
407 Bad{code, why}
408 case None{}:
409 Bytes.Bytes{+n, buf} = b
410 parse.take(U32.is_lt((n - hs : U32), len), b0, m, len, hs, Bytes.Bytes{n, buf})
411
412# A 64-bit length with a high word saturates to 2^32 - 1, over any max.
413def parse.check(+masked: Bool, +max: U32, +b0: U32, +hi: U32, +len: U32, +m: Bool, +hs: U32, b: Bytes.Bytes) -> Decode:
414 +size = Bool.pick(U32, U32.is_eq(hi, 0), len, 4294967295)
415 parse.body(
416 first(rules(U32.is_ne((b0 .&. 128 : U32), 0), ((b0 >> 4n) .&. 7 : U32), (b0 .&. 15 : U32), size),
417 first(reject(Bool.xor(m, masked), 1002, "mask bit does not match the peer's role"),
418 reject(U32.is_gt(size, max), 1009, "frame over the size limit"))),
419 b0, m, len, hs, b)
420
421def parse.len(short: Bool, +masked: Bool, +max: U32, +b0: U32, +l7: U32, +ext: U32, +m: Bool, +hs: U32, b: Bytes.Bytes) -> Decode:
422 match short:
423 case True{}:
424 Need{b}
425 case False{}:
426 match ext:
427 case 0:
428 parse.check(masked, max, b0, 0, l7, m, hs, b)
429 case 2:
430 with_number(Decode, Bytes.get.u16be(b, 2), b => +len =>
431 parse.check(masked, max, b0, 0, len, m, hs, b))
432 case _:
433 with_number(Decode, Bytes.get.u32be(b, 2), b => +hi =>
434 with_number(Decode, Bytes.get.u32be(b, 6), b => +len =>
435 parse.check(masked, max, b0, hi, len, m, hs, b)))
436
437def parse.head(+masked: Bool, +max: U32, +b0: U32, +b1: U32, b: Bytes.Bytes) -> Decode:
438 Bytes.Bytes{+n, buf} = b
439 +l7 = (b1 .&. 127 : U32)
440 +ext = Bool.pick(U32, U32.is_lt(l7, 126), 0, Bool.pick(U32, U32.is_eq(l7, 126), 2, 8))
441 +m = U32.is_ne((b1 .&. 128 : U32), 0)
442 +hs = (2 + ext + Bool.pick(U32, m, 4, 0) : U32)
443 parse.len(U32.is_lt(n, hs), masked, max, b0, l7, ext, m, hs, Bytes.Bytes{n, buf})
444
445def parse.start(short: Bool, +masked: Bool, +max: U32, b: Bytes.Bytes) -> Decode:
446 match short:
447 case True{}:
448 Need{b}
449 case False{}:
450 with_number(Decode, Bytes.get(b, 0), b => +b0 =>
451 with_number(Decode, Bytes.get(b, 1), b => +b1 =>
452 parse.head(masked, max, b0, b1, b)))
453
454# One frame from the front of b, unmasked. masked: this peer's frames must be masked
455# (true on a server, false on a client). max caps the payload length (1009 over it).
456# The header is checked as soon as it is whole, before its payload arrives.
457def parse(+masked: Bool, +max: U32, b: Bytes.Bytes) -> Decode:
458 Bytes.Bytes{+n, buf} = b
459 parse.start(U32.is_lt(n, 2), masked, max, Bytes.Bytes{n, buf})
460
461# UTF-8 (RFC 3629) validity. The state packs need | lo << 8 | hi << 16: continuation
462# bytes still needed and the range the next one must fall in. need 255 is a failure.
463def st(+need: U32, +lo: U32, +hi: U32) -> U32:
464 (need .|. (lo << 8n) .|. (hi << 16n) : U32)
465
466def utf8.lead(+b: U32) -> U32:
467 Bool.pick(U32, U32.is_lt(b, 128), st(0, 128, 191),
468 Bool.pick(U32, U32.is_lt(b, 194), 255,
469 Bool.pick(U32, U32.is_lt(b, 224), st(1, 128, 191),
470 Bool.pick(U32, U32.is_eq(b, 224), st(2, 160, 191),
471 Bool.pick(U32, U32.is_eq(b, 237), st(2, 128, 159),
472 Bool.pick(U32, U32.is_lt(b, 240), st(2, 128, 191),
473 Bool.pick(U32, U32.is_eq(b, 240), st(3, 144, 191),
474 Bool.pick(U32, U32.is_lt(b, 244), st(3, 128, 191),
475 Bool.pick(U32, U32.is_eq(b, 244), st(3, 128, 143), 255)))))))))
476
477def utf8.next(+s: U32, +b: U32) -> U32:
478 +need = (s .&. 255 : U32)
479 Bool.pick(U32, U32.is_eq(need, 255), 255,
480 Bool.pick(U32, U32.is_eq(need, 0), utf8.lead(b),
481 Bool.pick(U32, Bool.and(U32.is_le(((s >> 8n) .&. 255 : U32), b), U32.is_le(b, (s >> 16n : U32))),
482 st((need - 1 : U32), 128, 191), 255)))
483
484def utf8.go(n: Nat, r: Array<U32> & U32, +i: U32, +s: U32) -> Array<U32> & Bool:
485 match n:
486 case 0n:
487 (a, v) = r
488 (a, U32.is_eq((s .&. 255 : U32), 0))
489 case 1n+p:
490 (a, +b) = r
491 +j = (i + 1 : U32)
492 utf8.go(p, Bytes.peek(a, j), j, utf8.next(s, b))
493
494def utf8.fin(+len: U32, r: Array<U32> & Bool) -> Bytes.Bytes & Bool:
495 (a, ok) = r
496 (Bytes.Bytes{len, a}, ok)
497
498# b back, and whether it is well-formed UTF-8.
499def utf8.valid(b: Bytes.Bytes) -> Bytes.Bytes & Bool:
500 Bytes.Bytes{+len, buf} = b
501 utf8.fin(len, utf8.go(U32.to_nat(len), Bytes.peek(buf, 0), 0, st(0, 128, 191)))
502
503# Messages (§5.4): fragments join into one message; control frames may come between them.
504
505type Partial is Type:
506 Idle{}
507 Open{op: U32, data: Bytes.Bytes}
508
509type Msg is Type:
510 Message{op: U32, data: Bytes.Bytes}
511 Control{op: U32, data: Bytes.Bytes}
512 More{}
513
514def done.text(ok: Bytes.Bytes & Bool) -> Result<&1, &1, U32 & String, Partial & Msg>:
515 (d, v) = ok
516 match v:
517 case True{}:
518 Done{(Idle{}, Message{1, d})}
519 case False{}:
520 Fail{(1007, "text message is not UTF-8")}
521
522def finish(+op: U32, d: Bytes.Bytes) -> Result<&1, &1, U32 & String, Partial & Msg>:
523 match op:
524 case 1:
525 done.text(utf8.valid(d))
526 case +o:
527 Done{(Idle{}, Message{o, d})}
528
529def feed.more(fin: Bool, +op: U32, d: Bytes.Bytes) -> Result<&1, &1, U32 & String, Partial & Msg>:
530 match fin:
531 case True{}:
532 finish(op, d)
533 case False{}:
534 Done{(Open{op, d}, More{})}
535
536def feed.size(over: Bool, +fin: Bool, +op: U32, d: Bytes.Bytes) -> Result<&1, &1, U32 & String, Partial & Msg>:
537 match over:
538 case True{}:
539 Fail{(1009, "message over the size limit")}
540 case False{}:
541 feed.more(fin, op, d)
542
543def feed.join(+fin: Bool, +op: U32, d: Bytes.Bytes, +max: U32) -> Result<&1, &1, U32 & String, Partial & Msg>:
544 Bytes.Bytes{+n, buf} = d
545 feed.size(U32.is_gt(n, max), fin, op, Bytes.Bytes{n, buf})
546
547def feed.data(p: Partial, +fin: Bool, +op: U32, d: Bytes.Bytes, +max: U32) -> Result<&1, &1, U32 & String, Partial & Msg>:
548 match p:
549 case Idle{}:
550 match op:
551 case 0:
552 Fail{(1002, "continuation frame without a message")}
553 case +o:
554 feed.more(fin, o, d)
555 case Open{+o, acc}:
556 match op:
557 case 0:
558 feed.join(fin, o, Bytes.append(acc, d), max)
559 case _:
560 Fail{(1002, "data frame inside a fragmented message")}
561
562def feed.kind(ctl: Bool, p: Partial, +fin: Bool, +op: U32, d: Bytes.Bytes, +max: U32) -> Result<&1, &1, U32 & String, Partial & Msg>:
563 match ctl:
564 case True{}:
565 Done{(p, Control{op, d})}
566 case False{}:
567 feed.data(p, fin, op, d, max)
568
569# One parsed frame into the message being built. A whole text message must be UTF-8
570# (1007); max caps a message's total size (1009). Keep max at or below 2^31.
571def feed(p: Partial, f: Frame, +max: U32) -> Result<&1, &1, U32 & String, Partial & Msg>:
572 Frame{+fin, +op, d} = f
573 feed.kind(U32.is_ge(op, 8), p, fin, op, d, max)
574
575# Close payloads (§5.5.1, §7.4).
576
577# code (big-endian) then a UTF-8 reason.
578def close.payload(+code: U32, reason: Bytes.Bytes) -> Bytes.Bytes:
579 Bytes.append(Bytes.set.u16be(Bytes.new(2), 0, code), reason)
580
581# Codes a peer may send: §7.4.1, the IANA registry through 1014, and 3000-4999.
582def close.code.ok(+c: U32) -> Bool:
583 Bool.or(Bool.and(U32.is_ge(c, 1000), U32.is_le(c, 1003)),
584 Bool.or(Bool.and(U32.is_ge(c, 1007), U32.is_le(c, 1014)),
585 Bool.and(U32.is_ge(c, 3000), U32.is_le(c, 4999))))
586
587def close.utf8(+c: U32, r: Bytes.Bytes & Bool) -> Result<&1, &1, U32 & String, U32 & Bytes.Bytes>:
588 (b, ok) = r
589 match ok:
590 case True{}:
591 Done{(c, b)}
592 case False{}:
593 Fail{(1007, "close reason is not UTF-8")}
594
595def close.reason(ok: Bool, +c: U32, b: Bytes.Bytes) -> Result<&1, &1, U32 & String, U32 & Bytes.Bytes>:
596 match ok:
597 case False{}:
598 Fail{(1002, "invalid close code")}
599 case True{}:
600 Bytes.Bytes{+n, buf} = b
601 with_slice(Result<&1, &1, U32 & String, U32 & Bytes.Bytes>, Bytes.slice(Bytes.Bytes{n, buf}, 2, (n - 2 : U32)),
602 unused => r => close.utf8(c, utf8.valid(r)))
603
604def close.code(r: Bytes.Bytes & Maybe<&2, U32>) -> Result<&1, &1, U32 & String, U32 & Bytes.Bytes>:
605 (b, m) = r
606 match m:
607 case Some{+c}:
608 close.reason(close.code.ok(c), c, b)
609 case None{}:
610 Fail{(1002, "close payload of one byte")}
611
612# The code and reason of a close frame. An empty payload is 1005 (no status).
613def close.parse(p: Bytes.Bytes) -> Result<&1, &1, U32 & String, U32 & Bytes.Bytes>:
614 Bytes.Bytes{+n, buf} = p
615 match n:
616 case 0:
617 Done{(1005, Bytes.Bytes{0, buf})}
618 case +m:
619 close.code(Bytes.get.u16be(Bytes.Bytes{m, buf}, 0))
620
621# Connections over Wire.
622
623# server: this end is the server (peer frames arrive masked, ours go clear), for a socket
624# an HTTP server upgraded. input holds bytes read past the last frame. closing: we sent close.
625type Conn is Type:
626 Conn{sock: Socket, tls: Bool, server: Bool, input: Bytes.Bytes, partial: Partial, max: U32, closing: Bool}
627
628# What recv returns. Ping is answered with a pong inside recv and not returned.
629type Incoming is Type:
630 Text{data: Bytes.Bytes}
631 Binary{data: Bytes.Bytes}
632 Pong{data: Bytes.Bytes}
633 Closed{code: U32, reason: Bytes.Bytes}
634
635def io.send.if(tls: Bool, sock: Socket, +len: U32, buf: Array<U32>) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
636 match tls:
637 case True{}:
638 Wire.tls.send.words(sock, len, buf)
639 case False{}:
640 Wire.send.words(sock, len, buf)
641
642def io.send(sock: Socket, +tls: Bool, b: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
643 Bytes.Bytes{+len, buf} = b
644 io.send.if(tls, sock, len, buf)
645
646def io.recv(tls: Bool, sock: Socket, +ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>):
647 match tls:
648 case True{}:
649 Wire.tls.recv.words(sock, 65536, ms)
650 case False{}:
651 Wire.recv.words(sock, 65536, ms)
652
653def io.close(tls: Bool, sock: Socket) -> IO(Unit):
654 match tls:
655 case True{}:
656 Wire.tls.close(sock)
657 case False{}:
658 Socket.close(sock)
659
660type Head is Type:
661 HRead{r: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>, acc: Bytes.Bytes}
662 HSplit{sock: Socket, s: Split}
663
664def head.loop(n: Nat, h: Head, +tls: Bool, +ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>):
665 match n:
666 case 0n:
667 match h:
668 case HRead{r, acc}:
669 (sock, x) = r
670 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
671 return (sock, Fail{(1002, "HTTP head took too many reads")})
672 case HSplit{sock, s}:
673 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
674 return (sock, Fail{(1002, "HTTP head took too many reads")})
675 case 1n+p:
676 match h:
677 case HRead{r, acc}:
678 match r:
679 case (sock, Fail{e}):
680 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
681 return (sock, Fail{e})
682 case (sock, Done{(0, buf)}):
683 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
684 return (sock, Fail{(1006, "connection closed before the HTTP head ended")})
685 case (sock, Done{(+len, buf)}):
686 head.loop(p, HSplit{sock, split(Bytes.append(acc, Bytes.Bytes{len, buf}))}, tls, ms)
687 case HSplit{sock, s}:
688 match s:
689 case Found{head, rest}:
690 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
691 return (sock, Done{(head, rest)})
692 case Long{}:
693 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
694 return (sock, Fail{(1002, "HTTP head over 16 KiB")})
695 case Short{acc}:
696 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
697 r : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv(tls, sock, ms)
698 head.loop(p, HRead{r, acc}, tls, ms)
699
700# Reads an HTTP head: the text before its blank line, and the bytes after it.
701def head.read(sock: Socket, +tls: Bool, +ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>):
702 head.loop(256n, HSplit{sock, Short{Bytes.new(0)}}, tls, ms)
703
704def hs.fail(sock: Socket, +tls: Bool, e: U32 & String) -> IO(Result<&1, &1, U32 & String, Conn>):
705 do IO<Result<&1, &1, U32 & String, Conn>>:
706 io.close(tls, sock)
707 return Fail{e}
708
709def hs.checked(v: Result<&1, &1, U32 & String, Unit>, sock: Socket, +tls: Bool, +max: U32, rest: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, Conn>):
710 match v:
711 case Fail{e}:
712 hs.fail(sock, tls, e)
713 case Done{u}:
714 do IO<Result<&1, &1, U32 & String, Conn>>:
715 return Done{Conn{sock, tls, False{}, rest, Idle{}, max, False{}}}
716
717def hs.head(r: Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>, +tls: Bool, +max: U32, +want: String) -> IO(Result<&1, &1, U32 & String, Conn>):
718 match r:
719 case (sock, Fail{e}):
720 hs.fail(sock, tls, e)
721 case (sock, Done{(+head, rest)}):
722 hs.checked(check(head, want), sock, tls, max, rest)
723
724def hs.sent(r: Socket & Result<&1, &1, U32 & String, Unit>, +tls: Bool, +max: U32, +ms: U32, +want: String) -> IO(Result<&1, &1, U32 & String, Conn>):
725 match r:
726 case (sock, Fail{e}):
727 hs.fail(sock, tls, e)
728 case (sock, Done{u}):
729 do IO<Result<&1, &1, U32 & String, Conn>>:
730 h : Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes> <- head.read(sock, tls, ms)
731 hs.head(h, tls, max, want)
732
733def hs.request(q: Result<&1, &1, U32 & String, Bytes.Bytes>, sock: Socket, +tls: Bool, +max: U32, +ms: U32, +want: String) -> IO(Result<&1, &1, U32 & String, Conn>):
734 match q:
735 case Fail{e}:
736 hs.fail(sock, tls, e)
737 case Done{b}:
738 do IO<Result<&1, &1, U32 & String, Conn>>:
739 r : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(sock, tls, b)
740 hs.sent(r, tls, max, ms, want)
741
742def hs.accepted(a: Result<&1, &1, U32 & String, String>, sock: Socket, +tls: Bool, +host: String, +path: String, +max: U32, +ms: U32, +key: String) -> IO(Result<&1, &1, U32 & String, Conn>):
743 match a:
744 case Fail{e}:
745 hs.fail(sock, tls, e)
746 case Done{+want}:
747 hs.request(request(host, path, key), sock, tls, max, ms, want)
748
749def hs.keyed(k: Result<&1, &1, U32 & String, String>, sock: Socket, +tls: Bool, +host: String, +path: String, +max: U32, +ms: U32) -> IO(Result<&1, &1, U32 & String, Conn>):
750 match k:
751 case Fail{e}:
752 hs.fail(sock, tls, e)
753 case Done{+key}:
754 do IO<Result<&1, &1, U32 & String, Conn>>:
755 a : Result<&1, &1, U32 & String, String> <- accept(key)
756 hs.accepted(a, sock, tls, host, path, max, ms, key)
757
758# The opening handshake on a connected socket (TLS already up when tls). host is the Host
759# header and path the request target. max caps frame and message sizes. On failure the
760# socket is closed. Bytes the server sent after its head stay in the Conn.
761def handshake(sock: Socket, +tls: Bool, +host: String, +path: String, +max: U32, +ms: U32) -> IO(Result<&1, &1, U32 & String, Conn>):
762 do IO<Result<&1, &1, U32 & String, Conn>>:
763 k : Result<&1, &1, U32 & String, String> <- key()
764 hs.keyed(k, sock, tls, host, path, max, ms)
765
766def connect.tls(r: Socket & Result<&1, &1, U32 & String, Unit>, +authority: String, +path: String, +max: U32, +ms: U32) -> IO(Result<&1, &1, U32 & String, Conn>):
767 match r:
768 case (sock, Fail{e}):
769 hs.fail(sock, False{}, e)
770 case (sock, Done{u}):
771 handshake(sock, True{}, authority, path, max, ms)
772
773def connect.tcp(c: Result<&1, &1, U32 & String, Socket>, +tls: Bool, +host: String, +authority: String, +path: String, +max: U32, +ms: U32) -> IO(Result<&1, &1, U32 & String, Conn>):
774 match c:
775 case Fail{e}:
776 do IO<Result<&1, &1, U32 & String, Conn>>:
777 return Fail{e}
778 case Done{sock}:
779 match tls:
780 case True{}:
781 do IO<Result<&1, &1, U32 & String, Conn>>:
782 t : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.connect(sock, host, ms)
783 connect.tls(t, authority, path, max, ms)
784 case False{}:
785 handshake(sock, False{}, authority, path, max, ms)
786
787# ws:// (tls false) or wss:// to a numeric address (resolve names with dns). host is the
788# server name, for Host and TLS verification. ms bounds each socket step.
789def connect(+addr: String, +port: U32, +host: String, +path: String, +tls: Bool, +max: U32, +ms: U32) -> IO(Result<&1, &1, U32 & String, Conn>):
790 +std = U32.is_eq(port, Bool.pick(U32, tls, 443, 80))
791 +authority = Bool.pick(String, std, host, host ++ ":" ++ U32.show(port))
792 do IO<Result<&1, &1, U32 & String, Conn>>:
793 c : Result<&1, &1, U32 & String, Socket> <- Wire.connect(addr, port, ms)
794 connect.tcp(c, tls, host, authority, path, max, ms)
795
796def raw.encoded(e: Result<&1, &1, U32 & String, Bytes.Bytes>, sock: Socket, +tls: Bool) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
797 match e:
798 case Fail{err}:
799 do IO<Socket & Result<&1, &1, U32 & String, Unit>>:
800 return (sock, Fail{err})
801 case Done{b}:
802 io.send(sock, tls, b)
803
804def raw.key(r: Array<U32> & U32, sock: Socket, +tls: Bool, +fin: Bool, +op: U32, payload: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
805 (a, +key) = r
806 raw.encoded(encode(Frame{fin, op, payload}, Some{key}), sock, tls)
807
808def raw.keyed(k: Result<&1, &1, U32 & String, U32 & Array<U32>>, sock: Socket, +tls: Bool, +fin: Bool, +op: U32, payload: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
809 match k:
810 case Fail{e}:
811 do IO<Socket & Result<&1, &1, U32 & String, Unit>>:
812 return (sock, Fail{e})
813 case Done{(n, a)}:
814 raw.key(Array.get(U32, a, 0), sock, tls, fin, op, payload)
815
816# A client masks every frame with a fresh key from the OS secure random source (§5.3).
817def raw(server: Bool, sock: Socket, +tls: Bool, +fin: Bool, +op: U32, payload: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
818 match server:
819 case True{}:
820 raw.encoded(encode(Frame{fin, op, payload}, None{}), sock, tls)
821 case False{}:
822 do IO<Socket & Result<&1, &1, U32 & String, Unit>>:
823 k : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.random.words(4)
824 raw.keyed(k, sock, tls, fin, op, payload)
825
826def back(r: Socket & Result<&1, &1, U32 & String, Unit>, +tls: Bool, +server: Bool, input: Bytes.Bytes, partial: Partial, +max: U32, +closing: Bool) -> Conn & Result<&1, &1, U32 & String, Unit>:
827 (sock, x) = r
828 (Conn{sock, tls, server, input, partial, max, closing}, x)
829
830# Sends one frame: fin false starts or continues a fragmented message (later frames use op 0).
831def send(c: Conn, +fin: Bool, +op: U32, payload: Bytes.Bytes) -> IO(Conn & Result<&1, &1, U32 & String, Unit>):
832 Conn{sock, +tls, +server, input, partial, +max, +closing} = c
833 do IO<Conn & Result<&1, &1, U32 & String, Unit>>:
834 r : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, fin, op, payload)
835 return back(r, tls, server, input, partial, max, closing)
836
837# Sends a close frame; recv then runs until the peer's close comes back as Closed.
838def close(c: Conn, +code: U32, reason: Bytes.Bytes) -> IO(Conn & Result<&1, &1, U32 & String, Unit>):
839 Conn{sock, +tls, +server, input, partial, +max, +closing} = c
840 do IO<Conn & Result<&1, &1, U32 & String, Unit>>:
841 r : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, True{}, 8, close.payload(code, reason))
842 return back(r, tls, server, input, partial, max, True{})
843
844# Closes the socket (and its TLS session).
845def shutdown(c: Conn) -> IO(Unit):
846 Conn{sock, tls, server, input, partial, max, closing} = c
847 io.close(tls, sock)
848
849type Step is Type:
850 Parse{sock: Socket, input: Bytes.Bytes, partial: Partial}
851 Decoded{sock: Socket, partial: Partial, d: Decode}
852 Fed{sock: Socket, rest: Bytes.Bytes, r: Result<&1, &1, U32 & String, Partial & Msg>}
853 Read{r: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>, input: Bytes.Bytes, partial: Partial}
854 Ponged{r: Socket & Result<&1, &1, U32 & String, Unit>, input: Bytes.Bytes, partial: Partial}
855
856def recv.out(sock: Socket, +tls: Bool, +server: Bool, input: Bytes.Bytes, partial: Partial, +max: U32, +closing: Bool, r: Result<&1, &1, U32 & String, Incoming>) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
857 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
858 return (Conn{sock, tls, server, input, partial, max, closing}, r)
859
860def recv.failed(r: Socket & Result<&1, &1, U32 & String, Unit>, +tls: Bool, +server: Bool, +max: U32, e: U32 & String) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
861 (sock, x) = r
862 recv.out(sock, tls, server, Bytes.new(0), Idle{}, max, True{}, Fail{e})
863
864# A peer broke the protocol: send close with its code (§7.1.7), then report it.
865def recv.fail(sock: Socket, +tls: Bool, +server: Bool, +max: U32, e: U32 & String) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
866 (+code, why) = e
867 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
868 r : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, True{}, 8, close.payload(code, Bytes.new(0)))
869 recv.failed(r, tls, server, max, (code, why))
870
871def recv.echoed(r: Socket & Result<&1, &1, U32 & String, Unit>, +tls: Bool, +server: Bool, rest: Bytes.Bytes, partial: Partial, +max: U32, +code: U32, reason: Bytes.Bytes) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
872 (sock, x) = r
873 recv.out(sock, tls, server, rest, partial, max, True{}, Done{Closed{code, reason}})
874
875def recv.closed(r: Result<&1, &1, U32 & String, U32 & Bytes.Bytes>, sock: Socket, +tls: Bool, +server: Bool, rest: Bytes.Bytes, partial: Partial, +max: U32, closing: Bool) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
876 match r:
877 case Fail{e}:
878 recv.fail(sock, tls, server, max, e)
879 case Done{(+code, reason)}:
880 match closing:
881 case True{}:
882 recv.out(sock, tls, server, rest, partial, max, True{}, Done{Closed{code, reason}})
883 case False{}:
884 echo = Bool.pick(Bytes.Bytes, U32.is_eq(code, 1005), Bytes.new(0), close.payload(code, Bytes.new(0)))
885 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
886 s : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, True{}, 8, echo)
887 recv.echoed(s, tls, server, rest, partial, max, code, reason)
888
889def recv.stuck(h: Step, +tls: Bool, +server: Bool, +max: U32) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
890 match h:
891 case Parse{sock, input, partial}:
892 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
893 case Decoded{sock, partial, d}:
894 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
895 case Fed{sock, rest, r}:
896 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
897 case Read{r, input, partial}:
898 (sock, x) = r
899 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
900 case Ponged{r, input, partial}:
901 (sock, x) = r
902 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
903
904def recv.loop(n: Nat, h: Step, +tls: Bool, +server: Bool, +max: U32, +closing: Bool, +ms: U32) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
905 match n:
906 case 0n:
907 recv.stuck(h, tls, server, max)
908 case 1n+p:
909 match h:
910 case Parse{sock, input, partial}:
911 recv.loop(p, Decoded{sock, partial, parse(server, max, input)}, tls, server, max, closing, ms)
912 case Decoded{sock, partial, d}:
913 match d:
914 case Need{input}:
915 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
916 r : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv(tls, sock, ms)
917 recv.loop(p, Read{r, input, partial}, tls, server, max, closing, ms)
918 case Bad{+code, why}:
919 recv.fail(sock, tls, server, max, (code, why))
920 case Got{f, rest}:
921 recv.loop(p, Fed{sock, rest, feed(partial, f, max)}, tls, server, max, closing, ms)
922 case Fed{sock, rest, r}:
923 match r:
924 case Fail{e}:
925 recv.fail(sock, tls, server, max, e)
926 case Done{(partial, ev)}:
927 match ev:
928 case More{}:
929 recv.loop(p, Parse{sock, rest, partial}, tls, server, max, closing, ms)
930 case Message{1, d}:
931 recv.out(sock, tls, server, rest, partial, max, closing, Done{Text{d}})
932 case Message{op, d}:
933 recv.out(sock, tls, server, rest, partial, max, closing, Done{Binary{d}})
934 case Control{9, d}:
935 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
936 s : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, True{}, 10, d)
937 recv.loop(p, Ponged{s, rest, partial}, tls, server, max, closing, ms)
938 case Control{10, d}:
939 recv.out(sock, tls, server, rest, partial, max, closing, Done{Pong{d}})
940 case Control{op, d}:
941 recv.closed(close.parse(d), sock, tls, server, rest, partial, max, closing)
942 case Read{r, input, partial}:
943 match r:
944 case (sock, Fail{e}):
945 recv.out(sock, tls, server, input, partial, max, closing, Fail{e})
946 case (sock, Done{(0, buf)}):
947 recv.out(sock, tls, server, input, partial, max, closing, Fail{(1006, "connection closed without a close frame")})
948 case (sock, Done{(+len, buf)}):
949 recv.loop(p, Parse{sock, Bytes.append(input, Bytes.Bytes{len, buf}), partial}, tls, server, max, closing, ms)
950 case Ponged{r, input, partial}:
951 match r:
952 case (sock, Fail{e}):
953 recv.out(sock, tls, server, input, partial, max, closing, Fail{e})
954 case (sock, Done{u}):
955 recv.loop(p, Parse{sock, input, partial}, tls, server, max, closing, ms)
956
957# The next message, pong, or close. Fragments are joined and pings answered on the way.
958# A protocol fault sends close with its code and fails with it. ms bounds each read.
959def recv(c: Conn, +ms: U32) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
960 Conn{sock, +tls, +server, input, partial, +max, +closing} = c
961 recv.loop(U32.to_nat(16777216), Parse{sock, input, partial}, tls, server, max, closing, ms)