What a member guarantees

See "Opportunistic acknowledgements and backfill" in the group chat spec.

Rosters

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Entry.toVal (e : Entry) : Roster.Val Key ByteArray

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Rosters.toWatcher (r : Rosters) : Roster.Watcher Key Index ByteArray

A member's rosters as Roster.lean's watcher: a prefix names the one member known by it.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.entry_some (r : Rosters) (e : Entry) (n : Key) (h : (match e.key, e.prefix_ with | some k, x => some k | none, some p => if p.size = 0 then none else r.named p | none, none => none) = some n) : (match e.toVal with | Roster.Val.key m => some m | Roster.Val.named p => r.toWatcher.known p | Roster.Val.unknown => none) = some n

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.resolveAux_some (r : Rosters) (fuel : ℕ) (seen : List Key) (x : Key) (k : ℕ) (n : Key) : r.resolveAux fuel seen x k = some n → ∃ (f : ℕ), Roster.resolve r.toWatcher f x k = some n

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.resolve_sound {pre : Key → ByteArray} (hpre : Function.Injective pre) {r : Rosters} {W : Roster.World Key Index} (h : Roster.Sound pre r.toWatcher W) {x : Key} {k : ℕ} {n : Key} (hr : r.resolve x k = some n) : W.roster x k = some n

Whoever a member names at a roster index is correct, if what it holds is true of the world and no two members share a key prefix.

Acknowledgements sent

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AcksTrue (g : Group) (acks : List (ℕ × ℕ)) : Prop

What acksOf keeps true as it goes.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.acksOf_fold (g : Group) (es : List (ℕ × Option Key)) (acc : List (ℕ × ℕ) × Pending × Ledger) : (∀ e ∈ es, e ∈ g.rosters.known g.me) → AcksTrue g acc.1 → AcksTrue g (List.foldl (fun (acc : List (ℕ × ℕ) × Pending × Ledger) (e : ℕ × Option Key) => match e.2.bind g.readers.get? with | none => acc | some r => match acc.2.2.owed r.stream r.run with | none => acc | some owed => (acc.1 ++ [(e.1, counter owed)], have __src := acc.2.1; { numbers := __src.numbers, introduced := __src.introduced, acks := acc.2.1.acks.set r.stream (acc.2.2.published.get? r.stream, owed), control := __src.control }, acc.2.2.publish r.stream owed)) acc es).1

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.acksOf_runs (g : Group) (p : Pending) : AcksTrue g (g.acksOf p).1

Every acknowledgement a member sends is the run of its reader of that stream.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.acksOf_safe (g : Group) (p : Pending) (hist : Key → History) (inv : ∀ (m : Key) (r : Reader), g.readers.get? m = some r → Inv r (hist m)) (x : ℕ × ℕ) : x ∈ (g.acksOf p).1 → ∃ (m : Key) (b : Index), (x.1, some m) ∈ g.rosters.known g.me ∧ counter b = x.2 ∧ Safe (hist m) (some b)

What a member acknowledges it has read, with every box before it.

Acknowledgements taken

@[simp]

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.takeAck_sent (sender : Key) (g : Group) (a : ℕ × ℕ) : (Group.takeAck sender g a).sent = g.sent

@[simp]

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.takeAck_rosters (sender : Key) (g : Group) (a : ℕ × ℕ) : (Group.takeAck sender g a).rosters = g.rosters

@[simp]

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.takeAck_readCap (sender : Key) (g : Group) (a : ℕ × ℕ) : (Group.takeAck sender g a).readCap = g.readCap

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.takeAck_credit (sender : Key) (g : Group) (a : ℕ × ℕ) (m : Key) : (Group.takeAck sender g a).ledger.ackedBy.get? m = g.ledger.ackedBy.get? m ∨ m = sender ∧ g.rosters.resolve sender a.1 = some g.me ∧ g.sent.checkAt a.2 = true

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.takeAcks_credit (sender : Key) (acks : List (ℕ × ℕ)) (g : Group) (m : Key) : (List.foldl (Group.takeAck sender) g acks).ledger.ackedBy.get? m = g.ledger.ackedBy.get? m ∨ m = sender ∧ ∃ a ∈ acks, g.rosters.resolve sender a.1 = some g.me ∧ g.sent.checkAt a.2 = true

Acknowledgements change only the sender's count, and only for boxes the Sent-box check finds.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.SentBox.Keyed (s : SentBox) : Prop

Every record is kept under the Idx64 of its own box.

Equations

• s.Keyed = ∀ (k : ℕ) (r : Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Record), (k, r) ∈ s.records.pairs → Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.counter r.index = k

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keyed_record {s : SentBox} (hs : s.Keyed) (index : Index) (plaintext : Option Payload) (control : Bool) (epoch : ℕ) : (s.record index plaintext control epoch).Keyed

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keyed_retain {s : SentBox} (hs : s.Keyed) (epoch : ℕ) (policy : Retention) (acked : ℕ → Bool) : (s.retain epoch policy acked).Keyed

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keyed_backfill {s : SentBox} (hs : s.Keyed) (epoch : ℕ) (acked : ℕ → Bool) : (s.backfill epoch acked).1.Keyed

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.check_some {s : SentBox} {i : Index} {x : ℕ} (h : s.check i = some x) : ∃ (r : Record), (counter i, r) ∈ s.records.pairs ∧ r.index = i ∧ x = counter i

The Sent-box check finds only boxes the member wrote, returning their Idx64.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.checkAt_some {s : SentBox} (hs : s.Keyed) {idx64 : ℕ} (h : s.checkAt idx64 = true) : ∃ (r : Record), (idx64, r) ∈ s.records.pairs ∧ counter r.index = idx64

The Sent-box check by Idx64 finds a box the member wrote, at that Idx64.

Numbering

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.controlOf_fold (g : Group) (as : List At) (acc : ℕ × Numbers × List (ℕ × Option At) × List At) : List.map (fun (x : ℕ × Option ByteArray) => x.1) acc.2.1 = List.range' g.size (acc.1 - g.size) → g.size ≤ acc.1 → List.map (fun (x : ℕ × Option At) => x.1) acc.2.2.1 = List.map (fun (x : ℕ × Option ByteArray) => x.1) acc.2.1 → List.map (fun (x : ℕ × Option ByteArray) => x.1) (List.foldl g.controlStep acc as).2.1 = List.range' g.size ((List.foldl g.controlStep acc as).1 - g.size) ∧ List.map (fun (x : ℕ × Option At) => x.1) (List.foldl g.controlStep acc as).2.2.1 = List.map (fun (x : ℕ × Option ByteArray) => x.1) (List.foldl g.controlStep acc as).2.1

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.controlOf_consecutive (g : Group) : List.map (fun (x : ℕ × Option ByteArray) => x.1) g.controlOf.1.numbers = List.range' g.size (List.length g.controlOf.1.numbers) ∧ List.map (fun (x : ℕ × Option At) => x.1) g.controlOf.2.1.numbers = List.map (fun (x : ℕ × Option ByteArray) => x.1) g.controlOf.1.numbers

A control message numbers members at consecutive indexes from the next free one, counting composed messages, and its pending numbering assigns the same ones.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.size_eq (g : Group) (hp : ∀ p ∈ g.pending.values, p.numbers = []) : g.size = g.rosters.size g.me

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.reply_newcomer (g : Group) (s : Index) : (g.reply s).newcomer = g.rosters.size g.me

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.introduction_index (g : Group) (name : String) (readCap : ByteArray) (s : Index) (hp : ∀ p ∈ g.pending.values, p.numbers = []) (hn : g.numbered (keyOf readCap) = false) : (g.introductionOf name readCap).1.numbers = [((g.reply s).newcomer, none)]

An Introduction gives the new member the index the reply promised, when everything composed before it has been written.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.size_ge (g : Group) {p : Pending} (hp : p ∈ g.pending.values) {n : ℕ} {a : Option At} (hn : (n, a) ∈ p.numbers) : n + 1 ≤ g.size

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.introduction_index_pending (g : Group) (name : String) (readCap : ByteArray) (s : Index) {p : Pending} (hp : p ∈ g.pending.values) {a : Option At} (hn : ((g.reply s).newcomer, a) ∈ p.numbers) (hnew : g.numbered (keyOf readCap) = false) : ∃ (k : ℕ), (g.introductionOf name readCap).1.numbers = [(k, none)] ∧ (g.reply s).newcomer < k

If a composed message still holds the promised index, the Introduction gives a later one.

Retention and backfill

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.retain_spec (s : SentBox) (epoch : ℕ) (policy : Retention) (acked : ℕ → Bool) (e : ℕ × Record) : e ∈ (s.retain epoch policy acked).records.pairs → ∃ (r0 : Record), (e.1, r0) ∈ s.records.pairs ∧ (∀ (window : ℕ), policy.window = some window → epoch ≤ r0.written + window) ∧ e.2.index = r0.index ∧ e.2.control = r0.control ∧ e.2.written = r0.written ∧ (e.2.plaintext = r0.plaintext ∨ e.2.plaintext = none ∧ ((∃ (keep : ℕ), policy.keepSent = some keep ∧ r0.control = false ∧ r0.written + keep ≤ epoch) ∨ policy.discardAcked = true ∧ acked e.1 = true))

Retention keeps each record's box and kind, and drops plaintext only once every member has acknowledged it or the policy expired it. Records older than the window are gone.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.backfill_of {s : SentBox} {epoch : ℕ} (acked : ℕ → Bool) (h : s.backfilled = some epoch) : (s.backfill epoch acked).2 = []

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.backfill_once (s : SentBox) (epoch : ℕ) (acked : ℕ → Bool) : ((s.backfill epoch acked).1.backfill epoch acked).2 = []

A box is rewritten at most once an epoch.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.backfill_behind (s : SentBox) (epoch : ℕ) (acked : ℕ → Bool) {i : Index} {p : Payload} (h : Effect.writeBox i p ∈ (s.backfill epoch acked).2) : ∃ (k : ℕ) (r : Record), (k, r) ∈ s.records.pairs ∧ r.index = i ∧ r.plaintext = some p ∧ acked k = false

Backfill writes content only to boxes not yet acknowledged by every member.