Rosters with explicit numbering

Every roster index is announced explicitly, so a missed message leaves an index unresolved and never shifts others. A roster that began as its introducer's reads its early entries from that roster. See "Rosters" in the group chat spec.

@[reducible, inline]

abbrev Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.At : Type

An Introduction: its introducer and its box.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.At = (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Key × Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Index)

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

• key : Option Key
• prefix_ : Option ByteArray

  The start of the member's key, as a Numbers field names it.

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqEntry : DecidableEq Entry

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedEntry : Inhabited Entry

Equations

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

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

• entries : Common.Dict Key (Common.Dict Nat Entry)
• started : Common.Dict Key (Key × Nat)

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

• introductions : Common.Dict At Key
• keys : List Key

  Every member whose key this member knows: whom a prefix can name.

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqRosters : DecidableEq Rosters

Equations

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

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedRosters : Inhabited Rosters

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.learn (r : Rosters) (key : Key) : Rosters

Equations

• r.learn key = if r.keys.contains key = true then r else { entries := r.entries, started := r.started, introductions := r.introductions, keys := r.keys ++ [key] }

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.startsWith (key p : ByteArray) : Bool

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.startsWith key p = p.data.toList.isPrefixOf key.data.toList

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.named (r : Rosters) (p : ByteArray) : Option Key

The one member known whose key starts with p.

Equations

• r.named p = match List.filter (fun (x : ByteArray) => Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.startsWith x p) r.keys with | [k] => some k | x => none

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.sortKeys (l : List Key) : List Key

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.sortNats (l : List Nat) : List Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.sortNats l = l.eraseDups.mergeSort fun (x1 x2 : Nat) => decide (x1 ≤ x2)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.found (r : Rosters) (founders : List Key) : Rosters

Start a group: every founder's roster is all founders in ascending order of key.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.resolveAux (r : Rosters) : Nat → List Key → Key → Nat → Option Key

Who owner numbered index, following where rosters began; seen stops a cycle.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.resolve (r : Rosters) (owner : Key) (index : Nat) : Option Key

Who owner numbered index, if this member can tell.

Equations

• r.resolve owner index = r.resolveAux (r.started.size + 1) [] owner index

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.indexesAux (r : Rosters) : Nat → List Key → Key → List Nat

Equations

• One or more equations did not get rendered due to their size.
• r.indexesAux fuel✝ x✝¹ x✝ = (r.entries.getD x✝ ∅).keys

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.known (r : Rosters) (owner : Key) : List (Nat × Option Key)

Every index owner is known to have assigned, in ascending order, and to whom.

Equations

• r.known owner = List.map (fun (i : Nat) => (i, r.resolve owner i)) (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.sortNats (r.indexesAux (r.started.size + 1) [] owner))

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.size (r : Rosters) (owner : Key) : Nat

Equations

• r.size owner = match (r.known owner).getLast? with | some (i, snd) => i + 1 | none => 0

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.indexOf (r : Rosters) (owner member : Key) : Option Nat

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.number (r : Rosters) (owner : Key) (index : Nat) (entry : Entry) : Rosters

owner numbered index as entry says; an entry already held is kept.

Equations

• r.number owner index entry = { entries := r.entries.set owner ((r.entries.getD owner ∅).setDefault index entry), started := r.started, introductions := r.introductions, keys := r.keys }

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.retire (r : Rosters) (member token : Key) : Rosters

Forget member's key, keeping every place it holds, under token. A place named by a prefix is member's only if the prefix names no other member known.

Equations

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