B2 evaluate ballot proof

README.md

@@ -8,14 +8,15 @@ k=7 topological neighbor election, heartbeat-based failure detection, and thresh
 consensus. The code avoids dynamic allocation and recursion, keeps loops
 bounded, and uses 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 checks the consensus protocol's
-safety invariants above it (bounded model checking — see docs/tla/).
+pure HOL spec (phase B2), the heartbeat init and health-transition lemmas are
+discharged (B1/B3), 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)
+- the ballot evaluation core (`ekk_consensus_eval_ballot`) is machine-checked against a pure HOL spec (phase B2); the heartbeat lemmas are discharged too — B1 (init returns `EKK_OK` totally, zeroing loop terminates) and B3 (the C health-transition validator refines the abstract state machine) — with no `sorry`, no `quick_and_dirty` (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 (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
 
@@ -53,8 +54,12 @@ function `ekk_consensus_eval_ballot` (the same translation unit the runtime
 compiles) returns exactly the pure HOL spec `eval_ballot_spec` — totally, with
 every generated guard discharged — under the preconditions
 `yes_votes <= eligible_voters`, `total_votes <= eligible_voters`,
-`eligible_voters <= 64`, `0 <= threshold <= 65536`. The heartbeat lemmas
-(B1/B3) are stated, not yet discharged. The session builds without
+`eligible_voters <= 64`, `0 <= threshold <= 65536`. The heartbeat lemmas are
+also discharged: B1 (`ekk_heartbeat_init_verif_ok`) proves the init path returns
+`EKK_OK` totally, including termination of the 64-slot zeroing loop; B3 proves
+the C validator `health_transition_valid` computes exactly the abstract
+`valid_health_edge` relation, and that `set_neighbor_health_verif` writes only
+the addressed neighbor's `health` field. The session builds without
 `quick_and_dirty`; `scripts/check-no-sorry.sh` gates against regressions.
 To build it, you need:
 

docs/L4V_PARSEABILITY_PLAN.md

@@ -322,7 +322,8 @@ definitions. It does not affect the non-verification build in any way.
 
 Phase 1 is met at the gcc proxy level. `scripts/check-verification-parse.sh`
 runs the acceptance command — `gcc -DEKK_VERIFICATION -Iinclude -fsyntax-only`
-— over the seven verified core TUs (HAL excluded) and passes clean.
+— over the eight verified core TUs (HAL excluded; the B2 ballot core is
+single-sourced as `ekk_consensus_eval.c`) and passes clean.
 
 Done:
 
@@ -342,3 +343,33 @@ Remaining (needs a local l4v + Isabelle install, unavailable here):
 - Phase 2/3: the `docs/isabelle/` session now lifts structs that include the
   callback fields, so the `.thy` scaffold should be re-checked against actual
   AutoCorres output before the proof targets.
+
+---
+
+## Phase 1 status (2026-07-04) — real l4v run closes the remaining items
+
+The l4v + Isabelle environment is now provisioned on the build host
+(`~/verification/`: seL4 verification-manifest checkout — pinned Isabelle plus
+l4v with AutoCorres/CParser/Word_Lib; bootstrap `scripts/setup-isabelle-l4v.sh`).
+Both 2026-06-19 "Remaining" items are closed:
+
+- The real l4v C parser and AutoCorres lift run over the verification TUs. The
+  `EkkBase` heap (C parse + AutoCorres lift) builds, so the callback-inclusive
+  structs are lifted by the actual parser — not just the gcc proxy — and the
+  lift stays content-current with the headers (a rebuild re-lifts only when the
+  C changes).
+- `EkkVerification` builds green on top (B1/B2/B3): `sorry`-free, no
+  `quick_and_dirty`, and the `.thy` scaffold resolves against the generated
+  AutoCorres names.
+
+Reproduce (host is 8 GiB — keep `threads=2 -j1`, and do not run TLC
+concurrently):
+
+```bash
+L4V_ARCH=ARM ~/verification/isabelle/bin/isabelle build \
+  -o threads=2 -j1 -o document=false \
+  -d ~/verification/l4v -d docs/isabelle EkkVerification
+```
+
+The gcc gate (`scripts/check-verification-parse.sh`) stays as the cheap parse
+check for hosts without a local l4v.

docs/VERIFICATION_PLAN.md

@@ -55,6 +55,12 @@ docs/tla/
   Topology.tla        -- k-nearest election (stretch goal)
 ```
 
+**As built:** the layout above is the original plan, not what is on disk. Only
+the consensus model was built — `docs/tla/EkkConsensus.tla` + `EkkConsensus.cfg`
+(Phase A2). The heartbeat state machine (A1) was instead discharged in Isabelle
+as phase B3 (the `valid_health_edge` refinement), so no `Heartbeat.tla` exists.
+The topology election (A3) stays a stretch goal and is not modeled.
+
 ### Phase A1 — Heartbeat state machine
 
 Model a single module's view of its neighbors. Each neighbor is a TLA+

docs/tla/EkkConsensus.cfg

@@ -3,7 +3,7 @@
 \* 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.
+\* MaxBallots=1, MaxInflight=6, MaxInhibit=2. See docs/tla/README.md.
 
 SPECIFICATION Spec