From 84a03b74293a5a994c29fb22e8f03e375e007c8c Mon Sep 17 00:00:00 2001 From: mamut-studio Date: Sat, 4 Jul 2026 14:25:38 +0200 Subject: [PATCH 1/3] docs(readme): B1/B3 are discharged, align with VERIFICATION_PLAN README still said the heartbeat lemmas (B1/B3) were "stated, not yet discharged" in two places, contradicting docs/VERIFICATION_PLAN.md (B1/B2/B3 all DONE) and the actual sorry-free proofs in EkkHeartbeat.thy. The B1/B3 proof (8929ba5) postdates the callback-field struct change (fa50091), so the lemmas hold against the current headers. - intro and Current Status now report B1/B3 discharged alongside B2 - Verification section names the lemmas: B1 init totality (loop terminates), B3 health-transition validator refinement + set_neighbor_health field write Co-Authored-By: Claude Opus 4.8 --- README.md | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 80019cc..e9aea6a 100644 --- a/README.md +++ b/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: From ab4f6267301a073be2e12064638175094d30bc5a Mon Sep 17 00:00:00 2001 From: mamut-studio Date: Sat, 4 Jul 2026 14:35:58 +0200 Subject: [PATCH 2/3] =?UTF-8?q?docs(l4v):=20close=20the=20"run=20real=20l4?= =?UTF-8?q?v=20parser"=20item=20=E2=80=94=20env=20provisioned,=20build=20g?= =?UTF-8?q?reen?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 2026-06-19 "Remaining" note said the real l4v C parser still had to run and called a local l4v+Isabelle install unavailable. The environment is now provisioned (~/verification: pinned Isabelle + l4v + AutoCorres) and the real build passes: EkkBase lifts the callback-inclusive TUs and EkkVerification builds green (B1/B2/B3, sorry-free). Append a dated 2026-07-04 status with a reproduce command; keep the 06-19 snapshot as history. Co-Authored-By: Claude Opus 4.8 --- docs/L4V_PARSEABILITY_PLAN.md | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/docs/L4V_PARSEABILITY_PLAN.md b/docs/L4V_PARSEABILITY_PLAN.md index 338ef7c..225dff6 100644 --- a/docs/L4V_PARSEABILITY_PLAN.md +++ b/docs/L4V_PARSEABILITY_PLAN.md @@ -342,3 +342,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. From 8ab7f6b6cc0a5468dfe7ee00519d2c1f5462f929 Mon Sep 17 00:00:00 2001 From: mamut-studio Date: Sat, 4 Jul 2026 14:46:07 +0200 Subject: [PATCH 3/3] docs: fix docs<->proofs drift (TLA bounds, TU count, Track A as-built) Cross-check of every verifiable claim against the .thy proofs and the TLA model turned up three mismatches: - docs/tla/EkkConsensus.cfg: header comment said MaxBallots=2, MaxInflight=8; the model (EkkConsensus.tla) and docs/tla/README.md use 1/6/2. MaxBallots=1 is the bound that makes TLC terminate, so this was not cosmetic. - L4V_PARSEABILITY_PLAN.md: said "seven verified core TUs"; the gate (check-verification-parse.sh) covers eight and self-reports "8 core TUs" since 989ca77 single-sourced the B2 core into ekk_consensus_eval.c. - VERIFICATION_PLAN.md Track A: the proposed TLA file layout was never built as named. Added an as-built note: only EkkConsensus.tla exists (A2); heartbeat (A1) went to Isabelle B3; topology (A3) stays a stretch goal. All B1/B2/B3 lemma names, preconditions, specs, invariant names, and the threshold constant already matched. Co-Authored-By: Claude Opus 4.8 --- docs/L4V_PARSEABILITY_PLAN.md | 3 ++- docs/VERIFICATION_PLAN.md | 6 ++++++ docs/tla/EkkConsensus.cfg | 2 +- 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/docs/L4V_PARSEABILITY_PLAN.md b/docs/L4V_PARSEABILITY_PLAN.md index 225dff6..342e56e 100644 --- a/docs/L4V_PARSEABILITY_PLAN.md +++ b/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: diff --git a/docs/VERIFICATION_PLAN.md b/docs/VERIFICATION_PLAN.md index 79aec2a..1368de7 100644 --- a/docs/VERIFICATION_PLAN.md +++ b/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+ diff --git a/docs/tla/EkkConsensus.cfg b/docs/tla/EkkConsensus.cfg index a359fd4..cf7a30f 100644 --- a/docs/tla/EkkConsensus.cfg +++ b/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