Fixed-width evaluator output selection -- proof internals

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.stepOutputWire_lt_fullAvailable_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) : EvaluationLayout.stepOutputWire inputWidth gateBound slot < fullAvailable inputWidth gateBound

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.size_formula_internal (inputWidth gateBound : ℕ) : (formula inputWidth gateBound).size = selectorSize gateBound

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.vars_formula_lt_internal (inputWidth gateBound wire : ℕ) : wire ∈ (formula inputWidth gateBound).vars → wire < fullAvailable inputWidth gateBound

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.eval_formula_of_code_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (hpositive : description.Positive) (assignment : ℕ → Bool) (hcode : ∀ (coordinate : Fin (codeWidth inputWidth gateBound)), assignment ↑coordinate = description.encode coordinate) : BoolFormula.eval assignment (formula inputWidth gateBound) = assignment (EvaluationLayout.stepOutputWire inputWidth gateBound (lastActiveSlot description hpositive))

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.some_eval_formula_prefixResult_internal {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) (input : BitString inputWidth) (result : EvaluationSequence.PrefixResult description input gateBound ⋯) : some (BoolFormula.eval (memoAssignment result.circuitWires) (formula inputWidth gateBound)) = result.rawWires[inputWidth + ↑(lastActiveSlot description ⋯)]?

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.some_eval_formula_eq_eval?_internal {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) (input : BitString inputWidth) (result : EvaluationSequence.PrefixResult description input gateBound ⋯) : some (BoolFormula.eval (memoAssignment result.circuitWires) (formula inputWidth gateBound)) = description.toRawCircuit.eval? input.toList

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.length_compileRaw_internal (inputWidth gateBound : ℕ) : List.length (compileRaw inputWidth gateBound) = selectorSize gateBound

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.topologicallyWellFormed_compileRaw_internal (inputWidth gateBound : ℕ) : RawCircuit.TopologicallyWellFormed (fullAvailable inputWidth gateBound) (compileRaw inputWidth gateBound)

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.length_circuit_internal (inputWidth gateBound : ℕ) : List.length (circuit inputWidth gateBound) = EvaluationLayout.prefixSize inputWidth gateBound gateBound + selectorSize gateBound

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.outputWire_eq_internal (inputWidth gateBound : ℕ) : outputWire inputWidth gateBound = EvaluationLayout.baseWireCount inputWidth gateBound + List.length (circuit inputWidth gateBound) - 1

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.topologicallyWellFormed_circuit_internal (inputWidth gateBound : ℕ) : RawCircuit.TopologicallyWellFormed (EvaluationLayout.baseWireCount inputWidth gateBound) (circuit inputWidth gateBound)

noncomputable def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.resultInternal {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) (input : BitString inputWidth) : Result description input

Construct the complete fixed-width evaluation witness.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.resultInternal hdescription input = { wires := Classical.choose ⋯, circuitEval := ⋯, size := ⋯, output := ⋯ }

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.circuit_ne_nil_internal (inputWidth gateBound : ℕ) : circuit inputWidth gateBound ≠ []

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.eval?_circuit_internal {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) (input : BitString inputWidth) : (circuit inputWidth gateBound).eval? (EvaluationSequence.combinedInput description input).toList = description.toRawCircuit.eval? input.toList