diff --git a/.markdownlint.yml b/.markdownlint.yml index 6b4e78a33..baa78a116 100644 --- a/.markdownlint.yml +++ b/.markdownlint.yml @@ -6,3 +6,6 @@ MD024: { siblings_only: true } MD025: false MD033: false MD036: false +MD010: false +MD012: false +MD028: false diff --git a/README.md b/README.md index dcadaf9ce..9ce38ed5a 100644 --- a/README.md +++ b/README.md @@ -24,15 +24,15 @@ maintained by Informal Systems. ### P2P and Network Protocols -- [The Base P2P Layer](./p2p/node.md): multiplex the protocols ("reactors") on authenticated and encrypted TCP connections +- [The Base P2P Layer](./spec/p2p/node.md): multiplex the protocols ("reactors") on authenticated and encrypted TCP connections #### P2P Messages -- [Peer Exchange (PEX)](./p2p/messages/pex.md): gossip known peer addresses so peers can find each other -- [Block Sync](./p2p/messages/block_sync.md): gossip blocks so peers can catch up quickly -- [Consensus](./p2p/messages/consensus.md): gossip votes and block parts so new blocks can be committed -- [Mempool](./p2p/messages/mempool.md): gossip transactions so they get included in blocks -- [Evidence](./p2p/messages/evidence.md): sending invalid evidence will stop the peer +- [Peer Exchange (PEX)](./spec/p2p/messages/pex.md): gossip known peer addresses so peers can find each other +- [Block Sync](./spec/p2p/messages/block-sync.md): gossip blocks so peers can catch up quickly +- [Consensus](./spec/p2p/messages/consensus.md): gossip votes and block parts so new blocks can be committed +- [Mempool](./spec/p2p/messages/mempool.md): gossip transactions so they get included in blocks +- [Evidence](./spec/p2p/messages/evidence.md): sending invalid evidence will stop the peer ### ABCI diff --git a/ivy-proofs/README.md b/ivy-proofs/README.md index 80dc0ce7b..00a4bed25 100644 --- a/ivy-proofs/README.md +++ b/ivy-proofs/README.md @@ -1,9 +1,14 @@ -``` +# Ivy Proofs + +```copyright Copyright (c) 2020 Galois, Inc. SPDX-License-Identifier: Apache-2.0 ``` +## Contents + This folder contains: + * `tendermint.ivy`, a specification of Tendermint algorithm as described in *The latest gossip on BFT consensus* by E. Buchman, J. Kwon, Z. Milosevic. * `abstract_tendermint.ivy`, a more abstract specification of Tendermint that is more verification-friendly. * `classic_safety.ivy`, a proof that Tendermint satisfies the classic safety property of BFT consensus: if every two quorums have a well-behaved node in common, then no two well-behaved nodes ever disagree. @@ -17,7 +22,8 @@ All specifications and proofs are written in [Ivy](https://github.com/kenmcmil/i The license above applies to all files in this folder. -# Building and running +## Building and running + The easiest way to check the proofs is to use [Docker](https://www.docker.com/). 1. Install [Docker](https://docs.docker.com/get-docker/) and [Docker Compose](https://docs.docker.com/compose/install/). diff --git a/rfc/004-abci++.md b/rfc/004-abci++.md index 6ed2bffdf..61106ecab 100644 --- a/rfc/004-abci++.md +++ b/rfc/004-abci++.md @@ -42,6 +42,7 @@ This phase aims to allow applications to require their validators do more than j Example usecases of this include validator determined price oracles, validator guaranteed IBC connection attempts, and validator based threshold crypto. This adds an app-determined data field that every validator must include with their vote, and these will thus appear in the header. + #### Rename {BeginBlock, [DeliverTx], EndBlock} to FinalizeBlock The prior phases gives the application more flexibility in their execution model for a block, and they obsolete the current methods for how the consensus engine relates the block data to the state machine. Thus we refactor the existing methods to better reflect what is happening in the new ABCI model. @@ -185,7 +186,7 @@ We go through this phase by phase. ##### Prepare proposal IPC overhead -This requires a round of IPC communication, where both directions are quite large. Namely the proposer communicating an entire block to the application. +This requires a round of IPC communication, where both directions are quite large. Namely the proposer communicating an entire block to the application. However, this can be mitigated by splitting up `PrepareProposal` into two distinct, async methods, one for the block IPC communication, and one for the Header IPC communication. Then for chains where the block data does not depend on the header data, the block data IPC communication can proceed in parallel to the prior block's voting phase. (As a node can know whether or not its the leader in the next round) diff --git a/rfc/005-reverse-sync.md b/rfc/005-reverse-sync.md index 339b9d9fb..2b4eb6e5f 100644 --- a/rfc/005-reverse-sync.md +++ b/rfc/005-reverse-sync.md @@ -40,6 +40,7 @@ other data retrieving protocols (i.e. fast sync and state sync), we call this method **ReverseSync**. We will define the mechanism in four sections: + - Usage - Design - Verification @@ -107,6 +108,7 @@ also doesn't need to rely on RPC. ### Verification ReverseSync is used to fetch the following data structures: + - `Header` - `Commit` - `ValidatorSet` @@ -115,21 +117,24 @@ Nodes will also need to be able to verify these. This can be achieved by first retrieving the header at the base height from the block store. From this trusted header, the node hashes each of the three data structures and checks that they are correct. -1. The trusted header's last block ID matches the hash of the new header -```go -header[height].LastBlockID == hash(header[height-1]) -``` +1. The trusted header's last block ID matches the hash of the new header + + ```go + header[height].LastBlockID == hash(header[height-1]) + ``` 2. The trusted header's last commit hash matches the hash of the new commit -```go -header[height].LastCommitHash == hash(commit[height-1]) -``` + + ```go + header[height].LastCommitHash == hash(commit[height-1]) + ``` 3. Given that the node now trusts the new header, check that the header's validator set -hash matches the hash of the validator set -```go -header[height-1].ValidatorsHash == hash(validatorSet[height-1]) -``` + hash matches the hash of the validator set + + ```go + header[height-1].ValidatorsHash == hash(validatorSet[height-1]) + ``` ### Termination @@ -145,7 +150,7 @@ processes current block. This implies that we can't guarantee adequate history and thus the term "invariant" can't be used in the strictest sense. In the case that the first -condition isn't met, the node will log an error and optimistically attempt +condition isn't met, the node will log an error and optimistically attempt to continue with either fast sync or consensus. ## Alternative Solutions @@ -161,13 +166,13 @@ As it stands, if 2/3+ vote on evidence you can't verify, in the same manner if app hash), the node will halt. Another alternative is the method with which the relevant data is retrieved. -Instead of introducing new messages to the P2P layer, RPC could have been used +Instead of introducing new messages to the P2P layer, RPC could have been used instead. The aforementioned data is already available via the following RPC endpoints: `/commit` for `Header`'s' and `/validators` for `ValidatorSet`'s'. It was decided predominantly due to the instability of the current RPC infrastructure -that P2P be used instead. +that P2P be used instead. ## Status diff --git a/spec/consensus/proposer-based-timestamp/README.md b/spec/consensus/proposer-based-timestamp/README.md index ae7ec2337..82421d99d 100644 --- a/spec/consensus/proposer-based-timestamp/README.md +++ b/spec/consensus/proposer-based-timestamp/README.md @@ -3,7 +3,8 @@ This section describes a version of the Tendermint consensus protocol, which uses proposer-based timestamps. -## Contents +## Contents + - [Proposer-Based Time][main] (entry point) - [Part I - System Model and Properties][sysmodel] - [Part II - Protocol Specification][algorithm] diff --git a/spec/consensus/proposer-based-timestamp/pbts-algorithm_001_draft.md b/spec/consensus/proposer-based-timestamp/pbts-algorithm_001_draft.md index 8162e461e..9791ff86b 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-algorithm_001_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-algorithm_001_draft.md @@ -6,16 +6,19 @@ The algorithm in the [arXiv paper][arXiv] evaluates rules of the received messages without making explicit how these messages are received. In our solution, we will make some message filtering explicit. We will assume that there are message reception steps (where messages are received and possibly stored locally for later evaluation of rules) and processing steps (the latter roughly as described in a way similar to the pseudo code of the arXiv paper). -In contrast to the original algorithm the field `proposal` in the `PROPOSE` message is a pair `(v, time)`, of the proposed consensus value `v` and the proposed time `time`. +In contrast to the original algorithm the field `proposal` in the `PROPOSE` message is a pair `(v, time)`, of the proposed consensus value `v` and the proposed time `time`. #### **[PBTS-RECEPTION-STEP.0]** In the reception step at process `p` at local time `now_p`, upon receiving a message `m`: + - if the message `m` is of type `PROPOSE` and satisfies `now_p - PRECISION < m.time < now_p + PRECISION + MSGDELAY`, then mark the message as `timely` + > if `m` does not satisfy the constraint consider it `untimely` - + #### **[PBTS-PROCESSING-STEP.0]** + In the processing step, based on the messages stored, the rules of the algorithms are executed. Note that the processing step only operates on messages for the current height. The consensus algorithm rules are defined by the following updates to arXiv paper. @@ -23,6 +26,7 @@ for the current height. The consensus algorithm rules are defined by the followi #### New `StartRound` There are two additions + - in case the proposer's local time is smaller than the time of the previous block, the proposer waits until this is not the case anymore (to ensure the block time is monotonically increasing) - the proposer sends its time `now_p` as part of its proposal @@ -35,11 +39,12 @@ We update the timeout for the `PROPOSE` step according to the following reasonin So we should set the timeout to `max(timeoutPropose(round_p), waitingTime)`. -> If, in the future, a block delay parameter `BLOCKDELAY` is introduced, this means -that the proposer should wait for `now_p > blockTime + BLOCKDELAY` before sending a `PROPOSE` message. +> If, in the future, a block delay parameter `BLOCKDELAY` is introduced, this means +that the proposer should wait for `now_p > blockTime + BLOCKDELAY` before sending a `PROPOSE` message. Also, `BLOCKDELAY` needs to be added to `waitingTime`. #### **[PBTS-ALG-STARTROUND.0]** + ```go function StartRound(round) { blockTime ← block time of block h_p - 1 @@ -68,6 +73,7 @@ function StartRound(round) { - the code changes as the `PROPOSAL` message carries time (while `lockedValue` does not) #### **[PBTS-ALG-UPON-PROP.0]** + ```go upon timely(⟨PROPOSAL, h_p, round_p, (v,t), −1⟩) from proposer(h_p, round_p) while step_p = propose do { if valid(v) ∧ (lockedRound_p = −1 ∨ lockedValue_p = v) { @@ -82,12 +88,13 @@ upon timely(⟨PROPOSAL, h_p, round_p, (v,t), −1⟩) from proposer(h_p, round_ #### New Rule Replacing Lines 28 - 33 -In case consensus is not reached in round 1, in `StartRound` the proposer of future rounds may propose the same value but with a different time. -Thus, the time `tprop` in the `PROPOSAL` message need not match the time `tvote` in the (old) `PREVOTE` messages. -A validator may send `PREVOTE` for the current round as long as the value `v` matches. +In case consensus is not reached in round 1, in `StartRound` the proposer of future rounds may propose the same value but with a different time. +Thus, the time `tprop` in the `PROPOSAL` message need not match the time `tvote` in the (old) `PREVOTE` messages. +A validator may send `PREVOTE` for the current round as long as the value `v` matches. This gives the following rule: #### **[PBTS-ALG-OLD-PREVOTE.0]** + ```go upon timely(⟨PROPOSAL, h_p, round_p, (v, tprop), vr⟩) from proposer(h_p, round_p) AND 2f + 1 ⟨PREVOTE, h_p, vr, id((v, tvote)⟩ while step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do { @@ -107,6 +114,7 @@ while step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do { - the stored values (i.e., `lockedValue`, `validValue`) do not contain the time #### **[PBTS-ALG-NEW-PREVOTE.0]** + ```go upon timely(⟨PROPOSAL, h_p, round_p, (v,t), ∗⟩) from proposer(h_p, round_p) AND 2f + 1 ⟨PREVOTE, h_p, round_p, id(v,t)⟩ while valid(v) ∧ step_p ≥ prevote for the first time do { if step_p = prevote { @@ -121,11 +129,14 @@ upon timely(⟨PROPOSAL, h_p, round_p, (v,t), ∗⟩) from proposer(h_p, round_p ``` #### New Rule Replacing Lines 49 - 54 + - we decide on `v` as well as on the time from the proposal message -- here we do not care whether the proposal was received timely. +- here we do not care whether the proposal was received timely. + > In particular we need to take care of the case where the proposer is untimely to one correct validator only. We need to ensure that this validator decides if all decide. #### **[PBTS-ALG-DECIDE.0]** + ```go upon ⟨PROPOSAL, h_p, r, (v,t), ∗⟩ from proposer(h_p, r) AND 2f + 1 ⟨PRECOMMIT, h_p, r, id(v,t)⟩ while decisionp[h_p] = nil do { if valid(v) { diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_001_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_001_draft.md index b5521b696..2eb32bc7d 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_001_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_001_draft.md @@ -5,11 +5,13 @@ ### Time and Clocks #### **[PBTS-CLOCK-NEWTON.0]** + There is a reference Newtonian real-time `t` (UTC). Every correct validator `V` maintains a synchronized clock `C_V` that ensures: #### **[PBTS-CLOCK-PRECISION.0]** + There exists a system parameter `PRECISION` such that for any two correct validators `V` and `W`, and at any real-time `t`, `|C_V(t) - C_W(t)| < PRECISION` @@ -22,6 +24,7 @@ In general the local clock may drift from the global time. (It may progress fast #### **[PBTS-MSG-D.0]** + There exists a system parameter `MSGDELAY` for message end-to-end delays **counted in clock-time**. > Observe that [PBTS-MSG-D.0] imposes constraints on message delays as well as on the clock. @@ -36,32 +39,37 @@ The message end-to-end delay between a correct proposer and a correct validator In this section we define the properties of Tendermint consensus (cf. the [arXiv paper][arXiv]) in this new system model. #### **[PBTS-PROPOSE.0]** + A proposer proposes a pair `(v,t)` of consensus value `v` and time `t`. > We then restrict the allowed decisions along the following lines: #### **[PBTS-INV-AGREEMENT.0]** -[Agreement] No two correct validators decide on different values `v`. + +[Agreement] No two correct validators decide on different values `v`. #### **[PBTS-INV-TIME-VAL.0]** + [Time-Validity] If a correct validator decides on `t` then `t` is "OK" (we will formalize this below), even if up to `2f` validators are faulty. However, the properties of Tendermint consensus are of more interest with respect to the blocks, that is, what is written into a block and when. We therefore, in the following, will give the safety and liveness properties from this block-centric viewpoint. For this, observe that the time `t` decided at consensus height `k` will be written in the block of height `k+1`, and will be supported by `2f + 1` `PRECOMMIT` messages of the same consensus round `r`. The time written in the block, we will denote by `b.time` (to distinguish it from the term `bfttime` used for median-based time). For this, it is important to have the following consensus algorithm property: #### **[PBTS-INV-TIME-AGR.0]** + [Time-Agreement] If two correct validators decide in the same round, then they decide on the same `t`. #### **[PBTS-DECISION-ROUND.0]** + Note that the relation between consensus decisions, on the one hand, and blocks, on the other hand, is not immediate; in particular if we consider time: In the proposed solution, as validators may decide in different rounds, they may decide on different times. -The proposer of the next block, may pick a commit (at least `2f + 1` `PRECOMMIT` messages from one round), and thus it picks a decision round that is going to become "canonic". -As a result, the proposer implicitly has a choice of one of the times that belong to rounds in which validators decided. Observe that this choice was implicitly the case already in the median-based `bfttime`. +The proposer of the next block, may pick a commit (at least `2f + 1` `PRECOMMIT` messages from one round), and thus it picks a decision round that is going to become "canonic". +As a result, the proposer implicitly has a choice of one of the times that belong to rounds in which validators decided. Observe that this choice was implicitly the case already in the median-based `bfttime`. However, as most consensus instances terminate within one round on the Cosmos hub, this is hardly ever observed in practice. -Finally, observe that the agreement ([Agreement] and [Time-Agreement]) properties are based on the Tendermint security model [TMBC-FM-2THIRDS.0] of more than 2/3 correct validators, while [Time-Validity] is based on more than 1/3 correct validators. +Finally, observe that the agreement ([Agreement] and [Time-Agreement]) properties are based on the Tendermint security model [TMBC-FM-2THIRDS.0] of more than 2/3 correct validators, while [Time-Validity] is based on more than 1/3 correct validators. ### SAFETY @@ -69,10 +77,11 @@ Here we will provide specifications that relate local time to block time. Howeve For a correct validator `V`, let `beginConsensus(V,k)` be the local time when it sets its height to `k`, and let `endConsensus(V,k)` be the time when it sets its height to `k + 1`. -Let -- `beginConsensus(k)` be the minimum over `beginConsensus(V,k)`, and -- `last-beginConsensus(k)` be the maximum over `beginConsensus(V,k)`, and -- `endConsensus(k)` the maximum over `endConsensus(V,k)` +Let + +- `beginConsensus(k)` be the minimum over `beginConsensus(V,k)`, and +- `last-beginConsensus(k)` be the maximum over `beginConsensus(V,k)`, and +- `endConsensus(k)` the maximum over `endConsensus(V,k)` for all correct validators `V`. @@ -84,27 +93,34 @@ We assume that during one consensus instance, local clocks are not set back, in #### **[PBTS-CONSENSUS-TIME-VALID.0]** -If + +If + - there is a valid commit `c` for height `k`, and - `c` contains a `PRECOMMIT` message by at least one correct validator, -then the time `b.time` in the block `b` that is signed by `c` satisfies +then the time `b.time` in the block `b` that is signed by `c` satisfies + - `beginConsensus(k) - PRECISION <= b.time < endConsensus(k) + PRECISION + MSGDELAY`. > [PBTS-CONSENSUS-TIME-VALID.0] is based on an analysis where the proposer is faulty (and does does not count towards `beginConsensus(k)` and `endConsensus(k)`), and we estimate the times at which correct validators receive and `accept` the `propose` message. If the proposer is correct we obtain #### **[PBTS-CONSENSUS-LIVE-VALID-CORR-PROP.0]** -If the proposer of round 1 is correct, and + +If the proposer of round 1 is correct, and + - [TMBC-FM-2THIRDS.0] holds for a block of height `k - 1`, and - [PBTS-MSG-FAIR.0], and - [PBTS-CLOCK-PRECISION.0], and - [PBTS-CLOCK-GROW.0] (**TODO:** is that enough?) -then eventually (within bounded time) every correct validator decides in round 1. +then eventually (within bounded time) every correct validator decides in round 1. #### **[PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]** -If the proposer of round 1 is correct, and + +If the proposer of round 1 is correct, and + - [TMBC-FM-2THIRDS.0] holds for a block of height `k - 1`, and - [PBTS-MSG-FAIR.0], and - [PBTS-CLOCK-PRECISION.0], and @@ -117,7 +133,8 @@ then `beginConsensus_k <= b.time <= last-beginConsensus_k`. ### LIVENESS -If +If + - [TMBC-FM-2THIRDS.0] holds for a block of height `k - 1`, and - [PBTS-MSG-FAIR.0], - [PBTS-CLOCK.0], and @@ -132,7 +149,8 @@ then eventually there is a valid commit `c` for height `k`. #### **[PBTS-CLOCKSYNC-EXTERNAL.0]** -There is a system parameter `ACCURACY`, such that for all real-times `t` and all correct validators `V`, +There is a system parameter `ACCURACY`, such that for all real-times `t` and all correct validators `V`, + - `| C_V(t) - t | < ACCURACY`. > `ACCURACY` is not necessarily visible at the code level. The properties below just show that the smaller @@ -141,6 +159,7 @@ its value, the closer the block time will be to real-time #### **[PBTS-CONSENSUS-PTIME.0]** LET `m` be a propose message. We consider the following two real-times `proposalTime(m)` and `propRecvTime(m)`: + - if the proposer is correct and sends `m` at time `t`, we write `proposalTime(m)` for real-time `t`. - if first correct validator receives `m` at time `t`, we write `propRecvTime(m)` for real-time `t`. @@ -158,7 +177,7 @@ Let `b` be a block with a valid commit that contains at least one `precommit` me `proposalTime(m) - ACCURACY < b.time < proposalTime(m) + ACCURACY` -> by the algorithm at time `proposalTime(m)` the proposer fixes `m.time <- now_p(proposalTime(m))` +> by the algorithm at time `proposalTime(m)` the proposer fixes `m.time <- now_p(proposalTime(m))` > "triggered the `PRECOMMIT`" implies that the data in `m` and `b` are "matching", that is, `m` proposed the values that are actually stored in `b`. diff --git a/spec/consensus/proposer-based-timestamp/pbts_001_draft.md b/spec/consensus/proposer-based-timestamp/pbts_001_draft.md index ccaf55787..a4d876b28 100644 --- a/spec/consensus/proposer-based-timestamp/pbts_001_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts_001_draft.md @@ -1,22 +1,23 @@ # Proposer-Based Time -## Current BFTTime +## Current BFTTime ### Description In Tendermint consensus, the first version of how time is computed and stored in a block works as follows: + - validators send their current local time as part of `precommit` messages - upon collecting the `precommit` messages that the proposer uses to build a commit to be put in the next block, the proposer computes the `time` of the next block as the median (weighted over voting power) of the times in the `precommit` messages. ### Analysis 1. **Fault tolerance.** The computed median time is called [`bfttime`][bfttime] as it is indeed fault-tolerant: if **less than a third** of the validators is faulty (counted in voting power), it is guaranteed that the computed time lies between the minimum and the maximum times sent by correct validators. -2. **Effect of faulty validators.** If more than `1/2` of the voting power (which is in fact more than one third and less than two thirds of the voting power) is held by faulty validators, then the time is under total control of the faulty validators. (This is particularly challenging in the context of [lightclient][lcspec] security.) -3. **Proposer influence on block time.** The proposer of the next block has a degree of freedom in choosing the `bfttime`, since it computes the median time based on the timestamps from `precommit` messages sent by -`2f + 1` correct validators. - 1. If there are `n` different timestamps in the `precommit` messages, the proposer can use any subset of timestamps that add up to `2f + 1` - of the voting power in order to compute the median. - 1. If the validators decide in different rounds, the proposer can decide on which round the median computation is based. +1. **Effect of faulty validators.** If more than `1/2` of the voting power (which is in fact more than one third and less than two thirds of the voting power) is held by faulty validators, then the time is under total control of the faulty validators. (This is particularly challenging in the context of [lightclient][lcspec] security.) +1. **Proposer influence on block time.** The proposer of the next block has a degree of freedom in choosing the `bfttime`, since it computes the median time based on the timestamps from `precommit` messages sent by + `2f + 1` correct validators. + 1. If there are `n` different timestamps in the `precommit` messages, the proposer can use any subset of timestamps that add up to `2f + 1` + of the voting power in order to compute the median. + 1. If the validators decide in different rounds, the proposer can decide on which round the median computation is based. 1. **Liveness.** The liveness of the protocol: 1. does not depend on clock synchronization, 1. depends on bounded message delays. @@ -27,18 +28,18 @@ In Tendermint consensus, the first version of how time is computed and stored in ### Outline -An alternative approach to time has been discussed: Rather than having the validators send the time in the `precommit` messages, the proposer in the consensus algorithm sends its time in the `propose` message, and the validators locally check whether the time is OK (by comparing to their local clock). +An alternative approach to time has been discussed: Rather than having the validators send the time in the `precommit` messages, the proposer in the consensus algorithm sends its time in the `propose` message, and the validators locally check whether the time is OK (by comparing to their local clock). This proposed solution adds the requirement of having synchronized clocks, and other implicit assumptions. ### Comparison of the Suggested Method to the Old One -1. **Fault tolerance.** Maintained in the suggested protocol. -2. **Effect of faulty validators.** Eliminated in the suggested protocol, -that is, the block `time` can be corrupted only in the extreme case when -`>2/3` of the validators are faulty. +1. **Fault tolerance.** Maintained in the suggested protocol. +1. **Effect of faulty validators.** Eliminated in the suggested protocol, + that is, the block `time` can be corrupted only in the extreme case when + `>2/3` of the validators are faulty. 1. **Proposer influence on block time.** The proposer of the next block -has less freedom when choosing the block time. + has less freedom when choosing the block time. 1. This scenario is eliminated in the suggested protocol, provided that there are `<1/3` faulty validators. 1. This scenario is still there. 1. **Liveness.** The liveness of the suggested protocol: @@ -50,17 +51,21 @@ has less freedom when choosing the block time. ### Protocol Overview #### Proposed Time -We assume that the field `proposal` in the `PROPOSE` message is a pair `(v, time)`, of the proposed consensus value `v` and the proposed time `time`. + +We assume that the field `proposal` in the `PROPOSE` message is a pair `(v, time)`, of the proposed consensus value `v` and the proposed time `time`. #### Reception Step + In the reception step at node `p` at local time `now_p`, upon receiving a message `m`: + - **if** the message `m` is of type `PROPOSE` and satisfies `now_p - PRECISION < m.time < now_p + PRECISION + MSGDELAY`, then mark the message as `timely`. (`PRECISION` and `MSGDELAY` being system parameters, see [below](#safety-and-liveness)) + > after the presentation in the dev session, we realized that different semantics for the reception step is closer aligned to the implementation. Instead of dropping propose messages, we keep all of them, and mark timely ones. #### Processing Step -- Start round +- Start round @@ -228,7 +233,7 @@ upon ⟨PROPOSAL, h_p, r, (v,t), ∗⟩ from proposer(h_p, r) For safety (Point 1, Point 2, Point 3i) and liveness (Point 4) we need the following assumptions: -- There exists a system parameter `PRECISION` such that for any two correct validators `V` and `W`, and at any real-time `t`, their local times `C_V(t)` and `C_W(t)` differ by less than `PRECISION` time units, +- There exists a system parameter `PRECISION` such that for any two correct validators `V` and `W`, and at any real-time `t`, their local times `C_V(t)` and `C_W(t)` differ by less than `PRECISION` time units, i.e., `|C_V(t) - C_W(t)| < PRECISION` - The message end-to-end delay between a correct proposer and a correct validator (for `PROPOSE` messages) is less than `MSGDELAY`. @@ -237,8 +242,8 @@ i.e., `|C_V(t) - C_W(t)| < PRECISION` For analyzing real-time safety (Point 5), we use a system parameter `ACCURACY`, such that for all real-times `t` and all correct validators `V`, we have `| C_V(t) - t | < ACCURACY`. > `ACCURACY` is not necessarily visible at the code level. We might even view `ACCURACY` as variable over time. The smaller it is during a consensus instance, the closer the block time will be to real-time. - -> Note that `PRECISION` and `MSGDELAY` show up in the code. +> +> Note that `PRECISION` and `MSGDELAY` show up in the code. ### Detailed Specification @@ -248,9 +253,6 @@ This specification describes the changes needed to be done to the Tendermint con - [Part II - Protocol specification][algorithm] - [TLA+ Specification][proposertla] - - - [arXiv]: https://arxiv.org/abs/1807.04938 [tlatender]: https://github.com/tendermint/spec/blob/master/rust-spec/tendermint-accountability/README.md diff --git a/spec/core/state.md b/spec/core/state.md index 3b8e1a22c..512e0c43b 100644 --- a/spec/core/state.md +++ b/spec/core/state.md @@ -41,7 +41,7 @@ limit on the number of votes in a commit. Further information on [`Validator`'s](./data_structures.md#validator), [`ValidatorSet`'s](./data_structures.md#validatorset) and -[`ConsensusParams`'s](./data_structures.md#consensusparams) can +[`ConsensusParams`'s](./data_structures.md#consensusparams) can be found in [data structures](./data_structures.md) ## Execution