Proposer-based timestamp specification (#261)

* added proposer-based timestamp spec * Update spec/consensus/proposer-based-timestamp/pbts_001_draft.md Co-authored-by: Aleksandr Bezobchuk <alexanderbez@users.noreply.github.com> * Update spec/consensus/proposer-based-timestamp/pbts_001_draft.md Co-authored-by: Aleksandr Bezobchuk <alexanderbez@users.noreply.github.com> * Update spec/consensus/proposer-based-timestamp/pbts-algorithm_001_draft.md Co-authored-by: Marko <marbar3778@yahoo.com> * Update spec/consensus/proposer-based-timestamp/pbts-algorithm_001_draft.md * Update spec/consensus/proposer-based-timestamp/pbts-sysmodel_001_draft.md Co-authored-by: Callum Waters <cmwaters19@gmail.com> * fixes from PR Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> Co-authored-by: Aleksandr Bezobchuk <alexanderbez@users.noreply.github.com> Co-authored-by: Marko <marbar3778@yahoo.com> Co-authored-by: Callum Waters <cmwaters19@gmail.com>
4 years ago · 640b71038b
--- a/spec/consensus/proposer-based-timestamp/README.md
+++ b/spec/consensus/proposer-based-timestamp/README.md
@ -0,0 +1,19 @@
 # Proposer-Based Timestamps
 This section describes a version of the Tendermint consensus protocol,
 which uses proposer-based timestamps.
 ## Contents 
 - [Proposer-Based Time][main] (entry point)
 - [Part I - System Model and Properties][sysmodel]
 - [Part II - Protocol Specification][algorithm]
 - [TLA+ Specification][proposertla]
 [algorithm]: ./pbts-algorithm_001_draft.md
 [sysmodel]: ./pbts-sysmodel_001_draft.md
 [main]: ./pbts_001_draft.md
 [proposertla]: ./tla/TendermintPBT_001_draft.tla
--- a/spec/consensus/proposer-based-timestamp/pbts-algorithm_001_draft.md
+++ b/spec/consensus/proposer-based-timestamp/pbts-algorithm_001_draft.md
@ -0,0 +1,152 @@
 # Proposer-Based Time - Part II
 ## Updated Consensus Algorithm
 ### Outline
 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`. 
 #### **[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.
 #### 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
 We update the timeout for the `PROPOSE` step according to the following reasoning:
 - If a correct proposer needs to wait to make sure its proposed time is larger than the `blockTime` of the previous block, then it sends by realtime `blockTime + ACCURACY` (By this time, its local clock must exceed `blockTime`)
 - the receiver will receive a `PROPOSE` message by `blockTime + ACCURACY + MSGDELAY`
 - the receiver's local clock will be `<= blockTime + 2 * ACCURACY + MSGDELAY`
 - thus when the receiver `p` enters this round it can set its timeout to a value `waitingTime => blockTime + 2 * ACCURACY + MSGDELAY - now_p`
 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. 
 Also, `BLOCKDELAY` needs to be added to `waitingTime`.
 #### **[PBTS-ALG-STARTROUND.0]**
 ```go
 function StartRound(round) {
  blockTime ← block time of block h_p - 1
  waitingTime ← blockTime + 2 * ACCURACY + MSGDELAY - now_p
  round_p ← round
  step_p ← propose
  if proposer(h_p, round_p) = p {
    wait until now_p > blockTime // new wait condition
    if validValue_p != nil {
      proposal ← (validValue_p, now_p) // added "now_p"
    }
    else {
      proposal ← (getValue(), now_p)   // added "now_p"
    }
    broadcast ⟨PROPOSAL, h_p, round_p, proposal, validRound_p⟩
  }
  else {
    schedule OnTimeoutPropose(h_p,round_p) to be executed after max(timeoutPropose(round_p), waitingTime)
  }
 }
 ```
 #### New Rule Replacing Lines 22 - 27
 - a validator prevotes for the consensus value `v` **and** the time `t`
 - 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) {
    broadcast ⟨PREVOTE, h_p, round_p, id(v,t)⟩ 
  }
  else {
    broadcast ⟨PREVOTE, h_p, round_p, nil⟩ 
  }
  step_p ← prevote
 }
 ```
 #### 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. 
 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 {
  if valid(v) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) {
    broadcast ⟨PREVOTE, h_p, roundp, id(v, tprop)⟩
  }
  else {
    broadcast ⟨PREVOTE, hp, roundp, nil⟩
  }
  step_p ← prevote
 }
 ```
 #### New Rule Replacing Lines 36 - 43
 - As above, in the following `(v,t)` is part of the message rather than `v`
 - 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 {
    lockedValue_p ← v
    lockedRound_p ← round_p
    broadcast ⟨PRECOMMIT, h_p, round_p, id(v,t))⟩ 
    step_p ← precommit
  }
  validValue_p ← v 
  validRound_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. 
 > 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) {
    decision_p [h_p] = (v,t) // decide on time too
    h_p ← h_p + 1
    reset lockedRound_p , lockedValue_p, validRound_p and validValue_p to initial values and empty message log 
    StartRound(0)
  }
 }
 ```
 **All other rules remains unchanged.**
 Back to [main document][main].
 [main]: ./pbts_001_draft.md
 [arXiv]: https://arxiv.org/abs/1807.04938
 [tlatender]: https://github.com/tendermint/spec/blob/master/rust-spec/tendermint-accountability/README.md
 [bfttime]: https://github.com/tendermint/spec/blob/439a5bcacb5ef6ef1118566d7b0cd68fff3553d4/spec/consensus/bft-time.md
 [lcspec]: https://github.com/tendermint/spec/blob/439a5bcacb5ef6ef1118566d7b0cd68fff3553d4/rust-spec/lightclient/README.md
--- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_001_draft.md
+++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_001_draft.md
@ -0,0 +1,179 @@
 # Proposer-Based Time - Part I
 ## System Model
 ### 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`
 ### Message Delays
 We do not want to interfere with the Tendermint timing assumptions. We will postulate a timing restriction, which, if satisfied, ensures that liveness is preserved.
 In general the local clock may drift from the global time. (It may progress faster, e.g., one second of clock time might take 1.005 seconds of real-time). As a result the local clock and the global clock may be measured in different time units. Usually, the message delay is measured in global clock time units. To estimate the correct local timeout precisely, we would need to estimate the clock time duration of a message delay taking into account the clock drift. For simplicity we ignore this, and directly postulate the message delay assumption in terms of local time.
 #### **[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.
 #### **[PBTS-MSG-FAIR.0]**
 The message end-to-end delay between a correct proposer and a correct validator (for `PROPOSE` messages) is less than `MSGDELAY`.
 ## Problem Statement
 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`. 
 #### **[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`. 
 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. 
 ### SAFETY
 Here we will provide specifications that relate local time to block time. However, since we do not assume (by now) that local time is linked to real-time, these specifications also do not provide a relation between block time and real-time. Such properties are given [later](#REAL-TIME-SAFETY).
 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)` 
 for all correct validators `V`.
 > Observe that `beginConsensus(k) <= last-beginConsensus(k)` and if local clocks are monotonic, then `last-beginConsensus(k) <= endConsensus(k)`.
 #### **[PBTS-CLOCK-GROW.0]**
 We assume that during one consensus instance, local clocks are not set back, in particular for each correct validator `V` and each height `k`, we have `beginConsensus(V,k) < endConsensus(V,k)`.
 #### **[PBTS-CONSENSUS-TIME-VALID.0]**
 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 
 - `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 
 - [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. 
 #### **[PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]**
 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 `beginConsensus_k <= b.time <= last-beginConsensus_k`.
 > For the above two properties we will assume that a correct proposer `v` sends its `PROPOSAL` at its local time `beginConsensus(v,k)`.
 ### LIVENESS
 If 
 - [TMBC-FM-2THIRDS.0] holds for a block of height `k - 1`, and
 - [PBTS-MSG-FAIR.0],
 - [PBTS-CLOCK.0], and
 - [PBTS-CLOCK-GROW.0] (**TODO:** is that enough?)
 then eventually there is a valid commit `c` for height `k`.
 ### REAL-TIME SAFETY
 > We want to give a property that can be exploited from the outside, that is, given a block with some time stored in it, what is the estimate at which real-time the block was generated. To do so, we need to link clock-time to real-time; which is not the case with [PBTS-CLOCK.0]. For this, we introduce the following assumption on the clocks:
 #### **[PBTS-CLOCKSYNC-EXTERNAL.0]**
 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
 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`.
 #### **[PBTS-CONSENSUS-REALTIME-VALID.0]**
 Let `b` be a block with a valid commit that contains at least one `precommit` message by a correct validator (and `proposalTime` is the time for the height/round `propose` message `m` that triggered the `precommit`). Then:
 `propRecvTime(m) - ACCURACY - PRECISION < b.time < propRecvTime(m) + ACCURACY + PRECISION + MSGDELAY`
 #### **[PBTS-CONSENSUS-REALTIME-VALID-CORR.0]**
 Let `b` be a block with a valid commit that contains at least one `precommit` message by a correct validator (and `proposalTime` is the time for the height/round `propose` message `m` that triggered the `precommit`). Then, if the proposer is correct:
 `proposalTime(m) - ACCURACY < b.time < proposalTime(m) + ACCURACY`
 > 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`.
 Back to [main document][main].
 [main]: ./pbts_001_draft.md
 [arXiv]: https://arxiv.org/abs/1807.04938
 [tlatender]: https://github.com/tendermint/spec/blob/master/rust-spec/tendermint-accountability/README.md
 [bfttime]: https://github.com/tendermint/spec/blob/439a5bcacb5ef6ef1118566d7b0cd68fff3553d4/spec/consensus/bft-time.md
 [lcspec]: https://github.com/tendermint/spec/blob/439a5bcacb5ef6ef1118566d7b0cd68fff3553d4/rust-spec/lightclient/README.md
 [algorithm]: ./pbts-algorithm_001_draft.md
 [sysmodel]: ./pbts-sysmodel_001_draft.md
--- a/spec/consensus/proposer-based-timestamp/pbts_001_draft.md
+++ b/spec/consensus/proposer-based-timestamp/pbts_001_draft.md
@ -0,0 +1,268 @@
 # Proposer-Based Time
 ## 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. **Liveness.** The liveness of the protocol:
   1. does not depend on clock synchronization,
   1. depends on bounded message delays.
 1. **Relation to real time.** There is no clock synchronizaton, which implies that there is **no relation** between the computed block `time` and real time.
 1. **Aggregate signatures.** As the `precommit` messages contain the local times, all these `precommit` messages typically differ in the time field, which **prevents** the use of aggregate signatures.
 ## Suggested Proposer-Based Time
 ### 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). 
 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. **Proposer influence on block time.** The proposer of the next block
 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:
   1. depends on the introduced assumptions on synchronized clocks (see below),
   1. still depends on the message delays (unavoidable).
 1. **Relation to real time.** We formalize clock synchronization, and obtain a **well-defined relation** between the block `time` and real time.
 1. **Aggregate signatures.** The `precommit` messages free of time, which **allows** for aggregate signatures.
 ### 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`. 
 #### 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 
 <table>
 <tr>
 <th>arXiv paper</th>
 <th>Proposer-based time</th>
 </tr>
 <tr>
 <td>
 ```go
 function StartRound(round) {
 round_p ← round
 step_p ← propose
 if proposer(h_p, round_p) = p {
  if validValue_p != nil {
   proposal ← validValue_p
  } else {
   proposal ← getValue()
  }
   broadcast ⟨PROPOSAL, h_p, round_p, proposal, validRound_p⟩
 } else {
  schedule OnTimeoutPropose(h_p,round_p) to 
   be executed after timeoutPropose(round_p)
 }
 }
 ```
 </td>
 <td>
 ```go
 function StartRound(round) {
 round_p ← round
 step_p ← propose
 if proposer(h_p, round_p) = p {
  // new wait condition
  wait until now_p > block time of block h_p - 1
  if validValue_p != nil {
   // add "now_p"
   proposal ← (validValue_p, now_p) 
  } else {
   // add "now_p"
   proposal ← (getValue(), now_p) 
  }
  broadcast ⟨PROPOSAL, h_p, round_p, proposal, validRound_p⟩
 } else {
  schedule OnTimeoutPropose(h_p,round_p) to 
   be executed after timeoutPropose(round_p)
 }
 }
 ```
 </td>
 </tr>
 </table>
 - Rule on lines 28-35
 <table>
 <tr>
 <th>arXiv paper</th>
 <th>Proposer-based time</th>
 </tr>
 <tr>
 <td>
 ```go
 upon timely(⟨PROPOSAL, h_p, round_p, v, vr⟩) 
 from proposer(h_p, round_p)
 AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩ 
 while step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do {
 if valid(v) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) {
  broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩
 } else {
  broadcast ⟨PREVOTE, hp, round_p, nil⟩
 }
 }
 ```
 </td>
 <td>
 ```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 {
  if valid(v) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) {
   // send hash of v and tprop in PREVOTE message
   broadcast ⟨PREVOTE, h_p, round_p, id(v, tprop)⟩
  } else {
   broadcast ⟨PREVOTE, hp, round_p, nil⟩
  }
 }
 ```
 </td>
 </tr>
 </table>
 - Rule on lines 49-54
 <table>
 <tr>
 <th>arXiv paper</th>
 <th>Proposer-based time</th>
 </tr>
 <tr>
 <td>
 ```go
 upon ⟨PROPOSAL, h_p, r, v, ∗⟩ from proposer(h_p, r) 
 AND 2f + 1 ⟨PRECOMMIT, h_p, r, id(v)⟩ 
 while decisionp[h_p] = nil do {
  if valid(v) {
   decision_p [h_p] = v
   h_p ← h_p + 1
   reset lockedRound_p , lockedValue_p, validRound_p and 
    validValue_p to initial values and empty message log 
   StartRound(0)
  }
 }
 ```
 </td>
 <td>
 ```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) {
   // decide on time too
   decision_p [h_p] = (v,t) 
   h_p ← h_p + 1
   reset lockedRound_p , lockedValue_p, validRound_p and 
    validValue_p to initial values and empty message log 
   StartRound(0)
  }
 }
 ```
 </td>
 </tr>
 </table>
 - Other rules are extended in a similar way, or remain unchanged
 ### Property Overview
 #### Safety and Liveness
 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, 
 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`.
 #### Relation to Real-Time
 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. 
 ### Detailed Specification
 This specification describes the changes needed to be done to the Tendermint consensus algorithm as described in the [arXiv paper][arXiv] and the simplified specification in [TLA+][tlatender], and makes precise the underlying assumptions and the required properties.
 - [Part I - System Model and Properties][sysmodel]
 - [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
 [bfttime]: https://github.com/tendermint/spec/blob/439a5bcacb5ef6ef1118566d7b0cd68fff3553d4/spec/consensus/bft-time.md
 [lcspec]: https://github.com/tendermint/spec/blob/439a5bcacb5ef6ef1118566d7b0cd68fff3553d4/rust-spec/lightclient/README.md
 [algorithm]: ./pbts-algorithm_001_draft.md
 [sysmodel]: ./pbts-sysmodel_001_draft.md
 [main]: ./pbts_001_draft.md
 [proposertla]: ./tla/TendermintPBT_001_draft.tla
--- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
+++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
@ -0,0 +1,597 @@
 -------------------- MODULE TendermintPBT_001_draft ---------------------------
 (*
 A TLA+ specification of a simplified Tendermint consensus, with added clocks 
 and proposer-based timestamps. This TLA+ specification extends and modifies 
 the Tendermint TLA+ specification for fork accountability: 
    https://github.com/tendermint/spec/blob/master/spec/light-client/accountability/TendermintAcc_004_draft.tla
 * Version 1. A preliminary specification.
 Zarko Milosevic, Igor Konnov, Informal Systems, 2019-2020.
 Ilina Stoilkovska, Josef Widder, Informal Systems, 2021.
 *)
 EXTENDS Integers, FiniteSets
 (********************* PROTOCOL PARAMETERS **********************************)
 CONSTANTS
    Corr,          \* the set of correct processes 
    Faulty,        \* the set of Byzantine processes, may be empty
    N,             \* the total number of processes: correct, defective, and Byzantine
    T,             \* an upper bound on the number of Byzantine processes
    ValidValues,   \* the set of valid values, proposed both by correct and faulty
    InvalidValues, \* the set of invalid values, never proposed by the correct ones
    MaxRound,      \* the maximal round number
    MaxTimestamp,  \* the maximal value of the clock tick
    Delay,         \* message delay
    Precision,     \* clock precision: the maximal difference between two local clocks  
    Accuracy,      \* clock accuracy: the maximal difference between a local clock and the real time
    Proposer,      \* the proposer function from 0..NRounds to 1..N
    ClockDrift     \* is there clock drift between the local clocks and the global clock
 ASSUME(N = Cardinality(Corr \union Faulty))
 (*************************** DEFINITIONS ************************************)
 AllProcs == Corr \union Faulty      \* the set of all processes
 Rounds == 0..MaxRound               \* the set of potential rounds
 Timestamps == 0..MaxTimestamp       \* the set of clock ticks
 NilRound == -1   \* a special value to denote a nil round, outside of Rounds
 NilTimestamp == -1 \* a special value to denote a nil timestamp, outside of Ticks
 RoundsOrNil == Rounds \union {NilRound}
 Values == ValidValues \union InvalidValues \* the set of all values
 NilValue == "None"  \* a special value for a nil round, outside of Values
 Proposals == Values \X Timestamps
 NilProposal == <<NilValue, NilTimestamp>>
 ValuesOrNil == Values \union {NilValue}
 Decisions == Values \X Timestamps \X Rounds
 NilDecision == <<NilValue, NilTimestamp, NilRound>>
 \* a value hash is modeled as identity
 Id(v) == v
 \* The validity predicate
 IsValid(v) == v \in ValidValues
 \* the two thresholds that are used in the algorithm
 THRESHOLD1 == T + 1     \* at least one process is not faulty
 THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
 Min(S) == CHOOSE x \in S : \A y \in S : x <= y
 Max(S) == CHOOSE x \in S : \A y \in S : y <= x
 (********************* TYPE ANNOTATIONS FOR APALACHE **************************)
 \* the operator for type annotations
 a <: b == a
 \* the type of message records
 MT == [type |-> STRING, src |-> STRING, round |-> Int,
       proposal |-> <<STRING, Int>>, validRound |-> Int, id |-> <<STRING, Int>>]
 RP == <<STRING, MT>>  
 \* a type annotation for a message
 AsMsg(m) == m <: MT
 \* a type annotation for a set of messages
 SetOfMsgs(S) == S <: {MT}       
 \* a type annotation for an empty set of messages
 EmptyMsgSet == SetOfMsgs({})
 SetOfRcvProp(S) == S <: {RP}
 EmptyRcvProp == SetOfRcvProp({})
 SetOfProc(S) == S <: {STRING}
 EmptyProcSet == SetOfProc({})
 (********************* PROTOCOL STATE VARIABLES ******************************)
 VARIABLES
  round,    \* a process round number: Corr -> Rounds
  localClock,   \* a process local clock: Corr -> Ticks
  realTime, \* a reference Newtonian real time
  step,     \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
  decision, \* process decision: Corr -> ValuesOrNil
  lockedValue,  \* a locked value: Corr -> ValuesOrNil
  lockedRound,  \* a locked round: Corr -> RoundsOrNil
  validValue,   \* a valid value: Corr -> ValuesOrNil
  validRound    \* a valid round: Corr -> RoundsOrNil
 \* book-keeping variables
 VARIABLES
  msgsPropose,   \* PROPOSE messages broadcast in the system, Rounds -> Messages
  msgsPrevote,   \* PREVOTE messages broadcast in the system, Rounds -> Messages
  msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
  receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message, {<<Corr, Messages>>}
  inspectedProposal, \* used to keep track when a process tries to receive a message, [Rounds -> <<Corr, Messages>>]
  evidence, \* the messages that were used by the correct processes to make transitions
  action,        \* we use this variable to see which action was taken
  beginConsensus, \* the minimum of the local clocks in the initial state, Int
  endConsensus, \* the local time when a decision is made, [Corr -> Int]
  lastBeginConsensus, \* the maximum of the local clocks in the initial state, Int
  proposalTime, \* the real time when a proposer proposes in a round, [Rounds -> Int]
  proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round, [Rounds -> Int]
 (* to see a type invariant, check TendermintAccInv3 *)  
 \* a handy definition used in UNCHANGED
 vars == <<round, step, decision, lockedValue, lockedRound,
          validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
          localClock, realTime, receivedTimelyProposal, inspectedProposal, action,
          beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
 (********************* PROTOCOL INITIALIZATION ******************************)
 FaultyProposals(r) ==
    SetOfMsgs([type: {"PROPOSAL"}, src: Faulty,
               round: {r}, proposal: Proposals, validRound: RoundsOrNil])
 AllFaultyProposals ==
    SetOfMsgs([type: {"PROPOSAL"}, src: Faulty,
               round: Rounds, proposal: Proposals, validRound: RoundsOrNil])
 FaultyPrevotes(r) ==
    SetOfMsgs([type: {"PREVOTE"}, src: Faulty, round: {r}, id: Proposals])
 AllFaultyPrevotes ==    
    SetOfMsgs([type: {"PREVOTE"}, src: Faulty, round: Rounds, id: Proposals])
 FaultyPrecommits(r) ==
    SetOfMsgs([type: {"PRECOMMIT"}, src: Faulty, round: {r}, id: Proposals])
 AllFaultyPrecommits ==
    SetOfMsgs([type: {"PRECOMMIT"}, src: Faulty, round: Rounds, id: Proposals])
 AllProposals ==
    SetOfMsgs([type: {"PROPOSAL"}, src: AllProcs,
               round: Rounds, proposal: Proposals, validRound: RoundsOrNil])    
 RoundProposals(r) ==
    SetOfMsgs([type: {"PROPOSAL"}, src: AllProcs,
               round: {r}, proposal: Proposals, validRound: RoundsOrNil])    
 BenignRoundsInMessages(msgfun) ==
  \* the message function never contains a message for a wrong round
  \A r \in Rounds:
    \A m \in msgfun[r]:
      r = m.round
 \* The initial states of the protocol. Some faults can be in the system already.
 Init ==
    /\ round = [p \in Corr |-> 0]
    /\ \/ /\ ~ClockDrift
          /\ localClock \in [Corr -> 0..Accuracy]
       \/ /\ ClockDrift
          /\ localClock = [p \in Corr |-> 0]
    /\ realTime = 0
    /\ step = [p \in Corr |-> "PROPOSE"]
    /\ decision = [p \in Corr |-> NilDecision]
    /\ lockedValue = [p \in Corr |-> NilValue]
    /\ lockedRound = [p \in Corr |-> NilRound]
    /\ validValue = [p \in Corr |-> NilValue]
    /\ validRound = [p \in Corr |-> NilRound]
    /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
    /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
    /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
    /\ receivedTimelyProposal = EmptyRcvProp
    /\ inspectedProposal = [r \in Rounds |-> EmptyProcSet]
    /\ BenignRoundsInMessages(msgsPropose)
    /\ BenignRoundsInMessages(msgsPrevote)
    /\ BenignRoundsInMessages(msgsPrecommit)
    /\ evidence = EmptyMsgSet
    /\ action' = "Init"
    /\ beginConsensus = Min({localClock[p] : p \in Corr})
    /\ endConsensus = [p \in Corr |-> NilTimestamp]
    /\ lastBeginConsensus = Max({localClock[p] : p \in Corr})
    /\ proposalTime = [r \in Rounds |-> NilTimestamp]
    /\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp]
 (************************ MESSAGE PASSING ********************************)
 BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
  LET newMsg ==
    AsMsg([type |-> "PROPOSAL", src |-> pSrc, round |-> pRound,
           proposal |-> pProposal, validRound |-> pValidRound])
  IN
  msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
 BroadcastPrevote(pSrc, pRound, pId) ==
  LET newMsg == AsMsg([type |-> "PREVOTE",
                       src |-> pSrc, round |-> pRound, id |-> pId])
  IN
  msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
 BroadcastPrecommit(pSrc, pRound, pId) ==
  LET newMsg == AsMsg([type |-> "PRECOMMIT",
                       src |-> pSrc, round |-> pRound, id |-> pId])
  IN
  msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
 (***************************** TIME **************************************)
 \* [PBTS-CLOCK-PRECISION.0]
 SynchronizedLocalClocks ==
    \A p \in Corr : \A q \in Corr : 
        p /= q => 
            \/ /\ localClock[p] >= localClock[q]
               /\ localClock[p] - localClock[q] < Precision 
            \/ /\ localClock[p] < localClock[q]
               /\ localClock[q] - localClock[p] < Precision
 \* [PBTS-PROPOSE.0]
 Proposal(v, t) ==
    <<v, t>>
 \* [PBTS-DECISION-ROUND.0]
 Decision(v, t, r) ==
    <<v, t, r>>
 (**************** MESSAGE PROCESSING TRANSITIONS *************************)
 \* lines 12-13
 StartRound(p, r) ==
   /\ step[p] /= "DECIDED" \* a decided process does not participate in consensus
   /\ round' = [round EXCEPT ![p] = r]
   /\ step' = [step EXCEPT ![p] = "PROPOSE"] 
 \* lines 14-19, a proposal may be sent later
 InsertProposal(p) == 
  LET r == round[p] IN
  /\ p = Proposer[r]
  /\ step[p] = "PROPOSE"
    \* if the proposer is sending a proposal, then there are no other proposals
    \* by the correct processes for the same round
  /\ \A m \in msgsPropose[r]: m.src /= p
  /\ \E v \in ValidValues: 
      LET proposal == IF validValue[p] /= NilValue 
                      THEN Proposal(validValue[p], localClock[p])  
                      ELSE Proposal(v, localClock[p]) IN
      /\ BroadcastProposal(p, round[p], proposal, validRound[p])
      /\ proposalTime' = [proposalTime EXCEPT ![r] = realTime]
  /\ UNCHANGED <<evidence, round, decision, lockedValue, lockedRound,
                validValue, step, validRound, msgsPrevote, msgsPrecommit,
                localClock, realTime, receivedTimelyProposal, inspectedProposal,
                beginConsensus, endConsensus, lastBeginConsensus, proposalReceivedTime>>
  /\ action' = "InsertProposal"
 \* a new action used to filter messages that are not on time
 \* [PBTS-RECEPTION-STEP.0]
 ReceiveProposal(p) ==
  \E v \in Values, t \in Timestamps:
    /\ LET r == round[p] IN
       LET msg ==
        AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
               round |-> round[p], proposal |-> Proposal(v, t), validRound |-> NilRound]) IN
      /\ msg \in msgsPropose[round[p]] 
      /\ p \notin inspectedProposal[r]
      /\ <<p, msg>> \notin receivedTimelyProposal
      /\ inspectedProposal' = [inspectedProposal EXCEPT ![r] = @ \union {p}]
      /\ \/ /\ localClock[p] - Precision < t 
            /\ t < localClock[p] + Precision + Delay
            /\ receivedTimelyProposal' = receivedTimelyProposal \union {<<p, msg>>}
            /\ \/ /\ proposalReceivedTime[r] = NilTimestamp
                  /\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
               \/ /\ proposalReceivedTime[r] /= NilTimestamp
                  /\ UNCHANGED proposalReceivedTime
         \/ /\ \/ localClock[p] - Precision >= t
               \/ t >= localClock[p] + Precision + Delay
            /\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
      /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
          validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
          localClock, realTime, beginConsensus, endConsensus, lastBeginConsensus, proposalTime>>
      /\ action' = "ReceiveProposal"
 \* lines 22-27
 UponProposalInPropose(p) ==
  \E v \in Values, t \in Timestamps:
    /\ step[p] = "PROPOSE" (* line 22 *)
    /\ LET msg ==
        AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
               round |-> round[p], proposal |-> Proposal(v, t), validRound |-> NilRound]) IN
      /\ <<p, msg>> \in receivedTimelyProposal \* updated line 22
      /\ evidence' = {msg} \union evidence
    /\ LET mid == (* line 23 *)
         IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
         THEN Id(Proposal(v, t))
         ELSE NilProposal
       IN
       BroadcastPrevote(p, round[p], mid) \* lines 24-26
    /\ step' = [step EXCEPT ![p] = "PREVOTE"]
    /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
                   validValue, validRound, msgsPropose, msgsPrecommit,
                   localClock, realTime, receivedTimelyProposal, inspectedProposal,
                   beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
    /\ action' = "UponProposalInPropose"
 \* lines 28-33        
 \* [PBTS-ALG-OLD-PREVOTE.0]
 UponProposalInProposeAndPrevote(p) ==
  \E v \in Values, t1 \in Timestamps, t2 \in Timestamps, vr \in Rounds:
    /\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part
    /\ LET msg ==
         AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
                round |-> round[p], proposal |-> Proposal(v, t1), validRound |-> vr])
       IN
       /\ <<p, msg>> \in receivedTimelyProposal \* updated line 28
       /\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(Proposal(v, t2)) } IN
          /\ Cardinality(PV) >= THRESHOLD2 \* line 28
          /\ evidence' = PV \union {msg} \union evidence
    /\ LET mid == (* line 29 *)
         IF IsValid(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
         THEN Id(Proposal(v, t1)) 
         ELSE NilProposal 
       IN
       BroadcastPrevote(p, round[p], mid) \* lines 24-26
    /\ step' = [step EXCEPT ![p] = "PREVOTE"]
    /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
                   validValue, validRound, msgsPropose, msgsPrecommit,
                   localClock, realTime, receivedTimelyProposal, inspectedProposal,
                   beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
    /\ action' = "UponProposalInProposeAndPrevote"
 \* lines 34-35 + lines 61-64 (onTimeoutPrevote)
 UponQuorumOfPrevotesAny(p) ==
  /\ step[p] = "PREVOTE" \* line 34 and 61
  /\ \E MyEvidence \in SUBSET msgsPrevote[round[p]]:
      \* find the unique voters in the evidence
      LET Voters == { m.src: m \in MyEvidence } IN
      \* compare the number of the unique voters against the threshold
      /\ Cardinality(Voters) >= THRESHOLD2 \* line 34
      /\ evidence' = MyEvidence \union evidence
      /\ BroadcastPrecommit(p, round[p], NilProposal)
      /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
      /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
                    validValue, validRound, msgsPropose, msgsPrevote,
                    localClock, realTime, receivedTimelyProposal, inspectedProposal,
                    beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
      /\ action' = "UponQuorumOfPrevotesAny"
 \* lines 36-46
 \* [PBTS-ALG-NEW-PREVOTE.0]
 UponProposalInPrevoteOrCommitAndPrevote(p) ==
  \E v \in ValidValues, t \in Timestamps, vr \in RoundsOrNil:
    /\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
    /\ LET msg ==
         AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
                round |-> round[p], proposal |-> Proposal(v, t), validRound |-> vr]) IN
        /\ <<p, msg>> \in receivedTimelyProposal \* updated line 36
        /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(Proposal(v, t)) } IN
          /\ Cardinality(PV) >= THRESHOLD2 \* line 36
          /\ evidence' = PV \union {msg} \union evidence
    /\  IF step[p] = "PREVOTE"
        THEN \* lines 38-41:
          /\ lockedValue' = [lockedValue EXCEPT ![p] = v]
          /\ lockedRound' = [lockedRound EXCEPT ![p] = round[p]]
          /\ BroadcastPrecommit(p, round[p], Id(Proposal(v, t)))
          /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
        ELSE
          UNCHANGED <<lockedValue, lockedRound, msgsPrecommit, step>>
      \* lines 42-43
    /\ validValue' = [validValue EXCEPT ![p] = v]
    /\ validRound' = [validRound EXCEPT ![p] = round[p]]
    /\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote,
                  localClock, realTime, receivedTimelyProposal, inspectedProposal,
                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
    /\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
 \* lines 47-48 + 65-67 (onTimeoutPrecommit)
 UponQuorumOfPrecommitsAny(p) ==
  /\ \E MyEvidence \in SUBSET msgsPrecommit[round[p]]:
      \* find the unique committers in the evidence
      LET Committers == { m.src: m \in MyEvidence } IN
      \* compare the number of the unique committers against the threshold
      /\ Cardinality(Committers) >= THRESHOLD2 \* line 47
      /\ evidence' = MyEvidence \union evidence
      /\ round[p] + 1 \in Rounds
      /\ StartRound(p, round[p] + 1)   
      /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
                    validRound, msgsPropose, msgsPrevote, msgsPrecommit,
                    localClock, realTime, receivedTimelyProposal, inspectedProposal,
                    beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
      /\ action' = "UponQuorumOfPrecommitsAny"
 \* lines 49-54        
 \* [PBTS-ALG-DECIDE.0]
 UponProposalInPrecommitNoDecision(p) ==
  /\ decision[p] = NilDecision \* line 49
  /\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, vr \in RoundsOrNil:
    /\ LET msg == AsMsg([type |-> "PROPOSAL", src |-> Proposer[r],
                           round |-> r, proposal |-> Proposal(v, t), validRound |-> vr]) IN
     /\ msg \in msgsPropose[r] \* line 49
     /\ p \in inspectedProposal[r]
     /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(Proposal(v, t)) } IN
       /\ Cardinality(PV) >= THRESHOLD2 \* line 49
       /\ evidence' = PV \union {msg} \union evidence
       /\ decision' = [decision EXCEPT ![p] = Decision(v, t, round[p])] \* update the decision, line 51
    \* The original algorithm does not have 'DECIDED', but it increments the height.
    \* We introduced 'DECIDED' here to prevent the process from changing its decision.
       /\ endConsensus' = [endConsensus EXCEPT ![p] = localClock[p]]
       /\ step' = [step EXCEPT ![p] = "DECIDED"]
       /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
                     validRound, msgsPropose, msgsPrevote, msgsPrecommit,
                     localClock, realTime, receivedTimelyProposal, inspectedProposal,
                     beginConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
       /\ action' = "UponProposalInPrecommitNoDecision"
 \* the actions below are not essential for safety, but added for completeness
 \* lines 20-21 + 57-60
 OnTimeoutPropose(p) ==
  /\ step[p] = "PROPOSE"
  /\ p /= Proposer[round[p]]
  /\ BroadcastPrevote(p, round[p], NilProposal)
  /\ step' = [step EXCEPT ![p] = "PREVOTE"]
  /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
                validRound, decision, evidence, msgsPropose, msgsPrecommit,
                localClock, realTime, receivedTimelyProposal, inspectedProposal,
                beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
  /\ action' = "OnTimeoutPropose"
 \* lines 44-46
 OnQuorumOfNilPrevotes(p) ==
  /\ step[p] = "PREVOTE"
  /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(NilProposal) } IN
    /\ Cardinality(PV) >= THRESHOLD2 \* line 36
    /\ evidence' = PV \union evidence
    /\ BroadcastPrecommit(p, round[p], Id(NilProposal))
    /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
    /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
                  validRound, decision, msgsPropose, msgsPrevote,
                  localClock, realTime, receivedTimelyProposal, inspectedProposal,
                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
    /\ action' = "OnQuorumOfNilPrevotes"
 \* lines 55-56
 OnRoundCatchup(p) ==
  \E r \in {rr \in Rounds: rr > round[p]}:
    LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN
    \E MyEvidence \in SUBSET RoundMsgs:
        LET Faster == { m.src: m \in MyEvidence } IN
        /\ Cardinality(Faster) >= THRESHOLD1
        /\ evidence' = MyEvidence \union evidence
        /\ StartRound(p, r)
        /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
                      validRound, msgsPropose, msgsPrevote, msgsPrecommit,
                      localClock, realTime, receivedTimelyProposal, inspectedProposal,
                      beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
        /\ action' = "OnRoundCatchup"
 (********************* PROTOCOL TRANSITIONS ******************************)
 \* advance the global clock
 AdvanceRealTime == 
    /\ realTime < MaxTimestamp
    /\ realTime' = realTime + 1
    /\ \/ /\ ~ClockDrift
          /\ localClock' = [p \in Corr |-> localClock[p] + 1]  
       \/ /\ ClockDrift
          /\ UNCHANGED localClock
    /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
                  validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
                  localClock, receivedTimelyProposal, inspectedProposal,
                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>> 
    /\ action' = "AdvanceRealTime"
 \* advance the local clock of node p
 AdvanceLocalClock(p) ==
    /\ localClock[p] < MaxTimestamp
    /\ localClock' = [localClock EXCEPT ![p] = @ + 1]
    /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
                  validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
                  realTime, receivedTimelyProposal, inspectedProposal,
                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
    /\ action' = "AdvanceLocalClock"
 \* process timely messages
 MessageProcessing(p) ==
    \* start round
    \/ InsertProposal(p)
    \* reception step
    \/ ReceiveProposal(p)
    \* processing step
    \/ UponProposalInPropose(p)
    \/ UponProposalInProposeAndPrevote(p)
    \/ UponQuorumOfPrevotesAny(p)
    \/ UponProposalInPrevoteOrCommitAndPrevote(p)
    \/ UponQuorumOfPrecommitsAny(p)
    \/ UponProposalInPrecommitNoDecision(p)
    \* the actions below are not essential for safety, but added for completeness
    \/ OnTimeoutPropose(p)
    \/ OnQuorumOfNilPrevotes(p)
    \/ OnRoundCatchup(p)
 (*
 * A system transition. In this specificatiom, the system may eventually deadlock,
 * e.g., when all processes decide. This is expected behavior, as we focus on safety.
 *)
 Next ==
  \/ AdvanceRealTime
  \/ /\ ClockDrift
     /\ \E p \in Corr: AdvanceLocalClock(p)
  \/ /\ SynchronizedLocalClocks
     /\ \E p \in Corr: MessageProcessing(p)
 -----------------------------------------------------------------------------
 (*************************** INVARIANTS *************************************)
 \* [PBTS-INV-AGREEMENT.0]
 AgreementOnValue ==
    \A p, q \in Corr:
        /\ decision[p] /= NilDecision
        /\ decision[q] /= NilDecision
        => \E v \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r1 \in Rounds, r2 \in Rounds : 
            /\ decision[p] = Decision(v, t1, r1)
            /\ decision[q] = Decision(v, t2, r2)
 \* [PBTS-INV-TIME-AGR.0]
 AgreementOnTime ==
    \A p, q \in Corr: 
        \A v1 \in ValidValues, v2 \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r \in Rounds :
            /\ decision[p] = Decision(v1, t1, r)
            /\ decision[q] = Decision(v2, t2, r)
            => t1 = t2
 \* [PBTS-CONSENSUS-TIME-VALID.0]
 ConsensusTimeValid ==
    \A p \in Corr, t \in Timestamps : 
    \* if a process decides on v and t
    (\E v \in ValidValues, r \in Rounds : decision[p] = Decision(v, t, r))
        \* then 
        => /\ beginConsensus - Precision <= t 
           /\ t < endConsensus[p] + Precision + Delay
 \* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]
 ConsensusSafeValidCorrProp ==
    \A v \in ValidValues, t \in Timestamps :
        \* if the proposer in the first round is correct
       (/\ Proposer[0] \in Corr
        \* and there exists a process that decided on v, t 
        /\ \E p \in Corr, r \in Rounds : decision[p] = Decision(v, t, r))
            \* then t is between the minimal and maximal initial local time
            => /\ beginConsensus <= t 
               /\ t <= lastBeginConsensus
 \* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0]
 ConsensusRealTimeValidCorr ==
    \A t \in Timestamps, r \in Rounds :
       (/\ \E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r) 
        /\ proposalTime[r] /= NilTimestamp)
        => /\ proposalTime[r] - Accuracy < t
           /\ t < proposalTime[r] + Accuracy
 \* [PBTS-CONSENSUS-REALTIME-VALID.0]
 ConsensusRealTimeValid ==
    \A t \in Timestamps, r \in Rounds :
       (\E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r)) 
        => /\ proposalReceivedTime[r] - Accuracy - Precision < t
           /\ t < proposalReceivedTime[r] + Accuracy + Precision + Delay
 \* [PBTS-MSG-FAIR.0]
 BoundedDelay ==
    \A r \in Rounds : 
        (/\ proposalTime[r] /= NilTimestamp
         /\ proposalTime[r] + Delay < realTime)
            => inspectedProposal[r] = Corr
 \* [PBTS-CONSENSUS-TIME-LIVE.0]
 ConsensusTimeLive ==
    \A r \in Rounds, p \in Corr : 
       (/\ proposalTime[r] /= NilTimestamp
        /\ proposalTime[r] + Delay < realTime 
        /\ Proposer[r] \in Corr
        /\ round[p] <= r)
            => \E msg \in RoundProposals(r) : <<p, msg>> \in receivedTimelyProposal
 \* a conjunction of all invariants
 Inv ==
    /\ AgreementOnValue 
    /\ AgreementOnTime
    /\ ConsensusTimeValid
    /\ ConsensusSafeValidCorrProp
    /\ ConsensusRealTimeValid
    /\ ConsensusRealTimeValidCorr
    /\ BoundedDelay
 Liveness ==
    ConsensusTimeLive    
 =============================================================================