Metadata-Version: 2.4
Name: veriq-ancillaguard
Version: 0.1.0
Summary: VeriQ AncillaGuard verifies and repairs dirty-ancilla safety in Qiskit circuits.
Author-email: Jiqi Li <lijiqi@ios.ac.cn>, Jingyi Mei <j.mei@liacs.leidenuniv.nl>
License-Expression: MIT
Project-URL: Homepage, https://github.com/veriq-toolkit/Ancilla-Safety
Project-URL: Repository, https://github.com/veriq-toolkit/Ancilla-Safety
Project-URL: Issues, https://github.com/veriq-toolkit/Ancilla-Safety/issues
Project-URL: Changelog, https://github.com/veriq-toolkit/Ancilla-Safety/blob/main/CHANGELOG.md
Project-URL: Paper, https://arxiv.org/abs/2608.13099
Keywords: qiskit,quantum computing,formal verification,ancilla,veriq
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
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: Topic :: Scientific/Engineering :: Physics
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
License-File: NOTICE.md
Requires-Dist: mqt.qcec>=3.0
Requires-Dist: numpy>=2.2
Requires-Dist: qiskit<3,>=2.0
Provides-Extra: dev
Requires-Dist: build>=1.2; extra == "dev"
Requires-Dist: pytest>=8; extra == "dev"
Requires-Dist: ruff>=0.9; extra == "dev"
Requires-Dist: twine>=6; extra == "dev"
Dynamic: license-file

# VeriQ AncillaGuard

[![Qiskit](https://img.shields.io/badge/Qiskit-2.0%2B-6929C4)](https://www.ibm.com/quantum/qiskit)
[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](LICENSE)

VeriQ AncillaGuard verifies whether a unitary Qiskit circuit restores selected
dirty ancilla qubits for every possible input state. Unsafe targets are
diagnosed as logic errors, phase errors, or both. Ancilla-local violations can
also be repaired with a short sequence of single-qubit rotations.

The implementation accompanies the paper
[Formal Verification of Quantum Ancilla Safety](https://arxiv.org/abs/2608.13099).
It provides two complementary verification backends:

- **MQT QCEC**, an equivalence-checking backend that works out of the box.
- **Quokka-Sharp**, the weighted-model-counting backend used by the paper.

This experimental `0.1` release intentionally bundles the paper-era
Quokka-Sharp implementation. Migrating to the current upstream PyPI package is
planned separately so that the validated research kernel remains stable.

## Installation

VeriQ AncillaGuard requires Python 3.10 or newer and Qiskit 2.x.

```bash
python -m pip install veriq-ancillaguard
```

To install the latest source instead:

```bash
git clone https://github.com/veriq-toolkit/Ancilla-Safety.git
cd Ancilla-Safety
python -m pip install .
```

MQT QCEC is installed automatically. The Quokka backend additionally requires
an executable [GPMC](https://github.com/System-Verification-Lab/GPMC) weighted
model counter. Point the package to it with either an argument or an environment
variable:

```bash
export GPMC_PATH=/path/to/gpmc
```

The repository includes the pinned GPMC source under `third_party/GPMC` for
reproducible Linux builds. Its build prerequisites are CMake, GMP, MPFR, zlib,
and a C++ compiler.

### Optional Docker Image

Docker is not required for the Python package. It is provided as a reproducible
Linux environment that builds the pinned GPMC source and makes both backends
available without a separate solver installation:

```bash
docker build -t veriq-ancillaguard .
docker run --rm veriq-ancillaguard --help
docker run --rm -v "$PWD:/data:ro" veriq-ancillaguard \
  verify /data/circuit.qasm --ancilla 0 --backend quokka
```

### Installation Check

Run a built-in safe case and a known logic-error case after installation:

```bash
ancillaguard self-test
```

QCEC is always checked. Quokka is also checked when GPMC is available and is
otherwise reported as skipped. To require a specific backend:

```bash
ancillaguard self-test --backend qcec
ancillaguard self-test --backend quokka --gpmc /path/to/gpmc
```

## Quick Start

```python
from qiskit import QuantumCircuit
from veriq_ancillaguard import verify_dirty_safety

circuit = QuantumCircuit(2)
circuit.cx(0, 1)
circuit.cx(0, 1)

result = verify_dirty_safety(
    circuit,
    ancillas=[circuit.qubits[1]],
    backend="qcec",
)

print(result.status)                  # SafetyStatus.SAFE
print(result.targets[0].logic_safe)  # True
print(result.targets[0].phase_safe)  # True
```

Targets may be Qiskit `Qubit` objects or global integer indices. Targets must be
provided explicitly; the package never guesses which register contains
ancillas.

To use Quokka-Sharp:

```python
result = verify_dirty_safety(
    circuit,
    ancillas=[1],
    backend="quokka",
    gpmc_path="/path/to/gpmc",
)
```

## Repair

The repair pipeline handles violations that remain local to an ancilla qubit.
It returns a new circuit and leaves the input circuit unchanged.

```python
from qiskit import QuantumCircuit
from veriq_ancillaguard import repair_dirty_safety

circuit = QuantumCircuit(1)
circuit.z(0)

result = repair_dirty_safety(circuit, ancillas=[0])
repaired = result.circuit

print(result.before.status)  # SafetyStatus.UNSAFE
print(result.after.status)   # SafetyStatus.SAFE
print(result.patches[0].angles)
```

Repair uses the Quokka backend and therefore requires GPMC. If an error leaves
the ancilla entangled or correlated with other qubits, a local repair is not
possible and the result reports the failure rather than changing unrelated
qubits.

## Command Line

OpenQASM 2 files can be checked without writing Python:

```bash
ancillaguard verify circuit.qasm --ancilla 'anc[0]' --backend qcec
ancillaguard verify circuit.qasm --ancilla 3 --backend quokka --gpmc /path/to/gpmc
ancillaguard repair circuit.qasm repaired.qasm --ancilla 'anc[0]' --gpmc /path/to/gpmc
```

Commands print JSON results and return a nonzero exit code when verification
does not establish safety.

## Benchmark Examples

Four OpenQASM 2 examples are included under [`examples/benchmarks`](examples/benchmarks).
Each checks one documented ancilla target and is expected to be safe with both
backends. Run all examples from a source checkout:

```bash
python examples/run_benchmarks.py --backend qcec
python examples/run_benchmarks.py --backend both --gpmc /path/to/gpmc
```

The large GHZ example contains 1399 qubits and is intended to demonstrate the
backend workflow, not to define a portable performance baseline.

## Supported Circuits

The framework currently targets purely unitary circuits. Measurements, resets,
delays, classical control flow, and unbound parameters are rejected.

The frozen Quokka backend accepts the following basis instructions:

```text
id, x, y, z, h, s, sdg, t, tdg,
rx, ry, rz, cx, cz, cs, csdg, ccx
```

Transpile other unitary instructions explicitly before invoking Quokka. The
package does not silently transpile user circuits because preserving the exact
verification boundary is important.

## Result Semantics

For every selected ancilla, the verifier checks commutativity against Pauli-Z
and Pauli-X:

- failed Z check: `ErrorKind.LOGIC`
- failed X check: `ErrorKind.PHASE`
- both checks pass: the target is dirty safe
- backend cannot decide: `SafetyStatus.INCONCLUSIVE`

MQT QCEC's `equivalent_up_to_global_phase` result is a failed commutativity
check here. A non-trivial relative global phase between `U` and `P U P` is an
anti-commutation witness, not a successful exact equality.

## Development

```bash
python -m pip install -e '.[dev]'
pytest
ruff check src tests examples
python -m build
python -m twine check dist/*
```

Quokka integration tests run when `GPMC_PATH` is configured; otherwise they are
skipped. See [CONTRIBUTING.md](CONTRIBUTING.md) for the contribution workflow.

## Provenance and Citation

The bundled research backend is pinned to Quokka-Sharp commit
`9131a8eab786ffe983a77af6bb374ffdeab06dc4`. Detailed third-party provenance is
recorded in [NOTICE.md](NOTICE.md). Citation metadata is available in
[CITATION.cff](CITATION.cff).

The original artifact-evaluation package and experimental outputs are archived
separately at [Zenodo](https://doi.org/10.5281/zenodo.19784589).
The paper used the former repository URL `Veri-Q/Ancilla-Safety`. GitHub
redirects that transferred-repository URL to the canonical repository above.
The software is published under the product name VeriQ AncillaGuard while the
repository retains its original name for continuity with the paper.

## License

VeriQ AncillaGuard, the bundled Quokka-Sharp snapshot, and the vendored GPMC source
are available under the MIT License. See [LICENSE](LICENSE) and
[NOTICE.md](NOTICE.md).
