Internal: semantics of encoded fan-in-two circuits

This file proves that the iterative, machine-facing evaluator in Circuits.Encoding.Defs implements the existing mathematical circuit semantics. The central argument is a memo invariant: after the first k ordered gates have run, the evaluator's array contains exactly the values of descriptor wires 0, ..., N + k - 1.

theorem Complexity.CircuitCode.RawCircuit.eval?_ofCircuit {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (input : BitString N) : (ofCircuit c).eval? input.toList = some (c.eval input 0)

Raw evaluation of a serialized typed circuit agrees with the typed circuit's Boolean semantics.

theorem Complexity.CircuitCode.evalCode_encodeCircuit_internal {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (input : BitString N) : evalCode N (encodeCircuit c) input.toList = some (c.eval input 0)

Decoding and iteratively evaluating the canonical encoding of a typed fan-in-two circuit returns its typed output.

theorem Complexity.CircuitCode.evalCode_encodeCircuit_of_length_internal {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (input : List Bool) (hinput : input.length = N) : evalCode N (encodeCircuit c) input = some (c.eval (BitString.ofList input hinput) 0)

List-native form of evalCode_encodeCircuit for machine-facing clients.