Inputs for uniform circuit-family evaluation

The verified serialized evaluator consumes a pair of a tagged circuit code and the circuit input. A uniformity generator consumes unary length instead. This module names the pure preprocessing map connecting those interfaces.

def Complexity.generatorEvalInput (gen : List Bool → List Bool) (x : List Bool) : List Bool

On input x, run the prospective uniformity generator on 1^|x| and pair the resulting circuit code with the unchanged input.

Equations

• Complexity.generatorEvalInput gen x = Complexity.pair (gen (List.replicate x.length true)) x