Documentation

Complexity.Computability.Circuit.Boolean.Modular.InnerProduct

Modular inner products of unsigned word arrays #

Inputs are the complete first array followed by the complete second array, each in consecutive least-significant-first word blocks. Products run in parallel, then a balanced carry-save tree and one carry-lookahead addition compute the sum. The theorem applies to arbitrary raw words.

Main definitions #

Main results #

References #

This is the selected-row arithmetic used by Gentry, Sahai and Waters, Sections 3.1 and 3.4, with the modular multiplier and carry-save bounds proved in companion files.

source
def Cslib.Circuits.Boolean.Modular.innerProduct (k w : ℕ) :
Circuit signature (k * w + k * w) w

Compute all word products in parallel, then sum their carry-save representations.

Instances For
    source
    theorem Cslib.Circuits.Boolean.Modular.val_eval_innerProduct {k w : ℕ} (a b : BitString (k * w)) :
    ↑((BitString.equivFin w) ((innerProduct k w).eval interpretation (Fin.append a b))) = (∑ j : Fin k, ↑((BitString.equivFin w) (a.block j)) * ↑((BitString.equivFin w) (b.block j))) % 2 ^ w

    Exact inner-product value, including empty arrays and zero-width words.

    source
    theorem Cslib.Circuits.Boolean.Modular.depth_innerProduct_le (k w : ℕ) :
    (innerProduct k w).depth ≤ 17 + 16 * Nat.clog 2 (w + 1) + 12 * Nat.clog 2 k

    Both multiplication and the sum tree have logarithmic depth in their respective widths.

    source
    theorem Cslib.Circuits.Boolean.Modular.size_innerProduct_le (k w : ℕ) :
    (innerProduct k w).size ≤ 105 * (k + 1) * (w + 1) ^ 2

    Every product, fallback, pair-reduction gate and final addition is charged.