# Soufflé-LintQ

A reimplementation of **LintQ** (Paltenghi et al., FSE 2024 — static analysis
for quantum programs built on Qiskit) in **Soufflé Datalog**, for sub-second
quantum linting with **zero proprietary dependencies**.

The original LintQ lifts Qiskit code into quantum-specific domain abstractions on
top of CodeQL. CodeQL is powerful but carries heavy database-compilation
overhead, proprietary licensing, and friction for standalone CI/CD embedding.
Soufflé compiles Datalog rules to a native C++ binary, so the analysis runs as an
ultra-fast, dependency-free executable that lints quantum codebases in
milliseconds and drops trivially into CI / IDEs.

## Status

| Component | State | Verification |
|-----------|-------|--------------|
| `extractor/` — Python AST fact extractor | ✅ built | 13/13 unit tests pass (Python 3.11) |
| `engine/lintq.dl` — Soufflé rules (extractor EDB schema) | ✅ built | runs clean under Soufflé 2.5; 3 warnings fire on `sample_circuit.py` |
| `rules/lintq.dl` — Soufflé rules (compact `Op/ActsOn/Succ` schema) | ✅ built | `run.sh` exits 0; expected warnings, 0 false positives on clean input |
| `web/` — LintQ summary site | ✅ built | static, self-contained, all links resolve |

> **Two complementary engines were produced.** They use different EDB fact
> schemas (see below) but implement the same analyses. Both are verified
> end-to-end with Soufflé 2.5. The `web/` site documents both.

## Pipeline

```
Target Qiskit Script
        │
        ▼
  Python Fact Extractor   (extractor/  — ast.NodeVisitor)
        │  generates .facts (TSV)
        ▼
  [ EDB facts ]
        │
        ▼
  Soufflé Core Engine      (engine/lintq.dl  or  rules/lintq.dl)
   • Quantum domain model
   • CFG transitive closure
   • Quantum analyses
        │  emits .csv
        ▼
  [ Lint Warnings / Diagnostics ]
```

## Layout

| Path | Purpose |
|------|---------|
| `extractor/ast_to_facts.py` | AST visitor → 7 EDB `.facts` files (TSV). |
| `extractor/sample_circuit.py` | Tiny Qiskit snippet with all three anti-patterns. |
| `extractor/test_extractor.py` | 13 unit tests. |
| `extractor/facts/` | Sample EDB facts (7-relation schema). |
| `engine/lintq.dl` | Analyses over the extractor schema: **OpAfterMeas**, **DoubleMeas**, **GhostCompose**. |
| `rules/lintq.dl` | Analyses over the compact schema: **OpAfterMeas**, **DoubleMeas**, **MissingReset**. |
| `rules/run.sh` | Runs `souffle -F ../facts -D out` (creates `out/` first — required by Soufflé 2.5). |
| `facts/` | Sample EDB facts for the `rules/` engine (`Op`, `ActsOn`, `Succ`). |
| `web/index.html` | LintQ summary site (architecture, analyses, real sample warnings). |

## The analyses

- **OpAfterMeas** — a gate acts on a qubit after that qubit was measured, with
  no reset along the CFG path between them.
- **DoubleMeas** — two measurements of the same qubit with no operation on it
  between them (redundant consecutive measure).
- **MissingReset** — the first operation on a qubit is not a reset (used while
  uninitialised).
- **GhostCompose** — `qc.compose(sub)` whose return value is discarded (a silent
  no-op, since `compose` is non-mutating in Qiskit).

## Run it

Prerequisites: Python 3.11+ and Soufflé 2.5.

**Engine A — extractor → engine/**

```bash
# end-to-end: extract sample_circuit.py then run the analyses
bash run.sh

# …or lint an arbitrary Qiskit script
bash run.sh path/to/your_circuit.py

# unit tests
python3 -m unittest extractor.test_extractor   # 13/13 pass
```

> **Gotcha (Soufflé 2.5):** the extractor writes facts to `extractor/facts/`, so
> run the engine with `souffle -F extractor/facts -D out engine/lintq.dl` — **not**
> `-F facts`, which holds the *rules* engine's `Op/ActsOn/Succ` facts and would
> cause `Error loading … Cannot open fact file`. Also create `out/` first:
> Soufflé 2.5 aborts if the `-D` directory does not exist. `bash run.sh` does
> both for you.

**Engine B — rules/**

```bash
cd rules
bash run.sh           # creates out/ then runs souffle -F ../facts -D out
cat out/WarnOpAfterMeas.csv out/WarnDoubleMeas.csv out/WarnMissingReset.csv
```

> Soufflé 2.5 requires the `-D out` directory to pre-exist; `run.sh` creates it.

## Summary site (`web/`)

`web/index.html` is a static, self-contained page (no build step) that presents
the reimplementation: an architecture diagram (Mermaid), the four analysis
descriptions with real `.dl` snippets, the sample buggy program, and the actual
warnings emitted by both engines. Serve it from the repo root so the embedded
source links resolve (e.g. `python3 -m http.server --directory /path/to/parent`
then open `/souffle-lintq/web/index.html`).

## Deployment (lintq.matteopaltenghi.com)

The site is **live at https://lintq.matteopaltenghi.com/** (valid Let's Encrypt
cert, HTTP→HTTPS redirect). It is served by an `nginx:alpine` container
(`lintq-site`) on the host's pre-existing `web` Docker network, with Traefik
(`n8n-traefik_traefik_1`) auto-provisioning the `*.matteopaltenghi.com`
certificate via the `mytlschallenge` ACME resolver — the same wiring used by the
existing `public.matteopaltenghi.com` site. **No external DNS change or repo
token is required**: the subdomain already resolves to this host and Traefik
already terminates it.

The static content is the `lintq-deploy/` directory
(`index.html` + the `souffle-lintq/` source tree).

```bash
# Publish/refresh the live site (rebuild lintq-deploy/ from source first):
rsync -a --delete souffle-lintq/ lintq-deploy/souffle-lintq/
cp souffle-lintq/web/index.html lintq-deploy/index.html

# (re)start the serving container on the shared 'web' network:
docker rm -f lintq-site 2>/dev/null
docker run -d --name lintq-site --restart unless-stopped --network web \
  -v /home/ubuntu/lintq-deploy:/usr/share/nginx/html:ro \
  -v /home/ubuntu/lintq-deploy/nginx.conf:/etc/nginx/conf.d/default.conf:ro \
  -l 'traefik.enable=true' \
  -l 'traefik.http.routers.lintq.entrypoints=web,websecure' \
  -l 'traefik.http.routers.lintq.rule=Host(`lintq.matteopaltenghi.com`)' \
  -l 'traefik.http.routers.lintq.tls=true' \
  -l 'traefik.http.routers.lintq.tls.certresolver=mytlschallenge' \
  nginx:alpine
```

Files: `lintq-deploy/nginx.conf` (server block),
`lintq-deploy/docker-compose.yml` (equivalent compose spec for hosts with
`docker compose`).

## Reference

Paltenghi, Moriconi, et al. *LintQ: A Static Analysis Framework for Qiskit
Quantum Programs.* FSE 2024. This project is an independent Soufflé
reimplementation for dependency-free, sub-second linting.