Metadata-Version: 2.4
Name: emlint
Version: 0.1.2
Summary: A static analysis tool for quantum error correction
Author: Mathys Rennela
License: Apache-2.0
Keywords: quantum,error-correction,static-analysis,detector-error-model,stim,linter
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Natural Language :: English
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Physics
Classifier: Topic :: Software Development :: Quality Assurance
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: stim>=1.14
Provides-Extra: dev
Requires-Dist: pytest; extra == "dev"
Requires-Dist: hypothesis; extra == "dev"
Provides-Extra: benchmark
Requires-Dist: pytest; extra == "benchmark"
Requires-Dist: hypothesis; extra == "benchmark"
Requires-Dist: qldpc; extra == "benchmark"
Dynamic: license-file

# emlint

![emlint logo](docs/images/emlint_logo_with_name.png)

[![PyPI](https://img.shields.io/pypi/v/emlint)](https://pypi.org/project/emlint/)

**stim simulates. sinter samples. emlint verifies.**

emlint is a static linter for Detector Error Models (DEMs). It catches structural bugs in milliseconds — before you run a single shot.

## The problem

A DEM describes a circuit's noise as a list of *error mechanisms* — independent faults, each with a probability and a syndrome footprint: which detectors it fires and which logical observables it flips. 
A detector is a linear combination of syndrome measurement outcomes that detects when a specific error has occurred.

A `DETECTOR` instruction omitted in round 2 of a circuit leaves detector D1
wired to nothing. The decoder silently miscorrects. The logical error rate
rises. The bug is invisible until ~10⁶ simulation shots (≈45 minutes on a
standard laptop).

```
$ emlint check 'error(0.001) D0 L0
detector(0,0,0) D0
detector(1,0,2) D1'

Detectors: 2  Observables: 1  Error mechanisms: 1

  ✓ detectability: All error mechanisms that flip observables also trigger detectors.
  ✗ sensitivity: 1 detector(s) are never triggered by any error mechanism.
      Counter-example: Detector(s) not triggered by any error mechanism: D1@(1,0,2)
  ✓ observable_coverage: All declared observables are flipped by at least one error mechanism.
  ✓ probability_bounds: All error mechanism probabilities are in (0, 0.5].
  ✓ duplicates: No duplicate mechanism signatures found.
  ✓ correctability: Every syndrome maps to at most one distinct set of logical observables.
```

2ms. One line. No simulation. D1 carries coordinates `(1, 0, 2)` — round 2,
position (1, 0) — so you know exactly where in the circuit to look.

```
$ emlint check 'error(0.001) D0 L0
error(0.001) D1
detector(0,0,0) D0
detector(1,0,2) D1'

  ✓ detectability  ✓ sensitivity  ✓ observable_coverage
  ✓ probability_bounds  ✓ duplicates  ✓ correctability
```

## Installation

```
pip install emlint
```

## Usage

### CLI

```
emlint check path/to/circuit.dem
emlint check path/to/circuit.dem --format json
emlint check path/to/circuit.dem --check detectability,sensitivity
emlint check path/to/circuit.dem --severity error
```

Exit code `0` when all checks pass. Exit code `1` when any `error`-severity
check fails. Exit code `2` when there are warnings but no errors (usable in CI
to optionally escalate warnings without breaking the build).

`--severity error` suppresses `warning`-severity findings entirely — only
`error`-severity violations appear in output and affect the exit code. Useful
in CI pipelines where warnings are acknowledged but should not break the build.

### Python API

```python
import stim
import emlint

circuit = stim.Circuit.generated(
    "surface_code:rotated_memory_z",
    rounds=3,
    distance=5,
    after_clifford_depolarization=0.001,
)
report = emlint.check(circuit.detector_error_model(decompose_errors=True))
print(emlint.format_text(report))
```

`emlint.check()` also accepts a `pathlib.Path` or a raw DEM string.

### CI integration

Add to `.github/workflows/emlint.yml`:

```yaml
name: emlint
on:
  push:
    paths: ['**.dem']
  pull_request:
    paths: ['**.dem']

jobs:
  lint:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install emlint
        run: pip install emlint
      - name: Run emlint on all DEM files
        run: find . -name "*.dem" | xargs -I{} emlint check {}
```

## Checks

| Check | What it catches | Severity |
|---|---|---|
| `detectability` | Errors that flip observables but trigger no detectors (undetectable) | error |
| `sensitivity` | Detectors never triggered by any error mechanism (dead detectors) | warning |
| `observable_coverage` | Logical observables never flipped by any error mechanism | error |
| `probability_bounds` | Error probabilities outside `(0, 0.5]` | error |
| `duplicates` | Error mechanisms with identical (detector, observable) signatures | warning |
| `correctability` | Syndromes mapping to multiple distinct observable sets | error |

All checks operate on the standalone `.dem` file — no original circuit required.
Each failing check produces a counter-example pointing to the specific mechanism
or detector at fault.

## Formal grounding

The checks are formal properties of a detector error model, expressed in terms of error mechanisms, detectors, and observables:

- **mechanisms**: independent physical faults, each with a probability and a signature (which detectors it triggers, which observables it flips).
- **detectors**: the set of detector indices in the model.
- **observables**: the set of logical observable indices being protected.

The six checks verify these properties:

| Check | Formal property |
|---|---|
| `detectability` | ∀m ∈ mechanisms, obs(m) ≠ ∅ → det(m) ≠ ∅ |
| `sensitivity` | detectors ⊆ ⋃ₘ det(m) |
| `observable_coverage` | observables ⊆ ⋃ₘ obs(m) |
| `probability_bounds` | ∀m ∈ mechanisms, 0 < p(m) ≤ 0.5 and p(m) ∉ {NaN, ±∞} |
| `duplicates` | ∀m ≠ m′, (det(m), obs(m)) ≠ (det(m′), obs(m′)) |
| `correctability` | ∀m, m′, det(m) = det(m′) → obs(m) = obs(m′) |

## Tutorial: debugging using emlint

When a check fails, the counter-example tells you *where* in the DEM the problem
is. Each subsection below tells you *what* circuit-level mistake most likely produced it
and where to look in your circuit source.

### `detectability` fails

> `error(0.001) flips L0 but triggers 0 detectors`

The listed mechanism flips a logical observable but no detector fires — the
decoder has no syndrome signal to correct it.

**What went wrong in the circuit:**
- A `DETECTOR` instruction was omitted from a syndrome measurement round. The
  round still runs and produces data, but no detector was wired to it.
- `OBSERVABLE_INCLUDE` targets a qubit that is outside the fault support of every
  modelled error (wrong qubit index, wrong basis).

**Where to look:** search your circuit for the round that *should* cover the data
qubits referenced in the failing mechanism's observable. Check that every syndrome
extraction round ends with a `DETECTOR` pointing at the right ancilla measurement.

---

### `sensitivity` fails

> `Detector(s) not triggered by any error mechanism: D17@(1,0,2)`

The listed detector is declared but no error mechanism ever fires it.

**What went wrong in the circuit:**
- The ancilla qubit for this detector is measuring in the wrong Pauli basis
  (`X` vs `Z` mismatch), so the errors that should flip it pass through silently.
- The detector's coordinates point to the wrong spatial position — the qubit index
  in `DETECTOR rec[…]` is off by one.
- A syndrome round was accidentally removed from the circuit, leaving its detector
  declaration orphaned.

**Where to look:** the detector's coordinates (shown as `D17@(col,row,round)`)
identify the syndrome round and stabilizer position. Verify that the corresponding
ancilla qubit is connected to data qubits via the expected CNOT schedule, and that
the noise model includes errors on those CNOTs.

---

### `observable_coverage` fails

> `Observable(s) not flipped by any error mechanism: L1`

The listed logical observable is declared but no physical error can flip it.

**What went wrong in the circuit:**
- `OBSERVABLE_INCLUDE` on the wrong qubit or at the wrong point in the circuit
  (e.g. applied to an ancilla instead of a data qubit, or after a reset that
  erases the correlation).
- Observable index off-by-one in a multi-observable code.

**Where to look:** the counter-example gives you the observable index (e.g.
`L1`). Search your circuit source for every `OBSERVABLE_INCLUDE` with that
index. Verify that the qubit it references is part of the logical operator's
support and that errors on that qubit survive to the measurement record.
(`emlint check --format json` outputs counter-examples as structured data,
making it easy to script a targeted search when the circuit is auto-generated.)

---

### `probability_bounds` fails

> `error(0.0) D0 D1 — zero probability`  
> `error(nan) D3 — NaN probability`

An error mechanism has a probability of exactly 0 (a no-op), is negative, or is
NaN — all of which indicate a fault in DEM generation, not a physical noise model.

**What went wrong in the circuit / DEM generation script:**
- Numerical underflow: a product of small probabilities rounded to 0 instead of
  being pruned or clamped.
- Naive addition of two complementary probabilities exceeded 1, producing a
  negative remainder.
- A copy-paste error in a manual DEM left a placeholder (`nan`, `-1`, `0`)
  instead of a real probability.

**Where to look:** the mechanism's detector and observable targets identify which
fault path the DEM compiler was trying to express. Trace that fault path back to
the noise model parameters in your DEM generation script.

---

### `duplicates` fails

> `error(0.001, 0.001) share signature D3 D7; XOR-fused probability is 0.001998`

Two or more mechanisms share the same `(detectors, observables)` signature — the
same physical fault path is counted more than once.

**What went wrong in the circuit / DEM assembly:**
- Sub-circuit DEMs were concatenated (e.g. bulk + boundary + initialisation)
  without merging mechanisms that touch the same fault path. The correct operation
  is XOR-fusion: `p_eff = p1(1−p2) + p2(1−p1)`.
- An X error and a Y error on the same data qubit at a repetition code boundary
  each trigger the same detector set and flip the same observable (legitimate
  physics; use `--severity error` in CI to suppress this warning for known-correct
  code families).

**Where to look:** if the duplicate arises from concatenation, find the boundary
between the sub-circuits where the mechanism originates. If you are manually
composing DEMs with Python, apply XOR-fusion instead of list concatenation.

---

### `correctability` fails

> `syndrome {D3 D7} maps to observable sets {L0}, {L1}`

The same detector syndrome is produced by mechanisms that flip *different*
observables — the decoder cannot determine the correct logical correction.

**What went wrong in the circuit:**
- Two physically distinct errors (e.g. an X error on qubit A and a Z error on
  qubit B) produce the same syndrome but flip different logical observables. This
  is a genuine code distance problem: the code cannot distinguish them.
- A degenerate code family (colour codes) has syndromes that legitimately map to
  multiple valid logical corrections — this is an expected property, not a bug.

**Where to look:** the counter-example gives you the exact syndrome (e.g.
`{D3 D7}`) and the conflicting observable sets. Search your `.dem` file for
every `error(…)` line whose detector targets match that set — those are the two
colliding mechanisms. In the original circuit, find the gate locations
corresponding to each mechanism's targets (the detector coordinates annotate
the round and spatial position). If both locations are in the *same* Pauli
basis and the same round, this is likely a genuine distance-1 path. If they
are in different bases or rounds, look for a missing stabilizer measurement
or a mis-wired CNOT that merges two logically distinct fault paths.

**Be careful:** this check examines each mechanism individually. It does not
detect cases where two *co-occurring* faults combine to produce a syndrome that
maps to conflicting corrections — that is the code distance problem and is not
checked here.

## References

- [arXiv:2407.13826](https://arxiv.org/abs/2407.13826) — formal linear-algebra framework for detector error models;
  source of the detector, noise model, detector error matrix, and circuit
  distance definitions that ground the emlint checks.
- [arXiv:2603.20127](https://arxiv.org/abs/2603.20127) — formal decoder evaluation; operates at the circuit + decoder
  layer and assumes a structurally sound DEM (the precondition emlint establishes).

## License

Apache 2.0
