Logarithmic-depth modular multiplication

All shifted partial products are generated in parallel, reduced along the existing half-split carry-save tree, and finished by carry lookahead. The result is the product modulo 2 ^ w on every pair of words. Width zero uses the actual empty carry-save fallback and finishing circuit.

Main definitions

• Cslib.Circuits.Boolean.Modular.multiply: the complete unsigned modular multiplier.

Main results

• Cslib.Circuits.Boolean.Modular.val_eval_multiply: exact multiplication modulo 2 ^ w.
• Cslib.Circuits.Boolean.Modular.depth_multiply_le: depth at most 9 + 14 * clog 2 (w + 1).
• Cslib.Circuits.Boolean.Modular.size_multiply_le: at most 63 * (w + 1)^2 gates.

References

Binary partial products and carry-save reduction follow Vollmer, Chapter 1; parallel-prefix finishing follows Ladner and Fischer.

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

Reduce all shifted partial products and finish their sum with carry lookahead.

theorem Cslib.Circuits.Boolean.Modular.val_eval_multiply {w : ℕ} (a b : BitString w) : ↑((BitString.equivFin w) ((multiply w).eval interpretation (Fin.append a b))) = ↑((BitString.equivFin w) a) * ↑((BitString.equivFin w) b) % 2 ^ w

The circuit computes the modular product of arbitrary input words.

theorem Cslib.Circuits.Boolean.Modular.depth_multiply_le (w : ℕ) : (multiply w).depth ≤ 9 + 14 * Nat.clog 2 (w + 1)

The balanced pair tree uses one-level leaves and logarithmic-depth finishing.

theorem Cslib.Circuits.Boolean.Modular.size_multiply_le (w : ℕ) : (multiply w).size ≤ 63 * (w + 1) ^ 2

Every partial product and every carry-save gate is charged.