-
Notifications
You must be signed in to change notification settings - Fork 224
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes to TLA+ specs for model-based testing #546
Merged
Merged
Changes from 15 commits
Commits
Show all changes
16 commits
Select commit
Hold shift + click to select a range
26fb58e
#414 changes to TLA+ specs for model-based testing
andrey-kuprianov 2a2ebee
Lightclient_A_1.tla: add check for header from the future
andrey-kuprianov b479d59
Merge branch 'master' into andrey/mbt-spec-changes
andrey-kuprianov 85b8814
#414 fix testgen tester: wrong dir was removed
andrey-kuprianov 97844a6
#414 move history out of LightClient.tla into LightTests.tla
andrey-kuprianov 45ab864
#414 adapt apalache test runner to changes in specs
andrey-kuprianov ef474ff
#414 minor changes to model_based.rs
andrey-kuprianov 7edec1e
#579 fix validators sorting according to v.0.34 requirements
andrey-kuprianov 9c55866
#579 update CHANGELOG.md
andrey-kuprianov 702c87b
Merge branch 'andrey/valset_ordering' into andrey/mbt-spec-changes
andrey-kuprianov 43e4051
#579 sort validators correctly also in testgen
andrey-kuprianov 1f02ef0
Merge branch 'andrey/valset_ordering' into andrey/mbt-spec-changes
andrey-kuprianov 6ab98d3
#414 account for Igor's naming suggestions
andrey-kuprianov c1a421b
#414 copy and rename into Blockchain/Lightclient_002_draft.tla
andrey-kuprianov 3d8c480
Merge branch 'master' into andrey/mbt-spec-changes
andrey-kuprianov 65bd05a
#414 restore original Blockchain/Lightclient_A_1.tla
andrey-kuprianov File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
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
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
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
171 changes: 171 additions & 0 deletions
171
light-client/tests/support/model_based/Blockchain_002_draft.tla
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,171 @@ | ||
| ------------------------ MODULE Blockchain_002_draft ----------------------------- | ||
| (* | ||
| This is a high-level specification of Tendermint blockchain | ||
| that is designed specifically for the light client. | ||
| Validators have the voting power of one. If you like to model various | ||
| voting powers, introduce multiple copies of the same validator | ||
| (do not forget to give them unique names though). | ||
| *) | ||
| EXTENDS Integers, FiniteSets | ||
|
|
||
| Min(a, b) == IF a < b THEN a ELSE b | ||
|
|
||
| CONSTANT | ||
| AllNodes, | ||
| (* a set of all nodes that can act as validators (correct and faulty) *) | ||
| ULTIMATE_HEIGHT, | ||
| (* a maximal height that can be ever reached (modelling artifact) *) | ||
| TRUSTING_PERIOD | ||
| (* the period within which the validators are trusted *) | ||
|
|
||
| Heights == 1..ULTIMATE_HEIGHT (* possible heights *) | ||
|
|
||
| (* A commit is just a set of nodes who have committed the block *) | ||
| Commits == SUBSET AllNodes | ||
|
|
||
| (* The set of all block headers that can be on the blockchain. | ||
| This is a simplified version of the Block data structure in the actual implementation. *) | ||
| BlockHeaders == [ | ||
| height: Heights, | ||
| \* the block height | ||
| time: Int, | ||
| \* the block timestamp in some integer units | ||
| lastCommit: Commits, | ||
| \* the nodes who have voted on the previous block, the set itself instead of a hash | ||
| (* in the implementation, only the hashes of V and NextV are stored in a block, | ||
| as V and NextV are stored in the application state *) | ||
| VS: SUBSET AllNodes, | ||
| \* the validators of this bloc. We store the validators instead of the hash. | ||
| NextVS: SUBSET AllNodes | ||
| \* the validators of the next block. We store the next validators instead of the hash. | ||
| ] | ||
|
|
||
| (* A signed header is just a header together with a set of commits *) | ||
| LightBlocks == [header: BlockHeaders, Commits: Commits] | ||
|
|
||
| VARIABLES | ||
| now, | ||
| (* the current global time in integer units *) | ||
| blockchain, | ||
| (* A sequence of BlockHeaders, which gives us a bird view of the blockchain. *) | ||
| Faulty | ||
| (* A set of faulty nodes, which can act as validators. We assume that the set | ||
| of faulty processes is non-decreasing. If a process has recovered, it should | ||
| connect using a different id. *) | ||
|
|
||
| (* all variables, to be used with UNCHANGED *) | ||
| vars == <<now, blockchain, Faulty>> | ||
|
|
||
| (* The set of all correct nodes in a state *) | ||
| Corr == AllNodes \ Faulty | ||
|
|
||
| (* APALACHE annotations *) | ||
| a <: b == a \* type annotation | ||
|
|
||
| NT == STRING | ||
| NodeSet(S) == S <: {NT} | ||
| EmptyNodeSet == NodeSet({}) | ||
|
|
||
| BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}] | ||
|
|
||
| LBT == [header |-> BT, Commits |-> {NT}] | ||
| (* end of APALACHE annotations *) | ||
|
|
||
| (****************************** BLOCKCHAIN ************************************) | ||
|
|
||
| (* the header is still within the trusting period *) | ||
| InTrustingPeriod(header) == | ||
| now < header.time + TRUSTING_PERIOD | ||
|
|
||
| (* | ||
| Given a function pVotingPower \in D -> Powers for some D \subseteq AllNodes | ||
| and pNodes \subseteq D, test whether the set pNodes \subseteq AllNodes has | ||
| more than 2/3 of voting power among the nodes in D. | ||
| *) | ||
| TwoThirds(pVS, pNodes) == | ||
| LET TP == Cardinality(pVS) | ||
| SP == Cardinality(pVS \intersect pNodes) | ||
| IN | ||
| 3 * SP > 2 * TP \* when thinking in real numbers, not integers: SP > 2.0 / 3.0 * TP | ||
|
|
||
| (* | ||
| Given a set of FaultyNodes, test whether the voting power of the correct nodes in D | ||
| is more than 2/3 of the voting power of the faulty nodes in D. | ||
| *) | ||
| IsCorrectPower(pFaultyNodes, pVS) == | ||
| LET FN == pFaultyNodes \intersect pVS \* faulty nodes in pNodes | ||
| CN == pVS \ pFaultyNodes \* correct nodes in pNodes | ||
| CP == Cardinality(CN) \* power of the correct nodes | ||
| FP == Cardinality(FN) \* power of the faulty nodes | ||
| IN | ||
| \* CP + FP = TP is the total voting power, so we write CP > 2.0 / 3 * TP as follows: | ||
| CP > 2 * FP \* Note: when FP = 0, this implies CP > 0. | ||
|
|
||
| (* This is what we believe is the assumption about failures in Tendermint *) | ||
| FaultAssumption(pFaultyNodes, pNow, pBlockchain) == | ||
| \A h \in Heights: | ||
| pBlockchain[h].time + TRUSTING_PERIOD > pNow => | ||
| IsCorrectPower(pFaultyNodes, pBlockchain[h].NextVS) | ||
|
|
||
| (* Can a block be produced by a correct peer, or an authenticated Byzantine peer *) | ||
| IsLightBlockAllowedByDigitalSignatures(ht, block) == | ||
| \/ block.header = blockchain[ht] \* signed by correct and faulty (maybe) | ||
| \/ block.Commits \subseteq Faulty /\ block.header.height = ht /\ block.header.time >= 0 \* signed only by faulty | ||
|
|
||
| (* | ||
| Initialize the blockchain to the ultimate height right in the initial states. | ||
| We pick the faulty validators statically, but that should not affect the light client. | ||
| *) | ||
| InitToHeight == | ||
| /\ Faulty \in SUBSET AllNodes \* some nodes may fail | ||
| \* pick the validator sets and last commits | ||
| /\ \E vs, lastCommit \in [Heights -> SUBSET AllNodes]: | ||
| \E timestamp \in [Heights -> Int]: | ||
| \* now is at least as early as the timestamp in the last block | ||
| /\ \E tm \in Int: now = tm /\ tm >= timestamp[ULTIMATE_HEIGHT] | ||
| \* the genesis starts on day 1 | ||
| /\ timestamp[1] = 1 | ||
| /\ vs[1] = AllNodes | ||
| /\ lastCommit[1] = EmptyNodeSet | ||
| /\ \A h \in Heights \ {1}: | ||
| /\ lastCommit[h] \subseteq vs[h - 1] \* the non-validators cannot commit | ||
| /\ TwoThirds(vs[h - 1], lastCommit[h]) \* the commit has >2/3 of validator votes | ||
| /\ IsCorrectPower(Faulty, vs[h]) \* the correct validators have >2/3 of power | ||
| /\ timestamp[h] > timestamp[h - 1] \* the time grows monotonically | ||
| /\ timestamp[h] < timestamp[h - 1] + TRUSTING_PERIOD \* but not too fast | ||
| \* form the block chain out of validator sets and commits (this makes apalache faster) | ||
| /\ blockchain = [h \in Heights |-> | ||
| [height |-> h, | ||
| time |-> timestamp[h], | ||
| VS |-> vs[h], | ||
| NextVS |-> IF h < ULTIMATE_HEIGHT THEN vs[h + 1] ELSE AllNodes, | ||
| lastCommit |-> lastCommit[h]] | ||
| ] \****** | ||
|
|
||
|
|
||
| (* is the blockchain in the faulty zone where the Tendermint security model does not apply *) | ||
| InFaultyZone == | ||
| ~FaultAssumption(Faulty, now, blockchain) | ||
|
|
||
| (********************* BLOCKCHAIN ACTIONS ********************************) | ||
| (* | ||
| Advance the clock by zero or more time units. | ||
| *) | ||
| AdvanceTime == | ||
| \E tm \in Int: tm >= now /\ now' = tm | ||
| /\ UNCHANGED <<blockchain, Faulty>> | ||
|
|
||
| (* | ||
| One more process fails. As a result, the blockchain may move into the faulty zone. | ||
| The light client is not using this action, as the faults are picked in the initial state. | ||
| However, this action may be useful when reasoning about fork detection. | ||
| *) | ||
| OneMoreFault == | ||
| /\ \E n \in AllNodes \ Faulty: | ||
| /\ Faulty' = Faulty \cup {n} | ||
| /\ Faulty' /= AllNodes \* at least process remains non-faulty | ||
| /\ UNCHANGED <<now, blockchain>> | ||
| ============================================================================= | ||
| \* Modification History | ||
| \* Last modified Wed Jun 10 14:10:54 CEST 2020 by igor | ||
| \* Created Fri Oct 11 15:45:11 CEST 2019 by igor |
This file was deleted.
Oops, something went wrong.
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
Oops, something went wrong.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I see the
<=actually appears to contradict the english spec which saysSo it seems clear that what we ant is "less than", but perhaps this inconsistency was due in part to the wording and terminology here. E.g., in this paragraph
"trust period" is spoken of as a duration that the header needs to be within not as a limit point that the header time needs to be less than. I wonder if calling this
TRUST_PERIOD_LIMITmight help prevent such confusion i the future. I suspect a problem with the current wording may arise due to "trusting period" sounds like a span within which things are valid, when it's actually meant to be the outer limit beyond which things are invalid. iiuc, the trust period is that span of time up to but not including the limit.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You are right:
<=does contradict the English spec, so this is the TLA+ modeling artifact. That there can be ambiguities in the English spec, that's of course possible -- English is not a formal language after all;) I still think that our English spec does an amazing job of clarifying the requirements at the semi-formal (and as close to formal as possible) level. But exactly because of this non-strictness of the English language the TLA+ spec should, in my opinion, be the ultimate source of truth for all parties.One of the things we were discussing with @josef-widder and @konnov is that now, when we have the three artifacts: the English spec, the TLA+ spec, and the implementation, and also now that we have the MBT, which serves as the "missing link" helping to synchronize them, we need to establish a process (in the VDD sense) that will help us to resolve the conflicts.
In this PR I've fixed the TLA+ spec, because it was the most easy way for me to go, but it's not clear at all whether that's the right thing to do. We need to figure out a joint understanding between the research and the development teams on how to proceed in such cases.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In this case, given the larger context, I don't believe it matters much whether we use < or <= here since we are dealing with time and already assume clocks can drift some amount. The important thing is that
TRUST_PERIODis a fraction of theUNBONDING_PERIOD. This ensures that light clients have the duration ofUNBONDING_PERIOD - TRUST_PERIODto try and submit evidence to the chain and get faulty validators punished. And since all these periods are on the order of days/weeks, the < vs. <= here shouldn't make a difference in the end.Also while UNBONDING_PERIOD is a global consensus parameter (all nodes agree on), the TRUST_PERIOD is not, it's a local subjective parameter that clients can set depending on their risk tolerance. So again, the plank second difference between
<and<=shouldn't matter there.Of course that might be an unsatisfactory answer - I don't mean to be flippant about it and we should certainly be consistent and precise, but it's important to keep the practical context in mind so we know what details are most important to focus on. Of course this is just input from my feeble human mind so possibly machine will prove that it does matter, but thought it was worth providing the extra context here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the feedback! I totally agree, from the practical perspective these differences between
<and<=do not matter at all in this particular context, so this case we could fix however we like, and it would make no real difference. There are two things to keep in mind though:Also I tend to perceive us having this problem as rather a good thing, demonstrating that from now on we will have a living specification, which is in sync with the implementation.
This is only the input from another feeble human mind, just a bit different;) And I am sure fixing this will not take much of either our focus or time.