Synchronous One-Error Gossip with Correction

Basics

Here we define: agents, values, distributions, calls, sequents.

We use n for the number of agents.

@[reducible, inline]

abbrev Error.Agent {n : ℕ} : Type

Equations

• Error.Agent = Fin n

@[reducible, inline]

abbrev Error.Value {n : ℕ} : Type

Equations

• Error.Value = (Error.Agent × Bool)

instance Error.instCoeAgentValue {n : ℕ} : Coe Agent Value

We allow writing just the agent a for the value ⟨a, true⟩.

Equations

• Error.instCoeAgentValue = { coe := fun (a : Error.Agent) => (a, true) }

def Error.«term‾_» : Lean.ParserDescr

We write ‾a for the value ⟨a, false⟩.

Equations

• Error.«term‾_» = Lean.ParserDescr.node `Error.«term‾_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "‾") (Lean.ParserDescr.cat `term 1023))

@[reducible, inline]

abbrev Error.Dist {n : ℕ} : Type

An initial secret distribution, each agent only has their own value.

Equations

• Error.Dist = (Error.Agent → Bool)

def Error.Dist.switch {n : ℕ} : Agent → Dist → Dist

In the given distribution, invert the value for this agent i

Equations

• Error.Dist.switch x✝¹ x✝ = fun (a : Error.Agent) => if a = x✝¹ then !x✝ a else x✝ a

inductive Error.Call {n : ℕ} : Type

• normal {n : ℕ} (caller : Agent) (callee : { b : Agent // b ≠ caller }) : Call

  ⌜a b⌝

• fstE {n : ℕ} (caller err : Agent) (callee : { b : Agent // b ≠ caller }) : Call

  ⌜a^c b⌝

• sndE {n : ℕ} (caller : Agent) (callee : { b : Agent // b ≠ caller }) (err : Agent) : Call

  ⌜a b^c⌝

def Error.«term⌜__⌝» : Lean.ParserDescr

Equations

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

def Error.«term⌜_^__⌝» : Lean.ParserDescr

Equations

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

def Error.«term⌜__^_⌝» : Lean.ParserDescr

Equations

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

def Error.Call.pair {n : ℕ} : Call → Agent × Agent

The pair of agents in the call, ignoring whether an error is made.

Equations

• ⌜a b⌝.pair = (a, ↑b)
• ⌜a^err b⌝.pair = (a, ↑b)
• ⌜a b^err⌝.pair = (a, ↑b)

@[reducible, inline]

abbrev Error.Sequence {n : ℕ} : Type

(Def 2) A sequence is a list of calls. For easy pattern matching this is in reverse order: the newest call is the first element.

Equations

• Error.Sequence = List Error.Call

def Error.invert {n : ℕ} : Agent → Set Value → Set Value

Flip the value of the secret of this agent in the given set.

Equations

• Error.invert x✝¹ x✝ = (fun (x : Error.Value) => match x with | (j, b) => if j = x✝¹ then (j, !b) else (j, b)) '' x✝

theorem Error.mem_invert_iff {n : ℕ} {c : Agent} {A : Set Value} {v : Value} : v ∈ invert c A ↔ (if v.1 = c then (v.1, !v.2) else v) ∈ A

Membership in invert c A reduces to membership of the "flipped" value in A.

Syntax

inductive Error.Form {n : ℕ} : Type

(Def 3) Logical language

• Top {n : ℕ} : Form

  True constant

• Con {n : ℕ} : Form → Form → Form

  Conjunction

• Neg {n : ℕ} : Form → Form

  Negation

• Has {n : ℕ} (a : Agent) : Value → Form

  Has a (b, k) means agent a has value k of agent b.

• K {n : ℕ} (a : Agent) (φ : Form) : Form

  K a φ means agent a knows that φ is true.

def Error.Form.length {n : ℕ} : Form → ℕ

Equations

• Error.Form.Top.length = 0
• (φ1 ⋀ φ2).length = 1 + φ1.length + φ2.length
• ( ¬'φ).length = 1 + φ.length
• (a_1@a).length = 1
• (Error.Form.K a φ).length = 1 + φ.length

Roles

inductive Error.Role : Type

• Caller : Role
• Callee : Role
• Other : Role

  Not participating in the call

instance Error.instDecidableEqRole : DecidableEq Role

Equations

• Error.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Error.roleOfIn {n : ℕ} (i : Agent) (c : Call) : Role

What is the Role of i in this call?

Equations

• Error.roleOfIn i ⌜a b⌝ = if i = a then Error.Role.Caller else if i = ↑b then Error.Role.Callee else Error.Role.Other
• Error.roleOfIn i ⌜a^err b⌝ = if i = a then Error.Role.Caller else if i = ↑b then Error.Role.Callee else Error.Role.Other
• Error.roleOfIn i ⌜a b^err⌝ = if i = a then Error.Role.Caller else if i = ↑b then Error.Role.Callee else Error.Role.Other

@[simp]

theorem Error.roleOfIn_eq_caller {n : ℕ} {a : Agent} {b : { b : Agent // b ≠ a }} : roleOfIn a ⌜a b⌝ = Role.Caller

@[simp]

theorem Error.roleOfIn_eq_callee {n : ℕ} {a : Agent} {b : { b : Agent // b ≠ a }} : roleOfIn ↑b ⌜a b⌝ = Role.Callee

@[simp]

theorem Error.roleOfIn_fstE_eq_caller {n : ℕ} {a c : Agent} {b : { b : Agent // b ≠ a }} : roleOfIn a ⌜a^c b⌝ = Role.Caller

@[simp]

theorem Error.roleOfIn_fstE_eq_callee {n : ℕ} {a c : Agent} {b : { b : Agent // b ≠ a }} : roleOfIn ↑b ⌜a^c b⌝ = Role.Callee

@[simp]

theorem Error.roleOfIn_sndE_eq_caller {n : ℕ} {a c : Agent} {b : { b : Agent // b ≠ a }} : roleOfIn a ⌜a b^c⌝ = Role.Caller

@[simp]

theorem Error.roleOfIn_sndE_eq_callee {n : ℕ} {a c : Agent} {b : { b : Agent // b ≠ a }} : roleOfIn ↑b ⌜a b^c⌝ = Role.Callee

@[simp]

theorem Error.roleOfIn_eq_Caller_iff {n✝ : ℕ} {a x : Agent} {y : { b : Agent // b ≠ x }} : roleOfIn a ⌜x y⌝ = Role.Caller ↔ a = x

@[simp]

theorem Error.roleOfIn_eq_Callee_iff {n✝ : ℕ} {a x : Agent} {y : { b : Agent // b ≠ x }} : roleOfIn a ⌜x y⌝ = Role.Callee ↔ a ≠ x ∧ a = ↑y

@[simp]

theorem Error.roleOfIn_eq_Other_iff {n✝ : ℕ} {a x : Agent} {y : { b : Agent // b ≠ x }} : roleOfIn a ⌜x y⌝ = Role.Other ↔ a ≠ x ∧ a ≠ ↑y

@[simp]

theorem Error.roleOfIn_fstE_eq_Caller_iff {n✝ : ℕ} {a x z : Agent} {y : { b : Agent // b ≠ x }} : roleOfIn a ⌜x^z y⌝ = Role.Caller ↔ a = x

@[simp]

theorem Error.roleOfIn_fstE_eq_Callee_iff {n✝ : ℕ} {a x z : Agent} {y : { b : Agent // b ≠ x }} : roleOfIn a ⌜x^z y⌝ = Role.Callee ↔ a ≠ x ∧ a = ↑y

@[simp]

theorem Error.roleOfIn_fstE_eq_Other_iff {n✝ : ℕ} {a x z : Agent} {y : { b : Agent // b ≠ x }} : roleOfIn a ⌜x^z y⌝ = Role.Other ↔ a ≠ x ∧ a ≠ ↑y

@[simp]

theorem Error.roleOfIn_sndE_eq_Caller_iff {n✝ : ℕ} {a x : Agent} {y : { b : Agent // b ≠ x }} {z : Agent} : roleOfIn a ⌜x y^z⌝ = Role.Caller ↔ a = x

@[simp]

theorem Error.roleOfIn_sndE_eq_Callee_iff {n✝ : ℕ} {a x : Agent} {y : { b : Agent // b ≠ x }} {z : Agent} : roleOfIn a ⌜x y^z⌝ = Role.Callee ↔ a ≠ x ∧ a = ↑y

@[simp]

theorem Error.roleOfIn_sndE_eq_Other_iff {n✝ : ℕ} {a x : Agent} {y : { b : Agent // b ≠ x }} {z : Agent} : roleOfIn a ⌜x y^z⌝ = Role.Other ↔ a ≠ x ∧ a ≠ ↑y

@[simp]

theorem Error.roleOfIn_pair_fst {n✝ : ℕ} {C : Call} : roleOfIn C.pair.1 C = Role.Caller

@[simp]

theorem Error.roleOfIn_pair_snd {n✝ : ℕ} {C : Call} : roleOfIn C.pair.2 C = Role.Callee

Sequences with at most one transmission error

def Error.errFree {n : ℕ} : Sequence → Prop

This sequence contains no transmission errors.

Equations

• Error.errFree [] = True
• Error.errFree (⌜caller callee⌝ :: rest) = Error.errFree rest
• Error.errFree (⌜caller^err callee⌝ :: tail) = False
• Error.errFree (⌜caller callee^err⌝ :: tail) = False

@[simp]

theorem Error.errFree_nil {n : ℕ} : errFree []

def Error.maxOne {n : ℕ} : Sequence → Prop

This sequence contains at most one transmission error.

Equations

• Error.maxOne [] = True
• Error.maxOne (⌜caller callee⌝ :: rest) = Error.maxOne rest
• Error.maxOne (⌜caller^err callee⌝ :: tail) = Error.errFree tail
• Error.maxOne (⌜caller callee^err⌝ :: tail) = Error.errFree tail

@[simp]

theorem Error.maxOne_nil {n : ℕ} : maxOne []

theorem Error.Sequence.maxOne_of_errFree {n✝ : ℕ} {σ : Sequence} : errFree σ → maxOne σ

theorem Error.Sequence.maxOne_cons {n✝ : ℕ} {C : Call} {σ : List Call} : maxOne (C :: σ) → maxOne σ

def Error.«term⁻_» : Lean.ParserDescr

If o proves that C :: σ has at most one error then we use the short notation ⁻o to get a proof that σ has at most one error.

Equations

• Error.«term⁻_» = Lean.ParserDescr.node `Error.«term⁻_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⁻") (Lean.ParserDescr.cat `term 1023))

def Error.OSequence {n : ℕ} : Type

Sequence with at most one error.

Equations

• Error.OSequence = Subtype Error.maxOne

def Error.«term_⊑_» : Lean.TrailingParserDescr

Subsequence relation: σ⊑τ means that τ extends σ. Because sequences are lists with the newest call first we define this as List.IsSuffix σ τ.

Equations

• Error.«term_⊑_» = Lean.ParserDescr.trailingNode `Error.«term_⊑_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊑") (Lean.ParserDescr.cat `term 1023))

instance Error.instCoeOSequenceSequence {n : ℕ} : Coe OSequence Sequence

Equations

• Error.instCoeOSequenceSequence = { coe := Subtype.val }

def Error.OSequence.length {n : ℕ} (σ : OSequence) : ℕ

Equations

• σ.length = List.length ↑σ

def Error.OSequence.nil {n : ℕ} : OSequence

Equations

• Error.OSequence.nil = ⟨[], ⋯⟩

@[simp]

theorem Error.OSequence.length_nil {n : ℕ} {h : Error.maxOne []} : length ⟨[], h⟩ = 0

@[simp]

theorem Error.OSequence.length_def {n : ℕ} (σ : Sequence) (h : Error.maxOne σ) : length ⟨σ, h⟩ = List.length σ

@[simp]

theorem Error.OSequence.ofLen_length {n k : ℕ} (σ : { σ : OSequence // σ.length = k }) : (↑σ).length = k

@[simp]

theorem Error.OSequence.maxOne {n : ℕ} {σ : OSequence} : Error.maxOne ↑σ

Semantics

@[irreducible]

def Error.resultSet {n : ℕ} (i : Agent) : Dist → OSequence → Set Value

(Def 4) Semantics of call. What values does this agent have after this sequence?

Equations

• One or more equations did not get rendered due to their size.
• x✝⌈⟨[], property⟩⌉i = {(i, x✝ i)}
• x⌈⟨C :: σ, o⟩⌉i = x⌈⟨σ, ⋯⟩⌉i

@[irreducible]

def Error.contribSet {n : ℕ} (S : Dist) (σ : OSequence) : Call → Set Value × Set Value

Right after sequence σ, what values will caller and callee contribute to the call?

Equations

• Error.contribSet S σ ⌜a b⌝ = (S⌈σ⌉a, S⌈σ⌉↑b)
• Error.contribSet S σ ⌜a^err b⌝ = (Error.invert err (S⌈σ⌉a), S⌈σ⌉↑b)
• Error.contribSet S σ ⌜a b^err⌝ = (S⌈σ⌉a, Error.invert err (S⌈σ⌉↑b))

@[irreducible]

def Error.equiv {n k : ℕ} (a : Agent) : Dist × { σ : OSequence // σ.length = k } → Dist × { σ : OSequence // σ.length = k } → Prop

(Def 5) Observation relation. This is synchronous.

Equations

• One or more equations did not get rendered due to their size.
• Error.equiv a (S, ⟨⟨[], property⟩, property_1⟩) (T, ⟨⟨[], property_2⟩, property_3⟩) = (S a = T a)

@[irreducible]

def Error.eval {n : ℕ} : Dist → OSequence → Form → Prop

(Def 6) Semantics.

Equations

• x✝¹⌈x✝⌉ ⊧ Error.Form.Top = True
• x✝¹⌈x✝⌉ ⊧ ( ¬'φ) = ¬x✝¹⌈x✝⌉ ⊧ φ
• x✝¹⌈x✝⌉ ⊧ (j, k)@a = ((j, k) ∈ x✝¹⌈x✝⌉a)
• x✝¹⌈x✝⌉ ⊧ (φ ⋀ ψ) = (x✝¹⌈x✝⌉ ⊧ φ ∧ x✝¹⌈x✝⌉ ⊧ ψ)
• x✝¹⌈x✝⌉ ⊧ Error.Form.K a φ = ∀ (T : Error.Dist) (τ : { σ : Error.OSequence // σ.length = x✝.length }), Error.equiv a (x✝¹, ⟨x✝, ⋯⟩) (T, τ) → T⌈↑τ⌉ ⊧ φ

def Error.«term_⌈_⌉_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem Error.resultSet_nil {n : ℕ} {o : maxOne []} {S : Dist} {i : Agent} : S⌈⟨[], o⟩⌉i = {(i, S i)}

@[simp]

theorem Error.equiv_nil {n✝ : ℕ} {i : Agent} {S : Dist} {o1 : maxOne []} {a✝ : ℕ} {h1 : OSequence.length ⟨[], o1⟩ = a✝} {T : Dist} {o2 : maxOne []} {h2 : OSequence.length ⟨[], o2⟩ = a✝} : equiv i (S, ⟨⟨[], o1⟩, h1⟩) (T, ⟨⟨[], o2⟩, h2⟩) ↔ S i = T i

Notation and Abbreviations

def Error.«term¬'_» : Lean.ParserDescr

Equations

• Error.«term¬'_» = Lean.ParserDescr.node `Error.«term¬'_» 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ¬'") (Lean.ParserDescr.cat `term 70))

def Error.«term_⋀_» : Lean.TrailingParserDescr

Equations

• Error.«term_⋀_» = Lean.ParserDescr.trailingNode `Error.«term_⋀_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋀ ") (Lean.ParserDescr.cat `term 60))

def Error.«term_⋁_» : Lean.TrailingParserDescr

Equations

• Error.«term_⋁_» = Lean.ParserDescr.trailingNode `Error.«term_⋁_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋁ ") (Lean.ParserDescr.cat `term 1023))

def Error.«term_⟹_» : Lean.TrailingParserDescr

Equations

• Error.«term_⟹_» = Lean.ParserDescr.trailingNode `Error.«term_⟹_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⟹") (Lean.ParserDescr.cat `term 1023))

def Error.«term_⇔_» : Lean.TrailingParserDescr

Equations

• Error.«term_⇔_» = Lean.ParserDescr.trailingNode `Error.«term_⇔_» 1022 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ ") (Lean.ParserDescr.cat `term 1022))

def Error.«term_@_» : Lean.TrailingParserDescr

We write v @ a to say that agent a has value v.

Equations

• Error.«term_@_» = Lean.ParserDescr.trailingNode `Error.«term_@_» 1022 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1023))

def Error.termKv__ : Lean.ParserDescr

Equations

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

def Error.«term_⌈_⌉⊧_» : Lean.TrailingParserDescr

Equations

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

def Error.valid {n : ℕ} (φ : Form) : Prop

Validity of formulas

Equations

• ⊨ φ = ∀ (S : Error.Dist) (σ : Error.OSequence), S⌈σ⌉ ⊧ φ

def Error.«term⊨_» : Lean.ParserDescr

Equations

• Error.«term⊨_» = Lean.ParserDescr.node `Error.«term⊨_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊨ ") (Lean.ParserDescr.cat `term 100))

theorem Error.eval_biimpl {n✝ : ℕ} {S : Dist} {σ : OSequence} {φ1 φ2 : Form} : S⌈σ⌉ ⊧ ( ¬'( ¬' ¬'φ1 ⋀ ¬'φ2) ⋀ ¬'( ¬' ¬'φ2 ⋀ ¬'φ1)) ↔ (S⌈σ⌉ ⊧ φ1 ↔ S⌈σ⌉ ⊧ φ2)

theorem Error.eval_impl {n✝ : ℕ} {S : Dist} {σ : OSequence} {φ1 φ2 : Form} : S⌈σ⌉ ⊧ ( ¬'( ¬' ¬'φ1 ⋀ ¬'φ2)) ↔ S⌈σ⌉ ⊧ φ1 → S⌈σ⌉ ⊧ φ2

theorem Error.eval_con {n✝ : ℕ} {S : Dist} {σ : OSequence} {φ1 φ2 : Form} : S⌈σ⌉ ⊧ (φ1 ⋀ φ2) ↔ S⌈σ⌉ ⊧ φ1 ∧ S⌈σ⌉ ⊧ φ2

theorem Error.eval_dis {n✝ : ℕ} {S : Dist} {σ : OSequence} {φ1 φ2 : Form} : S⌈σ⌉ ⊧ ( ¬'( ¬'φ1 ⋀ ¬'φ2)) ↔ S⌈σ⌉ ⊧ φ1 ∨ S⌈σ⌉ ⊧ φ2

The observation relation is an equivalence

def Error.equi {n : ℕ} (a : Agent) (Sσ Tτ : Dist × OSequence) : Prop

An abbreviation to easily say that we have the same length and (can thus say) equiv.

Equations

• Sσ ~_ a Tτ = ∃ (h : Sσ.2.length = Tτ.2.length), Error.equiv a (Sσ.1, ⟨Sσ.2, ⋯⟩) (Tτ.1, ⟨Tτ.2, ⋯⟩)

def Error.«term_~___» : Lean.TrailingParserDescr

Equations

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

theorem Error.equi_of_equiv {n✝ : ℕ} {a : Agent} {S : Dist} {σ : OSequence} {a✝ : ℕ} {h1 : σ.length = a✝} {T : Dist} {τ : OSequence} {h2 : τ.length = a✝} : equiv a (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩) → (S, σ) ~_ a(T, τ)

theorem Error.equiv_of_equi {n✝ : ℕ} {a : Agent} {S : Dist} {σ : OSequence} {T : Dist} {τ : OSequence} {a✝ : ℕ} {h1 : σ.length = a✝} {h2 : τ.length = a✝} : (S, σ) ~_ a(T, τ) → equiv a (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩)

theorem Error.sameRole_of_equiv {n✝ : ℕ} {a : Agent} {S : Dist} {C₁ : Call} {σ : List Call} {o1 : maxOne (C₁ :: σ)} {a✝ : ℕ} {h1 : OSequence.length ⟨C₁ :: σ, o1⟩ = a✝} {T : Dist} {C₂ : Call} {τ : List Call} {o2 : maxOne (C₂ :: τ)} {h2 : OSequence.length ⟨C₂ :: τ, o2⟩ = a✝} : equiv a (S, ⟨⟨C₁ :: σ, o1⟩, h1⟩) (T, ⟨⟨C₂ :: τ, o2⟩, h2⟩) → roleOfIn a C₁ = roleOfIn a C₂

@[simp, irreducible]

theorem Error.equiv_refl {n : ℕ} {a : Agent} {S : Dist} {k : ℕ} {σ : { σ : OSequence // σ.length = k }} : equiv a (S, σ) (S, σ)

theorem Error.equiv_symm {n : ℕ} {i : Agent} {m : ℕ} {S : Dist} {σ : OSequence} {h1 : σ.length = m} {T : Dist} {τ : OSequence} {h2 : τ.length = m} : equiv i (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩) ↔ equiv i (T, ⟨τ, h2⟩) (S, ⟨σ, h1⟩)

theorem Error.equiv_trans {n : ℕ} {a : Agent} {m : ℕ} {S : Dist} {σ : OSequence} {h1 : σ.length = m} {T : Dist} {τ : OSequence} {h2 : τ.length = m} {R : Dist} {ρ : OSequence} {h3 : ρ.length = m} : equiv a (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩) → equiv a (T, ⟨τ, h2⟩) (R, ⟨ρ, h3⟩) → equiv a (S, ⟨σ, h1⟩) (R, ⟨ρ, h3⟩)

theorem Error.equiv_Equivalence {n k : ℕ} {i : Agent} : Equivalence (equiv i)

The observation relation equiv $∼_a$ is an equivalence relation.

theorem Error.equiv_then_know_same {n : ℕ} {a : Agent} {m : ℕ} {S : Dist} {σ : OSequence} {h1 : σ.length = m} {T : Dist} {τ : OSequence} {h2 : τ.length = m} (equ : equiv a (S, ⟨σ, h1⟩) (T, ⟨τ, h2⟩)) (φ : Form) : S⌈σ⌉ ⊧ Form.K a φ ↔ T⌈τ⌉ ⊧ Form.K a φ

theorem Error.not_in_call_equiv_of_equiv {n : ℕ} {κ : Call} {σ : Sequence} {o : maxOne (κ :: σ)} {τ : Sequence} {p : maxOne (κ :: τ)} {h1 : OSequence.length ⟨τ, ⋯⟩ = OSequence.length ⟨σ, ⋯⟩} {h2 : OSequence.length ⟨κ :: τ, p⟩ = OSequence.length ⟨κ :: σ, o⟩} {S T : Dist} (a : Agent) (not_in_call : roleOfIn a κ = Role.Other) (equ_before : equiv a (S, ⟨⟨σ, ⋯⟩, ⋯⟩) (T, ⟨⟨τ, ⋯⟩, h1⟩)) : equiv a (S, ⟨⟨κ :: σ, o⟩, ⋯⟩) (T, ⟨⟨κ :: τ, p⟩, h2⟩)