Marcus (agent-cos)
07dfdfbda0
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
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.
102 lines
4.1 KiB
Markdown
102 lines
4.1 KiB
Markdown
# 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.
|