MIgrate and integrate TLA+ files from the spec repo by creachadair · Pull Request #8018 · tendermint/tendermint

creachadair · 2022-02-26T00:41:42Z

Changes to the TLA+ specifications that need to be integrated.

This recreates #8004, which I merged not realizing it was more than just a migration of files. Apologies for the noise.

Kukovec

Since I wrote these changes it'd be odd if I didn't approve.

ancazamfir · 2022-03-02T08:54:47Z

spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla

    /\ BenignRoundsInMessages(msgsPrecommit)
-    /\ evidence = EmptyMsgSet
+    /\ evidence = {}
    /\ action' = "Init"


TLC is not happy about this. In its usual cryptic way: "In evaluation, the identifier action is either undefined or not an operator." This fixes it:

Suggested change

/\ action' = "Init"

/\ action = "Init"

But then we run into deadlock, with AdvanceRealTime.

Huh, I'm surprised this one slipped by. Apparently this has been here since v1:

tendermint/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla

Line 180 in a229425

/\ action' = "Init"

It definitely shouldn't be primed here.

Apalache has some tolerance for Init, where it will treat primes and non-primes inside exactly Init as the same, but I suppose TLC would complain.

Huh, I'm surprised this one slipped by. Apparently this has been here since v1:

Yes, it was in v1 as well, i remember fixing it there in my local experiments.

ancazamfir · 2022-03-02T08:57:54Z

spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla

+INSTANCE TendermintPBT_002_draft WITH
+  Corr <- {"c1", "c2"},
+  Faulty <- {"f3", "f4"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 5,
+  MaxTimestamp <- 10,
+  MinTimestamp <- 2,
+  Delay <- 2,        
+  Precision <- 2
+


Could we also have an instance with <1/3rd faulty? And for this case could we have a formula in the TLA spec for consensus being reached after f+1 rounds?

Sure, we can add any number of MC_XZY files with different parameters.

ancazamfir · 2022-03-02T09:19:41Z

spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla

+        => \E v \in ValidValues, t \in Timestamps, pr \in Rounds, r1 \in Rounds, r2 \in Rounds : 
+            LET prop == Proposal(v,t,pr)
+            IN
+            /\ decision[p] = Decision(prop, r1)
+            /\ decision[q] = Decision(prop, r2)


Could you provide a "NonAgreementOnValue" so we can see some counterexamples? I tried ~AgreementOnValue but i get a trace on Init state (with NilDecision), also tried some other variants, like:

Suggested change

=> \E v \in ValidValues, t \in Timestamps, pr \in Rounds, r1 \in Rounds, r2 \in Rounds :

LET prop == Proposal(v,t,pr)

IN

/\ decision[p] = Decision(prop, r1)

/\ decision[q] = Decision(prop, r2)

=> \E v \in ValidValues, t \in Timestamps, pr \in Rounds, r1 \in Rounds, r2 \in Rounds :

LET prop == Proposal(v,t,pr)

IN

\/ decision[p] /= Decision(prop, r1)

\/ decision[q] /= Decision(prop, r2)

Right, the problem with your suggestion is that neither process is required to decide on a valid proposal, if it is written with just this disjunction. I think what you want is something along the lines of:

Suggested change

=> \E v \in ValidValues, t \in Timestamps, pr \in Rounds, r1 \in Rounds, r2 \in Rounds :

LET prop == Proposal(v,t,pr)

IN

/\ decision[p] = Decision(prop, r1)

/\ decision[q] = Decision(prop, r2)

=> \E p1 \in ValidProposals, p2 \in ValidProposals, r1 \in Rounds, r2 \in Rounds :

/\ p1 /= p2

/\ decision[p] = Decision(p1, r1)

/\ decision[q] = Decision(p2, r2)

That doesn't work either. I will keep trying but let me know if you come up with an invariant that fails.

ancazamfir · 2022-03-02T09:38:35Z

spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla

         ELSE NilProposal
       IN
-       BroadcastPrevote(p, round[p], mid) \* lines 24-26
+       BroadcastPrevote(p, r, mid) \* lines 24-26


Not clear to me that we prevote nil if msg is not timely. Maybe move the msg \in receivedTimelyProposal[p] check in LET mid...??

If msg is not timely, the entire action UponProposalInPropose is disabled.

But we want to prevote nil, right?

ancazamfir · 2022-03-02T09:54:31Z

spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla

 *)
-Next ==
+Next == 
  \/ AdvanceRealTime


Follow up on the deadlock, if I disable the deadlock check, in TLC actions I only see AdvanceRealTime (in addition to Init and Next). And a simple run (2 correct processes) never finishes.

Ah actually it did finish.

williambanfield · 2022-03-02T14:07:23Z

Going to merge for now and open separate PRs for additional changes to these files.

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>

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)

Migration of TLA+ files from the spec repo (#8004)

e449704

creachadair requested review from cmwaters, ebuchman, tychoish and williambanfield as code owners February 26, 2022 00:41

creachadair changed the title ~~Migration of TLA+ files from the spec repo (#8004)~~ MIgrate and integrate TLA+ files from the spec repo Feb 26, 2022

Merge branch 'master' into jk/pbtsSpec

ad3ea65

tychoish approved these changes Feb 28, 2022

View reviewed changes

williambanfield requested review from Kukovec, ancazamfir and cason February 28, 2022 23:08

Kukovec approved these changes Mar 1, 2022

View reviewed changes

M. J. Fromberger added 2 commits March 1, 2022 04:57

Merge branch 'master' into jk/pbtsSpec

27f39e4

Merge branch 'master' into jk/pbtsSpec

f3dc874

creachadair requested review from josef-widder and milosevic as code owners March 1, 2022 17:13

Merge branch 'master' into jk/pbtsSpec

8a8298b

ancazamfir reviewed Mar 2, 2022

View reviewed changes

williambanfield merged commit c42c6d0 into master Mar 2, 2022

williambanfield deleted the jk/pbtsSpec branch March 2, 2022 14:08

cason mentioned this pull request Jan 5, 2024

PBTS: migrating to main the new version of the specification cometbft/cometbft#1973

Merged

Conversation

creachadair commented Feb 26, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kukovec left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ancazamfir Mar 2, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Kukovec Mar 2, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

williambanfield commented Mar 2, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

creachadair commented Feb 26, 2022 •

edited

Loading

ancazamfir Mar 2, 2022 •

edited

Loading

Kukovec Mar 2, 2022 •

edited

Loading