feat: watch_applied core verification campaign, v0.6.1#8
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>
…ch_applied core BUG (found while writing the cursor-authority model, reproduced live by transient_store_failure_never_leaves_a_cursor_gap): a failed store apply dropped its raw batch on the warn-and-continue path, and the NEXT successful flush committed only newer updates under the newest cursor — one transient store error followed by one success left a permanent, restart-surviving hole in the fold behind a cursor that claims completeness. The "snapshot is a cache, refold on restart" argument breaks precisely because the refold starts from the advanced cursor. Fix: a failed apply re-queues its raw batch (prepended, stream order preserved) so the next flush commits cumulatively — the store's cursor and contents always advance together. A persistent failure streak (16 consecutive) fail-stops before the backlog grows unboundedly; the restart refolds from the store's last good cursor. Models (campaign #3, the watch_applied core): - tests/model_applied.rs — cursor authority over every interleaving of delivery, flush boundaries, transient store failures, and crashes. Mutations prove both rules load-bearing: DropFailedBatch (the pre-fix shipped behavior) and ResumeFromMemApplied (why restarts must resume from the store's persisted cursor, which legitimately lags the in-memory applied cursor across failures) each reach the restart-surviving hole. - tests/model_resync_order.rs — the resync ack barrier's ordering claim ("synthetic deletes strictly before the first re-list put"), previously a comment, is now a theorem: delete-then-recreate converges straddling the listing in either direction; the NoAckBarrier mutation reaches the lost-recreate divergence that is the machine-checked reason the handshake exists. Fidelity note recorded in both models: no shared kernel exists here (the invariants are control-flow structure, not guard expressions), so fidelity rests on the transition audit, the mutation contrasts, and the live reproduction test. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… plain call The jared/applied-core branch pinned IN-BAND detection with a 5s timeout on gapped_delivery_with_advanced_floor_trips; main had already landed the same test without the timeout. Keeping the timeout: it's the regression guard against the periodic-only design the model checker rejected. Also commit the ARCHITECTURE.md additions from the /architecture-doc update: transient re-queue paragraph, live floor guard subsection, watch_applied state transition table, new model test file entries, and new configuration + failure-mode rows. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Machine-checked correctness for the watch_applied loop and its two critical ordering claims, plus ARCHITECTURE.md updates covering all new subsystems. **New Stateright models (3):** - `tests/model_applied.rs` — cursor-authority model: delivery → flush → transient failure → crash/restart pipeline exhaustively checked; `DropFailedBatch` and `ResumeFromMemApplied` mutations reach the restart-surviving hole, pinning both pre-fix bug classes - `tests/model_resync_order.rs` — resync ack-barrier model: proves synthetic deletes strictly precede re-list puts for every interleaving; `NoAckBarrier` mutation reaches the lost-recreate divergence - `tests/model_live_watch.rs` — floor-guard model: guarded variant proves the fold always converges; unguarded proves permanent silent divergence reachable — machine-checked record of the pre-guard design **Bug fixed (found while writing the models):** - Transient `store.apply()` failure dropped the raw batch; next successful flush advanced the cursor over a permanent hole. Fixed: re-queue the failed batch (prepend); fail-stop at 16 consecutive failures. Regression pin: `transient_store_failure_never_leaves_a_cursor_gap` **Regression pins added:** - `resync_listing_failure_is_fatal_not_degraded` — degrade-on-error resync leaves stale keys permanently; fail-stop is correct - `gapped_delivery_with_advanced_floor_trips` — 5 s timeout pins in-band detection (not the 30 s backstop) **ARCHITECTURE.md:** - Transient re-queue paragraph in cursor-after-apply section - Live retention floor guard subsection - watch_applied loop state transition table (13 rows) - Package structure updated with all new test files - MAX_STORE_APPLY_FAILURES and FLOOR_GUARD_INTERVAL in configuration Co-Authored-By: Claude Sonnet 4.6 <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
watch_appliedloop's two critical ordering invariants plus cursor authority under transient failure and crashstore.apply()failure dropped its raw batch; the next successful flush advanced the cursor over a permanent, restart-surviving hole. Fixed by re-queuing the failed batch (prepend to next flush); fail-stop at 16 consecutive failurestransient_store_failure_never_leaves_a_cursor_gap,resync_listing_failure_is_fatal_not_degraded,gapped_delivery_with_advanced_floor_trips(5 s timeout pins in-band floor-guard detection, not the 30 s backstop)watch_appliedstate transition table, all new test files in package structure, and new constants/failure modesModels
model_applied.rsDropFailedBatch(the shipped bug),ResumeFromMemAppliedmodel_resync_order.rsNoAckBarrierreaches lost-recreate divergencemodel_live_watch.rsTest plan
cargo test --test model_applied— 3 tests, all passcargo test --test model_resync_order— 2 tests, all passcargo test --test model_live_watch— 2 tests, all passcargo test --test resync— live NATS conformance including silent-clamp pincargo test --test multi_export— prevention proofs on live NATS + real backends🤖 Generated with Claude Code