The remainder protocol (CRN-3)

The protocol of [AADFP06, proof of Lemma 5(2)] for ∑ᵢ aᵢ xᵢ ≡ c (mod m), as a leader protocol (Leader.protocol) with values in ZMod m (AADFP06 store (u + u') mod m in an integer field; the residues are the same). Input i starts with value aᵢ mod m and output bit [aᵢ ≡ c] (needed for a single agent, see FORMALIZATION_DIFFERENCES.md); a leader encounter gives the initiator the sum of the two values and the responder 0, and the output test is t(u) = [u = c].

Correctness (stablyComputes): the sum of the values is ∑ᵢ aᵢ xᵢ mod m and non-leaders hold 0, so once the leaders are merged the leader holds ∑ᵢ aᵢ xᵢ mod m, and its test is the predicate's value.

def Crn.RemainderProtocol.protocol {X : Type u_1} (a : X → ℤ) (c : ℤ) (m : ℕ) : Protocol X (Bool × Bool × ZMod m)

The remainder protocol for ∑ᵢ aᵢ xᵢ ≡ c (mod m) [AADFP06, proof of Lemma 5(2)].

Equations

• Crn.RemainderProtocol.protocol a c m = Crn.Leader.protocol (fun (i : X) => ↑(a i)) (fun (x1 x2 : ZMod m) => x1 + x2) (fun (x x_1 : ZMod m) => 0) fun (u : ZMod m) => decide (u = ↑c)

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

[AADFP06, Lemma 5(2)] The remainder protocol stably computes ∑ᵢ aᵢ xᵢ ≡ c (mod m).