Metadata-Version: 2.4
Name: qrig
Version: 1.1.0
Summary: Verified controlled quantum circuits ("One rig to control them all"): exact semantics, control equations, Gray-code synthesis and optimisation, with a C core extracted from Lean 4
Author: Shashi Kumar
Maintainer: Shashi Kumar
License-Expression: Apache-2.0
Project-URL: Homepage, https://github.com/ShashiQubit/qrig
Project-URL: Repository, https://github.com/ShashiQubit/qrig
Project-URL: Documentation, https://github.com/ShashiQubit/qrig#readme
Keywords: quantum,quantum-computing,circuit-optimization,qiskit,formal-verification,lean4,control-equations
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Scientific/Engineering :: Physics
Classifier: Topic :: Software Development :: Compilers
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Operating System :: POSIX :: Linux
Classifier: Operating System :: MacOS
Classifier: Operating System :: Microsoft :: Windows
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: numpy
Provides-Extra: qiskit
Requires-Dist: qiskit>=1.0; extra == "qiskit"
Provides-Extra: test
Requires-Dist: pytest; extra == "test"
Requires-Dist: qiskit>=1.0; extra == "test"
Provides-Extra: mqt
Requires-Dist: qiskit>=1.0; extra == "mqt"
Requires-Dist: mqt.bench; extra == "mqt"
Requires-Dist: mqt.qcec; extra == "mqt"
Provides-Extra: noise
Requires-Dist: qiskit>=1.0; extra == "noise"
Requires-Dist: qiskit-aer; extra == "noise"
Requires-Dist: qiskit-ibm-runtime; extra == "noise"
Requires-Dist: mqt.bench; extra == "noise"
Requires-Dist: matplotlib; extra == "noise"
Dynamic: license-file

# 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:

```python
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

```bash
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:

```bash
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

```python
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)

```python
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`](benchmarks/MQT_PIPELINE.md) for the MQT Bench / MQT QCEC
pipeline and results.

### Circuit language (Definition 6 of the paper)

| Python            | paper                  |
|-------------------|------------------------|
| `I(n)`            | `id_n`                 |
| `X`               | the involution `x`     |
| `SWAP`            | the symmetry `σ₁,₁`    |
| `f >> g`          | `f ; g` (first `f`)    |
| `f + g`           | `f + g` (`f` on top)   |
| `C1(f)`, `C0(f)`  | the control functors   |
| `gate(M)`         | a one-qubit base gate with entries in Q(ω) |
| `phase(z)`        | a scalar (0 → 0 morphism) such as the global phase ω |

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/`).

| theorem | file | statement |
|---|---|---|
| `ctrl_seq`, `ctrl_id`, `ctrl_par_id`, `colour_change`, `complementarity`, `ctrl_comm`, `swap_eq_cnots`, `swap_ctrl_ctrl` | `QrigProofs/ControlEquations.lean` | the eight control equations (a)–(h) of Figure 1 hold in the semantics `den` (the functor `A : cP → P₂`), for every local interpretation of the base generators |
| `denA_eq_tab_den` | `QrigProofs/ArrayEval.lean` | the fast array evaluator used at run time computes `den` |
| `simulate_spec`, `unitary_spec`, `equivExact_iff` | `QrigProofs/Exact.lean` | simulation, the unitary matrix and the exact equivalence check are correct (equivalence is decided exactly) |
| `den_perm`, `synthPerm_sound` | `QrigProofs/Classical.lean` | classical circuits act as permutations of basis states; every circuit returned by the synthesiser is made of NOT/controlled-NOT gates only and implements the requested permutation |
| `grayR_bijOn`, `grayR_adjacent` | `QrigProofs/Gray.lean` | `rₙ` is a bijection of `{0,…,2ⁿ−1}` and consecutive Gray code words differ in exactly one bit |
| `simplify_sound` | `QrigProofs/Simplify.lean` | the rewrite-based optimiser preserves the semantics (for any local interpretation and any sound fusion rule) |
| `gateFuse_sound`, `simplifyQ_sound`, `unitary_simplifyQ` | `QrigProofs/GateFuse.lean` | the concrete optimiser used by `qrig.simplify` preserves the exact unitary |
| `QOmega.instCommRing` | `QrigProofs/QOmega.lean` | the exact scalar arithmetic Q(ω) is a commutative ring |
| `combine_sound`, `commutes_sound`, `xconj_sound`, `optimize_sound` | `QrigProofs/Peephole.lean` | the DAG-level rewrite rules ((a),(b),(e); (f) and diagonal commutation; (d)) and the whole gate-list optimiser preserve the action on every vector, for any sound matrix interpretation of the base gates |
| `peephole_sound` | `QrigProofs/PeepholeOps.lean` | the concrete optimiser behind `qrig.dag` preserves the exact action of the gate list on every complex state vector (gates X, Y, H, SX, SX†, P/RZ/RX/RY(qπ), opaque gates with arbitrary matrices) |
| `incrementer_spec`, `hamming_weight_correct`, `memberOracle_spec`, `qrom_spec`, `run_xconj` | `QrigProofs/Study/Reversible.lean` | study kernels, in a gate-list model of NOT/multiply controlled NOT circuits written to mirror `benchmarks/app_circuits.py`: the incrementer adds 1 mod 2ⁿ, the Hamming-weight kernel leaves the popcount in its counter, the membership oracle flips its target iff the input is in the set, QROM XORs `table[address]` into the data register; and colour change (d) on basis states |
| `phiAdd_correct`, `phiAdd_correct_qubit`, `phiAddOld_wrong` | `QrigProofs/Study/Draper.lean` | the phase angles of the Draper adder in `shor_modadd` turn `QFT\|x⟩` into `QFT\|(x+a) mod 2ⁿ⟩` under Qiskit's `QFTGate` convention; the formula used before a fix during the study does not |
| `esp_sublist_le`, `espUniform_robust`, `espUniform_tradeoff_not_robust`, `shotsNeeded_div`, `geomean_le_one` | `QrigProofs/Study/Metrics.lean` | properties of the report's metrics: removing gates never lowers the estimated success probability; using no more 1q and 2q gates gives a higher ESP at every noise strength (and both counts are needed); shot saving = (fidelity ratio)²; the per-circuit geometric mean ratio is ≤ 1 when no circuit gets worse |

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`](benchmarks/README.md).

![Benchmark comparison](benchmarks/benchmark.png)

## 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`](benchmarks/NOISE.md).

![Noise benchmark](benchmarks/noise_benchmark.png)

## Tests

```bash
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

```bibtex
@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}
}
```
