PBTS: additions and fixes on migrated spec

docs/core/configuration.md

@@ -11,7 +11,7 @@ further below are intended for advance power users.
 
 ## Options
 
-The default configuration file create by `cometbft init` has all
+The default configuration file created by `cometbft init` has all
 the parameters set with their default values. It will look something
 like the file below, however, double check by inspecting the
 `config.toml` created with your version of `cometbft` installed:
@@ -356,7 +356,7 @@ keep-invalid-txs-in-cache = false
 max_tx_bytes = 1048576
 
 # Maximum size of a batch of transactions to send to a peer
-# Including space needed by encoding (one varint per transaction).
+# Including space needed by encoding (one `varint` per transaction).
 # XXX: Unused due to https://github.com/tendermint/tendermint/issues/5796
 max_batch_bytes = 0
 
@@ -547,7 +547,7 @@ the delay between blocks by changing the `timeout_commit`. E.g. `timeout_commit
 
 ### create_empty_blocks = false
 
-In this setting, blocks are created when transactions received.
+In this setting, blocks are created when transactions are received.
 
 Note after the block H, CometBFT creates something we call a "proof block"
 (only if the application hash changed) H+1. The reason for this is to support
@@ -635,7 +635,7 @@ What happens in reality is, however, a little bit different:
 ```
 
 That's because Bob is too fast at proposing blocks. This leaves Alice very
-little chances to propose a block and not always be catching up. Note every
+little chances to propose a block and not always be catching up. Note that every
 block Bob creates needs a vote from Alice to constitute 2/3+.
 
 Imagine now there are ten geographically distributed validators. One of them

light/doc.go

@@ -121,7 +121,7 @@ See
 https://docs.cometbft.com/main/core/light-client.html
 for usage example.
 Or see
-https://github.com/cometbft/cometbft/tree/main/spec/consensus/light-client
+https://github.com/cometbft/cometbft/blob/main/spec/light-client/README.md
 for the full spec
 */
 package light

spec/consensus/proposer-based-timestamp/README.md

@@ -1,63 +1,25 @@
 # Proposer-Based Timestamps (PBTS)
 
-This section describes a version of the Tendermint consensus algorithm, adopted in CometBFT,
+This document describes a version of the Tendermint consensus algorithm, adopted in CometBFT,
 that uses proposer-based timestamps.
 
-## Context
+## Overview
 
-Tendermint provides a deterministic, Byzantine fault-tolerant, source of time,
-defined by the `Time` field present in the headers of committed blocks.
-
-In the current consensus implementation, the timestamp of a block is
-computed by the [`BFTTime`][bfttime] algorithm:
-
-- Validators include a timestamp in the `Precommit` messages they broadcast.
-Timestamps are retrieved from the validators' local clocks,
-with the only restriction that they must be **monotonic**:
-
-    - The timestamp of a `Precommit` message voting for a block
-	cannot be earlier than the `Time` field of that block;
-
-- The timestamp of a block is deterministically computed from the timestamps of
-a set of `Precommit` messages that certify the commit of the previous block.
-This certificate, a set of `Precommit` messages from a round of the previous height,
-is selected by the block's proposer and stored in the `Commit` field of the block:
-
-    - The block timestamp is the *median* of the timestamps of the `Precommit` messages
-	included in the `Commit` field, weighted by their voting power.
-	Block timestamps are **monotonic** because
-	timestamps of valid `Precommit` messages are monotonic;
-
-Assuming that the voting power controlled by Byzantine validators is bounded by `f`,
-the cumulative voting power of any valid `Commit` set must be at least `2f+1`.
-As a result, the timestamp computed by `BFTTime` is not influenced by Byzantine validators,
-as the weighted median of `Commit` timestamps comes from the clock of a non-faulty validator.
-
-Tendermint does not make any assumptions regarding the clocks of (correct) validators,
-as block timestamps have no impact in the consensus protocol.
-However, the `Time` field of committed blocks is used by other components of Tendermint,
-such as IBC, the evidence, staking, and slashing modules.
-And it is used based on the common belief that block timestamps
-should bear some resemblance to real time, which is **not guaranteed**.
-
-A more comprehensive discussion of the limitations of `BFTTime`
-can be found in the [first draft][main_v1] of this proposal.
-Of particular interest is to possibility of having validators equipped with "faulty" clocks,
-not fairly accurate with real time, that control more than `f` voting power,
-plus the proposer's flexibility when selecting a `Commit` set,
-and thus determining the timestamp for a block.
-
-## Proposal
-
-In the proposed solution, the timestamp of a block is assigned by its
+With PBTS, the timestamp of a block is assigned by its
 proposer, according with its local clock.
 In other words, the proposer of a block also *proposes* a timestamp for the block.
 Validators can accept or reject a proposed block.
 A block is only accepted if its timestamp is acceptable.
 A proposed timestamp is acceptable if it is *received* within a certain time window,
 determined by synchronous parameters.
 
-PBTS therefore augments the system model considered by Tendermint with *synchronous assumptions*:
+The motivation for introducing this new method for assigning timestamps is
+summarized in the [first draft proposal][main_v1].
+
+### Synchronous Parameters
+
+For validating timestamps, PBTS augments the system model considered by the
+consensus algorithm with *synchronous assumptions*:
 
 - **Synchronized clocks**: simultaneous clock reads at any two correct validators
 differ by at most `PRECISION`;
@@ -67,22 +29,25 @@ is bounded by `MSGDELAY`.
 This assumption is restricted to `Proposal` messages, broadcast by proposers.
 
 `PRECISION` and `MSGDELAY` are consensus parameters, shared by all validators,
-that define whether the timestamp of a block is acceptable.
-Let `t` be the time, read from its local clock, at which a validator
-receives, for the first time, a proposal with timestamp `ts`:
+that define whether the timestamp of a block is acceptable,
+according with the introduced `timely` predicate.
+
+### Timestamp Validation
 
-- **[Time-Validity]** The proposed timestamp `ts` received at local time `t`
-is accepted if it satisfies the **timely** predicate:
-	> `ts - PRECISION <= t <= ts + MSGDELAY + PRECISION`
+The `timely` predicate is defined as follows.
+Let `proposalReceiveTime` be the time, read from its local clock, at
+which a validator receives a `Proposal` message for a `block` with timestamp `ts = block.time`.
+The proposed timestamp `ts` can be accepted if both:
 
-The left inequality of the *timely* predicate establishes that proposed timestamps
-should be in the past, when adjusted by the clocks `PRECISION`.
-The right inequality of the *timely* predicate establishes that proposed timestamps
-should not be too much in the past, more precisely, not more than `MSGDELAY` in the past,
-when adjusted by the clocks `PRECISION`.
+ - `ts <= proposalReceiveTime + PRECISION`
+ - `ts >= proposalReceiveTime - MSGDELAY - PRECISION`
 
-A more detailed and formalized description is available in the
-[System Model and Properties][sysmodel] document
+The following diagram graphically represents the conditions for accepting a proposed timestamp:
+
+![diagram](./diagram.png)
+
+A more detailed and formalized description of the `timely` predicate is available in the
+[System Model and Properties][sysmodel] document.
 
 ## Implementation
 
@@ -99,52 +64,93 @@ The block's timestamp represents the time at which it was assembled
     - To preserve monotonicity, a proposer might need to wait until its clock
 	reads a time greater than the timestamp of the previous block;
 
-- A validator only prevotes for *timely* blocks,
-that is, blocks whose timestamps are considered *timely* (compared to the original Tendermint consensus, a check is added to line 23).
-If the block proposed in a round is considered *untimely*,
-the validator prevotes `nil` (line 26):
+- A validator only prevotes for a block if its timestamp is considered `timely`
+(compared to the original algorithm, a check is added to line 23).
+Otherwise, the validator prevotes `nil` (line 26):
 
     - Validators register the time at which they received `Proposal` messages,
-	in order to evaluate the *timely* predicate;
+	in order to evaluate the `timely` predicate;
 
     - Blocks that are re-proposed because they received `2f+1 Prevotes`
-	in a previous round (line 28) are not subject to the *timely* predicate,
-	as they have already been evaluated as *timely* at a previous round.
-
-The more complex change proposed regards blocks that can be re-proposed in multiple rounds.
-The current solution improves the [first version of the specification][algorithm_v1] (that never had been implemented)
-by simplifying the way this situation is handled,
-from a recursive reasoning regarding valid blocks that are re-proposed.
+	in a previous round (line 28) are not subject to the `timely` predicate,
+    as their timestamps have already been evaluated at a previous round.
 
-The full solution is detailed and formalized in the [Protocol Specification][algorithm] document.
+The full solution is detailed and formalized in the [Algorithm Specification][algorithm] document.
 
 ## Further details
 
 - [System Model and Properties][sysmodel]
-- [Protocol Specification][algorithm]
-- [TLA+ Specification][proposertla] (first draft, not updated)
+- [Algorithm Specification][algorithm]
+- [TLA+ Specification][proposertla]
+
+<!---
+## BFT Time
+
+CometBFT provides a deterministic, Byzantine fault-tolerant, source of time,
+defined by the `Time` field present in the headers of committed blocks.
+
+In the current consensus implementation, the timestamp of a block is
+computed by the [`BFT Time`][bfttime] algorithm:
+
+- Validators include a timestamp in the `Precommit` messages they broadcast.
+Timestamps are retrieved from the validators' local clocks,
+with the only restriction that they must be **monotonic**:
+
+    - The timestamp of a `Precommit` message voting for a block
+	cannot be earlier than the `Time` field of that block;
+
+- The timestamp of a block is deterministically computed from the timestamps of
+a set of `Precommit` messages that certify the commit of the previous block.
+This certificate, a set of `Precommit` messages from a round of the previous height,
+is selected by the block's proposer and stored in the `Commit` field of the block:
+
+    - The block timestamp is the *median* of the timestamps of the `Precommit` messages
+	included in the `Commit` field, weighted by their voting power.
+	Block timestamps are **monotonic** because
+	timestamps of valid `Precommit` messages are monotonic;
+
+Assuming that the voting power controlled by Byzantine validators is bounded by `f`,
+the cumulative voting power of any valid `Commit` set must be at least `2f+1`.
+As a result, the timestamp computed by `BFT Time` is not influenced by Byzantine validators,
+as the weighted median of `Commit` timestamps comes from the clock of a non-faulty validator.
+
+The consensus algorithm does not make any assumptions regarding the clocks of (correct) validators,
+as block timestamps have no impact in its operation.
+However, the `Time` field of committed blocks is used by other applications that integrate with CometBFT,
+including IBC, as well as Cosmos SDK modules such as evidence, staking, and slashing.
+And it is used based on the common belief that block timestamps
+should bear some resemblance to real time, which is **not guaranteed**.
+
+A more comprehensive discussion of the limitations of `BFT Time`
+can be found in the [first draft][main_v1] of this proposal.
+Of particular interest is to possibility of having validators equipped with "faulty" clocks,
+not fairly accurate with real time, that control more than `f` voting power,
+plus the proposer's flexibility when selecting a `Commit` set,
+and thus determining the timestamp for a block.
+--->
 
 ### Open issues
 
-- [PBTS: evidence #355][issue355]: not really clear the context, probably not going to be solved.
-- [PBTS: should synchrony parameters be adaptive? #371][issue371]
-- [PBTS: Treat proposal and block parts explicitly in the spec #372][issue372]
-- [PBTS: margins for proposal times assigned by Byzantine proposers #377][issue377]
+- [tendermint/spec#355: PBTS: evidence][issue355]: not really clear the context, probably not going to be solved.
+- [tendermint/spec#372: PBTS: Treat proposal and block parts explicitly in the spec][issue372]
+- [tendermint/spec#377: PBTS: margins for proposal times assigned by Byzantine proposers][issue377]
 
 ### Closed issues
 
-- [Proposer time - fix message filter condition #353][issue353]
-- [PBTS: association between timely predicate and timeout_commit #370][issue370]
+- [tendermint/spec#353: Proposer time - fix message filter condition][issue353]
+- [tendermint/spec#370: PBTS: association between timely predicate and timeout_commit][issue370]
+- [tendermint/spec#371: PBTS: should synchrony parameters be adaptive?][issue371]
 
 [main_v1]: ./v1/pbts_001_draft.md
 
-[algorithm]: ./pbts-algorithm_002_draft.md
+[algorithm]: ./pbts-algorithm.md
 [algorithm_v1]: ./v1/pbts-algorithm_001_draft.md
 
-[sysmodel]: ./pbts-sysmodel_002_draft.md
+[sysmodel]: ./pbts-sysmodel.md
 [sysmodel_v1]: ./v1/pbts-sysmodel_001_draft.md
+[timely-predicate]: ./pbts-sysmodel.md#timely-predicate
 
-[proposertla]: ./tla/TendermintPBT_001_draft.tla
+[proposertla]: ./tla/README.md
 
 [bfttime]: ../bft-time.md
 [arXiv]: https://arxiv.org/pdf/1807.04938.pdf