Acknowledgements

What this member has acknowledged, and what others have acknowledged of each stream. An induction holds publishing back. See "Joining" in the group chat spec.

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

• idle : Induction
• catchingUp : Induction
• inducting : Induction

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqInduction : DecidableEq Induction

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedInduction : Inhabited Induction

Equations

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

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

• published : Common.Dict Key Index

  The last index acknowledged of each stream.

• ackedBy : Common.Dict Key Nat

  The Idx64 of the last box of our stream each member has acknowledged, after the Sent-box check.

• heard : Common.Dict Key (Common.Dict Key Nat)

  For each stream, the Idx64 of the last box each other member acknowledged of it.

• induction : Induction
• invitee : Option (String × ByteArray)

  The name and read cap of the member being inducted.

• commit : Bool

  Commit the induction as soon as catching up is done.

• starts : Common.Dict Key Index

  Where each stream had been read when the invitation began.

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqLedger : DecidableEq Ledger

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedLedger : Inhabited Ledger

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Ledger.holding (l : Ledger) : Bool

Equations

• l.holding = decide (l.induction = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Induction.inducting)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Ledger.owed (l : Ledger) (stream : Key) (run : Option Index) : Option Index

The index to acknowledge of stream, the end of the unbroken run read, if anything new.

Equations

• l.owed stream none = none
• l.owed stream (some r) = if (l.holding || decide (l.published.get? stream = some r)) = true then none else some r

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Ledger.publish (l : Ledger) (stream : Key) (index : Index) : Ledger

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Ledger.hear (l : Ledger) (stream : Key) (idx64 : Nat) (by_ : Key) : Ledger

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Ledger.acked (l : Ledger) (member : Key) (idx64 : Nat) : Ledger

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Ledger.forget (l : Ledger) (member : Key) : Ledger

Equations

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