prisma-risk / tsoracle / 26408960300

95%

push

github

fix(server): make the clear-before-publish invariant unbypassable in the fence (#411)

The Leader arm of the leader watch published `NotServing` before clearing
the allocator, the inverse of invariant 2 (serving_core.rs), which every
other transition upholds. It was benign only because the published
`NotServing` closes the gate so `try_grant` is unreachable in the window
between the two calls — but a future edit that read the allocator without
the gate would turn it into a stale-epoch grant.

Rather than swap the two lines, remove the ability to get the order wrong:

- Add `ServingCore::enter_fencing()` (delegates to `step_down(None, None)`),
  named for the leadership-gain path where `step_down` reads backwards.
- Delete `clear_allocator()`. With no standalone clear primitive, `step_down`
  and `enter_fencing` become the only ways to clear the allocator, and both
  bake in clear-before-publish — so no call site can invert it. This makes
  invariant 2 enforced by construction, like invariant 1's `ExtensionSlot`.
- Collapse all three fence arms onto the encapsulated methods: Leader ->
  `enter_fencing()`, Unknown -> `step_down(None, None)` (a loss of certainty,
  not a gain), Follower -> `step_down(endpoint, epoch)`. The Follower/Unknown
  rewrites are byte-for-byte equivalent to their prior two-call bodies.

Updates invariant 2's doc to state it is enforced by construction.

18 of 21 new or added lines in 2 files covered. (85.71%)

9326 of 9817 relevant lines covered (95.0%)

495039.25 hits per line