feat: SQLite WAL concurrency model spec (speckl#36)

examples/SQLiteWAL.speck

@@ -0,0 +1,486 @@
+// SQLite Write-Ahead Log Concurrency Model (speckl#36)
+//
+// Models the WAL mode state machine: three-file system (X.db + X.db-wal + X.db-shm),
+// concurrent readers, single writer, checkpoint protocol, and WAL reset.
+// This is SQLite's most complex concurrency mechanism.
+//
+// Based on: docs/db-sqlite-reference.md Section 2: WAL Mode State Machine
+// Scope: WAL frame lifecycle, reader end-marks, checkpoint isolation, WAL reset
+// Does NOT cover: VDBE opcodes, B-Tree internals, SQL-level semantics
+
+speck SQLiteWAL {
+    author: "Engineering (agent-engineering) <engineering@marcus.local>"
+    source: architecture_review ref "SQLite-WAL-Core"
+    review: hybrid
+    derives from docs/db-sqlite-reference.md via "Section 2: WAL Mode State Machine"
+    satisfies speckl#36
+
+    // === Types ===
+
+    type PageData = Bytes
+    type FrameSeq = Nat
+    type ReaderId = Nat
+    type LockSlot = Nat
+
+    type Frame = {
+        page: Nat,
+        data: PageData,
+        seq: FrameSeq,
+        checksum: Nat,
+        dbSize: Nat,
+        isCommit: Bool
+    }
+
+    type ReaderState = {
+        endMark: FrameSeq,
+        lockSlot: LockSlot,
+        active: Bool
+    }
+
+    type WalIndexHeader = {
+        nBackfill: FrameSeq,
+        nBackfillAttempted: FrameSeq,
+        nFrame: FrameSeq,
+        aReadMark: Array(Nat, 5),
+        salt1: Nat,
+        salt2: Nat,
+        version: Nat
+    }
+
+    type LockType = String  // "READER", "WRITER", "CHECKPOINTER", "NONE"
+
+    // === State ===
+
+    state {
+        // WAL frames indexed by sequence number
+        walFrames: Map(FrameSeq, Frame)
+
+        // Number of valid commit frames in WAL
+        nFrames: FrameSeq
+
+        // Checkpoint backfill progress: frames already copied back to DB
+        checkpointSeq: FrameSeq
+        checkpointAttempted: FrameSeq
+
+        // Active readers with their end marks
+        readers: Map(ReaderId, ReaderState)
+
+        // Writer state
+        writerActive: Bool
+        writerLock: LockType
+
+        // Checkpoint state
+        checkpointActive: Bool
+        checkpointMode: String  // "PASSIVE" | "FULL" | "RESTART" | "TRUNCATE"
+
+        // WAL reset needed flag
+        walResetNeeded: Bool
+
+        // shm file state — WAL-index header
+        walIndex: WalIndexHeader
+
+        // Database page state (simplified: tracks which pages are in DB)
+        dbPages: Map(Nat, PageData)
+
+        // Lock slot tracking: which slot each reader holds
+        readLockSlots: Map(LockSlot, Bool)  // true = slot in use
+
+        // Error state
+        errorState: Bool
+        errCode: Nat
+    }
+
+    init {
+        walFrames == emptyMap
+        nFrames == 0
+        checkpointSeq == 0
+        checkpointAttempted == 0
+        readers == emptyMap
+        writerActive == false
+        writerLock == "NONE"
+        checkpointActive == false
+        checkpointMode == "PASSIVE"
+        walResetNeeded == false
+        walIndex == {
+            nBackfill: 0,
+            nBackfillAttempted: 0,
+            nFrame: 0,
+            aReadMark: [0, 0, 0, 0, 0],
+            salt1: 0,
+            salt2: 0,
+            version: 3007000
+        }
+        dbPages == emptyMap
+        readLockSlots == {0: false, 1: false, 2: false, 3: false, 4: false}
+        errorState == false
+        errCode == 0
+    }
+
+    // === Invariants ===
+
+    // W1: Read Consistency — a reader with end-mark M sees exactly the database
+    // state as of the last commit frame ≤ M. No partial WAL writes visible.
+    invariant ReadConsistency {
+        forall r in readers.keys:
+            readers[r].active == true implies
+                readers[r].endMark <= nFrames
+    }
+
+    // W2: Write Serialization — at most one writer at a time
+    invariant WriteSerialization {
+        writerActive == true implies checkpointActive == false
+    }
+
+    // W3: Checkpoint Safety — checkpoint does not remove frames still needed
+    // by active readers. nBackfill ≤ min(active reader end marks)
+    invariant CheckpointSafety {
+        forall r in readers.keys:
+            readers[r].active == true implies checkpointSeq <= readers[r].endMark
+    }
+
+    // W4: Frame Ordering — WAL frames are committed in sequence, no gaps.
+    // nFrames is monotonic (non-decreasing except during WAL reset).
+    invariant FrameOrdering {
+        // All committed frames have sequence numbers 1..nFrames
+        forall s in walFrames.keys:
+            s >= 1 and s <= nFrames
+    }
+
+    // W5: Snapshot Integrity — no WAL frame visible to a reader is overwritten
+    // until that reader completes
+    invariant SnapshotIntegrity {
+        forall r in readers.keys:
+            forall s in walFrames.keys:
+                readers[r].active == true and s <= readers[r].endMark implies
+                    s in walFrames.keys
+    }
+
+    // W6: WAL Reset Condition — WAL reset only happens when no reader is on
+    // an old snapshot (all readers must be on the newest frames or no active readers)
+    invariant WalResetCondition {
+        walIndex.nFrame == 0 implies
+            (forall r in readers.keys: readers[r].active == false)
+    }
+
+    // W7: Lock Deadlock Free — the lock protocol (READER/CHECKPOINTER/WRITER)
+    // doesn't deadlock: writer and checkpointer are never simultaneously active
+    invariant LockDeadlockFree {
+        writerActive == true implies checkpointActive == false
+        checkpointActive == true implies writerActive == false
+    }
+
+    // W8: Commit Durability — committed frames persist; if a frame has isCommit
+    // set, it remains in the WAL until properly checkpointed
+    invariant CommitDurability {
+        forall s in walFrames.keys:
+            walFrames[s].isCommit == true and s > checkpointSeq implies
+                s in walFrames.keys
+    }
+
+    // W9: Backfill Bound — checkpoint never backfills past the oldest active
+    // reader's end mark
+    invariant BackfillBound {
+        checkpointAttempted <= checkpointSeq or
+        checkpointAttempted <= nFrames
+    }
+
+    // W10: Three-File Consistency — the three files (wal, shm, db) are mutually
+    // consistent. walIndex.nFrame matches nFrames. walIndex.nBackfill matches checkpointSeq.
+    invariant ThreeFileConsistency {
+        walIndex.nFrame == nFrames and
+        walIndex.nBackfill == checkpointSeq
+    }
+
+    // === Actions ===
+
+    // Action 1: BeginRead — reader establishes snapshot at given startFrame
+    action BeginRead(startFrame: FrameSeq, readerId: ReaderId) {
+        require errorState == false
+        require readerId notIn readers.keys
+        require startFrame <= nFrames
+
+        // Find an available lock slot (0-4)
+        let slot := 0
+        require exists s in [0..4]: readLockSlots[s] == false
+
+        // Acquire a read lock slot
+        readLockSlots[slot] := true
+
+        // Register the reader with its end mark (snapshot point)
+        readers[readerId] := {
+            endMark: startFrame,
+            lockSlot: slot,
+            active: true
+        }
+
+        // Update walIndex read marks
+        walIndex.aReadMark[slot] := startFrame
+
+        emit ReadStarted { readerId: readerId, endMark: startFrame, lockSlot: slot }
+    }
+
+    // Action 2: ReadFrame — reader reads a page from WAL or DB
+    action ReadFrame(readerId: ReaderId, pageId: Nat) {
+        require errorState == false
+        require readerId in readers.keys
+        require readers[readerId].active == true
+
+        let readerMark := readers[readerId].endMark
+
+        // FindFrame(P, end_mark): find the latest frame for pageId with seq ≤ readerMark
+        // If found in WAL: read from WAL frame. If not: read from DB.
+        // (Reading is nondestructive — just verifies the frame exists)
+
+        emit FrameRead {
+            readerId: readerId,
+            pageId: pageId,
+            endMark: readerMark
+        }
+    }
+
+    // Action 3: EndRead — reader releases its end mark and lock slot
+    action EndRead(readerId: ReaderId) {
+        require readerId in readers.keys
+        require readers[readerId].active == true
+
+        let slot := readers[readerId].lockSlot
+
+        // Release the reader's lock slot
+        readers[readerId].active := false
+        readLockSlots[slot] := false
+
+        // Update walIndex read marks for this slot
+        walIndex.aReadMark[slot] := 0
+
+        emit ReadEnded { readerId: readerId, lockSlot: slot }
+    }
+
+    // Action 4: BeginWrite — writer starts (requires no active checkpoint)
+    action BeginWrite() {
+        require errorState == false
+        require writerActive == false
+        require checkpointActive == false
+
+        // Acquire WAL_WRITE_LOCK exclusively
+        writerActive := true
+        writerLock := "WRITER"
+
+        emit WriteStarted { startFrame: nFrames }
+    }
+
+    // Action 5: AppendFrame — writer appends a frame to the WAL
+    action AppendFrame(pageId: Nat, data: PageData, checksum: Nat, dbSize: Nat, isCommit: Bool) {
+        require errorState == false
+        require writerActive == true
+        require writerLock == "WRITER"
+
+        // Create new frame at next sequence number
+        let nextSeq := nFrames + 1
+
+        let frame: Frame := {
+            page: pageId,
+            data: data,
+            seq: nextSeq,
+            checksum: checksum,
+            dbSize: dbSize,
+            isCommit: isCommit
+        }
+
+        // Append to WAL
+        walFrames[nextSeq] := frame
+        nFrames := nextSeq
+
+        // Update walIndex
+        walIndex.nFrame := nFrames
+
+        emit FrameAppended { seq: nextSeq, pageId: pageId, isCommit: isCommit }
+    }
+
+    // Action 6: CommitWrite — writer commits its frames
+    action CommitWrite() {
+        require errorState == false
+        require writerActive == true
+        require writerLock == "WRITER"
+
+        // The last frame appended should be a commit frame
+        let lastFrame := walFrames[nFrames]
+        require lastFrame.isCommit == true
+
+        // Release WAL_WRITE_LOCK
+        writerActive := false
+        writerLock := "NONE"
+
+        emit WriteCommitted { commitSeq: nFrames }
+    }
+
+    // Action 7: BeginCheckpoint — start checkpoint process
+    action BeginCheckpoint(mode: String) {
+        require errorState == false
+        require checkpointActive == false
+        require writerActive == false
+        require mode == "PASSIVE" or mode == "FULL" or mode == "RESTART" or mode == "TRUNCATE"
+
+        // Acquire WAL_CKPT_LOCK
+        checkpointActive := true
+        checkpointMode := mode
+
+        emit CheckpointStarted { mode: mode, fromFrame: checkpointSeq }
+    }
+
+    // Action 8: MoveFrame — checkpoint moves a frame from WAL to DB
+    action MoveFrame(frameId: FrameSeq) {
+        require errorState == false
+        require checkpointActive == true
+        require frameId in walFrames.keys
+        require frameId > checkpointSeq
+
+        // Must respect active readers: don't move frames past the oldest reader
+        forall r in readers.keys:
+            readers[r].active == true implies frameId <= readers[r].endMark
+
+        // Copy frame data to database
+        let frame := walFrames[frameId]
+        dbPages[frame.page] := frame.data
+
+        // Advance checkpoint progress
+        checkpointSeq := frameId
+        walIndex.nBackfill := checkpointSeq
+
+        // Track attempted backfill
+        if frameId > checkpointAttempted {
+            checkpointAttempted := frameId
+            walIndex.nBackfillAttempted := checkpointAttempted
+        }
+
+        emit FrameMoved { seq: frameId, pageId: frame.page }
+    }
+
+    // Action 9: FinishCheckpoint — complete checkpoint
+    action FinishCheckpoint() {
+        require checkpointActive == true
+
+        // For RESTART/TRUNCATE mode, must ensure all frames are backfilled
+        if checkpointMode == "RESTART" or checkpointMode == "TRUNCATE" {
+            require checkpointSeq == nFrames
+        }
+
+        // Release WAL_CKPT_LOCK
+        checkpointActive := false
+
+        // If all frames are backfilled and no active readers, mark reset as possible
+        if checkpointSeq == nFrames {
+            walResetNeeded := true
+        }
+
+        emit CheckpointFinished { backfilledTo: checkpointSeq, mode: checkpointMode }
+    }
+
+    // Action 10: ResetWAL — reset WAL file (requires all readers on newest snapshot)
+    action ResetWAL() {
+        require errorState == false
+        require writerActive == false
+        require checkpointActive == false
+        require walResetNeeded == true
+
+        // All frames must be backfilled
+        require checkpointSeq == nFrames
+
+        // No reader must hold any lock slot with a non-zero end mark
+        forall r in readers.keys:
+            readers[r].active == true implies readers[r].endMark == nFrames
+
+        // Check that no reader lock slots are held (WAL_READ_LOCK for N>0)
+        forall slot in [0..4]:
+            readLockSlots[slot] == false
+
+        // Reset WAL: clear frames, rewind nFrames
+        walFrames := emptyMap
+        nFrames := 0
+        checkpointSeq := 0
+        checkpointAttempted := 0
+        walResetNeeded := false
+
+        // Reset walIndex
+        walIndex.nFrame := 0
+        walIndex.nBackfill := 0
+        walIndex.nBackfillAttempted := 0
+        walIndex.aReadMark := [0, 0, 0, 0, 0]
+
+        emit WalReset {}
+    }
+
+    // Action 11: ErrorInjection — model I/O error occurring during WAL operations
+    action InjectError(errorCode: Nat) {
+        require errorState == false
+
+        errorState := true
+        errCode := errorCode
+
+        // Abort any active operations
+        writerActive := false
+        writerLock := "NONE"
+        checkpointActive := false
+
+        emit ErrorOccurred { errCode: errorCode }
+    }
+
+    // Action 12: RecoverFromError — reset to clean state after error
+    action RecoverFromError() {
+        require errorState == true
+
+        errorState := false
+        errCode := 0
+
+        emit ErrorRecovered {}
+    }
+
+    // === Transition Relation ===
+
+    next:
+        BeginRead
+        | ReadFrame
+        | EndRead
+        | BeginWrite
+        | AppendFrame
+        | CommitWrite
+        | BeginCheckpoint
+        | MoveFrame
+        | FinishCheckpoint
+        | ResetWAL
+        | InjectError
+        | RecoverFromError
+
+    // === Bounded Model Checking ===
+
+    verify Always(ReadConsistency) {
+        depth 10
+    }
+
+    verify Always(WriteSerialization) {
+        depth 5
+    }
+
+    verify Always(CheckpointSafety) {
+        depth 10
+    }
+
+    verify Always(WalResetCondition) {
+        depth 5
+    }
+
+    verify Always(CommitDurability) {
+        depth 10
+    }
+
+    verify Always(FrameOrdering) {
+        depth 8
+    }
+
+    verify Always(LockDeadlockFree) {
+        depth 5
+    }
+
+    verify Always(ThreeFileConsistency) {
+        depth 8
+    }
+}