Implement and formally verify a compact Boolean substitution circuit

A hardware team has a fixed inverse eight-bit substitution function specified by all 256 entries in truth_table.json. Implement that exact function as a combinational Boolean circuit suitable for a backend where nonlinear gates are expensive. The function must not change. No decomposition or existing implementation is supplied.

Deliver circuit.json, Solution.lean and instructions for checking the proof with Lean 4.19.0. The circuit has eight Boolean inputs and eight Boolean outputs, both ordered least-significant bit first. It may use only two-input XOR, two-input AND and one-input NOT gates. It must contain no more than 64 AND gates and no more than 398 gates in total. Fanout and wiring are free. Every gate must read only input wires or earlier gate outputs. No lookup tables, multiplexers, conditional expressions, arithmetic primitives, opaque external calls or additional input-dependent state may be counted as free operations.

The JSON schema is specified in circuit_format.txt. Its wire-level semantics, the full target table and the Lean proof interface are fixed in CircuitSpec.lean. Prove that your circuit is well formed, satisfies both gate budgets and computes the specified output for every x : Fin 256. The Lean circuit must be the same circuit as circuit.json, in the same order; the evaluator will compare their data. Deliver a complete kernel-checked proof. Missing proofs, sorry, admitted assumptions, new axioms, unsafe evaluation shortcuts and native_decide are not accepted. Standard logical axioms supplied by Lean are allowed; the final declarations must not depend on sorryAx or Lean.ofReduceBool.

The target has at least one implementation within the declared budgets. You are not asked to establish that 64 AND gates is the global minimum. Any circuit meeting the exact specification and both budgets is a correct answer. There is no preferred architecture or required synthesis algorithm. The difficulty is discovering a sufficiently compact implementation and delivering its formal equivalence proof; a correct table lookup or an oversized truth-table expansion is not a solution.

Place all deliverables in output/. Include any source needed to build the proof, but do not modify CircuitSpec.lean or replace the target function. If you use external synthesis tools, identify their versions in output/tool_versions.txt. The final circuit and proof must be self-contained.

The supplied forward_table.json specifies the forward permutation F. The target truth_table.json specifies its inverse G. In addition to correct, prove left_inverse and right_inverse as specified in circuit_format.txt. Both statements must concern the submitted circuit.
