Merge 932c116ccb into e4ae922c33

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

@@ -0,0 +1,70 @@
+----------------------------- 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
+
+\* run Apalache with --cinit=CInit
+CInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

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

@@ -166,33 +166,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 *)  
 
@@ -294,15 +286,14 @@ Init ==
     /\ 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]
+    /\ proposalReceptionTime = [r \in Rounds, p \in Corr |-> NilTimestamp]
     /\ BenignRoundsInMessages(msgsPropose)
     /\ BenignRoundsInMessages(msgsPrevote)
     /\ BenignRoundsInMessages(msgsPrecommit)
     /\ 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 +305,6 @@ Init ==
         THEN Max({localClock[p] : p \in Corr})
         ELSE NilTimestamp
       ]
-    /\ proposalTime = [r \in Rounds |-> NilTimestamp]
-    /\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp]
 
 (************************ MESSAGE PASSING ********************************)
 \* @type: (PROCESS, ROUND, PROPOSAL, ROUND) => Bool;
@@ -391,7 +380,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] = Min2(@, localClock[p])]
    /\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])]
 
 \* lines 14-19, a proposal may be sent later
@@ -403,7 +392,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 +399,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 +424,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 +455,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 +477,7 @@ UponProposalInPropose(p) ==
       lockedRound, validValue, validRound>>
     /\ UNCHANGED 
       <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
-      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+      (*evidence,*) proposalReceptionTime>>
     /\ action' = "UponProposalInPropose"
 
 \* lines 28-33        
@@ -547,7 +522,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 +543,7 @@ UponQuorumOfPrevotesAny(p) ==
         lockedRound, validValue, validRound>>
       /\ UNCHANGED 
         <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
-        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+        (*evidence,*) proposalReceptionTime>>
       /\ action' = "UponQuorumOfPrevotesAny"
                      
 \* lines 36-46
@@ -616,7 +591,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 +607,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 +638,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 +653,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 +673,7 @@ OnTimeoutPropose(p) ==
     lockedRound, validValue, validRound>>
   /\ UNCHANGED 
     <<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
-    evidence, receivedTimelyProposal, inspectedProposal>>
+    evidence, proposalReceptionTime>>
   /\ action' = "OnTimeoutPropose"
 
 \* lines 44-46
@@ -718,7 +691,7 @@ OnQuorumOfNilPrevotes(p) ==
       lockedRound, validValue, validRound>>
     /\ UNCHANGED 
       <<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
-      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+      (*evidence,*) proposalReceptionTime>>
     /\ action' = "OnQuorumOfNilPrevotes"
 
 \* lines 55-56
@@ -733,14 +706,13 @@ OnRoundCatchup(p) ==
         /\ StartRound(p, r)
         /\ 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' = "OnRoundCatchup"
 
 
@@ -810,6 +782,13 @@ 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-CONSENSUS-TIME-VALID.0]
 ConsensusTimeValid ==
     \A p \in Corr: 
@@ -819,7 +798,7 @@ ConsensusTimeValid ==
         \* then 
         \* TODO: consider tighter bound where beginRound[pr] is replaced
         \* w/ MedianOfRound[pr]
-        => (/\ beginRound[pr] - Precision - Delay <= t 
+        => (/\ beginRound[pr,p] - Precision - Delay <= t 
             /\ t <= endConsensus[p] + Precision)
 
 \* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]
@@ -831,53 +810,58 @@ ConsensusSafeValidCorrProp ==
         (/\ 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 
+          => /\ beginRound[pr, p] <= t 
              /\ t <= lastBeginRound[pr]
 
-\* [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)
 
+
+\* @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 PS == POLSet(prop, r) IN
+    ( 
+      /\ IsValidPOL(PS)
+      /\ ContainsPrevoteFromCorrect(PS)
+    ) =>
+    \E rStar \in Rounds:
+      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 == 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 
     /\ ConsensusTimeValid
     /\ ConsensusSafeValidCorrProp
-    \* /\ ConsensusRealTimeValid
-    \* /\ ConsensusRealTimeValidCorr
-    \* /\ BoundedDelay
+    /\ DerivedProofOfLocks
 
 \* Liveness ==
 \*     ConsensusTimeLive