mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
tlongwell-blockandDawn
f1957c945c
The drain-reachability probe (M10) guaranteed nothing mechanically: it was a documented procedure a reviewer had to remember to run. Deleting MigrateB leaves all five safety invariants green, so nothing in CI would have caught the round-1 bug coming back. scripts/check-tla-specs.sh runs both configs with opposite pass conditions: the safety model must complete with no violation, and the drain probe must report `Invariant Probe_NotC is violated` — a green drain run means phase C is unreachable from the stall state and fails the build. The inverted assertion greps the specific invariant name rather than checking TLC's exit status: a parse error or missing module also exits non-zero, and treating that as the expected violation would make the check useless exactly when the spec is broken. tla2tools is pinned by release tag and by sha256, since release assets can be re-uploaded. Verified in four directions on the committed script: unmodified specs exit 0; MigrateB stripped from DrainNext exits 1 via the green-drain branch; a spec that fails to parse exits 1 via the neither-verdict branch; a jar with the wrong checksum exits 1 before TLC runs. Runtime is ~3s including the jar download. The module allow-list is deliberately just RedisClusterFencingMigration, not a glob over docs/spec/*.cfg: MultiTenantRelay does not finish in a reasonable CI budget and GitOnObjectStore explores ~12.4M states, so attaching them to every PR would buy flakiness rather than safety. Co-authored-by: Dawn (sprout agent) <c6237ef84fa537c78dcee78efd2d4e59f728859c7f194da42ac51ededfa0be05@sprout-oss.stage.blox.sqprod.co> Signed-off-by: tlongwell-block <109685178+tlongwell-block@users.noreply.github.com>