sw-block/design: v3-recovery-inv-test-map — INV-WAL-CURSOR-MONOTONIC-FROM-PINLSN

Adds the new invariant pin row for §3.2 #3 unified WAL stream / cursor-
rewind. Companion to the seaweed_block g7-redo/unified-wal-impl branch
(checkpoint 3/N at commit 0550e44) which adds the 7 new tests cited.

Row content:
  Definition: sender 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 kickoff v0.3 §5.1: ==applied+1 apply /
  >applied+1 gap → FailureContract / ==applied exact-duplicate →
  FailureProtocol / <applied backward → FailureProtocol).
  Tests pinned (7):
    TestSender_PumpHappyPath_OnMemoryWAL
    TestSender_LiveWritesDuringSession_OnMemoryWAL
    TestSender_KindByte_FlipsOnceAtCatchUp
    TestSender_StreamUntilHead_CtxCancel
    TestReceiver_RejectsBackwardLSN_InSession
    TestReceiver_RejectsGap_InSession
    TestReceiver_RejectsExactDuplicate_InSession
  Status:  pinned.
This commit is contained in:
pingqiu
2026-04-29 17:48:18 -07:00
parent 04b9d1ea53
commit 759d50ba5d

View File

@@ -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`)<br>`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`)<br>`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` / `<applied` backward → `FailureProtocol`). The only legitimate "rewind" is session-level `cursor:=pinLSN` at a NEW SessionStart, never in-stream. | Sender pump (memorywal substrate): `TestSender_PumpHappyPath_OnMemoryWAL`, `TestSender_LiveWritesDuringSession_OnMemoryWAL`, `TestSender_KindByte_FlipsOnceAtCatchUp`, `TestSender_StreamUntilHead_CtxCancel` (`core/recovery/unified_wal_test.go`).<br>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) |
---