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.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.