Serialized evaluation circuits from polynomial circuit oracles

The fixed-layout compiler below decides successful true evaluation of an arbitrary tagged family code. Malformed codes and successful false evaluations both return false, exactly as in circuitEvalLanguage.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.eval_queryCircuit {codeWidth inputWidth : ℕ} [NeZero codeWidth] (code : BitString codeWidth) (input : BitString inputWidth) : ((queryCircuit codeWidth inputWidth).eval (packedInput code input)).toList = pair code.toList input.toList

The query front end serializes exactly the family-code and argument blocks supplied in the packed ordinary input.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.eval_compile (oracle : PolynomialCircuitOracle circuitEvalLanguage) {codeWidth inputWidth : ℕ} [NeZero codeWidth] (code : BitString codeWidth) (input : BitString inputWidth) : (compile oracle codeWidth inputWidth).snd.eval (packedInput code input) 0 = decide (evalFamilyCode code.toList input.toList = some true)

The compiled evaluator circuit accepts exactly successful true evaluation of the supplied tagged family code.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.size_compile (oracle : PolynomialCircuitOracle circuitEvalLanguage) (codeWidth inputWidth : ℕ) [NeZero codeWidth] : (compile oracle codeWidth inputWidth).snd.size = queryWidth codeWidth inputWidth + oracle.family.size (queryWidth codeWidth inputWidth)

Exact cost of the fixed pairing front end and selected evaluator-oracle family member.