Balanced sums of carry-save pairs

The existing half-split circuit tree reduces any list of carry-save pairs. Its value is their sum modulo 2 ^ w, including the empty list. One carry-lookahead addition finishes the result. These are the arithmetic reductions used by modular multiplication and GSW's selected-row product.

Main definitions

• Cslib.Circuits.Boolean.reducePairs: balanced four-to-two reduction on shared inputs.
• Cslib.Circuits.Boolean.sumPairs: reduction followed by logarithmic-depth addition.

Main results

• Cslib.Circuits.Boolean.pairVal_eval_reducePairs_mod: the sum of the supplied pair values.
• Cslib.Circuits.Boolean.val_eval_sumPairs: the resulting modular word.
• Cslib.Circuits.Boolean.depth_reducePairs_le: depth is logarithmic in the number of pairs.

References

The underlying carry-save construction and source credit are in Boolean.CarrySave; parallel-prefix finishing follows Ladner and Fischer.

def Cslib.Circuits.Boolean.pairWithZero {n w : ℕ} (C : Circuit signature n w) : Circuit signature n (w + w)

Put an ordinary word into carry-save form, with a shared false gate for the second word.

@[simp]

theorem Cslib.Circuits.Boolean.eval_pairWithZero {n w : ℕ} (C : Circuit signature n w) (x : BitString n) : (pairWithZero C).eval interpretation x = Fin.append (C.eval interpretation x) fun (x : Fin w) => false

theorem Cslib.Circuits.Boolean.pairVal_eval_pairWithZero {n w : ℕ} (C : Circuit signature n w) (x : BitString n) : pairVal ((pairWithZero C).eval interpretation x) = ↑((BitString.equivFin w) (C.eval interpretation x))

@[simp]

theorem Cslib.Circuits.Boolean.size_pairWithZero {n w : ℕ} (C : Circuit signature n w) : (pairWithZero C).size = C.size + 1

theorem Cslib.Circuits.Boolean.depth_pairWithZero_le {n w : ℕ} (C : Circuit signature n w) : (pairWithZero C).depth ≤ max C.depth 1

def Cslib.Circuits.Boolean.reducePairs (n w : ℕ) (cs : List (Circuit signature n (w + w))) : Circuit signature n (w + w)

Reduce carry-save pairs along the existing half-split tree; the empty sum is zero.

theorem Cslib.Circuits.Boolean.pairVal_eval_reducePairs_mod {n w : ℕ} (cs : List (Circuit signature n (w + w))) (x : BitString n) : pairVal ((reducePairs n w cs).eval interpretation x) % 2 ^ w = (List.map (fun (C : Circuit signature n (w + w)) => pairVal (C.eval interpretation x) % 2 ^ w) cs).sum % 2 ^ w

The reduction preserves the complete sum modulo the word modulus.

theorem Cslib.Circuits.Boolean.size_reducePairs_le {n w : ℕ} (cs : List (Circuit signature n (w + w))) : (reducePairs n w cs).size ≤ 1 + (List.map Circuit.size cs).sum + cs.length * (40 * w)

Charge the fallback only for the empty sum and every reduction gate for nonempty sums.

theorem Cslib.Circuits.Boolean.depth_reducePairs_le {n w : ℕ} (cs : List (Circuit signature n (w + w))) {D : ℕ} (hD : ∀ C ∈ cs, C.depth ≤ D) : (reducePairs n w cs).depth ≤ max D 1 + 12 * Nat.clog 2 cs.length

The pair tree adds twelve levels per half-split round to the deepest supplied circuit.

def Cslib.Circuits.Boolean.sumPairs (n w : ℕ) (cs : List (Circuit signature n (w + w))) : Circuit signature n w

Finish a balanced carry-save sum as one unsigned modular word.

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

Finishing a carry-save word computes its value modulo 2 ^ w.

theorem Cslib.Circuits.Boolean.val_eval_sumPairs {n w : ℕ} (cs : List (Circuit signature n (w + w))) (x : BitString n) : ↑((BitString.equivFin w) ((sumPairs n w cs).eval interpretation x)) = (List.map (fun (C : Circuit signature n (w + w)) => pairVal (C.eval interpretation x) % 2 ^ w) cs).sum % 2 ^ w

The final word equals the complete pair sum, reduced only modulo the word width.

theorem Cslib.Circuits.Boolean.size_sumPairs_le {n w : ℕ} (cs : List (Circuit signature n (w + w))) : (sumPairs n w cs).size ≤ 21 * (w + 1) ^ 2 + 1 + (List.map Circuit.size cs).sum + cs.length * (40 * w)

Polynomial gate bound retaining the sizes of the actual input circuits.

theorem Cslib.Circuits.Boolean.depth_sumPairs_le {n w : ℕ} (cs : List (Circuit signature n (w + w))) {D : ℕ} (hD : ∀ C ∈ cs, C.depth ≤ D) : (sumPairs n w cs).depth ≤ 8 + 2 * Nat.clog 2 (w + 1) + max D 1 + 12 * Nat.clog 2 cs.length

Logarithmic finishing in addition to the balanced pair-reduction depth.