qrig — verified controlled quantum circuits

qrig implements the calculus of the paper One rig to control them all (Heunen, Kaarsgaard, Lemonnier, arXiv:2510.05032) as a Python module:

import qrig

Like numpy, qrig has a compiled core behind a thin Python layer. Here the core is C code generated by the Lean 4 compiler from Lean definitions that have machine-checked correctness proofs (see What is proved below). The Python layer only builds circuit terms, converts data and talks to Qiskit.

Installation

pip install ./python            # from the repository root
pip install "./python[qiskit]"  # with Qiskit support

The prebuilt native core (qrig/_bin/qrig-core, a self-contained Linux x86-64 executable) ships with the package. To rebuild it from the Lean sources:

cd python
python3 build_native.py          # lake build Qrig  ->  generated C  ->  cc
python3 build_native.py --no-lake   # recompile only the committed generated C

Two backends exist and agree on every command (QRIG_BACKEND=inproc|process):

• inproc: qrig/_bin/libqrig.so is loaded through ctypes (needs the Lean runtime libleanshared.so from a Lean toolchain);
• process: the static executable qrig-core is started once and used through a pipe (no dependencies). This backend is used automatically when inproc cannot be loaded.

Quick tour

import qrig
from qrig import X, H, T, S, C0, C1, I, SWAP

toffoli = C1(C1(X))                          # C¹(C¹(x))
qrig.permutation(toffoli)                    # [0, 1, 2, 3, 4, 5, 7, 6]
qrig.unitary(H)[0][0]                        # exact: 1/2·ω − 1/2·ω³  (= 1/√2)
qrig.unitary(H, exact=False)                 # numpy complex matrix

qrig.equivalent(C0(X) >> C1(X), I(1) + X)    # control equation (e): True
qrig.equivalent(T >> T, S)                   # True (exact arithmetic in Q(ω))

qrig.synthesize_permutation([0, 1, 3, 2, 4, 5, 7, 6])  # Gray-code synthesis (Thm 9)
qrig.simplify(H >> T >> T >> H >> H >> S.dagger() >> H)  # -> I1
qrig.gray_code(3)                            # [0, 1, 3, 2, 6, 7, 5, 4]

qc = toffoli.to_qiskit()                     # Qiskit QuantumCircuit
qrig.from_qiskit(qc)                         # and back (exact gates only)

from qrig.qiskit_bridge import optimize_qiskit, QrigOptimize   # Qiskit integration

Qiskit DAG pass (production circuits)

from qiskit.transpiler import PassManager
from qrig.dag import QrigControlEquations, optimize_circuit

pm = PassManager([QrigControlEquations(window=128)])   # before Qiskit's own passes
out = pm.run(qc)
pm.property_set["qrig_stats"].rules      # {'idRem':…, 'fuse':…, 'cancel':…, 'compl':…, 'xconj':…}
out, stats = optimize_circuit(qc)        # same, without a PassManager

Every DAG node is read as a multiply controlled one-qubit gate (cx, ccx, mcx, cp, mcphase, crz, ch, c3sx, u, … with any control state) and the list is rewritten by the Lean-verified core Qrig/Core/Peephole.lean using the control equations: (a) fusion, (a)+(b) cancellation, (b) identity removal, (e) complementarity, (d) colour change through NOT gates, (f) commutation. Angles are sent as exact rational multiples of π. Measurements, resets, barriers, swap and symbolic gates stay in place; other gates are expanded into their definitions. See benchmarks/MQT_PIPELINE.md for the MQT Bench / MQT QCEC pipeline and results.

Circuit language (Definition 6 of the paper)

Named gates: H, S, Sdg, T, Tdg, Z, Y, V (=SX), Vdg, XGATE, GLOBAL_OMEGA. Helpers: seq, par, on_wires, controlled_on, mcx, adjacent_swap. qrig.paper provides the control equations (a)–(h), the Sleator–Weinfurter construction (Figure 3), Gray transpositions β(θₙ,ᵢ) and the commuting CNOTs of equation (11).

Wire k of an n-wire circuit is Qiskit qubit n-1-k, so Operator(c.to_qiskit()).data == qrig.unitary(c, exact=False) entry by entry.

What is proved (in Lean 4, no sorry, standard axioms only)

The Lean project in the repository root contains the executable core (Qrig/, no Mathlib dependency, compiled to C) and the proofs about it (QrigProofs/).

The Study/ theorems are about Lean models of the study's kernels and metrics, not about the Python code itself; tests/test_kernels.py runs the actual Qiskit kernels on every basis state and checks them against the same specifications.

What is not formally verified (but is tested)

• The completeness theorem of the paper (every equation between circuits follows from (a)–(h)) is not formalised; qrig decides equality semantically instead.
• The synthesiser's search (bubble sort in Gray order) is not proved to always succeed; its output is checked at run time before being returned (and that check is what synthPerm_sound relies on). It succeeds on all 40 320 permutations of 3 bits and on random permutations of up to 5 bits in the test-suite.
• The textual serialisation between Python and C, dagger, equivalent(..., up_to_phase=True), the FFI glue (Qrig/FFI.lean, csrc/*.c) and the Python/Qiskit bridge are ordinary (tested) code.
• The conversion between Qiskit DAG nodes and flat gate lists in qrig/dag.py (reading control states, the exact decompositions U(θ,φ,λ) = P(φ)·RY(θ)·P(λ), expansion of other gates via their Qiskit definitions, float ↔ rational angles) is tested against Qiskit's Operator and MQT QCEC, not proved.
• The Lean compiler and the C compiler are trusted.

Benchmark: is it worth adding qrig to a Qiskit pipeline?

benchmarks/benchmark.py compares Qiskit's level-3 pipeline with and without QrigOptimize as a pre-pass, and produces benchmarks/benchmark.png. In short: large CNOT savings (29–100 %) on circuits with structured multi-controlled gates, no change on unstructured or library circuits, and the Gray-code permutation synthesis is not competitive on gate count. See benchmarks/README.md.

Noise: how much error does qrig remove?

benchmarks/noise_benchmark.py simulates the compiled circuits with and without qrig under noise (Qiskit Aer; depolarizing noise at 0.3 % per CX, and the IBM Torino calibration with routing and T1/T2). In the depolarizing model, removing gates with qrig removed 9–24 % of the output error on the MQT Bench Grover (4–5 qubits) and multiplier (8–16 qubits) circuits, and 32–100 % on circuits with structured multi-controlled gates. Deeper circuits keep less fidelity either way, but qrig still raises it by ×1.1–×16. When the circuit gives no CX saving, fidelity is unchanged. On the device model the gains mostly carry over, but placement and idle time can cancel a small saving (Grover 5: 2 % worse). With all-to-all connectivity (an IBM-Heron-median model and a trapped-ion-like model with assumed parameters), which removes any routing/topology bias, Grover 5 improves too (4 % and 13 % of the error removed) and most other gains are similar or larger. See benchmarks/NOISE.md.

Tests

cd python && python3 -m pytest -q tests

The suite (235 tests, including 85 for the DAG pass in tests/test_dag.py) compares qrig with Qiskit's Operator/Statevector on every named gate, every control pattern and placement on up to 4 wires, swaps and Fredkin gates, random circuits, imports of random and library Qiskit circuits, all control equations of the paper, the Sleator–Weinfurter identity, all 3-bit permutations for synthesis, the optimiser (random circuits, inverses, the Qiskit pass), error handling, serialisation round trips and both backends.

Authors & Contributors

• Shashi Kumar — Core implementation, cross-platform architecture, benchmarks, and packaging.

Citation

@article{heunen2025rig,
  title={One rig to control them all},
  author={Heunen, Chris and Kaarsgaard, Robin and Lemonnier, Nicolas},
  journal={arXiv preprint arXiv:2510.05032},
  year={2025}
}