diff --git a/sw-block/design/v3-recovery-inv-test-map.md b/sw-block/design/v3-recovery-inv-test-map.md index e0b041396..bcafcba83 100644 --- a/sw-block/design/v3-recovery-inv-test-map.md +++ b/sw-block/design/v3-recovery-inv-test-map.md @@ -24,6 +24,7 @@ Status legend: | `INV-DUAL-LANE-WAL-WINS-BASE` | Same LBA: once WAL lane has applied (`bitmap.MarkApplied`), base lane MUST skip subsequent base blocks for that LBA. Symmetric: base-then-WAL → WAL data overwrites via substrate's last-writer-wins LSN ordering. | `TestRebuildSession_WALWinsThenBaseSkips` (`core/recovery/rebuild_session_test.go:29`)
`TestRebuildSession_BaseFirstThenWALOverwrites` (`core/recovery/rebuild_session_test.go:54`) | ✅ pinned both directions | | `INV-SESSION-COMPLETE-ON-CONJUNCTION-LAYER1` | `TryComplete` returns `done=true` iff `baseDone ∧ walApplied ≥ targetLSN`. Latched: subsequent calls return `done=true` without state change. NOT including barrier-ack — that is layer-2's system-level confirmation. | `TestRebuildSession_TryComplete_Conjunction` (`core/recovery/rebuild_session_test.go:74`)
`TestRebuildSession_TryComplete_LatchesCompleted` (`core/recovery/rebuild_session_test.go:108`) | ✅ pinned (3 negative + 1 positive + latch) | | `INV-BITMAP-NO-INDEPENDENT-LOCK` | `RebuildBitmap` exposes no synchronization; callers (`RebuildSession`) serialize access via session mutex. | `TestRebuildSession_ConcurrentLanes` (`core/recovery/rebuild_session_test.go:130`) | ✅ stress test (4 base + 4 WAL goroutines × 1024 LBAs); needs `-race` on Linux for full proof | +| `INV-WAL-CURSOR-MONOTONIC-FROM-PINLSN` | Sender's WAL pump rewinds cursor to `fromLSN` once at session start; cursor advances monotonically per `ScanLBAs` callback; never decreases. Receiver enforces matching wire-level monotonic discipline (4-case per `v3-recovery-unified-wal-stream-kickoff.md` v0.3 §5.1: `==applied+1` apply / `>applied+1` gap → `FailureContract` / `==applied` exact-duplicate → `FailureProtocol` / `Receiver 4-case discipline: `TestReceiver_RejectsBackwardLSN_InSession`, `TestReceiver_RejectsGap_InSession`, `TestReceiver_RejectsExactDuplicate_InSession` (same file). | ✅ pinned (sender pump + receiver 4-case discipline; added in g7-redo/unified-wal-impl §3.2 #3 milestone) | ---