diff --git a/Specs/consensus/English/messsages-to-events.md b/Specs/consensus/English/messsages-to-events.md new file mode 100644 index 000000000..a8ce85b93 --- /dev/null +++ b/Specs/consensus/English/messsages-to-events.md @@ -0,0 +1,170 @@ +# Messages to Events + +The consensus state-machine operates on complex `Event`s that reflect the +reception of one or multiple `Message`s, combined with state elements and the +interaction with other modules. + +This document overviews how messages should be handled at different stages of +the protocol. + +It is assume that a process is at round `r` of height `h` of consensus, or in +short, at round `(h, r)`. + +## Pending + +- [ ] How to handle messages from [different heights](#different-heights) in general +- [ ] Definitions and details regarding the [round skipping](#round-skipping) mechanism +- [ ] How to limit the amount of messages from [future rounds](#future-rounds) stored +- [ ] Full mapping between messages of the [current round](#current-round) and the produced events + +## Different heights + +Messages with heights `h'` with either `h' < h` (past) or `h' > h` (future). + +The pseudo-code description of the algorithm ignores messages from different +heights. +If we take the same approach in this specification, we have to specify +separately modules responsible to handle those messages. + + +- Past heights (`h' < h`): the consensus state machine is not affected by such + messages. However, their reception might indicate that a peer is lagging + behind in the protocol, and need to be synchronized. + - In CometBFT's implementation we handle message from the previous height + (`h' = h - 1`) for the `LastCommit` vote set. This only happens during the + first step of the first round (`r = 0`) of a height. +- Future heights (`h' > h`): the consensus state machine is not able to process + message from future heights in a proper way, as the validator set for them is + not known. However, once the process reaches this height `h'`, those messages + are _required_ for proper operation. There are two options here: + 1. Buffer a limited amount of such messages + 2. Assume that the communication subsystem (p2p) is able to retrieve (ask for + retransmission) of them when the process reaches height `h'`. + Notice that this option implies that processes keep a minimal set of + consensus messages that enables peers lagging behind to decide a past height. + +## Previous rounds + +Messages from rounds `(h, r')` with `r' < r`: same height `h` but previous round `r'`. + +The consensus state machine requires receiving and processing messages from +previous rounds: + +- `PREVOTE` messages can produce a Proof of Lock (POL) `2f + 1 ⟨PREVOTE, h, vr, id(v)⟩` + needed for accepting `PROPOSAL(h, r, v, vr)` message from the current round, + where `vr == r' < r` (L28). +- `PRECOMMIT` messages can produce a Precommit quorum `2f + 1 ⟨PRECOMMIT, h, r', id(v)⟩` + that leads to the decision of `v` at round `r'` (L49). +- `PROPOSAL` messages can be required to match a produced Precommit quorum (L49). + - Associated full value messages are required to produce the `⟨PROPOSAL, h, r', v, *⟩` event + +The production of the enumerated events from previous rounds should be +identical to the production of events from messages from the [current round](#current-round). + +## Future rounds + +Messages from rounds `(h, r')` with `r' > r`: same height `h` but future round `r'`. + +### Round skipping + +The consensus state machine requires receiving and processing messages from +future rounds for enabling the _round skipping_ mechanism, defined as follows +in the pseudo-code: + +``` +55: upon f + 1 ⟨∗, hp, round, ∗, ∗⟩ with round > roundp do +56: StartRound(round) +``` + +The current interpretation of this rule is that messages from a round `r' > r` +are received from `f + 1` voting-power equivalent distinct senders. +This means, that at least `1` correct process is at round `r'`. + +While this threshold does not need to be adopted (it can be configurable), +messages from a future round should initially have their unique senders counted. +Once the round skip threshold of processes is reached, the corresponding event +should be produced. + +### Limits + +The same reasoning applied for messages from [future heights](#different-heights) +applies for messages from future rounds. + +Messages from future rounds are _required_ for the proper operation of the +consensus state machine once the process reaches their round `r'`. +There are two options, which can in particular be combined: + +1. Buffer a limited amount of such messages, or messages from a limited amount + of future rounds `r'` + - In CometBFT's implementation, only messages from round `r' = r + 1` are tracked. +2. Assume that the communication subsystem (p2p) is able to retrieve (ask for + retransmission) of messages from future rounds when the process reaches round `r'`. + Since messages from [previous rounds](#previous-rounds) are stored by + default, peers that have reached the future round `r'` should be able to + retransmit them. + +## Current round + +Messages matching the current round `(h, r)` of a process produce most of the +relevant events for the consensus state machine. + +TODO: + +## Counting votes + +Messages `⟨PREVOTE, h, r, *⟩` and `⟨PRECOMMIT, h, r, *⟩` are generically called votes. +They refer to a round step `(h, r, s)` of consensus, where `s` is defined by +the vote type, either `PREVOTE` or `PRECOMMIT`. + +The processing of _individual_ vote messages don't produce events relevant for +the consensus state machine. +But when the number of unique vote messages referring to a given round step +`(h, r, s)` reaches a given _threshold_, relevant events are produced; +the produced event depends on the value carried by such votes. + +General assumptions regarding vote messages: + +- Vote messages are produced, signed and broadcast by a validator, which is its + *sender* + - To define whether a vote message for round step `(h, r, s)` is valid, the + validator set for height `h` must to be known. + The validator set can change over heights, but it is the same within a height. +- To each validator in the validator set of a height `h` is associated a *voting power* + - Thresholds are computed from the voting power associated to the + sender of each vote message +- A vote message carries a value: either a reference to a proposed value + `id(v)`, or the special `nil` value + - For practical effects, it should be considered that the size of vote + messages is constant +- Correct validators produce at most one vote message per round step: either + for a `id(v)` or for `nil` +- Byzantine validators may equivocate and produce multiple distinct vote + messages for the same round step. Equivocating vote messages differ on the + value they carry: for `nil`, `id(v)`, `id(v')`, etc. + - This possibility constitutes an attack vector. A process must thus restrict + the number of distinct vote messages from the same sender and referring to + the same round step that can be stored. + +### `f + 1` threshold + +This threshold represents that vote messages referring to a round step were +received from a enough number of unique senders, so that it is guaranteed that +_at least one_ of the senders is a _correct_ validator. + +The rationale here is that the cumulative voting power of Byzantine validators +cannot exceed `f`, so that at least one of the considered vote messages must +have been produced by a correct validator. + +### `2f + 1` threshold + +This threshold represents that vote messages referring to a round step were +received from a enough number of unique senders, so that it is guaranteed that +_the majority_ of the senders are _correct_ validators. + +The rationale here is that the cumulative voting power of Byzantine validators +cannot exceed `f`, so that the subset of considered vote messages that must +have been produced by correct validators have a cumulative voting power of at +least `f + 1`, which is strictly greater than `f`. + +> TODO: this also means that the majority of the voting power hold by correct +> validators is represented in the considered set of vote messages. diff --git a/Specs/consensus/English/protocol-state-machine.md b/Specs/consensus/English/protocol-state-machine.md new file mode 100644 index 000000000..13c5c41c8 --- /dev/null +++ b/Specs/consensus/English/protocol-state-machine.md @@ -0,0 +1,263 @@ +# Consensus protocol: state-machine + +The consensus protocol consists of a sequence of **heights**, +identified by natural numbers `h`. +We define a [`Height(h)` state machine](#height-state-machine) to represent the +operation of a height `h`. + +Each height of consensus consists of a number of **rounds**, +identified by natural numbers `r`. +We define a [`Round(r)` state machine](#round-state-machine) to represent the +operation of each of the rounds `r` of a height. + +## Height state machine + +The state machine `Height(h)` represents the operation of a height `h` of consensus. + +The considered set of states are: + +- Unstarted + - Initial state + - Can be used to store messages for unstarted height `h` + - In the algorithm when `hp < h`, where `hp` is the node's current round, and `decisionp[h] == nil` +- InProgress: + - Actual consensus execution + - In the algorithm when `hp == h` and `decisionp[h] == nil` + - Controls the operation of multiple round state machines `Round(r)`, where `r` is a natural number +- Decided + - Final state + - May also include the commit/execution of decided value + - In the algorithm when `hp >= h` and `decisionp[h] != nil` + +The table below summarizes the major state transitions in the `Height(h)` state machine. +The `Ref` column refers to the line of the pseudo-code where the events can be found. + +| From | To | Event | Action | Ref | +|-------|-----------|-----------|--------|-----| +| Unstarted | InProgress | `start_height` | send `start` to `Round(0)` | L10, L54 | +| Round(r) | Decided | `decide(r', v)` | emit `decide(h, v)`
stop to every `Round(r)` | L49 | +| Round(r) | Round(r+1) | `next_round(r+1)` | send `start` to `Round(r+1)` | L65 | +| Round(r) | Round(r') | `next_round(r')` | send `start` to `Round(r')` | L55 | + +A height `h` consists of multiple rounds of consensus, always starting from +round `0`. +The `Unstarted` state is intended to store events and messages regarding height `h` +before its execution is actually started. + +The height is concluded when a decision is reached in _any_ of its rounds. +The `Decided` state is intended to represent that a decision has been reached, +while it also allows storing the summary of a decided height. + +Once the node moves to the `Decided` state of a height, the operation of +_every_ round `Round(r)` should be concluded. +The representation of this transition needs to be improved, for now it is +considered that the corresponding `Round(r)` state machines are killed. + + + +## Round state-machine + +The state machine `Round(r)` represents the operation of a round `r` of consensus. +It is controlled (started and stopped) by an instance of the `Height(h)` state machine. + +The considered set of states are: + +- Unstarted + - Initial state + - Can be used to store messages early received for this round + - In the algorithm when `roundp < r`, where `roundp` is the node's current round +- InProgress + - Actual consensus single-round execution + - In the algorithm when `roundp == r` +- Stalled + - Final state for an unsuccessful round + - In the algorithm when `roundp > r` + - Consists of the substates: `propose`, `prevote`, and `precommit` +- Decided + - Final state for an successful round + +The table below summarizes the major state transitions in the `Round(r)` state machine. +The `Ref` column refers to the line of the pseudo-code where the events can be found. + +| From | To | Ev Name | Event Details | Action | Ref | +| ------------ | ------------ | ------------------- | --------------------------------------------------------------------- | --------------------------- | ----- | +| InProgress | InProgress | PrecommitAny | `2f + 1 ⟨PRECOMMIT, h, r, *⟩`
for the first time | schedule `TimeoutPrecommit(h, r)` | L47 | +| InProgress | Unstarted (?) | TimeoutPrecommit | `TimeoutPrecommit(h, r)` | `next_round(r+1)` | L65 | +| InProgress | Unstarted (?) | RoundSkip(r') | `f + 1 ⟨*, h, r', *, *⟩` with `r' > r` | `next_round(r')` | L55 | +| InProgress | Decided | PrecommitValue(v) | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | `commit(v)` | L49 | + + + + +### InProgress round + +The table below summarizes the state transitions within the `InProgress` state +of the `Round(r)` state machine. +There can only be a single round state machine at the `InProgress` state at a +time, which represents the node's current round of consensus. +The following state transitions therefore represent the core of the consensus algorithm. +The `Ref` column refers to the line of the pseudo-code where the events can be found. + +| From | To | Ev Name | Ev Details | Actions and Return | Ref | +| ----------- | ----------- | ------------------ | --------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------- | ----- | +| Unstarted | propose | StartProposer(v) | `start` with `proposer(h, r) = p` and `v = getValue()` | broadcast `⟨PROPOSAL, h, r, v, validRound⟩` | L19 | +| Unstarted | propose | StartNonProposer | `start` with `proposer(h, r) != p` (optional restriction) | schedule `TimeoutPropose(h, r)` | L21 | +| propose | prevote | Proposal(v, -1) | `⟨PROPOSAL, h, r, v, −1⟩` | broadcast `⟨PREVOTE, h, r, {id(v), nil}⟩` | L22 | +| propose | prevote | Proposal(v, vr) | `⟨PROPOSAL, h, r, v, vr⟩`
`2f + 1 ⟨PREVOTE, h, vr, id(v)⟩` with `vr < r` | broadcast `⟨PREVOTE, h, r, {id(v), nil}⟩` | L28 | +| propose | prevote | TimeoutPropose | `TimeoutPropose(h, r)` | broadcast `⟨PREVOTE, h, r, nil⟩` | L57 | +| prevote | prevote | PolkaAny | `2f + 1 ⟨PREVOTE, h, r, *⟩`
for the first time | schedule `TimeoutPrevote(h, r)⟩` | L34 | +| prevote | precommit | PolkaValue(v) | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update `lockedValue, lockedRound, validValue, validRound`,
broadcast `⟨PRECOMMIT, h, r, id(v)⟩` | L36 | +| prevote | precommit | PolkaNil | `2f + 1 ⟨PREVOTE, h, r, nil⟩` | broadcast `⟨PRECOMMIT, h, r, nil⟩` | L44 | +| prevote | precommit | TimeoutPrevote | `TimeoutPrevote(h, r)` | broadcast `⟨PRECOMMIT, h, r, nil⟩` | L61 | +| precommit | precommit | PolkaValue(v) | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update `validValue, validRound` | L36 | + +The ordinary operation of a round of consensus consists on the sequence of +round steps `propose`, `prevote`, and `precommit`, represented in the table. +The conditions for concluding a round of consensus, therefore for leaving the +`InProgress` state, are presented in the next sub-section. + +All the state transitions represented in the table on consider message and +events referring to the node's current round `r`. +In the pseudo-code this current round of a node is referred as `round_p`. + +There is, however, an exception: the transition `L28` requires the node to have +access to `PREVOTE` messages from a previous round `r' < r`. +Ideally, messages for each round `r` should be handled by the corresponding +`Round(r)` state machine. +This transition constitutes an exception that have to be handled in a proper way. + + + +## Events + +Description of the events considered by the algorithm. + +We should consider renaming them for more clarity. +The production of such events requires, in most cases, the definition of a +state machine to produce them. + +### `⟨PROPOSAL, h, r, v, *⟩` + +A `PROPOSAL` message for round `(h,r)`. +Must be received from (i.e., signed by) `proposer(h, r)`. + +The algorithm considers that this message carries the (full) value `v`. +This specification should consider that the carried value can be obtained in a +different way. +This event, in this case, consists of the combination of possible multiple +message or events that have as a result the production of this event for the +algorithm. + +### `2f + 1 ⟨PREVOTE, h, r, *⟩` + +Quorum of `PREVOTE` messages for a round `(h, r)`. + +The last field value can be: + +- `id(v)`: quorum of votes for a value +- `nil`: quorum of votes for nil +- `any`: quorum of votes for multiple values and/or nil + +### `2f + 1 ⟨PRECOMMIT, h, r, *⟩` + +Quorum of `PRECOMMIT` messages for a round `(h, r)`. + +The last field value can be: + +- `id(v)`: quorum of votes for a value +- `nil`: quorum of votes for nil +- `any`: quorum of votes for multiple values and/or nil + +### `Timeout*(h, r)` + +Timeout events. +They must be scheduled in order to be triggered. + +### `f + 1 ⟨*, h, r, *⟩` + +For round-skipping, needs to be properly evaluated. + +## Pending of description + +- [ ] Events considered by every state machine + - Events produced by one state machine and processed by another + - External events, produced by the environment (e.g. messages and timeouts) +- [ ] State machine producing complex events (e.g. `2f + 1` message X) +- [ ] Routing of events from the higher-level state machine to lower-level state machines + diff --git a/Specs/Quint/0DecideNonProposerTest.itf.json b/Specs/consensus/Quint/0DecideNonProposerTest.itf.json similarity index 100% rename from Specs/Quint/0DecideNonProposerTest.itf.json rename to Specs/consensus/Quint/0DecideNonProposerTest.itf.json diff --git a/Specs/Quint/asyncModelsTest.qnt b/Specs/consensus/Quint/asyncModelsTest.qnt similarity index 100% rename from Specs/Quint/asyncModelsTest.qnt rename to Specs/consensus/Quint/asyncModelsTest.qnt diff --git a/Specs/Quint/basicSpells.qnt b/Specs/consensus/Quint/basicSpells.qnt similarity index 100% rename from Specs/Quint/basicSpells.qnt rename to Specs/consensus/Quint/basicSpells.qnt diff --git a/Specs/Quint/consensus.qnt b/Specs/consensus/Quint/consensus.qnt similarity index 100% rename from Specs/Quint/consensus.qnt rename to Specs/consensus/Quint/consensus.qnt diff --git a/Specs/Quint/consensusTest.qnt b/Specs/consensus/Quint/consensusTest.qnt similarity index 100% rename from Specs/Quint/consensusTest.qnt rename to Specs/consensus/Quint/consensusTest.qnt diff --git a/Specs/Quint/executor.qnt b/Specs/consensus/Quint/executor.qnt similarity index 100% rename from Specs/Quint/executor.qnt rename to Specs/consensus/Quint/executor.qnt diff --git a/Specs/Quint/extraSpells.qnt b/Specs/consensus/Quint/extraSpells.qnt similarity index 100% rename from Specs/Quint/extraSpells.qnt rename to Specs/consensus/Quint/extraSpells.qnt diff --git a/Specs/Quint/parameterizedTest.qnt b/Specs/consensus/Quint/parameterizedTest.qnt similarity index 100% rename from Specs/Quint/parameterizedTest.qnt rename to Specs/consensus/Quint/parameterizedTest.qnt diff --git a/Specs/Quint/statemachineAsync.qnt b/Specs/consensus/Quint/statemachineAsync.qnt similarity index 100% rename from Specs/Quint/statemachineAsync.qnt rename to Specs/consensus/Quint/statemachineAsync.qnt diff --git a/Specs/Quint/statemachineTest.qnt b/Specs/consensus/Quint/statemachineTest.qnt similarity index 100% rename from Specs/Quint/statemachineTest.qnt rename to Specs/consensus/Quint/statemachineTest.qnt diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/consensus/Quint/voteBookkeeper.qnt similarity index 100% rename from Specs/Quint/voteBookkeeper.qnt rename to Specs/consensus/Quint/voteBookkeeper.qnt diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/consensus/Quint/voteBookkeeperTest.qnt similarity index 100% rename from Specs/Quint/voteBookkeeperTest.qnt rename to Specs/consensus/Quint/voteBookkeeperTest.qnt