Carry-save addition trees and logarithmic-depth bit counting

A 3-to-2 carry-save adder (csa3to2 w) reduces three w-bit words x, y, z to a bitwise exclusive-or word csaSum x y z and a shifted carry word csaCarry x y z in constant depth (≤ 6) and linear size (≤ 20 w), preserving the sum of their unsigned values modulo 2 ^ w (val_csaSum_add_val_csaCarry_mod). Two carry-save layers form a 4-to-2 reducer (csa4to2 w) that combines two redundant carry-save pairs (a₁, b₁) and (a₂, b₂) into one pair (s, c) in depth at most 12 and size at most 40 w.

Combining k one-bit inputs along a balanced binary tree (Circuit.balanced) of 4-to-2 reducers produces a carry-save pair whose sum modulo 2 ^ w is the Hamming weight BitString.weight x, in depth O(log k) and size O(k w). Iterating csa3to2 w with a zero third word w times (finishCircuit w w) clears a further carry bit at every step (sndBits_eval_finishCircuit_eq_false), collapsing the carry-save pair to a single w-bit binary numeral in depth O(w) and size O(w²). Taking w = ⌈log₂ (k + 1)⌉ gives a De Morgan circuit (weightCircuit k) of depth O(log k) and size O(k log k) that outputs the exact binary representation of BitString.weight x (val_eval_weightCircuit) Chandra, Stockmeyer and Vishkin, Vollmer, Chapter 1.

Main definitions

• Cslib.Circuits.Boolean.pairVal, Cslib.Circuits.Boolean.maj3, Cslib.Circuits.Boolean.csaSum, Cslib.Circuits.Boolean.csaCarry: carry-save pair value, 3-bit majority carry, and bitwise sum and shifted carry words on w-bit words.
• Cslib.Circuits.Boolean.csaSumFormula, Cslib.Circuits.Boolean.maj3Formula, Cslib.Circuits.Boolean.csaCarryFormula, Cslib.Circuits.Boolean.csa4to2FirstIn: coordinate formulas and input wiring for 3-to-2 and 4-to-2 carry-save reduction.
• Cslib.Circuits.Boolean.csa3to2, Cslib.Circuits.Boolean.csa4to2: 3-to-2 and 4-to-2 carry-save reduction circuits on w-bit words.
• Cslib.Circuits.Boolean.finishStepIn, Cslib.Circuits.Boolean.finishStep, Cslib.Circuits.Boolean.finishCircuit: carry-clearing step and iteration reducing a carry-save pair to a single w-bit word.
• Cslib.Circuits.Boolean.zeroPairCircuit, Cslib.Circuits.Boolean.bitPairCircuit, Cslib.Circuits.Boolean.weightPairCircuit, Cslib.Circuits.Boolean.weightCircuit: leaf circuits, balanced carry-save reduction tree, and De Morgan circuit computing the binary numeral of the Hamming weight of k input bits.

Main results

• Cslib.Circuits.Boolean.val_csaSum_add_val_csaCarry_mod: 3-to-2 carry-save reduction preserves the sum modulo 2 ^ w.
• Cslib.Circuits.Boolean.val_eval_weightCircuit: weightCircuit k computes the exact binary numeral of BitString.weight x in ⌈log₂ (k + 1)⌉ bits.
• Cslib.Circuits.Boolean.size_weightCircuit_le, Cslib.Circuits.Boolean.depth_weightCircuit_le: size O(k log k) and depth O(log k).

References

• [A. K. Chandra, L. Stockmeyer, U. Vishkin, Constant depth reducibility] [CSV84]
• H. Vollmer, Introduction to Circuit Complexity

Unsigned word values and carry-save arithmetic

def Cslib.Circuits.Boolean.pairVal {w : ℕ} (p : BitString (w + w)) : ℕ

The sum of the unsigned values of a carry-save pair of w-bit words.

@[simp]

theorem Cslib.Circuits.Boolean.pairVal_append {w : ℕ} (x y : BitString w) : pairVal (Fin.append x y) = ↑((BitString.equivFin w) x) + ↑((BitString.equivFin w) y)

The carry-save value of an appended pair (x, y) is the sum of the unsigned values of x and y.

def Cslib.Circuits.Boolean.maj3 (a b c : Bool) : Bool

The carry of a 1-bit full adder: whether at least two of the three bits are true.

theorem Cslib.Circuits.Boolean.toNat_xor_add_two_mul_toNat_maj3 (a b c : Bool) : (a ^^ b ^^ c).toNat + 2 * (maj3 a b c).toNat = a.toNat + b.toNat + c.toNat

Single-bit full-adder identity: the exclusive-or sum plus twice the majority carry equals the integer sum of the three input bits.

def Cslib.Circuits.Boolean.csaSum {w : ℕ} (x y z : BitString w) : BitString w

The bitwise exclusive-or word of a 3-to-2 carry-save adder on w-bit words.

def Cslib.Circuits.Boolean.csaCarry {w : ℕ} (x y z : BitString w) : BitString w

The shifted carry word of a 3-to-2 carry-save adder on w-bit words: bit 0 is false and bit i + 1 is the full-adder carry from bit i.

theorem Cslib.Circuits.Boolean.val_csaSum_add_val_csaCarry_mod {w : ℕ} (x y z : BitString w) : (↑((BitString.equivFin w) (csaSum x y z)) + ↑((BitString.equivFin w) (csaCarry x y z))) % 2 ^ w = (↑((BitString.equivFin w) x) + ↑((BitString.equivFin w) y) + ↑((BitString.equivFin w) z)) % 2 ^ w

Carry-save 3-to-2 invariant: the sum and shifted carry words have the same sum of unsigned values modulo 2 ^ w as the three input words.

theorem Cslib.Circuits.Boolean.csaCarry_eq_false_of_lt {w t : ℕ} (x y : BitString w) (hy : ∀ (i : Fin w), ↑i < t → y i = false) (i : Fin w) (hi : ↑i < t + 1) : csaCarry x y (fun (x : Fin w) => false) i = false

When the third word is zero and the first t bits of y are false, the first t + 1 bits of the shifted carry word csaCarry x y 0 are false.

3-to-2 and 4-to-2 carry-save circuits

def Cslib.Circuits.Boolean.csaSumFormula (w : ℕ) (i : Fin w) : Formula signature (w + (w + w))

Formula for bit i of csaSum on three w-bit words.

@[simp]

theorem Cslib.Circuits.Boolean.eval_csaSumFormula {w : ℕ} (i : Fin w) (u : BitString (w + (w + w))) : (csaSumFormula w i).eval interpretation u = csaSum u.fstBits u.sndBits.fstBits u.sndBits.sndBits i

csaSumFormula w i evaluates to bit i of csaSum on the three w-bit words of u.

@[simp]

theorem Cslib.Circuits.Boolean.size_csaSumFormula {w : ℕ} (i : Fin w) : (csaSumFormula w i).size = 15

csaSumFormula w i has size 15.

theorem Cslib.Circuits.Boolean.depth_csaSumFormula_le {w : ℕ} (i : Fin w) : (csaSumFormula w i).depth ≤ 6

csaSumFormula w i has depth at most 6.

def Cslib.Circuits.Boolean.maj3Formula {n : ℕ} (a b c : Fin n) : Formula signature n

Formula for maj3 on three input coordinates.

@[simp]

theorem Cslib.Circuits.Boolean.eval_maj3Formula {n : ℕ} (a b c : Fin n) (u : BitString n) : (maj3Formula a b c).eval interpretation u = maj3 (u a) (u b) (u c)

maj3Formula a b c evaluates to maj3 (u a) (u b) (u c).

@[simp]

theorem Cslib.Circuits.Boolean.size_maj3Formula {n : ℕ} (a b c : Fin n) : (maj3Formula a b c).size = 5

maj3Formula a b c has size 5.

theorem Cslib.Circuits.Boolean.depth_maj3Formula_le {n : ℕ} (a b c : Fin n) : (maj3Formula a b c).depth ≤ 3

maj3Formula a b c has depth at most 3.

def Cslib.Circuits.Boolean.csaCarryFormula (w : ℕ) (i : Fin w) : Formula signature (w + (w + w))

Formula for bit i of csaCarry on three w-bit words.

@[simp]

theorem Cslib.Circuits.Boolean.eval_csaCarryFormula {w : ℕ} (i : Fin w) (u : BitString (w + (w + w))) : (csaCarryFormula w i).eval interpretation u = csaCarry u.fstBits u.sndBits.fstBits u.sndBits.sndBits i

csaCarryFormula w i evaluates to bit i of csaCarry on the three w-bit words of u.

theorem Cslib.Circuits.Boolean.size_csaCarryFormula_le {w : ℕ} (i : Fin w) : (csaCarryFormula w i).size ≤ 5

csaCarryFormula w i has size at most 5.

theorem Cslib.Circuits.Boolean.depth_csaCarryFormula_le {w : ℕ} (i : Fin w) : (csaCarryFormula w i).depth ≤ 3

csaCarryFormula w i has depth at most 3.

def Cslib.Circuits.Boolean.csa3to2 (w : ℕ) : Circuit signature (w + (w + w)) (w + w)

3-to-2 carry-save adder: reduces three w-bit words to two w-bit words (sum, carry) with the same sum modulo 2 ^ w, using at most 20 w gates and depth at most 6.

@[simp]

theorem Cslib.Circuits.Boolean.eval_csa3to2 {w : ℕ} (u : BitString (w + (w + w))) : (csa3to2 w).eval interpretation u = Fin.append (csaSum u.fstBits u.sndBits.fstBits u.sndBits.sndBits) (csaCarry u.fstBits u.sndBits.fstBits u.sndBits.sndBits)

csa3to2 w evaluates to the pair (csaSum, csaCarry) on the three w-bit words of u.

theorem Cslib.Circuits.Boolean.pairVal_eval_csa3to2_mod {w : ℕ} (u : BitString (w + (w + w))) : pairVal ((csa3to2 w).eval interpretation u) % 2 ^ w = (↑((BitString.equivFin w) u.fstBits) + pairVal u.sndBits) % 2 ^ w

csa3to2 w preserves the sum of the three w-bit input words modulo 2 ^ w.

theorem Cslib.Circuits.Boolean.size_csa3to2_le (w : ℕ) : (csa3to2 w).size ≤ 20 * w

csa3to2 w has size at most 20 * w.

theorem Cslib.Circuits.Boolean.depth_csa3to2_le (w : ℕ) : (csa3to2 w).depth ≤ 6

csa3to2 w has depth at most 6.

def Cslib.Circuits.Boolean.csa4to2FirstIn (w : ℕ) : Fin (w + (w + w)) → Fin (w + w + (w + w))

Wiring selecting the first three w-bit words of two carry-save pairs.

def Cslib.Circuits.Boolean.csa4to2 (w : ℕ) : Circuit signature (w + w + (w + w)) (w + w)

4-to-2 carry-save reducer: combines two carry-save pairs (a₁, b₁) and (a₂, b₂) of w-bit words into a single carry-save pair in depth at most 12 and size at most 40 w.

theorem Cslib.Circuits.Boolean.pairVal_eval_csa4to2_mod {w : ℕ} (p₁ p₂ : BitString (w + w)) : pairVal ((csa4to2 w).eval interpretation (Fin.append p₁ p₂)) % 2 ^ w = (pairVal p₁ + pairVal p₂) % 2 ^ w

csa4to2 w preserves the sum of the two carry-save input pairs modulo 2 ^ w.

theorem Cslib.Circuits.Boolean.size_csa4to2_le (w : ℕ) : (csa4to2 w).size ≤ 40 * w

csa4to2 w has size at most 40 * w.

theorem Cslib.Circuits.Boolean.depth_csa4to2_le (w : ℕ) : (csa4to2 w).depth ≤ 12

csa4to2 w has depth at most 12.

Carry-clearing iteration

def Cslib.Circuits.Boolean.finishStepIn (w : ℕ) : Fin (w + (w + w)) → Fin (w + w + 1)

Wiring that appends w copies of a single constant wire to a (w + w)-bit carry-save pair.

def Cslib.Circuits.Boolean.finishStep (w : ℕ) : Circuit signature (w + w) (w + w)

One carry-clearing step: applies csa3to2 w to (a, b, 0), clearing one more low carry bit.

theorem Cslib.Circuits.Boolean.eval_finishStep {w : ℕ} (p : BitString (w + w)) : (finishStep w).eval interpretation p = Fin.append (csaSum p.fstBits p.sndBits fun (x : Fin w) => false) (csaCarry p.fstBits p.sndBits fun (x : Fin w) => false)

finishStep w evaluates to (csaSum a b 0, csaCarry a b 0) on the carry-save pair p = (a, b).

theorem Cslib.Circuits.Boolean.pairVal_eval_finishStep_mod {w : ℕ} (p : BitString (w + w)) : pairVal ((finishStep w).eval interpretation p) % 2 ^ w = pairVal p % 2 ^ w

finishStep w preserves the carry-save value modulo 2 ^ w.

theorem Cslib.Circuits.Boolean.size_finishStep_le (w : ℕ) : (finishStep w).size ≤ 20 * w + 1

finishStep w has size at most 20 * w + 1.

theorem Cslib.Circuits.Boolean.depth_finishStep_le (w : ℕ) : (finishStep w).depth ≤ 7

finishStep w has depth at most 7.

def Cslib.Circuits.Boolean.finishCircuit (w a✝ : ℕ) : Circuit signature (w + w) (w + w)

t steps of carry-clearing on a (w + w)-bit carry-save pair.

theorem Cslib.Circuits.Boolean.pairVal_eval_finishCircuit_mod {w : ℕ} (t : ℕ) (p : BitString (w + w)) : pairVal ((finishCircuit w t).eval interpretation p) % 2 ^ w = pairVal p % 2 ^ w

finishCircuit w t preserves the carry-save value modulo 2 ^ w.

theorem Cslib.Circuits.Boolean.sndBits_eval_finishCircuit_eq_false {w : ℕ} (t : ℕ) (p : BitString (w + w)) (i : Fin w) (hi : ↑i < t) : BitString.sndBits ((finishCircuit w t).eval interpretation p) i = false

After t carry-clearing steps, the first t bits of the carry word are false.

theorem Cslib.Circuits.Boolean.val_fstBits_eval_finishCircuit_mod {w : ℕ} (p : BitString (w + w)) : ↑((BitString.equivFin w) (BitString.fstBits ((finishCircuit w w).eval interpretation p))) % 2 ^ w = pairVal p % 2 ^ w

After w carry-clearing steps, the carry word is identically zero, so the first w-bit word has unsigned value congruent to pairVal p modulo 2 ^ w.

theorem Cslib.Circuits.Boolean.size_finishCircuit_le (w t : ℕ) : (finishCircuit w t).size ≤ t * (20 * w + 1)

finishCircuit w t has size at most t * (20 * w + 1).

theorem Cslib.Circuits.Boolean.depth_finishCircuit_le (w t : ℕ) : (finishCircuit w t).depth ≤ 7 * t

finishCircuit w t has depth at most 7 * t.

Balanced carry-save tree for Hamming weight

def Cslib.Circuits.Boolean.zeroPairCircuit (k w : ℕ) : Circuit signature k (w + w)

A carry-save pair of w-bit words all of whose bits are false, from one const false gate.

@[simp]

theorem Cslib.Circuits.Boolean.eval_zeroPairCircuit {w k : ℕ} (x : BitString k) : (zeroPairCircuit k w).eval interpretation x = fun (x : Fin (w + w)) => false

zeroPairCircuit k w outputs false on every wire.

@[simp]

theorem Cslib.Circuits.Boolean.size_zeroPairCircuit {w k : ℕ} : (zeroPairCircuit k w).size = 1

zeroPairCircuit k w has size 1.

theorem Cslib.Circuits.Boolean.depth_zeroPairCircuit_le {w k : ℕ} : (zeroPairCircuit k w).depth ≤ 1

zeroPairCircuit k w has depth at most 1.

def Cslib.Circuits.Boolean.bitPairCircuit (k w : ℕ) (j : Fin k) : Circuit signature k (w + w)

Leaf circuit placing input bit j : Fin k into bit 0 of the first w-bit word, and false on all other wires of the (w + w)-bit carry-save pair, using one const false gate.

theorem Cslib.Circuits.Boolean.pairVal_eval_bitPairCircuit_mod {w k : ℕ} (j : Fin k) (x : BitString k) : pairVal ((bitPairCircuit k w j).eval interpretation x) % 2 ^ w = (x j).toNat % 2 ^ w

bitPairCircuit k w j outputs a carry-save pair with value congruent to (x j).toNat modulo 2 ^ w.

@[simp]

theorem Cslib.Circuits.Boolean.size_bitPairCircuit {w k : ℕ} (j : Fin k) : (bitPairCircuit k w j).size = 1

bitPairCircuit k w j has size 1.

theorem Cslib.Circuits.Boolean.depth_bitPairCircuit_le {w k : ℕ} (j : Fin k) : (bitPairCircuit k w j).depth ≤ 1

bitPairCircuit k w j has depth at most 1.

def Cslib.Circuits.Boolean.weightPairCircuit (k w : ℕ) : Circuit signature k (w + w)

Balanced binary tree of csa4to2 w reducers over all k input bits.

theorem Cslib.Circuits.Boolean.pairVal_eval_weightPairCircuit_mod {w k : ℕ} (x : BitString k) : pairVal ((weightPairCircuit k w).eval interpretation x) % 2 ^ w = BitString.weight x % 2 ^ w

weightPairCircuit k w outputs a carry-save pair whose value is congruent to the Hamming weight BitString.weight x modulo 2 ^ w.

theorem Cslib.Circuits.Boolean.size_weightPairCircuit_le (k w : ℕ) : (weightPairCircuit k w).size ≤ max 1 k + k * (40 * w)

weightPairCircuit k w has size at most max 1 k + k * (40 * w).

theorem Cslib.Circuits.Boolean.depth_weightPairCircuit_le (k w : ℕ) : (weightPairCircuit k w).depth ≤ 1 + 12 * Nat.clog 2 k

weightPairCircuit k w has depth at most 1 + 12 * Nat.clog 2 k.

def Cslib.Circuits.Boolean.weightCircuit (k : ℕ) : Circuit signature k (Nat.clog 2 (k + 1))

Logarithmic-depth Hamming weight circuit: outputs the ⌈log₂ (k + 1)⌉-bit binary numeral of BitString.weight x (least significant bit first), using O(k log k) gates and depth O(log k).

theorem Cslib.Circuits.Boolean.val_eval_weightCircuit {k : ℕ} (x : BitString k) : ↑((BitString.equivFin (Nat.clog 2 (k + 1))) ((weightCircuit k).eval interpretation x)) = BitString.weight x

weightCircuit k computes the exact binary numeral of BitString.weight x.

theorem Cslib.Circuits.Boolean.size_weightCircuit_le (k : ℕ) : (weightCircuit k).size ≤ max 1 k + k * (40 * Nat.clog 2 (k + 1)) + Nat.clog 2 (k + 1) * (20 * Nat.clog 2 (k + 1) + 1)

weightCircuit k has size O(k log k).

theorem Cslib.Circuits.Boolean.depth_weightCircuit_le (k : ℕ) : (weightCircuit k).depth ≤ 1 + 19 * Nat.clog 2 (k + 1)

weightCircuit k has depth O(log k).