feat: verified snapshot transport — pointer-swap protocol, model-checked, v0.6.0#6
Merged
Conversation
…ked, v0.6.0 Three real bugs found and fixed, each caught by a new verification layer: 1. NATS silently clamps a resume below first_seq (no error), so the entire CursorExpired -> resync path was dead code: every expired resume silently skipped the gap, evicted delete markers included. Expiry is now detected proactively (first_sequence comparison, re-checked after consumer creation), pinned by a live regression test. 2. A failed stale-key resync degraded to a warning, silently leaving deleted keys in the fold forever. Resync failure now fails the watch (fail-stop); the model proves degrade semantics break the convergence theorem. 3. The transport's two-object layout allowed a stalled exporter to regress "latest" (last-write-wins clobber) and a mid-upload crash to tear the payload/manifest pair. Replaced with content-addressed write-once payloads + a single pointer published last via monotonic conditional swap (If-Match CAS; fail-closed on non-CAS stores with explicit dev-only opt-in). The model checker additionally caught a dangling-pointer race between prune and an in-flight publish; the fix is the strictly-below- the-pointer prune rule, with cursors embedded in payload keys. Proof stack: - src/protocol.rs: shared decision kernels — production code and the model checker execute the same guard source, so guards cannot drift from proof. - tests/model.rs: Stateright model, exhaustive within bounds; theorems (no regression, no torn pairs, no dangling pointers, no mixed imports, no silent divergence, terminal liveness) over multi-round fleets at N=2/3; legacy configurations kept as machine-checked records of each bug; mutation tests prove every kernel guard is load-bearing; deep tier (~250M unique states) for release runs. - tests/multi_export.rs: prevention proofs on live NATS + real fjall/ RocksDB folds (slow-exporter refused, crash window keeps bootstrap available, post-compaction multi-SST fidelity under source churn). - tests/resync.rs: live expiry->resync chain end-to-end; NATS clamp pinned; no-reader divergence pinned. - tests/transport_s3.rs: conditional-put axiom verified on live MinIO (Create, If-Match swap, refusal, crash window, prune). Wire format change (payload location): upgrade exporters before bootstrap-dependent nodes. v0.6.0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…port pipeline Add the sections and content that were missing from the existing doc: - Rewrite summary to describe observable input → output behavior - Add data flow diagrams for artifact bootstrap and export round - Add 9 new Concepts & Terminology entries covering ExportLease, LeaseGuard, ExportManifest, ArtifactTransport, ObjectStoreTransport, PublishOutcome, etc. - Add Machine-Checked Protocol Kernels section documenting the three guards in protocol.rs (pointer_publish_allowed, payload_prunable, resume_window_ok), their Stateright theorem names, and why they are shared between production and model - Add Export Round State Machine with states, transitions, and failure outcomes - Add Export Lease section covering CAS acquisition, embedded TTL rationale, corrupt-lease stealing, and LeaseRecord wire format - Expand transport object layout to show content-addressed payload key derivation - Update Package Structure to include all new source files and test files - Update Failure Modes table with What-Actually-Happens column and export failures - Expand Trust Model to cover the transport layer's verification gates - Add two new Design Decisions: monotonic pointer vs. two-register layout and protocol.rs shared with model - Add BatchConfig, ObjectStoreTransport/ExportLease, and per-backend durability configuration tables Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A cache-restored rustup 1.92 sometimes lacks the clippy/rustfmt components
mise.toml requests, fast-failing the clippy step ("'cargo-clippy' is not
installed") — a recurrent flake (also 2026-06-04). An idempotent
`rustup component add` is ~2s when present and heals the poisoned cache.
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
This started as "is the snapshot export/import consistent with multiple exporting nodes?" and ended as a verification campaign that found and fixed three real correctness bugs, replaced the transport protocol with a machine-checked design, and left behind a proof stack that re-verifies the protocol on every test run.
Bugs found (each caught by a different verification layer)
The entire
CursorExpired→ resync path was dead code. NATS does not error on a resume belowfirst_seq— it silently clamps to the first retained message (pinned live bynats_silently_clamps_resume_below_first_seq). Every expired-cursor resume silently skipped the gap, evicted delete markers included: silent fold divergence with zero log lines. Fixed with proactive detection:first_sequencecomparison before and after consumer creation in all three resume paths.A failed resync degraded to a warning, leaving deleted keys in the fold forever. The model proves warn-and-continue semantics break the convergence theorem (
legacy_degrading_resync_diverges); resync failure now fails the watch and the caller's restart retries the whole resume → expiry → resync chain.The two-object transport layout (payload + sibling manifest, both last-write-wins) allowed: a stalled exporter overrunning its lease to regress the published "latest", and a crash between the two PUTs to tear the pair and break every bootstrap until the next round. Replaced with content-addressed write-once payloads + a single pointer object published last via monotonic conditional swap (If-Match CAS; fail-closed on stores without conditional puts, explicit dev-only opt-in for
file://). The model checker additionally caught a dangling-pointer race between prune and an in-flight publish — fixed structurally with the strictly-below-the-pointer prune rule (cursors embedded in payload keys).The proof stack
src/protocol.rs— shared decision kernels: production code and the model checker execute the same guard source, so the guards cannot drift from the proof.tests/model.rs— Stateright model, exhaustive within bounds: no regression, no torn pairs, no dangling pointers, no mixed imports, no silent divergence, and cycle-proof terminal liveness — over multi-round fleets at 2 and 3 exporters, with crashes between every step, zero-grace pruning, and no lease (a strict superset of all clock-skew behaviors). Legacy configurations are kept as machine-checked records of each bug; mutation tests prove every kernel guard is load-bearing. Deep tier: ~250M unique states (cargo test --release --test model -- --ignored).tests/multi_export.rs— prevention proofs on live NATS with real fjall/RocksDB folds: the slow-exporter clobber is refused, the crash window keeps bootstrap available, and multi-SST post-compaction artifacts survive source churn byte-exactly.tests/resync.rs— the expiry → fallback → resync chain end-to-end against a live server (self-validating: the deleted key's marker is purged, so only a working chain can remove it), plus the no-reader divergence pinned.tests/transport_s3.rs— the conditional-put axiom verified on live MinIO: Create, If-Match swap, monotonic refusal, crash-window availability, prune.Rollout note (wire format change → v0.6.0)
Payloads moved from
<key>to<key>.payloads/<cursor>-<hash>.tar; 0.6.0 readers cannot consume 0.5.0 layouts. Upgrade exporters before bootstrap-dependent nodes, or let the first 0.6.0 round publish before relying on it.Test plan
🤖 Generated with Claude Code