One member of one group chat

A state machine over Group, driven either by events (handle, returning effects) or by a client that reads and writes itself (observe, compose, written). A message changes rosters only once it has a box on the member's stream.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.poolSize : Nat

How many of its own indexes a member derives at a time.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.poolSize = 4

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.placeholder (place : Nat) : Key

What stands in a roster for a member known only by its place.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.placeholder place = "retired".toUTF8.push place.toUInt8

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

What a composed message does once it has a box.

• numbers : List (Nat × Option At)

  Roster indexes it assigns, and to whose Introduction; none for the one it carries.

• introduced : Option Key
• acks : Common.Dict Key (Option Index × Index)

  Each stream it acknowledges: what had been published before, and now.

• control : Bool

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqPending : DecidableEq Pending

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedPending : Inhabited Pending

Equations

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

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

• token : Nat
• message : Message

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqOutgoing : DecidableEq Outgoing

Equations

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

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedOutgoing : Inhabited Outgoing

Equations

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

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

• readCap : ByteArray

  Our own read cap: our key and our stream's first index.

• policy : Retention
• recheck : Nat

  How many boxes behind it a reader keeps one a scan stepped past.

• rosters : Rosters
• readers : Common.Dict Key Reader
• sent : SentBox
• ledger : Ledger
• epoch : Nat
• pool : List Index
• tip : Index

  The furthest of our own indexes derived so far.

• deriving_ : Bool
• outbox : List ByteArray

  Content waiting for an index.

• pending : Common.Dict Nat Pending

  Messages composed that have no box yet, by token.

• tokens : Nat
• unnumbered : List At

  Introductions read whose member we have not numbered yet.

• introducedAt : Option IntroRef

  Owed in our next message, once we have read our Introduction.

• joinedThrough : Option Key

  Our introducer, until we have read our Introduction.

• awaitingStart : Common.Dict Key Index

  IntroducedAt read before the Introduction it names.

• received : Common.Dict (Key × Index) Nat

  Content delivered, by sender and box, and the epoch it came.

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqGroup : DecidableEq Group

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedGroup : Inhabited Group

Equations

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

@[reducible, inline]

abbrev Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.GM (α : Type) : Type

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.GM = StateM Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.new (readCap : ByteArray) (policy : Retention := { }) (recheck : Nat := 256) : Group

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.me (g : Group) : Key

Equations

• g.me = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keyOf g.readCap

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.follow (readCap : ByteArray) (start : Index) : GM Unit

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.followIfNew (readCap : ByteArray) : GM Unit

Read the stream of readCap from its start, unless we read it already.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.found (readCap : ByteArray) (founders : List ByteArray) (policy : Retention := { }) (recheck : Nat := 256) : Group

Start a group with founders' read caps, ours among them.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.joined (readCap : ByteArray) (reply : JoinReply) (policy : Retention := { }) (recheck : Nat := 256) : Group

Join a group from what our introducer handed us.

Equations

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

Reading

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.heard (g : Group) (stream : Key) : List Nat

Equations

• g.heard stream = (g.ledger.heard.getD stream ∅).values

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.setReader (r : Reader) : GM Unit

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.scanStream (stream : Key) : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.numbered (g : Group) (member : Key) : Bool

Whether member is in our roster, or will be once what we have composed is written.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.beginRoster (member introducer : Key) : GM Unit

member's roster began as introducer's, through the index introducer gave it.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.started (member : Key) (index : Index) : GM Unit

member says it joined through the Introduction at index.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.noteOwn (introducer : Key) (index : Index) (new : Key) : GM Unit

Our own Introduction by the introducer we joined through: say where, in IntroducedAt.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.noteAwaited (introducer : Key) (index : Index) (new : Key) : GM Unit

An IntroducedAt read earlier named this Introduction.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.noteNew (introducer : Key) (index : Index) (intro : Introduction) : GM Unit

Read the new member's stream, and owe it a number.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.introduced (introducer : Key) (index : Index) (intro : Introduction) : GM Unit

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.takeAck (sender : Key) (g : Group) (a : Nat × Nat) : Group

Take one acknowledgement sender sent: of our own stream, it counts only for a box the Sent-box check finds; of another's, it is heard.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.deliver (sender : Key) (index : Index) (message : Message) : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.ingestIntroduction (sender : Key) (index : Index) (message : Message) : GM Unit

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.ingestIntroducedAt (sender : Key) (message : Message) : GM Unit

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.ingest (sender : Key) (index : Index) (message : Message) : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.boxRead (stream : Key) (index : Index) (result : ReadResult) (next : Option Index) : GM (List Effect)

Equations

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

Writing

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.size (g : Group) : Nat

The next index of our roster, counting what is composed.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.owesControl (g : Group) : Bool

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.controlStep (g : Group) (acc : Nat × Numbers × List (Nat × Option At) × List At) (a : At) : Nat × Numbers × List (Nat × Option At) × List At

Number every member whose Introduction we have read and whose introducer we have numbered, from the next index on: the message, what it does once written, and who is left unnumbered.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.controlOf (g : Group) : Message × Pending × List At

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.control : GM (Message × Pending)

Number every member whose Introduction we have read and whose introducer we have numbered, and say where we were introduced.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.release : GM Unit

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.hold : GM Unit

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.introductionOf (g : Group) (name : String) (readCap : ByteArray) : Message × Pending

The Introduction of the member read by readCap, numbering it next unless it is numbered already, and what it does once written.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.introduction (name : String) (readCap : ByteArray) : GM (Message × Pending)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.acksOf (g : Group) (pending : Pending) : List (Nat × Nat) × Pending × Ledger

Acknowledge every stream we read whose run has moved on since we last did: the acknowledgements, keyed by our roster index and naming each box by its Idx64, what the message does once written, and the ledger after.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.withAcks (message : Message) (pending : Pending) : GM (Message × Pending)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.stage (message : Message) (pending : Pending) : GM Outgoing

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.written (token : Nat) (index : Index) (plaintext : Option Payload) : GM Unit

The message token landed in the box index of our stream.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.write (o : Outgoing) : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.next : GM (Message × Pending)

The message to send next: control if owed, else the oldest content.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.flushSome : Nat → GM (List Effect)

Write what is owed, at most n messages.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.flushSome 0 = pure []

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.flush : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.settled (g : Group) : Bool

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.reply (g : Group) (ownStart : Index) : JoinReply

What to hand a new member, which will start our stream at ownStart.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.introduceNow (name : String) (readCap : ByteArray) : GM Outgoing

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.commitInduction : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.holdIfSettled : GM Unit

Do whatever has become possible: write what is owed, finish catching up, commit an induction.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.commitIfReady : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.progress : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.derived (indexes : List Index) : GM (List Effect)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.invite (name : String) (readCap : ByteArray) (commit : Bool) : GM (List Effect)

Equations

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

Membership and time

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.remove (member : Key) : GM Unit

Stop reading member and forget its key, keeping its places.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.everyoneAcked (g : Group) (idx64 : Nat) : Bool

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.onEpoch (epoch : Nat) : GM (List Effect)

Equations

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

Driven by events

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.handle (event : Event) : GM (List Effect)

Equations

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

Driven by a client that reads and writes for itself

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.observe (stream : Key) (index : Index) (message : Option Message) (next : Index) : GM (List Effect)

A box read on stream, in order: its message, or none for one that holds nothing we can use.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.stageAll : List (Message × Pending) → GM (List Outgoing)

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.stageAll [] = pure []

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.compose (content : Option ByteArray := none) : GM (List Outgoing)

The messages to send now, in order: a control message if one is owed, then content. Each takes effect when written.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.abandoned (token : Nat) : GM Unit

The message token will never be written: whatever it acknowledged is owed again, and whoever it numbered still needs numbering.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.beginInduction : GM (List Outgoing)

Begin inducting a member, starting each stream where we have read it now. Anything owed goes out first.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.cancelInduction : GM Unit

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.cancelInduction = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group.release