A reader acknowledges only what it has read

A History is a ghost record of every box a reader passed, read or not. Inv ties the reader's state to it; every operation keeps Inv, and under it run names a box read along with every box before it (run_safe). See "Opportunistic acknowledgements and backfill" in the group chat spec.

@[reducible, inline]

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

Every box a reader has passed, in order, and whether it has read it.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.History = List (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Index × Bool)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Names (h : History) (b : Index) (p : ℕ) : Prop

Box p of the history is b.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Names h b p = ∃ (x : Bool), h[p]? = some (b, x)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Safe (h : History) : Option Index → Prop

Every box up to and including the one named has been read.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Safe h none = True

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Inv (r : Reader) (h : History) : Prop

What the reader keeps is true of its history.

• len : List.length h = r.passed
• kept (e : Index × ℕ × Option Index) : e ∈ r.kept → h[e.2.1]? = some (e.1, false)
• nodup : (List.map (fun (x : Index × ℕ × Option Index) => x.2.1) r.kept).Nodup
• keptBefore (e : Index × ℕ × Option Index) : e ∈ r.kept → ∀ (b : Index), e.2.2 = some b → ∃ p < e.2.1, Names h b p
• lost (l : ℕ) (b : Option Index) : r.lost = some (l, b) → l ≤ List.length h ∧ ∀ (c : Index), b = some c → ∃ p < l, Names h c p
• covered (p : ℕ) (c : Index) : h[p]? = some (c, false) → (∃ e ∈ r.kept, e.2.1 = p) ∨ ∃ (l : ℕ) (b : Option Index), r.lost = some (l, b) ∧ l ≤ p

  Every box passed unread is kept, or at or after the first one given up on.

• last (b : Index) : r.last = some b → ∃ (p : ℕ), Names h b p

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Inv.start (stream : Key) (readCap : ByteArray) (next : Index) : Inv { stream := stream, readCap := readCap, next := next } []

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Inv.congr {r r' : Reader} {h : History} (inv : Inv r h) (hp : r'.passed = r.passed) (hk : r'.kept = r.kept) (hl : r'.lost = r.lost) (hla : r'.last = r.last) : Inv r' h

Inv depends only on what the reader keeps.

Histories only grow and only gain reads

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Grows (h h' : History) : Prop

h' extends h, with boxes possibly turned from unread to read.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Names.grow {h h' : History} (g : Grows h h') {b : Index} {p : ℕ} (n : Names h b p) : Names h' b p

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Safe.mono {h h' : History} (g : Grows h h') {b : Option Index} : Safe h b → Safe h' b

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Grows.refl (h : History) : Grows h h

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Grows.append (h t : History) : Grows h (h ++ t)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Grows.set (h : History) (p : ℕ) (c : Index) (hp : h[p]? = some (c, false)) : Grows h (List.set h p (c, true))

The acknowledgement is safe

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.foldl_min (gs : List (ℕ × Option Index)) (g : ℕ × Option Index) : have m := List.foldl (fun (m x : ℕ × Option Index) => if x.1 < m.1 then x else m) g gs; (m = g ∨ m ∈ gs) ∧ m.1 ≤ g.1 ∧ ∀ x ∈ gs, m.1 ≤ x.1

The gap with the earliest position, as run picks it.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.read_before {r : Reader} {h : History} (inv : Inv r h) {m : ℕ} (hk : ∀ e ∈ r.kept, m ≤ e.2.1) (hl : ∀ (l : ℕ) (b : Option Index), r.lost = some (l, b) → m ≤ l) (q : ℕ) : q < m → ∀ (c : Index) (x : Bool), h[q]? = some (c, x) → x = true

Every box before the earliest gap has been read.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.safe_upto {h : History} {m : ℕ} (hread : ∀ q < m, ∀ (c : Index) (x : Bool), h[q]? = some (c, x) → x = true) {b : Index} {p : ℕ} (hp : p < m) (n : Names h b p) : Safe h (some b)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.run_safe {r : Reader} {h : History} (inv : Inv r h) : Safe h r.run

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

Every operation keeps Inv

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.BeforeOK (h : History) (at_ : ℕ) (b : Option Index) : Prop

A gap's before names an earlier box.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.LostOK (h : History) (lost : Option (ℕ × Option Index)) : Prop

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.BeforeOK.grow {h h' : History} (g : Grows h h') {a : ℕ} {b : Option Index} (hb : BeforeOK h a b) : BeforeOK h' a b

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.lose_lost (r : Reader) (a : ℕ) (b : Option Index) : ∃ (l : ℕ) (c : Option Index), (r.lose a b).lost = some (l, c) ∧ l ≤ a ∧ ((l, c) = (a, b) ∨ r.lost = some (l, c)) ∧ ∀ (l0 : ℕ) (c0 : Option Index), r.lost = some (l0, c0) → l ≤ l0

@[simp]

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

@[simp]

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

@[simp]

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.lose_ok {h : History} {r : Reader} (hr : LostOK h r.lost) {a : ℕ} {b : Option Index} (ha : a ≤ List.length h) (hb : BeforeOK h a b) : LostOK h (r.lose a b).lost

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.loseAll_spec (h : History) (dropped : List (Index × ℕ × Option Index)) (r : Reader) : LostOK h r.lost → (∀ e ∈ dropped, e.2.1 ≤ List.length h ∧ BeforeOK h e.2.1 e.2.2) → (r.loseAll dropped).kept = r.kept ∧ (r.loseAll dropped).last = r.last ∧ (r.loseAll dropped).passed = r.passed ∧ LostOK h (r.loseAll dropped).lost ∧ (∀ e ∈ dropped, ∃ (l : ℕ) (b : Option Index), (r.loseAll dropped).lost = some (l, b) ∧ l ≤ e.2.1) ∧ ∀ (l0 : ℕ) (b0 : Option Index), r.lost = some (l0, b0) → ∃ (l : ℕ) (b : Option Index), (r.loseAll dropped).lost = some (l, b) ∧ l ≤ l0

Giving up on boxes dropped: each is then at or after the first one given up on.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.forget_inv {r : Reader} {h : History} (inv : Inv r h) (window : ℕ) : Inv (r.forget window) h

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.read_inv {r : Reader} {h : History} (inv : Inv r h) : Inv r.read.1 h

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.scan_inv {r : Reader} {h : History} (inv : Inv r h) (heard : List ℕ) (window : ℕ) : Inv (r.scan heard window).1 h

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.foundHistory (r : Reader) (h : History) (index : Index) (result : ReadResult) (next : Option Index) : History

What reading a box adds to the history.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.found_grows {r : Reader} {h : History} (inv : Inv r h) (index : Index) (result : ReadResult) (next : Option Index) : Grows h (foundHistory r h index result next)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.advance_inv {r : Reader} {h : History} (inv : Inv r h) (index next : Index) : Inv (r.advance index next) (h ++ [(index, true)])

Reading a box in order keeps Inv, with the box read added.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.not_mem_eraseP_self {α : Type} [DecidableEq α] {e : α} {l : List α} : l.Nodup → e ∉ List.eraseP (fun (x : α) => decide (x = e)) l

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.found_inv {r : Reader} {h : History} (inv : Inv r h) (index : Index) (result : ReadResult) (next : Option Index) (window : ℕ) : Inv (r.found index result next window).2.1 (foundHistory r h index result next)

Reading a box keeps Inv.

A walk keeps Inv

@[simp]

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.jump_passed (r : Reader) (t : Index) (skipped : List Index) (steps : ℕ) : (r.jump t skipped steps).passed = r.passed + steps

@[simp]

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.jump_kept (r : Reader) (t : Index) (skipped : List Index) (steps : ℕ) : (r.jump t skipped steps).kept = r.kept ++ r.stepped skipped (r.passed + steps - skipped.length)

@[simp]

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.jump_last (r : Reader) (t : Index) (skipped : List Index) (steps : ℕ) : (r.jump t skipped steps).last = r.last

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.jump_lost (r : Reader) (t : Index) (skipped : List Index) (steps : ℕ) : (r.jump t skipped steps).lost = if r.passed < r.passed + steps - skipped.length then (r.lose r.passed r.last).lost else r.lost

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.mem_stepped {r : Reader} {skipped : List Index} {start : ℕ} {x : Index × ℕ × Option Index} (hx : x ∈ r.stepped skipped start) : ∃ (k : ℕ) (hk : k < skipped.length), x = (skipped[k], start + k, if k = 0 then r.last else skipped[k - 1]?)

Each box a walk kept: its index, position and the box before it.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.stepped_mem {r : Reader} {skipped : List Index} {start k : ℕ} (hk : k < skipped.length) : (skipped[k], start + k, if k = 0 then r.last else skipped[k - 1]?) ∈ r.stepped skipped start

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.stepped_positions (r : Reader) (skipped : List Index) (start : ℕ) : List.map (fun (x : Index × ℕ × Option Index) => x.2.1) (r.stepped skipped start) = List.map (fun (x : ℕ) => start + x) (List.range skipped.length)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.walkedHistory (h : History) (all : List Index) : History

What a walk adds to the history: every box it stepped past, unread.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.walkedHistory h all = h ++ List.map (fun (x : Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Index) => (x, false)) all

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.walked_grows (h : History) (all : List Index) : Grows h (walkedHistory h all)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.jump_inv {r : Reader} {h : History} (inv : Inv r h) (target : Index) (all skipped : List Index) (hall : skipped = List.drop (all.length - skipped.length) all) : Inv (r.jump target skipped all.length) (walkedHistory h all)

A jump keeps Inv. all is every box the walk stepped past, of which the driver handed back the last skipped.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.walked_inv {r : Reader} {h : History} (inv : Inv r h) (target : Index) (all skipped : List Index) (hall : skipped = List.drop (all.length - skipped.length) all) (window : ℕ) : Inv (r.walked (some target) skipped all.length window).1 (walkedHistory h all)

A walk keeps Inv.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.walked_none_inv {r : Reader} {h : History} (inv : Inv r h) (skipped : List Index) (steps window : ℕ) : Inv (r.walked none skipped steps window).1 h