Context-Verified, Error-Budget-Aware Decomposition Selection for Toffoli Networks

Two-qubit-gate error dominates the failure budget of near-term quantum circuits, so the decomposition chosen for each Toffoli (CCX) gate should minimize hardware two-qubit infidelity, not gate count. The cheapest decompositions - relative-phase and approximate Toffolis - are only correct in context: their residual phase or bounded error must be cancelled or absorbed downstream. We present the first compiler pass that selects a per-Toffoli decomposition to minimize a two-qubit-infidelity error budget. It admits each context-dependent decomposition only when an exact, instance-specific equivalence check certifies its validity in that circuit context, coupling an error-budget objective with per-instance verification and closing the gap between context-aware-but-unverified and verified-but-context-free optimizers. The central result is a safety one: pattern-matched relative-phase substitution is silently incorrect. Our verifier flags 66 library rewrites of a deployed open optimizer as non-equivalent without a context check, and count-greedy substitution silently corrupts 6 of 12 benchmark circuits; the verification gate certifies 0 errors while still applying every valid decomposition. The two-qubit-gate reduction is real but workload-dependent: up to 39.5% fewer two-qubit gates and 36.7% lower infidelity over exact-only on a compute/uncompute-heavy suite (approx. 39%/35% versus Qiskit opt-3 and tket), and 15.6% aggregate on a larger 12-24-qubit suite, with decision-diagram checking certifying every substitution past the exhaustive-verification limit. At current superconducting and trapped-ion error rates, the certified substitutions lower estimated circuit infidelity by 36-43%, and on a quantum state-resetting circuit, the pass removes 48.8% of the native two-qubit gates, every substitution verified.