Verified raft state machine - #16
Open
yiyunliu wants to merge 7 commits into
Open
Conversation
Author
…mit, splice) Extract the Raft log's in-memory state into LogState and route every state change in Log through verified transitions: append_state (entry at last_index + 1 in the current term), commit_state (commit index never regresses), set_term_vote_state (nonzero, monotone term; vote can't change within a term), check_splice_entries (contiguous indexes, monotone terms), check_splice_connect (splice connects to the log without term regression), and splice_state (never writes at or below the commit index). Each verdict is proven exact, so Log panics with the same messages in the same cases; transitions preserve the wf invariant (last_term <= term, commit_index <= last_index), which is preserved rather than assumed since Log::new loads unverified disk state. Storage, serialization, and the splice skip-scan remain trusted. Opt raft::log into scripts/verus/verify.sh (42 -> 51 verified items). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UySbe8KkQbrWhQwiq1rtP1
…fety, log matching, leader completeness, state machine safety, linearizable reads) Add src/raft/safety.rs: a spec/proof-only Verus model of the whole Raft ensemble — per-host state, a monotone message history (drop/reorder/duplicate allowed), and ghost per-term leader logs, election records, and commit records — whose 14 transitions mirror the protocol steps of RawNode<Role> in node.rs (each documents the code it models). Over all reachable states, prove: - Election safety: at most one leader per term, from vote-once-per-term (the set_term_vote rule) plus quorum intersection. - Log matching: entries pin their log's prefix to the creating term's leader log; two logs agreeing on an entry's term agree on the whole prefix. - Leader completeness: a committed prefix is contained verbatim in every later leader's log. The inductive core: a commit's ack quorum intersects every later election's vote quorum; conditional persistence invariants (over current logs, and over log snapshots frozen in votes and election records) show the shared voter still held the prefix, and the section 5.4.1 up-to-date check transfers it into the winner's log. The section 5.4.2 own-term commit restriction of maybe_commit_and_apply is what makes the ack quorum meaningful. - State machine safety: hosts never disagree on committed entries; splices can't truncate a committed prefix because the append source agrees with it by leader completeness (this justifies the splice-below-commit panic). - Linearizable reads: a read served after quorum read-seq confirmation with an own-term committed tail (maybe_read's conditions) reflects every write committed anywhere at submission time, via read-confirm/ack quorum intersection and term monotonicity. The proof is an inductive global invariant (init_implies_inv + step_preserves_inv per transition, no admits/assumes), transported to all executions by execution_implies_inv; thm_* state the headline properties. This is a model-only proof in the TLA+/IronFleet-protocol-layer sense: the correspondence to node.rs is by documented inspection, not machine-checked refinement (that ironkv-style layer is future work), and liveness is out of scope. Everything erases under a normal cargo build. Opt raft::safety into scripts/verus/verify.sh (51 -> 90 verified items). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UySbe8KkQbrWhQwiq1rtP1
…nsitions Add src/raft/refine.rs, the node-local refinement layer connecting node.rs to the raft::safety model, and restructure node.rs to route every safety-relevant decision and state change through its verified step cores. Each core (core_grant, core_campaign, core_collect_vote, core_become_leader, core_propose, core_recv_append, core_leader_commit, core_recv_commit, core_send_append/ack/commit, core_submit_read, core_confirm_read, core_bump_term, core_step_down, core_restart) takes the node's concrete state summary plus its ghost abstract MHost state and proves host_refines: in every cluster state consistent with the node's local view and message evidence, performing this step is a transition of the safety model. Per-transition lifting lemmas construct the global witness state. The protocol decisions are computed by the cores and executed mechanically by the shell: the vote-once + section 5.4.1 up-to-date check (core_grant), the strict-majority quorum arithmetic for elections and commits (verified counting loops that also build the ghost ack-quorum evidence maps), the section 5.4.2 own-term commit condition, the append base-match/splice/ack computation, and the linearizable-read gate (core_can_serve), whose postcondition instantiates thm_read_linearizable: a served read reflects every write committed anywhere at submission time. Model additions to support write-level granularity: t_bump_term (a higher-term discovery as its own transition, also covering a crash between the term bump and the follow-up step) and t_step_down (candidate to follower in the same term); commands become opaque byte sequences. The trusted rim is explicit and greppable (refine.rs module docs): network non-forgery (received messages are in the ghost history; recv_* axioms recover ghost payloads behind concrete summaries), storage integrity (Log answers agree with the ghost log view), the mechanical shell discipline in node.rs (core preconditions at call sites are not machine-checked), and agreed cluster membership (model hosts are member ranks). node.rs carries the ghost state as zero-sized Ghost fields (habs, evid); a normal build erases all of it. The test harness's direct leader promotion now records the peers' votes so the verified quorum check is satisfied. Opt raft::refine into scripts/verus/verify.sh (90 -> 131 verified items). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UySbe8KkQbrWhQwiq1rtP1
Review follow-ups for the Raft safety/refinement layer: - Model: t_restart now takes the recovered commit index (c <= commit), since Log::commit does not fsync it; commit_leader_ok only claims a covering commit index while the host is still leader of that term, so thm_read_linearizable is unchanged. recover_abs documents exactly which model step it stands in for and the remaining fsync=false gap. - Cores check what the shell previously had to promise: member ids are verified distinct and in range at runtime (check_members) in core_leader_commit/core_can_serve; core_campaign and core_recv_append return None on term/index overflow instead of requiring it away. - Send-only cores return a #[must_use] Refined token consumed by send_refined/broadcast_refined (note_own_ack for the leader's self-ack), so a dropped core call is a compiler warning rather than a silent gap. - into_leader and propose share append_and_replicate; dead core_restart, lemma_lift_restart and cmd_view removed; mod refine no longer allows dead_code; document that the receiving cores only cover the equal-term path (the shell bumps first via core_bump_term). Verus: 134 verified, 0 errors. All tests pass; 300 random goldenscripts produce identical output against main. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JuukBNSENwNnQvaHZSXwhG
… to end Address the review findings on the refinement layer: the safety theorems were connected to the running code only through ~40 unchecked `requires` clauses on flat step cores, discharged by nobody in the unverified shell. Move those obligations into Verus-checked code: - Log (raft::log) now lives inside verus! with a ghost view of the stored entries. Every method pins its result and the new view (splice provably computes the model's splice, skip-scan included; has/get/read_range answer per the view). The trusted rim shrinks to the engine I/O functions plus Log::open, each with an explicit storage-integrity spec. Panics are preserved verbatim via a single diverging `fault` function. - A verified Members type (sorted ids, rank = position) replaces the shell's ad-hoc id->rank conversion, fixing the recover-time vote rank/id confusion and the 256-node size wrap. - Candidate votes and leader Progress move into the verified Abs state; Abs::inv backs every nonzero match index / read sequence with ack or confirmation evidence in the ghost history, so the commit quorum and the linearizable-read gate derive their evidence instead of trusting the shell to have recorded it. - One verified step function per protocol input composes the model transitions internally via host_refines_star (reflexive-transitive refinement that also carries the model invariant through step_preserves_inv). node.rs shrinks to an I/O shell with no core calls and no ghost values; the Refined token and note_* helpers are gone. - The four recv_* network axioms collapse into a single trusted recv_msg whose spec pins every concrete field of the received message, Append entry terms and commands included. scripts/verus/verify.sh: 177 verified, 0 errors (from 134). cargo test, clippy -D warnings, and fmt all green; raft goldenscripts unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LYvjWPjYtMgmPqUE3d5SWK
…osition
Address the three follow-ups from the round-2 review:
- M2 (apply path): add a verified `Log::read_committed` over the trusted
engine rim, whose postcondition pins the returned batch to the committed
prefix of the log's ghost view, and route `maybe_apply` /
`maybe_commit_and_apply` through it. The state machine is now fed exactly
the committed prefix the safety theorems are about; the unverified
`scan`/`scan_apply` iterators become test-only. Temper the docs that said
"applied prefix" where the theorem covers the committed prefix.
- m1 (mutator visibility): nest `raft::log` and `raft::refine` under a
shared `raft::verified` parent module (files stay in place via #[path])
and scope `Log::{set_term_vote, append, commit, splice}` to
`pub(in crate::raft::verified)`. The unverified I/O shell now gets read
access only, so a future node.rs edit cannot mutate the log behind the
refinement layer's back and silently vacate `Abs::inv`.
- M1 (composition): state trusted assumption 3 formally instead of in
prose. `cluster_bound` defines the composition invariant (a reachable,
invariant-satisfying model state binding every node's ghost state and
evidence); machine-checked lemmas establish it for a fresh cluster
(`lemma_cluster_init`) and maintain it across every step function call
(`lemma_cluster_step`) and crash-restart (`lemma_cluster_restart`);
`thm_cluster_safety` / `thm_impl_safety` instantiate the model's safety
theorems against a bound cluster — the latter directly against the
verified node states and the logs' verified views. The trusted residue is
reduced to the lemmas' hypotheses tracking the real run (assumptions 1,
2, 5).
The module rename perturbed two seed-sensitive SMT queries in log.rs
(`splice`, `count_present`); they get rlimit headroom and (for the latter) a
spinoff prover. Verification: 184 verified, 0 errors. Tests: 286 lib + 5
integration pass; goldenscripts unchanged.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LYvjWPjYtMgmPqUE3d5SWK
…coped Log mutators main added its own [lints.rust] table alongside the one this branch added, so cargo rejected Cargo.toml with 'duplicate key' on the PR merge commit. Keep main's copy only. Log::append/splice/commit are now pub(in crate::raft::verified), so the intra-doc links in Log's docs pointed at private items and failed cargo doc under -D warnings. Use plain code spans instead. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LYvjWPjYtMgmPqUE3d5SWK
yiyunliu
force-pushed
the
yl/raft-safety-refine
branch
from
September 1, 2026 02:32
6a4fc83 to
3d773dd
Compare
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.
No description provided.