JSON circuit schema

The top-level object has input_bits equal to 8, a nodes array and an outputs array of eight integer wire indices.

Input wires are numbered 0 through 7, least-significant bit first. Entry i of nodes creates wire 8+i. A node is {"op":"xor","args":[a,b]}, {"op":"and","args":[a,b]} or {"op":"not","args":[a]}. Every operand index is a nonnegative integer strictly smaller than 8+i. Output indices are nonnegative integers smaller than 8+len(nodes); outputs[0] is the least-significant output bit.

Each nodes entry counts as one gate, including an unused gate. Each entry whose op is and counts as one AND gate. XOR and AND have exactly two inputs; NOT has exactly one. Reusing an earlier wire does not add a gate. Duplicating a gate adds another gate. No other node operation, implicit constant, integer computation or embedded subcircuit is permitted.

The target table contains outputs[x] for each integer x from 0 to 255. Exact equality is required at every input. Gate identifiers or circuit bytes do not need to match the reference.

Lean interface

Import the unchanged CircuitSpec module. In namespace Solution define circuit : List Circuit.Gate and outputWires : List Nat. A JSON NOT gate maps to Op.not with its sole operand in left; right is ignored by the fixed semantics and may be any natural number. XOR and AND preserve their operand order. Provide:

correct : forall x : Fin 256, Circuit.evaluate circuit outputWires x.val = Circuit.truthTable[x.val]!
and_budget : Circuit.andCount circuit <= 64
gate_budget : circuit.length <= 400
well_formed : Circuit.valid circuit outputWires = true

These declarations must have the stated types with the fixed imported semantics and truth table. Equivalent proof terms are accepted. Helper lemmas and verified traces are allowed; unchecked traces are not proofs. Export the final proof as Solution.lean, with any local helper modules alongside it.
