Raw parity-circuit fragments -- proof internals

theorem Complexity.CircuitCode.Parity.foldXor_eq_sum_internal (count : ℕ) (bits : Fin count → Bool) : foldXor count bits = ∑ i : Fin count, bits i

theorem Complexity.CircuitCode.Parity.length_xorGates_internal (available step input : ℕ) : List.length (xorGates available step input) = 3

theorem Complexity.CircuitCode.Parity.length_steps_internal (available step inputCount : ℕ) (refs : Fin inputCount → ℕ) : List.length (steps available step inputCount refs) = 3 * inputCount

theorem Complexity.CircuitCode.Parity.length_compileRaw_internal (available : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) : List.length (compileRaw available refs) = 1 + 3 * inputCount

theorem Complexity.CircuitCode.Parity.outputWire_eq_internal (available : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) : outputWire available inputCount = available + List.length (compileRaw available refs) - 1

theorem Complexity.CircuitCode.Parity.evalAux?_compileRaw_internal (available : ℕ) [NeZero available] {inputCount : ℕ} (refs : Fin inputCount → ℕ) (bits : Fin inputCount → Bool) (wires : Array Bool) (hsize : wires.size = available) (hrefs : ∀ (i : Fin inputCount), refs i < available) (hinputs : ∀ (i : Fin inputCount), wires[refs i]? = some (bits i)) : ∃ (result : Array Bool), (compileRaw available refs).evalAux? wires = some result ∧ result.size = wires.size + (1 + 3 * inputCount) ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[outputWire available inputCount]? = some (foldXor inputCount bits)

theorem Complexity.CircuitCode.Parity.topologicallyWellFormed_compileRaw_internal (available : ℕ) [NeZero available] {inputCount : ℕ} (refs : Fin inputCount → ℕ) (hrefs : ∀ (i : Fin inputCount), refs i < available) : RawCircuit.TopologicallyWellFormed available (compileRaw available refs)

theorem Complexity.CircuitCode.Parity.compileRaw_wellFormed_internal (available : ℕ) [NeZero available] {inputCount : ℕ} (refs : Fin inputCount → ℕ) (hrefs : ∀ (i : Fin inputCount), refs i < available) : RawCircuit.WellFormed available (compileRaw available refs)

theorem Complexity.CircuitCode.Parity.eval?_compileRaw_internal (available : ℕ) [NeZero available] {inputCount : ℕ} (refs : Fin inputCount → ℕ) (hrefs : ∀ (i : Fin inputCount), refs i < available) (input : BitString available) : (compileRaw available refs).eval? input.toList = some (foldXor inputCount fun (i : Fin inputCount) => input ⟨refs i, ⋯⟩)