Byzpaxos - #10
Merged
Merged
Conversation
added ByzPaxos proof to examples directory
Contributor
|
@muenchnerkindl Weren't you supposed to also remove the file from the test suite? |
Contributor
Author
|
Removed the directory from the regression suite. |
Contributor
Author
|
I will again ignore the failed tests because they are not related to the PR. |
Member
|
The build breakage is bogus anyway because pr.yml is set to run with OCaml |
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 21, 2026
…dencies The ranked table did not have the granularity it implied, and the "recommended path" section restated it instead of adding to it. **Granularity.** The table now says explicitly that one row is one pull request, with a `commits` column: eight rows are groups that must land together (tlaplus#3 is 2 commits, tlaplus#15 is 3, tlaplus#17 is 2, tlaplus#18 is 3, tlaplus#19 is 6, tlaplus#20 is 5), twelve are a single commit. Item 17 also notes that the branch holds an add-then-revert pair there -- the prover-slot-division hypothesis, refuted by measurement -- which must not be replayed. **Two rows were missing entirely**, and the question exposed it: the measurement instrumentation (17 commits, 22 files, +876/-92) and the harness (5 commits, 9 files, +698) buy no performance, but T1/T2 *are* the checker and P1/P2/P3 *are* the probes -- an optimization landed before them ships unverifiable. They are now rows 0 and 0b, marked as prerequisites rather than ranked. **The step ladder is gone.** Its six invented steps were the same items regrouped, with diffstat totals that restated the table; the batching advice it carried was already one sentence in the summary. Replaced by what it should have been -- dependencies: * hard, in code: tlaplus#3's two commits in order; tlaplus#11 requires tlaplus#15 (the memo attaches to the expansion fold's shared states); tlaplus#15's three commits in order; tlaplus#19 requires tlaplus#5 (it patches the tree tlaplus#5 rebuilt); #0/#0b before any protocol; * hard by measurement, and easy to miss: tlaplus#3 must not ship without tlaplus#15 on INSTANCE-heavy specs -- alone it takes preparation 458 -> 842 s while cutting peak memory 13.9 -> 5.1 GB; * soft: tlaplus#6+#12 for the x49 elaboration clock, tlaplus#10+tlaplus#16 for the memory unlock, tlaplus#18/tlaplus#19 adjacent but independent. Plus three review-coherent batches, stated as such rather than as a path. The protocol section is renamed to say what it is. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CUUoeEmuL3jsYhUb3UrhJH
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 21, 2026
Bugfixes were sitting in the ranked list because two of them have a positive performance effect. That mixes two decisions of different natures: an optimization is a trade -- review effort and risk against a measured gain, declinable on either side -- while a bugfix repairs behaviour the program already advertises, and declining it means keeping the defect. Ranking them together invites the wrong conversation. The three are now item #0, out of the table: the broken `--timing` accounting (B1), the spurious prover timeouts (B2, already in tlaplus#286), and the prover left alive when the hangup signal is ignored (B3). Grouped effect stated once -- 5 commits, 8 files, +138/-35 -- with a verification recipe each, and B3's large measured effect explicitly framed as an argument for urgency rather than the reason to take the change. The optimizations renumber 1-18 accordingly, and every cross-reference follows: the three per-item tables, the dependency orderings (tlaplus#2's two commits, tlaplus#10 requires tlaplus#13, tlaplus#13's three commits, tlaplus#17 requires tlaplus#4, and tlaplus#2 must not ship without tlaplus#13), the batching, the guard list, the tlaplus#286 family mapping, the local-proof table and its "weak signal" list, and the tlaplus#284 comparison. The headline recomputes to 429 added lines (-130) across seven files for items 1-8, since the SIGTERM fix is no longer counted among them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CUUoeEmuL3jsYhUb3UrhJH
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
3 participants
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.
Added Byzantine Paxos spec and proofs to examples directory.