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