Serialized output-match evaluator queries -- definitions

A fixed gate count lets a live raw-gate stream be extended by the two-gate output-match fragment without computing on its code bits. The source circuit copies that stream, inserts the incremented count and fixed gate fields, and uses the live expected bit positively in both negation fields of the mismatch gate. The resulting tagged family code and its argument feed the verified serialized evaluator oracle.

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.sourceInputWidth (bodyWidth inputWidth : ℕ) : ℕ

Input width of a raw-gate body, evaluator argument, and expected bit.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.sourceInputWidth bodyWidth inputWidth = bodyWidth + (inputWidth + 1)

instance Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.instNeZeroNatSourceInputWidth (bodyWidth inputWidth : ℕ) : NeZero (sourceInputWidth bodyWidth inputWidth)

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.bodySource (bodyWidth inputWidth : ℕ) (coordinate : Fin bodyWidth) : Circuit.InputSource (sourceInputWidth bodyWidth inputWidth)

Source of one raw-gate-body bit.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.bodySource bodyWidth inputWidth coordinate = Complexity.Circuit.InputSource.input (Fin.castAdd (inputWidth + 1) coordinate)

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.argumentSource (bodyWidth inputWidth : ℕ) (coordinate : Fin inputWidth) : Circuit.InputSource (sourceInputWidth bodyWidth inputWidth)

Source of one evaluator-argument bit.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.argumentSource bodyWidth inputWidth coordinate = Complexity.Circuit.InputSource.input (Fin.natAdd bodyWidth coordinate.castSucc)

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.expectedSource (bodyWidth inputWidth : ℕ) : Circuit.InputSource (sourceInputWidth bodyWidth inputWidth)

Source of the expected output bit after the evaluator argument.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.expectedSource bodyWidth inputWidth = Complexity.Circuit.InputSource.input (Fin.natAdd bodyWidth (Fin.last inputWidth))

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.sourceInput {bodyWidth inputWidth : ℕ} (body : BitString bodyWidth) (input : BitString inputWidth) (expected : Bool) : BitString (sourceInputWidth bodyWidth inputWidth)

Pack a raw-gate body, evaluator argument, and expected output bit.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.sourceInput body input expected = Fin.append body fun (i : Fin (inputWidth + 1)) => Fin.lastCases expected input i

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.constantSources {sourceWidth : ℕ} (bits : List Bool) : List (Circuit.InputSource sourceWidth)

Materialize fixed bits as constant circuit sources.

Equations

• Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.constantSources bits = List.map Complexity.Circuit.InputSource.constant bits

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.liveCopySources {sourceWidth : ℕ} (wire : ℕ) (negated : Circuit.InputSource sourceWidth) : List (Circuit.InputSource sourceWidth)

Source-level encoding of a copy gate with one live negation bit.

Equations

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

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.codeSourceList (gateCount bodyWidth inputWidth : ℕ) : List (Circuit.InputSource (sourceInputWidth bodyWidth inputWidth))

Source list spelling the tagged family code for a live-bit output match.

Equations

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

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.codeWidth (gateCount bodyWidth inputWidth : ℕ) : ℕ

Width of the tagged output-match family code.

Equations

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

instance Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.instNeZeroNatCodeWidth (gateCount bodyWidth inputWidth : ℕ) : NeZero (codeWidth gateCount bodyWidth inputWidth)

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.codeSources (gateCount bodyWidth inputWidth : ℕ) : Fin (codeWidth gateCount bodyWidth inputWidth) → Circuit.InputSource (sourceInputWidth bodyWidth inputWidth)

Fixed-width view of the output-match code source list.

Equations

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

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.querySources (gateCount bodyWidth inputWidth : ℕ) : Fin (packedWidth (codeWidth gateCount bodyWidth inputWidth) inputWidth) → Circuit.InputSource (sourceInputWidth bodyWidth inputWidth)

Output-match family-code sources followed by argument sources.

Equations

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

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.queryCircuit (gateCount bodyWidth inputWidth : ℕ) : Circuit Basis.andOr2 (sourceInputWidth bodyWidth inputWidth) (packedWidth (codeWidth gateCount bodyWidth inputWidth) inputWidth) 0

Source circuit producing the evaluator adapter's packed input.

Equations

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

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.compile (oracle : PolynomialCircuitOracle circuitEvalLanguage) (gateCount bodyWidth inputWidth : ℕ) : (internalGates : ℕ) × Circuit Basis.andOr2 (sourceInputWidth bodyWidth inputWidth) 1 internalGates

Compose the output-match query sources with the serialized evaluator oracle member selected by their exact width.

Equations

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

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.familyCode (gateCount inputWidth : ℕ) (body : List Bool) (expected : Bool) : List Bool

Semantic tagged family code emitted for a gate body and expected bit.

Equations

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

def Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.codeValue {bodyWidth inputWidth : ℕ} (gateCount : ℕ) (body : BitString bodyWidth) (input : BitString inputWidth) (expected : Bool) : BitString (codeWidth gateCount bodyWidth inputWidth)

Semantic family-code bit string produced by the code sources.

Equations

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