Leader protocols (CRN-3)

The common shape of the threshold and remainder protocols of [AADFP06, proof of Lemma 5]. A state is a triple (leader bit, output bit, value u ∈ V). An encounter in which at least one agent is a leader makes the initiator the leader with value q(u, u') and the responder a non-leader with value r(u, u'), and sets both output bits to t(q(u, u')); an encounter of two non-leaders changes nothing. Inputs start as leaders with output bit t(u) (this initialisation makes the protocols correct also for a single agent, see FORMALIZATION_DIFFERENCES.md).

Generic facts proved here:

• invariants closed under steps: leaders output t of their value (LeadOut), a leader exists (HasLeader), weighted sums of the values are conserved if q + r conserves them (sum_step), non-leaders hold z if r always returns z (nonLeaderVal_step);
• leaders can be merged until at most one is left (exists_reaches_atMostOne), and a potential on the non-leaders' values can be decreased until no encounter with the leader decreases it (exists_reaches_noImprove);
• good configurations (one leader, with value L, and non-leaders with values satisfying R, where q(L, y) = q(y, L) = L and r(L, y) = r(y, L) = y for R y) are closed under steps, and from them the leader's output t L can be broadcast to every agent, which yields an output-stable configuration (Good.exists_outputStable).

def Crn.Leader.protocol {X : Type u_1} {V : Type u_2} (init : X → V) (q r : V → V → V) (t : V → Bool) : Protocol X (Bool × Bool × V)

The leader protocol with initial values init, merge functions q (initiator) and r (responder) and output test t.

Equations

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

theorem Crn.Leader.interact_of_not {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (c : Fin n → Bool × Bool × V) (e : AgentPair n) (h : ((c (↑e).1).1 || (c (↑e).2).1) = false) : (protocol init q r t).interact c e = c

An encounter of two non-leaders changes nothing.

theorem Crn.Leader.interact_fst {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (c : Fin n → Bool × Bool × V) (e : AgentPair n) (h : ((c (↑e).1).1 || (c (↑e).2).1) = true) : (protocol init q r t).interact c e (↑e).1 = (true, t (q (c (↑e).1).2.2 (c (↑e).2).2.2), q (c (↑e).1).2.2 (c (↑e).2).2.2)

In an encounter with a leader, the initiator becomes the leader with value q(u, u').

theorem Crn.Leader.interact_snd {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (c : Fin n → Bool × Bool × V) (e : AgentPair n) (h : ((c (↑e).1).1 || (c (↑e).2).1) = true) : (protocol init q r t).interact c e (↑e).2 = (false, t (q (c (↑e).1).2.2 (c (↑e).2).2.2), r (c (↑e).1).2.2 (c (↑e).2).2.2)

In an encounter with a leader, the responder becomes a non-leader with value r(u, u').

theorem Crn.Leader.step_cases {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {c d : Fin n → Bool × Bool × V} (h : (protocol init q r t).Step c d) : d = c ∨ ∃ (e : AgentPair n), ((c (↑e).1).1 || (c (↑e).2).1) = true ∧ d = (protocol init q r t).interact c e

A step either changes nothing or is an encounter involving a leader.

Invariants

def Crn.Leader.LeadOut {V : Type u_2} {n : ℕ} (t : V → Bool) (c : Fin n → Bool × Bool × V) : Prop

Every leader outputs t of its value.

Equations

• Crn.Leader.LeadOut t c = ∀ (w : Fin n), (c w).1 = true → (c w).2.1 = t (c w).2.2

def Crn.Leader.HasLeader {V : Type u_2} {n : ℕ} (c : Fin n → Bool × Bool × V) : Prop

Some agent is a leader.

Equations

• Crn.Leader.HasLeader c = ∃ (w : Fin n), (c w).1 = true

def Crn.Leader.AtMostOne {V : Type u_2} {n : ℕ} (c : Fin n → Bool × Bool × V) : Prop

At most one agent is a leader.

Equations

• Crn.Leader.AtMostOne c = ∀ (u w : Fin n), (c u).1 = true → (c w).1 = true → u = w

def Crn.Leader.NonLeaderVal {V : Type u_2} {n : ℕ} (z : V) (c : Fin n → Bool × Bool × V) : Prop

Every non-leader holds the value z.

Equations

• Crn.Leader.NonLeaderVal z c = ∀ (w : Fin n), (c w).1 = false → (c w).2.2 = z

theorem Crn.Leader.leadOut_step {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {c d : Fin n → Bool × Bool × V} (hc : LeadOut t c) (h : (protocol init q r t).Step c d) : LeadOut t d

LeadOut is preserved by steps.

theorem Crn.Leader.hasLeader_step {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {c d : Fin n → Bool × Bool × V} (h : (protocol init q r t).Step c d) (hc : HasLeader c) : HasLeader d

HasLeader is preserved by steps.

theorem Crn.Leader.eq_fst_of_atMostOne {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {c : Fin n → Bool × Bool × V} (hc : AtMostOne c) (e : AgentPair n) (he : ((c (↑e).1).1 || (c (↑e).2).1) = true) {w : Fin n} (hw : ((protocol init q r t).interact c e w).1 = true) : w = (↑e).1

After an encounter involving the only leader, the initiator is the only leader.

theorem Crn.Leader.atMostOne_step {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {c d : Fin n → Bool × Bool × V} (hc : AtMostOne c) (h : (protocol init q r t).Step c d) : AtMostOne d

AtMostOne is preserved by steps.

theorem Crn.Leader.nonLeaderVal_step {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {z : V} (hr : ∀ (a b : V), r a b = z) {c d : Fin n → Bool × Bool × V} (hc : NonLeaderVal z c) (h : (protocol init q r t).Step c d) : NonLeaderVal z d

If r always returns z, then NonLeaderVal z is preserved by steps.

theorem Crn.Leader.sum_step {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {M : Type u_3} [AddCancelCommMonoid M] {F : V → M} (hF : ∀ (a b : V), F (q a b) + F (r a b) = F a + F b) {c d : Fin n → Bool × Bool × V} (h : (protocol init q r t).Step c d) : ∑ w : Fin n, F (d w).2.2 = ∑ w : Fin n, F (c w).2.2

Weighted sums of the values are conserved if F(q(u, u')) + F(r(u, u')) = F(u) + F(u').

theorem Crn.Leader.hasLeader_input {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (hn : 0 < n) (ι : Fin n → X) : HasLeader ((protocol init q r t).input ∘ ι)

Initially every agent is a leader, so a nonempty population has one.

theorem Crn.Leader.leadOut_input {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (ι : Fin n → X) : LeadOut t ((protocol init q r t).input ∘ ι)

Initially every leader outputs t of its value.

theorem Crn.Leader.nonLeaderVal_input {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (z : V) (ι : Fin n → X) : NonLeaderVal z ((protocol init q r t).input ∘ ι)

Initially there are no non-leaders.

theorem Crn.Leader.sum_input {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} [Fintype X] [DecidableEq X] {M : Type u_3} [AddCommMonoid M] (F : V → M) (ι : Fin n → X) : ∑ w : Fin n, F (((protocol init q r t).input ∘ ι) w).2.2 = ∑ i : X, ↑(counts ι) i • F (init i)

The initial values, grouped by input symbol.

Merging the leaders

theorem Crn.Leader.exists_reaches_atMostOne {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (c : Fin n → Bool × Bool × V) : ∃ (d : Fin n → Bool × Bool × V), (protocol init q r t).Reaches c d ∧ AtMostOne d

The leaders can be merged until at most one is left.

Decreasing a potential

def Crn.Leader.NoImprove {V : Type u_2} {n : ℕ} (r : V → V → V) (μ : V → ℕ) (c : Fin n → Bool × Bool × V) : Prop

No encounter of a leader (as initiator) with a non-leader decreases the weight μ of the non-leader's value.

Equations

• Crn.Leader.NoImprove r μ c = ∀ (ℓ j : Fin n), (c ℓ).1 = true → (c j).1 = false → μ (c j).2.2 ≤ μ (r (c ℓ).2.2 (c j).2.2)

def Crn.Leader.pot {V : Type u_2} {n : ℕ} (μ : V → ℕ) (c : Fin n → Bool × Bool × V) : ℕ

The total weight ∑ μ of the non-leaders' values.

Equations

• Crn.Leader.pot μ c = ∑ w : Fin n, if (c w).1 = true then 0 else μ (c w).2.2

theorem Crn.Leader.pot_interact_lt {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (μ : V → ℕ) {c : Fin n → Bool × Bool × V} {ℓ j : Fin n} (hne : ℓ ≠ j) (hℓ : (c ℓ).1 = true) (hj : (c j).1 = false) (hlt : μ (r (c ℓ).2.2 (c j).2.2) < μ (c j).2.2) : pot μ ((protocol init q r t).interact c ⟨(ℓ, j), hne⟩) < pot μ c

An encounter of a leader (initiator) with a non-leader whose value decreases in weight decreases the potential.

theorem Crn.Leader.exists_reaches_noImprove {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} (μ : V → ℕ) (c : Fin n → Bool × Bool × V) (hc : AtMostOne c) : ∃ (d : Fin n → Bool × Bool × V), (protocol init q r t).Reaches c d ∧ AtMostOne d ∧ NoImprove r μ d

With at most one leader, encounters of the leader with non-leaders can be performed until none decreases the total weight ∑ μ of the non-leaders' values.

Good configurations and broadcasting the output

structure Crn.Leader.Good {V : Type u_2} {n : ℕ} (t : V → Bool) (L : V) (R : V → Prop) (c : Fin n → Bool × Bool × V) : Prop

Good configurations for the leader value L and the non-leader condition R: exactly one leader, which holds L and outputs t L, and non-leaders whose values satisfy R.

• exists_leader : ∃ (w : Fin n), (c w).1 = true
• unique : AtMostOne c
• leader (w : Fin n) : (c w).1 = true → (c w).2.2 = L ∧ (c w).2.1 = t L
• nonleader (w : Fin n) : (c w).1 = false → R (c w).2.2

theorem Crn.Leader.Good.merge {V : Type u_2} {n : ℕ} {q r : V → V → V} {t : V → Bool} {L : V} {R : V → Prop} (H : ∀ (y : V), R y → q L y = L ∧ r L y = y ∧ q y L = L ∧ r y L = y) {c : Fin n → Bool × Bool × V} (hc : Good t L R c) (e : AgentPair n) (he : ((c (↑e).1).1 || (c (↑e).2).1) = true) : q (c (↑e).1).2.2 (c (↑e).2).2.2 = L ∧ R (r (c (↑e).1).2.2 (c (↑e).2).2.2)

In a good configuration, an encounter involving the leader gives the initiator the value L and the responder the value of the non-leader.

theorem Crn.Leader.Good.step {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {L : V} {R : V → Prop} (H : ∀ (y : V), R y → q L y = L ∧ r L y = y ∧ q y L = L ∧ r y L = y) {c d : Fin n → Bool × Bool × V} (hc : Good t L R c) (h : (protocol init q r t).Step c d) : Good t L R d

Good configurations are closed under steps.

theorem Crn.Leader.Good.out_step {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {L : V} {R : V → Prop} (H : ∀ (y : V), R y → q L y = L ∧ r L y = y ∧ q y L = L ∧ r y L = y) {c : Fin n → Bool × Bool × V} (hc : Good t L R c) (e : AgentPair n) {w : Fin n} (hw : (c w).2.1 = t L) : ((protocol init q r t).interact c e w).2.1 = t L

In a good configuration, every encounter keeps correct outputs correct.

theorem Crn.Leader.Good.out_snd {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {L : V} {R : V → Prop} (H : ∀ (y : V), R y → q L y = L ∧ r L y = y ∧ q y L = L ∧ r y L = y) {c : Fin n → Bool × Bool × V} (hc : Good t L R c) (e : AgentPair n) (he : ((c (↑e).1).1 || (c (↑e).2).1) = true) : ((protocol init q r t).interact c e (↑e).2).2.1 = t L

In a good configuration, an encounter involving the leader sets the responder's output to t L.

theorem Crn.Leader.Good.exists_allOut {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {L : V} {R : V → Prop} (H : ∀ (y : V), R y → q L y = L ∧ r L y = y ∧ q y L = L ∧ r y L = y) {c : Fin n → Bool × Bool × V} (hc : Good t L R c) : ∃ (d : Fin n → Bool × Bool × V), (protocol init q r t).Reaches c d ∧ Good t L R d ∧ ∀ (w : Fin n), (d w).2.1 = t L

From a good configuration, the leader's output t L can be broadcast to all agents.

theorem Crn.Leader.Good.exists_outputStable {X : Type u_1} {V : Type u_2} {n : ℕ} {init : X → V} {q r : V → V → V} {t : V → Bool} {L : V} {R : V → Prop} (H : ∀ (y : V), R y → q L y = L ∧ r L y = y ∧ q y L = L ∧ r y L = y) {c : Fin n → Bool × Bool × V} (hc : Good t L R c) : ∃ (d : Fin n → Bool × Bool × V), (protocol init q r t).Reaches c d ∧ (protocol init q r t).OutputStable (t L) d

Output-stability of leader protocols. From a good configuration the protocol reaches an output-stable configuration with output t L.