Documentation

Complexity.Computability.Circuit.Boolean.Modular.PartialProduct

Shifted partial products of unsigned words #

One circuit layer selects the shifted first word by one bit of the second word. Bits shifted past the output width are discarded; this computes a modular partial product on every input.

Main definitions #

Main results #

References #

The carry-save multiplication construction is standard binary partial-product arithmetic; see Vollmer, Chapter 1.

source
def Cslib.Circuits.Boolean.Modular.partialProduct (w : ℕ) (i : Fin w) :
Circuit signature (w + w) w

Multiply the first word by the ith bit of the second word, shifted by i.

Instances For
    source
    theorem Cslib.Circuits.Boolean.Modular.val_eval_partialProduct {w : ℕ} (i : Fin w) (a b : BitString w) :
    ↑((BitString.equivFin w) ((partialProduct w i).eval interpretation (Fin.append a b))) = if b i = true then ↑((BitString.equivFin w) a) * 2 ^ ↑i % 2 ^ w else 0

    Unsigned value of one shifted partial product, including overflow truncation.

    source
    @[simp]
    theorem Cslib.Circuits.Boolean.Modular.size_partialProduct {w : ℕ} (i : Fin w) :
    (partialProduct w i).size = w

    Exactly one gate per output bit, including the false low positions.

    source
    theorem Cslib.Circuits.Boolean.Modular.depth_partialProduct_le {w : ℕ} (i : Fin w) :
    (partialProduct w i).depth ≤ 1

    All product digits are produced in parallel at depth one.