theorem makeCall_shares_secrets {n : ℕ} {a b : Fin n} : makeCall (initialState n) (a, b) a b

theorem addAgentOldOld {n : ℕ} {s : GossipState n} {i j : Fin n} : addAgent s i.castSucc j.castSucc ↔ s i j

theorem addAgentOldNew {n : ℕ} {s : GossipState n} {i : Fin n} : ¬addAgent s i.castSucc (Fin.last n)

theorem addAgentNewOld {n : ℕ} {s : GossipState n} {i : Fin n} : ¬addAgent s (Fin.last n) i.castSucc

theorem addAgentNewNew {n : ℕ} {s : GossipState n} : addAgent s (Fin.last n) (Fin.last n)

theorem persistsCallBefore (n : ℕ) (σ : List (Call n)) (i j k l : Fin n) : makeCalls (initialState n) σ i j → makeCalls (makeCall (initialState n) (k, l)) σ i j

theorem persistsCallAfter (n : ℕ) (i j k l : Fin n) (s : GossipState n) : s i j → makeCall s (k, l) i j

theorem initiallyOwnSecret (n : ℕ) (i : Fin n) : initialState n i i

theorem intiallyNoSecrets (n : ℕ) (i j : Fin n) : i ≠ j → ¬initialState n i j

def calls : List (Call 4)

Equations

• calls = [(0, 1), (1, 2), (2, 3), (3, 0)]

def calls_big : List (Call 10)

Equations

• calls_big = [(0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7), (7, 8), (8, 9), (9, 0)]