inductive Network.HTTP2.StreamState : Type

• idle : StreamState
• open : StreamState
• halfClosedLocal : StreamState
• halfClosedRemote : StreamState
• resetLocal : StreamState
• resetRemote : StreamState
• closed : StreamState
• reservedLocal : StreamState
• reservedRemote : StreamState

def Network.HTTP2.instReprStreamState.repr : StreamState → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Network.HTTP2.instReprStreamState : Repr StreamState

Equations

• Network.HTTP2.instReprStreamState = { reprPrec := Network.HTTP2.instReprStreamState.repr }

@[implicit_reducible]

instance Network.HTTP2.instInhabitedStreamState : Inhabited StreamState

Equations

• Network.HTTP2.instInhabitedStreamState = { default := Network.HTTP2.instInhabitedStreamState.default }

def Network.HTTP2.instInhabitedStreamState.default : StreamState

Equations

• Network.HTTP2.instInhabitedStreamState.default = Network.HTTP2.StreamState.idle

@[implicit_reducible]

instance Network.HTTP2.instBEqStreamState : BEq StreamState

Equations

• Network.HTTP2.instBEqStreamState = { beq := Network.HTTP2.instBEqStreamState.beq }

def Network.HTTP2.instBEqStreamState.beq : StreamState → StreamState → Bool

Equations

• Network.HTTP2.instBEqStreamState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Network.HTTP2.instToStringStreamState : ToString StreamState

Equations

• One or more equations did not get rendered due to their size.

structure Network.HTTP2.StreamInfo : Type

• streamId : StreamId
• state : StreamState
• sendWindow : Int
• recvWindow : Int
• priorityExclusive : Bool
• priorityDependency : StreamId
• priorityWeight : UInt8

def Network.HTTP2.instReprStreamInfo.repr : StreamInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Network.HTTP2.instReprStreamInfo : Repr StreamInfo

Equations

• Network.HTTP2.instReprStreamInfo = { reprPrec := Network.HTTP2.instReprStreamInfo.repr }

def Network.HTTP2.instInhabitedStreamInfo.default : StreamInfo

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Network.HTTP2.instInhabitedStreamInfo : Inhabited StreamInfo

Equations

• Network.HTTP2.instInhabitedStreamInfo = { default := Network.HTTP2.instInhabitedStreamInfo.default }

@[inline]

def Network.HTTP2.isClientStream (streamId : StreamId) : Bool

Equations

• Network.HTTP2.isClientStream streamId = streamId.isClientInitiated

@[inline]

def Network.HTTP2.isServerStream (streamId : StreamId) : Bool

Equations

• Network.HTTP2.isServerStream streamId = streamId.isServerInitiated

@[inline]

def Network.HTTP2.isConnectionStream (streamId : StreamId) : Bool

Equations

• Network.HTTP2.isConnectionStream streamId = (streamId.val == 0)

@[inline]

def Network.HTTP2.validateStreamId (newId lastId : StreamId) : Bool

Equations

• Network.HTTP2.validateStreamId newId lastId = decide (newId.val > lastId.val)

def Network.HTTP2.client_server_complementary_check (id : StreamId) (_h : id.val ≠ 0) : Bool

Equations

• Network.HTTP2.client_server_complementary_check id _h = (Network.HTTP2.isClientStream id || Network.HTTP2.isServerStream id)

structure Network.HTTP2.StreamTable : Type

• streams : Std.HashMap StreamId StreamInfo
• lastClientStreamId : StreamId
• lastServerStreamId : StreamId
• nextServerStreamId : StreamId

@[implicit_reducible]

instance Network.HTTP2.instInhabitedStreamTable : Inhabited StreamTable

Equations

• Network.HTTP2.instInhabitedStreamTable = { default := Network.HTTP2.instInhabitedStreamTable.default }

def Network.HTTP2.instInhabitedStreamTable.default : StreamTable

Equations

• Network.HTTP2.instInhabitedStreamTable.default = { streams := default, lastClientStreamId := default, lastServerStreamId := default, nextServerStreamId := default }

@[implicit_reducible]

instance Network.HTTP2.instReprStreamTable : Repr StreamTable

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.StreamTable.empty : StreamTable

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.StreamTable.lookup (table : StreamTable) (streamId : StreamId) : Option StreamInfo

Equations

• table.lookup streamId = table.streams[streamId]?

def Network.HTTP2.StreamTable.upsert (table : StreamTable) (info : StreamInfo) : StreamTable

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.StreamTable.openClientStream (table : StreamTable) (streamId : StreamId) (initialWindow : Int) : Option StreamTable

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.StreamTable.updateState (table : StreamTable) (streamId : StreamId) (state : StreamState) : StreamTable

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.StreamTable.updatePriority (table : StreamTable) (streamId : StreamId) (exclusive : Bool) (dependency : StreamId) (weight : UInt8) : StreamTable

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.StreamTable.activeStreamCount (table : StreamTable) : Nat

Equations

• One or more equations did not get rendered due to their size.