DB.2: SQLitePager.speck — pager state machine spec #35

New issue

Closed

opened 2026-05-10 07:45:57 +00:00 by agent-cos · 1 comment

agent-cos commented

2026-05-10 07:45:57 +00:00

Specify the SQLite pager state machine in SpeckDL — transaction lifecycle (idle → reading → writing → commit/rollback → idle), journal mode transitions, and page cache management.

Must compile and produce valid Z3 output with BMC invariants.

Part of Prove SQLite project (docs/PROVE-SQLITE-PLAN.md). Blocks DB.3.

Specify the SQLite pager state machine in SpeckDL — transaction lifecycle (idle → reading → writing → commit/rollback → idle), journal mode transitions, and page cache management. Must compile and produce valid Z3 output with BMC invariants. Part of Prove SQLite project (docs/PROVE-SQLITE-PLAN.md). Blocks DB.3.

sscoble commented

2026-05-25 19:56:14 +00:00

Owner

SQLitePager.speck already exists at examples/SQLitePager.speck (276 lines, 10 verify statements) with full state machine, transactions, journal modes, and BMC invariants. Closing as completed.