A member keeps every reader's invariant

ReadersOK: every reader of a member is filed under its own stream and satisfies Inv for some history. Every call on a member keeps it, given well-formed walk reports (Event.WF).

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Good (m : Key) (r : Reader) : Prop

A reader filed under m reads m's stream and keeps what is true of some history.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadersOK (d : Common.Dict Key Reader) : Prop

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps {α : Type} (p : GM α) : Prop

p keeps every reader OK.

Equations

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

Keeping is closed under the state monad

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps.pure {α : Type} (a : α) : Keeps (Pure.pure a)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps.bind {α β : Type} {p : GM α} {f : α → GM β} (hp : Keeps p) (hf : ∀ (a : α), Keeps (f a)) : Keeps (p >>= f)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps.get {β : Type} {k : Group → GM β} (hk : ∀ (g : Group), ReadersOK g.readers → Keeps (k g)) : Keeps (MonadState.get >>= k)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps.map {α β : Type} {p : GM α} (f : α → β) (hp : Keeps p) : Keeps (f <$> p)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps.set {g' : Group} (h' : ReadersOK g'.readers) : Keeps (MonadStateOf.set g')

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps.modify {f : Group → Group} (hf : ∀ (g : Group), ReadersOK g.readers → ReadersOK (f g).readers) : Keeps (_root_.modify f)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps.frame {f : Group → Group} (hf : ∀ (g : Group), (f g).readers = g.readers) : Keeps (_root_.modify f)

Readers

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadersOK.empty : ReadersOK ∅

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadersOK.set {d : Common.Dict Key Reader} (hd : ReadersOK d) {k : Key} {r : Reader} (hr : Good k r) : ReadersOK (d.set k r)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadersOK.erase {d : Common.Dict Key Reader} (hd : ReadersOK d) (k : Key) : ReadersOK (d.erase k)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadersOK.mapValues {d : Common.Dict Key Reader} (hd : ReadersOK d) {f : Reader → Reader} (hf : ∀ (m : Key) (r : Reader), Good m r → Good m (f r)) : ReadersOK (d.mapValues f)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadersOK.modify {d : Common.Dict Key Reader} (hd : ReadersOK d) (k : Key) {f : Reader → Reader} (hf : ∀ (m : Key) (r : Reader), Good m r → Good m (f r)) : ReadersOK (d.modify k f)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Good.congr {m : Key} {r r' : Reader} (h : Good m r) (hs : r'.stream = r.stream) (hp : r'.passed = r.passed) (hk : r'.kept = r.kept) (hl : r'.lost = r.lost) (hla : r'.last = r.last) : Good m r'

Inv depends only on what a reader keeps, so a reader that keeps the same is as good.

@[simp]

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.lose_stream (r : Reader) (a : ℕ) (b : Option Index) : (r.lose a b).stream = r.stream

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.loseAll_stream (dropped : List (Index × ℕ × Option Index)) (r : Reader) : (r.loseAll dropped).stream = r.stream

@[simp]

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.forget_stream (r : Reader) (w : ℕ) : (r.forget w).stream = r.stream

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.good_read {m : Key} {r : Reader} (h : Good m r) : Good m r.read.1

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.good_scan {m : Key} {r : Reader} (h : Good m r) (heard : List ℕ) (w : ℕ) : Good m (r.scan heard w).1

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.good_found {m : Key} {r : Reader} (h : Good m r) (index : Index) (result : ReadResult) (next : Option Index) (w : ℕ) : Good m (r.found index result next w).2.1

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.WalkWF (skipped : List Index) (steps : ℕ) : Prop

What a driver reports of a walk is possible: it kept no more boxes than it stepped past.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.WalkWF skipped steps = (skipped.length ≤ steps)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.good_walked {m : Key} {r : Reader} (h : Good m r) (target : Option Index) (skipped : List Index) (steps w : ℕ) (hwf : WalkWF skipped steps) : Good m (r.walked target skipped steps w).1

Each function of a member

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_follow (rc : ByteArray) (s : Index) : Keeps (Group.follow rc s)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_setReader {r : Reader} (hr : Good r.stream r) : Keeps (Group.setReader r)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_beginRoster (m i : Key) : Keeps (Group.beginRoster m i)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.foldl_frame {β : Type} (step : Group → β → Group) (hs : ∀ (g : Group) (x : β), (step g x).readers = g.readers) (l : List β) (g : Group) : (List.foldl step g l).readers = g.readers

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_started (m : Key) (i : Index) : Keeps (Group.started m i)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.tacticFrame : Lean.ParserDescr

modify of a function that leaves readers alone.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.takeAck_readers (s : Key) (g : Group) (a : ℕ × ℕ) : (Group.takeAck s g a).readers = g.readers

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_followIfNew (rc : ByteArray) : Keeps (Group.followIfNew rc)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_noteOwn (i : Key) (b : Index) (n : Key) : Keeps (Group.noteOwn i b n)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_noteAwaited (i : Key) (b : Index) (n : Key) : Keeps (Group.noteAwaited i b n)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_noteNew (i : Key) (b : Index) (intro : Introduction) : Keeps (Group.noteNew i b intro)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_introduced (i : Key) (b : Index) (intro : Introduction) : Keeps (Group.introduced i b intro)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_deliver (s : Key) (b : Index) (msg : Message) : Keeps (Group.deliver s b msg)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_ingest (s : Key) (b : Index) (msg : Message) : Keeps (Group.ingest s b msg)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Good.self {m : Key} {r : Reader} (h : Good m r) : Good r.stream r

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.good_get {d : Common.Dict Key Reader} (hd : ReadersOK d) {m : Key} {r : Reader} (h : d.get? m = some r) : Good r.stream r

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_scanStream (s : Key) : Keeps (Group.scanStream s)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_boxRead (s : Key) (b : Index) (res : ReadResult) (n : Option Index) : Keeps (Group.boxRead s b res n)

Writing

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_written (t : ℕ) (b : Index) (pt : Option Payload) : Keeps (Group.written t b pt)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_write (o : Outgoing) : Keeps (Group.write o)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_stage (m : Message) (p : Pending) : Keeps (Group.stage m p)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_withAcks (m : Message) (p : Pending) : Keeps (Group.withAcks m p)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_control : Keeps Group.control

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_next : Keeps Group.next

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_release : Keeps Group.release

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_hold : Keeps Group.hold

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_introduction (name : String) (rc : ByteArray) : Keeps (Group.introduction name rc)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_introduceNow (name : String) (rc : ByteArray) : Keeps (Group.introduceNow name rc)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_flushSome (n : ℕ) : Keeps (Group.flushSome n)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_flush : Keeps Group.flush

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_commitInduction : Keeps Group.commitInduction

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_progress : Keeps Group.progress

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_derived (l : List Index) : Keeps (Group.derived l)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_invite (name : String) (rc : ByteArray) (c : Bool) : Keeps (Group.invite name rc c)

Membership and time

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_remove (m : Key) : Keeps (Group.remove m)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_onEpoch (e : ℕ) : Keeps (Group.onEpoch e)

Every call on a member

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Event.WF : Event → Prop

What a driver reports is possible: a walk kept no more boxes than it stepped past.

Equations

• (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Event.walked stream target skipped steps).WF = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.WalkWF skipped steps
• x✝.WF = True

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.handle_keeps {e : Event} (hwf : e.WF) : Keeps (Group.handle e)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.observe_keeps (s : Key) (b : Index) (msg : Option Message) (n : Index) : Keeps (Group.observe s b msg n)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keeps_stageAll (l : List (Message × Pending)) : Keeps (Group.stageAll l)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.compose_keeps (c : Option ByteArray) : Keeps (Group.compose c)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.written_keeps (t : ℕ) (b : Index) (pt : Option Payload) : Keeps (Group.written t b pt)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.abandoned_keeps (t : ℕ) : Keeps (Group.abandoned t)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.beginInduction_keeps : Keeps Group.beginInduction

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.introduceNow_keeps (name : String) (rc : ByteArray) : Keeps (Group.introduceNow name rc)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.cancelInduction_keeps : Keeps Group.cancelInduction

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.remove_keeps (m : Key) : Keeps (Group.remove m)

Starting

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Keeps.foldlM {β : Type} {f : Unit → β → GM Unit} (hf : ∀ (x : β), Keeps (f () x)) (l : List β) : Keeps (List.foldlM f () l)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.found_ok (rc : ByteArray) (fs : List ByteArray) (policy : Retention) (w : ℕ) : ReadersOK (Group.found rc fs policy w).readers

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.joined_ok (rc : ByteArray) (reply : JoinReply) (policy : Retention) (w : ℕ) : ReadersOK (Group.joined rc reply policy w).readers

Acknowledgements sent

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reachable : Group → Prop

A member as calls on it can leave it, from its start.

• found (rc : ByteArray) (fs : List ByteArray) (policy : Retention) (w : ℕ) : Reachable (Group.found rc fs policy w)
• joined (rc : ByteArray) (reply : JoinReply) (policy : Retention) (w : ℕ) : Reachable (Group.joined rc reply policy w)
• handle {g : Group} (e : Event) : e.WF → Reachable g → Reachable (StateT.run (Group.handle e) g).2
• observe {g : Group} (s : Key) (b : Index) (msg : Option Message) (n : Index) : Reachable g → Reachable (StateT.run (Group.observe s b msg n) g).2
• compose {g : Group} (c : Option ByteArray) : Reachable g → Reachable (StateT.run (Group.compose c) g).2
• written {g : Group} (t : ℕ) (b : Index) (pt : Option Payload) : Reachable g → Reachable (StateT.run (Group.written t b pt) g).2
• abandoned {g : Group} (t : ℕ) : Reachable g → Reachable (StateT.run (Group.abandoned t) g).2
• beginInduction {g : Group} : Reachable g → Reachable (StateT.run Group.beginInduction g).2
• introduceNow {g : Group} (name : String) (rc : ByteArray) : Reachable g → Reachable (StateT.run (Group.introduceNow name rc) g).2
• cancelInduction {g : Group} : Reachable g → Reachable (StateT.run Group.cancelInduction g).2
• remove {g : Group} (m : Key) : Reachable g → Reachable (StateT.run (Group.remove m) g).2
• policy {g : Group} (p : Retention) : Reachable g → Reachable { readCap := g.readCap, policy := p, recheck := g.recheck, rosters := g.rosters, readers := g.readers, sent := g.sent, ledger := g.ledger, epoch := g.epoch, pool := g.pool, tip := g.tip, deriving_ := g.deriving_, outbox := g.outbox, pending := g.pending, tokens := g.tokens, unnumbered := g.unnumbered, introducedAt := g.introducedAt, joinedThrough := g.joinedThrough, awaitingStart := g.awaitingStart, received := g.received }

  The client changes its retention policy, as a user's disappearing messages setting does.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reachable.ok {g : Group} : Reachable g → ReadersOK g.readers

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.acks_sent_safe {g : Group} (hg : Reachable g) (p : Pending) (x : ℕ × ℕ) : x ∈ (g.acksOf p).1 → ∃ (m : Key) (r : Reader) (h : History) (b : Index), (x.1, some m) ∈ g.rosters.known g.me ∧ g.readers.get? m = some r ∧ r.stream = m ∧ Inv r h ∧ counter b = x.2 ∧ Safe h (some b)

Every acknowledgement a reachable member sends names a box its reader of that stream read, along with every box before it.