Repository navigation
Correct etcd log freshness and add commit liveness - #191
Merged
Merged
Conversation
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.
The existing log-freshness predicate rejects a legal five-server execution: a disconnected server can have a newer uncommitted log than a follower whose older-term entry was committed later. Require freshness relative to a quorum before concluding that a log contains committed prefixes.
Add
CommitLivenessas a ninth target. It requires eventual commitment of current-term entries during stable replication, with explicit failure and scheduling assumptions. It does not claim leader-election liveness or unconditional availability. The eight safety targets retain their statements and failure model; generated task contexts and counts are updated.Validation: 130 relevant tests passed, 1 skipped; the complete generated module suite verifies with 0 errors; Ruff checks pass. Tests include the original 70-step counterexample, an incorrect-election control, finite progress interleavings, a fair witness establishing satisfiable assumptions, and counterexamples after removing commit fairness or making commitment a no-op. These finite checks do not establish the unbounded TLAPS theorem.
A fresh Opus 5.5 max run is active with the original immutable tool image and isolated runtime policy (3M generated-output cap including reasoning, 8 checker CPUs, 3600-second checker base; 10800 seconds after the existing 9-target scaling). An initial launch was stopped after image selection triggered a rebuild; its artifacts and 396 output tokens are retained and charged against the combined 3M cap. The active attempt starts with a separate empty session. Earlier eight-target results are preserved. Draft pending semantic review and proof results.