feat: live retention floor guard — close the axiom-5 boundary for All-scope watches#7
Merged
Merged
Conversation
…-scope watches The hazard (machine-checked reachable in tests/model_live_watch.rs, unguarded variant): retention overrunning a LIVE consumer makes JetStream silently skip evicted messages — delete markers included — with no error anywhere: permanent silent fold divergence mid-watch, the same clamp class the resume-time check eliminated, previously covered only by the "retention >> lag" operating axiom. The model checker rejected the first guard design (periodic floor probe) with a counterexample: deliveries can catch the frontier up past the gap between probes, erasing the evidence. The shipped design is therefore in-band: a delivered revision that jumps the frontier by more than one is checked AT that delivery against first_sequence via the shared kernel (protocol::resume_window_ok) before the entry is processed — benign interior gaps pass, head eviction past the frontier fails the watch, and the restart routes into the verified resume -> CursorExpired -> resync repair path. A periodic probe backstops the no-traffic case only. Proof + conformance: - tests/model_live_watch.rs: guarded variant proves every maximal run ends with the fold equal to the bucket (trip witness earned, no phantom deletes); unguarded variant pins permanent silent divergence as the machine-checked record of the pre-guard code. - src/nats.rs floor_guard_tests: live-server twins — a clamped watch trips on its first gapped delivery before anything is folded; interior per-subject gaps pass with the dense tail delivered intact. - Axiom 5 narrowed accordingly: prefix-scoped watches (sparse by design, benign/hazardous eviction indistinguishable client-side) and the fresh full watch's history scan retain the operating requirement; the steady-state All-scope resume watch no longer relies on it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes the last known silent-divergence path: retention overrunning a live consumer. JetStream silently skips evicted messages — delete markers included — so an overrun watch's fold kept deleted keys permanently, with zero errors (
tests/model_live_watch.rsproves this reachable for the unguarded code). Previously covered only by the "retention ≫ lag" operating axiom.The model checker rejected the first design before any production code existed: a periodic floor probe has a hole — deliveries can catch the frontier up past a gap between probes, erasing the evidence (the checker produced that exact trace on first run). The shipped design is therefore in-band: a delivered revision that jumps the frontier by more than one is checked against
first_sequencevia the shared kernel (protocol::resume_window_ok) before the entry is processed. Benign interior gaps pass (monotonefirst_sequencemakes the discrimination airtight); head eviction past the frontier fails the watch into the already-verified restart →CursorExpired→ resync repair path. A periodic probe remains only as the no-traffic backstop.Proof + conformance
tests/model_live_watch.rs— guarded variant: every maximal run ends with the fold equal to the bucket (trip witness earned; no phantom deletes). Unguarded variant: permanent silent divergence pinned as the machine-checked record of the pre-guard code. Abstractions documented with soundness arguments (no client buffer modeled; repair composite = separately verified subprotocol; repair liveness conditional on supervision, safety unconditional).src/nats.rsfloor_guard_tests— live-server twins: a clamped watch trips on its first gapped delivery before folding anything; interior per-subject gaps pass with the dense tail intact.Test plan
🤖 Generated with Claude Code