One layer of Uhlig's construction

Split the input of f into a prefix of p bits and a suffix of w bits. For each of the 2 ^ p prefixes, the restriction of f is a function of the suffix. Uhlig's code of these restrictions gives 2 ^ p + 1 resource functions on w bits (resource). Group 2 t copies into t pairs. In each pair, every resource reads the suffix of the copy that uses it (BitString.Uhlig.first, BitString.Uhlig.second); each copy then sums its resources. Hence t copies of every resource yield 2 t copies of f, at an overhead linear in t.

The routing and decoding gates are disjunctive normal forms of the two prefixes in a pair, so their number is polynomial in 2 ^ p and w. This is far from optimal, but it is negligible in the recursion of Uhlig, where 2 ^ p is polynomial in the input length.

Sizes count all gates, including constants and negations. The theorem bounds circuit size; it does not certify the running time of any circuit constructor.

Main definitions

• Cslib.Circuits.Boolean.MassProduction.Uhlig.restriction: the restrictions of f to prefixes, numbered by BitString.equivFin.
• Cslib.Circuits.Boolean.MassProduction.Uhlig.resource: Uhlig's resource functions.
• Cslib.Circuits.Boolean.MassProduction.Uhlig.layerOverhead: the per-pair gate budget.

Main results

• Cslib.Circuits.Boolean.MassProduction.Uhlig.complexity_directProduct_two_mul_le: if every function on w inputs has t copies of size at most B, every function on p + w inputs has 2 t copies of size at most (2 ^ p + 1) * B + t * layerOverhead p w.

References

• D. Uhlig, Networks computing Boolean functions for multiple input values.
• I. Wegener, The Complexity of Boolean Functions, proof of Theorem 10.2.3.
• Simplifies MassProduction/UhligRoutingCircuit.lean, MassProduction/UhligDecoder.lean and MassProduction/UhligLayer.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.MassProduction.Uhlig.restriction {p w : ℕ} (f : BooleanFunction (p + w)) (z : BitString w) (a : ℕ) : Bool

The restriction of f to prefix number a, as a function of the suffix z. It is false when a numbers no prefix.

def Cslib.Circuits.Boolean.MassProduction.Uhlig.resource {p w : ℕ} (f : BooleanFunction (p + w)) (j : ℕ) : BooleanFunction w

Resource j of Uhlig's construction: position j of the code of the restrictions.

@[simp]

theorem Cslib.Circuits.Boolean.MassProduction.Uhlig.restriction_two_pow {p w : ℕ} (f : BooleanFunction (p + w)) (z : BitString w) : restriction f z (2 ^ p) = false

theorem Cslib.Circuits.Boolean.MassProduction.Uhlig.restriction_equivFin {p w : ℕ} (f : BooleanFunction (p + w)) (x : BitString (p + w)) : restriction f (x ∘ Fin.natAdd p) ↑((BitString.equivFin p) (x ∘ Fin.castAdd w)) = f x

Restricting to the number of the actual prefix evaluates f.

def Cslib.Circuits.Boolean.MassProduction.Uhlig.rank {p w k : ℕ} (x : BitString (k * (p + w))) (c : Fin k) : ℕ

The number of the prefix of copy c.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.MassProduction.Uhlig.pairCopy {t : ℕ} (s : Fin 2) (i : Fin t) : Fin (2 * t)

Copy s of pair i: pair i consists of copies i and t + i.

def Cslib.Circuits.Boolean.MassProduction.Uhlig.pairWires {p w t : ℕ} (i : Fin t) : Fin (p + p) → Fin (2 * t * (p + w))

The prefix wires of both copies of pair i.

def Cslib.Circuits.Boolean.MassProduction.Uhlig.pairSelect {p : ℕ} (s : Fin 2) (j : ℕ) (q : BitString (p + p)) : Bool

Whether copy s of a pair uses code position j, read from the pair's two prefixes.

theorem Cslib.Circuits.Boolean.MassProduction.Uhlig.pairSelect_comp_pairWires {p w t : ℕ} (s : Fin 2) (j : ℕ) (i : Fin t) (x : BitString (2 * t * (p + w))) : pairSelect s j (x ∘ pairWires i) = ![BitString.Uhlig.first, BitString.Uhlig.second] s (rank x (pairCopy 0 i)) (rank x (pairCopy 1 i)) j

def Cslib.Circuits.Boolean.MassProduction.Uhlig.routedBit {p w t : ℕ} (j : ℕ) (i : Fin t) (k : Fin w) (x : BitString (2 * t * (p + w))) : Bool

The suffix bit k routed to resource j from pair i.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.MassProduction.Uhlig.selectorCost (p : ℕ) : ℕ

The gate budget of one disjunctive normal form over the two prefixes of a pair.

def Cslib.Circuits.Boolean.MassProduction.Uhlig.layerOverhead (p w : ℕ) : ℕ

The gates spent on each pair, besides the resource circuits.

def Cslib.Circuits.Boolean.MassProduction.Uhlig.decoded {p w t : ℕ} (s : Fin 2) (i : Fin t) (y : BitString (2 * t * (p + w) + (2 ^ p + 1) * t)) : Bool

The decoded output of copy s of pair i, reading the bank outputs after the inputs.

theorem Cslib.Circuits.Boolean.MassProduction.Uhlig.decoded_eq {p w t : ℕ} (f : BooleanFunction (p + w)) (s : Fin 2) (i : Fin t) (x : BitString (2 * t * (p + w))) (y : BitString (2 * t * (p + w) + (2 ^ p + 1) * t)) (hx : y ∘ Fin.castAdd ((2 ^ p + 1) * t) = x) (hy : ∀ (j : Fin (2 ^ p + 1)), y (Fin.natAdd (2 * t * (p + w)) (finProdFinEquiv (j, i))) = resource f (↑j) (if BitString.Uhlig.first (rank x (pairCopy 0 i)) (rank x (pairCopy 1 i)) ↑j = true then directProductInput x (pairCopy 0 i) ∘ Fin.natAdd p else directProductInput x (pairCopy 1 i) ∘ Fin.natAdd p)) : decoded s i y = f (directProductInput x (pairCopy s i))

If the decoder reads the inputs and, for every resource, its value on the routed suffixes of pair i, then copy s of pair i decodes to f on that copy's input.

theorem Cslib.Circuits.Boolean.MassProduction.Uhlig.complexity_directProduct_two_mul_le {p w t B : ℕ} (hB : ∀ (g : BooleanFunction w), complexity interpretation (directProduct g t) ≤ B) (f : BooleanFunction (p + w)) : complexity interpretation (directProduct f (2 * t)) ≤ (2 ^ p + 1) * B + t * layerOverhead p w

One layer of Uhlig's construction. If every function on w inputs has t independent copies of size at most B, then every function on p + w inputs has 2 t independent copies of size at most (2 ^ p + 1) * B + t * layerOverhead p w.