docs: rebranding to CometBFT

Changed naming and repository URLs to refer to CometBFT.
Exceptions were made for links to old content, GitHub issues/PRs, etc.
that have not been replicated in the cometbft org repos.

docs/spec/README.md

@@ -1,9 +1,9 @@
 # Specification
 
 This directory served as location for English and TLA+
-specifications of the Tendermint protocols "fast sync" and "light
+specifications of the CometBFT protocols "fast sync" and "light
 client". The corresponding specification work is not happening in this directory
-anymore but in the [tendermint/spec](https://github.com/tendermint/spec)
-repository. The most recent versions of the specifications can be found
-there.
+anymore but in the [spec](https://github.com/cometbft/cometbft/tree/main/spec)
+directory of the CometBFT repository.
+The most recent versions of the specifications can be found there.
 

docs/spec/fastsync/README.md

@@ -9,7 +9,7 @@ for the most recent version.
 ## Abstract
 
 This directory contains English and TLA+ specifications for the FastSync
-protocol as it is currently implemented in the Tendermint Core codebase.
+protocol as it is currently implemented in the CometBFT Core codebase.
 
 ## English Specification
 
@@ -36,7 +36,7 @@ the redundancies between them, improve their utility to researchers and
 engineers, and to improve their verifiability. For now, they provide a complete
 description of the fast sync protocol in TLA+; especially the
 [scheduler.tla](scheduler.tla), which maps very closely to the current
-implementation of the [scheduler in Go](https://github.com/tendermint/tendermint/blockchain/v2/scheduler.go).
+implementation of the [scheduler in Go](https://github.com/cometbft/cometbft/blockchain/v2/scheduler.go).
 
 The [scheduler.tla](scheduler.tla) can be model checked in TLC with the following
 parameters:

docs/spec/fastsync/Tinychain.tla

@@ -3,7 +3,7 @@
 
    https://github.com/tendermint/spec/tree/master/rust-spec/fastsync
 
-   A very abstract model of Tendermint blockchain. Its only purpose is to highlight
+   A very abstract model of CometBFT blockchain. Its only purpose is to highlight
    the relation between validator sets, next validator sets, and last commits.
  *)
 

docs/spec/fastsync/fastsync.md

@@ -9,25 +9,25 @@ for the most recent version.
 ## Abstract
 
 Fastsync is a protocol that is used by a node to catch-up to the
-current state of a Tendermint blockchain. Its typical use case is a
+current state of a CometBFT blockchain. Its typical use case is a
 node that was disconnected from the system for some time. The
 recovering node locally has a copy of a prefix of the blockchain,
 and the corresponding application state that is slightly outdated. It
 then queries its peers for the blocks that were decided on by the
-Tendermint blockchain during the period the full node was
+CometBFT blockchain during the period the full node was
 disconnected. After receiving these blocks, it executes the
 transactions in the blocks in order to catch-up to the current height
 of the blockchain and the corresponding application state.
 
 In practice it is sufficient to catch-up only close to the current
-height: The Tendermint consensus reactor implements its own catch-up
+height: The CometBFT consensus reactor implements its own catch-up
 functionality and can synchronize a node that is close to the current height,
 perhaps within 10 blocks away from the current height of the blockchain.
 Fastsync should bring a node within this range.
 
 ## Outline
 
-- [Part I](#part-i---tendermint-blockchain): Introduction of Tendermint
+- [Part I](#part-i---cometbft-blockchain): Introduction of CometBFT
 blockchain terms that are relevant for FastSync protocol.
 
 - [Part II](#part-ii---sequential-definition-of-fastsync-problem): Introduction
@@ -84,7 +84,7 @@ In this document we quite extensively use tags in order to be able to
 reference assumptions, invariants, etc. in future communication. In
 these tags we frequently use the following short forms:
 
-- TMBC: Tendermint blockchain
+- TMBC: CometBFT blockchain
 - SEQ: for sequential specifications
 - FS: Fastsync
 - LIVE: liveness
@@ -96,9 +96,9 @@ these tags we frequently use the following short forms:
 - NewFS: refers to improved future Fastsync implementations
 
 
-# Part I - Tendermint Blockchain
+# Part I - CometBFT Blockchain
 
-We will briefly list some of the notions of Tendermint blockchains that are
+We will briefly list some of the notions of CometBFT blockchains that are
 required for this specification. More details can be found [here][block].
 
 #### **[TMBC-HEADER]**:
@@ -111,7 +111,7 @@ headers, rather than a list of blocks.
 
 #### **[TMBC-SEQ]**:
 
-The Tendermint blockchain is a list *chain* of headers.
+The CometBFT blockchain is a list *chain* of headers.
 
 #### **[TMBC-SEQ-GROW]**:
 
@@ -201,7 +201,7 @@ A full node has as input a block of the blockchain at height *h* and
 the corresponding application state (or the prefix of the current
 blockchain until height *h*). It has access to a set *peerIDs* of full
 nodes called *peers* that it knows of.  The full node uses the peers
-to read blocks of the Tendermint blockchain (in a safe way, that is,
+to read blocks of the CometBFT blockchain (in a safe way, that is,
 it checks the soundness conditions), until it has read the most recent
 block and then terminates.
 
@@ -216,7 +216,7 @@ as output (i) a list *L* of blocks starting at height *h* to some height
 *terminationHeight*, and (ii) the application state when applying the
 transactions of the list *L* to *s*.
 
-> In Tendermint, the commit for block of height *h* is contained in block *h + 1*,
+> In CometBFT, the commit for block of height *h* is contained in block *h + 1*,
 > and thus the block of height *h + 1* is needed to verify the block of
 > height *h*. Let us therefore clarify the following on the
 > termination height:
@@ -338,7 +338,7 @@ Initially, the set *peerIDs* contains at least one correct full node.
 > of the blockchain (it might lag behind), the property [FS-SEQ-SAFE-START]
 > cannot be ensured in an unreliable distributed setting. We consider
 > the following relaxation. (Which is typically sufficient for
-> Tendermint, as the consensus reactor then synchronizes from that
+> CometBFT, as the consensus reactor then synchronizes from that
 > height.)
 
 #### **[FS-DIST-SAFE-START]**:
@@ -420,15 +420,15 @@ are structured as finite state machines that receive input events and emit
 output events. The demuxer is responsible for all IO, including translating
 between internal events and IO messages, and routing events between components.
 
-Protocols in Tendermint can be considered to consist of two
+Protocols in CometBFT can be considered to consist of two
 components: a "core" state machine and a "peer" state machine. The core state
 machine refers to the internal state managed by the node, while the peer state
 machine determines what messages to send to peers. In the FastSync design, the
 core and peer state machines correspond to the processor and scheduler,
 respectively.
 
 In the case of FastSync, the core state machine (the processor) is effectively
-just the Tendermint block execution function, while virtually all protocol logic
+just the CometBFT block execution function, while virtually all protocol logic
 is contained in the peer state machine (the scheduler). The processor is
 only implemented as a separate component due to the computationally expensive nature
 of block execution. We therefore focus our specification here on the peer state machine
@@ -548,7 +548,7 @@ type bcBlockResponseMessage struct {
 ```
 
 Remark:
-- `msg.Block` is a Tendermint block as defined in [[block]].
+- `msg.Block` is a CometBFT block as defined in [[block]].
 - `msg.Block` != nil
 
 #### bcStatusRequestMessage
@@ -1142,7 +1142,7 @@ Arguments:
 
 [[block]] Specification of the block data structure.
 
-<!-- [[blockchain]] The specification of the Tendermint blockchain. Tags referring to this specification are labeled [TMBC-*]. -->
+<!-- [[blockchain]] The specification of the CometBFT blockchain. Tags referring to this specification are labeled [TMBC-*]. -->
 
 [block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md
 

docs/spec/fastsync/fastsync.tla

@@ -6,7 +6,7 @@
 
  In this document we give the high level specification of the fast sync
  protocol as implemented here:
- https://github.com/tendermint/tendermint/tree/main/blockchain/v2.
+ https://github.com/cometbft/cometbft/tree/main/blockchain/v2.
 
 We assume a system in which one node is trying to sync with the blockchain
 (replicated state machine) by downloading blocks from the set of full nodes
@@ -230,7 +230,7 @@ InitNode ==
 
 \* Remove faulty peers.
 \* Returns new block pool.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L222
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L222
 RemovePeers(rmPeers, bPool) ==
     LET keepPeers == bPool.peerIds \ rmPeers IN
     LET pHeights ==
@@ -258,7 +258,7 @@ RemovePeers(rmPeers, bPool) ==
     ELSE bPool
 
 \* Add a peer.
-\* see https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L198
+\* see https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L198
 AddPeer(peer, bPool) ==
     [bPool EXCEPT !.peerIds = bPool.peerIds \union {peer}]
 
@@ -268,7 +268,7 @@ Handle StatusResponse message.
 If valid status response, update peerHeights.
 If invalid (height is smaller than the current), then remove peer.
 Returns new block pool.
-See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L667
+See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L667
 *)
 HandleStatusResponse(msg, bPool) ==
     LET peerHeight == bPool.peerHeights[msg.peerId] IN
@@ -286,7 +286,7 @@ Handle BlockResponse message.
 If valid block response, update blockStore, pendingBlocks and receivedBlocks.
 If invalid (unsolicited response or malformed block), then remove peer.
 Returns new block pool.
-See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522
+See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522
 *)
 HandleBlockResponse(msg, bPool) ==
     LET h == msg.block.height IN
@@ -308,7 +308,7 @@ HandleBlockResponse(msg, bPool) ==
 
 
 \* Compute max peer height.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L440
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L440
 MaxPeerHeight(bPool) ==
     IF bPool.peerIds = AsPidSet({})
     THEN 0 \* no peers, just return 0
@@ -317,7 +317,7 @@ MaxPeerHeight(bPool) ==
 
 (* Returns next height for which request should be sent.
    Returns NilHeight in case there is no height for which request can be sent.
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L454 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L454 *)
 FindNextRequestHeight(bPool) ==
     LET S == {i \in Heights:
                 /\ i >= bPool.height
@@ -341,7 +341,7 @@ NumOfPendingRequests(bPool, peer) ==
 
 (* Returns peer that can serve block for a given height.
    Returns NilPeer in case there are no such peer.
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L477 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L477 *)
 FindPeerToServe(bPool, h) ==
     LET peersThatCanServe == { p \in bPool.peerIds:
                 /\ bPool.peerHeights[p] >= h
@@ -379,23 +379,23 @@ CreateRequest(bPool) ==
 
 
 \* Returns node state, i.e., defines termination condition.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L432
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L432
 ComputeNextState(bPool) ==
     IF bPool.syncedBlocks = 0  \* corresponds to the syncTimeout in case no progress has been made for a period of time.
     THEN "finished"
     ELSE IF /\ bPool.height > 1
-            /\ bPool.height >= MaxPeerHeight(bPool) \* see https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/scheduler.go#L566
+            /\ bPool.height >= MaxPeerHeight(bPool) \* see https://github.com/cometbft/cometbft/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/scheduler.go#L566
          THEN "finished"
          ELSE "running"
 
 (* Verify if commit is for the given block id and if commit has enough voting power.
-   See https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *)
+   See https://github.com/cometbft/cometbft/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *)
 VerifyCommit(block, lastCommit) ==
     PossibleCommit(block, lastCommit)
 
 (* Tries to execute next block in the pool, i.e., defines block validation logic.
    Returns new block pool (peers that has send invalid blocks are removed).
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *)
 ExecuteBlocks(bPool) ==
     LET bStore == bPool.blockStore IN
     LET block0 == bStore[bPool.height - 1] IN
@@ -426,7 +426,7 @@ ExecuteBlocks(bPool) ==
 
 
 \* Defines logic for pruning peers.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L613
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L613
 TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
     (* -----------------------------------------------------------------------------------------------------------------------*)
     (* Corresponds to function prunablePeers in scheduler.go file. Note that this function only checks if block has been  *)
@@ -436,7 +436,7 @@ TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
     (* In case of faulty peers, we don't have any guarantee that they will respond.                                           *)
     (* Therefore, we model this with nondeterministic behavior as it could lead to peer removal, for both correct and faulty. *)
     (* See scheduler.go                                                                                                       *)
-    (* https://github.com/tendermint/tendermint/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L335 *)
+    (* https://github.com/cometbft/cometbft/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L335 *)
     LET toRemovePeers == bPool.peerIds \intersect suspectedSet IN
 
     (*
@@ -446,7 +446,7 @@ TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
       correct peers respond timely and reliably. However, if a request is sent to a faulty peer then we 
       might get response on time or not, which is modelled with nondeterministic isTimedOut flag.
       See scheduler.go
-      https://github.com/tendermint/tendermint/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L617
+      https://github.com/cometbft/cometbft/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L617
     *)
     LET nextHeightPeer == bPool.pendingBlocks[bPool.height] IN
     LET prunablePeers ==

docs/spec/fastsync/scheduler.tla

@@ -6,7 +6,7 @@
 
  A specification of the fast sync scheduler that is introduced in blockchain/v2:
  
- https://github.com/tendermint/tendermint/tree/brapse/blockchain-v2-riri-reactor-2
+ https://github.com/cometbft/cometbft/tree/brapse/blockchain-v2-riri-reactor-2
  
  The model includes:
     - a scheduler that maintains the peers and blocks that it receives from the peers, and
@@ -108,7 +108,7 @@ OutEvents ==
 (* ----------------------------------------------------------------------------------------------*)
 (* The behavior of the scheduler that keeps track of peers, block requests and responses, etc.   *)
 (* See scheduler.go                                                                              *)
-(* https://github.com/tendermint/tendermint/blob/v0.33.3/blockchain/v2/scheduler.go              *)
+(* https://github.com/cometbft/cometbft/blob/v0.33.3/blockchain/v2/scheduler.go              *)
 (* ----------------------------------------------------------------------------------------------*)
 
 addPeer(sc, peerID) == 
@@ -244,7 +244,7 @@ highPeers(sc, minH) == {p \in sc.peers: sc.peerHeights[p] >= minH}
 (* ----------------------------------------------------------------------------------------------*)
 (* The behavior of the scheduler state machine                                                   *)
 (* See scheduler.go                                                                              *)
-(* https://github.com/tendermint/tendermint/tree/brapse/blockchain-v2-riri-reactor-2/scheduler.go*)
+(* https://github.com/cometbft/cometbft/tree/brapse/blockchain-v2-riri-reactor-2/scheduler.go*)
 (* ----------------------------------------------------------------------------------------------*)
 blStateInit(h, start) ==
   IF h <= start THEN

docs/spec/fastsync/verification/Tinychain.tla

@@ -1,5 +1,5 @@
 -------------------------- MODULE Tinychain ----------------------------------
-(* A very abstract model of Tendermint blockchain. Its only purpose is to highlight
+(* A very abstract model of CometBFT blockchain. Its only purpose is to highlight
    the relation between validator sets, next validator sets, and last commits.
  *)