http2.bend source
http2.bend on the hub · documented module
# RFC 9113 HTTP/2 client and frames, with RFC 7541 HPACK over packed Bytes.import Baseimport bend-kit-bytes@0.3.1.0/bytes.bend as Bytesimport ./hpack.bend as Hpacktype Frame is Type: Frame{kind: U32, flags: U32, stream: U32, payload: Bytes.Bytes}type Error is Data: Error{code: U32, connection: Bool, stream: U32}type Decode is Type: Need{input: Bytes.Bytes} Got{frame: Frame, rest: Bytes.Bytes} Bad{error: Error}type Checked is Type: Valid{frame: Frame} Invalid{error: Error}# Error codes from RFC 9113 §7: 1=PROTOCOL_ERROR, 3=FLOW_CONTROL_ERROR,# 6=FRAME_SIZE_ERROR. A connection error uses stream 0.def fail(+code: U32, +connection: Bool, +stream: U32) -> Maybe<&2, Error>: Some{Error{code, connection, Bool.pick(U32, connection, 0, stream)}}def reject(bad: Bool, +code: U32, +connection: Bool, +stream: U32) -> Maybe<&2, Error>: match bad: case True{}: fail(code, connection, stream) case False{}: None{}def first(m: Maybe<&2, Error>, n: Maybe<&2, Error>) -> Maybe<&2, Error>: match m: case Some{e}: Some{e} case None{}: ndef number(m: Maybe<&2, U32>) -> U32: match m: case Some{x}: x case None{}: 0def with_number(-R: Type, r: Bytes.Bytes & Maybe<&2, U32>, k: Bytes.Bytes -> U32 -> R) -> R: (b, m) = r k(b, number(m))def with_slice(-R: Type, r: Bytes.Bytes & Bytes.Bytes, k: Bytes.Bytes -> Bytes.Bytes -> R) -> R: (b, part) = r k(b, part)def has(+flags: U32, +bit: U32) -> Bool: U32.is_ne((flags .&. bit : U32), 0)# Field blocks, SETTINGS, and stream 0 make frame-size faults connection-wide.def size.scope(+kind: U32, +stream: U32) -> Bool: match kind: case 1: True{} case 4: True{} case 5: True{} case 9: True{} case _: U32.is_eq(stream, 0)def size.error(+kind: U32, +stream: U32) -> Error: +connection = size.scope(kind, stream) Error{6, connection, Bool.pick(U32, connection, 0, stream)}def size.reject(oversized: Bool, +kind: U32, +stream: U32) -> Maybe<&2, Error>: match oversized: case True{}: Some{size.error(kind, stream)} case False{}: None{}# A PADDED payload must contain the pad-length octet and all the padding.def padding(+flags: U32, +len: U32, +fixed: U32, +pad: U32) -> Bool: Bool.and(has(flags, 8), Bool.or(U32.is_le(len, fixed), U32.is_gt(pad, (len - fixed - 1 : U32))))def setting(+id: U32, +value: U32) -> Maybe<&2, Error>: match id: case 2: reject(U32.is_gt(value, 1), 1, True{}, 0) case 4: reject(U32.is_gt(value, 2147483647), 3, True{}, 0) case 5: reject(Bool.or(U32.is_lt(value, 16384), U32.is_gt(value, 16777215)), 1, True{}, 0) case _: None{}def settings.go(n: Nat, b: Bytes.Bytes, +at: U32, m: Maybe<&2, Error>) -> Bytes.Bytes & Maybe<&2, Error>: match n: case 0n: (b, m) case 1n+p: with_number(Bytes.Bytes & Maybe<&2, Error>, Bytes.get.u16be(b, at), b => id => with_number(Bytes.Bytes & Maybe<&2, Error>, Bytes.get.u32be(b, (at + 2 : U32)), b => value => settings.go(p, b, (at + 6 : U32), first(m, setting(id, value)))))def rules(+kind: U32, +flags: U32, +stream: U32, +len: U32, +pad: U32, +promised: U32, +value: U32, m: Maybe<&2, Error>) -> Maybe<&2, Error>: match kind: case 0: first(reject(U32.is_eq(stream, 0), 1, True{}, stream), first(reject(Bool.and(has(flags, 8), U32.is_eq(len, 0)), 6, False{}, stream), reject(padding(flags, len, 0, pad), 1, True{}, stream))) case 1: +fixed = Bool.pick(U32, has(flags, 32), 5, 0) +prefix = Bool.pick(U32, has(flags, 8), 1, 0) first(reject(U32.is_eq(stream, 0), 1, True{}, stream), first(reject(U32.is_lt(len, (fixed + prefix : U32)), 6, True{}, stream), reject(padding(flags, len, fixed, pad), 1, True{}, stream))) case 2: first(reject(U32.is_ne(len, 5), 6, U32.is_eq(stream, 0), stream), reject(U32.is_eq(stream, 0), 1, True{}, stream)) case 3: first(reject(U32.is_ne(len, 4), 6, True{}, stream), reject(U32.is_eq(stream, 0), 1, True{}, stream)) case 4: first(reject(U32.is_ne(stream, 0), 1, True{}, stream), first(reject(Bool.and(has(flags, 1), U32.is_ne(len, 0)), 6, True{}, stream), first(reject(U32.is_ne((len % 6 : U32), 0), 6, True{}, stream), m))) case 5: +prefix = Bool.pick(U32, has(flags, 8), 1, 0) first(reject(U32.is_eq(stream, 0), 1, True{}, stream), first(reject(U32.is_lt(len, (prefix + 4 : U32)), 6, True{}, stream), first(reject(padding(flags, len, 4, pad), 1, True{}, stream), reject(U32.is_eq(promised, 0), 1, True{}, stream)))) case 6: first(reject(U32.is_ne(len, 8), 6, True{}, stream), reject(U32.is_ne(stream, 0), 1, True{}, stream)) case 7: first(reject(U32.is_lt(len, 8), 6, True{}, stream), reject(U32.is_ne(stream, 0), 1, True{}, stream)) case 8: first(reject(U32.is_ne(len, 4), 6, U32.is_eq(stream, 0), stream), reject(U32.is_eq((value .&. 2147483647 : U32), 0), 1, U32.is_eq(stream, 0), stream)) case 9: reject(U32.is_eq(stream, 0), 1, True{}, stream) case _: None{}def checked(m: Maybe<&2, Error>, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Checked: match m: case Some{e}: Invalid{e} case None{}: Valid{Frame{kind, flags, stream, b}}def with_settings(r: Bytes.Bytes & Maybe<&2, Error>, +flags: U32, +stream: U32) -> Checked: (b, m) = r checked(m, 4, flags, stream, b)def inspect.settings(m: Maybe<&2, Error>, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked: match m: case Some{e}: Invalid{e} case None{}: with_settings(settings.go(U32.to_nat((len / 6 : U32)), b, 0, None{}), flags, stream)def inspect.promised(+kind: U32, +flags: U32, +stream: U32, +len: U32, +pad: U32, b: Bytes.Bytes) -> Checked: match kind: case 5: +prefix = Bool.pick(U32, has(flags, 8), 1, 0) with_number(Checked, Bytes.get.u32be(b, prefix), b => promised => checked(rules(kind, flags, stream, len, pad, (promised .&. 2147483647 : U32), 0, None{}), kind, flags, stream, b)) case _: checked(rules(kind, flags, stream, len, pad, 0, 0, None{}), kind, flags, stream, b)def inspect.padded.if(padded: Bool, +kind: U32, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked: match padded: case True{}: with_number(Checked, Bytes.get(b, 0), b => pad => inspect.promised(kind, flags, stream, len, pad, b)) case False{}: inspect.promised(kind, flags, stream, len, 0, b)def inspect.padded(+kind: U32, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked: inspect.padded.if(has(flags, 8), kind, flags, stream, len, b)def inspect.detail(+kind: U32, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked: match kind: case 0: inspect.padded(kind, flags, stream, len, b) case 1: inspect.padded(kind, flags, stream, len, b) case 4: inspect.settings(rules(kind, flags, stream, len, 0, 0, 0, None{}), flags, stream, len, b) case 5: inspect.padded(kind, flags, stream, len, b) case 8: with_number(Checked, Bytes.get.u32be(b, 0), b => value => checked(rules(kind, flags, stream, len, 0, 0, value, None{}), kind, flags, stream, b)) case _: checked(rules(kind, flags, stream, len, 0, 0, 0, None{}), kind, flags, stream, b)def inspect.basic(m: Maybe<&2, Error>, +kind: U32, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked: match m: case Some{e}: Invalid{e} case None{}: inspect.detail(kind, flags, stream, len, b)def inspect(max: U32, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Checked: Bytes.Bytes{+len, buf} = b +basic = first(size.reject(Bool.or(U32.is_gt(len, max), U32.is_gt(len, 16777215)), kind, stream), first(reject(U32.is_gt(kind, 255), 1, True{}, stream), first(reject(U32.is_gt(flags, 255), 1, True{}, stream), reject(U32.is_gt(stream, 2147483647), 1, True{}, stream)))) inspect.basic(basic, kind, flags, stream, len, Bytes.Bytes{len, buf})# max is the peer's SETTINGS_MAX_FRAME_SIZE, initially 16384.def allowed(+kind: U32) -> U32: match kind: case 0: 9 case 1: 45 case 2: 0 case 3: 0 case 4: 1 case 5: 12 case 6: 1 case 7: 0 case 8: 0 case 9: 4 case _: 255def encode.buffer(b: Bytes.Bytes, src: Array<U32>, +len: U32) -> Result<&1, &1, Error, Bytes.Bytes>: Bytes.Bytes{_, dst} = b Done{Bytes.Bytes{(len + 9 : U32), Bytes.dst(Bytes.copy(len, src, dst, 0, 9))}}def encode.flags(ok: Bool, +kind: U32, +flags: U32, +stream: U32, payload: Bytes.Bytes) -> Result<&1, &1, Error, Bytes.Bytes>: match ok: case False{}: Fail{Error{1, True{}, 0}} case True{}: Bytes.Bytes{+len, src} = payload encode.buffer(Bytes.set.u32be(Bytes.set(Bytes.set(Bytes.put(Bytes.new((len + 9 : U32)), 0, 3, True{}, len), 3, kind), 4, flags), 5, stream), src, len)def encode.checked(c: Checked) -> Result<&1, &1, Error, Bytes.Bytes>: match c: case Invalid{e}: Fail{e} case Valid{Frame{+kind, +flags, +stream, payload}}: encode.flags(U32.is_eq((flags .&. U32.not(allowed(kind)) : U32), 0), kind, flags, stream, payload)def encode(max: U32, f: Frame) -> Result<&1, &1, Error, Bytes.Bytes>: Frame{+kind, +flags, +stream, payload} = f encode.checked(inspect(max, kind, flags, stream, payload))def parse.result(c: Checked, b: Bytes.Bytes, +len: U32) -> Decode: match c: case Invalid{e}: Bad{e} case Valid{f}: Bytes.Bytes{+n, buf} = b with_slice(Decode, Bytes.slice(Bytes.Bytes{n, buf}, (len + 9 : U32), (n - len - 9 : U32)), unused => rest => Got{f, rest})def parse.payload(max: U32, +len: U32, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Decode: with_slice(Decode, Bytes.slice(b, 9, len), b => payload => parse.result(inspect(max, kind, flags, stream, payload), b, len))def parse.full(enough: Bool, max: U32, +len: U32, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Decode: match enough: case True{}: parse.payload(max, len, kind, flags, stream, b) case False{}: Need{b}def parse.size(oversized: Bool, max: U32, +len: U32, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Decode: match oversized: case True{}: Bad{size.error(kind, stream)} case False{}: Bytes.Bytes{+n, buf} = b parse.full(U32.is_le(len, (n - 9 : U32)), max, len, kind, flags, stream, Bytes.Bytes{n, buf})def parse.header(+max: U32, b: Bytes.Bytes) -> Decode: with_number(Decode, Bytes.uint(b, 0, 3, True{}), b => +len => with_number(Decode, Bytes.get(b, 3), b => kind => with_number(Decode, Bytes.get(b, 4), b => flags => with_number(Decode, Bytes.get.u32be(b, 5), b => stream => parse.size(U32.is_gt(len, max), max, len, kind, flags, (stream .&. 2147483647 : U32), b)))))def parse.start(short: Bool, max: U32, b: Bytes.Bytes) -> Decode: match short: case True{}: Need{b} case False{}: parse.header(max, b)# A partial header or payload returns Need with the original input intact.def parse(max: U32, b: Bytes.Bytes) -> Decode: Bytes.Bytes{+n, buf} = b parse.start(U32.is_lt(n, 9), max, Bytes.Bytes{n, buf})# Send windows use U32 two's-complement; a SETTINGS change can make a stream window negative.type Stream is Type: Stream{id: U32, send_window: U32, recv_window: U32, local_end: Bool, remote_end: Bool, head: Bool, headers: List<&2, Hpack.Field>, partial: Bytes.Bytes, body: Bytes.Bytes, outgoing: Bytes.Bytes}type Control is Data: Control{next: U32, active: U32, frame_max: U32, initial: U32, max_streams: Maybe<&2, U32>, send_window: U32, recv_window: U32, first: Bool, ack: Bool, continuation: Maybe<&2, U32>, goaway: Maybe<&2, U32>}type Client is Type: Client{input: Bytes.Bytes, streams: List<&1, Stream>, encoder: Hpack.State, decoder: Hpack.State, control: Control}type ClientEvent is Type: Response{id: U32, headers: List<&2, Hpack.Field>, body: Bytes.Bytes} Reset{id: U32, code: U32} Shutdown{last: U32, code: U32} Pong{data: Bytes.Bytes}type Reply is Type: Advanced{client: Client, writes: List<&1, Bytes.Bytes>, events: List<&1, ClientEvent>} Failed{error: Error}def client.start() -> Client & Bytes.Bytes: (Client{Bytes.new(0), Nil{}, Hpack.new(4096), Hpack.new(4096), Control{1, 0, 16384, 65535, None{}, 65535, 65535, True{}, True{}, None{}, None{}}}, Bytes.append(Bytes.from_string("PRI * HTTP/2.0\u{d}\u{a}\u{d}\u{a}SM\u{d}\u{a}\u{d}\u{a}"), Bytes.set.u16be(Bytes.set(Bytes.set(Bytes.new(15), 2, 6), 3, 4), 9, 2)))def client.frame(r: Result<&1, &1, Error, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>: match r: case Fail{error}: None{} case Done{bytes}: Some{bytes}def client.headers.empty(first: Bool, end_stream: Bool, id: U32, max: U32, rev: List<&1, Bytes.Bytes>) -> Maybe<&1, List<&1, Bytes.Bytes>>: match first: case False{}: Some{List.reverse(&1, Bytes.Bytes, rev)} case True{}: Maybe.map(&1, Bytes.Bytes, List<&1, Bytes.Bytes>, b => List.reverse(&1, Bytes.Bytes, Con{b, rev}), client.frame(encode(max, Frame{1, (4 + Bool.pick(U32, end_stream, 1, 0) : U32), id, Bytes.new(0)})))def client.headers.go(n: Nat, +first: Bool, +end_stream: Bool, +id: U32, +max: U32, block: Bytes.Bytes, rev: List<&1, Bytes.Bytes>) -> Maybe<&1, List<&1, Bytes.Bytes>>: match n: case 0n: None{} case 1n+p: match block: case Bytes.Bytes{0, buf}: client.headers.empty(first, end_stream, id, max, rev) case Bytes.Bytes{+len, buf}: +take = Bool.pick(U32, U32.is_le(len, max), len, max) +last = U32.is_le(len, max) with_slice(Maybe<&1, List<&1, Bytes.Bytes>>, Bytes.slice(Bytes.Bytes{len, buf}, 0, take), whole => part => with_slice(Maybe<&1, List<&1, Bytes.Bytes>>, Bytes.slice(whole, take, (len - take : U32)), unused => rest => Maybe.bind(&1, Bytes.Bytes, List<&1, Bytes.Bytes>, client.frame(encode(max, Frame{Bool.pick(U32, first, 1, 9), (Bool.pick(U32, last, 4, 0) + Bool.pick(U32, Bool.and(first, end_stream), 1, 0) : U32), id, part})), packet => client.headers.go(p, False{}, end_stream, id, max, rest, Con{packet, rev}))))def client.headers(end_stream: Bool, +id: U32, +max: U32, block: Bytes.Bytes) -> Maybe<&1, List<&1, Bytes.Bytes>>: Bytes.Bytes{+len, buf} = block client.headers.go(1n+U32.to_nat(len), True{}, end_stream, id, max, Bytes.Bytes{len, buf}, Nil{})type BodySent is Type: BodySent{remaining: Bytes.Bytes, ended: Bool, stream_window: U32, connection_window: U32, writes: List<&1, Bytes.Bytes>}def client.min(+a: U32, +b: U32) -> U32: Bool.pick(U32, U32.is_le(a, b), a, b)def client.positive(+w: U32) -> U32: Bool.pick(U32, U32.is_lt(w, 2147483648), w, 0)def client.available(+len: U32, +max: U32, +connection: U32, +stream: U32) -> U32: client.min(client.min(len, max), client.min(client.positive(connection), client.positive(stream)))def client.data.go(n: Nat, body: Bytes.Bytes, take: U32, +id: U32, +max: U32, +connection: U32, +stream: U32, rev: List<&1, Bytes.Bytes>) -> Maybe<&1, BodySent>: match n: case 0n: None{} case 1n+p: match body: case Bytes.Bytes{0, buf}: Some{BodySent{Bytes.Bytes{0, buf}, True{}, stream, connection, List.reverse(&1, Bytes.Bytes, rev)}} case Bytes.Bytes{+len, buf}: match take: case 0: Some{BodySent{Bytes.Bytes{len, buf}, False{}, stream, connection, List.reverse(&1, Bytes.Bytes, rev)}} case +count: with_slice(Maybe<&1, BodySent>, Bytes.slice(Bytes.Bytes{len, buf}, 0, count), whole => part => with_slice(Maybe<&1, BodySent>, Bytes.slice(whole, count, (len - count : U32)), unused => rest => Maybe.bind(&1, Bytes.Bytes, BodySent, client.frame(encode(max, Frame{0, Bool.pick(U32, U32.is_eq(count, len), 1, 0), id, part})), packet => +new_connection = (connection - count : U32) +new_stream = (stream - count : U32) +remaining = (len - count : U32) client.data.go(p, rest, client.available(remaining, max, new_connection, new_stream), id, max, new_connection, new_stream, Con{packet, rev}))))def client.data(+id: U32, +max: U32, +connection: U32, +stream: U32, body: Bytes.Bytes) -> Maybe<&1, BodySent>: Bytes.Bytes{+len, buf} = body client.data.go(1n+U32.to_nat(len), Bytes.Bytes{len, buf}, client.available(len, max, connection, stream), id, max, connection, stream, Nil{})def client.limit(m: Maybe<&2, U32>, active: U32) -> Bool: match m: case None{}: True{} case Some{max}: U32.is_lt(active, max)def client.can(c: Control) -> Bool: Control{+next, active, frame_max, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway} = c Bool.and(U32.is_le(next, 2147483647), Bool.and(Maybe.is_none(&2, U32, goaway), client.limit(max_streams, active)))def client.id(c: Control) -> U32: Control{next, active, frame_max, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway} = c nextdef client.frame_max(c: Control) -> U32: Control{next, active, frame_max, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway} = c frame_maxdef client.request.done(sent: BodySent, headers: List<&1, Bytes.Bytes>, encoder: Hpack.State, c: Client) -> Reply: BodySent{remaining, ended, stream_window, connection_window, data} = sent Client{input, streams, old, decoder, Control{+next, +active, frame_max, initial, max_streams, previous, recv_window, first, ack, continuation, goaway}} = c Advanced{Client{input, Con{Stream{next, stream_window, 65535, ended, False{}, False{}, Nil{}, Bytes.new(0), Bytes.new(0), remaining}, streams}, encoder, decoder, Control{(next + 2 : U32), (active + 1 : U32), frame_max, initial, max_streams, connection_window, recv_window, first, ack, continuation, goaway}}, List.append(&1, Bytes.Bytes, headers, data), Nil{}}def client.request.data(m: Maybe<&1, BodySent>, headers: List<&1, Bytes.Bytes>, encoder: Hpack.State, c: Client) -> Reply: match m: case None{}: Failed{Error{1, True{}, 0}} case Some{sent}: client.request.done(sent, headers, encoder, c)def client.request.frames(m: Maybe<&1, List<&1, Bytes.Bytes>>, body: Bytes.Bytes, encoder: Hpack.State, c: Client) -> Reply: match m: case None{}: Failed{Error{6, True{}, 0}} case Some{headers}: Client{input, streams, old, decoder, +control} = c Control{+next, active, +frame_max, initial, max_streams, +connection, recv_window, first, ack, continuation, goaway} = control client.request.data(client.data(next, frame_max, connection, initial, body), headers, encoder, Client{input, streams, old, decoder, control})def client.request.body(r: Bytes.Bytes & U32, encoder: Hpack.State, block: Bytes.Bytes, c: Client) -> Reply: (body, +len) = r Client{input, streams, old, decoder, +control} = c client.request.frames(client.headers(U32.is_eq(len, 0), client.id(control), client.frame_max(control), block), body, encoder, Client{input, streams, old, decoder, control})def client.request.encoded(m: Maybe<&1, Hpack.State & Bytes.Bytes>, c: Client, body: Bytes.Bytes) -> Reply: match m: case None{}: Failed{Error{1, True{}, 0}} case Some{(encoder, block)}: client.request.body(Bytes.length(body), encoder, block, c)def client.request.ready(valid: Bool, c: Client, fields: List<&2, Hpack.Field>, body: Bytes.Bytes) -> Reply: match valid: case False{}: Failed{Error{7, True{}, 0}} case True{}: Client{input, streams, +encoder, decoder, control} = c client.request.encoded(Hpack.encode(fields, False{}, encoder), Client{input, streams, encoder, decoder, control}, body)def client.request(c: Client, fields: List<&2, Hpack.Field>, body: Bytes.Bytes) -> Reply: Client{input, streams, encoder, decoder, +control} = c client.request.ready(client.can(control), Client{input, streams, encoder, decoder, control}, fields, body)def client.fail(+code: U32, +connection: Bool, +stream: U32) -> Reply: Failed{Error{code, connection, Bool.pick(U32, connection, 0, stream)}}def client.ok(c: Client) -> Reply: Advanced{c, Nil{}, Nil{}}def client.after(r: Reply, k: Client -> List<&1, Bytes.Bytes> -> List<&1, ClientEvent> -> Reply) -> Reply: match r: case Failed{error}: Failed{error} case Advanced{client, writes, events}: k(client, writes, events)def client.write(m: Maybe<&1, Bytes.Bytes>, c: Client) -> Reply: match m: case None{}: client.fail(1, True{}, 0) case Some{packet}: Advanced{c, [packet], Nil{}}def client.ping(+flags: U32, payload: Bytes.Bytes, c: Client) -> Reply: match flags: case 0: client.write(client.frame(encode(16384, Frame{6, 1, 0, payload})), c) case 1: Advanced{c, Nil{}, [Pong{payload}]} case _: client.fail(1, True{}, 0)def client.ping.request(c: Client, payload: Bytes.Bytes) -> Reply: client.write(client.frame(encode(16384, Frame{6, 0, 0, payload})), c)def client.window.add(valid: Bool, +w: U32, +delta: U32) -> Maybe<&1, U32>: match valid: case False{}: None{} case True{}: Some{(w + delta : U32)}def client.window.adjust.sign(positive: Bool, +w: U32, +delta: U32) -> Maybe<&1, U32>: match positive: case True{}: client.window.add(Bool.or(U32.is_ge(w, 2147483648), U32.is_le(w, (2147483647 - delta : U32))), w, delta) case False{}: client.window.add(Bool.or(U32.is_lt(w, 2147483648), U32.is_ge(w, (2147483648 - delta : U32))), w, delta)def client.window.adjust(+w: U32, +delta: U32) -> Maybe<&1, U32>: client.window.adjust.sign(U32.is_lt(delta, 2147483648), w, delta)def client.window.plus.sign(positive: Bool, +w: U32, +value: U32) -> Maybe<&1, U32>: match positive: case True{}: client.window.add(U32.is_le(value, (2147483647 - w : U32)), w, value) case False{}: Some{(w + value : U32)}def client.window.plus(+w: U32, value: U32) -> Maybe<&1, U32>: client.window.plus.sign(U32.is_lt(w, 2147483648), w, value)def client.stream.adjust(s: Stream, delta: U32) -> Maybe<&1, Stream>: Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s Maybe.map(&1, U32, Stream, next => Stream{id, next, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, client.window.adjust(send_window, delta))def client.streams.adjust(xs: List<&1, Stream>, +delta: U32) -> Maybe<&1, List<&1, Stream>>: match xs: case Nil{}: Some{Nil{}} case Con{first, rest}: Maybe.bind(&1, Stream, List<&1, Stream>, client.stream.adjust(first, delta), updated => Maybe.map(&1, List<&1, Stream>, List<&1, Stream>, tail => Con{updated, tail}, client.streams.adjust(rest, delta)))def client.settings.initial.done(m: Maybe<&1, List<&1, Stream>>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match m: case None{}: client.fail(3, True{}, 0) case Some{streams}: client.ok(Client{input, streams, encoder, decoder, control})def client.settings.initial(+value: U32, c: Client) -> Reply: Client{input, streams, encoder, decoder, Control{next, active, frame_max, +initial, max_streams, send_window, recv_window, first, ack, continuation, goaway}} = c +delta = (value - initial : U32) client.settings.initial.done(client.streams.adjust(streams, delta), input, encoder, decoder, Control{next, active, frame_max, value, max_streams, send_window, recv_window, first, ack, continuation, goaway})def client.settings.item(id: U32, +value: U32, c: Client) -> Reply: match id: case 1: Client{input, streams, encoder, decoder, control} = c client.ok(Client{input, streams, Hpack.set_limit(value, encoder), decoder, control}) case 2: client.fail(1, True{}, 0) case 3: Client{input, streams, encoder, decoder, Control{next, active, frame_max, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway}} = c client.ok(Client{input, streams, encoder, decoder, Control{next, active, frame_max, initial, Some{value}, send_window, recv_window, first, ack, continuation, goaway}}) case 4: client.settings.initial(value, c) case 5: Client{input, streams, encoder, decoder, Control{next, active, frame_max, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway}} = c client.ok(Client{input, streams, encoder, decoder, Control{next, active, value, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway}}) case _: client.ok(c)def client.settings.go(n: Nat, b: Bytes.Bytes, +at: U32, c: Client) -> Reply: match n: case 0n: client.write(client.frame(encode(16384, Frame{4, 1, 0, Bytes.new(0)})), c) case 1n+p: with_number(Reply, Bytes.get.u16be(b, at), read_id => id => with_number(Reply, Bytes.get.u32be(read_id, (at + 2 : U32)), rest => value => client.after(client.settings.item(id, value, c), next => writes => events => client.settings.go(p, rest, (at + 6 : U32), next))))def client.settings.mark(c: Client) -> Client: Client{input, streams, encoder, decoder, Control{next, active, frame_max, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway}} = c Client{input, streams, encoder, decoder, Control{next, active, frame_max, initial, max_streams, send_window, recv_window, False{}, ack, continuation, goaway}}def client.settings.ack(c: Client) -> Reply: Client{input, streams, encoder, decoder, Control{next, active, frame_max, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway}} = c match ack: case False{}: client.fail(1, True{}, 0) case True{}: client.ok(Client{input, streams, encoder, decoder, Control{next, active, frame_max, initial, max_streams, send_window, recv_window, first, False{}, continuation, goaway}})def client.settings(flags: U32, payload: Bytes.Bytes, c: Client) -> Reply: match flags: case 1: client.settings.ack(c) case 0: Bytes.Bytes{+len, buf} = payload client.settings.go(U32.to_nat(U32.div(len, 6)), Bytes.Bytes{len, buf}, 0, client.settings.mark(c)) case _: client.fail(1, True{}, 0)def client.streams.prefix(previous: Maybe<&1, Stream>, r: Reply) -> Reply: match previous: case None{}: r case Some{s}: match r: case Failed{error}: Failed{error} case Advanced{Client{input, streams, encoder, decoder, control}, writes, events}: Advanced{Client{input, Con{s, streams}, encoder, decoder, control}, writes, events}def client.streams.go(xs: List<&1, Stream>, found: Bool, previous: Maybe<&1, Stream>, +target: U32, k: Stream -> List<&1, Stream> -> Reply) -> Reply: match xs: case Nil{}: match found: case False{}: client.fail(5, False{}, target) case True{}: match previous: case None{}: client.fail(1, True{}, 0) case Some{s}: k(s, Nil{}) case Con{s, rest}: Stream{+id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s match found: case True{}: match previous: case None{}: client.fail(1, True{}, 0) case Some{matched}: k(matched, Con{Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, rest}) case False{}: client.streams.prefix(previous, client.streams.go(rest, U32.is_eq(id, target), Some{Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}}, target, k))def client.streams.use(xs: List<&1, Stream>, target: U32, k: Stream -> List<&1, Stream> -> Reply) -> Reply: client.streams.go(xs, False{}, None{}, target, k)type Flushed is Type: Flushed{streams: List<&1, Stream>, connection: U32, writes: List<&1, Bytes.Bytes>}def client.flush.prepend(s: Stream, packets: List<&1, Bytes.Bytes>, tail: Flushed) -> Flushed: Flushed{more, window, writes} = tail Flushed{Con{s, more}, window, List.append(&1, Bytes.Bytes, packets, writes)}def client.with_sent(-R: Type, sent: BodySent, k: Bytes.Bytes -> Bool -> U32 -> U32 -> List<&1, Bytes.Bytes> -> R) -> R: BodySent{remaining, ended, stream, connection, packets} = sent k(remaining, ended, stream, connection, packets)def client.flush.go(xs: List<&1, Stream>, +connection: U32, +max: U32) -> Maybe<&1, Flushed>: match xs: case Nil{}: Some{Flushed{Nil{}, connection, Nil{}}} case Con{Stream{+id, +stream_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, rest}: match outgoing: case Bytes.Bytes{0, buf}: Maybe.map(&1, Flushed, Flushed, tail => client.flush.prepend(Stream{id, stream_window, recv_window, local_end, remote_end, head, headers, partial, body, Bytes.Bytes{0, buf}}, Nil{}, tail), client.flush.go(rest, connection, max)) case Bytes.Bytes{+len, buf}: Maybe.bind(&1, BodySent, Flushed, client.data(id, max, connection, stream_window, Bytes.Bytes{len, buf}), sent => client.with_sent(Maybe<&1, Flushed>, sent, remaining => ended => next_stream => next_connection => packets => Maybe.map(&1, Flushed, Flushed, tail => client.flush.prepend(Stream{id, next_stream, recv_window, ended, remote_end, head, headers, partial, body, remaining}, packets, tail), client.flush.go(rest, next_connection, max))))def client.flush.done(m: Maybe<&1, Flushed>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match m: case None{}: client.fail(1, True{}, 0) case Some{Flushed{streams, +connection, writes}}: Control{next, active, frame_max, initial, max_streams, previous, recv_window, first, ack, continuation, goaway} = control Advanced{Client{input, streams, encoder, decoder, Control{next, active, frame_max, initial, max_streams, connection, recv_window, first, ack, continuation, goaway}}, writes, Nil{}}def client.window.connection.valid(m: Maybe<&1, U32>, c: Client) -> Reply: match m: case None{}: client.fail(3, True{}, 0) case Some{w}: Client{input, streams, encoder, decoder, +control} = c Control{next, active, +frame_max, initial, max_streams, send_window, recv_window, first, ack, continuation, goaway} = control client.flush.done(client.flush.go(streams, w, frame_max), input, encoder, decoder, control)def client.window.connection(+value: U32, c: Client) -> Reply: Client{input, streams, encoder, decoder, +control} = c Control{next, active, frame_max, initial, max_streams, +send_window, recv_window, first, ack, continuation, goaway} = control client.window.connection.valid(client.window.plus(send_window, value), Client{input, streams, encoder, decoder, control})def client.window.stream.valid(m: Maybe<&1, U32>, +id: U32, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, +control: Control) -> Reply: match m: case None{}: client.fail(3, False{}, id) case Some{w}: Stream{id, previous, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s Control{next, active, +frame_max, initial, max_streams, +connection, recv, first, ack, continuation, goaway} = control client.flush.done(client.flush.go( Con{Stream{id, w, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, tail}, connection, frame_max), input, encoder, decoder, control)def client.window.stream.handle(+value: U32, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: Stream{+id, +send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s client.window.stream.valid(client.window.plus(send_window, value), id, Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, tail, input, encoder, decoder, control)def client.window.stream(id: U32, +value: U32, c: Client) -> Reply: Client{input, streams, encoder, decoder, control} = c client.streams.use(streams, id, s => tail => client.window.stream.handle(value, s, tail, input, encoder, decoder, control))def client.window.route(stream: U32, value: U32, c: Client) -> Reply: match stream: case 0: client.window.connection(value, c) case +id: client.window.stream(id, value, c)def client.window.update(stream: U32, payload: Bytes.Bytes, c: Client) -> Reply: with_number(Reply, Bytes.get.u32be(payload, 0), rest => raw => client.window.route(stream, (raw .&. 2147483647 : U32), c))def client.rst.stream(s: Stream, tail: List<&1, Stream>, +code: U32, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: Stream{+id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s Control{next, +active, frame_max, initial, max_streams, connection, recv, first, ack, continuation, goaway} = control Advanced{Client{input, tail, encoder, decoder, Control{next, (active - 1 : U32), frame_max, initial, max_streams, connection, recv, first, ack, continuation, goaway}}, Nil{}, [Reset{id, code}]}def client.rst.code(id: U32, +code: U32, c: Client) -> Reply: Client{input, streams, encoder, decoder, control} = c client.streams.use(streams, id, s => tail => client.rst.stream(s, tail, code, input, encoder, decoder, control))def client.rst(id: U32, payload: Bytes.Bytes, c: Client) -> Reply: with_number(Reply, Bytes.get.u32be(payload, 0), rest => code => client.rst.code(id, code, c))type Gone is Type: Gone{streams: List<&1, Stream>, active: U32, events: List<&1, ClientEvent>}def client.goaway.cons(keep: Bool, s: Stream, id: U32, tail: Gone) -> Gone: match keep: case True{}: Gone{streams, +active, events} = tail Gone{Con{s, streams}, (active + 1 : U32), events} case False{}: Gone{streams, active, events} = tail Gone{streams, active, Con{Reset{id, 7}, events}}def client.goaway.filter(xs: List<&1, Stream>, +last: U32) -> Gone: match xs: case Nil{}: Gone{Nil{}, 0, Nil{}} case Con{Stream{+id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, rest}: client.goaway.cons(U32.is_le(id, last), Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, id, client.goaway.filter(rest, last))def client.goaway.allowed(previous: Maybe<&2, U32>, last: U32) -> Bool: match previous: case None{}: True{} case Some{older}: U32.is_le(last, older)def client.goaway.finish(g: Gone, +last: U32, code: U32, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: Gone{remaining, count, events} = g Control{next, active, frame_max, initial, max_streams, connection, recv, first, ack, continuation, previous} = control Advanced{Client{input, remaining, encoder, decoder, Control{next, count, frame_max, initial, max_streams, connection, recv, first, ack, continuation, Some{last}}}, Nil{}, Con{Shutdown{last, code}, events}}def client.goaway.valid(valid: Bool, +last: U32, code: U32, c: Client) -> Reply: match valid: case False{}: client.fail(1, True{}, 0) case True{}: Client{input, streams, encoder, decoder, control} = c client.goaway.finish(client.goaway.filter(streams, last), last, code, input, encoder, decoder, control)def client.goaway.body(+last: U32, +code: U32, c: Client) -> Reply: Client{input, streams, encoder, decoder, +control} = c Control{next, active, frame_max, initial, max_streams, connection, recv, first, ack, continuation, +previous} = control client.goaway.valid(client.goaway.allowed(previous, last), last, code, Client{input, streams, encoder, decoder, control})def client.goaway(payload: Bytes.Bytes, c: Client) -> Reply: with_number(Reply, Bytes.get.u32be(payload, 0), b => raw => with_number(Reply, Bytes.get.u32be(b, 4), rest => code => client.goaway.body((raw .&. 2147483647 : U32), code, c)))def client.complete.ready(+id: U32, headers: List<&2, Hpack.Field>, body: Bytes.Bytes, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control, writes: List<&1, Bytes.Bytes>) -> Reply: Control{next, +active, frame_max, initial, max_streams, connection, recv, first, ack, continuation, goaway} = control Advanced{Client{input, tail, encoder, decoder, Control{next, (active - 1 : U32), frame_max, initial, max_streams, connection, recv, first, ack, continuation, goaway}}, writes, [Response{id, headers, body}]}def client.complete.packet(m: Maybe<&1, Bytes.Bytes>, id: U32, headers: List<&2, Hpack.Field>, body: Bytes.Bytes, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match m: case None{}: client.fail(1, True{}, 0) case Some{packet}: client.complete.ready(id, headers, body, tail, input, encoder, decoder, control, [packet])def client.complete(s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: Stream{+id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s match local_end: case True{}: client.complete.ready(id, headers, body, tail, input, encoder, decoder, control, Nil{}) case False{}: client.complete.packet(client.frame(encode(16384, Frame{3, 0, id, Bytes.set.u32be(Bytes.new(4), 0, 8)})), id, headers, body, tail, input, encoder, decoder, control)def client.fragment.slice(b: Bytes.Bytes, +offset: U32, +pad: U32) -> Bytes.Bytes: Bytes.Bytes{+len, buf} = b with_slice(Bytes.Bytes, Bytes.slice(Bytes.Bytes{len, buf}, offset, (len - offset - pad : U32)), whole => part => part)def client.fragment.padded(padded: Bool, +fixed: U32, b: Bytes.Bytes) -> Bytes.Bytes: match padded: case False{}: client.fragment.slice(b, fixed, 0) case True{}: with_number(Bytes.Bytes, Bytes.get(b, 0), rest => pad => client.fragment.slice(rest, (fixed + 1 : U32), pad))def client.fragment(+kind: U32, +flags: U32, b: Bytes.Bytes) -> Bytes.Bytes: client.fragment.padded(has(flags, 8), Bool.pick(U32, Bool.and(U32.is_eq(kind, 1), has(flags, 32)), 5, 0), b)def client.fragments.join(first: Bytes.Bytes, second: Bytes.Bytes) -> Bytes.Bytes: Bytes.Bytes{len, buf} = first match len: case 0: second case +count: Bytes.append(Bytes.Bytes{count, buf}, second)def client.headers.interim.status(s: String) -> Bool: match s: case SCon{Chr{49}, rest}: True{} case _: False{}def client.headers.interim(xs: List<&2, Hpack.Field>) -> Bool: match xs: case Nil{}: False{} case Con{Hpack.Field{name, value, mode}, rest}: Bool.and(String.eq(name, ":status"), client.headers.interim.status(value))def client.headers.interim.valid(valid: Bool, id: U32, fields: List<&2, Hpack.Field>, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match valid: case False{}: client.fail(1, False{}, id) case True{}: Advanced{Client{input, Con{s, tail}, encoder, decoder, control}, Nil{}, [Response{id, fields, Bytes.new(0)}]}def client.headers.fields.select(interim: Bool, fields: List<&2, Hpack.Field>, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match interim: case True{}: Stream{+id, send_window, recv_window, local_end, +remote_end, head, headers, partial, body, outgoing} = s client.headers.interim.valid(Bool.not(remote_end), id, fields, Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, tail, input, encoder, decoder, control) case False{}: Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s match remote_end: case True{}: client.complete(Stream{id, send_window, recv_window, local_end, True{}, True{}, List.append(&2, Hpack.Field, headers, fields), partial, body, outgoing}, tail, input, encoder, decoder, control) case False{}: client.ok(Client{input, Con{Stream{id, send_window, recv_window, local_end, False{}, True{}, List.append(&2, Hpack.Field, headers, fields), partial, body, outgoing}, tail}, encoder, decoder, control})def client.headers.fields(+fields: List<&2, Hpack.Field>, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: client.headers.fields.select(client.headers.interim(fields), fields, s, tail, input, encoder, decoder, control)def client.headers.decoded(m: Maybe<&1, Hpack.State & List<&2, Hpack.Field>>, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, control: Control) -> Reply: match m: case None{}: client.fail(9, True{}, 0) case Some{(decoder, fields)}: client.headers.fields(fields, s, tail, input, encoder, decoder, control)def client.headers.finish(end_headers: Bool, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match end_headers: case False{}: Stream{+id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s Control{next, active, frame_max, initial, max_streams, connection, recv, first, ack, continuation, goaway} = control client.ok(Client{input, Con{Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, tail}, encoder, decoder, Control{next, active, frame_max, initial, max_streams, connection, recv, first, ack, Some{id}, goaway}}) case True{}: Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s Control{next, active, frame_max, initial, max_streams, connection, recv, first, ack, continuation, goaway} = control client.headers.decoded(Hpack.decode(partial, decoder), Stream{id, send_window, recv_window, local_end, remote_end, head, headers, Bytes.new(0), body, outgoing}, tail, input, encoder, Control{next, active, frame_max, initial, max_streams, connection, recv, first, ack, None{}, goaway})def client.headers.accumulate(end_headers: Bool, fragment: Bytes.Bytes, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s client.headers.finish(end_headers, Stream{id, send_window, recv_window, local_end, remote_end, head, headers, client.fragments.join(partial, fragment), body, outgoing}, tail, input, encoder, decoder, control)def client.headers.open.valid(valid: Bool, +id: U32, end_headers: Bool, end_stream: Bool, fragment: Bytes.Bytes, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match valid: case False{}: client.fail(5, False{}, id) case True{}: Stream{stream, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s client.headers.accumulate(end_headers, fragment, Stream{stream, send_window, recv_window, local_end, end_stream, head, headers, partial, body, outgoing}, tail, input, encoder, decoder, control)def client.headers.open(end_headers: Bool, +end_stream: Bool, fragment: Bytes.Bytes, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: Stream{+id, send_window, recv_window, local_end, +remote_end, +head, headers, partial, body, outgoing} = s client.headers.open.valid(Bool.and(Bool.not(remote_end), Bool.or(Bool.not(head), end_stream)), id, end_headers, end_stream, fragment, Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, tail, input, encoder, decoder, control)def client.headers.receive(+id: U32, +flags: U32, payload: Bytes.Bytes, c: Client) -> Reply: Client{input, streams, encoder, decoder, control} = c +end_headers = has(flags, 4) +end_stream = has(flags, 1) fragment = client.fragment(1, flags, payload) client.streams.use(streams, id, s => tail => client.headers.open(end_headers, end_stream, fragment, s, tail, input, encoder, decoder, control))def client.continuation(+id: U32, +flags: U32, payload: Bytes.Bytes, c: Client) -> Reply: Client{input, streams, encoder, decoder, control} = c client.streams.use(streams, id, s => tail => client.headers.accumulate(has(flags, 4), payload, s, tail, input, encoder, decoder, control))def client.data.updates.end(end_stream: Bool, +count: U32, id: U32, connection: Bytes.Bytes) -> Maybe<&1, List<&1, Bytes.Bytes>>: match end_stream: case True{}: Some{[connection]} case False{}: Maybe.map(&1, Bytes.Bytes, List<&1, Bytes.Bytes>, stream => [connection, stream], client.frame(encode(16384, Frame{8, 0, id, Bytes.set.u32be(Bytes.new(4), 0, count)})))def client.data.updates(+len: U32, end_stream: Bool, +id: U32) -> Maybe<&1, List<&1, Bytes.Bytes>>: match len: case 0: Some{Nil{}} case +count: Maybe.bind(&1, Bytes.Bytes, List<&1, Bytes.Bytes>, client.frame(encode(16384, Frame{8, 0, 0, Bytes.set.u32be(Bytes.new(4), 0, count)})), connection => client.data.updates.end(end_stream, count, id, connection))def client.data.content(end_stream: Bool, content: Bytes.Bytes, writes: List<&1, Bytes.Bytes>, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match end_stream: case False{}: Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s Advanced{Client{input, Con{Stream{id, send_window, recv_window, local_end, False{}, head, headers, partial, Bytes.append(body, content), outgoing}, tail}, encoder, decoder, control}, writes, Nil{}} case True{}: Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing} = s client.after(client.complete(Stream{id, send_window, recv_window, local_end, True{}, head, headers, partial, Bytes.append(body, content), outgoing}, tail, input, encoder, decoder, control), next => extra => events => Advanced{next, List.append(&1, Bytes.Bytes, writes, extra), events})def client.data.content.updated(m: Maybe<&1, List<&1, Bytes.Bytes>>, end_stream: Bool, content: Bytes.Bytes, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match m: case None{}: client.fail(1, True{}, 0) case Some{writes}: client.data.content(end_stream, content, writes, s, tail, input, encoder, decoder, control)def client.data.stream.state(open: Bool, available: Bool, +id: U32, +len: U32, +end_stream: Bool, content: Bytes.Bytes, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: match open: case False{}: client.fail(1, False{}, id) case True{}: match available: case False{}: client.fail(3, False{}, id) case True{}: client.data.content.updated(client.data.updates(len, end_stream, id), end_stream, content, s, tail, input, encoder, decoder, control)def client.data.stream(+len: U32, end_stream: Bool, content: Bytes.Bytes, s: Stream, tail: List<&1, Stream>, input: Bytes.Bytes, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: Stream{+id, send_window, +recv_window, local_end, +remote_end, +head, headers, partial, body, outgoing} = s client.data.stream.state(Bool.and(head, Bool.not(remote_end)), U32.is_le(len, recv_window), id, len, end_stream, content, Stream{id, send_window, recv_window, local_end, remote_end, head, headers, partial, body, outgoing}, tail, input, encoder, decoder, control)def client.data.connection(valid: Bool, +id: U32, +flags: U32, +len: U32, payload: Bytes.Bytes, c: Client) -> Reply: match valid: case False{}: client.fail(3, True{}, 0) case True{}: Client{input, streams, encoder, decoder, control} = c content = client.fragment(0, flags, payload) client.streams.use(streams, id, s => tail => client.data.stream(len, has(flags, 1), content, s, tail, input, encoder, decoder, control))def client.data.receive(+id: U32, +flags: U32, payload: Bytes.Bytes, c: Client) -> Reply: Bytes.Bytes{+len, buf} = payload Client{input, streams, encoder, decoder, +control} = c Control{next, active, frame_max, initial, max_streams, connection, +recv_window, first, ack, continuation, goaway} = control client.data.connection(U32.is_le(len, recv_window), id, flags, len, Bytes.Bytes{len, buf}, Client{input, streams, encoder, decoder, control})def client.continuation.expected(m: Maybe<&2, U32>, +kind: U32, id: U32) -> Bool: match m: case None{}: U32.is_ne(kind, 9) case Some{expected}: Bool.and(U32.is_eq(kind, 9), U32.is_eq(expected, id))def client.apply.allowed(c: Control, +kind: U32, flags: U32, id: U32) -> Bool: Control{next, active, frame_max, initial, max_streams, connection, recv, first, ack, continuation, goaway} = c Bool.and(Bool.or(Bool.not(first), Bool.and(U32.is_eq(kind, 4), U32.is_eq(flags, 0))), client.continuation.expected(continuation, kind, id))def client.apply.frame(kind: U32, flags: U32, id: U32, payload: Bytes.Bytes, c: Client) -> Reply: match kind: case 0: client.data.receive(id, flags, payload, c) case 1: client.headers.receive(id, flags, payload, c) case 2: client.ok(c) case 3: client.rst(id, payload, c) case 4: client.settings(flags, payload, c) case 5: client.fail(1, True{}, 0) case 6: client.ping(flags, payload, c) case 7: client.goaway(payload, c) case 8: client.window.update(id, payload, c) case 9: client.continuation(id, flags, payload, c) case _: client.ok(c)def client.apply.checked(valid: Bool, kind: U32, flags: U32, id: U32, payload: Bytes.Bytes, c: Client) -> Reply: match valid: case False{}: client.fail(1, True{}, 0) case True{}: client.apply.frame(kind, flags, id, payload, c)def client.apply(f: Frame, c: Client) -> Reply: Frame{+kind, +flags, +id, payload} = f Client{input, streams, encoder, decoder, +control} = c client.apply.checked(client.apply.allowed(control, kind, flags, id), kind, flags, id, payload, Client{input, streams, encoder, decoder, control})def client.receive.advance(c: Client, k: Decode -> List<&1, Stream> -> Hpack.State -> Hpack.State -> Control -> Reply) -> Reply: Client{input, streams, encoder, decoder, control} = c k(parse(16384, input), streams, encoder, decoder, control)def client.receive.go(n: Nat, d: Decode, streams: List<&1, Stream>, encoder: Hpack.State, decoder: Hpack.State, control: Control, rev_writes: List<&1, Bytes.Bytes>, rev_events: List<&1, ClientEvent>) -> Reply: match n: case 0n: client.fail(1, True{}, 0) case 1n+p: match d: case Need{input}: Advanced{Client{input, streams, encoder, decoder, control}, List.reverse(&1, Bytes.Bytes, rev_writes), List.reverse(&1, ClientEvent, rev_events)} case Bad{error}: Failed{error} case Got{frame, rest}: client.after(client.apply(frame, Client{rest, streams, encoder, decoder, control}), next => writes => events => client.receive.advance(next, more => streams2 => enc => dec => ctl => client.receive.go(p, more, streams2, enc, dec, ctl, List.append(&1, Bytes.Bytes, List.reverse(&1, Bytes.Bytes, writes), rev_writes), List.append(&1, ClientEvent, List.reverse(&1, ClientEvent, events), rev_events))))def client.receive.buffer(b: Bytes.Bytes, streams: List<&1, Stream>, encoder: Hpack.State, decoder: Hpack.State, control: Control) -> Reply: Bytes.Bytes{+len, buf} = b client.receive.go(1n+U32.to_nat(len), parse(16384, Bytes.Bytes{len, buf}), streams, encoder, decoder, control, Nil{}, Nil{})def client.receive(c: Client, chunk: Bytes.Bytes) -> Reply: Client{input, streams, encoder, decoder, control} = c client.receive.buffer(Bytes.append(input, chunk), streams, encoder, decoder, control)