docs: drain-reachability probe (M10) + B->A rollback session-loss note

Review round 2 (Dawn) found the safety model could not distinguish the
B2 fix from its absence: unguarded ExpireOld lets the C-gate be
discharged by luck, so deleting MigrateB left all invariants green.
Added DrainSpec/Probe_NotC — TLC from the stall state (full-B fleet, live
old-key lease, no spontaneous expiry) with inverted verdict semantics:
violation proves C reachable (93/44); mutant M10 (MigrateB removed =
round-1 behavior) stays green, making the round-1 bug permanently
visible. Main safety model unchanged (12636/3637, M1-M9 all killed).

Also per Dawn N1: rollback matrix now names B->A as dropping every
migrated session (A renews the old key; nobody renews the migrated
lease; renewer treats Lost as fatal) — liveness cost, prefer forward-fix.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

docs/redis-cluster-mode.md

@@ -364,6 +364,17 @@ costs):
    - No phase rollback while in `compatible`; revert the mode to
      `disabled` first (the mode doors and phase machinery never move in
      the same step).
+   - **Rolling back B→A drops every session B has already migrated —
+     prefer forward-fix.** An A-pod's renew addresses the *old* key
+     (§Per-phase operation table), so a lease `MigrateB` moved to the new
+     key is renewed by nobody after the downgrade: it dies within one TTL
+     and the renewer treats the loss as fatal (session torn down, verified
+     live against `spawn_lease_renewer_with_interval`'s `Lost` handling).
+     Safety is unaffected — A's union check sees the new-key lease and
+     refuses to fork — but rollback from B is **not free**, and an
+     operator reaching for it should expect to shed exactly the sessions
+     the migration had already carried forward. (Liveness, so outside the
+     safety model's scope; found and reproduced live by review round 2.)
 5. **Pre-G3 checklist:** compute `CLUSTER KEYSLOT` on both members of a
    real hash-tagged pair and require equality **before** entering
    compatible — a mis-tagged pair is invisible in disabled mode (slot
@@ -421,6 +432,11 @@ $ java -cp tla2tools.jar tlc2.TLC RedisClusterFencingMigration.tla \
     -config RedisClusterFencingMigration.cfg -deadlock
 Model checking completed. No error has been found.
 12636 states generated, 3637 distinct states found.
+
+$ java -cp tla2tools.jar tlc2.TLC RedisClusterFencingMigration.tla \
+    -config RedisClusterFencingMigrationDrain.cfg -deadlock
+Error: Invariant Probe_NotC is violated.   # INVERTED verdict: this is PASS
+93 states generated, 44 distinct states found.
 ```
 
 (`-deadlock` disables deadlock reporting because the model has *intended*
@@ -431,8 +447,9 @@ writers; a fourth adds no qualitatively new interleaving. Bounded check,
 mutation-shown non-vacuous — the standard claim for a TLC-checked safety
 spec.)
 
-**Every invariant is non-vacuous by mutation** (9 mutants, each run in
-isolation, all killed):
+**Every invariant is non-vacuous by mutation** (10 mutants, each run in
+isolation, each distinguished from the true model — M1–M9 by a violated
+safety invariant, M10 by the drain probe's inverted verdict):
 
 | Mutation | Models the real bug | Trips |
 |---|---|---|
@@ -445,6 +462,24 @@ isolation, all killed):
 | M7: rollback into O drops the reverse max-merge | O re-issues generations B already issued | `Inv_Monotonic` |
 | M8: rollback allowed past a running downgrade | skipped-phase rollback: O and B pods coexist | `Inv_SingleAuthority` |
 | M9: compatible entered without fleet fully on C | A/B cross-slot scripts meet live slot rules | `Inv_SlotRulesSafe` |
+| M10: `MigrateB` deleted (round-1 behavior: B renews old-key leases instead of migrating) | migration stalls at the C-gate forever | `Probe_NotC` **stays green** (inverted verdict — see below) |
+
+M10 needs a word, because it defends a fix the safety invariants cannot
+see. The safety model lets leases expire spontaneously (`ExpireOld`
+unguarded) — correct as the adversarial worst case for safety, but for
+*drain* it is the friendly best case: it lets the C-gate's
+`oldOwner = None` be discharged by luck, so deleting `MigrateB` from
+`Next` leaves all five safety invariants green (found by review round 2).
+The **drain-reachability probe** (`DrainSpec` +
+`RedisClusterFencingMigrationDrain.cfg`) closes the hole: it starts TLC in
+the stall state (fleet fully on B, backfilled, one live B-pod owning an
+old-key lease), removes spontaneous expiry (faithful to a lease whose
+owner is alive and renewing — renew is `PEXPIRE`), and checks
+`Probe_NotC == phase /= 3` with **inverted verdict semantics**: TLC
+reporting the "invariant" *violated* proves C is *reachable* (pass, 93/44
+states); TLC green means the migration deadlocks at the gate forever.
+With `MigrateB`: violated (C reachable). M10 (without it): green — the
+exact round-1 bug, now permanently visible to the model.
 
 M4 is the operationally scary one: it is exactly "someone deploys the final
 script version early because everything looks green." M6–M8 are the price

docs/spec/RedisClusterFencingMigration.tla

@@ -343,4 +343,58 @@ Inv_LeaseGenGrounded ==
   /\ (oldOwner /= None) => (oldLeaseGen > 0 /\ oldLeaseGen <= oldGen)
   /\ (newOwner /= None) => (newLeaseGen > 0 /\ newLeaseGen <= newGen)
 
+(***************************************************************************)
+(* Drain-reachability probe (spec S:B2 defense; found in review round 2).  *)
+(*                                                                         *)
+(* The safety model above lets ExpireOld/ExpireNew fire unguarded — the    *)
+(* adversarial worst case for SAFETY (leases may vanish at any moment).    *)
+(* But for DRAIN it is the friendly best case: an old-key lease whose      *)
+(* owner is alive and renewing never expires (renew is PEXPIRE — the exact *)
+(* premise B2 falsified), so unguarded expiry lets the C-gate's            *)
+(* oldOwner = None conjunct be discharged by luck. Consequence: deleting   *)
+(* MigrateB from Next leaves every safety invariant green — the model      *)
+(* could not tell the B2 fix from its absence (found by Dawn, round 2).    *)
+(*                                                                         *)
+(* This probe closes that hole. DrainInit is the stall state: fleet fully  *)
+(* on B, backfill done, one live B-pod still owning an old-key lease.      *)
+(* DrainNext is Next WITHOUT spontaneous expiry — faithful to a lease      *)
+(* whose owner never crashes. Probe_NotC is checked as an "invariant"      *)
+(* with INVERTED verdict semantics: TLC reporting Probe_NotC VIOLATED      *)
+(* proves phase C is REACHABLE from the stall state (pass); TLC GREEN      *)
+(* means the migration deadlocks at the C-gate forever (fail). Run with    *)
+(* RedisClusterFencingMigrationDrain.cfg. Mutant M10 (drop MigrateB from   *)
+(* DrainNext = round-1 behavior, B renews the old key instead of           *)
+(* migrating) must leave this probe green — proving MigrateB is the only   *)
+(* mechanism that discharges the gate without luck.                        *)
+(***************************************************************************)
+
+DrainInit ==
+  /\ phase = 2
+  /\ ver = [p \in Pods |-> 2]
+  /\ oldOwner = CHOOSE p \in Pods : TRUE
+  /\ oldLeaseGen = 1
+  /\ newOwner = None /\ newLeaseGen = 0
+  /\ oldGen = 1 /\ newGen = 1
+  /\ backfilled = TRUE
+  /\ mode = 0
+  /\ lastIssued = 1
+  /\ monoOk = TRUE
+
+DrainNext ==
+  \/ AdvancePhase
+  \/ RollbackPhase
+  \/ Backfill
+  \/ EnterCompatible
+  \/ RevertCompatible
+  \/ EnableCluster
+  \/ \E p \in Pods : UpgradePod(p) \/ DowngradePod(p)
+                     \/ AcquireO(p) \/ AcquireA(p) \/ AcquireB(p)
+                     \/ AcquireC(p)
+                     \/ MigrateB(p)  \* the B2 mechanism under test (M10)
+
+DrainSpec == DrainInit /\ [][DrainNext]_vars
+
+\* INVERTED verdict: a violation is the PASS (C reachable by participation).
+Probe_NotC == phase /= 3
+
 =============================================================================

docs/spec/RedisClusterFencingMigrationDrain.cfg

@@ -0,0 +1,11 @@
+\* Drain-reachability probe (see module header of the Drain section).
+\* INVERTED verdict: TLC reporting Probe_NotC VIOLATED = PASS (C reachable
+\* from the stall state); TLC green = FAIL (migration deadlocks at the
+\* C-gate). Mutant M10 removes MigrateB from DrainNext and must be green.
+CONSTANTS
+  Pods = {p1, p2, p3}
+  None = None
+  MaxGen = 4
+SPECIFICATION DrainSpec
+INVARIANTS
+  Probe_NotC