The walk to an acknowledged box

Indexes advance only by next, and each step adds one to the Idx64 (counter), so a reader reaches an acknowledged box by advancing to its Idx64. See "Rewrite and scan" in the group chat spec.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.Before {I : Type} (next : I → I) (a b : I) : Prop

b comes after a on their stream.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.Before next a b = ∃ (n : ℕ), 0 < n ∧ next^[n] a = b

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.stepsFrom {I : Type} (next : I → I) (start : I) (n : ℕ) : List I

The indexes start, next start, ... : the first n of the stream from start.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.stepsFrom next start n = List.map (fun (j : ℕ) => next^[j] start) (List.range n)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.keptOf {I : Type} (next : I → I) (start : I) (steps keep : ℕ) : List I

The last keep of the steps indexes from start, or all of them for keep = 0.

Equations

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

The walk

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.walk {I : Type} (next : I → I) (counter : I → ℕ) (targets : List ℕ) (start : I) (limit keep : ℕ) : Option (I × List I × ℕ)

Advance from start to the box at the furthest of targets fewer than limit boxes ahead: that box, the last keep indexes before it (all of them for keep = 0), and how many steps ahead it is.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.walkBoxes {I : Type} (next : I → I) [DecidableEq I] (boxes : List I) (start : I) (limit keep : ℕ) : Option (I × List I × ℕ)

Step forward from start, comparing whole indexes, to the furthest of boxes met within limit steps.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.Counts {I : Type} (next : I → I) (counter : I → ℕ) : Prop

Each step forward adds one to counter.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.Counts next counter = ∀ (i : I), counter (next i) = counter i + 1

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.counter_iterate {I : Type} {next : I → I} {counter : I → ℕ} (hc : Counts next counter) (i : I) (n : ℕ) : counter (next^[n] i) = counter i + n

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.le_of_max {l : List ℕ} {a b : ℕ} (h : l.max? = some a) (hb : b ∈ l) : b ≤ a

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.walk_some {I : Type} {next : I → I} {counter : I → ℕ} {targets : List ℕ} {start : I} {limit keep : ℕ} {b : I} {skipped : List I} {steps : ℕ} (h : walk next counter targets start limit keep = some (b, skipped, steps)) : ∃ (t : ℕ), (List.filter (fun (t : ℕ) => decide (counter start ≤ t) && decide (t < counter start + limit)) targets).max? = some t ∧ steps = t - counter start ∧ b = next^[steps] start ∧ skipped = keptOf next start steps keep

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.walk_target {I : Type} {next : I → I} {counter : I → ℕ} (hc : Counts next counter) {targets : List ℕ} {start : I} {limit keep : ℕ} {b : I} {skipped : List I} {steps : ℕ} (h : walk next counter targets start limit keep = some (b, skipped, steps)) : counter b ∈ targets ∧ next^[steps] start = b ∧ steps < limit ∧ (0 < steps → Before next start b)

The box a walk finds carries one of the targets and is the start stepped forward by the reported step count, within the limit.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.walk_skipped {I : Type} {next : I → I} {counter : I → ℕ} {targets : List ℕ} {start : I} {limit keep : ℕ} {b : I} {skipped : List I} {steps : ℕ} (h : walk next counter targets start limit keep = some (b, skipped, steps)) : skipped = List.drop (if keep = 0 then 0 else steps - keep) (stepsFrom next start steps)

The indexes a walk keeps are the last keep before the box it finds, in stream order.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.walk_furthest {I : Type} {next : I → I} {counter : I → ℕ} (hc : Counts next counter) {targets : List ℕ} {start : I} {limit keep : ℕ} {b : I} {skipped : List I} {steps : ℕ} (h : walk next counter targets start limit keep = some (b, skipped, steps)) (j : ℕ) : steps < j → j < limit → ¬counter (next^[j] start) ∈ targets

No target lies between the box a walk finds and its limit.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.walk_none {I : Type} {next : I → I} {counter : I → ℕ} (hc : Counts next counter) {targets : List ℕ} {start : I} {limit keep : ℕ} (h : walk next counter targets start limit keep = none) (j : ℕ) : j < limit → ¬counter (next^[j] start) ∈ targets

A walk that finds nothing has no target within its limit.

Naming a box by Idx64 finds the box its whole index names

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.OnStream {I : Type} (next : I → I) (s0 b : I) : Prop

b is a box of the stream that begins at s0.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.OnStream next s0 b = ∃ (n : ℕ), next^[n] s0 = b

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.eq_of_counter_eq {I : Type} {next : I → I} {counter : I → ℕ} (hc : Counts next counter) {s0 a b : I} (ha : OnStream next s0 a) (hb : OnStream next s0 b) (h : counter a = counter b) : a = b

On one stream, two boxes with the same Idx64 are the same box.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.max?_congr {l₁ l₂ : List ℕ} (h : ∀ (x : ℕ), x ∈ l₁ ↔ x ∈ l₂) : l₁.max? = l₂.max?

Two lists with the same members have the same greatest.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.max?_map_sub {l : List ℕ} {c : ℕ} (h : ∀ (x : ℕ), x ∈ l → c ≤ x) : (List.map (fun (x : ℕ) => x - c) l).max? = Option.map (fun (x : ℕ) => x - c) l.max?

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ReaderScan.walk_eq_walkBoxes {I : Type} {next : I → I} {counter : I → ℕ} [DecidableEq I] (hc : Counts next counter) {s0 start : I} (hstart : OnStream next s0 start) {boxes : List I} (hon : ∀ (b : I), b ∈ boxes → OnStream next s0 b) (limit keep : ℕ) : walk next counter (List.map counter boxes) start limit keep = walkBoxes next boxes start limit keep

When start and every target box are on one stream, walk by Idx64 returns the same result as walkBoxes.