Generators

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

@@ -1,109 +0,0 @@
---------------------------- 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_2C_2F.tla

@@ -1,4 +1,4 @@
------------------------------ MODULE MC_PBT -------------------------------
+----------------------------- MODULE MC_PBT_2C_2F -------------------------------
 CONSTANT 
   \* @type: ROUND -> PROCESS;
   Proposer
@@ -38,24 +38,17 @@ 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;
-  inspectedProposal \* used to keep track when a process tries to receive a message
+  proposalReceptionTime \* used to keep track when a process receives a message
   
 \* Invariant support
 VARIABLES
-  \* @type: ROUND -> TIME;
+  \* @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
-  \* @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
-
+  lastBeginRound \* the maximum of the local clocks in each round
 
 INSTANCE TendermintPBT_002_draft WITH
   Corr <- {"c1", "c2"},
@@ -64,14 +57,16 @@ INSTANCE TendermintPBT_002_draft WITH
   T <- 1,
   ValidValues <- { "v0", "v1" },
   InvalidValues <- {"v2"},
-  MaxRound <- 5,
-  MaxTimestamp <- 10,
+  MaxRound <- 3,
+  MaxTimestamp <- 7,
   MinTimestamp <- 2,
   Delay <- 2,        
-  Precision <- 2
+  Precision <- 2,
+  PreloadAllFaultyMsgs <- TRUE,
+  N_GEN <- 5
 
 \* run Apalache with --cinit=CInit
 CInit == \* the proposer is arbitrary -- works for safety
-  Proposer \in [Rounds -> AllProcs]
+  ArbitraryProposer
 
 =============================================================================    

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

@@ -0,0 +1,72 @@
+----------------------------- 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,17 +518,18 @@ 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)
+        => \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)
 
-\* [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-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-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, typedefs
+EXTENDS Integers, FiniteSets, Apalache, Sequences, typedefs
 
 (********************* PROTOCOL PARAMETERS **********************************)
 \* General protocol parameters
@@ -47,6 +47,13 @@ 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
@@ -75,6 +82,14 @@ 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;
@@ -108,13 +123,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) == FoldSet( Min2, MaxTimestamp, S )
+Min(S) == ApaFoldSet( 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) == FoldSet( Max2, NilTimestamp, S )
+Max(S) == ApaFoldSet( Max2, NilTimestamp, S )
 \* Max(S) == CHOOSE x \in S : \A y \in S : y <= x
 
 \* @type: (Set(MESSAGE)) => Int;
@@ -122,7 +137,7 @@ Card(S) ==
   LET 
     \* @type: (Int, MESSAGE) => Int;
     PlusOne(i, m) == i + 1
-  IN FoldSet( PlusOne, 0, S )
+  IN ApaFoldSet( PlusOne, 0, S )
 
 (********************* PROTOCOL STATE VARIABLES ******************************)
 VARIABLES
@@ -166,33 +181,25 @@ 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;
-  inspectedProposal \* used to keep track when a process tries to receive a message
+  proposalReceptionTime \* used to keep track when a process receives a message
   
 \* Action is excluded from the tuple, because it always changes
 bookkeepingVars == 
   <<msgsPropose, msgsPrevote, msgsPrecommit, 
-  evidence, (*action,*) receivedTimelyProposal, 
-  inspectedProposal>>
+  evidence, (*action,*) proposalReceptionTime>>
 
 \* Invariant support
 VARIABLES
-  \* @type: ROUND -> TIME;
+  \* @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
-  \* @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
+  lastBeginRound \* the maximum of the local clocks in each round
 
 invariantVars == 
-  <<beginRound, endConsensus, lastBeginRound,
-  proposalTime, proposalReceivedTime>>
+  <<beginRound, endConsensus, lastBeginRound>>
 
 (* to see a type invariant, check TendermintAccInv3 *)  
 
@@ -280,6 +287,39 @@ 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]
@@ -291,18 +331,12 @@ Init ==
     /\ lockedRound = [p \in Corr |-> NilRound]
     /\ validValue = [p \in Corr |-> NilProposal]
     /\ validRound = [p \in Corr |-> NilRound]
-    /\ 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)
+    /\ InitMsgs
+    /\ proposalReceptionTime = [r \in Rounds, p \in Corr |-> NilTimestamp]
     /\ evidence = {}
-    /\ action' = "Init"
+    /\ action = "Init"
     /\ beginRound = 
-      [r \in Rounds |-> 
+      [r \in Rounds, c \in Corr |-> 
         IF r = 0
         THEN Min({localClock[p] : p \in Corr})
         ELSE MaxTimestamp
@@ -314,8 +348,30 @@ Init ==
         THEN Max({localClock[p] : p \in Corr})
         ELSE NilTimestamp
       ]
-    /\ proposalTime = [r \in Rounds |-> NilTimestamp]
-    /\ proposalReceivedTime = [r \in Rounds |-> 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>>
 
 (************************ MESSAGE PASSING ********************************)
 \* @type: (PROCESS, ROUND, PROPOSAL, ROUND) => Bool;
@@ -391,7 +447,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] = Min2(@, localClock[p])]
+   /\ beginRound' = [beginRound EXCEPT ![r,p] = localClock[p]]
    /\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])]
 
 \* lines 14-19, a proposal may be sent later
@@ -403,7 +459,6 @@ 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 
@@ -411,17 +466,14 @@ 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, receivedTimelyProposal, inspectedProposal>>
-  /\ UNCHANGED
-    <<beginRound, endConsensus, lastBeginRound,
-    (*proposalTime,*) proposalReceivedTime>>
+    evidence, proposalReceptionTime>>
+  /\ UNCHANGED invariantVars
   /\ action' = "InsertProposal"
   
-\* a new action used to filter messages that are not on time
+\* a new action used to register the proposal and note the reception time.
 \* [PBTS-RECEPTION-STEP.0]
 \* @type: (PROCESS) => Bool;
 ReceiveProposal(p) ==
@@ -439,30 +491,13 @@ ReceiveProposal(p) ==
           ] 
        IN
       /\ msg \in msgsPropose[round[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>>
+      /\ proposalReceptionTime[r,p] = NilTimestamp
+      /\ proposalReceptionTime' = [proposalReceptionTime EXCEPT ![r,p] = localClock[p]]
       /\ UNCHANGED <<temporalVars, coreVars>>
       /\ UNCHANGED
         <<msgsPropose, msgsPrevote, msgsPrecommit, 
-        evidence(*, receivedTimelyProposal, inspectedProposal*)>>
-      /\ UNCHANGED 
-        <<beginRound, endConsensus, lastBeginRound,
-        proposalTime(*, proposalReceivedTime*)>>
+        evidence(*, proposalReceptionTime*)>>
+      /\ UNCHANGED invariantVars
       /\ action' = "ReceiveProposal"
       
 \* lines 22-27
@@ -487,10 +522,17 @@ UponProposalInPropose(p) ==
           validRound |-> NilRound
         ] 
        IN
-      /\ msg \in receivedTimelyProposal[p] \* updated line 22
       /\ evidence' = {msg} \union evidence
     /\ LET mid == (* line 23 *)
-         IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
+         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)
          THEN Id(prop)
          ELSE NilProposal
        IN
@@ -502,7 +544,7 @@ UponProposalInPropose(p) ==
       lockedRound, validValue, validRound>>
     /\ UNCHANGED 
       <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
-      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+      (*evidence,*) proposalReceptionTime>>
     /\ action' = "UponProposalInPropose"
 
 \* lines 28-33        
@@ -547,7 +589,7 @@ UponProposalInProposeAndPrevote(p) ==
       lockedRound, validValue, validRound>>
     /\ UNCHANGED 
       <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
-      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+      (*evidence,*) proposalReceptionTime>>
     /\ action' = "UponProposalInProposeAndPrevote"
                      
 \* lines 34-35 + lines 61-64 (onTimeoutPrevote)
@@ -568,7 +610,7 @@ UponQuorumOfPrevotesAny(p) ==
         lockedRound, validValue, validRound>>
       /\ UNCHANGED 
         <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
-        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+        (*evidence,*) proposalReceptionTime>>
       /\ action' = "UponQuorumOfPrevotesAny"
                      
 \* lines 36-46
@@ -616,7 +658,7 @@ UponProposalInPrevoteOrCommitAndPrevote(p) ==
       lockedRound, validValue, validRound*)>>
     /\ UNCHANGED 
       <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
-      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+      (*evidence,*) proposalReceptionTime>>
     /\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
 
 \* lines 47-48 + 65-67 (onTimeoutPrecommit)
@@ -632,14 +674,13 @@ UponQuorumOfPrecommitsAny(p) ==
       /\ StartRound(p, round[p] + 1)
       /\ UNCHANGED temporalVars
       /\ UNCHANGED
-        <<(*beginRound,*) endConsensus, (*lastBeginRound,*)
-        proposalTime, proposalReceivedTime>>
+        <<(*beginRound,*) endConsensus(*, lastBeginRound*)>>
       /\ UNCHANGED
         <<(*round, step,*) decision, lockedValue, 
         lockedRound, validValue, validRound>>
       /\ UNCHANGED 
         <<msgsPropose, msgsPrevote, msgsPrecommit,
-        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+        (*evidence,*) proposalReceptionTime>>
       /\ action' = "UponQuorumOfPrecommitsAny"
                      
 \* lines 49-54        
@@ -664,7 +705,7 @@ UponProposalInPrecommitNoDecision(p) ==
         ] 
        IN 
      /\ msg \in msgsPropose[r] \* line 49
-     /\ inspectedProposal[r,p] /= NilTimestamp \* Keep?
+     /\ proposalReceptionTime[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
@@ -679,10 +720,9 @@ UponProposalInPrecommitNoDecision(p) ==
          lockedRound, validValue, validRound>>
        /\ UNCHANGED 
          <<msgsPropose, msgsPrevote, msgsPrecommit,
-         (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+         (*evidence,*) proposalReceptionTime>>
        /\ UNCHANGED
-         <<beginRound, (*endConsensus,*) lastBeginRound,
-         proposalTime, proposalReceivedTime>>
+         <<beginRound, (*endConsensus,*) lastBeginRound>>
        /\ action' = "UponProposalInPrecommitNoDecision"
                                                           
 \* the actions below are not essential for safety, but added for completeness
@@ -700,7 +740,7 @@ OnTimeoutPropose(p) ==
     lockedRound, validValue, validRound>>
   /\ UNCHANGED 
     <<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
-    evidence, receivedTimelyProposal, inspectedProposal>>
+    evidence, proposalReceptionTime>>
   /\ action' = "OnTimeoutPropose"
 
 \* lines 44-46
@@ -718,30 +758,30 @@ OnQuorumOfNilPrevotes(p) ==
       lockedRound, validValue, validRound>>
     /\ UNCHANGED 
       <<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
-      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+      (*evidence,*) proposalReceptionTime>>
     /\ action' = "OnQuorumOfNilPrevotes"
 
 \* lines 55-56
 \* @type: (PROCESS) => Bool;
 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 temporalVars
-        /\ UNCHANGED
-          <<(*beginRound,*) endConsensus, (*lastBeginRound,*)
-          proposalTime, proposalReceivedTime>>
-        /\ UNCHANGED
-          <<(*round, step,*) decision, lockedValue, 
-          lockedRound, validValue, validRound>>
-        /\ UNCHANGED 
-          <<msgsPropose, msgsPrevote, msgsPrecommit,
-          (*evidence,*) receivedTimelyProposal, inspectedProposal>>
-        /\ action' = "OnRoundCatchup"
+  \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"
 
 
 (********************* PROTOCOL TRANSITIONS ******************************)
@@ -792,6 +832,7 @@ MessageProcessing(p) ==
  *)
 Next == 
   \/ AdvanceRealTime
+  \/ FaultyBroadcast
   \/ /\ SynchronizedLocalClocks
      /\ \E p \in Corr: MessageProcessing(p)
 
@@ -810,74 +851,100 @@ AgreementOnValue ==
             /\ decision[p] = Decision(prop, r1)
             /\ decision[q] = Decision(prop, r2)
 
-\* [PBTS-CONSENSUS-TIME-VALID.0]
+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]
 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 
-        \* TODO: consider tighter bound where beginRound[pr] is replaced
-        \* w/ MedianOfRound[pr]
-        => (/\ beginRound[pr] - Precision - Delay <= t 
-            /\ t <= endConsensus[p] + Precision)
+        \* 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)
+           )
 
 \* [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] <= t 
-             /\ t <= lastBeginRound[pr]
+\* 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)
+
+
 
 \* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0]
-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)
-
+\* ConsensusRealTimeValidCorr == TODO?
 \* [PBTS-CONSENSUS-REALTIME-VALID.0]
-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
+\* ConsensusRealTimeValid == TODO?
 
 DecideAfterMin == TRUE
   \* if decide => time > min
 
 \* [PBTS-MSG-FAIR.0]
-BoundedDelay ==
-    \A r \in Rounds : 
-        (/\ proposalTime[r] /= NilTimestamp
-         /\ proposalTime[r] + Delay < realTime)
-            => \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp
+\* BoundedDelay == TODO?
 
 \* [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) : msg \in receivedTimelyProposal[p]
+\* ConsensusTimeLive == TODO?
 
 \* a conjunction of all invariants
 Inv ==
     /\ AgreementOnValue 
+    /\ ConsensusValidValue
     /\ ConsensusTimeValid
-    /\ ConsensusSafeValidCorrProp
-    \* /\ ConsensusRealTimeValid
-    \* /\ ConsensusRealTimeValidCorr
-    \* /\ BoundedDelay
+\*    /\ ConsensusSafeValidCorrProp
+\*    /\ DerivedProofOfLocks
 
 \* Liveness ==
 \*     ConsensusTimeLive