mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-01-03 11:45:18 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'main' into wb/issue-9227

Browse Source
This commit is contained in:
William Banfield
2022-08-17 11:03:40 -04:00
committed by GitHub
parent 20fa59eaad 3003e05581
commit e15a65abec
15 changed files with 875 additions and 468 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
docs/rfc/README.md
View File

@@ -60,5 +60,6 @@ sections.
- [RFC-020: Onboarding Projects](./rfc-020-onboarding-projects.rst)
- [RFC-021: The Future of the Socket Protocol](./rfc-021-socket-protocol.md)
- [RFC-023: Semi-permanent Testnet](./rfc-023-semi-permanent-testnet.md)
- [RFC-024: Block Structure Consolidation](./rfc-024-block-structure-consolidation.md)
<!-- - [RFC-NNN: Title](./rfc-NNN-title.md) -->

364
docs/rfc/rfc-024-block-structure-consolidation.md Normal file
View File

@@ -0,0 +1,364 @@
# RFC 024: Block Structure Consolidation
## Changelog
- 19-Apr-2022: Initial draft started (@williambanfield).
- 3-May-2022: Initial draft complete (@williambanfield).
## Abstract
The `Block` data structure is a very central structure within Tendermint. Because
of its centrality, it has gained several fields over the years through accretion.
Not all of these fields may be necessary any more. This document examines which
of these fields may no longer be necessary for inclusion in the block and makes
recommendations about how to proceed with each of them.
## Background
The current block structure contains multiple fields that are not required for
validation or execution of a Tendermint block. Some of these fields had vestigial
purposes that they no longer serve and some of these fields exist as a result of
internal Tendermint domain objects leaking out into the external data structure.
In so far as is possible, we should consolidate and prune these superfluous
fields before releasing a 1.0 version of Tendermint. All pruning of these
fields should be done with the aim of simplifying the structures to what
is needed while preserving information that aids with debugging and that also
allow external protocols to function more efficiently than if they were removed.
### Current Block Structure
The current block structures are included here to aid discussion.
```proto
message Block {
Header header = 1;
Data data = 2;
tendermint.types.EvidenceList evidence = 3;
Commit last_commit = 4;
}
```
```proto
message Header {
tendermint.version.Consensus version = 1;
string chain_id = 2;
int64 height = 3;
google.protobuf.Timestamp time = 4;
BlockID last_block_id = 5;
bytes last_commit_hash = 6;
bytes data_hash = 7;
bytes validators_hash = 8;
bytes next_validators_hash = 9;
bytes consensus_hash = 10;
bytes app_hash = 11;
bytes last_results_hash = 12;
bytes evidence_hash = 13;
bytes proposer_address = 14;
}
```
```proto
message Data {
repeated bytes txs = 1;
}
```
```proto
message EvidenceList {
repeated Evidence evidence = 1;
}
```
```proto
message Commit {
int64 height = 1;
int32 round = 2;
BlockID block_id = 3;
repeated CommitSig signatures = 4;
}
```
```proto
message CommitSig {
BlockIDFlag block_id_flag = 1;
bytes validator_address = 2;
google.protobuf.Timestamp timestamp = 3;
bytes signature = 4;
}
```
```proto
message BlockID {
bytes hash = 1;
PartSetHeader part_set_header = 2;
}
```
### On Tendermint Blocks
#### What is a Tendermint 'Block'?
A block is the structure produced as the result of an instance of the Tendermint
consensus algorithm. At its simplest, the 'block' can be represented as a Merkle
root hash of all of the data used to construct and produce the hash. Our current
block proto structure includes _far_ from all of the data used to produce the
hashes included in the block.
It does not contain the full `AppState`, it does not contain the `ConsensusParams`,
nor the `LastResults`, nor the `ValidatorSet`. Additionally, the layout of
the block structure is not inherently tied to this Merkle root hash. Different
layouts of the same set of data could trivially be used to construct the
exact same hash. The thing we currently call the 'Block' is really just a view
into a subset of the data used to construct the root hash. Sections of the
structure can be modified as long as alternative methods exist to query and
retrieve the constituent values.
#### Why this digression?
This digression is aimed at informing what it means to consolidate 'fields' in the
'block'. The discussion of what should be included in the block can be teased
apart into a few different lines of inquiry.
1. What values need to be included as part of the Merkle tree so that the
consensus algorithm can use proof-of-stake consensus to validate all of the
properties of the chain that we would like?
2. How can we create views of the data that can be easily retrieved, stored, and
verified by the relevant protocols?
These two concerns are intertwined at the moment as a result of how we store
and propagate our data but they don't necessarily need to be. This document
focuses primarily on the first concern by suggesting fields that can be
completely removed without any loss in the function of our consensus algorithm.
This document also suggests ways that we may update our storage and propagation
mechanisms to better take advantage of Merkle tree nature of our data although
these are not its primary concern.
## Discussion
### Data to consider removing
This section proposes a list of data that could be completely removed from the
Merkle tree with no loss to the functionality of our consensus algorithm.
Where the change is possible but would hamper external protocols or make
debugging more difficult, that is noted in discussion.
#### CommitSig.Timestamp
This field contains the timestamp included in the precommit message that was
issued for the block. The field was once used to produce the timestamp of the block.
With the introduction of Proposer-Based Timestamps, This field is no longer used
in any Tendermint algorithms and can be completely removed.
#### CommitSig.ValidatorAddress
The `ValidatorAddress` is included in each `CommitSig` structure. This field
is hashed along with all of the other fields of the `CommitSig`s in the block
to form the `LastCommitHash` field in the `Header`. The `ValidatorAddress` is
somewhat redundant in the hash. Each validator has a unique position in the
`CommitSig` and the hash is built preserving this order. Therefore, the
information of which signature corresponds to which validator is included in
the root hash, even if the address is absent.
It's worth noting that the validator address could still be included in the
_hash_ even if it is absent from the `CommitSig` structure in the block by
simply hashing it locally at each validator but not including it in the block.
The reverse is also true. It would be perfectly possible to not include the
`ValidatorAddress` data in the `LastCommitHash` but still include the field in
the block.
#### BlockID.PartSetHeader
The [BlockID][block-id] field comprises the [PartSetHeader][part-set-header] and the hash of the block.
The `PartSetHeader` is used by nodes to gossip the block by dividing it into
parts. Nodes receive the `PartSetHeader` from their peers, informing them of
what pieces of the block to gather. There is no strong reason to include this
value in the block. Validators will still be able to gossip and validate the
blocks that they received from their peers using this mechanism even if it is
not written into the block. The `BlockID` can therefore be consolidated into
just the hash of the block. This is by far the most uncontroversial change
and there appears to be no good reason _not_ to do it. Further evidence that
the field is not meaningful can be found in the fact that the field is not
actually validated to ensure it is correct during block validation. Validation
only checks that the [field is well formed][psh-check].
#### ChainID
The `ChainID` is a string selected by the chain operators, usually a
human-readable name for the network. This value is immutable for the lifetime
of the chain and is defined in the genesis file. It is therefore hashed into the
original block and therefore transitively included as in the Merkle root hash of
every block. The redundant field is a candidate for removal from the root hash
of each block. However, aesthetically, it's somewhat nice to include in each
block, as if the block was 'stamped' with the ID. Additionally, re-validating
the value from genesis would be painful and require reconstituting potentially
large chains. I'm therefore mildly in favor of maintaining this redundant
piece of information. We pay almost no storage cost for maintaining this
identical data, so the only cost is in the time required to hash it into the
structure.
#### LastResultsHash
`LastResultsHash` is a hash covering the result of executing the transactions
from the previous block. It covers the response `Code`, `Data`, `GasWanted`,
and `GasUsed` with the aim of ensuring that execution of all of the transactions
was performed identically on each node. The data covered by this field _should_
be also reflected in the `AppHash`. The `AppHash` is provided by the application
and should be deterministically calculated by each node. This field could
therefore be removed on the grounds that its data is already reflected elsewhere.
I would advocate for keeping this field. This field provides an additional check
for determinism across nodes. Logic to update the application hash is more
complicated for developers to implement because it relies either on building a
complete view of the state of the application data. The `Results` returned by
the application contain simple response codes and deterministic data bytes.
Leaving the field will allow for transaction execution issues that are not
correctly reflected in the `AppHash` to be more completely diagnosed.
Take the case of mismatch of `LastResultsHash` between two nodes, A and B, where both
nodes report divergent values. If `A` and `B` both report
the same `AppHash`, then some non-deterministic behavior occurred that was not
accurately reflected in the `AppHash`. The issue caused by this
non-determinism may not show itself for several blocks, but catching the divergent
state earlier will improve the chances that a chain is able to recover.
#### ValidatorsHash
Both `ValidatorsHash` and `NextValidatorsHash` are included in the block
header. `Validatorshash` contains the hash of the [public key and voting power][val-hash]
of each validator in the active set for the current block and `NextValidatorsHash`
contains the same data but for the next height.
This data is effectively redundant. Having both values present in the block
structure is helpful for light client verification. The light client is able to
easily determine if two sequential blocks used the same validator set by querying
only one header.
`ValidatorsHash` is also important to the light client algorithm for performing block
validation. The light client uses this field to ensure that the validator set
it fetched from a full node is correct. It can be sure of the correctness of
the retrieved structure by hashing it and checking the hash against the `ValidatorsHash`
of the block it is verifying. Because a validator that the light client trusts
signed over the `ValidatorsHash`, it can be certain of the validity of the
structure. Without this check, phony validator sets could be handed to the light
client and the code tricked into believing a different validator set was present
at a height, opening up a major hole in the light client security model.
This creates a recursive problem. To verify the validator set that signed the
block at height `H`, what information do we need? We could fetch the
`NextValidatorsHash` from height `H-1`, but how do we verify that that hash is correct?
#### ProposerAddress
The section below details a change to allow the `ProposerAddress` to be calculated
from a field added to the block. This would allow the `Address` to be dropped
from the block. Consumers of the chain could run the proposer selection [algorithm][proposer-selection]
to determine who proposed each block.
I would advocate against this. Any consumer of the chain that wanted to
know which validator proposed a block would have to run the proposer selection
algorithm. This algorithm is not widely implemented, meaning that consumers
in other languages would need to implement the algorithm to determine a piece
of basic information about the chain.
### Data to consider adding
#### ProofOfLockRound
The *proof of lock round* is the round of consensus for a height in which the
Tendermint algorithm observed a super majority of voting power on the network for
a block.
Including this value in the block will allow validation of currently
un-validated metadata. Specifically, including this value will allow Tendermint
to validate that the `ProposerAddress` in the block is correct. Without knowing
the locked round number, Tendermint cannot calculate which validator was supposed
to propose a height. Because of this, our [validation logic][proposer-check] does not check that
the `ProposerAddress` included in the block corresponds to the validator that
proposed the height. Instead, the validation logic simply checks that the value
is an address of one of the known validators.
Currently, we maintain the _committed round_ in the `Commit` for height `H`, which is
written into the block at height `H+1`. This value corresponds to the round in
which the proposer of height `H+1` received the commit for height `H`. The proof
of lock round would not subsume this value.
### Additional possible updates
#### Updates to storage
Currently we store the [every piece of each block][save-block] in the `BlockStore`.
I suspect that this has lead to some mistakes in reasoning around the merits of
consolidating fields in the block. We could update the storage scheme we use to
store only some pieces of each block and still achieve a space savings without having
to change the block structure at all.
The main way to achieve this would be by _no longer saving data that does not change_.
At each height we save a set of data that is unlikely to have changed from the
previous height in the block structure, this includes the `ValidatorAddress`es,
the `ValidatorsHash`, the `ChainID`. These do not need to be saved along with
_each_ block. We could easily save the value and the height at which the value
was updated and construct each block using the data that existed at the time.
This document does not make any specific recommendations around storage since
that is likely to change with upcoming improvements to to the database infrastructure.
However, it's important to note that removing fields from the block for the
purposes of 'saving space' may not be that meaningful. We should instead focus
our attention of removing fields from the block that are no longer needed
for correct functioning of the protocol.
#### Updates to propagation
Block propagation suffers from the same issue that plagues block storage, we
propagate all of the contents of each block proto _even when these contents are redundant
or unchanged from previous blocks_. For example, we propagate the `ValidatorAddress`es
for each block in the `CommitSig` structure even when it never changed from a
previous height. We could achieve a speed-up in many cases by communicating the
hashes _first_ and letting peers request additional information when they do not
recognize the communicated hash.
For example, in the case of the `ValidatorAddress`es, the node would first
communicate the `ValidatorsHash` of the block to its peers. The peers would
check their storage for a validator set matching the provided hash. If the peer
has a matching set, it would populate its local block structure with the
appropriate values from its store. If peer did not have a matching set, it would
issue a request to its peers, either via P2P or RPC for the data it did not have.
Conceptually, this is very similar to how content addressing works in protocols
such as git where pushing a commit does not require pushing the entire contents
of the tree referenced by the commit.
### Impact on light clients
As outlined in the section [On Tendermint Blocks](#on-tendermint-blocks), there
is a distinction between what data is referenced in the Merkle root hash and the
contents of the proto structure we currently call the `Block`.
Any changes to the Merkle root hash will necessarily be breaking for legacy light clients.
Either a soft-upgrades scheme will need to be implemented or a hard fork will
be required for chains and light clients to function with the new hashes.
This means that all of the additions and deletions from the Merkle root hash
proposed by this document will be light client breaking.
Changes to the block structure alone are not necessarily light client breaking if the
data being hashed are identical and legacy views into the data are provided
for old light clients during transitions. For example, a newer version of the
block structure could move the `ValidatorAddress` field to a different field
in the block while still including it in the hashed data of the `LastCommitHash`.
As long as old light clients could still fetch the old data structure, then
this would not be light client breaking.
## References
[light-verify-trusting]: https://github.com/tendermint/tendermint/blob/208a15dadf01e4e493c187d8c04a55a61758c3cc/types/validation.go#L124
[part-set-header]: https://github.com/tendermint/tendermint/blob/208a15dadf01e4e493c187d8c04a55a61758c3cc/types/part_set.go#L94
[block-id]: https://github.com/tendermint/tendermint/blob/208a15dadf01e4e493c187d8c04a55a61758c3cc/types/block.go#L1090
[psh-check]: https://github.com/tendermint/tendermint/blob/208a15dadf01e4e493c187d8c04a55a61758c3cc/types/part_set.go#L116
[proposer-selection]: https://github.com/tendermint/tendermint/blob/208a15dadf01e4e493c187d8c04a55a61758c3cc/spec/consensus/proposer-selection.md
[chain-experiment]: https://github.com/williambanfield/tmtools/blob/master/hash-changes/RUN.txt
[val-hash]: https://github.com/tendermint/tendermint/blob/29e5fbcc648510e4763bd0af0b461aed92c21f30/types/validator.go#L160
[proposer-check]: https://github.com/tendermint/tendermint/blob/29e5fbcc648510e4763bd0af0b461aed92c21f30/internal/state/validation.go#L102
[save-block]: https://github.com/tendermint/tendermint/blob/59f0236b845c83009bffa62ed44053b04370b8a9/internal/store/store.go#L490

58
spec/light-client/accountability/MC_n4_f1.tla
View File

@@ -1,34 +1,38 @@
----------------------------- MODULE MC_n4_f1 -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
CONSTANT
\* @type: $round -> $process;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
\* @type: PROCESS -> ROUND;
round,
\* @type: PROCESS -> STEP;
step,
\* @type: PROCESS -> VALUE;
decision,
\* @type: PROCESS -> VALUE;
lockedValue,
\* @type: PROCESS -> ROUND;
lockedRound,
\* @type: PROCESS -> VALUE;
validValue,
\* @type: PROCESS -> ROUND;
validRound,
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit,
\* @type: Set(MESSAGE);
evidence,
\* @type: ACTION;
action
\* @type: $process -> $round;
round, \* a process round number: Corr -> Rounds
\* @type: $process -> $step;
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
\* @type: $process -> $value;
decision, \* process decision: Corr -> ValuesOrNil
\* @type: $process -> $value;
lockedValue, \* a locked value: Corr -> ValuesOrNil
\* @type: $process -> $round;
lockedRound, \* a locked round: Corr -> RoundsOrNil
\* @type: $process -> $value;
validValue, \* a valid value: Corr -> ValuesOrNil
\* @type: $process -> $round;
validRound, \* a valid round: Corr -> RoundsOrNil
\* @type: $round -> Set($proposeMsg);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set($proposeMsg);
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
\* @type: $action;
action \* we use this variable to see which action was taken
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2", "c3"},
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
=============================================================================
=============================================================================

58
spec/light-client/accountability/MC_n4_f2.tla
View File

@@ -1,34 +1,38 @@
----------------------------- MODULE MC_n4_f2 -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
CONSTANT
\* @type: $round -> $process;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
\* @type: PROCESS -> ROUND;
round,
\* @type: PROCESS -> STEP;
step,
\* @type: PROCESS -> VALUE;
decision,
\* @type: PROCESS -> VALUE;
lockedValue,
\* @type: PROCESS -> ROUND;
lockedRound,
\* @type: PROCESS -> VALUE;
validValue,
\* @type: PROCESS -> ROUND;
validRound,
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit,
\* @type: Set(MESSAGE);
evidence,
\* @type: ACTION;
action
\* @type: $process -> $round;
round, \* a process round number: Corr -> Rounds
\* @type: $process -> $step;
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
\* @type: $process -> $value;
decision, \* process decision: Corr -> ValuesOrNil
\* @type: $process -> $value;
lockedValue, \* a locked value: Corr -> ValuesOrNil
\* @type: $process -> $round;
lockedRound, \* a locked round: Corr -> RoundsOrNil
\* @type: $process -> $value;
validValue, \* a valid value: Corr -> ValuesOrNil
\* @type: $process -> $round;
validRound, \* a valid round: Corr -> RoundsOrNil
\* @type: $round -> Set($proposeMsg);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set($proposeMsg);
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
\* @type: $action;
action \* we use this variable to see which action was taken
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2"},
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
=============================================================================
=============================================================================

62
spec/light-client/accountability/MC_n4_f2_amnesia.tla
View File

@@ -1,40 +1,44 @@
---------------------- MODULE MC_n4_f2_amnesia -------------------------------
EXTENDS Sequences
CONSTANT
\* @type: ROUND -> PROCESS;
CONSTANT
\* @type: $round -> $process;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
\* @type: PROCESS -> ROUND;
round,
\* @type: PROCESS -> STEP;
step,
\* @type: PROCESS -> VALUE;
decision,
\* @type: PROCESS -> VALUE;
lockedValue,
\* @type: PROCESS -> ROUND;
lockedRound,
\* @type: PROCESS -> VALUE;
validValue,
\* @type: PROCESS -> ROUND;
validRound,
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit,
\* @type: Set(MESSAGE);
evidence,
\* @type: ACTION;
action
\* @type: $process -> $round;
round, \* a process round number: Corr -> Rounds
\* @type: $process -> $step;
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
\* @type: $process -> $value;
decision, \* process decision: Corr -> ValuesOrNil
\* @type: $process -> $value;
lockedValue, \* a locked value: Corr -> ValuesOrNil
\* @type: $process -> $round;
lockedRound, \* a locked round: Corr -> RoundsOrNil
\* @type: $process -> $value;
validValue, \* a valid value: Corr -> ValuesOrNil
\* @type: $process -> $round;
validRound, \* a valid round: Corr -> RoundsOrNil
\* @type: $round -> Set($proposeMsg);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set($proposeMsg);
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
\* @type: $action;
action \* we use this variable to see which action was taken
\* the variable declared in TendermintAccTrace3
VARIABLE
\* @type: TRACE;
\* @type: $trace;
toReplay
INSTANCE TendermintAccTrace_004_draft WITH
@@ -49,7 +53,7 @@ INSTANCE TendermintAccTrace_004_draft WITH
"UponProposalInPropose",
"UponProposalInPrevoteOrCommitAndPrevote",
"UponProposalInPrecommitNoDecision",
"OnRoundCatchup",
"OnRoundCatchup",
"UponProposalInPropose",
"UponProposalInPrevoteOrCommitAndPrevote",
"UponProposalInPrecommitNoDecision"
@@ -59,4 +63,4 @@ INSTANCE TendermintAccTrace_004_draft WITH
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
=============================================================================
=============================================================================

58
spec/light-client/accountability/MC_n4_f3.tla
View File

@@ -1,34 +1,38 @@
----------------------------- MODULE MC_n4_f3 -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
CONSTANT
\* @type: $round -> $process;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
\* @type: PROCESS -> ROUND;
round,
\* @type: PROCESS -> STEP;
step,
\* @type: PROCESS -> VALUE;
decision,
\* @type: PROCESS -> VALUE;
lockedValue,
\* @type: PROCESS -> ROUND;
lockedRound,
\* @type: PROCESS -> VALUE;
validValue,
\* @type: PROCESS -> ROUND;
validRound,
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit,
\* @type: Set(MESSAGE);
evidence,
\* @type: ACTION;
action
\* @type: $process -> $round;
round, \* a process round number: Corr -> Rounds
\* @type: $process -> $step;
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
\* @type: $process -> $value;
decision, \* process decision: Corr -> ValuesOrNil
\* @type: $process -> $value;
lockedValue, \* a locked value: Corr -> ValuesOrNil
\* @type: $process -> $round;
lockedRound, \* a locked round: Corr -> RoundsOrNil
\* @type: $process -> $value;
validValue, \* a valid value: Corr -> ValuesOrNil
\* @type: $process -> $round;
validRound, \* a valid round: Corr -> RoundsOrNil
\* @type: $round -> Set($proposeMsg);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set($proposeMsg);
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
\* @type: $action;
action \* we use this variable to see which action was taken
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1"},
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
=============================================================================
=============================================================================

58
spec/light-client/accountability/MC_n5_f1.tla
View File

@@ -1,34 +1,38 @@
----------------------------- MODULE MC_n5_f1 -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
CONSTANT
\* @type: $round -> $process;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
\* @type: PROCESS -> ROUND;
round,
\* @type: PROCESS -> STEP;
step,
\* @type: PROCESS -> VALUE;
decision,
\* @type: PROCESS -> VALUE;
lockedValue,
\* @type: PROCESS -> ROUND;
lockedRound,
\* @type: PROCESS -> VALUE;
validValue,
\* @type: PROCESS -> ROUND;
validRound,
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit,
\* @type: Set(MESSAGE);
evidence,
\* @type: ACTION;
action
\* @type: $process -> $round;
round, \* a process round number: Corr -> Rounds
\* @type: $process -> $step;
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
\* @type: $process -> $value;
decision, \* process decision: Corr -> ValuesOrNil
\* @type: $process -> $value;
lockedValue, \* a locked value: Corr -> ValuesOrNil
\* @type: $process -> $round;
lockedRound, \* a locked round: Corr -> RoundsOrNil
\* @type: $process -> $value;
validValue, \* a valid value: Corr -> ValuesOrNil
\* @type: $process -> $round;
validRound, \* a valid round: Corr -> RoundsOrNil
\* @type: $round -> Set($proposeMsg);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set($proposeMsg);
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
\* @type: $action;
action \* we use this variable to see which action was taken
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2", "c3", "c4"},
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
=============================================================================
=============================================================================

58
spec/light-client/accountability/MC_n5_f2.tla
View File

@@ -1,34 +1,38 @@
----------------------------- MODULE MC_n5_f2 -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
CONSTANT
\* @type: $round -> $process;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
\* @type: PROCESS -> ROUND;
round,
\* @type: PROCESS -> STEP;
step,
\* @type: PROCESS -> VALUE;
decision,
\* @type: PROCESS -> VALUE;
lockedValue,
\* @type: PROCESS -> ROUND;
lockedRound,
\* @type: PROCESS -> VALUE;
validValue,
\* @type: PROCESS -> ROUND;
validRound,
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit,
\* @type: Set(MESSAGE);
evidence,
\* @type: ACTION;
action
\* @type: $process -> $round;
round, \* a process round number: Corr -> Rounds
\* @type: $process -> $step;
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
\* @type: $process -> $value;
decision, \* process decision: Corr -> ValuesOrNil
\* @type: $process -> $value;
lockedValue, \* a locked value: Corr -> ValuesOrNil
\* @type: $process -> $round;
lockedRound, \* a locked round: Corr -> RoundsOrNil
\* @type: $process -> $value;
validValue, \* a valid value: Corr -> ValuesOrNil
\* @type: $process -> $round;
validRound, \* a valid round: Corr -> RoundsOrNil
\* @type: $round -> Set($proposeMsg);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set($proposeMsg);
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
\* @type: $action;
action \* we use this variable to see which action was taken
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2", "c3"},
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
=============================================================================
=============================================================================

58
spec/light-client/accountability/MC_n6_f1.tla
View File

@@ -1,34 +1,38 @@
----------------------------- MODULE MC_n6_f1 -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
CONSTANT
\* @type: $round -> $process;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
\* @type: PROCESS -> ROUND;
round,
\* @type: PROCESS -> STEP;
step,
\* @type: PROCESS -> VALUE;
decision,
\* @type: PROCESS -> VALUE;
lockedValue,
\* @type: PROCESS -> ROUND;
lockedRound,
\* @type: PROCESS -> VALUE;
validValue,
\* @type: PROCESS -> ROUND;
validRound,
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote,
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit,
\* @type: Set(MESSAGE);
evidence,
\* @type: ACTION;
action
\* @type: $process -> $round;
round, \* a process round number: Corr -> Rounds
\* @type: $process -> $step;
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
\* @type: $process -> $value;
decision, \* process decision: Corr -> ValuesOrNil
\* @type: $process -> $value;
lockedValue, \* a locked value: Corr -> ValuesOrNil
\* @type: $process -> $round;
lockedRound, \* a locked round: Corr -> RoundsOrNil
\* @type: $process -> $value;
validValue, \* a valid value: Corr -> ValuesOrNil
\* @type: $process -> $round;
validRound, \* a valid round: Corr -> RoundsOrNil
\* @type: $round -> Set($proposeMsg);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: $round -> Set($preMsg);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set($proposeMsg);
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
\* @type: $action;
action \* we use this variable to see which action was taken
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2", "c3", "c4", "c5"},
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
=============================================================================
=============================================================================

21
spec/light-client/accountability/TendermintAccDebug_004_draft.tla
View File

@@ -19,7 +19,9 @@ NFaultyPrecommits == 6 \* the number of injected faulty PRECOMMIT messages
\* rounds to sets of messages.
\* Importantly, there will be exactly k messages in the image of msgFun.
\* We use this action to produce k faults in an initial state.
\* @type: (ROUND -> Set(MESSAGE), Set(MESSAGE), Int) => Bool;
\* @type: ($round -> Set({ round: $round, a }),
\* Set({ round: $round, a }), Int)
\* => Bool;
ProduceFaults(msgFun, From, k) ==
\E f \in [1..k -> From]:
msgFun = [r \in Rounds |-> {m \in {f[i]: i \in 1..k}: m.round = r}]
@@ -33,10 +35,12 @@ InitNoFaults ==
/\ lockedRound = [p \in Corr |-> NilRound]
/\ validValue = [p \in Corr |-> NilValue]
/\ validRound = [p \in Corr |-> NilRound]
/\ msgsPropose = [r \in Rounds |-> EmptyMsgSet]
/\ msgsPrevote = [r \in Rounds |-> EmptyMsgSet]
/\ msgsPrecommit = [r \in Rounds |-> EmptyMsgSet]
/\ evidence = EmptyMsgSet
/\ msgsPropose = [r \in Rounds |-> {}]
/\ msgsPrevote = [r \in Rounds |-> {}]
/\ msgsPrecommit = [r \in Rounds |-> {}]
/\ evidencePropose = {}
/\ evidencePrevote = {}
/\ evidencePrecommit = {}
(*
A specialized version of Init that injects NFaultyProposals proposals,
@@ -60,7 +64,9 @@ InitFewFaults ==
[type: {"PROPOSAL"}, src: Faulty, round: Rounds,
proposal: Values, validRound: Rounds \cup {NilRound}],
NFaultyProposals)
/\ evidence = EmptyMsgSet
/\ evidencePropose = {}
/\ evidencePrevote = {}
/\ evidencePrecommit = {}
\* Add faults incrementally
NextWithFaults ==
@@ -68,7 +74,8 @@ NextWithFaults ==
\/ Next
\* or a faulty process sends a message
\//\ UNCHANGED <<round, step, decision, lockedValue,
lockedRound, validValue, validRound, evidence>>
lockedRound, validValue, validRound,
evidencePropose, evidencePrevote, evidencePrecommit>>
/\ \E p \in Faulty:
\E r \in Rounds:
\//\ UNCHANGED <<msgsPrevote, msgsPrecommit>>

111
spec/light-client/accountability/TendermintAccInv_004_draft.tla
View File

@@ -10,25 +10,22 @@
*)
EXTENDS TendermintAcc_004_draft
(************************** TYPE INVARIANT ***********************************)
(* first, we define the sets of all potential messages *)
\* @type: Set(PROPMESSAGE);
AllProposals ==
AllProposals ==
[type: {"PROPOSAL"},
src: AllProcs,
round: Rounds,
proposal: ValuesOrNil,
validRound: RoundsOrNil]
\* @type: Set(PREMESSAGE);
AllPrevotes ==
[type: {"PREVOTE"},
src: AllProcs,
round: Rounds,
id: ValuesOrNil]
\* @type: Set(PREMESSAGE);
AllPrecommits ==
[type: {"PRECOMMIT"},
src: AllProcs,
@@ -50,7 +47,9 @@ TypeOK ==
/\ BenignRoundsInMessages(msgsPrevote)
/\ msgsPrecommit \in [Rounds -> SUBSET AllPrecommits]
/\ BenignRoundsInMessages(msgsPrecommit)
/\ evidence \in SUBSET (AllProposals \union AllPrevotes \union AllPrecommits)
/\ evidencePropose \in SUBSET AllProposals
/\ evidencePrevote \in SUBSET AllPrevotes
/\ evidencePrecommit \in SUBSET AllPrecommits
/\ action \in {
"Init",
"InsertProposal",
@@ -69,13 +68,12 @@ TypeOK ==
EvidenceContainsMessages ==
\* evidence contains only the messages from:
\* msgsPropose, msgsPrevote, and msgsPrecommit
\A m \in evidence:
LET r == m.round
t == m.type
IN
CASE t = "PROPOSAL" -> m \in msgsPropose[r]
[] t = "PREVOTE" -> m \in msgsPrevote[r]
[] OTHER -> m \in msgsPrecommit[r]
/\ \A m \in evidencePropose:
m \in msgsPropose[m.round]
/\ \A m \in evidencePrevote:
m \in msgsPrevote[m.round]
/\ \A m \in evidencePrecommit:
m \in msgsPrecommit[m.round]
NoFutureMessagesForLargerRounds(p) ==
\* a correct process does not send messages for the future rounds
@@ -89,14 +87,14 @@ NoFutureMessagesForCurrentRound(p) ==
LET r == round[p] IN
/\ Proposer[r] = p \/ \A m \in msgsPropose[r]: m.src /= p
/\ \/ step[p] \in {"PREVOTE", "PRECOMMIT", "DECIDED"}
\/ \A m \in msgsPrevote[r]: m.src /= p
\/ \A m \in msgsPrevote[r]: m.src /= p
/\ \/ step[p] \in {"PRECOMMIT", "DECIDED"}
\/ \A m \in msgsPrecommit[r]: m.src /= p
\/ \A m \in msgsPrecommit[r]: m.src /= p
\* the correct processes never send future messages
AllNoFutureMessagesSent ==
\A p \in Corr:
/\ NoFutureMessagesForCurrentRound(p)
/\ NoFutureMessagesForCurrentRound(p)
/\ NoFutureMessagesForLargerRounds(p)
\* a correct process in the PREVOTE state has sent a PREVOTE message
@@ -105,9 +103,9 @@ IfInPrevoteThenSentPrevote(p) ==
\E m \in msgsPrevote[round[p]]:
/\ m.id \in ValidValues \cup { NilValue }
/\ m.src = p
AllIfInPrevoteThenSentPrevote ==
\A p \in Corr: IfInPrevoteThenSentPrevote(p)
\A p \in Corr: IfInPrevoteThenSentPrevote(p)
\* a correct process in the PRECOMMIT state has sent a PRECOMMIT message
IfInPrecommitThenSentPrecommit(p) ==
@@ -115,42 +113,44 @@ IfInPrecommitThenSentPrecommit(p) ==
\E m \in msgsPrecommit[round[p]]:
/\ m.id \in ValidValues \cup { NilValue }
/\ m.src = p
AllIfInPrecommitThenSentPrecommit ==
\A p \in Corr: IfInPrecommitThenSentPrecommit(p)
\A p \in Corr: IfInPrecommitThenSentPrecommit(p)
\* a process in the PRECOMMIT state has sent a PRECOMMIT message
IfInDecidedThenValidDecision(p) ==
step[p] = "DECIDED" <=> decision[p] \in ValidValues
AllIfInDecidedThenValidDecision ==
\A p \in Corr: IfInDecidedThenValidDecision(p)
\A p \in Corr: IfInDecidedThenValidDecision(p)
\* a decided process should have received a proposal on its decision
IfInDecidedThenReceivedProposal(p) ==
step[p] = "DECIDED" =>
\E r \in Rounds: \* r is not necessarily round[p]
/\ \E m \in msgsPropose[r] \intersect evidence:
/\ \E m \in msgsPropose[r] \intersect evidencePropose:
/\ m.src = Proposer[r]
/\ m.proposal = decision[p]
\* not inductive: /\ m.src \in Corr => (m.validRound <= r)
AllIfInDecidedThenReceivedProposal ==
\A p \in Corr:
IfInDecidedThenReceivedProposal(p)
IfInDecidedThenReceivedProposal(p)
\* a decided process has received two-thirds of precommit messages
IfInDecidedThenReceivedTwoThirds(p) ==
step[p] = "DECIDED" =>
\E r \in Rounds:
LET PV ==
{ m \in msgsPrecommit[r] \intersect evidence: m.id = decision[p] }
LET PV == {
m \in msgsPrecommit[r] \intersect evidencePrecommit:
m.id = decision[p]
}
IN
Cardinality(PV) >= THRESHOLD2
AllIfInDecidedThenReceivedTwoThirds ==
\A p \in Corr:
IfInDecidedThenReceivedTwoThirds(p)
IfInDecidedThenReceivedTwoThirds(p)
\* for a round r, there is proposal by the round proposer for a valid round vr
ProposalInRound(r, proposedVal, vr) ==
@@ -160,7 +160,7 @@ ProposalInRound(r, proposedVal, vr) ==
/\ m.validRound = vr
TwoThirdsPrevotes(vr, v) ==
LET PV == { mm \in msgsPrevote[vr] \intersect evidence: mm.id = v } IN
LET PV == { mm \in msgsPrevote[vr] \intersect evidencePrevote: mm.id = v } IN
Cardinality(PV) >= THRESHOLD2
\* if a process sends a PREVOTE, then there are three possibilities:
@@ -189,8 +189,9 @@ IfSentPrecommitThenReceivedTwoThirds ==
\A mpc \in msgsPrecommit[r]:
mpc.src \in Corr =>
\/ /\ mpc.id \in ValidValues
/\ LET PV ==
{ m \in msgsPrevote[r] \intersect evidence: m.id = mpc.id }
/\ LET PV == {
m \in msgsPrevote[r] \intersect evidencePrevote: m.id = mpc.id
}
IN
Cardinality(PV) >= THRESHOLD2
\/ /\ mpc.id = NilValue
@@ -208,22 +209,22 @@ IfSentPrecommitThenSentPrevote ==
\* there is a locked round if a only if there is a locked value
LockedRoundIffLockedValue(p) ==
(lockedRound[p] = NilRound) <=> (lockedValue[p] = NilValue)
AllLockedRoundIffLockedValue ==
\A p \in Corr:
LockedRoundIffLockedValue(p)
\* when a process locked a round, it must have sent a precommit on the locked value.
IfLockedRoundThenSentCommit(p) ==
lockedRound[p] /= NilRound
=> \E r \in { rr \in Rounds: rr <= round[p] }:
\E m \in msgsPrecommit[r]:
m.src = p /\ m.id = lockedValue[p]
AllIfLockedRoundThenSentCommit ==
\A p \in Corr:
IfLockedRoundThenSentCommit(p)
\* a process always locks the latest round, for which it has sent a PRECOMMIT
LatestPrecommitHasLockedRound(p) ==
LET pPrecommits ==
@@ -237,7 +238,7 @@ LatestPrecommitHasLockedRound(p) ==
IN
/\ lockedRound[p] = latest.round
/\ lockedValue[p] = latest.id
AllLatestPrecommitHasLockedRound ==
\A p \in Corr:
LatestPrecommitHasLockedRound(p)
@@ -245,7 +246,7 @@ AllLatestPrecommitHasLockedRound ==
\* Every correct process sends only one value or NilValue.
\* This test has quantifier alternation -- a threat to all decision procedures.
\* Luckily, the sets Corr and ValidValues are small.
\* @type: (ROUND, ROUND -> Set(PREMESSAGE)) => Bool;
\* @type: ($round, $round -> Set($preMsg)) => Bool;
NoEquivocationByCorrect(r, msgs) ==
\A p \in Corr:
\E v \in ValidValues \union {NilValue}:
@@ -254,22 +255,22 @@ NoEquivocationByCorrect(r, msgs) ==
\/ m.id = v
\* a proposer nevers sends two values
\* @type: (ROUND, ROUND -> Set(PROPMESSAGE)) => Bool;
\* @type: ($round, $round -> Set($proposeMsg)) => Bool;
ProposalsByProposer(r, msgs) ==
\* if the proposer is not faulty, it sends only one value
\E v \in ValidValues:
\A m \in msgs[r]:
\/ m.src \in Faulty
\/ m.src = Proposer[r] /\ m.proposal = v
AllNoEquivocationByCorrect ==
\A r \in Rounds:
/\ ProposalsByProposer(r, msgsPropose)
/\ NoEquivocationByCorrect(r, msgsPrevote)
/\ NoEquivocationByCorrect(r, msgsPrecommit)
/\ ProposalsByProposer(r, msgsPropose)
/\ NoEquivocationByCorrect(r, msgsPrevote)
/\ NoEquivocationByCorrect(r, msgsPrecommit)
\* construct the set of the message senders
\* @type: (Set(MESSAGE)) => Set(PROCESS);
\* @type: (Set({ src: $process, a })) => Set($process);
Senders(M) == { m.src: m \in M }
\* The final piece by Josef Widder:
@@ -286,15 +287,15 @@ PrecommitsLockValue ==
LET Prevotes == {m \in msgsPrevote[fr]: m.id = w}
IN
Cardinality(Senders(Prevotes)) < THRESHOLD2
\* a combination of all lemmas
Inv ==
/\ EvidenceContainsMessages
/\ AllNoFutureMessagesSent
/\ AllIfInPrevoteThenSentPrevote
/\ AllIfInPrecommitThenSentPrecommit
/\ AllIfInDecidedThenReceivedProposal
/\ AllIfInDecidedThenReceivedTwoThirds
/\ AllIfInDecidedThenReceivedProposal
/\ AllIfInDecidedThenReceivedTwoThirds
/\ AllIfInDecidedThenValidDecision
/\ AllLockedRoundIffLockedValue
/\ AllIfLockedRoundThenSentCommit
@@ -306,8 +307,8 @@ Inv ==
/\ PrecommitsLockValue
\* this is the inductive invariant we like to check
TypedInv == TypeOK /\ Inv
TypedInv == TypeOK /\ Inv
\* UNUSED FOR SAFETY
ValidRoundNotSmallerThanLockedRound(p) ==
validRound[p] >= lockedRound[p]
@@ -325,10 +326,10 @@ IfValidRoundThenTwoThirds(p) ==
\/ validRound[p] = NilRound
\/ LET PV == { m \in msgsPrevote[validRound[p]]: m.id = validValue[p] } IN
Cardinality(PV) >= THRESHOLD2
\* UNUSED FOR SAFETY
AllIfValidRoundThenTwoThirds ==
\A p \in Corr: IfValidRoundThenTwoThirds(p)
\A p \in Corr: IfValidRoundThenTwoThirds(p)
\* a valid round can be only set to a valid value that was proposed earlier
IfValidRoundThenProposal(p) ==
@@ -372,5 +373,5 @@ THEOREM AgreementWhenLessThanThirdFaulty ==
THEOREM AgreementOrFork ==
~FaultyQuorum /\ TypedInv => Accountability
=============================================================================
=============================================================================

12
spec/light-client/accountability/TendermintAccTrace_004_draft.tla
View File

@@ -3,22 +3,22 @@
When Apalache is running too slow and we have an idea of a counterexample,
we use this module to restrict the behaviors only to certain actions.
Once the whole trace is replayed, the system deadlocks.
Version 1.
Igor Konnov, 2020.
*)
EXTENDS Sequences, Apalache, TendermintAcc_004_draft
EXTENDS Sequences, Apalache, typedefs, TendermintAcc_004_draft
\* a sequence of action names that should appear in the given order,
\* excluding "Init"
CONSTANT
\* @type: TRACE;
CONSTANT
\* @type: $trace;
Trace
VARIABLE
\* @type: TRACE;
VARIABLE
\* @type: $trace;
toReplay
TraceInit ==

361
spec/light-client/accountability/TendermintAcc_004_draft.tla
View File

@@ -21,7 +21,7 @@
Byzantine processes can demonstrate arbitrary behavior, including
no communication. We show that if agreement is violated, then the Byzantine
processes demonstrate one of the two behaviors:
processes demonstrate one of the two behaviours:
- Equivocation: a Byzantine process may send two different values
in the same round.
@@ -29,6 +29,7 @@
- Amnesia: a Byzantine process may lock a value without unlocking
the previous value that it has locked in the past.
* Version 5. Refactor evidence, migrate to Apalache Type System 1.2.
* Version 4. Remove defective processes, fix bugs, collect global evidence.
* Version 3. Modular and parameterized definitions.
* Version 2. Bugfixes in the spec and an inductive invariant.
@@ -41,34 +42,34 @@ EXTENDS Integers, FiniteSets, typedefs
(********************* PROTOCOL PARAMETERS **********************************)
CONSTANTS
\* @type: Set(PROCESS);
Corr, \* the set of correct processes
\* @type: Set(PROCESS);
\* @type: Set($process);
Corr, \* the set of correct processes
\* @type: Set($process);
Faulty, \* the set of Byzantine processes, may be empty
\* @type: Int;
\* @type: Int;
N, \* the total number of processes: correct, defective, and Byzantine
\* @type: Int;
\* @type: Int;
T, \* an upper bound on the number of Byzantine processes
\* @type: Set(VALUE);
\* @type: Set($value);
ValidValues, \* the set of valid values, proposed both by correct and faulty
\* @type: Set(VALUE);
\* @type: Set($value);
InvalidValues, \* the set of invalid values, never proposed by the correct ones
\* @type: ROUND;
\* @type: $round;
MaxRound, \* the maximal round number
\* @type: ROUND -> PROCESS;
\* @type: $round -> $process;
Proposer \* the proposer function from Rounds to AllProcs
ASSUME(N = Cardinality(Corr \union Faulty))
(*************************** DEFINITIONS ************************************)
AllProcs == Corr \union Faulty \* the set of all processes
\* @type: Set(ROUND);
\* @type: Set($round);
Rounds == 0..MaxRound \* the set of potential rounds
\* @type: ROUND;
\* @type: $round;
NilRound == -1 \* a special value to denote a nil round, outside of Rounds
RoundsOrNil == Rounds \union {NilRound}
Values == ValidValues \union InvalidValues \* the set of all values
\* @type: VALUE;
\* @type: $value;
NilValue == "None" \* a special value for a nil round, outside of Values
ValuesOrNil == Values \union {NilValue}
@@ -83,106 +84,105 @@ IsValid(v) == v \in ValidValues
THRESHOLD1 == T + 1 \* at least one process is not faulty
THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
(********************* TYPE ANNOTATIONS FOR APALACHE **************************)
\* An empty set of messages
\* @type: Set(MESSAGE);
EmptyMsgSet == {}
(********************* PROTOCOL STATE VARIABLES ******************************)
VARIABLES
\* @type: PROCESS -> ROUND;
\* @type: $process -> $round;
round, \* a process round number: Corr -> Rounds
\* @type: PROCESS -> STEP;
\* @type: $process -> $step;
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
\* @type: PROCESS -> VALUE;
\* @type: $process -> $value;
decision, \* process decision: Corr -> ValuesOrNil
\* @type: PROCESS -> VALUE;
\* @type: $process -> $value;
lockedValue, \* a locked value: Corr -> ValuesOrNil
\* @type: PROCESS -> ROUND;
\* @type: $process -> $round;
lockedRound, \* a locked round: Corr -> RoundsOrNil
\* @type: PROCESS -> VALUE;
\* @type: $process -> $value;
validValue, \* a valid value: Corr -> ValuesOrNil
\* @type: PROCESS -> ROUND;
\* @type: $process -> $round;
validRound \* a valid round: Corr -> RoundsOrNil
\* book-keeping variables
VARIABLES
\* @type: ROUND -> Set(PROPMESSAGE);
\* @type: $round -> Set($proposeMsg);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: ROUND -> Set(PREMESSAGE);
\* @type: $round -> Set($preMsg);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: ROUND -> Set(PREMESSAGE);
\* @type: $round -> Set($preMsg);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set(MESSAGE);
evidence, \* the messages that were used by the correct processes to make transitions
\* @type: ACTION;
\* @type: Set($proposeMsg);
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
\* @type: Set($preMsg);
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
\* @type: $action;
action \* we use this variable to see which action was taken
(* to see a type invariant, check TendermintAccInv3 *)
(* to see a type invariant, check TendermintAccInv3 *)
\* a handy definition used in UNCHANGED
vars == <<round, step, decision, lockedValue, lockedRound,
validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit>>
validValue, validRound, msgsPropose, msgsPrevote, msgsPrecommit,
evidencePropose, evidencePrevote, evidencePrecommit>>
(********************* PROTOCOL INITIALIZATION ******************************)
\* @type: (ROUND) => Set(PROPMESSAGE);
\* @type: ($round) => Set($proposeMsg);
FaultyProposals(r) ==
[
type : {"PROPOSAL"},
type : {"PROPOSAL"},
src : Faulty,
round : {r},
proposal : Values,
round : {r},
proposal : Values,
validRound: RoundsOrNil
]
\* @type: Set(PROPMESSAGE);
\* @type: Set($proposeMsg);
AllFaultyProposals ==
[
type : {"PROPOSAL"},
type : {"PROPOSAL"},
src : Faulty,
round : Rounds,
proposal : Values,
round : Rounds,
proposal : Values,
validRound: RoundsOrNil
]
\* @type: (ROUND) => Set(PREMESSAGE);
\* @type: ($round) => Set($preMsg);
FaultyPrevotes(r) ==
[
type : {"PREVOTE"},
src : Faulty,
round: {r},
type : {"PREVOTE"},
src : Faulty,
round: {r},
id : Values
]
\* @type: Set(PREMESSAGE);
AllFaultyPrevotes ==
\* @type: Set($preMsg);
AllFaultyPrevotes ==
[
type : {"PREVOTE"},
src : Faulty,
round: Rounds,
type : {"PREVOTE"},
src : Faulty,
round: Rounds,
id : Values
]
\* @type: (ROUND) => Set(PREMESSAGE);
\* @type: ($round) => Set($preMsg);
FaultyPrecommits(r) ==
[
type : {"PRECOMMIT"},
src : Faulty,
round: {r},
type : {"PRECOMMIT"},
src : Faulty,
round: {r},
id : Values
]
\* @type: Set(PREMESSAGE);
\* @type: Set($preMsg);
AllFaultyPrecommits ==
[
type : {"PRECOMMIT"},
src : Faulty,
round: Rounds,
type : {"PRECOMMIT"},
src : Faulty,
round: Rounds,
id : Values
]
\* @type: (ROUND -> Set(MESSAGE)) => Bool;
\* @type: ($round -> Set({ round: Int, a })) => Bool;
BenignRoundsInMessages(msgfun) ==
\* the message function never contains a message for a wrong round
\A r \in Rounds:
@@ -204,50 +204,43 @@ Init ==
/\ BenignRoundsInMessages(msgsPropose)
/\ BenignRoundsInMessages(msgsPrevote)
/\ BenignRoundsInMessages(msgsPrecommit)
/\ evidence = EmptyMsgSet
/\ evidencePropose = {}
/\ evidencePrevote = {}
/\ evidencePrecommit = {}
/\ action = "Init"
(************************ MESSAGE PASSING ********************************)
\* @type: (PROCESS, ROUND, VALUE, ROUND) => Bool;
\* @type: ($process, $round, $value, $round) => Bool;
BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
LET
\* @type: PROPMESSAGE;
newMsg ==
[
type |-> "PROPOSAL",
src |-> pSrc,
LET newMsg == [
type |-> "PROPOSAL",
src |-> pSrc,
round |-> pRound,
proposal |-> pProposal,
proposal |-> pProposal,
validRound |-> pValidRound
]
]
IN
msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
\* @type: (PROCESS, ROUND, VALUE) => Bool;
\* @type: ($process, $round, $value) => Bool;
BroadcastPrevote(pSrc, pRound, pId) ==
LET
\* @type: PREMESSAGE;
newMsg ==
[
LET newMsg == [
type |-> "PREVOTE",
src |-> pSrc,
round |-> pRound,
src |-> pSrc,
round |-> pRound,
id |-> pId
]
]
IN
msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
\* @type: (PROCESS, ROUND, VALUE) => Bool;
\* @type: ($process, $round, $value) => Bool;
BroadcastPrecommit(pSrc, pRound, pId) ==
LET
\* @type: PREMESSAGE;
newMsg ==
[
LET newMsg == [
type |-> "PRECOMMIT",
src |-> pSrc,
round |-> pRound,
src |-> pSrc,
round |-> pRound,
id |-> pId
]
]
IN
msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
@@ -257,46 +250,42 @@ BroadcastPrecommit(pSrc, pRound, pId) ==
StartRound(p, r) ==
/\ step[p] /= "DECIDED" \* a decided process does not participate in consensus
/\ round' = [round EXCEPT ![p] = r]
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
\* lines 14-19, a proposal may be sent later
\* @type: (PROCESS) => Bool;
InsertProposal(p) ==
\* @type: $process => Bool;
InsertProposal(p) ==
LET r == round[p] IN
/\ p = Proposer[r]
/\ step[p] = "PROPOSE"
\* if the proposer is sending a proposal, then there are no other proposals
\* by the correct processes for the same round
/\ \A m \in msgsPropose[r]: m.src /= p
/\ \E v \in ValidValues:
LET
\* @type: VALUE;
proposal ==
IF validValue[p] /= NilValue
THEN validValue[p]
ELSE v
/\ \E v \in ValidValues:
LET proposal ==
IF validValue[p] /= NilValue
THEN validValue[p]
ELSE v
IN BroadcastProposal(p, round[p], proposal, validRound[p])
/\ UNCHANGED <<evidence, round, decision, lockedValue, lockedRound,
validValue, step, validRound, msgsPrevote, msgsPrecommit>>
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
validValue, step, validRound, msgsPrevote, msgsPrecommit,
evidencePropose, evidencePrevote, evidencePrecommit>>
/\ action' = "InsertProposal"
\* lines 22-27
UponProposalInPropose(p) ==
\E v \in Values:
/\ step[p] = "PROPOSE" (* line 22 *)
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
/\ LET msg == [
type |-> "PROPOSAL",
src |-> Proposer[round[p]],
round |-> round[p],
proposal |-> v,
round |-> round[p],
proposal |-> v,
validRound |-> NilRound
]
]
IN
/\ msg \in msgsPropose[round[p]] \* line 22
/\ evidence' = {msg} \union evidence
/\ evidencePropose' = {msg} \union evidencePropose
/\ LET mid == (* line 23 *)
IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
THEN Id(v)
@@ -305,28 +294,27 @@ UponProposalInPropose(p) ==
BroadcastPrevote(p, round[p], mid) \* lines 24-26
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
validValue, validRound, msgsPropose, msgsPrecommit>>
validValue, validRound, msgsPropose, msgsPrecommit,
evidencePrevote, evidencePrecommit>>
/\ action' = "UponProposalInPropose"
\* lines 28-33
\* lines 28-33
UponProposalInProposeAndPrevote(p) ==
\E v \in Values, vr \in Rounds:
/\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
/\ LET msg == [
type |-> "PROPOSAL",
src |-> Proposer[round[p]],
round |-> round[p],
proposal |-> v,
round |-> round[p],
proposal |-> v,
validRound |-> vr
]
]
IN
/\ msg \in msgsPropose[round[p]] \* line 28
/\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(v) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 28
/\ evidence' = PV \union {msg} \union evidence
/\ evidencePropose' = {msg} \union evidencePropose
/\ evidencePrevote' = PV \union evidencePrevote
/\ LET mid == (* line 29 *)
IF IsValid(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
THEN Id(v)
@@ -335,9 +323,10 @@ UponProposalInProposeAndPrevote(p) ==
BroadcastPrevote(p, round[p], mid) \* lines 24-26
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
validValue, validRound, msgsPropose, msgsPrecommit>>
validValue, validRound, msgsPropose, msgsPrecommit,
evidencePrecommit>>
/\ action' = "UponProposalInProposeAndPrevote"
\* lines 34-35 + lines 61-64 (onTimeoutPrevote)
UponQuorumOfPrevotesAny(p) ==
/\ step[p] = "PREVOTE" \* line 34 and 61
@@ -346,32 +335,31 @@ UponQuorumOfPrevotesAny(p) ==
LET Voters == { m.src: m \in MyEvidence } IN
\* compare the number of the unique voters against the threshold
/\ Cardinality(Voters) >= THRESHOLD2 \* line 34
/\ evidence' = MyEvidence \union evidence
/\ evidencePrevote' = MyEvidence \union evidencePrevote
/\ BroadcastPrecommit(p, round[p], NilValue)
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
validValue, validRound, msgsPropose, msgsPrevote>>
validValue, validRound, msgsPropose, msgsPrevote,
evidencePropose, evidencePrecommit>>
/\ action' = "UponQuorumOfPrevotesAny"
\* lines 36-46
UponProposalInPrevoteOrCommitAndPrevote(p) ==
\E v \in ValidValues, vr \in RoundsOrNil:
/\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
/\ LET msg == [
type |-> "PROPOSAL",
src |-> Proposer[round[p]],
round |-> round[p],
proposal |-> v,
round |-> round[p],
proposal |-> v,
validRound |-> vr
]
]
IN
/\ msg \in msgsPropose[round[p]] \* line 36
/\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(v) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
/\ evidence' = PV \union {msg} \union evidence
/\ evidencePrevote' = PV \union evidencePrevote
/\ evidencePropose' = {msg} \union evidencePropose
/\ IF step[p] = "PREVOTE"
THEN \* lines 38-41:
/\ lockedValue' = [lockedValue EXCEPT ![p] = v]
@@ -383,7 +371,8 @@ UponProposalInPrevoteOrCommitAndPrevote(p) ==
\* lines 42-43
/\ validValue' = [validValue EXCEPT ![p] = v]
/\ validRound' = [validRound EXCEPT ![p] = round[p]]
/\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote>>
/\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote,
evidencePrecommit>>
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
\* lines 47-48 + 65-67 (onTimeoutPrecommit)
@@ -393,40 +382,40 @@ UponQuorumOfPrecommitsAny(p) ==
LET Committers == { m.src: m \in MyEvidence } IN
\* compare the number of the unique committers against the threshold
/\ Cardinality(Committers) >= THRESHOLD2 \* line 47
/\ evidence' = MyEvidence \union evidence
/\ evidencePrecommit' = MyEvidence \union evidencePrecommit
/\ round[p] + 1 \in Rounds
/\ StartRound(p, round[p] + 1)
/\ StartRound(p, round[p] + 1)
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
validRound, msgsPropose, msgsPrevote, msgsPrecommit,
evidencePropose, evidencePrevote>>
/\ action' = "UponQuorumOfPrecommitsAny"
\* lines 49-54
\* lines 49-54
UponProposalInPrecommitNoDecision(p) ==
/\ decision[p] = NilValue \* line 49
/\ \E v \in ValidValues (* line 50*) , r \in Rounds, vr \in RoundsOrNil:
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
/\ LET msg == [
type |-> "PROPOSAL",
src |-> Proposer[r],
round |-> r,
proposal |-> v,
round |-> r,
proposal |-> v,
validRound |-> vr
]
]
IN
/\ msg \in msgsPropose[r] \* line 49
/\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(v) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 49
/\ evidence' = PV \union {msg} \union evidence
/\ evidencePrecommit' = PV \union evidencePrecommit
/\ evidencePropose' = evidencePropose \union { msg }
/\ decision' = [decision EXCEPT ![p] = v] \* update the decision, line 51
\* The original algorithm does not have 'DECIDED', but it increments the height.
\* We introduced 'DECIDED' here to prevent the process from changing its decision.
/\ step' = [step EXCEPT ![p] = "DECIDED"]
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
validRound, msgsPropose, msgsPrevote, msgsPrecommit,
evidencePrevote>>
/\ action' = "UponProposalInPrecommitNoDecision"
\* the actions below are not essential for safety, but added for completeness
\* lines 20-21 + 57-60
@@ -436,7 +425,8 @@ OnTimeoutPropose(p) ==
/\ BroadcastPrevote(p, round[p], NilValue)
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
validRound, decision, evidence, msgsPropose, msgsPrecommit>>
validRound, decision, msgsPropose, msgsPrecommit,
evidencePropose, evidencePrevote, evidencePrecommit>>
/\ action' = "OnTimeoutPropose"
\* lines 44-46
@@ -444,21 +434,30 @@ OnQuorumOfNilPrevotes(p) ==
/\ step[p] = "PREVOTE"
/\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(NilValue) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
/\ evidence' = PV \union evidence
/\ evidencePrevote' = PV \union evidencePrevote
/\ BroadcastPrecommit(p, round[p], Id(NilValue))
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
validRound, decision, msgsPropose, msgsPrevote>>
validRound, decision, msgsPropose, msgsPrevote,
evidencePropose, evidencePrecommit>>
/\ action' = "OnQuorumOfNilPrevotes"
\* lines 55-56
OnRoundCatchup(p) ==
\E r \in {rr \in Rounds: rr > round[p]}:
LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN
\E MyEvidence \in SUBSET RoundMsgs:
LET Faster == { m.src: m \in MyEvidence } IN
\E EvPropose \in SUBSET msgsPropose[r],
EvPrevote \in SUBSET msgsPrevote[r],
EvPrecommit \in SUBSET msgsPrecommit[r]:
LET \* @type: Set({ src: $process, a }) => Set($process);
Src(E) == { m.src: m \in E }
IN
LET Faster ==
Src(EvPropose) \union Src(EvPrevote) \union Src(EvPrecommit)
IN
/\ Cardinality(Faster) >= THRESHOLD1
/\ evidence' = MyEvidence \union evidence
/\ evidencePropose' = EvPropose \union evidencePropose
/\ evidencePrevote' = EvPrevote \union evidencePrevote
/\ evidencePrecommit' = EvPrecommit \union evidencePrecommit
/\ StartRound(p, r)
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
@@ -482,17 +481,24 @@ Next ==
\/ OnQuorumOfNilPrevotes(p)
\/ OnRoundCatchup(p)
(**************************** FORK SCENARIOS ***************************)
\* equivocation by a process p
EquivocationBy(p) ==
\E m1, m2 \in evidence:
/\ m1 /= m2
/\ m1.src = p
/\ m2.src = p
/\ m1.round = m2.round
/\ m1.type = m2.type
LET
\* @type: Set({ src: $process, a }) => Bool;
EquivocationIn(S) ==
\E m1, m2 \in S:
/\ m1 /= m2
/\ m1.src = p
/\ m2.src = p
/\ m1.round = m2.round
/\ m1.type = m2.type
IN
\/ EquivocationIn(evidencePropose)
\/ EquivocationIn(evidencePrevote)
\/ EquivocationIn(evidencePrecommit)
\* amnesic behavior by a process p
AmnesiaBy(p) ==
@@ -501,21 +507,20 @@ AmnesiaBy(p) ==
/\ \E v1, v2 \in ValidValues:
/\ v1 /= v2
/\ [
type |-> "PRECOMMIT",
type |-> "PRECOMMIT",
src |-> p,
round |-> r1,
round |-> r1,
id |-> Id(v1)
] \in evidence
] \in evidencePrecommit
/\ [
type |-> "PREVOTE",
type |-> "PREVOTE",
src |-> p,
round |-> r2,
round |-> r2,
id |-> Id(v2)
] \in evidence
] \in evidencePrevote
/\ \A r \in { rnd \in Rounds: r1 <= rnd /\ rnd < r2 }:
LET prevotes ==
{ m \in evidence:
m.type = "PREVOTE" /\ m.round = r /\ m.id = Id(v2) }
{ m \in evidencePrevote: m.round = r /\ m.id = Id(v2) }
IN
Cardinality(prevotes) < THRESHOLD2
@@ -545,7 +550,7 @@ Accountability ==
EquivocationBy(p) \/ AmnesiaBy(p)
(****************** FALSE INVARIANTS TO PRODUCE EXAMPLES ***********************)
\* This property is violated. You can check it to see how amnesic behavior
\* appears in the evidence variable.
NoAmnesia ==
@@ -562,12 +567,12 @@ NoAgreement ==
\A p, q \in Corr:
(p /= q /\ decision[p] /= NilValue /\ decision[q] /= NilValue)
=> decision[p] /= decision[q]
\* Either agreement holds, or the faulty processes indeed demonstrate amnesia.
\* This property is violated. A counterexample should demonstrate equivocation.
AgreementOrAmnesia ==
Agreement \/ (\A p \in Faulty: AmnesiaBy(p))
\* We expect this property to be violated. It shows us a protocol run,
\* where one faulty process demonstrates amnesia without equivocation.
\* However, the absence of amnesia
@@ -584,7 +589,7 @@ AmnesiaImpliesEquivocation ==
(*
This property is violated. You can check it to see that all correct processes
may reach MaxRound without making a decision.
may reach MaxRound without making a decision.
*)
NeverUndecidedInMaxRound ==
LET AllInMax == \A p \in Corr: round[p] = MaxRound
@@ -592,5 +597,5 @@ NeverUndecidedInMaxRound ==
IN
AllInMax => AllDecided
=============================================================================
=============================================================================

53
spec/light-client/accountability/typedefs.tla
View File

@@ -1,36 +1,27 @@
-------------------- MODULE typedefs ---------------------------
(*
@typeAlias: PROCESS = Str;
@typeAlias: VALUE = Str;
@typeAlias: STEP = Str;
@typeAlias: ROUND = Int;
@typeAlias: ACTION = Str;
@typeAlias: TRACE = Seq(Str);
@typeAlias: PROPMESSAGE =
[
type: STEP,
src: PROCESS,
round: ROUND,
proposal: VALUE,
validRound: ROUND
];
@typeAlias: PREMESSAGE =
[
type: STEP,
src: PROCESS,
round: ROUND,
id: VALUE
];
@typeAlias: MESSAGE =
[
type: STEP,
src: PROCESS,
round: ROUND,
proposal: VALUE,
validRound: ROUND,
id: VALUE
];
@typeAlias: process = Str;
@typeAlias: value = Str;
@typeAlias: step = Str;
@typeAlias: round = Int;
@typeAlias: action = Str;
@typeAlias: trace = Seq(Str);
@typeAlias: proposeMsg =
{
type: $step,
src: $process,
round: $round,
proposal: $value,
validRound: $round
};
@typeAlias: preMsg =
{
type: $step,
src: $process,
round: $round,
id: $value
};
*)
TypeAliases == TRUE
=============================================================================
=============================================================================

10
test/fuzz/oss-fuzz-build.sh Executable file
View File

@@ -0,0 +1,10 @@
#!/bin/bash
# This script is invoked by OSS-Fuzz to run fuzz tests against Tendermint core.
# See https://github.com/google/oss-fuzz/blob/master/projects/tendermint/build.sh
compile_go_fuzzer github.com/tendermint/tendermint/test/fuzz/mempool/v0 Fuzz mempool_v0_fuzzer
compile_go_fuzzer github.com/tendermint/tendermint/test/fuzz/mempool/v1 Fuzz mempool_v1_fuzzer
compile_go_fuzzer github.com/tendermint/tendermint/test/fuzz/p2p/addrbook Fuzz p2p_addrbook_fuzzer
compile_go_fuzzer github.com/tendermint/tendermint/test/fuzz/p2p/pex Fuzz p2p_pex_fuzzer
compile_go_fuzzer github.com/tendermint/tendermint/test/fuzz/p2p/secret_connection Fuzz p2p_secret_connection_fuzzer
compile_go_fuzzer github.com/tendermint/tendermint/test/fuzz/rpc/jsonrpc/server Fuzz rpc_jsonrpc_server_fuzzer