Serialized evaluation circuits from polynomial circuit oracles -- definitions

A polynomial circuit oracle for the verified serialized evaluator can be specialized to fixed family-code and argument widths. A zero-internal-gate front end pairs the two input blocks, and ordinary circuit composition feeds that canonical query to the matching oracle-family member.

def Complexity.CircuitCode.EvaluationOracleCircuit.packedWidth (codeWidth inputWidth : ℕ) : ℕ

Input width of a fixed-layout family-code and argument pair.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.packedWidth codeWidth inputWidth = codeWidth + inputWidth

instance Complexity.CircuitCode.EvaluationOracleCircuit.instNeZeroNatPackedWidth (codeWidth inputWidth : ℕ) [NeZero codeWidth] : NeZero (packedWidth codeWidth inputWidth)

def Complexity.CircuitCode.EvaluationOracleCircuit.queryWidth (codeWidth inputWidth : ℕ) : ℕ

Serialized query width after applying the canonical pairing codec.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.queryWidth codeWidth inputWidth = Complexity.Circuit.pairSourceWidth codeWidth inputWidth

instance Complexity.CircuitCode.EvaluationOracleCircuit.instNeZeroNatQueryWidth (codeWidth inputWidth : ℕ) : NeZero (queryWidth codeWidth inputWidth)

def Complexity.CircuitCode.EvaluationOracleCircuit.codeSource (codeWidth inputWidth : ℕ) (coordinate : Fin codeWidth) : Circuit.InputSource (packedWidth codeWidth inputWidth)

Source of one family-code bit in the packed ordinary input.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.codeSource codeWidth inputWidth coordinate = Complexity.Circuit.InputSource.input (Fin.castAdd inputWidth coordinate)

def Complexity.CircuitCode.EvaluationOracleCircuit.inputSource (codeWidth inputWidth : ℕ) (coordinate : Fin inputWidth) : Circuit.InputSource (packedWidth codeWidth inputWidth)

Source of one argument bit in the packed ordinary input.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.inputSource codeWidth inputWidth coordinate = Complexity.Circuit.InputSource.input (Fin.natAdd codeWidth coordinate)

def Complexity.CircuitCode.EvaluationOracleCircuit.queryCircuit (codeWidth inputWidth : ℕ) [NeZero codeWidth] : Circuit Basis.andOr2 (packedWidth codeWidth inputWidth) (queryWidth codeWidth inputWidth) 0

Canonical paired evaluator query produced from the two packed blocks.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.EvaluationOracleCircuit.packedInput {codeWidth inputWidth : ℕ} (code : BitString codeWidth) (input : BitString inputWidth) : BitString (packedWidth codeWidth inputWidth)

Pack a fixed-width family code before its fixed-width argument.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.packedInput code input = Fin.append code input

def Complexity.CircuitCode.EvaluationOracleCircuit.compile (oracle : PolynomialCircuitOracle circuitEvalLanguage) (codeWidth inputWidth : ℕ) [NeZero codeWidth] : (internalGates : ℕ) × Circuit Basis.andOr2 (packedWidth codeWidth inputWidth) 1 internalGates

Compose the fixed-layout query front end with the evaluator-oracle member at the resulting serialized query width.

Equations

• One or more equations did not get rendered due to their size.