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
2	import Base
3	import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
4	import bend-kit-crypto@0.2.2.1/crypto.bend as Crypto
5	import 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	
14	def guid() -> String:
15	  "258EAFA5-E914-47DA-95CA-C5AB0DC85B11"
16	
17	# The octets SHA-1 hashes for Sec-WebSocket-Accept: the key, then the GUID.
18	def 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).
22	def accept.of(digest: Bytes.Bytes) -> String:
23	  Bytes.to_base64(digest)
24	
25	def 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	
32	def 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.
37	def 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.
43	def key.of(nonce: Bytes.Bytes) -> String:
44	  Bytes.to_base64(nonce)
45	
46	def 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.
54	def 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	
59	def 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	
66	def 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	
73	def 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.
81	def 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).
91	def 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	
100	def 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	
108	def 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	
115	def 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.
123	def 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.
127	def fields(head: String, +name: String) -> List<&2, String>:
128	  fields.go(headers(head), name)
129	
130	def 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.
138	def 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.
143	def 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	
150	def 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	
157	def 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.
165	def 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	
172	def 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	
179	def 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	
186	def 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).
194	def 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	
201	def 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).
211	def 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	
222	def 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.
227	type Split is Type:
228	  Found{head: String, rest: Bytes.Bytes}
229	  Short{acc: Bytes.Bytes}
230	  Long{}
231	
232	def split.long(long: Bool, b: Bytes.Bytes) -> Split:
233	  match long:
234	    case True{}:
235	      Long{}
236	    case False{}:
237	      Short{b}
238	
239	def 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	
243	def 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.
254	def 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.
260	type 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.
265	type 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	
270	def 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	
280	def 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	
284	def 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.
292	def 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.
298	def 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	
302	def 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.
321	def 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	
327	def 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	
330	def 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	
339	def 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	
346	def 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.
351	def 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	
359	def 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	
366	def 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.
375	def 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.
382	type 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	
387	def 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.
395	def 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	
400	def 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.
404	def 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	
415	def be32(+a: U32, +b: U32, +c: U32, +d: U32) -> U32:
416	  ((a << 24n) .|. (b << 16n) .|. (c << 8n) .|. d : U32)
417	
418	def 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	
425	def 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.
433	def 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	
444	def 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.
454	def 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.
464	def 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	
471	def 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	
475	def 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.
484	def 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	
491	def 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	
500	def 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).
506	def 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	
512	def 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	
516	def 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	
529	def 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	
533	def 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.
538	def 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	
542	def 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	
546	def 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	
551	def bytes.unmask(+key: U32, b: Bytes.Bytes) -> Bytes.Bytes:
552	  mask(key, b)
553	
554	# The decoder over Bytes, as recv runs it.
555	def 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	
558	def 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.
567	def 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	
573	def list.prefix(xs: List<&2, U32>) -> List<&2, U32> & List<&2, U32>:
574	  +ys = xs
575	  (ys, ys)
576	
577	def 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	
581	def 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.
587	def 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	
594	def list.unmask(+key: U32, xs: List<&2, U32>) -> List<&2, U32>:
595	  list.unmask.go(xs, key)
596	
597	def 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.
602	def st(+need: U32, +lo: U32, +hi: U32) -> U32:
603	  (need .|. (lo << 8n) .|. (hi << 16n) : U32)
604	
605	def 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	
616	def 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	
623	def 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	
633	def 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.
638	def 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	
644	type Partial is Type:
645	  Idle{}
646	  Open{op: U32, data: Bytes.Bytes}
647	
648	type Msg is Type:
649	  Message{op: U32, data: Bytes.Bytes}
650	  Control{op: U32, data: Bytes.Bytes}
651	  More{}
652	
653	def 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	
661	def 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	
668	def 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	
675	def 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	
682	def 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	
686	def 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	
701	def 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.
710	def 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.
717	def 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.
721	def 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	
726	def 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	
734	def 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	
743	def 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).
752	def 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.
764	type 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.
768	type 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	
774	def 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	
781	def 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	
785	def 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	
792	def 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	
799	type 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	
803	def 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.
840	def 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	
843	def 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	
848	def 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	
856	def 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	
863	def 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	
872	def 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	
881	def 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	
888	def 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.
900	def 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	
905	def 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	
912	def 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.
928	def 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	
935	def 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	
943	def 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	
947	def 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).
956	def 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	
965	def 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).
970	def 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.
977	def 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).
984	def shutdown(c: Conn) -> IO(Unit):
985	  Conn{sock, tls, server, input, partial, max, closing} = c
986	  io.close(tls, sock)
987	
988	type 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	
995	def 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	
999	def 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.
1004	def 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	
1010	def 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	
1014	def 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	
1028	def 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	
1043	def 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.
1098	def 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)