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>
Specifies the bb-public relay's migration from single-shard cluster-mode-
disabled Valkey to a sharded cluster, in the house style of
docs/git-on-object-storage.md and docs/multi-tenant-relay.md.
The mechanized core is the fenced session directory key migration: the
tunnel lease/generation pair must be renamed to share a hash slot, which
is a live handoff of fencing authority under a rolling deploy. The TLA+
model (docs/spec/RedisClusterFencingMigration.tla) proves single-authority,
generation-monotonicity, and one-way-door safety across the O->A->B->
backfill->C phase protocol; all five invariants are mutation-tested
non-vacuous (5 mutants, each trips its intended invariant).
The rest is gated engineering: split client architecture (deadpool cluster
pool + separate RESP3 push_sender subscription client), sharded pub/sub as
a sizing prerequisite (classic PUBLISH broadcasts to every node), the
silently-partial SCAN in mesh discovery replaced by a scored-expiry index,
and the staged ElastiCache mode change with cluster-mode=enabled named as
irreversible.
Inputs: Wren's deployed-source inventory and Dawn's migration-mechanics
digs (channel buzz-redis-cluster-mode, thread 3440fed6).
Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d