Serialized output-match evaluator queries

This module exposes a source circuit that turns a live raw-gate stream, evaluator argument, and expected output bit into a tagged circuit-family code. Composing it with the verified evaluator oracle accepts exactly when the raw circuit represented by that stream returns the expected bit.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.eval_codeSources {bodyWidth inputWidth : ℕ} (gateCount : ℕ) (body : BitString bodyWidth) (input : BitString inputWidth) (expected : Bool) : (BitString.toList fun (coordinate : Fin (codeWidth gateCount bodyWidth inputWidth)) => (codeSources gateCount bodyWidth inputWidth coordinate).eval (sourceInput body input expected)) = familyCode gateCount inputWidth body.toList expected

Code sources serialize exactly the tagged two-gate output-match extension.

@[simp]

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.toList_codeValue {bodyWidth inputWidth : ℕ} (gateCount : ℕ) (body : BitString bodyWidth) (input : BitString inputWidth) (expected : Bool) : (codeValue gateCount body input expected).toList = familyCode gateCount inputWidth body.toList expected

The semantic code value has the exact emitted tagged family code.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.eval_queryCircuit {bodyWidth inputWidth : ℕ} (gateCount : ℕ) (body : BitString bodyWidth) (input : BitString inputWidth) (expected : Bool) : (queryCircuit gateCount bodyWidth inputWidth).eval (sourceInput body input expected) = packedInput (codeValue gateCount body input expected) input

The source front end emits the output-match family code followed by its evaluator argument.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.eval_compile (oracle : PolynomialCircuitOracle circuitEvalLanguage) {bodyWidth inputWidth : ℕ} (gateCount : ℕ) (body : BitString bodyWidth) (input : BitString inputWidth) (expected : Bool) : (compile oracle gateCount bodyWidth inputWidth).snd.eval (sourceInput body input expected) 0 = decide (evalFamilyCode (familyCode gateCount inputWidth body.toList expected) input.toList = some true)

The compiled evaluator branch accepts exactly successful true evaluation of its tagged output-match code.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.codeWidth_eq (gateCount bodyWidth inputWidth : ℕ) : codeWidth gateCount bodyWidth inputWidth = 1 + (gateCount + 3) + bodyWidth + (5 + 2 * (inputWidth + gateCount - 1)) + (5 + 2 * (inputWidth + gateCount))

Exact width of the tagged family code produced by a gate-stream branch.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.size_queryCircuit (gateCount bodyWidth inputWidth : ℕ) : (queryCircuit gateCount bodyWidth inputWidth).size = packedWidth (codeWidth gateCount bodyWidth inputWidth) inputWidth

The source front end pays one output gate per packed evaluator input bit.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.size_compile (oracle : PolynomialCircuitOracle circuitEvalLanguage) (gateCount bodyWidth inputWidth : ℕ) : (compile oracle gateCount bodyWidth inputWidth).snd.size = packedWidth (codeWidth gateCount bodyWidth inputWidth) inputWidth + queryWidth (codeWidth gateCount bodyWidth inputWidth) inputWidth + oracle.family.size (queryWidth (codeWidth gateCount bodyWidth inputWidth) inputWidth)

Exact cost of source materialization, evaluator pairing, and the selected oracle-family member.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.familyCode_eq_appendOutputMatchBit (gateCount inputWidth : ℕ) (circuit : RawCircuit) (expected : Bool) (hlength : List.length circuit = gateCount) : familyCode gateCount inputWidth (List.flatMap RawGate.encode circuit) expected = true :: (RawCircuit.appendOutputMatchBit inputWidth circuit expected).encode

A canonical gate stream produces exactly the tagged encoding of its two-gate live-bit output-match extension.

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.eval_compile_gateStream (oracle : PolynomialCircuitOracle circuitEvalLanguage) {gateCount bodyWidth inputWidth : ℕ} [NeZero inputWidth] (body : BitString bodyWidth) (input : BitString inputWidth) (expected : Bool) (circuit : RawCircuit) (hbody : body.toList = List.flatMap RawGate.encode circuit) (hlength : List.length circuit = gateCount) (hnonempty : circuit ≠ []) : (compile oracle gateCount bodyWidth inputWidth).snd.eval (sourceInput body input expected) 0 = decide (circuit.eval? input.toList = some expected)

On a canonical nonempty gate stream, the compiled branch accepts exactly when the represented raw circuit returns the live expected bit.