bend-kit-websocket Releases (6): 0.4.0.0 0x17030e400bb458b9f30b76fb230026a8 indexed https://jend.leeeet.dev/files.txt?path=bend-kit-websocket@0.4.0.0 0.3.0.1 0xd3a8227bb088fbb88eaf453ee7cd660a unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-websocket@0.3.0.1 0.3.0.0 0x3203e8e8b1f5bad19dfc5a52014642af unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-websocket@0.3.0.0 0.2.0.1 0xa62177ca680fb4d3408fedd3cc24c3e6 invalid https://jend.leeeet.dev/files.txt?path=bend-kit-websocket@0.2.0.1 expected a fresh constructor name (duplicate declaration: Text) At https://jend.leeeet.dev/read.txt?path=bend-kit-websocket@0.2.0.1/websocket.bend&start_line=769. Files that do not load: websocket.bend. 0.2.0.0 0x47923dd1ad3a8d9d2cddf5f98ac7ca93 invalid https://jend.leeeet.dev/files.txt?path=bend-kit-websocket@0.2.0.0 expected a fresh constructor name (duplicate declaration: Text) At https://jend.leeeet.dev/read.txt?path=bend-kit-websocket@0.2.0.0/websocket.bend&start_line=769. Files that do not load: websocket.bend. 0.1.0.0 0x6ff0f96d54a186e76b90f54fca91949f invalid https://jend.leeeet.dev/files.txt?path=bend-kit-websocket@0.1.0.0 expected a fresh constructor name (duplicate declaration: Text) At https://jend.leeeet.dev/read.txt?path=bend-kit-websocket@0.1.0.0/websocket.bend&start_line=630. Files that do not load: websocket.bend. Definitions (148, 1 to 100 shown): Websocket.guid (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=guid) def guid() -> String: Websocket.accept.input (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=accept.input) # The octets SHA-1 hashes for Sec-WebSocket-Accept: the key, then the GUID. def accept.input(key: String) -> Bytes.Bytes: Websocket.accept.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=accept.of) # Sec-WebSocket-Accept from the SHA-1 digest of accept.input(key). def accept.of(digest: Bytes.Bytes) -> String: Websocket.accept.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=accept.fin) def accept.fin(r: Result<&1, &1, U32 & String, U32 & Array>) -> Result<&1, &1, U32 & String, String>: Websocket.accept.words (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=accept.words) def accept.words(b: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, U32 & Array>): Websocket.accept (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=accept) # The Sec-WebSocket-Accept a server must answer to key. def accept(key: String) -> IO(Result<&1, &1, U32 & String, String>): Websocket.key.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=key.of) # Sec-WebSocket-Key from a 16-octet nonce. def key.of(nonce: Bytes.Bytes) -> String: Websocket.key.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=key.fin) def key.fin(r: Result<&1, &1, U32 & String, U32 & Array>) -> Result<&1, &1, U32 & String, String>: Websocket.key (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=key) # A fresh key from 16 octets of the OS secure random source. def key() -> IO(Result<&1, &1, U32 & String, String>): Websocket.first (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=first) def first(m: Maybe<&1, U32 & String>, n: Maybe<&1, U32 & String>) -> Maybe<&1, U32 & String>: Websocket.reject (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=reject) def reject(bad: Bool, +code: U32, +why: String) -> Maybe<&1, U32 & String>: Websocket.verdict (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=verdict) def verdict(-A: Type, m: Maybe<&1, U32 & String>, v: A) -> Result<&1, &1, U32 & String, A>: Websocket.visible (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=visible) # Every char is visible ASCII (0x21-0x7E): no space, CR, LF, or other control. def visible(s: String) -> Bool: Websocket.request (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=request) # 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 request(+host: String, +path: String, +key: String) -> Result<&1, &1, U32 & String, Bytes.Bytes>: Websocket.fields.line (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=fields.line) def fields.line(parts: List<&2, String>, +name: String, +later: List<&2, String>) -> List<&2, String>: Websocket.fields.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=fields.go) def fields.go(ls: List<&2, String>, +name: String) -> List<&2, String>: Websocket.after.first (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=after.first) def after.first(ls: List<&2, String>) -> List<&2, String>: Websocket.headers (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=headers) # The header lines of an HTTP head: every line after the start line. def headers(head: String) -> List<&2, String>: Websocket.fields (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=fields) # The trimmed values of every header line named name (lowercase), in order. def fields(head: String, +name: String) -> List<&2, String>: Websocket.only (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=only) def only(xs: List<&2, String>) -> Maybe<&2, String>: Websocket.field (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=field) # The value of the header named name when exactly one line has it. def field(head: String, +name: String) -> Maybe<&2, String>: Websocket.line.parts (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=line.parts) # 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 line.parts(parts: List<&2, String>) -> Bool: Websocket.lines.ok (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=lines.ok) def lines.ok(ls: List<&2, String>) -> Bool: Websocket.status.parts (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=status.parts) def status.parts(parts: List<&2, String>) -> Bool: Websocket.status (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=status) # The first line is exactly "HTTP/1.1 101" and a reason, with nothing before it. def status(ls: List<&2, String>) -> Bool: Websocket.token (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=token) def token(xs: List<&2, String>, +want: String) -> Bool: Websocket.value.is (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=value.is) def value.is(m: Maybe<&2, String>, +want: String) -> Bool: Websocket.value.lower (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=value.lower) def value.lower(m: Maybe<&2, String>) -> Maybe<&2, String>: Websocket.tokens (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=tokens) # Connection is a list header: its lines join into one comma list (RFC 9110 §5.3). def tokens(xs: List<&2, String>, +want: String) -> Bool: Websocket.none (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=none) def none(xs: List<&2, String>) -> Bool: Websocket.check (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=check) # 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 check(+head: String, +want: String) -> Result<&1, &1, U32 & String, Unit>: Websocket.with_slice (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=with_slice) def with_slice(-R: Type, r: Bytes.Bytes & Bytes.Bytes, k: Bytes.Bytes -> Bytes.Bytes -> R) -> R: Websocket.Split (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=Split) # An HTTP head cut at its blank line, with the bytes after it. type Split is Type: Found{head: String, rest: Bytes.Bytes} Short{acc: Bytes.Bytes} Long{} Websocket.split.long (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=split.long) def split.long(long: Bool, b: Bytes.Bytes) -> Split: Websocket.split.short (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=split.short) def split.short(b: Bytes.Bytes) -> Split: Websocket.split.found (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=split.found) def split.found(r: Bytes.Bytes & Maybe<&2, U32>) -> Split: Websocket.split (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=split) # Found once b holds "\r\n\r\n"; Long when 16 KiB came without it. def split(b: Bytes.Bytes) -> Split: Websocket.Frame (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=Frame) # The payload P is Bytes at run time and a List of octets in the proofs. type Frame<-P: Type> is Type: Frame{fin: Bool, op: U32, payload: P} Websocket.Decode (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=Decode) # 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. type Decode<-P: Type, -S: Type> is Type: Need{input: S} Got{frame: Frame

, rest: S} Bad{code: U32, why: String} Websocket.mask.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=mask.go) def mask.go(n: Nat, r: Array & U32, +i: U32, +key: U32) -> Array: Websocket.mask.trim.word (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=mask.trim.word) def mask.trim.word(+k: U32, +m: U32, r: Array & U32) -> Array: Websocket.mask.trim.if (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=mask.trim.if) def mask.trim.if(whole: Bool, +k: U32, +m: U32, a: Array) -> Array: Websocket.mask.trim (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=mask.trim) # Bytes at or past len stay 0, as Bytes requires. def mask.trim(+len: U32, a: Array) -> Array: Websocket.mask (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=mask) # 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 mask(+key: U32, b: Bytes.Bytes) -> Bytes.Bytes: Websocket.known (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=known) def known(+op: U32) -> Bool: Websocket.rules.big (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=rules.big) # 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.big(+fin: Bool, +rsv: U32, +op: U32, big: Bool) -> Maybe<&1, U32 & String>: Websocket.rules (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=rules) def rules(+fin: Bool, +rsv: U32, +op: U32, +len: U32) -> Maybe<&1, U32 & String>: Websocket.encode.ext (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=encode.ext) def encode.ext(+ext: U32, +len: U32, b: Bytes.Bytes) -> Bytes.Bytes: Websocket.encode.mkey (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=encode.mkey) def encode.mkey(+keylen: U32, +at: U32, +key: U32, b: Bytes.Bytes) -> Bytes.Bytes: Websocket.encode.copy (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=encode.copy) def encode.copy(+len: U32, src: Array, +hs: U32, b: Bytes.Bytes) -> Bytes.Bytes: Websocket.encode.frame (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=encode.frame) # Payload lengths use the shortest form (§5.2): 7 bits, then 16, then 64. def encode.frame(+b0: U32, +mbit: U32, +keylen: U32, +key: U32, p: Bytes.Bytes) -> Bytes.Bytes: Websocket.encode.key (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=encode.key) def encode.key(key: Maybe<&2, U32>, +b0: U32, p: Bytes.Bytes) -> Bytes.Bytes: Websocket.encode.checked (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=encode.checked) 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>: Websocket.encode (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=encode) # 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 encode(f: Frame, key: Maybe<&2, U32>) -> Result<&1, &1, U32 & String, Bytes.Bytes>: Websocket.Header (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=Header) # 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. type Header is Data: HNeed{} HBad{code: U32, why: String} HOk{fin: Bool, op: U32, m: Bool, key: U32, hs: U32, len: U32} Websocket.header.verdict (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=header.verdict) def header.verdict(err: Maybe<&1, U32 & String>, +fin: Bool, +op: U32, +m: Bool, +key: U32, +hs: U32, +len: U32) -> Header: Websocket.header.err (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=header.err) # A 64-bit length with a high word is over any U32 max, and is a control frame over 125. def header.err(+masked: Bool, +b0: U32, +m: Bool, +hi: U32, +len: U32) -> Maybe<&1, U32 & String>: Websocket.header.check (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=header.check) def header.check(+masked: Bool, +b0: U32, +m: Bool, +key: U32, +hs: U32, +hi: U32, +len: U32) -> Header: Websocket.header.key (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=header.key) # The mask key (§5.3) follows the length; its first octet is the key's low byte. def header.key(m: Bool, t: List<&2, U32>, +masked: Bool, +b0: U32, +hs: U32, +hi: U32, +len: U32) -> Header: Websocket.be32 (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=be32) def be32(+a: U32, +b: U32, +c: U32, +d: U32) -> U32: Websocket.header.ext16 (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=header.ext16) def header.ext16(t: List<&2, U32>, +masked: Bool, +b0: U32, +m: Bool) -> Header: Websocket.header.ext64 (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=header.ext64) def header.ext64(t: List<&2, U32>, +masked: Bool, +b0: U32, +m: Bool) -> Header: Websocket.header.ext (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=header.ext) # short: no extended length (l7 < 126); mid: 2 octets of it (l7 == 126); else 8. def header.ext(short: Bool, mid: Bool, t: List<&2, U32>, +masked: Bool, +b0: U32, +m: Bool, +l7: U32) -> Header: Websocket.header.b1 (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=header.b1) def header.b1(m: Bool, t: List<&2, U32>, +masked: Bool, +b0: U32, +b1: U32) -> Header: Websocket.header (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=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 header(p: List<&2, U32>, +masked: Bool) -> Header: Websocket.unmask.when (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=unmask.when) # 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. def unmask.when(~P: Type, ~unmask: @+key:U32 -> P -> P, m: Bool, +key: U32, p: P) -> P: Websocket.next.got (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=next.got) def next.got(~P: Type, ~S: Type, ~unmask: @+key:U32 -> P -> P, +fin: Bool, +op: U32, +m: Bool, +key: U32, r: P & S) -> Decode: Websocket.next.fits (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=next.fits) 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: Websocket.next.size (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=next.size) # over: the payload is longer than max. 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: Websocket.next.head (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=next.head) 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: Websocket.next.start (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=next.start) 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: Websocket.next (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=next) # 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). 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: Websocket.bytes.prefix.con (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=bytes.prefix.con) def bytes.prefix.con(+v: U32, r: Bytes.Bytes & List<&2, U32>) -> Bytes.Bytes & List<&2, U32>: Websocket.bytes.prefix.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=bytes.prefix.go) def bytes.prefix.go(n: Nat, r: Bytes.Bytes & Maybe<&2, U32>, +i: U32) -> Bytes.Bytes & List<&2, U32>: Websocket.bytes.prefix.back (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=bytes.prefix.back) def bytes.prefix.back(+pos: U32, +start: U32, +end: U32, r: Bytes.Bytes & List<&2, U32>) -> Bytes.Cursor & List<&2, U32>: Websocket.bytes.prefix (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=bytes.prefix) def bytes.prefix(c: Bytes.Cursor) -> Bytes.Cursor & List<&2, U32>: Websocket.bytes.fits (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=bytes.fits) # hs + len octets fit in end - pos exactly when this holds (Bytes law fits_exact); see law cut_exact. def bytes.fits(c: Bytes.Cursor, +hs: U32, +len: U32) -> Bytes.Cursor & Bool: Websocket.bytes.cut.rest (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=bytes.cut.rest) def bytes.cut.rest(+pos: U32, +start: U32, +end: U32, r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes & Bytes.Cursor: Websocket.bytes.cut (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=bytes.cut) def bytes.cut(c: Bytes.Cursor, +hs: U32, +len: U32) -> Bytes.Bytes & Bytes.Cursor: Websocket.bytes.unmask (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=bytes.unmask) def bytes.unmask(+key: U32, b: Bytes.Bytes) -> Bytes.Bytes: Websocket.parse (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=parse) # The decoder over Bytes, as recv runs it. def parse(+masked: Bool, +max: U32, c: Bytes.Cursor) -> Decode: Websocket.push.when (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=push.when) def push.when(whole: Bool, b: Bytes.Bytes, +pos: U32, +end: U32, read: Bytes.Bytes) -> Bytes.Cursor: Websocket.push (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=push) # 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 push(c: Bytes.Cursor, read: Bytes.Bytes) -> Bytes.Cursor: Websocket.list.prefix (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=list.prefix) def list.prefix(xs: List<&2, U32>) -> List<&2, U32> & List<&2, U32>: Websocket.list.fits (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=list.fits) def list.fits(xs: List<&2, U32>, +hs: U32, +len: U32) -> List<&2, U32> & Bool: Websocket.list.cut (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=list.cut) def list.cut(xs: List<&2, U32>, +hs: U32, +len: U32) -> List<&2, U32> & List<&2, U32>: Websocket.list.unmask.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=list.unmask.go) # Octet i goes XOR key byte i mod 4; the key turns one byte per octet. def list.unmask.go(xs: List<&2, U32>, +key: U32) -> List<&2, U32>: Websocket.list.unmask (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=list.unmask) def list.unmask(+key: U32, xs: List<&2, U32>) -> List<&2, U32>: Websocket.list.next (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=list.next) def list.next(+masked: Bool, +max: U32, xs: List<&2, U32>) -> Decode, List<&2, U32>>: Websocket.st (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=st) # 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 st(+need: U32, +lo: U32, +hi: U32) -> U32: Websocket.utf8.lead (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=utf8.lead) def utf8.lead(+b: U32) -> U32: Websocket.utf8.next (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=utf8.next) def utf8.next(+s: U32, +b: U32) -> U32: Websocket.utf8.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=utf8.go) def utf8.go(n: Nat, r: Array & U32, +i: U32, +s: U32) -> Array & Bool: Websocket.utf8.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=utf8.fin) def utf8.fin(+len: U32, r: Array & Bool) -> Bytes.Bytes & Bool: Websocket.utf8.valid (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=utf8.valid) # b back, and whether it is well-formed UTF-8. def utf8.valid(b: Bytes.Bytes) -> Bytes.Bytes & Bool: Websocket.Partial (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=Partial) type Partial is Type: Idle{} Open{op: U32, data: Bytes.Bytes} Websocket.Msg (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=Msg) type Msg is Type: Message{op: U32, data: Bytes.Bytes} Control{op: U32, data: Bytes.Bytes} More{} Websocket.done.text (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=done.text) def done.text(ok: Bytes.Bytes & Bool) -> Result<&1, &1, U32 & String, Partial & Msg>: Websocket.finish (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=finish) def finish(+op: U32, d: Bytes.Bytes) -> Result<&1, &1, U32 & String, Partial & Msg>: Websocket.feed.more (https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=feed.more) def feed.more(fin: Bool, +op: U32, d: Bytes.Bytes) -> Result<&1, &1, U32 & String, Partial & Msg>: More: https://jend.leeeet.dev/packages/bend-kit-websocket.txt?definitions_offset=100