# LintQ Challenge Example Set

A curated, **engine-verified** benchmark of Qiskit code snippets that exercise
the bug classes detected by Souffle-LintQ. Each example ships with:

  * the source (`exNN_*.py`),
  * the expected bug type and ground-truth detector labels
    (`challenges.json`), and
  * a verification harness (`verify_challenges.py`) that runs every example
    through **both** LintQ engines and checks the emitted warnings against the
    labels.

The goal of this set is to give detector implementers a concrete, labelled
corpus to build against, and to give evaluators a stable regression suite.

## Bug classes (the four LintQ detectors)

| Detector        | Bug class                                            | Engines |
|-----------------|------------------------------------------------------|---------|
| OpAfterMeas     | A gate acts on a qubit *after* that qubit was        | A, B    |
|                 | measured, with no reset between along the CFG path.   |         |
| DoubleMeas      | Two measurements of the *same* qubit with no          | A, B    |
|                 | operation on that qubit between them (redundant).     |         |
| MissingReset    | The first operation on a qubit is not a reset         | B only  |
|                 | (used / measured while uninitialised).                |         |
| GhostCompose    | `qc.compose(sub)` whose return value is discarded     | A only  |
|                 | (a silent no-op, because `compose` is non-mutating).  |         |

Engine A (`engine/lintq.dl`) consumes the extractor's 7-relation EDB schema
and implements OpAfterMeas, DoubleMeas, GhostCompose. Engine B
(`rules/lintq.dl`) consumes the compact `Op/ActsOn/Succ` schema and implements
OpAfterMeas (reset-aware), DoubleMeas, MissingReset.

> Coverage note: Engine A's OpAfterMeas does **not** model a reset between the
> measure and the later gate, so it can false-positive on reset-safe code
> (see ex02). Engine B's OpAfterMeas is reset-aware and stays silent there.
> Engine A has no MissingReset rule; Engine B has no GhostCompose rule. These
> gaps are captured explicitly in the labels via `N/A` / `FALSE_POS`.

## Ground-truth label legend

Each example carries a `ground_truth` map keyed by detector, with one value:

  * `FIRE`      — the bug class is present; the detector is expected to warn.
  * `SILENT`    — the bug class is intentionally **absent**; the detector must
                  stay silent (a negative / anti-pattern-false example).
  * `FALSE_POS` — a known engine limitation: a reset-blind detector will
                  erroneously fire here (documented, not a defect to fix).
  * `N/A`       — the engine/detector is structurally unable to observe this
                  bug class (schema or rule gap).

## The 17 examples

| #  | File                                | Bug class            | Category       | Why it is challenging |
|----|-------------------------------------|----------------------|----------------|------------------------|
| 1  | ex01_op_after_meas_basic.py         | OpAfterMeas          | correctness    | Baseline post-measure gate on q0. |
| 2  | ex02_op_after_meas_reset_safe.py    | OpAfterMeas (neg.)   | correctness    | Reset between measure & gate: B silent, A falsely fires (limitation). |
| 3  | ex03_op_reach_2qubit.py             | OpAfterMeas (cx)     | correctness    | 2-qubit gate touches the measured qubit only; must not flag the control qubit. |
| 4  | ex04_op_after_meas_branch.py        | OpAfterMeas (branch) | correctness    | Gate after measure only on the if-true path. |
| 5  | ex05_op_after_meas_loop.py          | OpAfterMeas (loop)   | correctness    | Gate after measure inside a loop body (CFG back-edge). |
| 6  | ex06_double_meas_basic.py           | DoubleMeas           | correctness    | Consecutive measure of q0. |
| 7  | ex07_double_meas_reset_between.py   | DoubleMeas (neg.)    | correctness    | Reset between the two measures suppresses DoubleMeas. |
| 8  | ex08_double_meas_diff_qubits.py     | DoubleMeas (neg.)    | correctness    | Two measures of *different* qubits must not trigger. |
| 9  | ex09_double_meas_branch.py          | DoubleMeas (branch)  | correctness    | Second measure only on the if-true path. |
| 10 | ex10_double_meas_2qubitgate.py      | OpAfterMeas+DoubleMeas| correctness  | Same `cx` suppresses DoubleMeas but triggers OpAfterMeas (opposite verdicts). |
| 11 | ex11_missing_reset_basic.py         | MissingReset         | correctness    | First op on q0 is a gate, not a reset. |
| 12 | ex12_missing_reset_multi.py         | MissingReset (multi) | correctness    | q1 and q2 uninitialised; q0 reset first; two qubits reported. |
| 13 | ex13_missing_reset_meas_first.py    | MissingReset+OpAfterMeas| correctness | measure-then-gate feeds both analyses across the two engines. |
| 14 | ex14_missing_reset_2qubit_gate.py   | MissingReset (cx)    | correctness    | cx is the first op touching q0 & q1 — both uninitialised. |
| 15 | ex15_ghost_compose_basic.py         | GhostCompose         | silent-noop   | `qc.compose(sub)` return value discarded. |
| 16 | ex16_ghost_compose_assigned.py      | GhostCompose (neg.)  | silent-noop   | `qc2 = qc.compose(sub)` keeps the value; must stay silent. |
| 17 | ex17_ghost_compose_loop.py          | GhostCompose (loop)  | silent-noop   | `compose()` discarded repeatedly in a loop. |

Full per-example metadata (description, notes, and the complete label map) is
in `challenges.json` — that file is the **single source of truth** for the
harness and this document.

## How to verify the set

From the repo root (needs Python 3.11+, Souffle 2.5, and the extractor on the
path — `verify_challenges.py` adds `extractor/` automatically):

    cd souffle-lintq/examples
    python3 verify_challenges.py

The harness:
  1. parses each example with the AST extractor -> Engine A EDB facts;
  2. runs Engine A and collects its warnings;
  3. synthesises Engine B's compact `Op/ActsOn/Succ` facts (reset is modelled
     as `kind="reset"`, so Engine B's reset-aware OpAfterMeas behaves
     correctly) and runs Engine B;
  4. compares every detector's verdict against `challenges.json`.

It exits non-zero if any detector expected to FIRE/SILENT produces a real
FALSE_POS / FALSE_NEG (a `FALSE_POS(limitation)` on ex02 and any `N/A` are not
counted as failures). The current run confirms all 17 examples with 0
mismatches.

## Using this set to implement detectors

  * Start with the `FIRE` examples per detector — they must each trigger a
    warning with the correct qubit/statement location.
  * Add the `SILENT` negatives (ex02, ex07, ex08, ex16) as regression tests so
    the detector does not over-report.
  * ex10 is the key cross-detector case: the same `cx` must fire OpAfterMeas
    while DoubleMeas stays silent.
  * ex02 documents the reset-model gap between Engine A (reset-blind) and
    Engine B (reset-aware) OpAfterMeas — a good target for a shared,
    reset-aware rule.

## Extending the set

Append an entry to `challenges.json` (with `id`, `file`, `title`, `category`,
`bug_class`, `description`, `ground_truth`, `notes`) and create the matching
`exNN_*.py`. Re-run `verify_challenges.py`; it validates that every referenced
file exists and that the engines' output matches the new labels.