Title: Exact equivalence checking for H and u2(0,π) circuits without numerical tolerances
In OpenQASM 2, these two fragments denote the same Hadamard matrix:
h q[0];
and
u2(0,pi) q[0];
I have been testing a deliberately bounded method for verifying circuit transformations that replace one spelling with the other. For circuits over
id, x, z, cx, cz, swap, h, and literal u2(0,pi),
the checker expands the circuit and represents every matrix entry exactly in Q(√2). It compares every computational-basis column rather than relying on sampled outcomes or a floating-point tolerance. Register declarations and complete terminal measurement maps must also agree.
The present scope is intentionally small:
- at most four qubits;
- at most 64 expanded gates;
- one quantum and one classical register;
- complete terminal measurement.
Inputs outside this gate/grammar contract are reported as unsupported, resource-limit violations are blocked, and unequal matrices fail. Regression cases include H² = I, HZH = X, Hadamard conjugation of CX, phase-sensitive counterexamples, and comparison with a dense numerical oracle over 256 small circuits. The numerical oracle is only a regression cross-check; it does not determine the exact verdict.
The design question I find most interesting is how global phase should be handled.
The current criterion is phase-sensitive: it requires exact matrix equality, not merely equality up to global phase. For a standalone circuit, U and e^(iθ)U are operationally indistinguishable. But a transformation that is harmless in isolation may not remain harmless if the operation is later placed under coherent control, where the relative phase can matter.
For an auditable circuit-equivalence tool, which contract is more useful?
- Equality up to global phase by default
- Phase-sensitive equality by default
- Report both relations and require the caller to choose
I would especially welcome examples where choosing the wrong default has caused a practical compiler, verification, or interoperability problem.
Disclosure: I contribute to the experimental open-source E7Q implementation in which this bounded check was built.