mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d
56303ba8ea
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>