PBTS: system model made more precise #8096
Merged
Conversation
This file contains 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
josef-widder
approved these changes
Mar 9, 2022
* The property needs to be properly demonstrated.
williambanfield
approved these changes
Mar 15, 2022
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
Comment on lines
214
to
223
| The existence of `POL(v,r)` is a requirement for the decision of `v` at round | ||
| `r` of consensus. | ||
|
|
||
| At the same time, the Time-Validity property established that if `v` is decided | ||
| then a timely proof-of-lock `POL(v,v.round)` must have been produced. | ||
|
|
||
| So, we need to demonstrate here that any valid `POL(v,r)` is either a timely | ||
| proof-of-lock or it is derived from a timely proof-of-lock: | ||
|
|
||
| #### **[PBTS-DERIVED-POL.0]** |
There was a problem hiding this comment.
Really like this section! Very clear.
Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com>
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
williambanfield
approved these changes
Apr 18, 2022
josef-widder
approved these changes
Apr 29, 2022
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
…t.md Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com>
…t.md Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com>
Comment on lines
280
to
281
| `beginRound(p,r)` to represent the time the process `p` reads from its clock | ||
| when it starts round `r` of consensus. |
There was a problem hiding this comment.
Suggested change
| `beginRound(p,r)` to represent the time the process `p` reads from its clock | |
| when it starts round `r` of consensus. | |
| `beginRound(p,r)` as the value of process `p`'s local clock | |
| when it starts round `r` of consensus. |
…t.md Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>
…t.md Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>
…t.md Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>
30 tasks
github-merge-queue bot
pushed a commit
to cometbft/cometbft
that referenced
this pull request
Jan 9, 2024
This PR cherry-picks a number of commits present in the `master` branch of this repository. Some of the commits are from the old `tendermint/spec` repository, namely: - tendermint/spec#369 - tendermint/spec#373 - tendermint/spec#375 - tendermint/spec#398 - tendermint/spec#399 This content has then been migrated to the `tendermint/tendermint` repository, from which follow PRs were considered: - tendermint/tendermint#7804 (**not cherry-picked**) - tendermint/tendermint#8018 - tendermint/tendermint#8096 Most of the conflicts and the fixes needed refer to links to content, that have been updated or referred to old repositories. The MD files that are currently under `spec/consensus/proposer-based-timestamp` were moved to the `v1` subdir. Files with similar names, but the `-002` suffix were added with the new solution, replacing the old ones. The differences from the original content, on `master` and the content of this PR are minimal, as one can check by running ` git diff master spec/consensus/proposer-based-timestamp/` Finally, the entry point of the added content can be found [here](https://github.com/cometbft/cometbft/blob/cason/pbts-spec/spec/consensus/proposer-based-timestamp/README.md). --------- Co-authored-by: Daniel <daniel.cason@usi.ch> Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com> Co-authored-by: Kukovec <jure.kukovec@gmail.com> Co-authored-by: Daniel Cason <cason@gandria> Co-authored-by: M. J. Fromberger <fromberger@interchain.io> Co-authored-by: Anton Kaliaev <anton.kalyaev@gmail.com>
mergify bot
pushed a commit
to cometbft/cometbft
that referenced
this pull request
Mar 8, 2024
This PR cherry-picks a number of commits present in the `master` branch of this repository. Some of the commits are from the old `tendermint/spec` repository, namely: - tendermint/spec#369 - tendermint/spec#373 - tendermint/spec#375 - tendermint/spec#398 - tendermint/spec#399 This content has then been migrated to the `tendermint/tendermint` repository, from which follow PRs were considered: - tendermint/tendermint#7804 (**not cherry-picked**) - tendermint/tendermint#8018 - tendermint/tendermint#8096 Most of the conflicts and the fixes needed refer to links to content, that have been updated or referred to old repositories. The MD files that are currently under `spec/consensus/proposer-based-timestamp` were moved to the `v1` subdir. Files with similar names, but the `-002` suffix were added with the new solution, replacing the old ones. The differences from the original content, on `master` and the content of this PR are minimal, as one can check by running ` git diff master spec/consensus/proposer-based-timestamp/` Finally, the entry point of the added content can be found [here](https://github.com/cometbft/cometbft/blob/cason/pbts-spec/spec/consensus/proposer-based-timestamp/README.md). --------- Co-authored-by: Daniel <daniel.cason@usi.ch> Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com> Co-authored-by: Kukovec <jure.kukovec@gmail.com> Co-authored-by: Daniel Cason <cason@gandria> Co-authored-by: M. J. Fromberger <fromberger@interchain.io> Co-authored-by: Anton Kaliaev <anton.kalyaev@gmail.com> (cherry picked from commit 84339ef)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
System model updated from comments received in meetings, being also aligned with the restrictions imposed by the formal specification of the solution in TLA+.