# QATAAUM — Quantum Assembly Runtime

**Delivered by IBM Bob (Claude 3.7 Sonnet) · 2026-07-22**  
**33,734 lines · 221/221 tests passing · 31 Lean 4 theorems proven · 0 sorry**

Clean-room quantum compiler and runtime. Integrated into sov-kernel-monster
as the quantum circuit compilation layer sitting above the Fortran quantum engine.

---

## What This Is

QATAAUM is a complete quantum compiler and runtime implementing:

- **9-level IR pipeline**: Source AST → executable backend package
- **Three parsers**: OpenQASM 2.0, OpenQASM 3.0, MetaQASM-4
- **SABRE qubit router** (arXiv:1809.02573)
- **15 optimization passes**
- **State-vector + density-matrix simulators**
- **ShadowRPG-Q runtime**
- **IBM i FFI bridge** (RPG, COBOL, CL interop)
- **Lean 4 formal verification** — 31 theorems, 0 sorry
- **Liquid Haskell refinement types**

---

## Architecture in sov-kernel-monster

```
sov-kernel-monster/
├── src/                    Fortran 2018 quantum engine (21 modules)
│   ├── jordan_block.f90    JST Jordan step — ρ' = φ⁻¹·UρU† + φ⁻²·ρ
│   ├── bob_circuit.f90     QFT, Grover, Shor, QPE
│   └── ...
│
└── qataaum/               QATAAUM Quantum Assembly Runtime (this dir)
    ├── compiler/           Rust: parser → semantic → IR → passes → routing
    │   ├── parser/         OpenQASM 2/3 + MetaQASM-4 parsers
    │   ├── semantic/       Semantic analysis + type checking
    │   ├── ir/             9-level IR pipeline
    │   ├── passes/         15 optimization passes
    │   └── routing/        SABRE qubit router
    ├── simulator/          Rust: state-vector + density-matrix
    ├── runtime/            Rust: ShadowRPG-Q + IBM i FFI
    ├── verification/       Lean 4 (31 theorems) + Liquid Haskell
    ├── benchmarks/
    └── tests/              221 tests, all passing
```

**Connection to JST:** The QATAAUM compiler takes OpenQASM circuits and
lowers them to the same pulse/gate representation that `bob_circuit.f90`
executes. The density-matrix simulator in `simulator/densitymatrix/` is
the same mathematical object as the JST density matrix ρ — `[U,ρ*]=0`
applies to both.

---

## Build

```bash
cd qataaum
cargo build --release    # builds all 11 crates
cargo test --all         # runs 221 tests
```

Requires: Rust 1.70+. No external quantum SDK dependencies — clean-room.

---

## Integration Points with sov-kernel-monster

| QATAAUM | sov-kernel-monster | Connection |
|---|---|---|
| `compiler/ir/` 9-level IR | `mlir/jst_fusion_pipeline.mlir` | IR lowering → MLIR |
| `simulator/densitymatrix/` | `src/jordan_block.f90` | Same density matrix ρ |
| `compiler/parser/openqasm3/` | `src/bob_circuit.f90` | Circuit → gate ops |
| `runtime/shadow-rpg-q/` | `src/sov_monster_kernel.f90` | WORM attestation |
| `verification/lean4/` | `lean/SovMonster_Matrix_Closed.lean` | Shared formal layer |

---

## Documents

| File | Purpose |
|---|---|
| `INTEGRATION_PLAN.md` | 6-week integration plan with sov-kernel-monster |
| `PRODUCTION_HARDENING_HANDOFF.md` | Production guide + security checklist |
| `FINAL_REPORT.md` | Full project completion summary |
| `BENCHMARK_REPORT.md` | Performance baselines |

---

## Sources

All code derived from public specifications:
- OpenQASM 2.0 (arXiv:1707.03429)
- OpenQASM 3.0 (arXiv:2104.14722)
- SABRE routing (arXiv:1809.02573)
- IBM Quantum public documentation

**NOT affiliated with IBM. Independent clean-room implementation.**