Correctness of the machine-facing circuit codec

This internal module proves that the proof-free encoding and iterative evaluator in Encoding.Defs faithfully enforce their advertised syntactic invariants. Semantic agreement with typed circuit evaluation is deliberately kept in a separate proof layer.

@[simp]

theorem Complexity.CircuitCode.NatCode.length_encode (n : ℕ) : (encode n).length = n + 1

The unary encoding of n uses exactly n + 1 bits (n trues and a false).

@[simp]

theorem Complexity.CircuitCode.NatCode.decodePrefix?_encode_append (n : ℕ) (suffix : List Bool) : decodePrefix? (encode n ++ suffix) = some (n, suffix)

A unary field can be decoded in front of an arbitrary suffix.

theorem Complexity.CircuitCode.NatCode.decodePrefix?_eq_some_iff (bits : List Bool) (n : ℕ) (suffix : List Bool) : decodePrefix? bits = some (n, suffix) ↔ bits = encode n ++ suffix

Successful unary prefix decoding reconstructs the consumed input exactly.

@[simp]

theorem Complexity.CircuitCode.RawGate.isWellFormedAt_eq_true (gate : RawGate) (available : ℕ) : gate.isWellFormedAt available = true ↔ gate.WellFormedAt available

The Boolean well-formedness check agrees with the WellFormedAt predicate.

@[simp]

theorem Complexity.CircuitCode.RawGate.opOfBit_opBit (g : RawGate) : opOfBit g.opBit = g.op

Decoding a gate's operation bit recovers its operation.

@[simp]

theorem Complexity.CircuitCode.RawGate.length_encode (g : RawGate) : g.encode.length = 5 + g.input₀ + g.input₁

A gate encoding uses five header/delimiter bits plus one bit per unary input reference.

@[simp]

theorem Complexity.CircuitCode.RawGate.decodePrefix?_encode_append (g : RawGate) (suffix : List Bool) : decodePrefix? (g.encode ++ suffix) = some (g, suffix)

A gate can be decoded in front of an arbitrary suffix.

theorem Complexity.CircuitCode.RawGate.decodePrefix?_eq_some_iff (bits : List Bool) (gate : RawGate) (suffix : List Bool) : decodePrefix? bits = some (gate, suffix) ↔ bits = gate.encode ++ suffix

Successful gate-prefix decoding reconstructs the consumed input exactly.

@[simp]

theorem Complexity.CircuitCode.RawCircuit.isWellFormed_eq_true (circuit : RawCircuit) (N : ℕ) : isWellFormed N circuit = true ↔ WellFormed N circuit

The Boolean well-formedness check agrees with the WellFormed predicate.

@[simp]

theorem Complexity.CircuitCode.RawCircuit.decodeGates?_flatMap_encode_append (c : RawCircuit) (suffix : List Bool) : decodeGates? (List.length c) (List.flatMap RawGate.encode c ++ suffix) = some (c, suffix)

Parsing an encoded gate list consumes exactly that list and leaves the caller-supplied suffix untouched.

@[simp]

theorem Complexity.CircuitCode.RawCircuit.decodePrefix?_encode_append (c : RawCircuit) (suffix : List Bool) : decodePrefix? (c.encode ++ suffix) = some (c, suffix)

A circuit prefix can be decoded in front of an arbitrary suffix.

@[simp]

theorem Complexity.CircuitCode.RawCircuit.decode?_encode (c : RawCircuit) : decode? c.encode = some c

Exact decoding is a left inverse of circuit serialization.

theorem Complexity.CircuitCode.RawCircuit.decode?_encode_append_eq_none (c : RawCircuit) {suffix : List Bool} (h : suffix ≠ []) : decode? (c.encode ++ suffix) = none

Exact decoding rejects any nonempty suffix after a canonical encoding.

@[simp]

theorem Complexity.CircuitCode.RawCircuit.length_encode (c : RawCircuit) : c.encode.length = List.length c + 1 + (List.map (fun (gate : RawGate) => gate.encode.length) c).sum

A circuit encoding consists of the unary gate count followed by the concatenated gate encodings.

theorem Complexity.CircuitCode.RawCircuit.topologicallyWellFormed_cons (N : ℕ) (gate : RawGate) (gates : RawCircuit) : TopologicallyWellFormed N (gate :: gates) ↔ gate.WellFormedAt N ∧ TopologicallyWellFormed (N + 1) gates

Topological well-formedness of a nonempty gate list splits at its head.

theorem Complexity.CircuitCode.RawCircuit.decodeGates?_eq_some_iff (count : ℕ) (bits : List Bool) (circuit : RawCircuit) (suffix : List Bool) : decodeGates? count bits = some (circuit, suffix) ↔ List.length circuit = count ∧ bits = List.flatMap RawGate.encode circuit ++ suffix

Successful fixed-count gate decoding reconstructs the consumed input.

theorem Complexity.CircuitCode.RawCircuit.decodePrefix?_eq_some_iff (bits : List Bool) (circuit : RawCircuit) (suffix : List Bool) : decodePrefix? bits = some (circuit, suffix) ↔ bits = circuit.encode ++ suffix

Successful circuit-prefix decoding reconstructs its canonical encoding.

theorem Complexity.CircuitCode.RawCircuit.decode?_eq_some_iff_internal (bits : List Bool) (circuit : RawCircuit) : decode? bits = some circuit ↔ bits = circuit.encode

Exact decoding succeeds precisely on canonical encodings.

theorem Complexity.CircuitCode.RawCircuit.evalAux?_isSome_iff (circuit : RawCircuit) (wires : Array Bool) : (circuit.evalAux? wires).isSome = true ↔ TopologicallyWellFormed wires.size circuit

Running the iterative evaluator succeeds exactly for topological gate lists.

theorem Complexity.CircuitCode.RawCircuit.evalAux?_size {circuit : RawCircuit} {wires result : Array Bool} (h : circuit.evalAux? wires = some result) : result.size = wires.size + List.length circuit

Successful iterative evaluation appends exactly one wire per gate.

theorem Complexity.CircuitCode.RawCircuit.eval?_isSome_iff_internal (circuit : RawCircuit) (input : List Bool) : (circuit.eval? input).isSome = true ↔ WellFormed input.length circuit

Raw evaluation succeeds precisely for nonempty topologically ordered circuits.

theorem Complexity.CircuitCode.evalCode_isSome_iff (N : ℕ) (code input : List Bool) : (evalCode N code input).isSome = true ↔ input.length = N ∧ ∃ (circuit : RawCircuit), code = circuit.encode ∧ RawCircuit.WellFormed N circuit

Code evaluation succeeds exactly when the input length is the declared arity, the code is canonical, and the decoded raw circuit is well formed.

@[simp]

theorem Complexity.CircuitCode.RawGate.ofGate_input₀ {W : ℕ} (gate : Gate Basis.andOr2 W) : (ofGate gate).input₀ = ↑(gate.inputs ⟨0, ⋯⟩)

The first raw reference is the first typed input wire.

@[simp]

theorem Complexity.CircuitCode.RawGate.ofGate_input₁ {W : ℕ} (gate : Gate Basis.andOr2 W) : (ofGate gate).input₁ = ↑(gate.inputs ⟨1, ⋯⟩)

The second raw reference is the second typed input wire.

theorem Complexity.CircuitCode.RawGate.ofGate_wellFormedAt {W : ℕ} (gate : Gate Basis.andOr2 W) : (ofGate gate).WellFormedAt W

Erasing a typed gate's proofs never introduces an out-of-range reference.

@[simp]

theorem Complexity.CircuitCode.RawCircuit.length_ofCircuit {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : List.length (ofCircuit c) = G + 1

Translating a typed single-output circuit produces one raw gate per internal gate, followed by its output gate.

theorem Complexity.CircuitCode.RawCircuit.ofCircuit_topologicallyWellFormed {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : TopologicallyWellFormed N (ofCircuit c)

Translation preserves the typed circuit's topological ordering.

theorem Complexity.CircuitCode.RawCircuit.ofCircuit_wellFormed {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : WellFormed N (ofCircuit c)

Translation of a typed circuit is a valid raw single-output circuit.

theorem Complexity.CircuitCode.RawCircuit.encode_length_le (N G : ℕ) (circuit : RawCircuit) (hlen : List.length circuit = G) (hwell : TopologicallyWellFormed N circuit) : circuit.encode.length ≤ G + 1 + G * (2 * (N + G) + 5)

A generic topological raw circuit with G gates and input arity N has quadratic-size unary encoding.

theorem Complexity.CircuitCode.evalCode_encodeCircuit_isSome_iff {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (input : List Bool) : (evalCode N (encodeCircuit c) input).isSome = true ↔ input.length = N

A code produced from a typed circuit is evaluable exactly on inputs of the circuit's declared arity.

theorem Complexity.CircuitCode.encodeCircuit_length_le {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : (encodeCircuit c).length ≤ G + 1 + 1 + (G + 1) * (2 * (N + (G + 1)) + 5)

The unary encoding of a typed G-internal-gate circuit has a concrete quadratic length bound.

theorem Complexity.CircuitCode.encodeCircuit_length_le_size_internal {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : (encodeCircuit c).length ≤ 1 + c.size * (2 * (N + c.size) + 6)

In the library's size convention, which counts internal and output gates but not primary inputs or free negations, unary circuit codes have quadratic length in the input arity and circuit size.