The threshold protocol (CRN-3)

The protocol of [AADFP06, proof of Lemma 5(1)] for ∑ᵢ aᵢ xᵢ < c, as a leader protocol (Leader.protocol). Values are integers in [-s, s] with s = |c| + 1 + ∑ᵢ |aᵢ|; input i starts with value aᵢ. A leader encounter gives the initiator the clamped sum q(u, u') = max(-s, min(s, u + u')) and the responder the rest r(u, u') = u + u' - q(u, u'), and the output test is t(u) = [u < c]. Unlike AADFP06 (output bit 0), an input starts with output bit t(aᵢ), which is needed for a single agent (see FORMALIZATION_DIFFERENCES.md).

Correctness (stablyComputes): the sum of the values is ∑ᵢ aᵢ xᵢ; merge the leaders, then let the leader absorb the non-leaders' values while this decreases ∑ |u| over non-leaders. Then (classify) either all non-leaders hold 0, or the leader holds s and all non-leaders are ≥ 0, or the leader holds -s and all non-leaders are ≤ 0 (AADFP06's stable configurations), and the leader's test t is the predicate's value in each case.

@[reducible, inline]

abbrev Crn.ThresholdProtocol.Val (s : ℤ) : Type

Counter values u ∈ [-s, s].

Equations

• Crn.ThresholdProtocol.Val s = { u : ℤ // -s ≤ u ∧ u ≤ s }

instance Crn.ThresholdProtocol.instFiniteVal (s : ℤ) : Finite (Val s)

There are finitely many counter values.

def Crn.ThresholdProtocol.clamp (s z : ℤ) : ℤ

Clamping to [-s, s].

Equations

• Crn.ThresholdProtocol.clamp s z = max (-s) (min s z)

def Crn.ThresholdProtocol.q (s : ℤ) (u v : Val s) : Val s

The initiator's new value: the clamped sum.

Equations

• Crn.ThresholdProtocol.q s u v = ⟨Crn.ThresholdProtocol.clamp s (↑u + ↑v), ⋯⟩

def Crn.ThresholdProtocol.r (s : ℤ) (u v : Val s) : Val s

The responder's new value: the rest of the sum.

Equations

• Crn.ThresholdProtocol.r s u v = ⟨↑u + ↑v - Crn.ThresholdProtocol.clamp s (↑u + ↑v), ⋯⟩

def Crn.ThresholdProtocol.t (s c : ℤ) (u : Val s) : Bool

The output test [u < c].

Equations

• Crn.ThresholdProtocol.t s c u = decide (↑u < c)

theorem Crn.ThresholdProtocol.q_add_r (s : ℤ) (u v : Val s) : ↑(q s u v) + ↑(r s u v) = ↑u + ↑v

An encounter conserves the sum of the two values.

theorem Crn.ThresholdProtocol.classify {s : ℤ} (L y : Val s) (h : (↑y).natAbs ≤ (↑(r s L y)).natAbs) : ↑y = 0 ∨ ↑L = s ∧ 0 ≤ ↑y ∨ ↑L = -s ∧ ↑y ≤ 0

If no encounter with the leader holding L decreases |y|, then y = 0, or L = s and y ≥ 0, or L = -s and y ≤ 0.

theorem Crn.ThresholdProtocol.merge_zero {s : ℤ} (L y : Val s) : ↑y = 0 → q s L y = L ∧ r s L y = y ∧ q s y L = L ∧ r s y L = y

Stable shape 1: all non-leaders hold 0.

theorem Crn.ThresholdProtocol.merge_top {s : ℤ} (L : Val s) (hL : ↑L = s) (y : Val s) : 0 ≤ ↑y → q s L y = L ∧ r s L y = y ∧ q s y L = L ∧ r s y L = y

Stable shape 2: the leader holds s, the non-leaders are ≥ 0.

theorem Crn.ThresholdProtocol.merge_bot {s : ℤ} (L : Val s) (hL : ↑L = -s) (y : Val s) : ↑y ≤ 0 → q s L y = L ∧ r s L y = y ∧ q s y L = L ∧ r s y L = y

Stable shape 3: the leader holds -s, the non-leaders are ≤ 0.

def Crn.ThresholdProtocol.bound {X : Type u_1} [Fintype X] (a : X → ℤ) (c : ℤ) : ℤ

The bound s = |c| + 1 + ∑ᵢ |aᵢ| on the counter values.

Equations

• Crn.ThresholdProtocol.bound a c = |c| + 1 + ∑ i : X, |a i|

theorem Crn.ThresholdProtocol.bound_spec {X : Type u_1} [Fintype X] (a : X → ℤ) (c : ℤ) : c < bound a c ∧ -bound a c < c ∧ 1 ≤ bound a c

c < s, -s < c and s ≥ 1.

theorem Crn.ThresholdProtocol.abs_le_bound {X : Type u_1} [Fintype X] (a : X → ℤ) (c : ℤ) (i : X) : -bound a c ≤ a i ∧ a i ≤ bound a c

The coefficients lie in [-s, s].

def Crn.ThresholdProtocol.init {X : Type u_1} [Fintype X] (a : X → ℤ) (c : ℤ) (i : X) : Val (bound a c)

The initial value aᵢ of input i.

Equations

• Crn.ThresholdProtocol.init a c i = ⟨a i, ⋯⟩

def Crn.ThresholdProtocol.protocol {X : Type u_1} [Fintype X] (a : X → ℤ) (c : ℤ) : Protocol X (Bool × Bool × Val (bound a c))

The threshold protocol for ∑ᵢ aᵢ xᵢ < c [AADFP06, proof of Lemma 5(1)].

Equations

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

theorem Crn.ThresholdProtocol.stablyComputes {X : Type u_1} [Fintype X] [DecidableEq X] (a : X → ℤ) (c : ℤ) : (protocol a c).StablyComputes fun (x : X → ℕ) => decide (∑ i : X, a i * ↑(x i) < c)

[AADFP06, Lemma 5(1)] The threshold protocol stably computes ∑ᵢ aᵢ xᵢ < c.