From 75d18e676f465cac0f119b11e7dba8d710a2f3ac Mon Sep 17 00:00:00 2001 From: pingqiu Date: Sun, 26 Apr 2026 00:24:23 -0700 Subject: [PATCH] T4d batch close: catalogue invariant upgrades + checklist v0.3 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Catalogue §3.3 — 12 T4d invariants flipped from ⏭ to ✓ PORTED with specific commit hashes; 4 round-47/48 invariants newly inscribed: Pre-existing flipped to ✓ PORTED: - INV-REPL-NO-PER-LBA-DATA-REGRESSION → bd2de99 + 01f4ab9 - INV-REPL-RECOVERY-STALE-ENTRY-SKIP-PER-LBA → bd2de99 - INV-REPL-RECOVERY-COVERAGE-ADVANCES-ON-SKIP → bd2de99 - INV-REPL-LIVE-LANE-STALE-FAILS-LOUD → bd2de99 - INV-REPL-RECOVERY-COVERAGE-RESTART-SAFE → bd2de99 - INV-REPL-LANE-DERIVED-FROM-HANDLER-CONTEXT → 01f4ab9 + 44c60dd (with named carry CARRY-T4D-LANE-CONTEXT-001 to post-G5) - INV-REPL-TRANSPORT-STORAGE-CONTRACT-ONLY → 44c60dd + 1edeb36 - INV-REPL-CATCHUP-FROMLSN-IS-REPLICA-FLUSHED-PLUS-1 → 44c60dd - INV-REPL-CATCHUP-FROMLSN-FROM-ENGINE-STATE-NOT-PROBE → 44c60dd Newly inscribed (round-47 + round-48 architect additions): - INV-REPL-CATCHUP-EXHAUSTION-ESCALATES-TO-REBUILD → 812d3fa + e642ae8 - INV-REPL-REBUILD-FAILURE-TERMINAL → 812d3fa - INV-REPL-FAILED-SESSION-KIND-DRIVES-ESCALATION (part C bug #1) → e642ae8 - INV-REPL-REBUILD-ESCALATION-STICKY-UNTIL-TERMINAL (part C bug #2) → e642ae8 Forward-carry checklist v0.3: - All per-batch focus rows resolved - m01 -race verified across all T4d batches including T2A NVMe race fix - Status transitions from "active gating" to "G5-baseline" Co-Authored-By: Claude Opus 4.7 (1M context) --- .../design/v2-v3-contract-bridge-catalogue.md | 27 ++++++++++++------- ...v3-phase-15-t4d-forward-carry-checklist.md | 7 ++--- 2 files changed, 22 insertions(+), 12 deletions(-) diff --git a/sw-block/design/v2-v3-contract-bridge-catalogue.md b/sw-block/design/v2-v3-contract-bridge-catalogue.md index 26bc9213e..33aeab5a2 100644 --- a/sw-block/design/v2-v3-contract-bridge-catalogue.md +++ b/sw-block/design/v2-v3-contract-bridge-catalogue.md @@ -712,19 +712,28 @@ Each row carries V2 attributes (from L1 survey) + V3 home + per-contract verdict | INV-REPL-FENCE-EPOCH-EQ | Replica drops WAL entries with `entry.Epoch != currentEpoch` silently | §3.2.1 C1 + §3.2.3 C3 | ⊙ coding T4a-2 + T4c | | INV-REPL-CATCHUP-WITHIN-RETENTION-001 *(Path A only)* | Reconnect within retained WAL window catches up via delta; `ErrWALRecycled` escalates to rebuild | Sketch §6.1 B Path A | **⏭ T4d (downgraded from T4c per closure §B delta #4)** — un-pinned at T4c because catch-up sender hardcodes `ScanLBAs(1)` not R+1; spurious-rebuild risk under checkpoint-past-1 + replica-within-retention. T4d-2 (apply gate) + T4d-3 (R+1 threading) co-pin | | INV-REPL-CATCHUP-FULL-TRANSFER-001 *(Path B only)* | Reconnect after any disconnect catches up via full-state transfer of `AllBlocks()`; retention-window deferred to P10 | Sketch §6.1 B Path B | NOT ACTIVE — Path A signed by architect | -| **INV-REPL-NO-PER-LBA-DATA-REGRESSION** *(round-43 lock, GOAL-LEVEL)* | Per-LBA data on a replica MUST NOT regress under any apply path (live, recovery, retry, replica restart mid-recovery). Frontier monotonicity (walHead/nextLSN/R/H) is necessary but not sufficient — `BlockStore.ApplyEntry` regressed walHead AND blindly overwrote LBA bytes on older-LSN apply pre-`f6084ee`. The mechanism invariants below (STALE-ENTRY-SKIP-PER-LBA + COVERAGE-ADVANCES-ON-SKIP + LIVE-LANE-STALE-FAILS-LOUD + RESTART-SAFE) collectively make this hold | Round-43 architect lock | ⏭ T4d-2 | -| **INV-REPL-RECOVERY-STALE-ENTRY-SKIP-PER-LBA** *(round-43 lock, MECHANISM)* | Replica must skip recovery-stream entry data writes when `entry.LSN <= appliedLSN[LBA]`. Apply only if strictly newer; on apply, update `appliedLSN[LBA] = entry.LSN`. Substrate fixes are defense-in-depth; the replica recovery apply gate (T4d-2) is authoritative | Round-43 architect lock | ⏭ T4d-2 | -| **INV-REPL-RECOVERY-COVERAGE-ADVANCES-ON-SKIP** *(round-44 refinement)* | Skipped recovery entries (data-skip per stale-LSN check) MUST still update `recoveryCovered[LBA]=true`. Skip data ≠ ignore frame: completion accounting depends on every LBA in the recovery window being marked processed. Architect text: "Recovery-stream stale entries are valid duplicates and must be skipped as data writes while still counted as recovery-stream coverage." | Round-44 architect refinement | ⏭ T4d-2 | -| **INV-REPL-LIVE-LANE-STALE-FAILS-LOUD** *(round-44 refinement)* | Live-lane stale entries (received `MsgShipEntry` on the live handler with `LSN <= appliedLSN[LBA]`) are abnormal — repeat packet, stale session, lineage error, or retry on wrong lane. They MUST NOT mutate data, MUST be skipped/rejected with diagnostic surfacing, and MUST NOT advance `recoveryCovered[LBA]`. Distinct from the recovery-lane stale-skip, which is normal | Round-44 architect refinement | ⏭ T4d-2 | -| **INV-REPL-RECOVERY-COVERAGE-RESTART-SAFE** *(Option C hybrid lock)* | Replica restart mid-recovery MUST NOT regress per-LBA data. Apply gate seeds `appliedLSN[LBA]` from substrate query at session start (Option C hybrid: substrate-native truth where available, in-memory session map updated thereafter). Re-shipped recovery window after restart correctly skips entries already applied pre-restart | Architect §2.5 #1 ratification (Option C) | ⏭ T4d-2 | -| **INV-REPL-LANE-DERIVED-FROM-HANDLER-CONTEXT** *(§9 architect Q2 lock; round-46 architect re-emphasis)* | `MsgShipEntry` lane is derived from the **accepting handler/session context** in T4d. **NOT from payload-derived signals like `lineage.TargetLSN` sentinels.** Live handlers MUST NOT execute recovery stale-skip/coverage logic; recovery handlers MUST NOT bypass it. Apply gate hook MUST expose lane-explicit methods (e.g. `ApplyLive(...)` + `ApplyRecovery(...)`, or `Apply(..., lane ApplyLane)`) — caller supplies lane from connection/session context. A test must fail if a recovery entry reaches the live path or a live entry reaches the recovery accounting path. Regression `TestApplyGate_RecoveryWithTargetLSN1_RoutesToRecoveryLane` pins the edge case where TargetLSN=1 (sentinel-collision-with-live) MUST still route via handler-context to recovery. Explicit lane wire-tag deferred to post-G5 protocol-hardening if handler-context discipline becomes fragile. **Round-46 history**: T4d-2 `bd2de99` initial implementation drifted to payload-derived discrimination via `lineage.TargetLSN > 1` sentinel; QA T4d-2 review surfaced the edge case (recovery with H=1 misroutes); architect reaffirmed handler-context as the correct rule + bound T4d-2 follow-up rework as HARD GATE before T4d-3 | §9 architect Q2 + round-46 architect re-emphasis | ⏭ T4d-2 follow-up (REWORK GATE) → T4d-3 | -| **INV-REPL-TRANSPORT-STORAGE-CONTRACT-ONLY** *(§9 architect Q1+Q3 lock; T4d-1 strengthened)* | `core/transport` may depend on `core/storage` recovery-contract symbols only (`LogicalStorage`, `RecoveryEntry`, `ErrWALRecycled` / structured replacement, `RecoveryMode`), never substrate internals (`core/storage/walstore`, `core/storage/smartwal`). Engine retry loop lives in `core/engine` (Q1 Option α); package move to `core/recovery` deferred per Q3. Lane-aware apply decisions go through the T4d-2 apply gate interface, not via direct substrate queries from transport. **T4d-1 strengthening (architect-endorsed 2026-04-25)**: 2-enum split inscribed — `storage.StorageRecoveryFailureKind` is substrate classification; `engine.RecoveryFailureKind` is engine decision vocabulary; `transport.classifyRecoveryFailure` is the explicit boundary mapper. `core/engine` MUST NOT import `core/storage` at all (stricter than Q1+Q3 baseline; verified at `1edeb36` build). | §9 architect Q1+Q3 + T4d-1 architect endorsement | ⏭ T4d-3 (transport fence); ⊙ T4d-1 (engine-purity verified) | -| **INV-REPL-CATCHUP-FROMLSN-IS-REPLICA-FLUSHED-PLUS-1** *(T4d-3 G-1 §5 hidden invariant)* | Engine emits `StartCatchUp.FromLSN = Recovery.R + 1`. Sender does NOT add `+1` (avoids double-add). The "+1 to skip already-applied LSN" semantic lives at the engine command-emit site, not transport. Surfaced at G-1 §6.1 placement decision; QA-ratified Option A (engine adds +1) | T4d-3 G-1 §5 (architect Q1 derivation) | ⏭ T4d-3 | -| **INV-REPL-CATCHUP-FROMLSN-FROM-ENGINE-STATE-NOT-PROBE** *(T4d-3 G-1 §5 hidden invariant)* | Engine populates `StartCatchUp.FromLSN` from its **own** `Recovery.R` state (the single source of truth). Probe results are ingested as facts that update engine state; the command emit path reads the updated state, never the raw probe payload directly. Pins the race window: probe → recovery decision → command emit always goes through engine state, no shortcut. Positive-form per QA nit; predecessor name `INV-REPL-CATCHUP-FROMLSN-NOT-FROM-PROBE-DIRECTLY` retained in G-1 history only | T4d-3 G-1 §5 (architect Q1 derivation) | ⏭ T4d-3 | +| **INV-REPL-NO-PER-LBA-DATA-REGRESSION** *(round-43 lock, GOAL-LEVEL)* | Per-LBA data on a replica MUST NOT regress under any apply path (live, recovery, retry, replica restart mid-recovery). Frontier monotonicity (walHead/nextLSN/R/H) is necessary but not sufficient — `BlockStore.ApplyEntry` regressed walHead AND blindly overwrote LBA bytes on older-LSN apply pre-`f6084ee`. The mechanism invariants below (STALE-ENTRY-SKIP-PER-LBA + COVERAGE-ADVANCES-ON-SKIP + LIVE-LANE-STALE-FAILS-LOUD + RESTART-SAFE) collectively make this hold | Round-43 architect lock | ✓ PORTED T4d-2 (`seaweed_block@bd2de99` + `01f4ab9`); apply gate enforces; m01 -race verified | +| **INV-REPL-RECOVERY-STALE-ENTRY-SKIP-PER-LBA** *(round-43 lock, MECHANISM)* | Replica must skip recovery-stream entry data writes when `entry.LSN <= appliedLSN[LBA]`. Apply only if strictly newer; on apply, update `appliedLSN[LBA] = entry.LSN`. Substrate fixes are defense-in-depth; the replica recovery apply gate (T4d-2) is authoritative | Round-43 architect lock | ✓ PORTED T4d-2 (`seaweed_block@bd2de99` `apply_gate.go ApplyRecovery`) | +| **INV-REPL-RECOVERY-COVERAGE-ADVANCES-ON-SKIP** *(round-44 refinement)* | Skipped recovery entries (data-skip per stale-LSN check) MUST still update `recoveryCovered[LBA]=true`. Skip data ≠ ignore frame: completion accounting depends on every LBA in the recovery window being marked processed. Architect text: "Recovery-stream stale entries are valid duplicates and must be skipped as data writes while still counted as recovery-stream coverage." | Round-44 architect refinement | ✓ PORTED T4d-2 (`seaweed_block@bd2de99`) | +| **INV-REPL-LIVE-LANE-STALE-FAILS-LOUD** *(round-44 refinement)* | Live-lane stale entries (received `MsgShipEntry` on the live handler with `LSN <= appliedLSN[LBA]`) are abnormal — repeat packet, stale session, lineage error, or retry on wrong lane. They MUST NOT mutate data, MUST be skipped/rejected with diagnostic surfacing, and MUST NOT advance `recoveryCovered[LBA]`. Distinct from the recovery-lane stale-skip, which is normal | Round-44 architect refinement | ✓ PORTED T4d-2 (`seaweed_block@bd2de99` `apply_gate.go ApplyLive`) | +| **INV-REPL-RECOVERY-COVERAGE-RESTART-SAFE** *(Option C hybrid lock)* | Replica restart mid-recovery MUST NOT regress per-LBA data. Apply gate seeds `appliedLSN[LBA]` from substrate query at session start (Option C hybrid: substrate-native truth where available, in-memory session map updated thereafter). Re-shipped recovery window after restart correctly skips entries already applied pre-restart | Architect §2.5 #1 ratification (Option C) | ✓ PORTED T4d-2 (`seaweed_block@bd2de99` `apply_gate.go initSessionLocked`) | +| **INV-REPL-LANE-DERIVED-FROM-HANDLER-CONTEXT** *(§9 architect Q2 lock; round-46 architect re-emphasis)* | `MsgShipEntry` lane is derived from the **accepting handler/session context** in T4d. **NOT from payload-derived signals like `lineage.TargetLSN` sentinels.** Live handlers MUST NOT execute recovery stale-skip/coverage logic; recovery handlers MUST NOT bypass it. Apply gate hook MUST expose lane-explicit methods (e.g. `ApplyLive(...)` + `ApplyRecovery(...)`, or `Apply(..., lane ApplyLane)`) — caller supplies lane from connection/session context. A test must fail if a recovery entry reaches the live path or a live entry reaches the recovery accounting path. Regression `TestApplyGate_RecoveryWithTargetLSN1_RoutesToRecoveryLane` pins the edge case where TargetLSN=1 (sentinel-collision-with-live) MUST still route via handler-context to recovery. Explicit lane wire-tag deferred to post-G5 protocol-hardening if handler-context discipline becomes fragile. **Round-46 history**: T4d-2 `bd2de99` initial implementation drifted to payload-derived discrimination via `lineage.TargetLSN > 1` sentinel; QA T4d-2 review surfaced the edge case (recovery with H=1 misroutes); architect reaffirmed handler-context as the correct rule + bound T4d-2 follow-up rework as HARD GATE before T4d-3 | §9 architect Q2 + round-46 architect re-emphasis | ✓ PORTED T4d-2 follow-up (`seaweed_block@01f4ab9` lane-pure rework) → ✓ PORTED T4d-3 (`seaweed_block@44c60dd` transport caller-side discipline + transitional shim under named carry CARRY-T4D-LANE-CONTEXT-001) | +| **INV-REPL-TRANSPORT-STORAGE-CONTRACT-ONLY** *(§9 architect Q1+Q3 lock; T4d-1 strengthened)* | `core/transport` may depend on `core/storage` recovery-contract symbols only (`LogicalStorage`, `RecoveryEntry`, `ErrWALRecycled` / structured replacement, `RecoveryMode`), never substrate internals (`core/storage/walstore`, `core/storage/smartwal`). Engine retry loop lives in `core/engine` (Q1 Option α); package move to `core/recovery` deferred per Q3. Lane-aware apply decisions go through the T4d-2 apply gate interface, not via direct substrate queries from transport. **T4d-1 strengthening (architect-endorsed 2026-04-25)**: 2-enum split inscribed — `storage.StorageRecoveryFailureKind` is substrate classification; `engine.RecoveryFailureKind` is engine decision vocabulary; `transport.classifyRecoveryFailure` is the explicit boundary mapper. `core/engine` MUST NOT import `core/storage` at all (stricter than Q1+Q3 baseline; verified at `1edeb36` build). | §9 architect Q1+Q3 + T4d-1 architect endorsement | ✓ PORTED T4d-3 (`seaweed_block@44c60dd` `core/transport/import_discipline_test.go` source-grep fence); ✓ PORTED T4d-1 (`seaweed_block@1edeb36` engine-purity verified by build — engine has zero core/storage imports) | +| **INV-REPL-CATCHUP-FROMLSN-IS-REPLICA-FLUSHED-PLUS-1** *(T4d-3 G-1 §5 hidden invariant)* | Engine emits `StartCatchUp.FromLSN = Recovery.R + 1`. Sender does NOT add `+1` (avoids double-add). The "+1 to skip already-applied LSN" semantic lives at the engine command-emit site, not transport. Surfaced at G-1 §6.1 placement decision; QA-ratified Option A (engine adds +1) | T4d-3 G-1 §5 (architect Q1 derivation) | ✓ PORTED T4d-3 (`seaweed_block@44c60dd` `core/engine/apply.go` engine emit + `t4d3_rplus1_test.go` pin tests) | +| **INV-REPL-CATCHUP-FROMLSN-FROM-ENGINE-STATE-NOT-PROBE** *(T4d-3 G-1 §5 hidden invariant)* | Engine populates `StartCatchUp.FromLSN` from its **own** `Recovery.R` state (the single source of truth). Probe results are ingested as facts that update engine state; the command emit path reads the updated state, never the raw probe payload directly. Pins the race window: probe → recovery decision → command emit always goes through engine state, no shortcut. Positive-form per QA nit; predecessor name `INV-REPL-CATCHUP-FROMLSN-NOT-FROM-PROBE-DIRECTLY` retained in G-1 history only | T4d-3 G-1 §5 (architect Q1 derivation) | ✓ PORTED T4d-3 (`seaweed_block@44c60dd` `core/engine/apply.go` engine emit + `t4d3_rplus1_test.go` pin tests) | | **CARRY-T4D-LANE-CONTEXT-001** *(named carry — round-46+ architect)* | **NOT AN INVARIANT — A NAMED CARRY.** T4d-2 follow-up `01f4ab9` made the apply gate lane-pure (correct architectural fence: gate ≠ payload-sniffer) but moved the lane-discrimination payload sniffing one layer up to `core/transport/replica.go:13-18,156-165` as a TRANSITIONAL CALLER-SIDE SHIM — replica handler reads `lineage.TargetLSN==liveShipTargetLSN(=1)` to dispatch to gate's `ApplyLive` vs `ApplyRecovery`. Edge case: recovery session with H=1 (primary has exactly 1 entry, replica empty) ships with `TargetLSN=1` and misroutes to live-lane via the shim → fail-loud fires incorrectly. **Bound resolution**: replace the TargetLSN==1 caller shim with true handler/session context lane signal (per-conn lane tag at handshake / separate handlers / distinct ports — implementation choice). **Owner**: sw. **Bind point**: T4e (preferred) or post-G5 protocol-hardening (latest). **T4d-3 close gate**: T4d-3 MUST do exactly one of (A) land the fix and remove the shim, or (B) add explicit failing/skip-marked L2 test `TestT4d3_RecoveryTargetLSN1_KnownGap` documenting H=1 as known gap with godoc citing this carry id. Architect explicit prohibition: NO engine precondition `TargetLSN >= 2`. | T4d-2 follow-up review round-46+ architect direction | ⏳ CARRY (active) — T4d-3 close evidence cites; resolution at T4e or post-G5 | Exactly one of `INV-REPL-CATCHUP-{WITHIN-RETENTION,FULL-TRANSFER}` queues ACTIVE per architect Item B choice (Path A signed; WITHIN-RETENTION active, FULL-TRANSFER not). +**T4d-4 invariants** (round-47 + round-48 architect additions, inscribed at T4d batch close): + +| Invariant | Statement | Origin | Status | +|---|---|---|---| +| **INV-REPL-CATCHUP-EXHAUSTION-ESCALATES-TO-REBUILD** *(round-47 architect addition)* | When catch-up retry budget is exhausted (`MaxRetries` reached on consecutive non-recycle failures), engine MUST directly emit a `StartRebuild` command. Pre-round-47: cleared `Decision` + emit `PublishDegraded`; rebuild only fired if a fresh probe arrived. Round-47: rebuild path becomes engine-driven end-to-end without probe dependency. | Round-47 architect ruling at T4d-4 part B | ✓ PORTED T4d-4 part B (`seaweed_block@812d3fa`); refined at part C bug fix `e642ae8` | +| **INV-REPL-REBUILD-FAILURE-TERMINAL** *(round-47 architect addition)* | Rebuild has `MaxRetries=0` per `DefaultRuntimePolicyFor`; first rebuild failure terminates with cleared `Decision` + `PublishDegraded`. There is no rebuild retry loop; failure is terminal. | Round-47 architect ruling at T4d-4 part B | ✓ PORTED T4d-4 part B (`seaweed_block@812d3fa`); pinned by `TestSessionFailed_NonRecycled_RetriesUntilBudget` post-update + L2 matrix `TestT4d4_FullL2_*` | +| **INV-REPL-FAILED-SESSION-KIND-DRIVES-ESCALATION** *(part C Bug #1 capture)* | Catch-up exhaustion check MUST key on `st.Session.Kind == SessionCatchUp` (truth = what session actually failed), NOT on the mutable `Decision` field. Resists stray auto-probes that re-classify Decision mid-flight. Pre-fix: stray auto-probe between catch-up retry attempts re-classified `Recovery.Decision` from CatchUp → Rebuild (because empty replica showed R