FaultyBcast + typefix

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

@@ -61,10 +61,11 @@ INSTANCE TendermintPBT_002_draft WITH
   MaxTimestamp <- 7,
   MinTimestamp <- 2,
   Delay <- 2,        
-  Precision <- 2
+  Precision <- 2,
+  PreloadAllFaultyMsgs <- FALSE
 
 \* 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

@@ -61,10 +61,11 @@ INSTANCE TendermintPBT_002_draft WITH
   MaxTimestamp <- 7,
   MinTimestamp <- 2,
   Delay <- 2,        
-  Precision <- 2
+  Precision <- 2,
+  PreloadAllFaultyMsgs <- FALSE
 
 \* run Apalache with --cinit=CInit
 CInit == \* the proposer is arbitrary -- works for safety
-  Proposer \in [Rounds -> AllProcs]
+  ArbitraryProposer
 
 =============================================================================    

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,11 @@ CONSTANTS
 
 ASSUME(N = Cardinality(Corr \union Faulty))
 
+\* Modeling parameter
+CONSTANTS
+  \* @type: Bool;
+  PreloadAllFaultyMsgs
+
 (*************************** DEFINITIONS ************************************)
 \* @type: Set(PROCESS);
 AllProcs == Corr \union Faulty      \* the set of all processes
@@ -75,6 +80,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) \* can't call-by-name for built-in operators
+    IN ApaFoldSet(Append, <<>>, 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 +121,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 +135,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
@@ -272,6 +285,19 @@ BenignRoundsInMessages(msgfun) ==
     \A m \in msgfun[r]:
       r = m.round
 
+InitMsgs ==
+  \/ /\ PreloadAllFaultyMsgs
+     /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
+     /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
+     /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
+     /\ BenignRoundsInMessages(msgsPropose)
+     /\ BenignRoundsInMessages(msgsPrevote)
+     /\ BenignRoundsInMessages(msgsPrecommit)
+  \/ /\ ~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]
@@ -283,13 +309,8 @@ 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]
+    /\ InitMsgs
     /\ proposalReceptionTime = [r \in Rounds, p \in Corr |-> NilTimestamp]
-    /\ BenignRoundsInMessages(msgsPropose)
-    /\ BenignRoundsInMessages(msgsPrevote)
-    /\ BenignRoundsInMessages(msgsPrecommit)
     /\ evidence = {}
     /\ action = "Init"
     /\ beginRound = 
@@ -306,6 +327,30 @@ Init ==
         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>>
+
 (************************ MESSAGE PASSING ********************************)
 \* @type: (PROCESS, ROUND, PROPOSAL, ROUND) => Bool;
 BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
@@ -380,7 +425,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] = 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
@@ -697,23 +742,24 @@ OnQuorumOfNilPrevotes(p) ==
 \* 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*)>>
-        /\ UNCHANGED
-          <<(*round, step,*) decision, lockedValue, 
-          lockedRound, validValue, validRound>>
-        /\ UNCHANGED 
-          <<msgsPropose, msgsPrevote, msgsPrecommit,
-          (*evidence,*) proposalReceptionTime>>
-        /\ 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 ******************************)
@@ -764,6 +810,7 @@ MessageProcessing(p) ==
  *)
 Next == 
   \/ AdvanceRealTime
+  \/ FaultyBroadcast
   \/ /\ SynchronizedLocalClocks
      /\ \E p \in Corr: MessageProcessing(p)
 
@@ -793,7 +840,8 @@ DisagreementOnValue ==
 ConsensusValidValue ==
     \A p \in Corr:
         \* decision[p] = Decision(Proposal(v,t,pr), r)
-        LET prop == decision[p][1] IN prop /= NilProposal => IsValid(prop[1])
+        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
@@ -841,12 +889,12 @@ ContainsPrevoteFromCorrect(set) ==
 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)
     ) =>
-    \E rStar \in Rounds:
       LET PSStar == POLSet(prop, rStar) IN 
         /\ rStar <= r
         /\ ContainsPrevoteFromCorrect(PSStar)