Synchronous One-Error Gossip with Correction

Decidability / Model Checking

def Error.Value.all {n : ℕ} : List Value

Equations

• Error.Value.all = List.flatMap (fun (a : { x : ℕ // x ∈ List.range n }) => [(⟨↑a, ⋯⟩, true), (⟨↑a, ⋯⟩, false)]) (List.range n).attach

def Error.Value.all_spec {n✝ : ℕ} {x : Value} : x ∈ all

Equations

• ⋯ = ⋯

List of all distributions

def Error.Dist.all {n : ℕ} : List Dist

Equations

• Error.Dist.all = [fun (x : Error.Agent) => ⋯.elim]
• Error.Dist.all = List.flatMap (fun (f : Error.Dist) => [fun (k_1 : Error.Agent) => Fin.lastCases false f k_1, fun (k_1 : Error.Agent) => Fin.lastCases true f k_1]) Error.Dist.all

@[reducible, inline]

abbrev Error.Dist.forget {n : ℕ} (S : Dist) : Dist

Forget about the maximum agent.

Equations

• S.forget a = S (Fin.castSucc a)

theorem Error.Dist.all_spec {n : ℕ} (S : Dist) : S ∈ all

List of all calls

def Error.Call.castSucc {n : ℕ} : Call → Call

Equations

• ⌜a b⌝.castSucc = ⌜(Fin.castSucc a)⟨Fin.castSucc ↑b, ⋯⟩⌝
• ⌜a^c b⌝.castSucc = ⌜(Fin.castSucc a)^(Fin.castSucc c)⟨Fin.castSucc ↑b, ⋯⟩⌝
• ⌜a b^c⌝.castSucc = ⌜(Fin.castSucc a)⟨Fin.castSucc ↑b, ⋯⟩^(Fin.castSucc c)⌝

def Error.Call.allAmong {n : ℕ} : Agent → Agent → List Call

Equations

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

def Error.Call.all {n : ℕ} : List Call

Equations

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

theorem Error.Call.all_spec {n : ℕ} (C : Call) : C ∈ all

List of all OSequences of a given length

instance Error.instDecErrFree {n✝ : ℕ} {σ : Sequence} : Decidable (errFree σ)

Equations

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

instance Error.instDecMaxOne {n✝ : ℕ} {σ : Sequence} : Decidable (maxOne σ)

Equations

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

def Error.OSequence.fixLen_all {n : ℕ} (k : ℕ) : List { σ : OSequence // σ.length = k }

Equations

• One or more equations did not get rendered due to their size.
• Error.OSequence.fixLen_all 0 = [⟨⟨[], ⋯⟩, ⋯⟩]

@[irreducible]

theorem Error.OSequence.fixLen_all_spec {n k : ℕ} (σ : { σ : OSequence // σ.length = k }) : σ ∈ fixLen_all k

Deciding the Semantics

@[irreducible]

instance Error.instDecInvertMem {n : ℕ} {S : Dist} {σ : OSequence} {a c : Agent} {x : Value} : Decidable (x ∈ invert c (S⌈σ⌉a))

Decidability of membership in invert c (S⌈σ⌉a).

Equations

• Error.instDecInvertMem = ⋯.mpr Error.instDecResultSetMem

@[irreducible]

instance Error.instDecResultSetEq {n k : ℕ} {S T : Dist} {σ τ : { σ : OSequence // σ.length = k }} {a b : Agent} : Decidable (S⌈↑σ⌉a = T⌈↑τ⌉b)

Equations

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

@[irreducible]

instance Error.instDecInvertResultSetEq {n k : ℕ} {S T : Dist} {σ τ : { σ : OSequence // σ.length = k }} {c a b : Agent} : Decidable (invert c (S⌈↑σ⌉a) = T⌈↑τ⌉b)

Decidability of invert c (S⌈σ⌉a) = T⌈τ⌉b.

Equations

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

@[irreducible]

instance Error.instDecResultSetInvertEq {n k : ℕ} {S T : Dist} {σ τ : { σ : OSequence // σ.length = k }} {c a b : Agent} : Decidable (S⌈↑σ⌉a = invert c (T⌈↑τ⌉b))

Decidability of S⌈σ⌉a = invert c (T⌈τ⌉b).

Equations

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

@[irreducible]

instance Error.instDecInvertInvertEq {n k : ℕ} {S T : Dist} {σ τ : { σ : OSequence // σ.length = k }} {c d a b : Agent} : Decidable (invert c (S⌈↑σ⌉a) = invert d (T⌈↑τ⌉b))

Decidability of invert c (S⌈σ⌉a) = invert d (T⌈τ⌉b).

Equations

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

@[irreducible]

instance Error.instDecEquiv {n k : ℕ} {a : Agent} {S T : Dist} {σ τ : { σ : OSequence // σ.length = k }} : Decidable (equiv a (S, σ) (T, τ))

Equations

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

@[irreducible]

instance Error.instDecEval {n : ℕ} {S : Dist} {σ : OSequence} {φ : Form} : Decidable (S⌈σ⌉ ⊧ φ)

Equations

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