websocket.bend
bend-kit-websocket@0.3.0.0 · 1,100 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.2.0/bytes.bend as Bytes
4import bend-kit-crypto@0.2.2.1/crypto.bend as Crypto
5import bend-kit-wire@0.4.6.1/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_slice(-R: Type, r: Bytes.Bytes & Bytes.Bytes, k: Bytes.Bytes -> Bytes.Bytes -> R) -> R:
223 (b, part) = r
224 k(b, part)
225
226# An HTTP head cut at its blank line, with the bytes after it.
227type Split is Type:
228 Found{head: String, rest: Bytes.Bytes}
229 Short{acc: Bytes.Bytes}
230 Long{}
231
232def split.long(long: Bool, b: Bytes.Bytes) -> Split:
233 match long:
234 case True{}:
235 Long{}
236 case False{}:
237 Short{b}
238
239def split.short(b: Bytes.Bytes) -> Split:
240 Bytes.Bytes{+n, buf} = b
241 split.long(U32.is_gt(n, 16384), Bytes.Bytes{n, buf})
242
243def split.found(r: Bytes.Bytes & Maybe<&2, U32>) -> Split:
244 (b, m) = r
245 match m:
246 case Some{+i}:
247 with_slice(Split, Bytes.slice(b, 0, i), b => head =>
248 with_slice(Split, Bytes.slice(b, (i + 4 : U32), 4294967295), unused => rest =>
249 Found{Bytes.to_string(head), rest}))
250 case None{}:
251 split.short(b)
252
253# Found once b holds "\r\n\r\n"; Long when 16 KiB came without it.
254def split(b: Bytes.Bytes) -> Split:
255 split.found(Bytes.find(b, "\r\n\r\n"))
256
257# Frames (§5.2).
258
259# The payload P is Bytes at run time and a List of octets in the proofs.
260type Frame<-P: Type> is Type:
261 Frame{fin: Bool, op: U32, payload: P}
262
263# Need: the input does not hold a whole frame yet, and comes back intact.
264# Got: one frame, and the octets after it. Bad: the input breaks §5.2 whatever comes next.
265type Decode<-P: Type, -S: Type> is Type:
266 Need{input: S}
267 Got{frame: Frame<P>, rest: S}
268 Bad{code: U32, why: String}
269
270def mask.go(n: Nat, r: Array<U32> & U32, +i: U32, +key: U32) -> Array<U32>:
271 match n:
272 case 0n:
273 (a, w) = r
274 a
275 case 1n+p:
276 (a, +w) = r
277 +j = (i + 1 : U32)
278 mask.go(p, Array.get(U32, Array.set(U32, a, i, (w .^. key : U32)), j), j, key)
279
280def mask.trim.word(+k: U32, +m: U32, r: Array<U32> & U32) -> Array<U32>:
281 (a, +w) = r
282 Array.set(U32, a, k, (w .&. m : U32))
283
284def mask.trim.if(whole: Bool, +k: U32, +m: U32, a: Array<U32>) -> Array<U32>:
285 match whole:
286 case True{}:
287 a
288 case False{}:
289 mask.trim.word(k, m, Array.get(U32, a, k))
290
291# Bytes at or past len stay 0, as Bytes requires.
292def mask.trim(+len: U32, a: Array<U32>) -> Array<U32>:
293 +r = (len .&. 3 : U32)
294 mask.trim.if(U32.is_eq(r, 0), (len >> 2n : U32), (U32.shln(1, U32.to_nat((r * 8 : U32))) - 1 : U32), a)
295
296# The payload XOR the mask key (§5.3), a word at a time. key's byte k (low first) is mask octet k.
297# Masking twice gives the payload back.
298def mask(+key: U32, b: Bytes.Bytes) -> Bytes.Bytes:
299 Bytes.Bytes{+len, buf} = b
300 Bytes.Bytes{len, mask.trim(len, mask.go(U32.to_nat(Bytes.words(len)), Array.get(U32, buf, 0), 0, key))}
301
302def known(+op: U32) -> Bool:
303 match op:
304 case 0:
305 True{}
306 case 1:
307 True{}
308 case 2:
309 True{}
310 case 8:
311 True{}
312 case 9:
313 True{}
314 case 10:
315 True{}
316 case _:
317 False{}
318
319# The §5.2 and §5.5 rules on a frame header. No extension is in use, so RSV must be 0.
320# big: the payload is over 125 octets.
321def rules.big(+fin: Bool, +rsv: U32, +op: U32, big: Bool) -> Maybe<&1, U32 & String>:
322 first(reject(U32.is_ne(rsv, 0), 1002, "reserved bits set"),
323 first(reject(Bool.not(known(op)), 1002, "unknown opcode"),
324 first(reject(Bool.and(U32.is_ge(op, 8), Bool.not(fin)), 1002, "fragmented control frame"),
325 reject(Bool.and(U32.is_ge(op, 8), big), 1002, "control frame over 125 bytes"))))
326
327def rules(+fin: Bool, +rsv: U32, +op: U32, +len: U32) -> Maybe<&1, U32 & String>:
328 rules.big(fin, rsv, op, U32.is_gt(len, 125))
329
330def encode.ext(+ext: U32, +len: U32, b: Bytes.Bytes) -> Bytes.Bytes:
331 match ext:
332 case 0:
333 b
334 case 2:
335 Bytes.set.u16be(b, 2, len)
336 case _:
337 Bytes.set.u32be(b, 6, len)
338
339def encode.mkey(+keylen: U32, +at: U32, +key: U32, b: Bytes.Bytes) -> Bytes.Bytes:
340 match keylen:
341 case 0:
342 b
343 case _:
344 Bytes.set.u32le(b, at, key)
345
346def encode.copy(+len: U32, src: Array<U32>, +hs: U32, b: Bytes.Bytes) -> Bytes.Bytes:
347 Bytes.Bytes{+n, dst} = b
348 Bytes.Bytes{n, Bytes.dst(Bytes.copy(len, src, dst, 0, hs))}
349
350# Payload lengths use the shortest form (§5.2): 7 bits, then 16, then 64.
351def encode.frame(+b0: U32, +mbit: U32, +keylen: U32, +key: U32, p: Bytes.Bytes) -> Bytes.Bytes:
352 Bytes.Bytes{+len, src} = p
353 +ext = Bool.pick(U32, U32.is_le(len, 125), 0, Bool.pick(U32, U32.is_le(len, 65535), 2, 8))
354 +l7 = Bool.pick(U32, U32.is_le(len, 125), len, Bool.pick(U32, U32.is_le(len, 65535), 126, 127))
355 +hs = (2 + ext + keylen : U32)
356 encode.copy(len, src, hs, encode.mkey(keylen, (2 + ext : U32), key, encode.ext(ext, len,
357 Bytes.set(Bytes.set(Bytes.new((hs + len : U32)), 0, b0), 1, (mbit .|. l7 : U32)))))
358
359def encode.key(key: Maybe<&2, U32>, +b0: U32, p: Bytes.Bytes) -> Bytes.Bytes:
360 match key:
361 case Some{+k}:
362 encode.frame(b0, 128, 4, k, mask(k, p))
363 case None{}:
364 encode.frame(b0, 0, 0, 0, p)
365
366def 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>:
367 match err:
368 case Some{e}:
369 Fail{e}
370 case None{}:
371 Done{encode.key(key, (Bool.pick(U32, fin, 128, 0) .|. op : U32), p)}
372
373# A frame's octets. A client passes Some{mask key} and the payload goes masked;
374# None sends it clear, as a server does. Fails on a frame that breaks rules.
375def encode(f: Frame<Bytes.Bytes>, key: Maybe<&2, U32>) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
376 Frame{+fin, +op, payload} = f
377 Bytes.Bytes{+len, buf} = payload
378 encode.checked(rules(fin, 0, op, len), fin, op, key, Bytes.Bytes{len, buf})
379
380# A frame header, read from a list of the first octets of the input.
381# Ok: hs header octets, then len payload octets, masked with key when m.
382type Header is Data:
383 HNeed{}
384 HBad{code: U32, why: String}
385 HOk{fin: Bool, op: U32, m: Bool, key: U32, hs: U32, len: U32}
386
387def header.verdict(err: Maybe<&1, U32 & String>, +fin: Bool, +op: U32, +m: Bool, +key: U32, +hs: U32, +len: U32) -> Header:
388 match err:
389 case Some{(code, why)}:
390 HBad{code, why}
391 case None{}:
392 HOk{fin, op, m, key, hs, len}
393
394# A 64-bit length with a high word is over any U32 max, and is a control frame over 125.
395def header.err(+masked: Bool, +b0: U32, +m: Bool, +hi: U32, +len: U32) -> Maybe<&1, U32 & String>:
396 first(rules(U32.is_ne((b0 .&. 128 : U32), 0), ((b0 >> 4n) .&. 7 : U32), (b0 .&. 15 : U32), Bool.pick(U32, U32.is_eq(hi, 0), len, 4294967295)),
397 first(reject(Bool.xor(m, masked), 1002, "mask bit does not match the peer's role"),
398 reject(U32.is_ne(hi, 0), 1009, "frame over the size limit")))
399
400def header.check(+masked: Bool, +b0: U32, +m: Bool, +key: U32, +hs: U32, +hi: U32, +len: U32) -> Header:
401 header.verdict(header.err(masked, b0, m, hi, len), U32.is_ne((b0 .&. 128 : U32), 0), (b0 .&. 15 : U32), m, key, hs, len)
402
403# The mask key (§5.3) follows the length; its first octet is the key's low byte.
404def header.key(m: Bool, t: List<&2, U32>, +masked: Bool, +b0: U32, +hs: U32, +hi: U32, +len: U32) -> Header:
405 match m:
406 case True{}:
407 match t:
408 case Con{+k0, Con{+k1, Con{+k2, Con{+k3, r}}}}:
409 header.check(masked, b0, True{}, (k0 .|. (k1 << 8n) .|. (k2 << 16n) .|. (k3 << 24n) : U32), (hs + 4 : U32), hi, len)
410 case _:
411 HNeed{}
412 case False{}:
413 header.check(masked, b0, False{}, 0, hs, hi, len)
414
415def be32(+a: U32, +b: U32, +c: U32, +d: U32) -> U32:
416 ((a << 24n) .|. (b << 16n) .|. (c << 8n) .|. d : U32)
417
418def header.ext16(t: List<&2, U32>, +masked: Bool, +b0: U32, +m: Bool) -> Header:
419 match t:
420 case Con{+x, Con{+y, r}}:
421 header.key(m, r, masked, b0, 4, 0, ((x << 8n) .|. y : U32))
422 case _:
423 HNeed{}
424
425def header.ext64(t: List<&2, U32>, +masked: Bool, +b0: U32, +m: Bool) -> Header:
426 match t:
427 case Con{+a, Con{+b, Con{+c, Con{+d, Con{+e, Con{+f, Con{+g, Con{+h, r}}}}}}}}:
428 header.key(m, r, masked, b0, 10, be32(a, b, c, d), be32(e, f, g, h))
429 case _:
430 HNeed{}
431
432# short: no extended length (l7 < 126); mid: 2 octets of it (l7 == 126); else 8.
433def header.ext(short: Bool, mid: Bool, t: List<&2, U32>, +masked: Bool, +b0: U32, +m: Bool, +l7: U32) -> Header:
434 match short:
435 case True{}:
436 header.key(m, t, masked, b0, 2, 0, l7)
437 case False{}:
438 match mid:
439 case True{}:
440 header.ext16(t, masked, b0, m)
441 case False{}:
442 header.ext64(t, masked, b0, m)
443
444def header.b1(m: Bool, t: List<&2, U32>, +masked: Bool, +b0: U32, +b1: U32) -> Header:
445 match m:
446 case True{}:
447 +l7 = (b1 - 128 : U32)
448 header.ext(U32.is_lt(l7, 126), U32.is_eq(l7, 126), t, masked, b0, True{}, l7)
449 case False{}:
450 header.ext(U32.is_lt(b1, 126), U32.is_eq(b1, 126), t, masked, b0, False{}, b1)
451
452# The header at the front of p, from octets below 256. It reads at most 14 octets, and is
453# HNeed until all of them are in p. It is checked as soon as it is whole, before its payload.
454def header(p: List<&2, U32>, +masked: Bool) -> Header:
455 match p:
456 case Con{+b0, Con{+b1, t}}:
457 header.b1(U32.is_le(128, b1), t, masked, b0, b1)
458 case _:
459 HNeed{}
460
461# The decoder, over any input S with four operations, giving payloads P:
462# prefix gives at least the first 14 octets as a list; fits tells if hs + len octets are in;
463# cut splits into the payload [hs, hs + len) and the input from hs + len on; unmask XORs a mask key.
464def unmask.when(~P: Type, ~unmask: @+key:U32 -> P -> P, m: Bool, +key: U32, p: P) -> P:
465 match m:
466 case True{}:
467 unmask(key, p)
468 case False{}:
469 p
470
471def next.got(~P: Type, ~S: Type, ~unmask: @+key:U32 -> P -> P, +fin: Bool, +op: U32, +m: Bool, +key: U32, r: P & S) -> Decode<P, S>:
472 (payload, rest) = r
473 Got{Frame{fin, op, unmask.when(~P, ~unmask, m, key, payload)}, rest}
474
475def next.fits(~P: Type, ~S: Type, ~cut: S -> @+hs:U32 -> @+len:U32 -> P & S, ~unmask: @+key:U32 -> P -> P, +fin: Bool, +op: U32, +m: Bool, +key: U32, +hs: U32, +len: U32, r: S & Bool) -> Decode<P, S>:
476 (b, ok) = r
477 match ok:
478 case True{}:
479 next.got(~P, ~S, ~unmask, fin, op, m, key, cut(b, hs, len))
480 case False{}:
481 Need{b}
482
483# over: the payload is longer than max.
484def next.size(~P: Type, ~S: Type, ~fits: S -> @+hs:U32 -> @+len:U32 -> S & Bool, ~cut: S -> @+hs:U32 -> @+len:U32 -> P & S, ~unmask: @+key:U32 -> P -> P, over: Bool, +fin: Bool, +op: U32, +m: Bool, +key: U32, +hs: U32, +len: U32, b: S) -> Decode<P, S>:
485 match over:
486 case True{}:
487 Bad{1009, "frame over the size limit"}
488 case False{}:
489 next.fits(~P, ~S, ~cut, ~unmask, fin, op, m, key, hs, len, fits(b, hs, len))
490
491def next.head(~P: Type, ~S: Type, ~fits: S -> @+hs:U32 -> @+len:U32 -> S & Bool, ~cut: S -> @+hs:U32 -> @+len:U32 -> P & S, ~unmask: @+key:U32 -> P -> P, +max: U32, h: Header, b: S) -> Decode<P, S>:
492 match h:
493 case HNeed{}:
494 Need{b}
495 case HBad{code, why}:
496 Bad{code, why}
497 case HOk{+fin, +op, +m, +key, +hs, +len}:
498 next.size(~P, ~S, ~fits, ~cut, ~unmask, U32.is_lt(max, len), fin, op, m, key, hs, len, b)
499
500def next.start(~P: Type, ~S: Type, ~fits: S -> @+hs:U32 -> @+len:U32 -> S & Bool, ~cut: S -> @+hs:U32 -> @+len:U32 -> P & S, ~unmask: @+key:U32 -> P -> P, +masked: Bool, +max: U32, r: S & List<&2, U32>) -> Decode<P, S>:
501 (b, p) = r
502 next.head(~P, ~S, ~fits, ~cut, ~unmask, max, header(p, masked), b)
503
504# One frame from the front of b, unmasked. masked: this peer's frames must be masked
505# (true on a server, false on a client). max caps the payload length (1009 over it).
506def next(~P: Type, ~S: Type, ~prefix: S -> S & List<&2, U32>, ~fits: S -> @+hs:U32 -> @+len:U32 -> S & Bool, ~cut: S -> @+hs:U32 -> @+len:U32 -> P & S, ~unmask: @+key:U32 -> P -> P, +masked: Bool, +max: U32, b: S) -> Decode<P, S>:
507 next.start(~P, ~S, ~fits, ~cut, ~unmask, masked, max, prefix(b))
508
509# The Bytes operations. The input is a cursor: the octets in [pos, end) are not decoded
510# yet. A frame moves pos past its octets; the octets stay in place, and only its payload is copied.
511
512def bytes.prefix.con(+v: U32, r: Bytes.Bytes & List<&2, U32>) -> Bytes.Bytes & List<&2, U32>:
513 (b, t) = r
514 (b, Con{v, t})
515
516def bytes.prefix.go(n: Nat, r: Bytes.Bytes & Maybe<&2, U32>, +i: U32) -> Bytes.Bytes & List<&2, U32>:
517 match n:
518 case 0n:
519 (b, x) = r
520 (b, Nil{})
521 case 1n+p:
522 (b, x) = r
523 match x:
524 case None{}:
525 (b, Nil{})
526 case Some{+v}:
527 bytes.prefix.con(v, bytes.prefix.go(p, Bytes.get(b, (i + 1 : U32)), (i + 1 : U32)))
528
529def bytes.prefix.back(+pos: U32, +start: U32, +end: U32, r: Bytes.Bytes & List<&2, U32>) -> Bytes.Cursor & List<&2, U32>:
530 (b, t) = r
531 (Bytes.Cursor{b, pos, start, end}, t)
532
533def bytes.prefix(c: Bytes.Cursor) -> Bytes.Cursor & List<&2, U32>:
534 Bytes.Cursor{b, +pos, +start, +end} = c
535 bytes.prefix.back(pos, start, end, bytes.prefix.go(U32.to_nat(U32.min(14, (end - pos : U32))), Bytes.get(b, pos), pos))
536
537# hs + len octets fit in end - pos exactly when this holds (Bytes law fits_exact); see law cut_exact.
538def bytes.fits(c: Bytes.Cursor, +hs: U32, +len: U32) -> Bytes.Cursor & Bool:
539 Bytes.Cursor{b, +pos, +start, +end} = c
540 (Bytes.Cursor{b, pos, start, end}, Bytes.fits((end - pos : U32), hs, len))
541
542def bytes.cut.rest(+pos: U32, +start: U32, +end: U32, r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes & Bytes.Cursor:
543 (b, payload) = r
544 (payload, Bytes.Cursor{b, pos, start, end})
545
546def bytes.cut(c: Bytes.Cursor, +hs: U32, +len: U32) -> Bytes.Bytes & Bytes.Cursor:
547 Bytes.Cursor{b, +pos, +start, +end} = c
548 +at = (pos + hs : U32)
549 bytes.cut.rest((at + len : U32), start, end, Bytes.slice(b, at, len))
550
551def bytes.unmask(+key: U32, b: Bytes.Bytes) -> Bytes.Bytes:
552 mask(key, b)
553
554# The decoder over Bytes, as recv runs it.
555def parse(+masked: Bool, +max: U32, c: Bytes.Cursor) -> Decode<Bytes.Bytes, Bytes.Cursor>:
556 next(~Bytes.Bytes, ~Bytes.Cursor, ~bytes.prefix, ~bytes.fits, ~bytes.cut, ~bytes.unmask, masked, max, c)
557
558def push.when(whole: Bool, b: Bytes.Bytes, +pos: U32, +end: U32, read: Bytes.Bytes) -> Bytes.Cursor:
559 match whole:
560 case True{}:
561 Bytes.Cursor.new(Bytes.append(b, read))
562 case False{}:
563 Bytes.Cursor.new(Bytes.append(Bytes.snd(Bytes.slice(b, pos, (end - pos : U32))), read))
564
565# The input with a read after it. Decoded octets are dropped first, so each octet is
566# copied once for the frame it ends up in; when there are none, the read goes into the same buffer.
567def push(c: Bytes.Cursor, read: Bytes.Bytes) -> Bytes.Cursor:
568 Bytes.Cursor{Bytes.Bytes{+n, buf}, +pos, start, +end} = c
569 push.when(Bool.and(U32.is_eq(pos, 0), U32.is_eq(end, n)), Bytes.Bytes{n, buf}, pos, end, read)
570
571# The list operations: the model that PROOF.bend proves the decoder on.
572
573def list.prefix(xs: List<&2, U32>) -> List<&2, U32> & List<&2, U32>:
574 +ys = xs
575 (ys, ys)
576
577def list.fits(xs: List<&2, U32>, +hs: U32, +len: U32) -> List<&2, U32> & Bool:
578 +ys = xs
579 (ys, Nat.is_le(Nat.add(U32.to_nat(hs), U32.to_nat(len)), List.length(&2, U32, ys)))
580
581def list.cut(xs: List<&2, U32>, +hs: U32, +len: U32) -> List<&2, U32> & List<&2, U32>:
582 +ys = xs
583 (List.take(&2, U32, List.drop(&2, U32, ys, U32.to_nat(hs)), U32.to_nat(len)),
584 List.drop(&2, U32, ys, Nat.add(U32.to_nat(hs), U32.to_nat(len))))
585
586# Octet i goes XOR key byte i mod 4; the key turns one byte per octet.
587def list.unmask.go(xs: List<&2, U32>, +key: U32) -> List<&2, U32>:
588 match xs:
589 case Nil{}:
590 Nil{}
591 case Con{+x, t}:
592 Con{(x .^. (key .&. 255 : U32) : U32), list.unmask.go(t, ((key >> 8n) .|. (key << 24n) : U32))}
593
594def list.unmask(+key: U32, xs: List<&2, U32>) -> List<&2, U32>:
595 list.unmask.go(xs, key)
596
597def list.next(+masked: Bool, +max: U32, xs: List<&2, U32>) -> Decode<List<&2, U32>, List<&2, U32>>:
598 next(~List<&2, U32>, ~List<&2, U32>, ~list.prefix, ~list.fits, ~list.cut, ~list.unmask, masked, max, xs)
599
600# UTF-8 (RFC 3629) validity. The state packs need | lo << 8 | hi << 16: continuation
601# bytes still needed and the range the next one must fall in. need 255 is a failure.
602def st(+need: U32, +lo: U32, +hi: U32) -> U32:
603 (need .|. (lo << 8n) .|. (hi << 16n) : U32)
604
605def utf8.lead(+b: U32) -> U32:
606 Bool.pick(U32, U32.is_lt(b, 128), st(0, 128, 191),
607 Bool.pick(U32, U32.is_lt(b, 194), 255,
608 Bool.pick(U32, U32.is_lt(b, 224), st(1, 128, 191),
609 Bool.pick(U32, U32.is_eq(b, 224), st(2, 160, 191),
610 Bool.pick(U32, U32.is_eq(b, 237), st(2, 128, 159),
611 Bool.pick(U32, U32.is_lt(b, 240), st(2, 128, 191),
612 Bool.pick(U32, U32.is_eq(b, 240), st(3, 144, 191),
613 Bool.pick(U32, U32.is_lt(b, 244), st(3, 128, 191),
614 Bool.pick(U32, U32.is_eq(b, 244), st(3, 128, 143), 255)))))))))
615
616def utf8.next(+s: U32, +b: U32) -> U32:
617 +need = (s .&. 255 : U32)
618 Bool.pick(U32, U32.is_eq(need, 255), 255,
619 Bool.pick(U32, U32.is_eq(need, 0), utf8.lead(b),
620 Bool.pick(U32, Bool.and(U32.is_le(((s >> 8n) .&. 255 : U32), b), U32.is_le(b, (s >> 16n : U32))),
621 st((need - 1 : U32), 128, 191), 255)))
622
623def utf8.go(n: Nat, r: Array<U32> & U32, +i: U32, +s: U32) -> Array<U32> & Bool:
624 match n:
625 case 0n:
626 (a, v) = r
627 (a, U32.is_eq((s .&. 255 : U32), 0))
628 case 1n+p:
629 (a, +b) = r
630 +j = (i + 1 : U32)
631 utf8.go(p, Bytes.peek(a, j), j, utf8.next(s, b))
632
633def utf8.fin(+len: U32, r: Array<U32> & Bool) -> Bytes.Bytes & Bool:
634 (a, ok) = r
635 (Bytes.Bytes{len, a}, ok)
636
637# b back, and whether it is well-formed UTF-8.
638def utf8.valid(b: Bytes.Bytes) -> Bytes.Bytes & Bool:
639 Bytes.Bytes{+len, buf} = b
640 utf8.fin(len, utf8.go(U32.to_nat(len), Bytes.peek(buf, 0), 0, st(0, 128, 191)))
641
642# Messages (§5.4): fragments join into one message; control frames may come between them.
643
644type Partial is Type:
645 Idle{}
646 Open{op: U32, data: Bytes.Bytes}
647
648type Msg is Type:
649 Message{op: U32, data: Bytes.Bytes}
650 Control{op: U32, data: Bytes.Bytes}
651 More{}
652
653def done.text(ok: Bytes.Bytes & Bool) -> Result<&1, &1, U32 & String, Partial & Msg>:
654 (d, v) = ok
655 match v:
656 case True{}:
657 Done{(Idle{}, Message{1, d})}
658 case False{}:
659 Fail{(1007, "text message is not UTF-8")}
660
661def finish(+op: U32, d: Bytes.Bytes) -> Result<&1, &1, U32 & String, Partial & Msg>:
662 match op:
663 case 1:
664 done.text(utf8.valid(d))
665 case +o:
666 Done{(Idle{}, Message{o, d})}
667
668def feed.more(fin: Bool, +op: U32, d: Bytes.Bytes) -> Result<&1, &1, U32 & String, Partial & Msg>:
669 match fin:
670 case True{}:
671 finish(op, d)
672 case False{}:
673 Done{(Open{op, d}, More{})}
674
675def feed.size(over: Bool, +fin: Bool, +op: U32, d: Bytes.Bytes) -> Result<&1, &1, U32 & String, Partial & Msg>:
676 match over:
677 case True{}:
678 Fail{(1009, "message over the size limit")}
679 case False{}:
680 feed.more(fin, op, d)
681
682def feed.join(+fin: Bool, +op: U32, d: Bytes.Bytes, +max: U32) -> Result<&1, &1, U32 & String, Partial & Msg>:
683 Bytes.Bytes{+n, buf} = d
684 feed.size(U32.is_gt(n, max), fin, op, Bytes.Bytes{n, buf})
685
686def feed.data(p: Partial, +fin: Bool, +op: U32, d: Bytes.Bytes, +max: U32) -> Result<&1, &1, U32 & String, Partial & Msg>:
687 match p:
688 case Idle{}:
689 match op:
690 case 0:
691 Fail{(1002, "continuation frame without a message")}
692 case +o:
693 feed.more(fin, o, d)
694 case Open{+o, acc}:
695 match op:
696 case 0:
697 feed.join(fin, o, Bytes.append(acc, d), max)
698 case _:
699 Fail{(1002, "data frame inside a fragmented message")}
700
701def feed.kind(ctl: Bool, p: Partial, +fin: Bool, +op: U32, d: Bytes.Bytes, +max: U32) -> Result<&1, &1, U32 & String, Partial & Msg>:
702 match ctl:
703 case True{}:
704 Done{(p, Control{op, d})}
705 case False{}:
706 feed.data(p, fin, op, d, max)
707
708# One parsed frame into the message being built. A whole text message must be UTF-8
709# (1007); max caps a message's total size (1009). Keep max at or below 2^31.
710def feed(p: Partial, f: Frame<Bytes.Bytes>, +max: U32) -> Result<&1, &1, U32 & String, Partial & Msg>:
711 Frame{+fin, +op, d} = f
712 feed.kind(U32.is_ge(op, 8), p, fin, op, d, max)
713
714# Close payloads (§5.5.1, §7.4).
715
716# code (big-endian) then a UTF-8 reason.
717def close.payload(+code: U32, reason: Bytes.Bytes) -> Bytes.Bytes:
718 Bytes.append(Bytes.set.u16be(Bytes.new(2), 0, code), reason)
719
720# Codes a peer may send: §7.4.1, the IANA registry through 1014, and 3000-4999.
721def close.code.ok(+c: U32) -> Bool:
722 Bool.or(Bool.and(U32.is_ge(c, 1000), U32.is_le(c, 1003)),
723 Bool.or(Bool.and(U32.is_ge(c, 1007), U32.is_le(c, 1014)),
724 Bool.and(U32.is_ge(c, 3000), U32.is_le(c, 4999))))
725
726def close.utf8(+c: U32, r: Bytes.Bytes & Bool) -> Result<&1, &1, U32 & String, U32 & Bytes.Bytes>:
727 (b, ok) = r
728 match ok:
729 case True{}:
730 Done{(c, b)}
731 case False{}:
732 Fail{(1007, "close reason is not UTF-8")}
733
734def close.reason(ok: Bool, +c: U32, b: Bytes.Bytes) -> Result<&1, &1, U32 & String, U32 & Bytes.Bytes>:
735 match ok:
736 case False{}:
737 Fail{(1002, "invalid close code")}
738 case True{}:
739 Bytes.Bytes{+n, buf} = b
740 with_slice(Result<&1, &1, U32 & String, U32 & Bytes.Bytes>, Bytes.slice(Bytes.Bytes{n, buf}, 2, (n - 2 : U32)),
741 unused => r => close.utf8(c, utf8.valid(r)))
742
743def close.code(r: Bytes.Bytes & Maybe<&2, U32>) -> Result<&1, &1, U32 & String, U32 & Bytes.Bytes>:
744 (b, m) = r
745 match m:
746 case Some{+c}:
747 close.reason(close.code.ok(c), c, b)
748 case None{}:
749 Fail{(1002, "close payload of one byte")}
750
751# The code and reason of a close frame. An empty payload is 1005 (no status).
752def close.parse(p: Bytes.Bytes) -> Result<&1, &1, U32 & String, U32 & Bytes.Bytes>:
753 Bytes.Bytes{+n, buf} = p
754 match n:
755 case 0:
756 Done{(1005, Bytes.Bytes{0, buf})}
757 case +m:
758 close.code(Bytes.get.u16be(Bytes.Bytes{m, buf}, 0))
759
760# Connections over Wire.
761
762# server: this end is the server (peer frames arrive masked, ours go clear), for a socket
763# an HTTP server upgraded. input holds octets read past the last frame. closing: we sent close.
764type Conn is Type:
765 Conn{sock: Socket, tls: Bool, server: Bool, input: Bytes.Cursor, partial: Partial, max: U32, closing: Bool}
766
767# What recv returns. Ping is answered with a pong inside recv and not returned.
768type Incoming is Type:
769 TextMessage{data: Bytes.Bytes}
770 Binary{data: Bytes.Bytes}
771 Pong{data: Bytes.Bytes}
772 Closed{code: U32, reason: Bytes.Bytes}
773
774def io.send.if(tls: Bool, sock: Socket, +len: U32, buf: Array<U32>) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
775 match tls:
776 case True{}:
777 Wire.tls.send.words(sock, len, buf)
778 case False{}:
779 Wire.send.words(sock, len, buf)
780
781def io.send(sock: Socket, +tls: Bool, b: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
782 Bytes.Bytes{+len, buf} = b
783 io.send.if(tls, sock, len, buf)
784
785def io.recv(tls: Bool, sock: Socket, +ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>):
786 match tls:
787 case True{}:
788 Wire.tls.recv.words(sock, 65536, ms)
789 case False{}:
790 Wire.recv.words(sock, 65536, ms)
791
792def io.close(tls: Bool, sock: Socket) -> IO(Unit):
793 match tls:
794 case True{}:
795 Wire.tls.close(sock)
796 case False{}:
797 Socket.close(sock)
798
799type Head is Type:
800 HRead{r: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>, acc: Bytes.Bytes}
801 HSplit{sock: Socket, s: Split}
802
803def head.loop(n: Nat, h: Head, +tls: Bool, +ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>):
804 match n:
805 case 0n:
806 match h:
807 case HRead{r, acc}:
808 (sock, x) = r
809 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
810 return (sock, Fail{(1002, "HTTP head took too many reads")})
811 case HSplit{sock, s}:
812 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
813 return (sock, Fail{(1002, "HTTP head took too many reads")})
814 case 1n+p:
815 match h:
816 case HRead{r, acc}:
817 match r:
818 case (sock, Fail{e}):
819 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
820 return (sock, Fail{e})
821 case (sock, Done{(0, buf)}):
822 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
823 return (sock, Fail{(1006, "connection closed before the HTTP head ended")})
824 case (sock, Done{(+len, buf)}):
825 head.loop(p, HSplit{sock, split(Bytes.append(acc, Bytes.Bytes{len, buf}))}, tls, ms)
826 case HSplit{sock, s}:
827 match s:
828 case Found{head, rest}:
829 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
830 return (sock, Done{(head, rest)})
831 case Long{}:
832 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
833 return (sock, Fail{(1002, "HTTP head over 16 KiB")})
834 case Short{acc}:
835 do IO<Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>>:
836 r : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv(tls, sock, ms)
837 head.loop(p, HRead{r, acc}, tls, ms)
838
839# Reads an HTTP head: the text before its blank line, and the bytes after it.
840def head.read(sock: Socket, +tls: Bool, +ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes>):
841 head.loop(256n, HSplit{sock, Short{Bytes.new(0)}}, tls, ms)
842
843def hs.fail(sock: Socket, +tls: Bool, e: U32 & String) -> IO(Result<&1, &1, U32 & String, Conn>):
844 do IO<Result<&1, &1, U32 & String, Conn>>:
845 io.close(tls, sock)
846 return Fail{e}
847
848def 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>):
849 match v:
850 case Fail{e}:
851 hs.fail(sock, tls, e)
852 case Done{u}:
853 do IO<Result<&1, &1, U32 & String, Conn>>:
854 return Done{Conn{sock, tls, False{}, Bytes.Cursor.new(rest), Idle{}, max, False{}}}
855
856def 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>):
857 match r:
858 case (sock, Fail{e}):
859 hs.fail(sock, tls, e)
860 case (sock, Done{(+head, rest)}):
861 hs.checked(check(head, want), sock, tls, max, rest)
862
863def 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>):
864 match r:
865 case (sock, Fail{e}):
866 hs.fail(sock, tls, e)
867 case (sock, Done{u}):
868 do IO<Result<&1, &1, U32 & String, Conn>>:
869 h : Socket & Result<&1, &1, U32 & String, String & Bytes.Bytes> <- head.read(sock, tls, ms)
870 hs.head(h, tls, max, want)
871
872def 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>):
873 match q:
874 case Fail{e}:
875 hs.fail(sock, tls, e)
876 case Done{b}:
877 do IO<Result<&1, &1, U32 & String, Conn>>:
878 r : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(sock, tls, b)
879 hs.sent(r, tls, max, ms, want)
880
881def 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>):
882 match a:
883 case Fail{e}:
884 hs.fail(sock, tls, e)
885 case Done{+want}:
886 hs.request(request(host, path, key), sock, tls, max, ms, want)
887
888def 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>):
889 match k:
890 case Fail{e}:
891 hs.fail(sock, tls, e)
892 case Done{+key}:
893 do IO<Result<&1, &1, U32 & String, Conn>>:
894 a : Result<&1, &1, U32 & String, String> <- accept(key)
895 hs.accepted(a, sock, tls, host, path, max, ms, key)
896
897# The opening handshake on a connected socket (TLS already up when tls). host is the Host
898# header and path the request target. max caps frame and message sizes. On failure the
899# socket is closed. Bytes the server sent after its head stay in the Conn.
900def handshake(sock: Socket, +tls: Bool, +host: String, +path: String, +max: U32, +ms: U32) -> IO(Result<&1, &1, U32 & String, Conn>):
901 do IO<Result<&1, &1, U32 & String, Conn>>:
902 k : Result<&1, &1, U32 & String, String> <- key()
903 hs.keyed(k, sock, tls, host, path, max, ms)
904
905def 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>):
906 match r:
907 case (sock, Fail{e}):
908 hs.fail(sock, False{}, e)
909 case (sock, Done{u}):
910 handshake(sock, True{}, authority, path, max, ms)
911
912def 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>):
913 match c:
914 case Fail{e}:
915 do IO<Result<&1, &1, U32 & String, Conn>>:
916 return Fail{e}
917 case Done{sock}:
918 match tls:
919 case True{}:
920 do IO<Result<&1, &1, U32 & String, Conn>>:
921 t : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.connect(sock, host, ms)
922 connect.tls(t, authority, path, max, ms)
923 case False{}:
924 handshake(sock, False{}, authority, path, max, ms)
925
926# ws:// (tls false) or wss:// to a numeric address (resolve names with dns). host is the
927# server name, for Host and TLS verification. ms bounds each socket step.
928def connect(+addr: String, +port: U32, +host: String, +path: String, +tls: Bool, +max: U32, +ms: U32) -> IO(Result<&1, &1, U32 & String, Conn>):
929 +std = U32.is_eq(port, Bool.pick(U32, tls, 443, 80))
930 +authority = Bool.pick(String, std, host, host ++ ":" ++ U32.show(port))
931 do IO<Result<&1, &1, U32 & String, Conn>>:
932 c : Result<&1, &1, U32 & String, Socket> <- Wire.connect(addr, port, ms)
933 connect.tcp(c, tls, host, authority, path, max, ms)
934
935def raw.encoded(e: Result<&1, &1, U32 & String, Bytes.Bytes>, sock: Socket, +tls: Bool) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
936 match e:
937 case Fail{err}:
938 do IO<Socket & Result<&1, &1, U32 & String, Unit>>:
939 return (sock, Fail{err})
940 case Done{b}:
941 io.send(sock, tls, b)
942
943def 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>):
944 (a, +key) = r
945 raw.encoded(encode(Frame{fin, op, payload}, Some{key}), sock, tls)
946
947def 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>):
948 match k:
949 case Fail{e}:
950 do IO<Socket & Result<&1, &1, U32 & String, Unit>>:
951 return (sock, Fail{e})
952 case Done{(n, a)}:
953 raw.key(Array.get(U32, a, 0), sock, tls, fin, op, payload)
954
955# A client masks every frame with a fresh key from the OS secure random source (§5.3).
956def raw(server: Bool, sock: Socket, +tls: Bool, +fin: Bool, +op: U32, payload: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
957 match server:
958 case True{}:
959 raw.encoded(encode(Frame{fin, op, payload}, None{}), sock, tls)
960 case False{}:
961 do IO<Socket & Result<&1, &1, U32 & String, Unit>>:
962 k : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.random.words(4)
963 raw.keyed(k, sock, tls, fin, op, payload)
964
965def back(r: Socket & Result<&1, &1, U32 & String, Unit>, +tls: Bool, +server: Bool, input: Bytes.Cursor, partial: Partial, +max: U32, +closing: Bool) -> Conn & Result<&1, &1, U32 & String, Unit>:
966 (sock, x) = r
967 (Conn{sock, tls, server, input, partial, max, closing}, x)
968
969# Sends one frame: fin false starts or continues a fragmented message (later frames use op 0).
970def send(c: Conn, +fin: Bool, +op: U32, payload: Bytes.Bytes) -> IO(Conn & Result<&1, &1, U32 & String, Unit>):
971 Conn{sock, +tls, +server, input, partial, +max, +closing} = c
972 do IO<Conn & Result<&1, &1, U32 & String, Unit>>:
973 r : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, fin, op, payload)
974 return back(r, tls, server, input, partial, max, closing)
975
976# Sends a close frame; recv then runs until the peer's close comes back as Closed.
977def close(c: Conn, +code: U32, reason: Bytes.Bytes) -> IO(Conn & Result<&1, &1, U32 & String, Unit>):
978 Conn{sock, +tls, +server, input, partial, +max, +closing} = c
979 do IO<Conn & Result<&1, &1, U32 & String, Unit>>:
980 r : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, True{}, 8, close.payload(code, reason))
981 return back(r, tls, server, input, partial, max, True{})
982
983# Closes the socket (and its TLS session).
984def shutdown(c: Conn) -> IO(Unit):
985 Conn{sock, tls, server, input, partial, max, closing} = c
986 io.close(tls, sock)
987
988type Step is Type:
989 Parse{sock: Socket, input: Bytes.Cursor, partial: Partial}
990 Decoded{sock: Socket, partial: Partial, d: Decode<Bytes.Bytes, Bytes.Cursor>}
991 Fed{sock: Socket, rest: Bytes.Cursor, r: Result<&1, &1, U32 & String, Partial & Msg>}
992 Read{r: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>, input: Bytes.Cursor, partial: Partial}
993 Ponged{r: Socket & Result<&1, &1, U32 & String, Unit>, input: Bytes.Cursor, partial: Partial}
994
995def recv.out(sock: Socket, +tls: Bool, +server: Bool, input: Bytes.Cursor, partial: Partial, +max: U32, +closing: Bool, r: Result<&1, &1, U32 & String, Incoming>) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
996 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
997 return (Conn{sock, tls, server, input, partial, max, closing}, r)
998
999def 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>):
1000 (sock, x) = r
1001 recv.out(sock, tls, server, Bytes.Cursor.new(Bytes.new(0)), Idle{}, max, True{}, Fail{e})
1002
1003# A peer broke the protocol: send close with its code (§7.1.7), then report it.
1004def recv.fail(sock: Socket, +tls: Bool, +server: Bool, +max: U32, e: U32 & String) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
1005 (+code, why) = e
1006 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
1007 r : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, True{}, 8, close.payload(code, Bytes.new(0)))
1008 recv.failed(r, tls, server, max, (code, why))
1009
1010def recv.echoed(r: Socket & Result<&1, &1, U32 & String, Unit>, +tls: Bool, +server: Bool, rest: Bytes.Cursor, partial: Partial, +max: U32, +code: U32, reason: Bytes.Bytes) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
1011 (sock, x) = r
1012 recv.out(sock, tls, server, rest, partial, max, True{}, Done{Closed{code, reason}})
1013
1014def recv.closed(r: Result<&1, &1, U32 & String, U32 & Bytes.Bytes>, sock: Socket, +tls: Bool, +server: Bool, rest: Bytes.Cursor, partial: Partial, +max: U32, closing: Bool) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
1015 match r:
1016 case Fail{e}:
1017 recv.fail(sock, tls, server, max, e)
1018 case Done{(+code, reason)}:
1019 match closing:
1020 case True{}:
1021 recv.out(sock, tls, server, rest, partial, max, True{}, Done{Closed{code, reason}})
1022 case False{}:
1023 echo = Bool.pick(Bytes.Bytes, U32.is_eq(code, 1005), Bytes.new(0), close.payload(code, Bytes.new(0)))
1024 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
1025 s : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, True{}, 8, echo)
1026 recv.echoed(s, tls, server, rest, partial, max, code, reason)
1027
1028def recv.stuck(h: Step, +tls: Bool, +server: Bool, +max: U32) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
1029 match h:
1030 case Parse{sock, input, partial}:
1031 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
1032 case Decoded{sock, partial, d}:
1033 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
1034 case Fed{sock, rest, r}:
1035 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
1036 case Read{r, input, partial}:
1037 (sock, x) = r
1038 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
1039 case Ponged{r, input, partial}:
1040 (sock, x) = r
1041 recv.fail(sock, tls, server, max, (1011, "frame budget exhausted"))
1042
1043def recv.loop(n: Nat, h: Step, +tls: Bool, +server: Bool, +max: U32, +closing: Bool, +ms: U32) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
1044 match n:
1045 case 0n:
1046 recv.stuck(h, tls, server, max)
1047 case 1n+p:
1048 match h:
1049 case Parse{sock, input, partial}:
1050 recv.loop(p, Decoded{sock, partial, parse(server, max, input)}, tls, server, max, closing, ms)
1051 case Decoded{sock, partial, d}:
1052 match d:
1053 case Need{input}:
1054 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
1055 r : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv(tls, sock, ms)
1056 recv.loop(p, Read{r, input, partial}, tls, server, max, closing, ms)
1057 case Bad{+code, why}:
1058 recv.fail(sock, tls, server, max, (code, why))
1059 case Got{f, rest}:
1060 recv.loop(p, Fed{sock, rest, feed(partial, f, max)}, tls, server, max, closing, ms)
1061 case Fed{sock, rest, r}:
1062 match r:
1063 case Fail{e}:
1064 recv.fail(sock, tls, server, max, e)
1065 case Done{(partial, ev)}:
1066 match ev:
1067 case More{}:
1068 recv.loop(p, Parse{sock, rest, partial}, tls, server, max, closing, ms)
1069 case Message{1, d}:
1070 recv.out(sock, tls, server, rest, partial, max, closing, Done{TextMessage{d}})
1071 case Message{op, d}:
1072 recv.out(sock, tls, server, rest, partial, max, closing, Done{Binary{d}})
1073 case Control{9, d}:
1074 do IO<Conn & Result<&1, &1, U32 & String, Incoming>>:
1075 s : Socket & Result<&1, &1, U32 & String, Unit> <- raw(server, sock, tls, True{}, 10, d)
1076 recv.loop(p, Ponged{s, rest, partial}, tls, server, max, closing, ms)
1077 case Control{10, d}:
1078 recv.out(sock, tls, server, rest, partial, max, closing, Done{Pong{d}})
1079 case Control{op, d}:
1080 recv.closed(close.parse(d), sock, tls, server, rest, partial, max, closing)
1081 case Read{r, input, partial}:
1082 match r:
1083 case (sock, Fail{e}):
1084 recv.out(sock, tls, server, input, partial, max, closing, Fail{e})
1085 case (sock, Done{(0, buf)}):
1086 recv.out(sock, tls, server, input, partial, max, closing, Fail{(1006, "connection closed without a close frame")})
1087 case (sock, Done{(+len, buf)}):
1088 recv.loop(p, Parse{sock, push(input, Bytes.Bytes{len, buf}), partial}, tls, server, max, closing, ms)
1089 case Ponged{r, input, partial}:
1090 match r:
1091 case (sock, Fail{e}):
1092 recv.out(sock, tls, server, input, partial, max, closing, Fail{e})
1093 case (sock, Done{u}):
1094 recv.loop(p, Parse{sock, input, partial}, tls, server, max, closing, ms)
1095
1096# The next message, pong, or close. Fragments are joined and pings answered on the way.
1097# A protocol fault sends close with its code and fails with it. ms bounds each read.
1098def recv(c: Conn, +ms: U32) -> IO(Conn & Result<&1, &1, U32 & String, Incoming>):
1099 Conn{sock, +tls, +server, input, partial, +max, +closing} = c
1100 recv.loop(U32.to_nat(16777216), Parse{sock, input, partial}, tls, server, max, closing, ms)