B2 evaluate ballot proof#5
Merged
Merged
Conversation
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 <noreply@anthropic.com>
…ild green 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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
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.
B2 evaluate ballot proof