From 07dfdfbda02b7fa4fdbb5c65d0fa3416a590d04d Mon Sep 17 00:00:00 2001 From: "Marcus (agent-cos)" Date: Sun, 10 May 2026 00:45:13 -0700 Subject: [PATCH] =?UTF-8?q?docs:=20Prove=20SQLite=20project=20plan=20?= =?UTF-8?q?=E2=80=94=20pager,=20WAL,=20VDBE,=20B-Tree?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Sequel to Prove Kafka. Targets SQLite's core state machines for formal verification: pager (transaction lifecycle, journal modes), WAL (concurrent read/write, checkpoint), VDBE (bytecode engine), and B-Tree (page organization, splits, merges). 12 milestones across 3 phases, documented invariants per layer. --- docs/PROVE-SQLITE-PLAN.md | 102 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 102 insertions(+) create mode 100644 docs/PROVE-SQLITE-PLAN.md diff --git a/docs/PROVE-SQLITE-PLAN.md b/docs/PROVE-SQLITE-PLAN.md new file mode 100644 index 0000000..475b185 --- /dev/null +++ b/docs/PROVE-SQLITE-PLAN.md @@ -0,0 +1,102 @@ +# Prove SQLite — Project Plan + +> *The most deployed database in the world. Never formally verified. We're going to fix that.* + +--- + +## Objective + +Specify SQLite's core state machines in SpeckDL — pager, WAL mode, VDBE bytecode engine, and B-Tree — then verify their critical invariants with Z3. Publish findings. This is the sequel to Prove Kafka (docs/PROVE-KAFKA-PLAN.md, now complete). + +--- + +## Why SQLite + +SQLite is the most deployed database engine in the world — every smartphone, every browser, countless embedded systems. Its testing infrastructure (TH3, 100% branch coverage, mutation testing) is among the best in the industry. But coverage is not proof. + +Formal verification of SQLite's core invariants would be a first. Not a theoretical exercise — this is software running on billions of devices. + +--- + +## Phases + +### Phase 1 — SQLite Pager & Journal Modes + +**Target:** Specify and verify the pager state machine, including transaction lifecycle, journal modes, and WAL concurrency. + +| Milestone | Description | Dependencies | Status | +|-----------|-------------|--------------|--------| +| DB.1 | Research doc: pager, WAL, VDBE, B-Tree | None | 🚧 In progress | +| DB.2 | `SQLitePager.speck` | DB.1 | ⬜ | +| DB.3 | Z3 verification of pager invariants | DB.2 | ⬜ | +| DB.4 | `SQLiteWAL.speck` | DB.1 | ⬜ | +| DB.5 | Z3 verification of WAL concurrency | DB.4 | ⬜ | +| DB.6 | Blog post: "Prove SQLite" | DB.3, DB.5 | 🚧 In progress | + +### Phase 2 — SQLite VDBE Bytecode Engine + +**Target:** Specify the VDBE execution model — program counter, registers, key opcodes, transaction integration. + +| Milestone | Description | Dependencies | Status | +|-----------|-------------|--------------|--------| +| DB.7 | `SQLiteVDBE.speck` | DB.1 | ⬜ | +| DB.8 | Z3 verification of VDBE invariants | DB.7 | ⬜ | +| DB.9 | B-Tree cursor integration spec | DB.8 | ⬜ | + +### Phase 3 — B-Tree + +**Target:** Specify the B-Tree structure — page organization, splits, merges, cursor operations. + +| Milestone | Description | Dependencies | Status | +|-----------|-------------|--------------|--------| +| DB.10 | `SQLiteBTree.speck` | DB.7 | ⬜ | +| DB.11 | Z3 verification of B-Tree invariants | DB.10 | ⬜ | +| DB.12 | Synthesis: unified SQLite verification report | DB.3, DB.5, DB.8, DB.11 | ⬜ | + +--- + +## Target Invariants (by layer) + +### Pager Invariants +1. **Transaction atomicity:** pages are either fully written or fully rolled back +2. **Journal integrity:** journal reflects committed state, is cleaned on rollback +3. **Cache consistency:** dirty pages are written back before journal deletion +4. **File format:** page size is consistent across the database file + +### WAL Invariants +1. **Read consistency:** a reader sees a consistent snapshot (no partial WAL writes) +2. **Write serialization:** at most one writer at a time +3. **Checkpoint safety:** checkpoint does not remove frames still needed by active readers +4. **Frame ordering:** WAL frames are committed in sequence, no gaps + +### VDBE Invariants +1. **Program counter validity:** PC stays within instruction bounds +2. **Register type safety:** read register types match write register types +3. **Cursor consistency:** open cursors point to valid B-Tree positions +4. **HALT guarantee:** every program reaches HALT (no infinite loops) + +### B-Tree Invariants +1. **Page organization:** every page has valid header and cell pointers +2. **Key ordering:** keys are sorted within a page and across sibling pages +3. **Balance:** tree depth is uniform across all leaves +4. **Split correctness:** splitting a page preserves key ordering and parent linkage + +--- + +## Deliverables + +- `docs/db-sqlite-reference.md` — research source material +- `examples/SQLitePager.speck` — pager + WAL specification +- `examples/SQLiteVDBE.speck` — VDBE specification +- `examples/SQLiteBTree.speck` — B-Tree specification +- `docs/blog-07-prove-sqlite.md` — blog post +- Z3 verification results (sat/unsat per invariant) +- For any gaps found: documented counterexample traces + +--- + +## Guiding Principle + +Dependencies only. No wall-time estimates. Each milestone lists what must be true before it can start. + +Same approach as Prove Kafka, bigger target.