Events a driver gives a member, and effects the member asks for

A member never derives a BACAP index, encrypts, or touches the network itself.

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Missing : Type

• tombstone : Missing
• notFound : Missing

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqMissing : DecidableEq Missing

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqMissing x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedMissing : Inhabited Missing

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedMissing = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedMissing.default }

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadResult : Type

What reading a box found: a message, none for one that holds nothing a member can decode, or why there is none.

• data (message : Option Message) : ReadResult
• missing (why : Missing) : ReadResult

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqReadResult.decEq (x✝ x✝¹ : ReadResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqReadResult : DecidableEq ReadResult

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqReadResult = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqReadResult.decEq

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedReadResult : Inhabited ReadResult

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedReadResult = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedReadResult.default }

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.JoinReply : Type

What an introducer hands a new member. Members are named by their place in members, the introducer's roster; the new member takes place newcomer.

• members : List (Option (ByteArray × Index))

  Each member's read cap and start index, or none for a slot not filled.

• rosters : List (Option (List (Nat × Option Nat)))

  Each member's roster as (index, place), or none when unknown.

• introductions : List (Nat × Index × Nat)

  (introducer place, box, member place).

• introducer : Nat
• newcomer : Nat

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqJoinReply : DecidableEq JoinReply

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqJoinReply = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqJoinReply.decEq

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqJoinReply.decEq (x✝ x✝¹ : JoinReply) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedJoinReply : Inhabited JoinReply

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedJoinReply = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedJoinReply.default }

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Event : Type

• send (content : ByteArray) : Event
• read (stream : Key) : Event
• scan (stream : Key) : Event
• boxRead (stream : Key) (index : Index) (result : ReadResult) (next : Option Index) : Event

  The result of Effect.readBox, with the index after it.

• indexesDerived (stream : Key) (indexes : List Index) : Event
• walked (stream : Key) (target : Option Index) (skipped : List Index) (steps : Nat) : Event

  The result of Effect.walk: the box at the furthest target Idx64 within reach, the indexes before it (the last keep of them), and how many steps ahead it is.

• invite (name : String) (readCap : ByteArray) : Event
• introduce (name : String) (readCap : ByteArray) : Event
• remove (member : Key) : Event
• epochChanged (epoch : Nat) : Event

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEvent : DecidableEq Event

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEvent = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEvent.decEq

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEvent.decEq (x✝ x✝¹ : Event) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedEvent : Inhabited Event

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedEvent = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedEvent.default }

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Payload : Type

What a box of the member's own stream holds, as its Sent box keeps it: a message the member composed, which its client encodes, or the bytes a client that writes for itself handed over, which the member never looks into.

• message (message : Message) : Payload
• bytes (bytes : ByteArray) : Payload

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqPayload.decEq (x✝ x✝¹ : Payload) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqPayload : DecidableEq Payload

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqPayload = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqPayload.decEq

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedPayload : Inhabited Payload

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedPayload = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedPayload.default }

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Effect : Type

• writeBox (index : Index) (payload : Payload) : Effect
• writeTombstone (index : Index) : Effect
• readBox (stream : Key) (readCap : ByteArray) (index : Index) (recheck : Bool) : Effect
• deriveIndexes (stream : Key) (start : Index) (count : Nat) : Effect
• walk (stream : Key) (start : Index) (targets : List Nat) (keep : Nat) : Effect
• deliver (sender : Key) (index : Index) (content : ByteArray) : Effect
• expire (sender : Key) (index : Index) : Effect
• sendJoinReply (to : ByteArray) (reply : JoinReply) : Effect

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEffect.decEq (x✝ x✝¹ : Effect) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEffect : DecidableEq Effect

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEffect = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEffect.decEq

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedEffect : Inhabited Effect

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedEffect = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedEffect.default }