Merge remote-tracking branch 'origin/add-makefile' into add-makefile

specs/consensus/misbehavior.md

@@ -69,19 +69,20 @@ constitute a source of information for social or legal actions after-the-fact.
 CometBFT only record specific misbehavior, namely the [duplicate vote
 evidence](https://github.com/cometbft/cometbft/blob/main/spec/core/data_structures.md#duplicatevoteevidence).
 While attacks are rare, such behavior has been observed as a result of
-misconfiguration. Most companies operating a validator typically implement this
+misconfiguration. Most companies operating a consensus process (also known as a
+_validator_) typically implement this
 node as a fault-tolerant setup itself, having copies of the private key of the
-validator on multiple machines. If such a fault-tolerant setup is implemented
+process on multiple machines. If such a fault-tolerant setup is implemented
 poorly or misconfigured, this may result in duplicate (and sometimes
 conflicting) signatures in a protocol step, although no actual attack was
 intended. Still, such behavior may be used for mild penalties (e.g., not paying
 fees to the validator for some time, taking a small penalty of their stake), as
-part of the incentivization scheme motivating validator operators to fix such
+part of the incentivization scheme motivating operators to fix such
 issues and ensure reliability of their node. 
 
 While a single instance of an unintentional double vote of one process does
 not pose big problems (it cannot bring disagreement), repeated unintentional
-double votes by several validator operators having large voting power might
+double votes by several processes having large voting power might
 eventually lead to disagreement and a chain halt. Therefore it make sense to
 incentivize individual operators to fix their setup while the whole system is
 still operational.
@@ -121,26 +122,34 @@ a small proposal message carrying only the has of the value, and the big proposa
       is run.   
 
 Observe that the way it is typically implemented, `proposer(h, r)` is not a
-"mathematical function" that takes as input the height and the round and
-produces an ID. Rather it is typically implemented as a stateful function that
-is based on priorities. The latter depend on voting powers and who has been
-proposer in previous heights.
+"mathematical function" that takes as input the height, the round, and the set
+of processes running that height and returns a process.
+Rather it is typically implemented as a function that keeps an internal state,
+for instance to represent the process priorities, as in the case of
+the [proposer selection procedure of CometBFT][cometbft-proposer].
+The latter depends on voting powers and who has been proposer in previous
+heights.
 
 Verification is more complex than double vote and double propose:
 
 - In contrast to double vote, where it is still trivial to verify the
   misbehavior evidence a week after it was generated, in order to verify bad
-  proposer we need knowledge on the validator priorities at that time. 
+  proposer we may need knowledge of the internal state of the proposer selection
+  algorithm at that time.
 - multiple layers are involved
     - maintaining and updating voting powers is typically an application level
       concern
-    - the `proposer(h, r)` function is situated at the consensus level
+    - the [`proposer(h, r)` function](./overview.md#proposer-selection) is
+      situated at the consensus level
     - misbehavior detection can only happen at consensus level
     - in order to use the evidence, the application must be able to verify the
       evidence. This this case it means that the application must
-        - be aware of the consensus-level `proposer` function and priorities, namely, be able to reproduce the output of `proposer(h, r)` for any given state
+        - be aware of the consensus-level `proposer(h, r)` function and its
+          internal state, namely, be able to reproduce the output of
+          `proposer(h, r)` for any given height
         - potentially have historical data (the evidence might come a couple of
-          blocks after the fact) on validator sets
+          blocks after the fact) on the set of processes running consensus at
+          multiple heights
 
 ### What cannot be done
 
@@ -202,3 +211,5 @@ The change to Tendermint is just that prevote messages have an additional field
 that carries the content of the `vr` field of the proposal that triggered
 the sending of the prevote. 
 See [Accountable Tendermint](./accountable-tm/README.md) for more details.
+
+[cometbft-proposer]: https://github.com/cometbft/cometbft/blob/main/spec/consensus/proposer-selection.md

specs/consensus/overview.md

@@ -411,19 +411,84 @@ correct behaviour provided that `p` is able to prove the existence of a
 
 ## Functions
 
-The [pseudo-code][pseudo-code] of the consensus algorithm includes calls to
-functions that are not defined in the pseudo-code itself, but are assumed to be
+The [pseudo-code][pseudo-code] of the algorithm includes calls to functions
+that are not defined in the pseudo-code itself, but are assumed to be
 implemented by the processes running the consensus protocol.
 
 ### Proposer Selection
 
-The first external function is `proposer(h, r)` that returns the process
-selected as the proposer of round `r` of height `h` of consensus. The roles of
-the proposer of a round are described in the [propose round step](#propose).
-
-> The formalization of the properties requires for the proposer selection
-> algorithm is a work in progress, see
-> https://github.com/informalsystems/malachite/issues/396.
+The `proposer(h, r)` function receives a height `h >= 0` and a round `r >= 0`
+and returns the process, among the processes running height `h`, selected as
+the proposer of round `r` of height `h`.
+The role of the proposer is described in the [`propose`](#propose) round step.
+
+The `proposer(h, r)` function requires the knowledge of the set of processes
+running the height `h` of consensus.
+The set of processes running a given height of consensus is fixed:
+it cannot vary over rounds.
+But different heights on consensus may be run by distinct set of processes and
+processes may have distinct associated [voting powers](#voting-power) in different heights.
+
+#### Determinism
+
+Given a consensus height `h` and the set of processes running height `h`,
+the `proposer(h, r)` function **must be deterministic**.
+This means that any two correct processes that invoke `proposer(h, r)` with the
+same inputs, including the implicit input that is the set of processes running
+consensus height `h` and associated voting powers, should receive the exactly
+same output (process).
+
+#### Correctness
+
+The main goal of the `proposer(h, r)` function is to eventually select a
+correct process to coordinate a round of consensus and to propose an
+appropriate value for it.
+A correct implementation of the function must guarantee that, for every height
+`h`, there is a round `r* >= 0` where `proposer(h, r*)` returns a process `p`
+that is a correct process: `p` does not misbehave nor crash.
+
+Fortunately, it is relatively simple to produce a correct implementation of the
+`proposer(h, r)` method: it is enough to ensure that every process running
+consensus height `h` is selected as the proposer for at least one round.
+In other words, it is enough that processes take turns as the proposers of
+different rounds of a height.
+
+#### Fairness
+
+Tendermint is a consensus algorithm that adheres to the _rotating coordinator_
+approach.
+This means that the role of coordinating rounds and proposing values is
+expected to be played by different processes over time, in successive
+heights of consensus.
+(In contrast to the _fixed coordinator_ approach, where the coordinator or
+proposer is only replaced when it is suspected to be faulty).
+
+While a correct `proposer(h, r)` implementation eventually selects every
+process as the proposer of a round of height `h`, being the proposer of the
+first round of a height is the most relevant role, since most heights of
+consensus are expected to be finalized in round 0.
+A fair proposer selection algorithm should therefore ensure that all processes
+have, over a reasonable long sequence of heights `h`, a similar chance of being
+selected as `proposer(h, 0)`, thus to propose the value that is most likely to be
+decided on that height.
+
+In the case of Proof-of-Stake (PoS) blockchains, where processes are assumed to
+have distinct voting powers, a fair proposer selection algorithm should ensure
+that every process is chosen,  over a reasonable long sequence of heights, as
+`proposer(h, 0)` in a number of heights `h` that is proportional to its voting
+power.
+Observe that when the set of processes running consensus varies over heights,
+so as the voting power associated to each process, producing a fair proposer
+selection algorithm becomes more challenging.
+
+> The [proposer selection procedure of CometBFT][cometbft-proposer], which
+> implements Tendermint in Go, is a useful reference of how a fair proposer
+> selection can be achieved with a dynamic set of processes and voting powers.
+> It is worth noting that this algorithm maintains an internal state, which is
+> updated whenever a new proposer is selected.
+> This means that reproducing the algorithm output requires, in addition to the
+> inputs mentioned in the [Determinism section](#determinism), retrieving or
+> recomputing the associated algorithm's internal state.
 
 ### Proposal value
 
@@ -487,3 +552,4 @@ to the current time plus the duration returned by the corresponding functions
 [pseudo-code]: ./pseudo-code.md
 [tendermint-arxiv]: https://arxiv.org/abs/1807.04938
 [accountable-tendermint]: ./misbehavior.md#misbehavior-detection-and-verification-in-accountable-tendermint
+[cometbft-proposer]: https://github.com/cometbft/cometbft/blob/main/spec/consensus/proposer-selection.md

specs/consensus/quint/statemachineAsync.qnt

@@ -23,6 +23,7 @@ export driver.*
 import consensus.* from "./consensus"
 export consensus.* 
 import votekeeper.* from "./votekeeper"
+import extraSpells.* from "./spells/extra"
 
 const validators: Set[Address]
 const validatorSet: Address -> Weight
@@ -65,10 +66,13 @@ action unchangedAll = all {
     _hist' = _hist
 }
 
+/// Any two processes agree in the consensus instances in which they both have already decided
 val AgreementInv = tuples(Correct, Correct).forall(p => 
-    (system.get(p._1).es.chain != List() and system.get(p._2).es.chain != List())
-        implies
-            system.get(p._1).es.chain[0] == system.get(p._2).es.chain[0])
+    val numDecidedInstances = min(  system.get(p._1).es.chain.length(),
+                                    system.get(p._2).es.chain.length())
+    to(0, numDecidedInstances-1).forall(i =>
+            system.get(p._1).es.chain[i] == system.get(p._2).es.chain[i])
+)
 
 // Actions
 action init = all {
@@ -224,13 +228,21 @@ action deliverSomeCertificate(v: Address) : bool = all {
 }
 
 
-// deliver a message or a certiciate. 
+// deliver a message or a certificate. 
 // Take it from the network buffer of from the faulty set and put it into the incoming sets
 action deliver(v: Address) : bool = any {
-    nondet prop = oneOf(propBuffer.get(v).union(AllFaultyProposals))
-    deliverProposal(v, prop),
-    nondet vote = oneOf(voteBuffer.get(v).union(AllFaultyVotes))
-    deliverVote(v, vote),
+    val props = propBuffer.get(v).union(AllFaultyProposals)
+    all{
+        props.size() > 0,
+        nondet prop = oneOf(props)
+        deliverProposal(v, prop),
+    },
+    val votes = voteBuffer.get(v).union(AllFaultyVotes)
+    all {
+        votes.size() > 0,
+        nondet vote = oneOf(votes)
+        deliverVote(v, vote),
+    },
     deliverSomeCertificate(v),  // we might do fault injection here. But faulty nodes cannot
                                 // totally make up certificates. They cannot forge messages to look 
                                 // like being sent by correct nodes