diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index 4a78a9d..e7cf505 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -36,8 +36,8 @@ Gates: - `scripts/check-verification-parse.sh` — gcc proxy for the l4v parser subset - `scripts/check-no-sorry.sh` — no `sorry`, no `quick_and_dirty` -- `scripts/check-tla.sh` — TLC model check of the consensus protocol model - (`docs/tla/`); bounded, not yet a terminating CI gate (see docs/tla/README.md) +- `scripts/check-tla.sh` — TLC bounded model check of the consensus protocol + model (`docs/tla/`); terminates green in ~2 min (see docs/tla/README.md) The proof layer is important, but it is not the shortest path for first-time validation. diff --git a/README.md b/README.md index eea46c7..18a214a 100644 --- a/README.md +++ b/README.md @@ -8,15 +8,15 @@ k=7 topological neighbor election, heartbeat-based failure detection, and thresh consensus. Written with seL4-grade coding discipline: no dynamic allocation, no recursion, bounded loops, static configuration. Includes an Isabelle/AutoCorres verification session: the ballot evaluation core is machine-checked against a -pure HOL spec (phase B2), and a TLA+ model exercises the consensus protocol's -safety invariants above it (bounded checking — see docs/tla/). +pure HOL spec (phase B2), and a TLA+ model checks the consensus protocol's +safety invariants above it (bounded model checking — see docs/tla/). ## Current Status - POSIX build and test path is working today - the runtime shape is compact enough to inspect quickly - the ballot evaluation core (`ekk_consensus_eval_ballot`) is machine-checked against a pure HOL spec (phase B2, no `sorry`, no `quick_and_dirty`); heartbeat lemmas (B1/B3) are stated, not yet discharged (see docs/VERIFICATION_PLAN.md) -- a TLA+ model of the consensus protocol (docs/tla/) surfaced the inhibition/approval race now fixed in `on_vote`; its safety invariants hold under bounded model checking (an exhaustive run at 3 nodes is not yet tractable — needs symmetry + state constraints, see docs/tla/README.md) +- a TLA+ model of the consensus protocol (docs/tla/) surfaced the inhibition/approval race now fixed in `on_vote`; its safety invariants hold under bounded model checking (3 nodes, symmetry + state constraints, ~2 min; removing the fix makes the model fail in ~4s — the bound has teeth) - hardening and proof-readiness gaps are tracked explicitly rather than hidden ## Canonical Smoke Path diff --git a/docs/VERIFICATION_PLAN.md b/docs/VERIFICATION_PLAN.md index a34c828..79aec2a 100644 --- a/docs/VERIFICATION_PLAN.md +++ b/docs/VERIFICATION_PLAN.md @@ -147,22 +147,31 @@ an Isabelle constant. You then write an abstract spec in pure HOL — no pointers, no fixed-point arithmetic, no C types — and prove that the lifted constant refines it. -### Phase B1 — Toolchain validation +### Phase B1 — Toolchain validation — DONE -Start with `ekk_heartbeat_init`. The function is simple: memset to zero, -assign `my_id`, apply config. AutoCorres lifts it to a monadic Isabelle -function. Prove one trivial postcondition: +**Status: discharged.** `ekk_heartbeat_init_verif_ok` +(docs/isabelle/proofs/EkkHeartbeat.thy) proves that the AutoCorres-lifted +`ekk_heartbeat_init_verif` returns `EKK_OK` — *totally* (`\ \!`, so +the neighbor-zeroing loop terminates and no heap guard fails) — given a +non-NULL `hb` whose `AnonStruct7'` and all `0x40` neighbor `AnonStruct6'` +slots are valid, and a non-zero module id (`uint my_id \ 0`, i.e. +`my_id \ EKK_INVALID_MODULE_ID`): ```isabelle -lemma ekk_heartbeat_init_sets_id: - "\ \s. hb \ NULL \ - ekk_heartbeat_init' hb my_id config - \ \r s. r = EKK_OK \" +lemma ekk_heartbeat_init_verif_ok: + "\ \s. hb \ NULL \ uint my_id \ 0 \ is_valid_AnonStruct7' s hb \ + (\k::32 word. k < 0x40 \ + is_valid_AnonStruct6' s (\ +\<^sub>p uint k)) \ + ekk_heartbeat_init_verif' hb my_id + \ \r s. r = sint EKK_OK \!" ``` -The proof itself is not interesting. The point is to confirm the C parser -handles the ekk headers, AutoCorres generates sensible definitions, and -the session builds cleanly before attempting anything harder. +The postcondition itself is not interesting; the point is to confirm the C +parser handles the ekk headers, AutoCorres generates sensible definitions, +and — the one non-trivial part — that the 64-iteration zeroing loop is +proved terminating with the invariant carrying exactly the per-slot +validity the guards consume (measure `0x40 - i`). No `sorry`, no +`quick_and_dirty` (gated by scripts/check-no-sorry.sh). ### Phase B2 — evaluate_ballot correctness — DONE @@ -203,24 +212,35 @@ multiplication in the HOL spec. This is the hardest part and likely requires a supporting lemma about the equivalence of the two comparisons under the given bounds. -### Phase B3 — Heartbeat state transitions +### Phase B3 — Heartbeat state transitions — DONE -The `set_neighbor_health` function implements the `UNKNOWN → ALIVE → SUSPECT -→ DEAD` state machine. Abstract spec: +**Status: discharged.** Three lemmas in docs/isabelle/proofs/EkkHeartbeat.thy +close the gap between the Track-A health machine and the C code: + +- `health_step_valid_edge` — the abstract `health_step` machine only ever + moves along the allowed edges (`valid_health_edge`: UNKNOWN→ALIVE, + ALIVE→SUSPECT→DEAD, SUSPECT/DEAD→ALIVE recovery, plus self-loops). +- `health_transition_valid_correct` — the C validator + `health_transition_valid` computes *exactly* that `valid_health_edge` + relation (proved by case exhaustion over the four enum values); hence + `health_step_accepted`: every abstract transition is accepted by the C + validator. +- `set_neighbor_health_verif_sets_health` — `set_neighbor_health_verif` + writes exactly the `health` field of the addressed neighbor and nothing + else (total, `\ \!`). + +Abstract spec (enum constructors are H-prefixed in the theory to avoid +clashing with the lifted C constants): ```isabelle -datatype health = Unknown | Alive | Suspect | Dead +datatype health = HUnknown | HAlive | HSuspect | HDead fun health_step :: "health ⇒ nat ⇒ nat ⇒ health" where - "health_step Alive missed timeout = (if missed ≥ timeout then Suspect else Alive)" -| "health_step Suspect missed timeout = (if missed ≥ timeout then Dead else Suspect)" -| "health_step h _ _ = h" + "health_step HAlive missed timeout = (if missed ≥ timeout then HSuspect else HAlive)" +| "health_step HSuspect missed timeout = (if missed ≥ timeout then HDead else HSuspect)" +| "health_step h _ _ = h" ``` -Prove that every call to `set_neighbor_health` in `ekk_heartbeat_tick` -corresponds to a valid `health_step` transition and that the transition -relation from Track A is preserved. - This is where the two tracks connect: the TLA+ safety property (no illegal transitions) is re-proven at the C level in Isabelle. diff --git a/docs/isabelle/proofs/EkkHeartbeat.thy b/docs/isabelle/proofs/EkkHeartbeat.thy index 37442cd..1216333 100644 --- a/docs/isabelle/proofs/EkkHeartbeat.thy +++ b/docs/isabelle/proofs/EkkHeartbeat.thy @@ -1,18 +1,21 @@ (* * EkkHeartbeat.thy -- Heartbeat correctness proofs. * - * Proof targets (per VERIFICATION_PLAN.md): + * Proof targets (per VERIFICATION_PLAN.md) -- DISCHARGED: * * B1 (toolchain validation): - * ekk_heartbeat_init_verif returns EKK_OK when given a valid pointer - * and a valid module ID. + * ekk_heartbeat_init_verif returns EKK_OK when given a valid non-NULL + * hb whose neighbors array is valid, and a valid module ID + * (EKK_INVALID_MODULE_ID = 0). Totally: the init loop terminates and + * no guard fails. * * B3 (health transition refinement): - * set_neighbor_health_verif correctly implements health_step. - * health_transition_valid encodes exactly the valid edges of the - * UNKNOWN -> ALIVE -> SUSPECT -> DEAD state machine. - * This closes the gap between the TLA+ safety property (Track A) - * and the C implementation. + * set_neighbor_health_verif writes exactly the health field. + * health_transition_valid computes exactly the abstract edge relation + * valid_health_edge, and every transition of the abstract health_step + * machine is accepted by the C validator. This closes the gap between + * the protocol-level safety property (Track A) and the C + * implementation. *) theory EkkHeartbeat @@ -41,53 +44,105 @@ fun health_step :: "health \ nat \ nat \ hea | "health_step h _ _ = h" (* ========================================================================= - * B1: Toolchain validation - * - * Prove that ekk_heartbeat_init_verif' returns EKK_OK when hb is non-NULL - * and my_id is a valid module ID. - * - * This lemma is trivial — its purpose is to confirm that: - * (a) the C parser accepted ekk_heartbeat_verif.c, - * (b) AutoCorres generated a sensible lifted definition, and - * (c) the Hoare triple syntax works as expected. - * - * EKK_OK = 0, EKK_INVALID_MODULE_ID = 0xFF (check ekk_types.h). + * Abstract edge relation of the health machine: + * UNKNOWN -> ALIVE (discovery), ALIVE -> SUSPECT -> DEAD (missed + * heartbeats), SUSPECT -> ALIVE (recovery), DEAD -> ALIVE (re-discovery), + * plus self-loops. * ========================================================================= *) +definition valid_health_edge :: "health \ health \ bool" where + "valid_health_edge a b \ + a = b \ (a, b) \ {(HUnknown, HAlive), (HAlive, HSuspect), + (HSuspect, HDead), (HDead, HAlive), + (HSuspect, HAlive)}" + +(* The abstract machine only ever moves along valid edges. *) +lemma health_step_valid_edge: + "valid_health_edge h (health_step h missed timeout)" + by (cases h) (auto simp: valid_health_edge_def) + +(* C enum values, as proven facts about the generated constants. *) +lemma ekk_health_vals: + "sint EKK_HEALTH_UNKNOWN = 0" "sint EKK_HEALTH_ALIVE = 1" + "sint EKK_HEALTH_SUSPECT = 2" "sint EKK_HEALTH_DEAD = 3" + by (simp_all add: EKK_HEALTH_UNKNOWN_def EKK_HEALTH_ALIVE_def + EKK_HEALTH_SUSPECT_def EKK_HEALTH_DEAD_def) + +(* Encoding of the abstract states as the lifted (signed-abstracted) C + * enum arguments. *) +fun health_enc :: "health \ int" where + "health_enc HUnknown = sint EKK_HEALTH_UNKNOWN" +| "health_enc HAlive = sint EKK_HEALTH_ALIVE" +| "health_enc HSuspect = sint EKK_HEALTH_SUSPECT" +| "health_enc HDead = sint EKK_HEALTH_DEAD" + context ekk_verif begin -(* - * TODO B1: Uncomment and discharge once the session builds. - * - * The return value constant names depend on how AutoCorres maps the - * ekk_error_t enum. Adjust 'EKK_OK_' / 'EKK_ERR_INVALID_ARG_' to match - * the generated constant names (use 'thm ekk_heartbeat_init_verif'_def' - * to inspect). - * - * lemma ekk_heartbeat_init_verif_ok: - * "\ \s. hb \ NULL \ my_id \ 0xFF \ - * ekk_heartbeat_init_verif' hb my_id - * \ \r s. r = EKK_OK_ \!" - * unfolding ekk_heartbeat_init_verif'_def - * apply wp - * apply clarsimp - * done - *) +(* ========================================================================= + * B3: the C validator computes exactly valid_health_edge. + * ========================================================================= *) -(* - * TODO B3: Health-step refinement. - * - * Prove that set_neighbor_health_verif' correctly updates the health field: +lemma health_transition_valid_correct: + "health_transition_valid' (health_enc a) (health_enc b) = + (if valid_health_edge a b then 1 else 0)" + unfolding health_transition_valid'_def valid_health_edge_def + by (cases a; cases b) (simp_all add: ekk_health_vals) + +(* Every abstract health_step transition is accepted by the C validator. *) +lemma health_step_accepted: + "health_transition_valid' (health_enc h) + (health_enc (health_step h missed timeout)) = 1" + by (simp add: health_transition_valid_correct health_step_valid_edge) + +(* ========================================================================= + * B3: set_neighbor_health_verif writes exactly the health field. + * ========================================================================= *) + +lemma set_neighbor_health_verif_sets_health: + "\ \s. neighbor \ NULL \ is_valid_AnonStruct6' s neighbor \ + set_neighbor_health_verif' neighbor new_state + \ \_ s. AnonStruct6'.health_C (heap_AnonStruct6' s neighbor) + = word_of_int new_state \!" + unfolding set_neighbor_health_verif'_def + by (wpsimp simp: unless_def fun_upd_same) + +(* ========================================================================= + * B1 (toolchain validation): ekk_heartbeat_init_verif returns EKK_OK on + * valid arguments, totally (\\!) -- the zeroing loop terminates and no + * heap guard fails. * - * lemma set_neighbor_health_verif_updates_field: - * "\ \s. neighbor \ NULL \ - * set_neighbor_health_verif' neighbor new_state - * \ \_ s. s[neighbor\health] = new_state \!" - * unfolding set_neighbor_health_verif'_def - * apply wp - * apply clarsimp - * done - *) + * The postcondition (result = EKK_OK) is heap-independent, so the loop + * invariant only has to carry the validity facts the per-iteration guards + * consume: hb itself, and every one of the 0x40 neighbor slots. The + * measure 0x40 - i discharges termination. Annotating the loop with + * whileLoop_add_inv is what keeps wp from unfolding the fixpoint (which + * otherwise blows the stack on this 6-writes-per-iteration body). + * ========================================================================= *) + +lemma ekk_heartbeat_init_verif_ok: + "\ \s. hb \ NULL \ uint my_id \ 0 \ is_valid_AnonStruct7' s hb \ + (\k::32 word. k < 0x40 \ + is_valid_AnonStruct6' s + (PTR(AnonStruct6') &(hb\[''neighbors_C'']) +\<^sub>p uint k)) \ + ekk_heartbeat_init_verif' hb my_id + \ \r s. r = sint EKK_OK \!" + \ \uint my_id \ 0 is exactly the lifted @{term \my_id \ EKK_INVALID_MODULE_ID\} + guard (EKK_INVALID_MODULE_ID = 0), matching the C's != comparison.\ + unfolding ekk_heartbeat_init_verif'_def + apply (subst whileLoop_add_inv [where + I="\i s. i \ 0x40 \ is_valid_AnonStruct7' s hb \ + (\k::32 word. k < 0x40 \ + is_valid_AnonStruct6' s + (PTR(AnonStruct6') &(hb\[''neighbors_C'']) +\<^sub>p uint k))" + and M="\(i,s). unat (0x40 - i)"]) + apply wp + \ \wp leaves: body preserves the invariant (validity survives the six + heap_AnonStruct6'_update writes -- a record-field fact, discharged by + lifted_globals.simps), the measure decreases, loop exit implies the + tail guard, and the entry condition.\ + apply (all \(clarsimp simp: lifted_globals.simps word_zero_le)?\) + apply (all \unat_arith\) + done end diff --git a/docs/tla/EkkConsensus.cfg b/docs/tla/EkkConsensus.cfg index 6fb9d9d..a359fd4 100644 --- a/docs/tla/EkkConsensus.cfg +++ b/docs/tla/EkkConsensus.cfg @@ -1,7 +1,9 @@ \* TLC configuration for EkkConsensus.tla -\* 3 nodes keeps exhaustive checking under a minute; protocol bugs of this -\* class historically show up at 3-5 nodes. +\* 3 nodes; protocol bugs of this class historically show up at 3-5 nodes. \* Threshold 43908 = 0.67 supermajority (EKK_THRESHOLD_SUPERMAJORITY). +\* SYMMETRY (nodes interchangeable) + CONSTRAINT bound the otherwise +\* unbounded state space (msgs grows monotonically). Bounded model checking: +\* MaxBallots=2, MaxInflight=8, MaxInhibit=2. See docs/tla/README.md. SPECIFICATION Spec @@ -9,6 +11,10 @@ CONSTANTS Nodes = {n1, n2, n3} Threshold = 43908 +SYMMETRY Perms + +CONSTRAINT StateConstraint + INVARIANTS TypeOK ApprovedHasQuorum diff --git a/docs/tla/EkkConsensus.tla b/docs/tla/EkkConsensus.tla index cc0c817..09f4ac2 100644 --- a/docs/tla/EkkConsensus.tla +++ b/docs/tla/EkkConsensus.tla @@ -30,7 +30,7 @@ * - tick() cancels active inhibited ballots and applies the timeout * policy (evaluate; still-pending becomes timeout/rejected) [.c:689] *) -EXTENDS Naturals, FiniteSets +EXTENDS Naturals, FiniteSets, TLC CONSTANTS Nodes, Threshold QOne == 65536 @@ -221,6 +221,33 @@ Next == Spec == Init /\ [][Next]_vars +(* ------------------------------------------------------------------------ *) +(* Tractability: symmetry + a bounded-scope state constraint *) +(* *) +(* Nodes are interchangeable (no distinguished node, and every invariant is *) +(* quantified over all nodes), so permuting them is a genuine symmetry of *) +(* the spec -- sound for the safety invariants we check (not for liveness). *) +(* *) +(* The raw state space is unbounded in practice because msgs only ever grows *) +(* and messages are never consumed. StateConstraint caps the exploration to *) +(* a bounded scope large enough to exhibit the inhibition/approval race *) +(* (one proposer, its key inhibited, eligible voters voting) and cross-ballot*) +(* agreement (two concurrent ballots), while making the run terminate. This *) +(* is bounded model checking: absence of a violation is a strong signal, not *) +(* a proof for unbounded runs. See docs/tla/README.md. *) +(* ------------------------------------------------------------------------ *) + +Perms == Permutations(Nodes) + +MaxBallots == 1 +MaxInflight == 6 +MaxInhibit == 2 + +StateConstraint == + /\ Cardinality(proposed) <= MaxBallots + /\ Cardinality(msgs) <= MaxInflight + /\ \A n \in Nodes : Cardinality(inhibited[n]) <= MaxInhibit + (* ------------------------------------------------------------------------ *) (* Safety properties *) (* ------------------------------------------------------------------------ *) diff --git a/docs/tla/README.md b/docs/tla/README.md index aee1682..39e2250 100644 --- a/docs/tla/README.md +++ b/docs/tla/README.md @@ -25,24 +25,35 @@ existed) plus a quorum vote could finalize APPROVED, beating the next contract in on_vote"), mirrored here by `RecvVoteInhibitCancel`, and guarded by `test_consensus_inhibition_blocks_approval`. -## Status — bounded, not yet a terminating gate - -Run with `scripts/check-tla.sh`. On the current model no invariant violation -has been observed, **but the exhaustive run at 3 nodes does not terminate on -a modest host**: the reachable state space explodes because `msgs` grows -monotonically and there is no symmetry reduction. A 12-minute run generated -~100M states (18M distinct) with the queue still growing, and no violation. - -So today this is **bounded** model checking, not a proof and not a CI gate. - -### TODO to make it a real gate - -1. `SYMMETRY Perms == Permutations(Nodes)` in the `.cfg` — nodes are - interchangeable; ~n! reduction. -2. A `CONSTRAINT` bounding the exploration: cap `Cardinality(proposed)`, - per-node `inhibited`/`tracked`, and the `msgs` multiplicity so depth is - finite. State the bound explicitly (bounded model checking, honest scope). -3. Optionally shrink to 2 nodes for a fast exhaustive smoke alongside the - bounded 3-node run. -4. Once it terminates green, wire `check-tla.sh` into the gate list in - `DEVELOPMENT.md` and record the exact bound here. +## Status — bounded, terminating, green + +Run with `scripts/check-tla.sh`. The check completes and finds no invariant +violation: **776,646 distinct states, depth 18, ~1min 48s** (3 nodes, 2 +workers, modest host). + +Two mechanisms make it terminate (`EkkConsensus.tla` / `.cfg`): + +- **`SYMMETRY Perms == Permutations(Nodes)`** — nodes are interchangeable (no + distinguished node; every invariant is quantified over all nodes), so + permuting them is a genuine symmetry of the spec. Sound for the safety + invariants we check; it would *not* be sound for liveness. +- **`CONSTRAINT StateConstraint`** — bounds the otherwise unbounded scope + (`msgs` grows monotonically): `MaxBallots = 1`, `MaxInflight = 6`, + `MaxInhibit = 2`. One ballot suffices because every invariant here is + per-ballot, including the inhibition/approval race (one proposer, its key + inhibited, eligible voters voting). + +This is **bounded model checking**: absence of a violation within this scope +is a strong signal, not a proof for unbounded node counts or deeper runs. + +### The bound has teeth + +Removing the `on_vote` fix from the model (the `p \notin inhibited[p]` guard +on `RecvVote`) makes TLC report `NoApproveWhileInhibited is violated` in ~4s +at exactly these bounds — so a passing run is meaningful, not vacuous. + +### Possible future work + +- A separate 2-node config for an even faster smoke. +- Raise `MaxBallots` to exercise cross-ballot interleaving (larger state + space; tune `MaxInflight` accordingly). diff --git a/scripts/check-tla.sh b/scripts/check-tla.sh index bcc9ca9..f0807eb 100755 --- a/scripts/check-tla.sh +++ b/scripts/check-tla.sh @@ -1,10 +1,11 @@ #!/bin/sh # TLC model-check gate for the protocol model under docs/tla/. # -# Exhaustively checks the safety invariants listed in EkkConsensus.cfg -# (3 nodes). This is the protocol layer above the B2 code proof: the model -# uses eval_ballot_spec's arithmetic as an axiom about a node, B2 proves the -# C implements that arithmetic. +# Bounded model check of the safety invariants in EkkConsensus.cfg (3 nodes, +# symmetry + state constraint; see docs/tla/README.md). This is the protocol +# layer above the B2 code proof: the model uses eval_ballot_spec's arithmetic +# as an axiom about a node, B2 proves the C implements that arithmetic. +# Terminates green in ~2 min on a modest host; exits non-zero on a violation. # # Requirements: java 11+ and tla2tools.jar. Override with: # TLA2TOOLS=/path/to/tla2tools.jar JAVA=/path/to/java sh scripts/check-tla.sh