Rosters: following another member's numbering

Every roster index is announced in a message's Numbers, by key prefix or as the member its own Introduction introduces. A member's roster begins as its introducer's, which a watcher learns from IntroducedAt. If no two members share a prefix, a watcher that misses messages leaves indexes unresolved but never misplaced. See "Rosters" in the group chat spec.

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.Val (M P : Type) : Type

A roster entry as a watcher holds it.

• key {M P : Type} (m : M) : Val M P
• named {M P : Type} (p : P) : Val M P
• unknown {M P : Type} : Val M P

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.instDecidableEqVal {M✝ P✝ : Type} [DecidableEq M✝] [DecidableEq P✝] : DecidableEq (Val M✝ P✝)

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.instDecidableEqVal = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.instDecidableEqVal.decEq

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.instDecidableEqVal.decEq {M✝ P✝ : Type} [DecidableEq M✝] [DecidableEq P✝] (x✝ x✝¹ : Val M✝ P✝) : Decidable (x✝ = x✝¹)

Equations

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

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.Watcher (M B P : Type) : Type

• entries : M → ℕ → Option (Val M P)
• introductions : M → B → Option M
• started : M → Option (M × ℕ)
• known : P → Option M

  The member known by a prefix.

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.World (M B : Type) : Type

• roster : M → ℕ → Option M
• introduced : M → B → Option M

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.resolve {M B P : Type} (w : Watcher M B P) : ℕ → M → ℕ → Option M

Who x numbered k, if the watcher can tell: from its own entry, else from the roster it began as, through the index its introducer gave it. fuel bounds the chain of introducers.

Equations

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

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.Sound {M B P : Type} (pre : M → P) (w : Watcher M B P) (W : World M B) : Prop

Everything the watcher holds is true of the world, where pre gives a member's prefix.

• key (x : M) (k : ℕ) (m : M) : w.entries x k = some (Val.key m) → W.roster x k = some m
• named (x : M) (k : ℕ) (p : P) : w.entries x k = some (Val.named p) → ∃ (n : M), W.roster x k = some n ∧ pre n = p
• known (p : P) (n : M) : w.known p = some n → pre n = p
• introductions (i : M) (b : B) (n : M) : w.introductions i b = some n → W.introduced i b = some n
• started (x i : M) (top : ℕ) : w.started x = some (i, top) → ∀ (j : ℕ), j ≤ top → W.roster x j = W.roster i j

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.resolve_sound {M B P : Type} {pre : M → P} (hpre : Function.Injective pre) {w : Watcher M B P} {W : World M B} (h : Sound pre w W) (fuel : ℕ) (x : M) (k : ℕ) (n : M) : resolve w fuel x k = some n → W.roster x k = some n

Reading keeps a watcher sound

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.Msg (M B P : Type) : Type

A message of x's stream, as far as rosters are concerned: each number with the prefix of the member assigned it, or none for the member the message's own Introduction introduces.

• box : B
• numbers : List (ℕ × Option P)
• intro : Option M

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.Truthful {M B P : Type} (pre : M → P) (W : World M B) (x : M) (msg : Msg M B P) : Prop

What x says is true: each number names a member x put there, and the message introduces whom it says.

• own (k : ℕ) (n : M) : (k, none) ∈ msg.numbers → msg.intro = some n → W.roster x k = some n
• named (k : ℕ) (p : P) : (k, some p) ∈ msg.numbers → ∃ (n : M), W.roster x k = some n ∧ pre n = p
• introduced : W.introduced x msg.box = msg.intro

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.value {M B P : Type} (msg : Msg M B P) : Option P → Val M P

The entry a watcher keeps for one Numbers entry of x's message.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.value msg (some n) = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.Val.named n

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.ingestOne {M B P : Type} [DecidableEq M] (x : M) (msg : Msg M B P) (w : Watcher M B P) : ℕ × Option P → Watcher M B P

Take one Numbers entry of x's message, keeping any entry already held.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.ingest {M B P : Type} [DecidableEq M] (x : M) (msg : Msg M B P) (w : Watcher M B P) : Watcher M B P

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.ingest x msg w = List.foldl (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.ingestOne x msg) w msg.numbers

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.ingestOne_sound {M B P : Type} [DecidableEq M] {pre : M → P} {w : Watcher M B P} {W : World M B} {x : M} {msg : Msg M B P} (h : Sound pre w W) (ht : Truthful pre W x msg) {e : ℕ × Option P} (he : e ∈ msg.numbers) : Sound pre (ingestOne x msg w e) W

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.ingest_sound {M B P : Type} [DecidableEq M] {pre : M → P} {w : Watcher M B P} {W : World M B} {x : M} {msg : Msg M B P} (h : Sound pre w W) (ht : Truthful pre W x msg) : Sound pre (ingest x msg w) W

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.introduce {M B P : Type} [DecidableEq M] [DecidableEq B] [DecidableEq P] (pre : M → P) (x : M) (box : B) (n : M) (w : Watcher M B P) : Watcher M B P

Learn that the Introduction in x's box introduced n, and so learn n's key.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.introduce_sound {M B P : Type} [DecidableEq M] [DecidableEq B] [DecidableEq P] {pre : M → P} {w : Watcher M B P} {W : World M B} {x : M} {box : B} {n : M} (h : Sound pre w W) (hi : W.introduced x box = some n) : Sound pre (introduce pre x box n w) W

Following an IntroducedAt keeps a watcher sound

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.JoinedThrough {M B : Type} (W : World M B) (x i : M) : Prop

x's roster began as i's, through the index i gave it.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.begin {M B P : Type} [DecidableEq M] (x i : M) (top : ℕ) (w : Watcher M B P) : Watcher M B P

x says it joined through the Introduction in box b: its roster began as that introducer's, through the index the watcher finds x at in that introducer's roster.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.begin_sound {M B P : Type} [DecidableEq M] {pre : M → P} (hpre : Function.Injective pre) {w : Watcher M B P} {W : World M B} {fuel : ℕ} {x i : M} {b : B} {top : ℕ} (h : Sound pre w W) (hb : w.introductions i b = some x) (hat : ∀ (i' : M), W.introduced i' b = some x → JoinedThrough W x i') (htop : resolve w fuel i top = some x) : Sound pre (begin x i top w) W

Without IntroducedAt, a member introduced twice is misplaced

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.exWorld : World (Fin 4) (Fin 2)

Founders 0 and 1. 0 introduces 2, and 1 introduces 3, who joins through 1. 0 then introduces 3 again, in its box 1, and numbers it 3.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.exWatcher : Watcher (Fin 4) (Fin 2) (Fin 4)

A watcher that read 0's roster and its second Introduction of 3 first, and took that as where 3's roster began.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster.first_introduction_misplaces : resolve exWatcher 4 3 2 = some 2 ∧ exWorld.roster 3 2 = some 3