A matching upper bound for parity with shared gates

Cut the n inputs into k + 1 blocks of m = ⌈n / (k + 1)⌉ consecutive bits (SharedProgram.blockLength). Share the parity of the first block and then, for each of the next k - 1 blocks, the exclusive or of the last shared value with the block's parity, and output the exclusive or of the last shared value with the parity of the last block (SharedProgram.parityProgram, built from SharedProgram.xorChain). This program has k shared gates and computes parity (SharedProgram.parityProgram_computes).

A balanced formula for the parity of m consecutive bits (Formula.parityRange) has at most 2 m² gates (Formula.gates_parityRange_le), and each step z ⊕ φ = (z ∧ ¬φ) ∨ (¬z ∧ φ) reads φ and its De Morgan dual, so (k + 1) · gates ≤ 4 (n + k)² + 3 k (k + 1) (SharedProgram.mul_gates_parityProgram_le), which is at most 19 n² when k < n (SharedProgram.exists_parity_mul_gates_le_of_lt). Together with the lower bound n² ≤ (k + 1) · (gates + k + 1) of SharedProgram.parity_sq_le_gates, the minimum number of gates of a program with k shared gates computing parity is Θ(n² / (k + 1)) whenever 2 (k + 1)² ≤ n².

@[simp]

theorem Algebraic.KW.Formula.gates_xor {n : ℕ} (L R : Formula n) : (L.xor R).gates = 2 * (L.gates + R.gates) + 3

theorem Algebraic.KW.Formula.xor_eq_add (a b : Bool) : (a ^^ b) = a + b

On Bool, exclusive or is the addition used by parity.

@[irreducible]

def Algebraic.KW.Formula.parityRange {n : ℕ} : ℕ → ℕ → Formula n

A balanced formula for the parity of the inputs with index in [a, a + m): split the range in half and combine the halves with Formula.xor. Indices outside Fin n are skipped.

Equations

• Algebraic.KW.Formula.parityRange x✝ 0 = Algebraic.KW.Formula.const false
• Algebraic.KW.Formula.parityRange x✝ 1 = if h : x✝ < n then Algebraic.KW.Formula.lit ⟨x✝, h⟩ true else Algebraic.KW.Formula.const false
• Algebraic.KW.Formula.parityRange x✝ m.succ.succ = (Algebraic.KW.Formula.parityRange x✝ ((m + 2) / 2)).xor (Algebraic.KW.Formula.parityRange (x✝ + (m + 2) / 2) (m + 2 - (m + 2) / 2))

theorem Algebraic.KW.Formula.eval_parityRange {n : ℕ} (x : Fin n → Bool) (a m : ℕ) : (parityRange a m).eval x = ∑ i : Fin n, if a ≤ ↑i ∧ ↑i < a + m then x i else 0

theorem Algebraic.KW.Formula.gates_parityRange_add_two_le {n : ℕ} (a m : ℕ) : 1 ≤ m → (parityRange a m).gates + 2 ≤ 2 * m ^ 2

theorem Algebraic.KW.Formula.gates_parityRange_le {n : ℕ} (a m : ℕ) : (parityRange a m).gates ≤ 2 * m ^ 2

The balanced parity formula on m bits has at most 2 m² gates.

def Algebraic.KW.SharedProgram.xorChain {N r : ℕ} : Formula N → (Fin r → Formula N) → SharedProgram N r

The program that shares acc, then shares in turn the exclusive or z ⊕ ψ i of the last shared value z with each ψ i but the last, and outputs z ⊕ ψ (r - 1). It has r shared gates and computes acc ⊕ ψ 0 ⊕ ⋯ ⊕ ψ (r - 1).

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.KW.SharedProgram.xorChain x✝ x_5 = Algebraic.KW.SharedProgram.output x✝

theorem Algebraic.KW.SharedProgram.eval_xorChain {N r : ℕ} (acc : Formula N) (ψ : Fin r → Formula N) (x : Fin N → Bool) : (xorChain acc ψ).eval x = acc.eval x + ∑ i : Fin r, (ψ i).eval x

theorem Algebraic.KW.SharedProgram.gates_xorChain {N r : ℕ} (acc : Formula N) (ψ : Fin r → Formula N) : (xorChain acc ψ).gates = acc.gates + ∑ i : Fin r, (2 * (ψ i).gates + 3)

def Algebraic.KW.SharedProgram.blockLength (n k : ℕ) : ℕ

The block length ⌈n / (k + 1)⌉: k + 1 blocks of this length cover n inputs.

Equations

• Algebraic.KW.SharedProgram.blockLength n k = (n + k) / (k + 1)

theorem Algebraic.KW.SharedProgram.le_mul_blockLength (n k : ℕ) : n ≤ (k + 1) * blockLength n k

theorem Algebraic.KW.SharedProgram.mul_blockLength_le (n k : ℕ) : (k + 1) * blockLength n k ≤ n + k

def Algebraic.KW.SharedProgram.parityProgram (n k : ℕ) : SharedProgram n k

Parity with k shared gates: cut the inputs into k + 1 blocks of blockLength n k consecutive bits and chain the block parities with xorChain.

Equations

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

theorem Algebraic.KW.SharedProgram.parityProgram_computes (n k : ℕ) : (parityProgram n k).Computes GateElimination.Xor.parity

theorem Algebraic.KW.SharedProgram.mul_gates_parityProgram_le (n k : ℕ) : (k + 1) * (parityProgram n k).gates ≤ 4 * (n + k) ^ 2 + 3 * k * (k + 1)

theorem Algebraic.KW.SharedProgram.exists_parity_mul_gates_le (n k : ℕ) : ∃ (P : SharedProgram n k), P.Computes GateElimination.Xor.parity ∧ (k + 1) * P.gates ≤ 4 * (n + k) ^ 2 + 3 * k * (k + 1)

A matching upper bound. For all n and k some program with k shared gates computes the parity of n bits with (k + 1) · gates ≤ 4 (n + k)² + 3 k (k + 1).

theorem Algebraic.KW.SharedProgram.exists_parity_mul_gates_le_of_lt {n k : ℕ} (hk : k < n) : ∃ (P : SharedProgram n k), P.Computes GateElimination.Xor.parity ∧ (k + 1) * P.gates ≤ 19 * n ^ 2

A matching upper bound, for k < n. Some program with k shared gates computes the parity of n bits with at most 19 n² / (k + 1) gates.