Fixed-width evaluator output selection

The compiled selector is scoped to the completed gate-sequence memo. On an encoded positive description it returns exactly the last active gate value, which the sequence invariant identifies with the corresponding direct raw-gate memo entry.

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

Every bounded gate result is available before output selection begins.

@[simp]

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

Exact size of the last-active-gate selector formula.

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

The selector only names the description prefix and completed gate outputs.

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.eval_formula_of_code {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))

The encoded positive gate count selects exactly the last active slot.

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.some_eval_formula_prefixResult {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 ⋯)]?

On a complete lockstep evaluation, selector semantics is the direct padded memo value at the last active slot.

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.some_eval_formula_eq_eval? {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

On a valid description, selector semantics is exactly ordinary raw-circuit evaluation on the sample input.

@[simp]

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

Selector compilation emits exactly its advertised formula size.

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

The selector fragment only references wires available after the complete gate sequence.

@[simp]

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

The complete evaluator emits the gate-sequence prefix and one selector formula.

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

The complete evaluator's designated output is its final emitted wire.

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

The complete evaluator is topologically valid from its description-and- sample input block.

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

A valid fixed-width description's complete evaluator runs successfully and returns its direct raw-circuit value.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.result hdescription input = Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.resultInternal hdescription input

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

The complete evaluator is nonempty because its selector emits at least one gate.

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.eval?_circuit {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

Complete fixed-width evaluation agrees exactly with ordinary raw-circuit evaluation on a valid encoded description and sample.