De Morgan circuits for affine hashes

Fixed affine maps over the Boolean ring have polynomial circuit size. The four-gate XOR implementation is shared with the circuit synthesis API.

def Complexity.CircuitSparseSynthesis.Internal.hashBudget (n m : ℕ) : ℕ

Gate budget for m affine forms on n inputs, using four-gate XORs.

Equations

• Complexity.CircuitSparseSynthesis.Internal.hashBudget n m = m * (5 * (n + 1) + 1)

theorem Complexity.CircuitSparseSynthesis.Internal.exists_hashCircuit (n m : ℕ) (seed : BitString (PairwiseIndependentHash.affineSeedWidth n m)) : ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n m), c.Computes Cslib.Circuits.Boolean.interpretation (PairwiseIndependentHash.affineEval seed) ∧ c.size ≤ hashBudget n m