Appendable raw-circuit fragments

Primitive copy/constant gates and generic composition laws for building a CircuitCode.RawCircuit in successive topologically ordered fragments. Evaluation passes the memo array from one fragment to the next, and successful evaluation preserves every previously available wire.

@[simp]

theorem Complexity.CircuitCode.RawGate.eval_copy (input : ℕ) (negated value : Bool) : (copy input negated).eval value value = (negated ^^ value)

A duplicated-input copy gate returns its input, optionally negated.

@[simp]

theorem Complexity.CircuitCode.RawGate.eval_constant (input : ℕ) (constantValue wireValue : Bool) : (constant input constantValue).eval wireValue wireValue = constantValue

A dual-input constant gate ignores the value of its witness wire.

theorem Complexity.CircuitCode.RawCircuit.evalAux?_append (first second : RawCircuit) (wires : Array Bool) : (first ++ second).evalAux? wires = (first.evalAux? wires).bind second.evalAux?

Evaluating appended raw fragments is sequential evaluation with the first fragment's memo array passed to the second.

theorem Complexity.CircuitCode.RawCircuit.eval?_append_copy (circuit : RawCircuit) (input : List Bool) (negated : Bool) (hnonempty : circuit ≠ []) : (circuit ++ [RawGate.copy (input.length + List.length circuit - 1) negated]).eval? input = Option.map (fun (value : Bool) => negated ^^ value) (circuit.eval? input)

Appending a copy gate to a nonempty circuit maps its original output by the gate's optional negation.

theorem Complexity.CircuitCode.RawCircuit.encode_appendOutputMatch (inputWidth : ℕ) (circuit : RawCircuit) (expected : Bool) : (appendOutputMatch inputWidth circuit expected).encode = NatCode.encode (List.length circuit + 1) ++ List.flatMap RawGate.encode circuit ++ (RawGate.copy (inputWidth + List.length circuit - 1) !expected).encode

Output-match extension serialization consists of the incremented gate count, the original gate stream, and one final copy gate.

theorem Complexity.CircuitCode.RawCircuit.eval?_appendOutputMatch_eq_some_true_iff (circuit : RawCircuit) (input : List Bool) (expected : Bool) (hnonempty : circuit ≠ []) : (appendOutputMatch input.length circuit expected).eval? input = some true ↔ circuit.eval? input = some expected

An output-match extension returns true exactly when the original nonempty circuit returns the selected bit.

theorem Complexity.CircuitCode.RawCircuit.evalCode_appendOutputMatch_encode_iff_of_length (inputWidth : ℕ) (circuit : RawCircuit) (input : List Bool) (expected : Bool) (hnonempty : circuit ≠ []) (hwidth : input.length = inputWidth) : evalCode inputWidth (appendOutputMatch inputWidth circuit expected).encode input = some true ↔ circuit.eval? input = some expected

Exact decoding turns an output-match extension into a true-evaluation test at the declared input width.

theorem Complexity.CircuitCode.RawCircuit.encode_appendOutputMatchBit (inputWidth : ℕ) (circuit : RawCircuit) (expected : Bool) : (appendOutputMatchBit inputWidth circuit expected).encode = NatCode.encode (List.length circuit + 2) ++ List.flatMap RawGate.encode circuit ++ (RawGate.copy (inputWidth + List.length circuit - 1) expected).encode ++ (RawGate.copy (inputWidth + List.length circuit) true).encode

Live-bit output-match extension serialization consists of the incremented gate count, the original gate stream, and two final copy gates. The live expected bit occurs positively in the first new gate.

theorem Complexity.CircuitCode.RawCircuit.eval?_appendOutputMatchBit_eq_some_true_iff (circuit : RawCircuit) (input : List Bool) (expected : Bool) (hnonempty : circuit ≠ []) : (appendOutputMatchBit input.length circuit expected).eval? input = some true ↔ circuit.eval? input = some expected

A live-bit output-match extension returns true exactly when the original nonempty circuit returns the selected bit.

theorem Complexity.CircuitCode.RawCircuit.evalCode_appendOutputMatchBit_encode_iff_of_length (inputWidth : ℕ) (circuit : RawCircuit) (input : List Bool) (expected : Bool) (hnonempty : circuit ≠ []) (hwidth : input.length = inputWidth) : evalCode inputWidth (appendOutputMatchBit inputWidth circuit expected).encode input = some true ↔ circuit.eval? input = some expected

Exact decoding turns a live-bit output-match extension into a true-evaluation test at the declared input width.

theorem Complexity.CircuitCode.RawCircuit.topologicallyWellFormed_append (available : ℕ) (first second : RawCircuit) : TopologicallyWellFormed available (first ++ second) ↔ TopologicallyWellFormed available first ∧ TopologicallyWellFormed (available + List.length first) second

Appended fragments are topological exactly when each fragment is topological at its corresponding initial wire count.

theorem Complexity.CircuitCode.RawCircuit.evalAux?_preserves_prefix {circuit : RawCircuit} {wires result : Array Bool} (heval : circuit.evalAux? wires = some result) {i : ℕ} (hi : i < wires.size) : result[i]? = wires[i]?

Successful fragment evaluation does not change any pre-existing wire.