websocket.bend relies on unsafe/foreign
raw source on the hub · import bend-kit-websocket@0.2.0.0/websocket.bend as Websocket
RFC 6455 WebSocket client: opening handshake, frames over packed Bytes, and messages over Wire. Source: https://github.com/paymog/bend-kit/tree/main/websocket
4 imports
import Base import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes import bend-kit-crypto@0.1.0.0/crypto.bend as Crypto import bend-kit-wire@0.4.2.0/wire.bend as Wire
Types
type Split source · line 227 · raw
Type
An HTTP head cut at its blank line, with the bytes after it.
Found@head:String -> @rest:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Split
Short@acc:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Split
LongSplit
type Frame source · line 260 · raw
@-P:Type -> Type
The payload P is Bytes at run time and a List of octets in the proofs.
Frame@-P:Type -> @fin:Bool -> @op:U32 -> @payload:P -> Frame<P>
type Decode source · line 265 · raw
@-P:Type -> @-S:Type -> Type
Need: the input does not hold a whole frame yet, and comes back intact. Got: one frame, and the octets after it. Bad: the input breaks §5.2 whatever comes next.
Need@-P:Type -> @-S:Type -> @input:S -> Decode<P, S>
Got@-P:Type -> @-S:Type -> @frame:Frame<P> -> @rest:S -> Decode<P, S>
Bad@-P:Type -> @-S:Type -> @code:U32 -> @why:String -> Decode<P, S>
type Header source · line 382 · raw
Data
A frame header, read from a list of the first octets of the input. Ok: hs header octets, then len payload octets, masked with key when m.
HNeedHeader
HBad@code:U32 -> @why:String -> Header
HOk@fin:Bool -> @op:U32 -> @m:Bool -> @key:U32 -> @hs:U32 -> @len:U32 -> Header
type Partial source · line 644 · raw
Type
IdlePartial
Open@op:U32 -> @data:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Partial
type Msg source · line 648 · raw
Type
Message@op:U32 -> @data:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Msg
Control@op:U32 -> @data:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Msg
MoreMsg
type Conn source · line 764 · raw
Type
server: this end is the server (peer frames arrive masked, ours go clear), for a socket an HTTP server upgraded. input holds octets read past the last frame. closing: we sent close.
Conn@sock:Socket -> @tls:Bool -> @server:Bool -> @input:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @partial:Partial -> @max:U32 -> @closing:Bool -> Conn
type Incoming source · line 768 · raw
Type
What recv returns. Ping is answered with a pong inside recv and not returned.
Text@data:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Incoming
Binary@data:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Incoming
Pong@data:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Incoming
Closed@code:U32 -> @reason:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Incoming
type Head source · line 799 · raw
Type
HRead@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Pair(U32, Array<U32>)>) -> @acc:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Head
HSplit@sock:Socket -> @s:Split -> Head
type Step source · line 988 · raw
Type
Parse@sock:Socket -> @input:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @partial:Partial -> Step
Decoded@sock:Socket -> @partial:Partial -> @d:Decode<0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor> -> Step
Fed@sock:Socket -> @rest:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @r:Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)> -> Step
Read@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Pair(U32, Array<U32>)>) -> @input:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @partial:Partial -> Step
Ponged@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>) -> @input:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @partial:Partial -> Step
Definitions
def guid source · line 14 · raw
String
def accept.input source · line 18 · raw
@key:String -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
The octets SHA-1 hashes for Sec-WebSocket-Accept: the key, then the GUID.
def accept.of source · line 22 · raw
@digest:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> String
Sec-WebSocket-Accept from the SHA-1 digest of accept.input(key).
def accept.fin source · line 25 · raw
@r:Result<&1, &1, Pair(U32, String), Pair(U32, Array<U32>)> -> Result<&1, &1, Pair(U32, String), String>
def accept.words source · line 32 · raw
@b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Result<&1, &1, Pair(U32, String), Pair(U32, Array<U32>)>)
def accept source · line 37 · raw
@key:String -> IO(Result<&1, &1, Pair(U32, String), String>)
The Sec-WebSocket-Accept a server must answer to key.
def key.of source · line 43 · raw
@nonce:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> String
Sec-WebSocket-Key from a 16-octet nonce.
def key.fin source · line 46 · raw
@r:Result<&1, &1, Pair(U32, String), Pair(U32, Array<U32>)> -> Result<&1, &1, Pair(U32, String), String>
def key source · line 54 · raw
IO(Result<&1, &1, Pair(U32, String), String>)
A fresh key from 16 octets of the OS secure random source.
def first source · line 59 · raw
@m:Maybe<&1, Pair(U32, String)> -> @n:Maybe<&1, Pair(U32, String)> -> Maybe<&1, Pair(U32, String)>
def reject source · line 66 · raw
@bad:Bool -> @+code:U32 -> @+why:String -> Maybe<&1, Pair(U32, String)>
def verdict source · line 73 · raw
@-A:Type -> @m:Maybe<&1, Pair(U32, String)> -> @v:A -> Result<&1, &1, Pair(U32, String), A>
def visible source · line 81 · raw
@s:String -> Bool
Every char is visible ASCII (0x21-0x7E): no space, CR, LF, or other control.
def request source · line 91 · raw
@+host:String -> @+path:String -> @+key:String -> Result<&1, &1, Pair(U32, String), 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes>
The GET that asks to upgrade. host is the Host header (with :port when not the default); path is the origin-form target ("/" and on, percent-encoded). A char outside visible ASCII could split the head and inject headers, so it fails with EINVAL (22).
def fields.line source · line 100 · raw
@parts:List<&2, String> -> @+name:String -> @+later:List<&2, String> -> List<&2, String>
def fields.go source · line 108 · raw
@ls:List<&2, String> -> @+name:String -> List<&2, String>
def after.first source · line 115 · raw
@ls:List<&2, String> -> List<&2, String>
def headers source · line 123 · raw
@head:String -> List<&2, String>
The header lines of an HTTP head: every line after the start line.
def fields source · line 127 · raw
@head:String -> @+name:String -> List<&2, String>
The trimmed values of every header line named name (lowercase), in order.
def only source · line 130 · raw
@xs:List<&2, String> -> Maybe<&2, String>
def field source · line 138 · raw
@head:String -> @+name:String -> Maybe<&2, String>
The value of the header named name when exactly one line has it.
def line.parts source · line 143 · raw
@parts:List<&2, String> -> Bool
A header line is name ":" value, with a non-empty name that holds no space or tab (RFC 9112 §5.1). That rules out obsolete line folding and bare text.
def lines.ok source · line 150 · raw
@ls:List<&2, String> -> Bool
def status.parts source · line 157 · raw
@parts:List<&2, String> -> Bool
def status source · line 165 · raw
@ls:List<&2, String> -> Bool
The first line is exactly "HTTP/1.1 101" and a reason, with nothing before it.
def token source · line 172 · raw
@xs:List<&2, String> -> @+want:String -> Bool
def value.is source · line 179 · raw
@m:Maybe<&2, String> -> @+want:String -> Bool
def value.lower source · line 186 · raw
@m:Maybe<&2, String> -> Maybe<&2, String>
def tokens source · line 194 · raw
@xs:List<&2, String> -> @+want:String -> Bool
Connection is a list header: its lines join into one comma list (RFC 9110 §5.3).
def none source · line 201 · raw
@xs:List<&2, String> -> Bool
def check source · line 211 · raw
@+head:String -> @+want:String -> Result<&1, &1, Pair(U32, String), Unit>
Does a server's head (up to its blank line) accept the upgrade? want is accept(key). Upgrade and Sec-WebSocket-Accept must each come once. No extension or subprotocol was asked for, so the server may name none (§4.1).
def with_slice source · line 222 · raw
@-R:Type -> @r:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes) -> @k:(@_:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> @_:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> R) -> R
def split.long source · line 232 · raw
@long:Bool -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Split
def split.short source · line 239 · raw
@b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Split
def split.found source · line 243 · raw
@r:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, Maybe<&2, U32>) -> Split
def split source · line 254 · raw
@b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Split
Found once b holds "\r\n\r\n"; Long when 16 KiB came without it.
def mask.go source · line 270 · raw
@n:Nat -> @r:Pair(Array<U32>, U32) -> @+i:U32 -> @+key:U32 -> Array<U32>
def mask.trim.word source · line 280 · raw
@+k:U32 -> @+m:U32 -> @r:Pair(Array<U32>, U32) -> Array<U32>
def mask.trim.if source · line 284 · raw
@whole:Bool -> @+k:U32 -> @+m:U32 -> @a:Array<U32> -> Array<U32>
def mask.trim source · line 292 · raw
@+len:U32 -> @a:Array<U32> -> Array<U32>
Bytes at or past len stay 0, as Bytes requires.
def mask source · line 298 · raw
@+key:U32 -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
The payload XOR the mask key (§5.3), a word at a time. key's byte k (low first) is mask octet k. Masking twice gives the payload back.
def known source · line 302 · raw
@+op:U32 -> Bool
def rules.big source · line 321 · raw
@+fin:Bool -> @+rsv:U32 -> @+op:U32 -> @big:Bool -> Maybe<&1, Pair(U32, String)>
The §5.2 and §5.5 rules on a frame header. No extension is in use, so RSV must be 0. big: the payload is over 125 octets.
def rules source · line 327 · raw
@+fin:Bool -> @+rsv:U32 -> @+op:U32 -> @+len:U32 -> Maybe<&1, Pair(U32, String)>
def encode.ext source · line 330 · raw
@+ext:U32 -> @+len:U32 -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
def encode.mkey source · line 339 · raw
@+keylen:U32 -> @+at:U32 -> @+key:U32 -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
def encode.copy source · line 346 · raw
@+len:U32 -> @src:Array<U32> -> @+hs:U32 -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
def encode.frame source · line 351 · raw
@+b0:U32 -> @+mbit:U32 -> @+keylen:U32 -> @+key:U32 -> @p:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
Payload lengths use the shortest form (§5.2): 7 bits, then 16, then 64.
def encode.key source · line 359 · raw
@key:Maybe<&2, U32> -> @+b0:U32 -> @p:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
def encode.checked source · line 366 · raw
@err:Maybe<&1, Pair(U32, String)> -> @+fin:Bool -> @+op:U32 -> @key:Maybe<&2, U32> -> @p:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Result<&1, &1, Pair(U32, String), 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes>
def encode source · line 375 · raw
@f:Frame<0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes> -> @key:Maybe<&2, U32> -> Result<&1, &1, Pair(U32, String), 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes>
A frame's octets. A client passes Some{mask key} and the payload goes masked; None sends it clear, as a server does. Fails on a frame that breaks rules.
def header.verdict source · line 387 · raw
@err:Maybe<&1, Pair(U32, String)> -> @+fin:Bool -> @+op:U32 -> @+m:Bool -> @+key:U32 -> @+hs:U32 -> @+len:U32 -> Header
def header.err source · line 395 · raw
@+masked:Bool -> @+b0:U32 -> @+m:Bool -> @+hi:U32 -> @+len:U32 -> Maybe<&1, Pair(U32, String)>
A 64-bit length with a high word is over any U32 max, and is a control frame over 125.
def header.check source · line 400 · raw
@+masked:Bool -> @+b0:U32 -> @+m:Bool -> @+key:U32 -> @+hs:U32 -> @+hi:U32 -> @+len:U32 -> Header
def header.key source · line 404 · raw
@m:Bool -> @t:List<&2, U32> -> @+masked:Bool -> @+b0:U32 -> @+hs:U32 -> @+hi:U32 -> @+len:U32 -> Header
The mask key (§5.3) follows the length; its first octet is the key's low byte.
def be32 source · line 415 · raw
@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> U32
def header.ext16 source · line 418 · raw
@t:List<&2, U32> -> @+masked:Bool -> @+b0:U32 -> @+m:Bool -> Header
def header.ext64 source · line 425 · raw
@t:List<&2, U32> -> @+masked:Bool -> @+b0:U32 -> @+m:Bool -> Header
def header.ext source · line 433 · raw
@short:Bool -> @mid:Bool -> @t:List<&2, U32> -> @+masked:Bool -> @+b0:U32 -> @+m:Bool -> @+l7:U32 -> Header
short: no extended length (l7 < 126); mid: 2 octets of it (l7 == 126); else 8.
def header.b1 source · line 444 · raw
@m:Bool -> @t:List<&2, U32> -> @+masked:Bool -> @+b0:U32 -> @+b1:U32 -> Header
def header source · line 454 · raw
@p:List<&2, U32> -> @+masked:Bool -> Header
The header at the front of p, from octets below 256. It reads at most 14 octets, and is HNeed until all of them are in p. It is checked as soon as it is whole, before its payload.
def bytes.prefix.con source · line 512 · raw
@+v:U32 -> @r:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, List<&2, U32>) -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, List<&2, U32>)
def bytes.prefix.go source · line 516 · raw
@n:Nat -> @r:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, Maybe<&2, U32>) -> @+i:U32 -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, List<&2, U32>)
def bytes.prefix.back source · line 529 · raw
@+pos:U32 -> @+start:U32 -> @+end:U32 -> @r:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, List<&2, U32>) -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, List<&2, U32>)
def bytes.prefix source · line 533 · raw
@c:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, List<&2, U32>)
def bytes.fits source · line 538 · raw
@c:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @+hs:U32 -> @+len:U32 -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, Bool)
hs + len octets fit in end - pos exactly when this holds (Bytes law fits_exact); see law cut_exact.
def bytes.cut.rest source · line 542 · raw
@+pos:U32 -> @+start:U32 -> @+end:U32 -> @r:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes) -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor)
def bytes.cut source · line 546 · raw
@c:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @+hs:U32 -> @+len:U32 -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor)
def bytes.unmask source · line 551 · raw
@+key:U32 -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
def parse source · line 555 · raw
@+masked:Bool -> @+max:U32 -> @c:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> Decode<0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor>
The decoder over Bytes, as recv runs it.
def push.when source · line 558 · raw
@whole:Bool -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> @+pos:U32 -> @+end:U32 -> @read:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor
def push source · line 567 · raw
@c:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @read:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor
The input with a read after it. Decoded octets are dropped first, so each octet is copied once for the frame it ends up in; when there are none, the read goes into the same buffer.
def list.prefix source · line 573 · raw
@xs:List<&2, U32> -> Pair(List<&2, U32>, List<&2, U32>)
def list.fits source · line 577 · raw
@xs:List<&2, U32> -> @+hs:U32 -> @+len:U32 -> Pair(List<&2, U32>, Bool)
def list.cut source · line 581 · raw
@xs:List<&2, U32> -> @+hs:U32 -> @+len:U32 -> Pair(List<&2, U32>, List<&2, U32>)
def list.unmask.go source · line 587 · raw
@xs:List<&2, U32> -> @+key:U32 -> List<&2, U32>
Octet i goes XOR key byte i mod 4; the key turns one byte per octet.
def list.unmask source · line 594 · raw
@+key:U32 -> @xs:List<&2, U32> -> List<&2, U32>
def list.next source · line 597 · raw
@+masked:Bool -> @+max:U32 -> @xs:List<&2, U32> -> Decode<List<&2, U32>, List<&2, U32>>
def st source · line 602 · raw
@+need:U32 -> @+lo:U32 -> @+hi:U32 -> U32
UTF-8 (RFC 3629) validity. The state packs need | lo << 8 | hi << 16: continuation bytes still needed and the range the next one must fall in. need 255 is a failure.
def utf8.lead source · line 605 · raw
@+b:U32 -> U32
def utf8.next source · line 616 · raw
@+s:U32 -> @+b:U32 -> U32
def utf8.go source · line 623 · raw
@n:Nat -> @r:Pair(Array<U32>, U32) -> @+i:U32 -> @+s:U32 -> Pair(Array<U32>, Bool)
def utf8.fin source · line 633 · raw
@+len:U32 -> @r:Pair(Array<U32>, Bool) -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, Bool)
def utf8.valid source · line 638 · raw
@b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, Bool)
b back, and whether it is well-formed UTF-8.
def done.text source · line 653 · raw
@ok:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, Bool) -> Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)>
def finish source · line 661 · raw
@+op:U32 -> @d:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)>
def feed.more source · line 668 · raw
@fin:Bool -> @+op:U32 -> @d:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)>
def feed.size source · line 675 · raw
@over:Bool -> @+fin:Bool -> @+op:U32 -> @d:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)>
def feed.join source · line 682 · raw
@+fin:Bool -> @+op:U32 -> @d:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> @+max:U32 -> Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)>
def feed.data source · line 686 · raw
@p:Partial -> @+fin:Bool -> @+op:U32 -> @d:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> @+max:U32 -> Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)>
def feed.kind source · line 701 · raw
@ctl:Bool -> @p:Partial -> @+fin:Bool -> @+op:U32 -> @d:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> @+max:U32 -> Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)>
def feed source · line 710 · raw
@p:Partial -> @f:Frame<0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes> -> @+max:U32 -> Result<&1, &1, Pair(U32, String), Pair(Partial, Msg)>
One parsed frame into the message being built. A whole text message must be UTF-8 (1007); max caps a message's total size (1009). Keep max at or below 2^31.
def close.payload source · line 717 · raw
@+code:U32 -> @reason:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes
code (big-endian) then a UTF-8 reason.
def close.code.ok source · line 721 · raw
@+c:U32 -> Bool
Codes a peer may send: §7.4.1, the IANA registry through 1014, and 3000-4999.
def close.utf8 source · line 726 · raw
@+c:U32 -> @r:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, Bool) -> Result<&1, &1, Pair(U32, String), Pair(U32, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes)>
def close.reason source · line 734 · raw
@ok:Bool -> @+c:U32 -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Result<&1, &1, Pair(U32, String), Pair(U32, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes)>
def close.code source · line 743 · raw
@r:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, Maybe<&2, U32>) -> Result<&1, &1, Pair(U32, String), Pair(U32, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes)>
def close.parse source · line 752 · raw
@p:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> Result<&1, &1, Pair(U32, String), Pair(U32, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes)>
The code and reason of a close frame. An empty payload is 1005 (no status).
def io.send.if source · line 774 · raw
@tls:Bool -> @sock:Socket -> @+len:U32 -> @buf:Array<U32> -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>))
def io.send source · line 781 · raw
@sock:Socket -> @+tls:Bool -> @b:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>))
def io.recv source · line 785 · raw
@tls:Bool -> @sock:Socket -> @+ms:U32 -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Pair(U32, Array<U32>)>))
def io.close source · line 792 · raw
@tls:Bool -> @sock:Socket -> IO(Unit)
def head.loop source · line 803 · raw
@n:Nat -> @h:Head -> @+tls:Bool -> @+ms:U32 -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Pair(String, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes)>))
def head.read source · line 840 · raw
@sock:Socket -> @+tls:Bool -> @+ms:U32 -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Pair(String, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes)>))
Reads an HTTP head: the text before its blank line, and the bytes after it.
def hs.fail source · line 843 · raw
@sock:Socket -> @+tls:Bool -> @e:Pair(U32, String) -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def hs.checked source · line 848 · raw
@v:Result<&1, &1, Pair(U32, String), Unit> -> @sock:Socket -> @+tls:Bool -> @+max:U32 -> @rest:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def hs.head source · line 856 · raw
@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Pair(String, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes)>) -> @+tls:Bool -> @+max:U32 -> @+want:String -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def hs.sent source · line 863 · raw
@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>) -> @+tls:Bool -> @+max:U32 -> @+ms:U32 -> @+want:String -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def hs.request source · line 872 · raw
@q:Result<&1, &1, Pair(U32, String), 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes> -> @sock:Socket -> @+tls:Bool -> @+max:U32 -> @+ms:U32 -> @+want:String -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def hs.accepted source · line 881 · raw
@a:Result<&1, &1, Pair(U32, String), String> -> @sock:Socket -> @+tls:Bool -> @+host:String -> @+path:String -> @+max:U32 -> @+ms:U32 -> @+key:String -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def hs.keyed source · line 888 · raw
@k:Result<&1, &1, Pair(U32, String), String> -> @sock:Socket -> @+tls:Bool -> @+host:String -> @+path:String -> @+max:U32 -> @+ms:U32 -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def handshake source · line 900 · raw
@sock:Socket -> @+tls:Bool -> @+host:String -> @+path:String -> @+max:U32 -> @+ms:U32 -> IO(Result<&1, &1, Pair(U32, String), Conn>)
The opening handshake on a connected socket (TLS already up when tls). host is the Host header and path the request target. max caps frame and message sizes. On failure the socket is closed. Bytes the server sent after its head stay in the Conn.
def connect.tls source · line 905 · raw
@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>) -> @+authority:String -> @+path:String -> @+max:U32 -> @+ms:U32 -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def connect.tcp source · line 912 · raw
@c:Result<&1, &1, Pair(U32, String), Socket> -> @+tls:Bool -> @+host:String -> @+authority:String -> @+path:String -> @+max:U32 -> @+ms:U32 -> IO(Result<&1, &1, Pair(U32, String), Conn>)
def connect source · line 928 · raw
@+addr:String -> @+port:U32 -> @+host:String -> @+path:String -> @+tls:Bool -> @+max:U32 -> @+ms:U32 -> IO(Result<&1, &1, Pair(U32, String), Conn>)
ws:// (tls false) or wss:// to a numeric address (resolve names with dns). host is the server name, for Host and TLS verification. ms bounds each socket step.
def raw.encoded source · line 935 · raw
@e:Result<&1, &1, Pair(U32, String), 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes> -> @sock:Socket -> @+tls:Bool -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>))
def raw.key source · line 943 · raw
@r:Pair(Array<U32>, U32) -> @sock:Socket -> @+tls:Bool -> @+fin:Bool -> @+op:U32 -> @payload:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>))
def raw.keyed source · line 947 · raw
@k:Result<&1, &1, Pair(U32, String), Pair(U32, Array<U32>)> -> @sock:Socket -> @+tls:Bool -> @+fin:Bool -> @+op:U32 -> @payload:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>))
def raw source · line 956 · raw
@server:Bool -> @sock:Socket -> @+tls:Bool -> @+fin:Bool -> @+op:U32 -> @payload:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>))
A client masks every frame with a fresh key from the OS secure random source (§5.3).
def back source · line 965 · raw
@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>) -> @+tls:Bool -> @+server:Bool -> @input:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @partial:Partial -> @+max:U32 -> @+closing:Bool -> Pair(Conn, Result<&1, &1, Pair(U32, String), Unit>)
def send source · line 970 · raw
@c:Conn -> @+fin:Bool -> @+op:U32 -> @payload:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Unit>))
Sends one frame: fin false starts or continues a fragmented message (later frames use op 0).
def close source · line 977 · raw
@c:Conn -> @+code:U32 -> @reason:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Unit>))
Sends a close frame; recv then runs until the peer's close comes back as Closed.
def shutdown source · line 984 · raw
@c:Conn -> IO(Unit)
Closes the socket (and its TLS session).
def recv.out source · line 995 · raw
@sock:Socket -> @+tls:Bool -> @+server:Bool -> @input:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @partial:Partial -> @+max:U32 -> @+closing:Bool -> @r:Result<&1, &1, Pair(U32, String), Incoming> -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Incoming>))
def recv.failed source · line 999 · raw
@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>) -> @+tls:Bool -> @+server:Bool -> @+max:U32 -> @e:Pair(U32, String) -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Incoming>))
def recv.fail source · line 1004 · raw
@sock:Socket -> @+tls:Bool -> @+server:Bool -> @+max:U32 -> @e:Pair(U32, String) -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Incoming>))
A peer broke the protocol: send close with its code (§7.1.7), then report it.
def recv.echoed source · line 1010 · raw
@r:Pair(Socket, Result<&1, &1, Pair(U32, String), Unit>) -> @+tls:Bool -> @+server:Bool -> @rest:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @partial:Partial -> @+max:U32 -> @+code:U32 -> @reason:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Incoming>))
def recv.closed source · line 1014 · raw
@r:Result<&1, &1, Pair(U32, String), Pair(U32, 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes)> -> @sock:Socket -> @+tls:Bool -> @+server:Bool -> @rest:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @partial:Partial -> @+max:U32 -> @closing:Bool -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Incoming>))
def recv.stuck source · line 1028 · raw
@h:Step -> @+tls:Bool -> @+server:Bool -> @+max:U32 -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Incoming>))
def recv.loop source · line 1043 · raw
@n:Nat -> @h:Step -> @+tls:Bool -> @+server:Bool -> @+max:U32 -> @+closing:Bool -> @+ms:U32 -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Incoming>))
def recv source · line 1098 · raw
@c:Conn -> @+ms:U32 -> IO(Pair(Conn, Result<&1, &1, Pair(U32, String), Incoming>))
The next message, pong, or close. Fragments are joined and pings answered on the way. A protocol fault sends close with its code and fails with it. ms bounds each read.
Templates
template unmask.when source · line 464 · raw
@-P:Type -> @-unmask:(@+key:U32 -> @_:P -> P) -> @m:Bool -> @+key:U32 -> @p:P -> P
The decoder, over any input S with four operations, giving payloads P: prefix gives at least the first 14 octets as a list; fits tells if hs + len octets are in; cut splits into the payload [hs, hs + len) and the input from hs + len on; unmask XORs a mask key.
template next.got source · line 471 · raw
@-P:Type -> @-S:Type -> @-unmask:(@+key:U32 -> @_:P -> P) -> @+fin:Bool -> @+op:U32 -> @+m:Bool -> @+key:U32 -> @r:Pair(P, S) -> Decode<P, S>
template next.fits source · line 475 · raw
@-P:Type -> @-S:Type -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(P, S)) -> @-unmask:(@+key:U32 -> @_:P -> P) -> @+fin:Bool -> @+op:U32 -> @+m:Bool -> @+key:U32 -> @+hs:U32 -> @+len:U32 -> @r:Pair(S, Bool) -> Decode<P, S>
template next.size source · line 484 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, Bool)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(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>
over: the payload is longer than max.
template next.head source · line 491 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, Bool)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(P, S)) -> @-unmask:(@+key:U32 -> @_:P -> P) -> @+max:U32 -> @h:Header -> @b:S -> Decode<P, S>
template next.start source · line 500 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, Bool)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(P, S)) -> @-unmask:(@+key:U32 -> @_:P -> P) -> @+masked:Bool -> @+max:U32 -> @r:Pair(S, List<&2, U32>) -> Decode<P, S>
template next source · line 506 · raw
@-P:Type -> @-S:Type -> @-prefix:(@_:S -> Pair(S, List<&2, U32>)) -> @-fits:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, Bool)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(P, S)) -> @-unmask:(@+key:U32 -> @_:P -> P) -> @+masked:Bool -> @+max:U32 -> @b:S -> Decode<P, S>
One frame from the front of b, unmasked. masked: this peer's frames must be masked (true on a server, false on a client). max caps the payload length (1009 over it).