From 759d50ba5ddb4fc28f64470e0a3e2a19c8babcf6 Mon Sep 17 00:00:00 2001
From: pingqiu <pingqiu@gmail.com>
Date: Wed, 29 Apr 2026 17:48:18 -0700
Subject: [PATCH] =?UTF-8?q?sw-block/design:=20v3-recovery-inv-test-map=20?=
 =?UTF-8?q?=E2=80=94=20INV-WAL-CURSOR-MONOTONIC-FROM-PINLSN?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 sw-block/design/v3-recovery-inv-test-map.md | 1 +
 1 file changed, 1 insertion(+)

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`)<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) |
 
 ---