Merge branch 'master' into marko/bringbackdocs

This is a follow-up to #8352. The check for legacy evidence keys is only based
on the prefix of the key. Hashes, which are unprefixed, could easily have this
form and be misdiagnosed.

Because the conversion for evidence checks the key structure, this should not
cause corruption. The probability that a hash is a syntactically valid evidence
key is negligible.  The tool will report an error rather than storing bad data.
But this does mean that such transaction hashes could cause the migration to
stop and report an error before it is complete.

To ensure we convert all the data, refine the legacy key check to filter these
keys more precisely. Update the test cases to exercise this condition.

* Update upgrading instructions.

.github/workflows/docs.yaml

@@ -0,0 +1,32 @@
+name: Documentation
+# This workflow builds the static documentation site, and publishes the results to GitHub Pages.
+# It runs on every push to the main branch, with changes in the docs and spec directories
+on:
+  workflow_dispatch:  # allow manual updates
+  push:
+    branches:
+      - master
+    paths:
+      - "docs/**"
+      - "spec/**"
+
+jobs:
+  build-and-deploy:
+    runs-on: ubuntu-latest
+    container:
+      image: tendermintdev/docker-website-deployment
+    steps:
+      - name: Checkout 🛎️
+        uses: actions/checkout@v3
+
+      - name: Install and Build 🔧
+        run: |
+          apk add rsync
+          make build-docs
+      - name: Deploy 🚀
+        uses: JamesIves/github-pages-deploy-action@v4.3.0
+        with:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          BRANCH: gh-pages
+          FOLDER: ~/output
+          single-commit: true

UPGRADING.md

@@ -212,22 +212,25 @@ and one function have moved to the Tendermint `crypto` package:
 
 The format of all tendermint on-disk database keys changes in
 0.35. Upgrading nodes must either re-sync all data or run a migration
-script provided in this release. The script located in
-`github.com/tendermint/tendermint/scripts/keymigrate/migrate.go`
-provides the function `Migrate(context.Context, db.DB)` which you can
-operationalize as makes sense for your deployment.
+script provided in this release.
+
+The script located in
+`github.com/tendermint/tendermint/scripts/keymigrate/migrate.go` provides the
+function `Migrate(context.Context, db.DB)` which you can operationalize as
+makes sense for your deployment.
 
 For ease of use the `tendermint` command includes a CLI version of the
 migration script, which you can invoke, as in:
 
 	tendermint key-migrate
 
-This reads the configuration file as normal and allows the
-`--db-backend` and `--db-dir` flags to change database operations as
-needed.
+This reads the configuration file as normal and allows the `--db-backend` and
+`--db-dir` flags to override the database location as needed.
 
-The migration operation is idempotent and can be run more than once,
-if needed.
+The migration operation is intended to be idempotent, and should be safe to
+rerun on the same database multiple times.  As a safety measure, however, we
+recommend that operators test out the migration on a copy of the database
+first, if it is practical to do so, before applying it to the production data.
 
 ### CLI Changes
 

docs/tendermint-core/consensus/proposer-based-timestamps.md

@@ -13,14 +13,15 @@ order: 3
 The PBTS algorithm defines a way for a Tendermint blockchain to create block
 timestamps that are within a reasonable bound of the clocks of the validators on
 the network. This replaces the original BFTTime algorithm for timestamp
-assignment that relied on the timestamps included in precommit messages.
+assignment that computed a timestamp using the timestamps included in precommit
+messages.
 
 ## Algorithm Parameters
 
 The functionality of the PBTS algorithm is governed by two parameters within
 Tendermint. These two parameters are [consensus
 parameters](https://github.com/tendermint/tendermint/blob/master/spec/abci/apps.md#L291),
-meaning they are configured by the ABCI application and are expected to be the
+meaning they are configured by the ABCI application and are therefore the same
 same across all nodes on the network.
 
 ### `Precision`
@@ -51,7 +52,7 @@ useful for the protocols and applications built on top of Tendermint.
 The following protocols and application features require a reliable source of time:
 
 * Tendermint Light Clients [rely on correspondence between their known time](https://github.com/tendermint/tendermint/blob/master/spec/light-client/verification/README.md#definitions-1) and the block time for block verification.
-* Tendermint Evidence validity is determined [either in terms of heights or in terms of time](https://github.com/tendermint/tendermint/blob/master/spec/consensus/evidence.md#verification).
+* Tendermint Evidence expiration is determined [either in terms of heights or in terms of time](https://github.com/tendermint/tendermint/blob/master/spec/consensus/evidence.md#verification).
 * Unbonding of staked assets in the Cosmos Hub [occurs after a period of 21
  days](https://github.com/cosmos/governance/blob/master/params-change/Staking.md#unbondingtime).
 * IBC packets can use either a [timestamp or a height to timeout packet

go.mod

@@ -38,7 +38,7 @@ require (
 )
 
 require (
-	github.com/creachadair/atomicfile v0.2.5
+	github.com/creachadair/atomicfile v0.2.6
 	github.com/creachadair/taskgroup v0.3.2
 	github.com/golangci/golangci-lint v1.45.2
 	github.com/google/go-cmp v0.5.8

go.sum

@@ -227,8 +227,8 @@ github.com/cpuguy83/go-md2man v1.0.10/go.mod h1:SmD6nW6nTyfqj6ABTjUi3V3JVMnlJmwc
 github.com/cpuguy83/go-md2man/v2 v2.0.0-20190314233015-f79a8a8ca69d/go.mod h1:maD7wRr/U5Z6m/iR4s+kqSMx2CaBsrgA7czyZG/E6dU=
 github.com/cpuguy83/go-md2man/v2 v2.0.0/go.mod h1:maD7wRr/U5Z6m/iR4s+kqSMx2CaBsrgA7czyZG/E6dU=
 github.com/cpuguy83/go-md2man/v2 v2.0.1/go.mod h1:tgQtvFlXSQOSOSIRvRPT7W67SCa46tRHOmNcaadrF8o=
-github.com/creachadair/atomicfile v0.2.5 h1:wkOlpsjyJOvJ3Hd8juHKdirJnCSIPacvtY21/3nYjAo=
-github.com/creachadair/atomicfile v0.2.5/go.mod h1:BRq8Une6ckFneYXZQ+kO7p1ZZP3I2fzVzf28JxrIkBc=
+github.com/creachadair/atomicfile v0.2.6 h1:FgYxYvGcqREApTY8Nxg8msM6P/KVKK3ob5h9FaRUTNg=
+github.com/creachadair/atomicfile v0.2.6/go.mod h1:BRq8Une6ckFneYXZQ+kO7p1ZZP3I2fzVzf28JxrIkBc=
 github.com/creachadair/taskgroup v0.3.2 h1:zlfutDS+5XG40AOxcHDSThxKzns8Tnr9jnr6VqkYlkM=
 github.com/creachadair/taskgroup v0.3.2/go.mod h1:wieWwecHVzsidg2CsUnFinW1faVN4+kq+TDlRJQ0Wbk=
 github.com/creachadair/tomledit v0.0.19 h1:zbpfUtYFYFdpRjwJY9HJlto1iZ4M5YwYB6qqc37F6UM=

scripts/keymigrate/migrate.go

@@ -86,27 +86,30 @@ const (
 var prefixes = []struct {
 	prefix []byte
 	ktype  keyType
+	check  func(keyID) bool
 }{
-	{[]byte("consensusParamsKey:"), consensusParamsKey},
-	{[]byte("abciResponsesKey:"), abciResponsesKey},
-	{[]byte("validatorsKey:"), validatorsKey},
-	{[]byte("stateKey"), stateStoreKey},
-	{[]byte("H:"), blockMetaKey},
-	{[]byte("P:"), blockPartKey},
-	{[]byte("C:"), commitKey},
-	{[]byte("SC:"), seenCommitKey},
-	{[]byte("BH:"), blockHashKey},
-	{[]byte("size"), lightSizeKey},
-	{[]byte("lb/"), lightBlockKey},
-	{[]byte("\x00"), evidenceCommittedKey},
-	{[]byte("\x01"), evidencePendingKey},
+	{[]byte("consensusParamsKey:"), consensusParamsKey, nil},
+	{[]byte("abciResponsesKey:"), abciResponsesKey, nil},
+	{[]byte("validatorsKey:"), validatorsKey, nil},
+	{[]byte("stateKey"), stateStoreKey, nil},
+	{[]byte("H:"), blockMetaKey, nil},
+	{[]byte("P:"), blockPartKey, nil},
+	{[]byte("C:"), commitKey, nil},
+	{[]byte("SC:"), seenCommitKey, nil},
+	{[]byte("BH:"), blockHashKey, nil},
+	{[]byte("size"), lightSizeKey, nil},
+	{[]byte("lb/"), lightBlockKey, nil},
+	{[]byte("\x00"), evidenceCommittedKey, checkEvidenceKey},
+	{[]byte("\x01"), evidencePendingKey, checkEvidenceKey},
 }
 
 // checkKeyType classifies a candidate key based on its structure.
 func checkKeyType(key keyID) keyType {
 	for _, p := range prefixes {
 		if bytes.HasPrefix(key, p.prefix) {
-			return p.ktype
+			if p.check == nil || p.check(key) {
+				return p.ktype
+			}
 		}
 	}
 
@@ -342,6 +345,35 @@ func convertEvidence(key keyID, newPrefix int64) ([]byte, error) {
 	return orderedcode.Append(nil, newPrefix, binary.BigEndian.Uint64(hb), string(evidenceHash))
 }
 
+// checkEvidenceKey reports whether a candidate key with one of the legacy
+// evidence prefixes has the correct structure for a legacy evidence key.
+//
+// This check is needed because transaction hashes are stored without a prefix,
+// so checking the one-byte prefix alone is not enough to distinguish them.
+// Legacy evidence keys are suffixed with a string of the format:
+//
+//     "%0.16X/%X"
+//
+// where the first element is the height and the second is the hash.  Thus, we
+// check
+func checkEvidenceKey(key keyID) bool {
+	parts := bytes.SplitN(key[1:], []byte("/"), 2)
+	if len(parts) != 2 || len(parts[0]) != 16 || !isHex(parts[0]) || !isHex(parts[1]) {
+		return false
+	}
+	return true
+}
+
+func isHex(data []byte) bool {
+	for _, b := range data {
+		if ('0' <= b && b <= '9') || ('a' <= b && b <= 'f') || ('A' <= b && b <= 'F') {
+			continue
+		}
+		return false
+	}
+	return len(data) != 0
+}
+
 func replaceKey(db dbm.DB, key keyID, gooseFn migrateFunc) error {
 	exists, err := db.Has(key)
 	if err != nil {

scripts/keymigrate/migrate_test.go

@@ -1,11 +1,11 @@
 package keymigrate
 
 import (
-	"bytes"
 	"context"
 	"errors"
 	"fmt"
 	"math"
+	"strings"
 	"testing"
 
 	"github.com/google/orderedcode"
@@ -21,6 +21,7 @@ func makeKey(t *testing.T, elems ...interface{}) []byte {
 }
 
 func getLegacyPrefixKeys(val int) map[string][]byte {
+	vstr := fmt.Sprintf("%02x", byte(val))
 	return map[string][]byte{
 		"Height":            []byte(fmt.Sprintf("H:%d", val)),
 		"BlockPart":         []byte(fmt.Sprintf("P:%d:%d", val, val)),
@@ -40,14 +41,19 @@ func getLegacyPrefixKeys(val int) map[string][]byte {
 		"UserKey1":          []byte(fmt.Sprintf("foo/bar/baz/%d/%d", val, val)),
 		"TxHeight":          []byte(fmt.Sprintf("tx.height/%s/%d/%d", fmt.Sprint(val), val, val)),
 		"TxHash": append(
-			bytes.Repeat([]byte{fmt.Sprint(val)[0]}, 16),
-			bytes.Repeat([]byte{fmt.Sprint(val)[len([]byte(fmt.Sprint(val)))-1]}, 16)...,
+			[]byte(strings.Repeat(vstr[:1], 16)),
+			[]byte(strings.Repeat(vstr[1:], 16))...,
 		),
+
+		// Transaction hashes that could be mistaken for evidence keys.
+		"TxHashMimic0": append([]byte{0}, []byte(strings.Repeat(vstr, 16)[:31])...),
+		"TxHashMimic1": append([]byte{1}, []byte(strings.Repeat(vstr, 16)[:31])...),
 	}
 }
 
 func getNewPrefixKeys(t *testing.T, val int) map[string][]byte {
 	t.Helper()
+	vstr := fmt.Sprintf("%02x", byte(val))
 	return map[string][]byte{
 		"Height":            makeKey(t, int64(0), int64(val)),
 		"BlockPart":         makeKey(t, int64(1), int64(val), int64(val)),
@@ -66,7 +72,9 @@ func getNewPrefixKeys(t *testing.T, val int) map[string][]byte {
 		"UserKey0":          makeKey(t, "foo", "bar", int64(val), int64(val)),
 		"UserKey1":          makeKey(t, "foo", "bar/baz", int64(val), int64(val)),
 		"TxHeight":          makeKey(t, "tx.height", fmt.Sprint(val), int64(val), int64(val+2), int64(val+val)),
-		"TxHash":            makeKey(t, "tx.hash", string(bytes.Repeat([]byte{[]byte(fmt.Sprint(val))[0]}, 32))),
+		"TxHash":            makeKey(t, "tx.hash", strings.Repeat(vstr, 16)),
+		"TxHashMimic0":      makeKey(t, "tx.hash", "\x00"+strings.Repeat(vstr, 16)[:31]),
+		"TxHashMimic1":      makeKey(t, "tx.hash", "\x01"+strings.Repeat(vstr, 16)[:31]),
 	}
 }
 

spec/consensus/proposer-based-timestamp/tla/Apalache.tla

@@ -0,0 +1,109 @@
+--------------------------- MODULE Apalache -----------------------------------
+(*
+ * This is a standard module for use with the Apalache model checker.
+ * The meaning of the operators is explained in the comments.
+ * Many of the operators serve as additional annotations of their arguments.
+ * As we like to preserve compatibility with TLC and TLAPS, we define the
+ * operator bodies by erasure. The actual interpretation of the operators is
+ * encoded inside Apalache. For the moment, these operators are mirrored in
+ * the class at.forsyte.apalache.tla.lir.oper.ApalacheOper.
+ *                                                                          
+ * Igor Konnov, Jure Kukovec, Informal Systems 2020-2021                    
+ *)
+
+(**
+ * An assignment of an expression e to a state variable x. Typically, one
+ * uses the non-primed version of x in the initializing predicate Init and
+ * the primed version of x (that is, x') in the transition predicate Next.
+ * Although TLA+ does not have a concept of a variable assignment, we find
+ * this concept extremely useful for symbolic model checking. In pure TLA+,
+ * one would simply write x = e, or x \in {e}.
+ *
+ * Apalache automatically converts some expressions of the form
+ * x = e or x \in {e} into assignments. However, if you like to annotate
+ * assignments by hand, you can use this operator.
+ *
+ * For a further discussion on that matter, see:
+ * https://github.com/informalsystems/apalache/blob/ik/idiomatic-tla/docs/idiomatic/assignments.md
+ *)
+x := e == x = e
+
+(**
+ * A generator of a data structure. Given a positive integer `bound`, and
+ * assuming that the type of the operator application is known, we
+ * recursively generate a TLA+ data structure as a tree, whose width is
+ * bound by the number `bound`.
+ *
+ * The body of this operator is redefined by Apalache.
+ *)
+Gen(size) == {}
+
+(**
+ * Convert a set of pairs S to a function F. Note that if S contains at least
+ * two pairs <<x, y>> and <<u, v>> such that x = u and y /= v,
+ * then F is not uniquely defined. We use CHOOSE to resolve this ambiguity.
+ * Apalache implements a more efficient encoding of this operator
+ * than the default one.
+ *
+ * @type: Set(<<a, b>>) => (a -> b);
+ *)
+SetAsFun(S) ==
+    LET Dom == { x: <<x, y>> \in S }
+        Rng == { y: <<x, y>> \in S }
+    IN
+    [ x \in Dom |-> CHOOSE y \in Rng: <<x, y>> \in S ]
+
+(**
+ * As TLA+ is untyped, one can use function- and sequence-specific operators
+ * interchangeably. However, to maintain correctness w.r.t. our type-system,
+ * an explicit cast is needed when using functions as sequences.
+ *)
+LOCAL INSTANCE Sequences
+FunAsSeq(fn, maxSeqLen) == SubSeq(fn, 1, maxSeqLen)
+
+(**
+ * Annotating an expression \E x \in S: P as Skolemizable. That is, it can
+ * be replaced with an expression c \in S /\ P(c) for a fresh constant c.
+ * Not every exisential can be replaced with a constant, this should be done
+ * with care. Apalache detects Skolemizable expressions by static analysis.
+ *)
+Skolem(e) == e
+
+(**
+ * A hint to the model checker to expand a set S, instead of dealing
+ * with it symbolically. Apalache finds out which sets have to be expanded
+ * by static analysis.
+ *)
+Expand(S) == S
+
+(**
+ * A hint to the model checker to replace its argument Cardinality(S) >= k
+ * with a series of existential quantifiers for a constant k.
+ * Similar to Skolem, this has to be done carefully. Apalache automatically
+ * places this hint by static analysis.
+ *)
+ConstCardinality(cardExpr) == cardExpr
+
+(**
+ * The folding operator, used to implement computation over a set.
+ * Apalache implements a more efficient encoding than the one below.
+ * (from the community modules).
+ *)
+RECURSIVE FoldSet(_,_,_)
+FoldSet( Op(_,_), v, S ) == IF S = {}
+                            THEN v
+                            ELSE LET w == CHOOSE x \in S: TRUE
+                                  IN LET T == S \ {w}
+                                      IN FoldSet( Op, Op(v,w), T )
+
+(**
+ * The folding operator, used to implement computation over a sequence.
+ * Apalache implements a more efficient encoding than the one below.
+ * (from the community modules).
+ *)
+RECURSIVE FoldSeq(_,_,_)
+FoldSeq( Op(_,_), v, seq ) == IF seq = <<>>
+                              THEN v
+                              ELSE FoldSeq( Op, Op(v,Head(seq)), Tail(seq) )
+
+===============================================================================

spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla

@@ -1,4 +1,4 @@
------------------------------ MODULE MC_PBT_2C_2F -------------------------------
+----------------------------- MODULE MC_PBT -------------------------------
 CONSTANT 
   \* @type: ROUND -> PROCESS;
   Proposer
@@ -38,17 +38,24 @@ VARIABLES
   evidence, \* the messages that were used by the correct processes to make transitions
   \* @type: ACTION;
   action,       \* we use this variable to see which action was taken
+  \* @type: PROCESS -> Set(PROPMESSAGE);
+  receivedTimelyProposal, \* used to keep track when a process receives a timely VALUE message
   \* @type: <<ROUND,PROCESS>> -> TIME;
-  proposalReceptionTime \* used to keep track when a process receives a message
+  inspectedProposal \* used to keep track when a process tries to receive a message
   
 \* Invariant support
 VARIABLES
-  \* @type: <<ROUND, PROCESS>> -> TIME;
+  \* @type: ROUND -> TIME;
   beginRound, \* the minimum of the local clocks at the time any process entered a new round
   \* @type: PROCESS -> TIME;
   endConsensus, \* the local time when a decision is made
   \* @type: ROUND -> TIME;
-  lastBeginRound \* the maximum of the local clocks in each round
+  lastBeginRound, \* the maximum of the local clocks in each round
+  \* @type: ROUND -> TIME;
+  proposalTime, \* the real time when a proposer proposes in a round
+  \* @type: ROUND -> TIME;
+  proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
+
 
 INSTANCE TendermintPBT_002_draft WITH
   Corr <- {"c1", "c2"},
@@ -57,16 +64,14 @@ INSTANCE TendermintPBT_002_draft WITH
   T <- 1,
   ValidValues <- { "v0", "v1" },
   InvalidValues <- {"v2"},
-  MaxRound <- 3,
-  MaxTimestamp <- 7,
+  MaxRound <- 5,
+  MaxTimestamp <- 10,
   MinTimestamp <- 2,
   Delay <- 2,        
-  Precision <- 2,
-  PreloadAllFaultyMsgs <- TRUE,
-  N_GEN <- 5
+  Precision <- 2
 
 \* run Apalache with --cinit=CInit
 CInit == \* the proposer is arbitrary -- works for safety
-  ArbitraryProposer
+  Proposer \in [Rounds -> AllProcs]
 
 =============================================================================    

spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla

@@ -1,72 +0,0 @@
------------------------------ MODULE MC_PBT_3C_1F -------------------------------
-CONSTANT 
-  \* @type: ROUND -> PROCESS;
-  Proposer
-
-VARIABLES
-  \* @type: PROCESS -> ROUND;
-  round,    \* a process round number
-  \* @type: PROCESS -> STEP;
-  step,     \* a process step
-  \* @type: PROCESS -> DECISION;
-  decision, \* process decision
-  \* @type: PROCESS -> VALUE;
-  lockedValue,  \* a locked value
-  \* @type: PROCESS -> ROUND;
-  lockedRound,  \* a locked round
-  \* @type: PROCESS -> PROPOSAL;
-  validValue,   \* a valid value
-  \* @type: PROCESS -> ROUND;
-  validRound    \* a valid round
-
-\* time-related variables
-VARIABLES  
-  \* @type: PROCESS -> TIME;
-  localClock, \* a process local clock: Corr -> Ticks
-  \* @type: TIME;
-  realTime   \* a reference Newtonian real time
-
-\* book-keeping variables
-VARIABLES
-  \* @type: ROUND -> Set(PROPMESSAGE);
-  msgsPropose,   \* PROPOSE messages broadcast in the system, Rounds -> Messages
-  \* @type: ROUND -> Set(PREMESSAGE);
-  msgsPrevote,   \* PREVOTE messages broadcast in the system, Rounds -> Messages
-  \* @type: ROUND -> Set(PREMESSAGE);
-  msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
-  \* @type: Set(MESSAGE);
-  evidence, \* the messages that were used by the correct processes to make transitions
-  \* @type: ACTION;
-  action,       \* we use this variable to see which action was taken
-  \* @type: <<ROUND,PROCESS>> -> TIME;
-  proposalReceptionTime \* used to keep track when a process receives a message
-  
-\* Invariant support
-VARIABLES
-  \* @type: <<ROUND, PROCESS>> -> TIME;
-  beginRound, \* the minimum of the local clocks at the time any process entered a new round
-  \* @type: PROCESS -> TIME;
-  endConsensus, \* the local time when a decision is made
-  \* @type: ROUND -> TIME;
-  lastBeginRound \* the maximum of the local clocks in each round
-
-INSTANCE TendermintPBT_002_draft WITH
-  Corr <- {"c1", "c2", "c3"},
-  Faulty <- {"f4"},
-  N <- 4,
-  T <- 1,
-  ValidValues <- { "v0", "v1" },
-  InvalidValues <- {"v2"},
-  MaxRound <- 3,
-  MaxTimestamp <- 7,
-  MinTimestamp <- 2,
-  Delay <- 2,        
-  Precision <- 2,
-  PreloadAllFaultyMsgs <- TRUE,
-  N_GEN <- 5
-
-\* run Apalache with --cinit=CInit
-CInit == \* the proposer is arbitrary -- works for safety
-  ArbitraryProposer
-
-=============================================================================    

spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla

@@ -518,18 +518,17 @@ AgreementOnValue ==
     \A p, q \in Corr:
         /\ decision[p] /= NilDecision
         /\ decision[q] /= NilDecision
-        => \E v \in ValidValues, t \in Timestamps, r1 \in Rounds, r2 \in Rounds :
-            /\ decision[p] = Decision(v, t, r1)
-            /\ decision[q] = Decision(v, t, r2)
+        => \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-VALID.0]
-ConsensusValidValue ==
-    \A p \in Corr:
-        \* decision[p] = Decision(v, t, r)
-        LET dec == decision[p] IN dec /= NilDecision => IsValid(dec[1])
-
-\* [PBTS-INV-MONOTONICITY.0]
-\* TODO: we would need to compare timestamps of blocks from different height
+\* [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 ==

spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla

@@ -12,7 +12,7 @@
  Jure Kukovec, Informal Systems, 2022.
  *)
 
-EXTENDS Integers, FiniteSets, Apalache, Sequences, typedefs
+EXTENDS Integers, FiniteSets, Apalache, typedefs
 
 (********************* PROTOCOL PARAMETERS **********************************)
 \* General protocol parameters
@@ -47,13 +47,6 @@ CONSTANTS
 
 ASSUME(N = Cardinality(Corr \union Faulty))
 
-\* Modeling parameter
-CONSTANTS
-  \* @type: Bool;
-  PreloadAllFaultyMsgs,
-  \* @type: Int;
-  N_GEN
-
 (*************************** DEFINITIONS ************************************)
 \* @type: Set(PROCESS);
 AllProcs == Corr \union Faulty      \* the set of all processes
@@ -82,14 +75,6 @@ Decisions == Proposals \X Rounds
 \* @type: DECISION;
 NilDecision == <<NilProposal, NilRound>>
 
-ArbitraryProposer == Proposer \in [Rounds -> AllProcs]
-CorrectProposer == Proposer \in [Rounds -> Corr]
-CyclicalProposer == 
-  LET ProcOrder ==
-    LET App(s,e) == Append(s,e)
-    IN ApaFoldSet(App, <<>>, AllProcs)
-  IN Proposer = [ r \in Rounds |-> ProcOrder[1 + (r % N)] ]
-
 ValidProposals == ValidValues \X (MinTimestamp..MaxTimestamp) \X Rounds
 \* a value hash is modeled as identity
 \* @type: (t) => t;
@@ -123,13 +108,13 @@ THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
 \* @type: (TIME, TIME) => TIME;
 Min2(a,b) == IF a <= b THEN a ELSE b
 \* @type: (Set(TIME)) => TIME;
-Min(S) == ApaFoldSet( Min2, MaxTimestamp, S )
+Min(S) == FoldSet( Min2, MaxTimestamp, S )
 \* Min(S) == CHOOSE x \in S : \A y \in S : x <= y
 
 \* @type: (TIME, TIME) => TIME;
 Max2(a,b) == IF a >= b THEN a ELSE b
 \* @type: (Set(TIME)) => TIME;
-Max(S) == ApaFoldSet( Max2, NilTimestamp, S )
+Max(S) == FoldSet( Max2, NilTimestamp, S )
 \* Max(S) == CHOOSE x \in S : \A y \in S : y <= x
 
 \* @type: (Set(MESSAGE)) => Int;
@@ -137,7 +122,7 @@ Card(S) ==
   LET 
     \* @type: (Int, MESSAGE) => Int;
     PlusOne(i, m) == i + 1
-  IN ApaFoldSet( PlusOne, 0, S )
+  IN FoldSet( PlusOne, 0, S )
 
 (********************* PROTOCOL STATE VARIABLES ******************************)
 VARIABLES
@@ -181,25 +166,33 @@ VARIABLES
   evidence, \* the messages that were used by the correct processes to make transitions
   \* @type: ACTION;
   action,       \* we use this variable to see which action was taken
+  \* @type: PROCESS -> Set(PROPMESSAGE);
+  receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message
   \* @type: <<ROUND,PROCESS>> -> TIME;
-  proposalReceptionTime \* used to keep track when a process receives a message
+  inspectedProposal \* used to keep track when a process tries to receive a message
   
 \* Action is excluded from the tuple, because it always changes
 bookkeepingVars == 
   <<msgsPropose, msgsPrevote, msgsPrecommit, 
-  evidence, (*action,*) proposalReceptionTime>>
+  evidence, (*action,*) receivedTimelyProposal, 
+  inspectedProposal>>
 
 \* Invariant support
 VARIABLES
-  \* @type: <<ROUND, PROCESS>> -> TIME;
+  \* @type: ROUND -> TIME;
   beginRound, \* the minimum of the local clocks at the time any process entered a new round
   \* @type: PROCESS -> TIME;
   endConsensus, \* the local time when a decision is made
   \* @type: ROUND -> TIME;
-  lastBeginRound \* the maximum of the local clocks in each round
+  lastBeginRound, \* the maximum of the local clocks in each round
+  \* @type: ROUND -> TIME;
+  proposalTime, \* the real time when a proposer proposes in a round
+  \* @type: ROUND -> TIME;
+  proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
 
 invariantVars == 
-  <<beginRound, endConsensus, lastBeginRound>>
+  <<beginRound, endConsensus, lastBeginRound,
+  proposalTime, proposalReceivedTime>>
 
 (* to see a type invariant, check TendermintAccInv3 *)  
 
@@ -287,39 +280,6 @@ BenignRoundsInMessages(msgfun) ==
     \A m \in msgfun[r]:
       r = m.round
 
-\* @type: (ROUND -> Set(MESSAGE), Set(MESSAGE)) => Bool;
-BenignAndSubset(msgfun, set) == 
-  /\ \A r \in Rounds: 
-    \* The generated values belong to SUBSET set
-    /\ msgfun[r] \subseteq set
-    \* the message function never contains a message for a wrong round
-    /\ \A m \in msgfun[r]: r = m.round
-
-InitGen == 
-  /\ msgsPropose \in [Rounds -> Gen(N_GEN)]
-  /\ msgsPrevote \in [Rounds -> Gen(N_GEN)]
-  /\ msgsPrecommit \in [Rounds -> Gen(N_GEN)]
-  /\ BenignAndSubset(msgsPropose, AllFaultyProposals)
-  /\ BenignAndSubset(msgsPrevote, AllFaultyPrevotes)
-  /\ BenignAndSubset(msgsPrecommit, AllFaultyPrecommits)
-
-InitPreloadAllMsgs ==
-  /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
-  /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
-  /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
-  /\ BenignRoundsInMessages(msgsPropose)
-  /\ BenignRoundsInMessages(msgsPrevote)
-  /\ BenignRoundsInMessages(msgsPrecommit)
-
-InitMsgs ==
-  \/ /\ PreloadAllFaultyMsgs
-     \* /\ InitPreloadAllMsgs
-     /\ InitGen
-  \/ /\ ~PreloadAllFaultyMsgs
-     /\ msgsPropose = [r \in Rounds |-> {}]
-     /\ msgsPrevote = [r \in Rounds |-> {}]
-     /\ msgsPrecommit = [r \in Rounds |-> {}]
-
 \* The initial states of the protocol. Some faults can be in the system already.
 Init ==
     /\ round = [p \in Corr |-> 0]
@@ -331,12 +291,18 @@ Init ==
     /\ lockedRound = [p \in Corr |-> NilRound]
     /\ validValue = [p \in Corr |-> NilProposal]
     /\ validRound = [p \in Corr |-> NilRound]
-    /\ InitMsgs
-    /\ proposalReceptionTime = [r \in Rounds, p \in Corr |-> NilTimestamp]
+    /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
+    /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
+    /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
+    /\ receivedTimelyProposal = [p \in Corr |-> {}]
+    /\ inspectedProposal = [r \in Rounds, p \in Corr |-> NilTimestamp]
+    /\ BenignRoundsInMessages(msgsPropose)
+    /\ BenignRoundsInMessages(msgsPrevote)
+    /\ BenignRoundsInMessages(msgsPrecommit)
     /\ evidence = {}
-    /\ action = "Init"
+    /\ action' = "Init"
     /\ beginRound = 
-      [r \in Rounds, c \in Corr |-> 
+      [r \in Rounds |-> 
         IF r = 0
         THEN Min({localClock[p] : p \in Corr})
         ELSE MaxTimestamp
@@ -348,30 +314,8 @@ Init ==
         THEN Max({localClock[p] : p \in Corr})
         ELSE NilTimestamp
       ]
-
-\* Faulty processes send messages
-FaultyBroadcast == 
-  /\ ~PreloadAllFaultyMsgs
-  /\ action' = "FaultyBroadcast"
-  /\ \E r \in Rounds:
-    \/ \E msgs \in SUBSET FaultyProposals(r):
-        /\ msgsPropose' = [msgsPropose EXCEPT ![r] = @ \union msgs]
-        /\ UNCHANGED <<coreVars, temporalVars, invariantVars>>
-        /\ UNCHANGED 
-          <<(*msgsPropose,*) msgsPrevote, msgsPrecommit, 
-          evidence, (*action,*) proposalReceptionTime>>
-    \/ \E msgs \in SUBSET FaultyPrevotes(r):
-        /\ msgsPrevote' = [msgsPrevote EXCEPT ![r] = @ \union msgs]
-        /\ UNCHANGED <<coreVars, temporalVars, invariantVars>>
-        /\ UNCHANGED 
-          <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
-          evidence, (*action,*) proposalReceptionTime>>
-    \/ \E msgs \in SUBSET FaultyPrecommits(r):
-        /\ msgsPrecommit' = [msgsPrecommit EXCEPT ![r] = @ \union msgs]
-        /\ UNCHANGED <<coreVars, temporalVars, invariantVars>>
-        /\ UNCHANGED 
-          <<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
-          evidence, (*action,*) proposalReceptionTime>>
+    /\ proposalTime = [r \in Rounds |-> NilTimestamp]
+    /\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp]
 
 (************************ MESSAGE PASSING ********************************)
 \* @type: (PROCESS, ROUND, PROPOSAL, ROUND) => Bool;
@@ -447,7 +391,7 @@ StartRound(p, r) ==
    /\ round' = [round EXCEPT ![p] = r]
    /\ step' = [step EXCEPT ![p] = "PROPOSE"]
    \* We only need to update (last)beginRound[r] once a process enters round `r`
-   /\ beginRound' = [beginRound EXCEPT ![r,p] = localClock[p]]
+   /\ beginRound' = [beginRound EXCEPT ![r] = Min2(@, localClock[p])]
    /\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])]
 
 \* lines 14-19, a proposal may be sent later
@@ -459,6 +403,7 @@ InsertProposal(p) ==
     \* 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
+  \* /\ localClock[p] > 
   /\ \E v \in ValidValues: 
       LET proposal == 
         IF validValue[p] /= NilProposal 
@@ -466,14 +411,17 @@ InsertProposal(p) ==
         ELSE Proposal(v, localClock[p], r)
       IN               
       /\ BroadcastProposal(p, r, proposal, validRound[p])
+      /\ proposalTime' = [proposalTime EXCEPT ![r] = realTime]
   /\ UNCHANGED <<temporalVars, coreVars>>
   /\ UNCHANGED 
     <<(*msgsPropose,*) msgsPrevote, msgsPrecommit, 
-    evidence, proposalReceptionTime>>
-  /\ UNCHANGED invariantVars
+    evidence, receivedTimelyProposal, inspectedProposal>>
+  /\ UNCHANGED
+    <<beginRound, endConsensus, lastBeginRound,
+    (*proposalTime,*) proposalReceivedTime>>
   /\ action' = "InsertProposal"
   
-\* a new action used to register the proposal and note the reception time.
+\* a new action used to filter messages that are not on time
 \* [PBTS-RECEPTION-STEP.0]
 \* @type: (PROCESS) => Bool;
 ReceiveProposal(p) ==
@@ -491,13 +439,30 @@ ReceiveProposal(p) ==
           ] 
        IN
       /\ msg \in msgsPropose[round[p]] 
-      /\ proposalReceptionTime[r,p] = NilTimestamp
-      /\ proposalReceptionTime' = [proposalReceptionTime EXCEPT ![r,p] = localClock[p]]
+      /\ inspectedProposal[r,p] = NilTimestamp
+      /\ msg \notin receivedTimelyProposal[p]
+      /\ inspectedProposal' = [inspectedProposal EXCEPT ![r,p] = localClock[p]]
+      /\ LET 
+          isTimely == IsTimely(localClock[p], t)
+         IN
+          \/ /\ isTimely
+             /\ receivedTimelyProposal' = [receivedTimelyProposal EXCEPT ![p] = @ \union {msg}]
+             /\ LET
+                  isNilTimestamp == proposalReceivedTime[r] = NilTimestamp
+                IN
+                  \/ /\ isNilTimestamp
+                     /\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
+                  \/ /\ ~isNilTimestamp
+                     /\ UNCHANGED proposalReceivedTime
+          \/ /\ ~isTimely
+             /\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
       /\ UNCHANGED <<temporalVars, coreVars>>
       /\ UNCHANGED
         <<msgsPropose, msgsPrevote, msgsPrecommit, 
-        evidence(*, proposalReceptionTime*)>>
-      /\ UNCHANGED invariantVars
+        evidence(*, receivedTimelyProposal, inspectedProposal*)>>
+      /\ UNCHANGED 
+        <<beginRound, endConsensus, lastBeginRound,
+        proposalTime(*, proposalReceivedTime*)>>
       /\ action' = "ReceiveProposal"
       
 \* lines 22-27
@@ -522,17 +487,10 @@ UponProposalInPropose(p) ==
           validRound |-> NilRound
         ] 
        IN
+      /\ msg \in receivedTimelyProposal[p] \* updated line 22
       /\ evidence' = {msg} \union evidence
     /\ LET mid == (* line 23 *)
-         IF 
-          \* Timeliness is checked against the process time, as was
-          \* recorded in proposalReceptionTime, not as it is now.
-          \* In the implementation, if the proposal is not timely, then we prevote
-          \* nil. In the natural-language specification, nothing happens. 
-          \* This specification maintains consistency with the implementation.
-          /\ IsTimely( proposalReceptionTime[r, p], t) \* updated line 22
-          /\ IsValid(prop) 
-          /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
+         IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
          THEN Id(prop)
          ELSE NilProposal
        IN
@@ -544,7 +502,7 @@ UponProposalInPropose(p) ==
       lockedRound, validValue, validRound>>
     /\ UNCHANGED 
       <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
-      (*evidence,*) proposalReceptionTime>>
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInPropose"
 
 \* lines 28-33        
@@ -589,7 +547,7 @@ UponProposalInProposeAndPrevote(p) ==
       lockedRound, validValue, validRound>>
     /\ UNCHANGED 
       <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
-      (*evidence,*) proposalReceptionTime>>
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInProposeAndPrevote"
                      
 \* lines 34-35 + lines 61-64 (onTimeoutPrevote)
@@ -610,7 +568,7 @@ UponQuorumOfPrevotesAny(p) ==
         lockedRound, validValue, validRound>>
       /\ UNCHANGED 
         <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
-        (*evidence,*) proposalReceptionTime>>
+        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
       /\ action' = "UponQuorumOfPrevotesAny"
                      
 \* lines 36-46
@@ -658,7 +616,7 @@ UponProposalInPrevoteOrCommitAndPrevote(p) ==
       lockedRound, validValue, validRound*)>>
     /\ UNCHANGED 
       <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
-      (*evidence,*) proposalReceptionTime>>
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
 
 \* lines 47-48 + 65-67 (onTimeoutPrecommit)
@@ -674,13 +632,14 @@ UponQuorumOfPrecommitsAny(p) ==
       /\ StartRound(p, round[p] + 1)
       /\ UNCHANGED temporalVars
       /\ UNCHANGED
-        <<(*beginRound,*) endConsensus(*, lastBeginRound*)>>
+        <<(*beginRound,*) endConsensus, (*lastBeginRound,*)
+        proposalTime, proposalReceivedTime>>
       /\ UNCHANGED
         <<(*round, step,*) decision, lockedValue, 
         lockedRound, validValue, validRound>>
       /\ UNCHANGED 
         <<msgsPropose, msgsPrevote, msgsPrecommit,
-        (*evidence,*) proposalReceptionTime>>
+        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
       /\ action' = "UponQuorumOfPrecommitsAny"
                      
 \* lines 49-54        
@@ -705,7 +664,7 @@ UponProposalInPrecommitNoDecision(p) ==
         ] 
        IN 
      /\ msg \in msgsPropose[r] \* line 49
-     /\ proposalReceptionTime[r,p] /= NilTimestamp \* Keep?
+     /\ inspectedProposal[r,p] /= NilTimestamp \* Keep?
      /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(prop) } IN
        /\ Cardinality(PV) >= THRESHOLD2 \* line 49
        /\ evidence' = PV \union {msg} \union evidence
@@ -720,9 +679,10 @@ UponProposalInPrecommitNoDecision(p) ==
          lockedRound, validValue, validRound>>
        /\ UNCHANGED 
          <<msgsPropose, msgsPrevote, msgsPrecommit,
-         (*evidence,*) proposalReceptionTime>>
+         (*evidence,*) receivedTimelyProposal, inspectedProposal>>
        /\ UNCHANGED
-         <<beginRound, (*endConsensus,*) lastBeginRound>>
+         <<beginRound, (*endConsensus,*) lastBeginRound,
+         proposalTime, proposalReceivedTime>>
        /\ action' = "UponProposalInPrecommitNoDecision"
                                                           
 \* the actions below are not essential for safety, but added for completeness
@@ -740,7 +700,7 @@ OnTimeoutPropose(p) ==
     lockedRound, validValue, validRound>>
   /\ UNCHANGED 
     <<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
-    evidence, proposalReceptionTime>>
+    evidence, receivedTimelyProposal, inspectedProposal>>
   /\ action' = "OnTimeoutPropose"
 
 \* lines 44-46
@@ -758,30 +718,30 @@ OnQuorumOfNilPrevotes(p) ==
       lockedRound, validValue, validRound>>
     /\ UNCHANGED 
       <<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
-      (*evidence,*) proposalReceptionTime>>
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "OnQuorumOfNilPrevotes"
 
 \* lines 55-56
 \* @type: (PROCESS) => Bool;
 OnRoundCatchup(p) ==
-  \E r \in Rounds: 
-    /\ r > 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 temporalVars
-           /\ UNCHANGED
-             <<(*beginRound,*) endConsensus(*, lastBeginRound*)>>
-           /\ UNCHANGED
-             <<(*round, step,*) decision, lockedValue, 
-             lockedRound, validValue, validRound>>
-           /\ UNCHANGED 
-             <<msgsPropose, msgsPrevote, msgsPrecommit,
-             (*evidence,*) proposalReceptionTime>>
-           /\ action' = "OnRoundCatchup"
+  \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 temporalVars
+        /\ UNCHANGED
+          <<(*beginRound,*) endConsensus, (*lastBeginRound,*)
+          proposalTime, proposalReceivedTime>>
+        /\ UNCHANGED
+          <<(*round, step,*) decision, lockedValue, 
+          lockedRound, validValue, validRound>>
+        /\ UNCHANGED 
+          <<msgsPropose, msgsPrevote, msgsPrecommit,
+          (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+        /\ action' = "OnRoundCatchup"
 
 
 (********************* PROTOCOL TRANSITIONS ******************************)
@@ -832,7 +792,6 @@ MessageProcessing(p) ==
  *)
 Next == 
   \/ AdvanceRealTime
-  \/ FaultyBroadcast
   \/ /\ SynchronizedLocalClocks
      /\ \E p \in Corr: MessageProcessing(p)
 
@@ -851,100 +810,74 @@ AgreementOnValue ==
             /\ decision[p] = Decision(prop, r1)
             /\ decision[q] = Decision(prop, r2)
 
-DisagreementOnValue ==
-  \E p, q \in Corr:
-    \E p1 \in ValidProposals, p2 \in ValidProposals, r1 \in Rounds, r2 \in Rounds:
-    /\ p1 /= p2
-    /\ decision[p] = Decision(p1, r1)
-    /\ decision[q] = Decision(p2, r2) 
-
-\* [PBTS-INV-VALID.0]
-ConsensusValidValue ==
-    \A p \in Corr:
-        \* decision[p] = Decision(Proposal(v,t,pr), r)
-        LET prop == decision[p][1] IN 
-          prop /= NilProposal => prop[1] \in ValidValues
-
-\* [PBTS-INV-MONOTONICITY.0]
-\* TODO: we would need to compare timestamps of blocks from different height
-
-\* [PBTS-INV-TIMELY.0]
+\* [PBTS-CONSENSUS-TIME-VALID.0]
 ConsensusTimeValid ==
     \A p \in Corr: 
     \* if a process decides on v and t
       \E v \in ValidValues, t \in Timestamps, pr \in Rounds, dr \in Rounds : 
-        \* FIXME: do we need to enforce pr <= dr?
         decision[p] = Decision(Proposal(v,t,pr), dr)
-        \* then a process found t timely at its proposal round (pr) 
-        => \E q \in Corr:
-           LET propRecvTime == proposalReceptionTime[pr, q] IN
-           (
-             /\ beginRound[pr, q] <= propRecvTime
-             /\ beginRound[pr+1, q] >= propRecvTime
-             /\ IsTimely(propRecvTime, t)
-           )
+        \* then 
+        \* TODO: consider tighter bound where beginRound[pr] is replaced
+        \* w/ MedianOfRound[pr]
+        => (/\ beginRound[pr] - Precision - Delay <= t 
+            /\ t <= endConsensus[p] + Precision)
 
 \* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]
-\* ConsensusSafeValidCorrProp ==
-\*     \A v \in ValidValues:
-\*       \* and there exists a process that decided on v, t 
-\*       /\ \E p \in Corr, t \in Timestamps, pr \in Rounds, dr \in Rounds : 
-\*         \* if the proposer in the round is correct
-\*         (/\ Proposer[pr] \in Corr
-\*         /\ decision[p] = Decision(Proposal(v,t,pr), dr))
-\*           \* then t is between the minimal and maximal initial local time
-\*           => /\ beginRound[pr, p] <= t 
-\*              /\ t <= lastBeginRound[pr]
-\* 
-
-\* @type: (PROPOSAL, ROUND) => Set(PREMESSAGE);
-POLSet(prop, rnd) == 
-  { msg \in msgsPrevote[rnd]: msg.id = prop}
-\* @type: (Set(PREMESSAGE)) => Bool;
-IsValidPOL(s) == Cardinality(s) >= THRESHOLD2
-
-\* @type: (Set(PREMESSAGE)) => Bool;
-ContainsPrevoteFromCorrect(set) ==
-  \E p \in Corr, msg \in set: msg.src = p
-
-\* [PBS-DERIVED-POL.1]
-DerivedProofOfLocks == 
-  \A r \in Rounds, prop \in ValidProposals:
-    LET t == prop[2] IN
-    LET rStar == prop[3] IN
-    LET PS == POLSet(prop, r) IN
-    ( 
-      /\ IsValidPOL(PS)
-      /\ ContainsPrevoteFromCorrect(PS)
-    ) =>
-      LET PSStar == POLSet(prop, rStar) IN 
-        /\ rStar <= r
-        /\ ContainsPrevoteFromCorrect(PSStar)
-        /\ \E p \in Corr: IsTimely( proposalReceptionTime[rStar, p], t)
-
-
+ConsensusSafeValidCorrProp ==
+    \A v \in ValidValues:
+      \* and there exists a process that decided on v, t 
+      /\ \E p \in Corr, t \in Timestamps, pr \in Rounds, dr \in Rounds : 
+        \* if the proposer in the round is correct
+        (/\ Proposer[pr] \in Corr
+        /\ decision[p] = Decision(Proposal(v,t,pr), dr))
+          \* then t is between the minimal and maximal initial local time
+          => /\ beginRound[pr] <= t 
+             /\ t <= lastBeginRound[pr]
 
 \* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0]
-\* ConsensusRealTimeValidCorr == TODO?
+ConsensusRealTimeValidCorr ==
+  \A r \in Rounds :
+    \E p \in Corr, v \in ValidValues, t \in Timestamps, pr \in Rounds: 
+     (/\ decision[p] = Decision(Proposal(v,t,pr), r) 
+      /\ proposalTime[r] /= NilTimestamp)
+        => (/\ proposalTime[r] - Precision <= t
+            /\ t <= proposalTime[r] + Precision)
+
 \* [PBTS-CONSENSUS-REALTIME-VALID.0]
-\* ConsensusRealTimeValid == TODO?
+ConsensusRealTimeValid ==
+    \A t \in Timestamps, r \in Rounds :
+       (\E p \in Corr, v \in ValidValues, pr \in Rounds : 
+        decision[p] = Decision(Proposal(v,t,pr), r)) 
+        => /\ proposalReceivedTime[r] - Precision < t
+           /\ t < proposalReceivedTime[r] + Precision + Delay
 
 DecideAfterMin == TRUE
   \* if decide => time > min
 
 \* [PBTS-MSG-FAIR.0]
-\* BoundedDelay == TODO?
+BoundedDelay ==
+    \A r \in Rounds : 
+        (/\ proposalTime[r] /= NilTimestamp
+         /\ proposalTime[r] + Delay < realTime)
+            => \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp
 
 \* [PBTS-CONSENSUS-TIME-LIVE.0]
-\* ConsensusTimeLive == TODO?
+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) : msg \in receivedTimelyProposal[p]
 
 \* a conjunction of all invariants
 Inv ==
     /\ AgreementOnValue 
-    /\ ConsensusValidValue
     /\ ConsensusTimeValid
-\*    /\ ConsensusSafeValidCorrProp
-\*    /\ DerivedProofOfLocks
+    /\ ConsensusSafeValidCorrProp
+    \* /\ ConsensusRealTimeValid
+    \* /\ ConsensusRealTimeValidCorr
+    \* /\ BoundedDelay
 
 \* Liveness ==
 \*     ConsensusTimeLive