Serialized output-match evaluator queries -- proof internals

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.eval_codeSources_internal {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

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

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.eval_queryCircuit_internal {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

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.eval_compile_internal (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)

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

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

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.size_compile_internal (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)

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.familyCode_eq_appendOutputMatchBit_internal (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

theorem Complexity.CircuitCode.EvaluationOracleCircuit.OutputMatchBranch.eval_compile_gateStream_internal (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)