----------------------------- MODULE VoteProof ------------------------------ (***************************************************************************) (* This is a high-level consensus algorithm in which a set of processes *) (* called `acceptors' cooperatively choose a value. The algorithm uses *) (* numbered ballots, where a ballot is a round of voting. Acceptors cast *) (* votes in ballots, casting at most one vote per ballot. A value is *) (* chosen when a large enough set of acceptors, called a `quorum', have *) (* all voted for the same value in the same ballot. *) (* *) (* Ballots are not executed in order. Different acceptors may be *) (* concurrently performing actions for different ballots. *) (***************************************************************************) EXTENDS Integers, NaturalsInduction, FiniteSets, FiniteSetTheorems, WellFoundedInduction, TLC, TLAPS CONSTANT Value, \* As in module Consensus, the set of choosable values. Acceptor, \* The set of all acceptors. Quorum \* The set of all quorums. (***************************************************************************) (* The following assumption asserts that a quorum is a set of acceptors, *) (* and the fundamental assumption we make about quorums: any two quorums *) (* have a non-empty intersection. *) (***************************************************************************) ASSUME QA == /\ \A Q \in Quorum : Q \subseteq Acceptor /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 # {} THEOREM QuorumNonEmpty == \A Q \in Quorum : Q # {} PROOF BY QA ----------------------------------------------------------------------------- (***************************************************************************) (* Ballot is the set of all ballot numbers. For simplicity, we let it be *) (* the set of natural numbers. However, we write Ballot for that set to *) (* make it clear what the function of those natural numbers are. *) (* *) (* The algorithm and its refinements work with Ballot any set with minimal *) (* element 0, -1 not an element of Ballot, and a well-founded total order *) (* < on Ballot \cup {-1} with minimal element -1, and 0 < b for all *) (* non-zero b in Ballot. In the proof, any set of the form i..j must be *) (* replaced by the set of all elements b in Ballot \cup {-1} with i \leq b *) (* \leq j, and i..(j-1) by the set of such b with i \leq b < j. *) (***************************************************************************) Ballot == Nat ----------------------------------------------------------------------------- (***************************************************************************) (* In the algorithm, each acceptor can cast one or more votes, where each *) (* vote cast by an acceptor has the form <> indicating that the *) (* acceptor has voted for value v in ballot b. A value is chosen if a *) (* quorum of acceptors have voted for it in the same ballot. *) (* *) (* The algorithm uses two variables, `votes' and `maxBal', both arrays *) (* indexed by acceptor. Their meanings are: *) (* *) (* votes[a] - The set of votes cast by acceptor `a'. *) (* *) (* maxBal[a] - The number of the highest-numbered ballot in which `a' *) (* has cast a vote, or -1 if it has not yet voted. *) (* *) (* The algorithm does not let acceptor `a' vote in any ballot less than *) (* maxBal[a]. *) (* *) (* We specify our algorithm by the following PlusCal algorithm. The *) (* specification Spec defined by this algorithm describes only the safety *) (* properties of the algorithm. In other words, it specifies what steps *) (* the algorithm may take. It does not require that any (non-stuttering) *) (* steps be taken. We prove that this specification Spec implements the *) (* specification Spec of module Consensus under a refinement mapping *) (* defined below. This shows that the safety properties of the voting *) (* algorithm (and hence the algorithm with additional liveness *) (* requirements) imply the safety properties of the Consensus *) (* specification. Liveness is discussed later. *) (***************************************************************************) (*************************** --algorithm Voting { variables votes = [a \in Acceptor |-> {}], maxBal = [a \in Acceptor |-> -1]; define { (************************************************************************) (* We now define the operator SafeAt so SafeAt(b, v) is function of the *) (* state that equals TRUE if no value other than v has been chosen or *) (* can ever be chosen in the future (because the values of the *) (* variables votes and maxBal are such that the algorithm does not *) (* allow enough acceptors to vote for it). We say that value v is safe *) (* at ballot number b iff Safe(b, v) is true. We define Safe in terms *) (* of the following two operators. *) (* *) (* Note: This definition is weaker than would be necessary to allow a *) (* refinement of ordinary Paxos consensus, since it allows different *) (* quorums to "cooperate" in determining safety at b. This is used in *) (* algorithms like Vertical Paxos that are designed to allow *) (* reconfiguration within a single consensus instance, but not in *) (* ordinary Paxos. See *) (* *) (* AUTHOR = "Leslie Lamport and Dahlia Malkhi and Lidong Zhou ", *) (* TITLE = "Vertical Paxos and Primary-Backup Replication", *) (* Journal = "ACM SIGACT News (Distributed Computing Column)", *) (* editor = {Srikanta Tirthapura and Lorenzo Alvisi}, *) (* booktitle = {PODC}, *) (* publisher = {ACM}, *) (* YEAR = 2009, *) (* PAGES = "312--313" *) (************************************************************************) VotedFor(a, b, v) == <> \in votes[a] (**********************************************************************) (* True iff acceptor a has voted for v in ballot b. *) (**********************************************************************) DidNotVoteIn(a, b) == \A v \in Value : ~ VotedFor(a, b, v) (************************************************************************) (* We now define SafeAt. We define it recursively. The nicest *) (* definition is *) (* *) (* RECURSIVE SafeAt(_, _) *) (* SafeAt(b, v) == *) (* \/ b = 0 *) (* \/ \E Q \in Quorum : *) (* /\ \A a \in Q : maxBal[a] \geq b *) (* /\ \E c \in -1..(b-1) : *) (* /\ (c # -1) => /\ SafeAt(c, v) *) (* /\ \A a \in Q : *) (* \A w \in Value : *) (* VotedFor(a, c, w) => (w = v) *) (* /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteIn(a, d) *) (* *) (* However, TLAPS does not currently support recursive operator *) (* definitions. We therefore define it as follows using a recursive *) (* function definition. *) (************************************************************************) SafeAt(b, v) == LET SA[bb \in Ballot] == (****************************************************************) (* This recursively defines SA[bb] to equal SafeAt(bb, v). *) (****************************************************************) \/ bb = 0 \/ \E Q \in Quorum : /\ \A a \in Q : maxBal[a] \geq bb /\ \E c \in -1..(bb-1) : /\ (c # -1) => /\ SA[c] /\ \A a \in Q : \A w \in Value : VotedFor(a, c, w) => (w = v) /\ \A d \in (c+1)..(bb-1), a \in Q : DidNotVoteIn(a, d) IN SA[b] } (*************************************************************************) (* There are two possible actions that an acceptor can perform, each *) (* defined by a macro. In these macros, `self' is the acceptor that is *) (* to perform the action. The first action, IncreaseMaxBal(b) allows *) (* acceptor `self' to set maxBal[self] to b if b is greater than the *) (* current value of maxBal[self]. *) (*************************************************************************) macro IncreaseMaxBal(b) { when b > maxBal[self] ; maxBal[self] := b } (*************************************************************************) (* Action VoteFor(b, v) allows acceptor `self' to vote for value v in *) (* ballot b if its `when' condition is satisfied. *) (*************************************************************************) macro VoteFor(b, v) { when /\ maxBal[self] \leq b /\ DidNotVoteIn(self, b) /\ \A p \in Acceptor \ {self} : \A w \in Value : VotedFor(p, b, w) => (w = v) /\ SafeAt(b, v) ; votes[self] := votes[self] \cup {<>}; maxBal[self] := b } (*************************************************************************) (* The following process declaration asserts that every process `self' *) (* in the set Acceptor executes its body, which loops forever *) (* nondeterministically choosing a Ballot b and executing either an *) (* IncreaseMaxBal(b) action or nondeterministically choosing a value v *) (* and executing a VoteFor(b, v) action. The single label indicates *) (* that an entire execution of the body of the `while' loop is performed *) (* as a single atomic action. *) (* *) (* From this intuitive description of the process declaration, one might *) (* think that a process could be deadlocked by choosing a ballot b in *) (* which neither an IncreaseMaxBal(b) action nor any VoteFor(b, v) *) (* action is enabled. An examination of the TLA+ translation (and an *) (* elementary knowledge of the meaning of existential quantification) *) (* shows that this is not the case. You can think of all possible *) (* choices of b and of v being examined simultaneously, and one of the *) (* choices for which a step is possible being made. *) (*************************************************************************) process (acceptor \in Acceptor) { acc : while (TRUE) { with (b \in Ballot) { either IncreaseMaxBal(b) or with (v \in Value) { VoteFor(b, v) } } } } } The following is the TLA+ specification produced by the translation. Blank lines, produced by the translation because of the comments, have been deleted. ****************************) \* BEGIN TRANSLATION VARIABLES votes, maxBal (* define statement *) VotedFor(a, b, v) == <> \in votes[a] DidNotVoteIn(a, b) == \A v \in Value : ~ VotedFor(a, b, v) SafeAt(b, v) == LET SA[bb \in Ballot] == \/ bb = 0 \/ \E Q \in Quorum : /\ \A a \in Q : maxBal[a] \geq bb /\ \E c \in -1..(bb-1) : /\ (c # -1) => /\ SA[c] /\ \A a \in Q : \A w \in Value : VotedFor(a, c, w) => (w = v) /\ \A d \in (c+1)..(bb-1), a \in Q : DidNotVoteIn(a, d) IN SA[b] vars == << votes, maxBal >> ProcSet == (Acceptor) Init == (* Global variables *) /\ votes = [a \in Acceptor |-> {}] /\ maxBal = [a \in Acceptor |-> -1] acceptor(self) == \E b \in Ballot: \/ /\ b > maxBal[self] /\ maxBal' = [maxBal EXCEPT ![self] = b] /\ UNCHANGED votes \/ /\ \E v \in Value: /\ /\ maxBal[self] \leq b /\ DidNotVoteIn(self, b) /\ \A p \in Acceptor \ {self} : \A w \in Value : VotedFor(p, b, w) => (w = v) /\ SafeAt(b, v) /\ votes' = [votes EXCEPT ![self] = votes[self] \cup {<>}] /\ maxBal' = [maxBal EXCEPT ![self] = b] Next == (\E self \in Acceptor: acceptor(self)) Spec == Init /\ [][Next]_vars \* END TRANSLATION ----------------------------------------------------------------------------- (***************************************************************************) (* To reason about a recursively-defined operator, one must prove a *) (* theorem about it. In particular, to reason about SafeAt, we need to *) (* prove that SafeAt(b, v) equals the right-hand side of its definition, *) (* for b \in Ballot and v \in Value. This is not automatically true for a *) (* recursive definition. For example, from the recursive definition *) (* *) (* Silly[n \in Nat] == CHOOSE v : v # Silly[n] *) (* *) (* we cannot deduce that *) (* *) (* Silly[42] = CHOOSE v : v # Silly[42] *) (* *) (* (From that, we could easily deduce Silly[42] # Silly[42].) *) (***************************************************************************) (***************************************************************************) (* Here is the theorem that essentially asserts that SafeAt(b, v) equals *) (* the right-hand side of its definition. *) (***************************************************************************) THEOREM SafeAtProp == \A b \in Ballot, v \in Value : SafeAt(b, v) <=> \/ b = 0 \/ \E Q \in Quorum : /\ \A a \in Q : maxBal[a] \geq b /\ \E c \in -1..(b-1) : /\ (c # -1) => /\ SafeAt(c, v) /\ \A a \in Q : \A w \in Value : VotedFor(a, c, w) => (w = v) /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteIn(a, d) <1>1. SUFFICES ASSUME NEW v \in Value PROVE \A b \in Ballot : SafeAtProp!(b, v) BY Zenon <1> USE DEF Ballot <1> DEFINE Def(SA, bb) == \/ bb = 0 \/ \E Q \in Quorum : /\ \A a \in Q : maxBal[a] \geq bb /\ \E c \in -1..(bb-1) : /\ (c # -1) => /\ SA[c] /\ \A a \in Q : \A w \in Value : VotedFor(a, c, w) => (w = v) /\ \A d \in (c+1)..(bb-1), a \in Q : DidNotVoteIn(a, d) SA[bb \in Ballot] == Def(SA, bb) <1>2. \A b : SafeAt(b, v) = SA[b] BY DEF SafeAt <1>3. ASSUME NEW n \in Nat, NEW g, NEW h, \A i \in 0..(n-1) : g[i] = h[i] PROVE Def(g, n) = Def(h, n) BY <1>3 <1>4. SA = [b \in Ballot |-> Def(SA, b)] <2> HIDE DEF Def <2> QED BY <1>3, RecursiveFcnOfNat, Isa <1>5. \A b \in Ballot : SA[b] = Def(SA, b) <2> HIDE DEF Def <2> QED BY <1>4, Zenon <1>6. QED BY <1>2, <1>5, Zenon DEF SafeAt ----------------------------------------------------------------------------- (***************************************************************************) (* We now define TypeOK to be the type-correctness invariant. *) (***************************************************************************) TypeOK == /\ votes \in [Acceptor -> SUBSET (Ballot \X Value)] /\ maxBal \in [Acceptor -> Ballot \cup {-1}] (***************************************************************************) (* We now define `chosen' to be the state function so that the algorithm *) (* specified by formula Spec conjoined with the liveness requirements *) (* described below implements the algorithm of module Consensus (satisfies *) (* the specification LiveSpec of that module) under a refinement mapping *) (* that substitutes this state function `chosen' for the variable `chosen' *) (* of module Consensus. The definition uses the following one, which *) (* defines ChosenIn(b, v) to be true iff a quorum of acceptors have all *) (* voted for v in ballot b. *) (***************************************************************************) ChosenIn(b, v) == \E Q \in Quorum : \A a \in Q : VotedFor(a, b, v) chosen == {v \in Value : \E b \in Ballot : ChosenIn(b, v)} ----------------------------------------------------------------------------- (***************************************************************************) (* The following lemma is used for reasoning about the operator SafeAt. *) (* It is proved from SafeAtProp by induction. *) (***************************************************************************) LEMMA SafeLemma == TypeOK => \A b \in Ballot : \A v \in Value : SafeAt(b, v) => \A c \in 0..(b-1) : \E Q \in Quorum : \A a \in Q : /\ maxBal[a] >= c /\ \/ DidNotVoteIn(a, c) \/ VotedFor(a, c, v) <1> SUFFICES ASSUME TypeOK PROVE SafeLemma!2 OBVIOUS <1> DEFINE P(b) == \A c \in 0..b : SafeLemma!2!(c) <1> USE DEF Ballot <1>1. P(0) OBVIOUS <1>2. ASSUME NEW b \in Ballot, P(b) PROVE P(b+1) <2>1. /\ b+1 \in Ballot \ {0} /\ (b+1) - 1 = b OBVIOUS <2>2. 0..(b+1) = (0..b) \cup {b+1} OBVIOUS <2>3. SUFFICES ASSUME NEW v \in Value, SafeAt(b+1, v), NEW c \in 0..b PROVE \E Q \in Quorum : \A a \in Q : /\ maxBal[a] >= c /\ \/ DidNotVoteIn(a, c) \/ VotedFor(a, c, v) BY <1>2 <2>4. PICK Q \in Quorum : /\ \A a \in Q : maxBal[a] \geq (b+1) /\ \E cc \in -1..b : /\ (cc # -1) => /\ SafeAt(cc, v) /\ \A a \in Q : \A w \in Value : VotedFor(a, cc, w) => (w = v) /\ \A d \in (cc+1)..b, a \in Q : DidNotVoteIn(a, d) BY SafeAtProp, <2>3, <2>1, Zenon <2>5. PICK cc \in -1..b : /\ (cc # -1) => /\ SafeAt(cc, v) /\ \A a \in Q : \A w \in Value : VotedFor(a, cc, w) => (w = v) /\ \A d \in (cc+1)..b, a \in Q : DidNotVoteIn(a, d) BY <2>4 <2>6. CASE c > cc BY <2>4, <2>5, <2>6, QA DEF TypeOK <2>7. CASE c = cc <3>2. \A a \in Q : maxBal[a] \in Ballot \cup {-1} BY QA DEF TypeOK <3>3. \A a \in Q : maxBal[a] \geq c BY <2>4, <2>7, <3>2 <3>4. \A a \in Q : \/ DidNotVoteIn(a, c) \/ VotedFor(a, c, v) BY <2>7, <2>5 DEF DidNotVoteIn <3>5. QED BY <3>3, <3>4 <2>8. CASE c < cc BY <2>8, <1>2, <2>5 <2>9. QED BY <2>6, <2>7, <2>8 <1>3. \A b \in Ballot : P(b) BY <1>1, <1>2, NatInduction, Isa <1>4. QED BY <1>3 ----------------------------------------------------------------------------- (***************************************************************************) (* We now define the invariant that is used to prove the correctness of *) (* our algorithm--meaning that specification Spec implements specification *) (* Spec of module Consensus under our refinement mapping. Correctness of *) (* the voting algorithm follows from the the following three invariants: *) (* *) (* VInv1: In any ballot, an acceptor can vote for at most one value. *) (* *) (* VInv2: An acceptor can vote for a value v in ballot b iff v is *) (* safe at b. *) (* *) (* VInv3: Two different acceptors cannot vote for different values in *) (* the same ballot. *) (* *) (* Their precise definitions are as follows. *) (***************************************************************************) VInv1 == \A a \in Acceptor, b \in Ballot, v, w \in Value : VotedFor(a, b, v) /\ VotedFor(a, b, w) => (v = w) VInv2 == \A a \in Acceptor, b \in Ballot, v \in Value : VotedFor(a, b, v) => SafeAt(b, v) VInv3 == \A a1, a2 \in Acceptor, b \in Ballot, v1, v2 \in Value : VotedFor(a1, b, v1) /\ VotedFor(a2, b, v2) => (v1 = v2) (***************************************************************************) (* It is obvious, that VInv3 implies VInv1--a fact that we now let TLAPS *) (* prove as a little check that we haven't made a mistake in our *) (* definitions. (Actually, we used TLC to check everything before *) (* attempting any proofs.) We define VInv1 separately because VInv3 is not *) (* needed for proving safety, only for liveness. *) (***************************************************************************) THEOREM VInv3 => VInv1 BY DEF VInv1, VInv3 ----------------------------------------------------------------------------- (***************************************************************************) (* The following lemma proves that SafeAt(b, v) implies that no value *) (* other than v can have been chosen in any ballot numbered less than b. *) (* The fact that it also implies that no value other than v can ever be *) (* chosen in the future follows from this and the fact that SafeAt(b, v) *) (* is stable--meaning that once it becomes true, it remains true forever. *) (* The stability of SafeAt(b, v) is proved as step <1>6 of theorem *) (* InductiveInvariance below. *) (* *) (* This lemma is used only in the proof of theorem VT1 below. *) (***************************************************************************) LEMMA VT0 == /\ TypeOK /\ VInv1 /\ VInv2 => \A v, w \in Value, b, c \in Ballot : (b > c) /\ SafeAt(b, v) /\ ChosenIn(c, w) => (v = w) <1> SUFFICES ASSUME TypeOK, VInv1, VInv2, NEW v \in Value, NEW w \in Value PROVE \A b, c \in Ballot : (b > c) /\ SafeAt(b, v) /\ ChosenIn(c, w) => (v = w) OBVIOUS <1> P(b) == \A c \in Ballot : (b > c) /\ SafeAt(b, v) /\ ChosenIn(c, w) => (v = w) <1> USE DEF Ballot <1>1. P(0) OBVIOUS <1>2. ASSUME NEW b \in Ballot, \A i \in 0..(b-1) : P(i) PROVE P(b) <2>1. CASE b = 0 BY <2>1 <2>2. CASE b # 0 <3>1. SUFFICES ASSUME NEW c \in Ballot, b > c, SafeAt(b, v), ChosenIn(c, w) PROVE v=w OBVIOUS <3>2. PICK Q \in Quorum : \A a \in Q : VotedFor(a, c, w) BY <3>1 DEF ChosenIn <3>3. PICK QQ \in Quorum, d \in -1..(b-1) : /\ (d # -1) => /\ SafeAt(d, v) /\ \A a \in QQ : \A x \in Value : VotedFor(a, d, x) => (x = v) /\ \A e \in (d+1)..(b-1), a \in QQ : DidNotVoteIn(a, e) BY <2>2, <3>1, SafeAtProp, Zenon <3> PICK aa \in QQ \cap Q : TRUE BY QA <3>4. c \leq d BY <3>1, <3>2, <3>3 DEF DidNotVoteIn <3>5. CASE c = d BY <3>2, <3>3, <3>4, <3>5 <3>6. CASE d > c BY <1>2, <3>1, <3>3, <3>4, <3>6 <3>7. QED BY <3>4, <3>5, <3>6 <2>. QED BY <2>1, <2>2 <1>3. \A b \in Ballot : P(b) <2>. HIDE DEF P <2>. QED BY <1>2, GeneralNatInduction, Isa <1>4. QED BY <1>3 (***************************************************************************) (* The following theorem asserts that the invariance of TypeOK, VInv1, and *) (* VInv2 implies that the algorithm satisfies the basic consensus property *) (* that at most one value is chosen (at any time). If you can prove it, *) (* then you understand why the Paxos consensus algorithm allows only a *) (* single value to be chosen. Note that VInv3 is not needed to prove this *) (* property. *) (***************************************************************************) THEOREM VT1 == /\ TypeOK /\ VInv1 /\ VInv2 => \A v, w : (v \in chosen) /\ (w \in chosen) => (v = w) <1>1. SUFFICES ASSUME TypeOK, VInv1, VInv2, NEW v, NEW w, v \in chosen, w \in chosen PROVE v = w OBVIOUS <1>2. v \in Value /\ w \in Value BY <1>1 DEF chosen <1>3. PICK b \in Ballot, c \in Ballot : ChosenIn(b, v) /\ ChosenIn(c, w) BY <1>1 DEF chosen <1>4. PICK Q \in Quorum, R \in Quorum : /\ \A a \in Q : VotedFor(a, b, v) /\ \A a \in R : VotedFor(a, c, w) BY <1>3 DEF ChosenIn <1>5. PICK av \in Q, aw \in R: /\ VotedFor(av, b, v) /\ VotedFor(aw, c, w) BY <1>4, QuorumNonEmpty <1>6. SafeAt(b, v) /\ SafeAt(c, w) BY <1>1, <1>2, <1>5, QA DEF VInv2 <1>7. CASE b = c <2> PICK a \in Q \cap R : TRUE BY QA <2>1. /\ VotedFor(a, b, v) /\ VotedFor(a, c, w) BY <1>4 <2>2. QED BY <1>1, <1>2, <1>7, <2>1, QA DEF VInv1 <1>8. CASE b > c BY <1>1, <1>6, <1>3, <1>8, VT0, <1>2 <1>9. CASE c > b BY <1>1, <1>6, <1>3, <1>9, VT0, <1>2 <1>10. QED BY <1>7, <1>8, <1>9 DEF Ballot (***************************************************************************) (* The rest of the proof uses only the primed version of VT1--that is, the *) (* theorem whose statement is VT1'. (Remember that VT1 names the formula *) (* being asserted by the theorem we call VT1.) The formula VT1' asserts *) (* that VT1 is true in the second state of any transition (pair of *) (* states). We derive that theorem from VT1 by simple temporal logic, and *) (* similarly for VT0 and SafeAtProp. *) (***************************************************************************) THEOREM SafeAtPropPrime == \A b \in Ballot, v \in Value : SafeAt(b, v)' <=> \/ b = 0 \/ \E Q \in Quorum : /\ \A a \in Q : maxBal'[a] \geq b /\ \E c \in -1..(b-1) : /\ (c # -1) => /\ SafeAt(c, v)' /\ \A a \in Q : \A w \in Value : VotedFor(a, c, w)' => (w = v) /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteIn(a, d)' <1>1. SafeAtProp' BY SafeAtProp, PTL <1>. QED BY <1>1 LEMMA VT0Prime == /\ TypeOK' /\ VInv1' /\ VInv2' => \A v, w \in Value, b, c \in Ballot : (b > c) /\ SafeAt(b, v)' /\ ChosenIn(c, w)' => (v = w) <1>1. VT0' BY VT0, PTL <1>. QED BY <1>1 THEOREM VT1Prime == /\ TypeOK' /\ VInv1' /\ VInv2' => \A v, w : (v \in chosen') /\ (w \in chosen') => (v = w) <1>1. VT1' BY VT1, PTL <1>. QED BY <1>1 ----------------------------------------------------------------------------- (***************************************************************************) (* The invariance of VInv2 depends on SafeAt(b, v) being stable, meaning *) (* that once it becomes true it remains true forever. Stability of *) (* SafeAt(b, v) depends on the following invariant. *) (***************************************************************************) VInv4 == \A a \in Acceptor, b \in Ballot : maxBal[a] < b => DidNotVoteIn(a, b) (***************************************************************************) (* The inductive invariant that we use to prove correctness of this *) (* algorithm is VInv, defined as follows. *) (***************************************************************************) VInv == TypeOK /\ VInv2 /\ VInv3 /\ VInv4 ----------------------------------------------------------------------------- (***************************************************************************) (* To simplify reasoning about the next-state action Next, we want to *) (* express it in a more convenient form. This is done by lemma NextDef *) (* below, which shows that Next equals an action defined in terms of the *) (* following subactions. *) (***************************************************************************) IncreaseMaxBal(self, b) == /\ b > maxBal[self] /\ maxBal' = [maxBal EXCEPT ![self] = b] /\ UNCHANGED votes VoteFor(self, b, v) == /\ maxBal[self] \leq b /\ DidNotVoteIn(self, b) /\ \A p \in Acceptor \ {self} : \A w \in Value : VotedFor(p, b, w) => (w = v) /\ SafeAt(b, v) /\ votes' = [votes EXCEPT ![self] = votes[self] \cup {<>}] /\ maxBal' = [maxBal EXCEPT ![self] = b] BallotAction(self, b) == \/ IncreaseMaxBal(self, b) \/ \E v \in Value : VoteFor(self, b, v) (***************************************************************************) (* When proving lemma NextDef, we were surprised to discover that it *) (* required the assumption that the set of acceptors is non-empty. This *) (* assumption isn't necessary for safety, since if there are no acceptors *) (* there can be no quorums (see theorem QuorumNonEmpty above) so no value *) (* is ever chosen and the Consensus specification is trivially implemented *) (* under our refinement mapping. However, the assumption is necessary for *) (* liveness and it allows us to lemma NextDef for the safety proof as *) (* well, so we assert it now. *) (***************************************************************************) ASSUME AcceptorNonempty == Acceptor # {} (***************************************************************************) (* The proof of the lemma itself is quite simple. *) (***************************************************************************) LEMMA NextDef == TypeOK => (Next = \E self \in Acceptor : \E b \in Ballot : BallotAction(self, b) ) <1> HAVE TypeOK <1>2. Next = \E self \in Acceptor: acceptor(self) BY AcceptorNonempty DEF Next, ProcSet <1>3. @ = NextDef!2!2 BY DEF Next, BallotAction, IncreaseMaxBal, VoteFor, ProcSet, acceptor <1>4. QED BY <1>2, <1>3 ----------------------------------------------------------------------------- (***************************************************************************) (* We now come to the proof that VInv is an invariant of the *) (* specification. This follows from the following result, which asserts *) (* that it is an inductive invariant of the next-state action. This fact *) (* is used in the liveness proof as well. *) (***************************************************************************) THEOREM InductiveInvariance == VInv /\ [Next]_vars => VInv' <1>1. VInv /\ (vars' = vars) => VInv' BY Isa DEF VInv, vars, TypeOK, VInv2, VotedFor, SafeAt, DidNotVoteIn, VInv3, VInv4 <1> SUFFICES ASSUME VInv, NEW self \in Acceptor, NEW b \in Ballot, BallotAction(self, b) PROVE VInv' BY <1>1, NextDef DEF VInv <1>2. TypeOK' <2>1. CASE IncreaseMaxBal(self, b) BY <2>1 DEF IncreaseMaxBal, VInv, TypeOK <2>2. CASE \E v \in Value : VoteFor(self, b, v) BY <2>2 DEF VInv, TypeOK, VoteFor <2>3. QED BY <2>1, <2>2 DEF BallotAction <1>3. ASSUME NEW a \in Acceptor, NEW c \in Ballot, NEW w \in Value, VotedFor(a, c, w) PROVE VotedFor(a, c, w)' <2>1. CASE IncreaseMaxBal(self, b) BY <2>1, <1>3 DEF IncreaseMaxBal, VotedFor <2>2. CASE \E v \in Value : VoteFor(self, b, v) <3>1. PICK v \in Value : VoteFor(self, b, v) BY <2>2 <3>2. CASE a = self <4>1. votes'[a] = votes[a] \cup {<>} BY <3>1, <3>2 DEF VoteFor, VInv, TypeOK <4>2. QED BY <1>3, <4>1 DEF VotedFor <3>3. CASE a # self <4>1. votes[a] = votes'[a] BY <3>1, <3>3 DEF VoteFor, VInv, TypeOK <4>2. QED BY <1>3, <4>1 DEF VotedFor <3>4. QED BY <3>2, <3>3 DEF VoteFor <2>3. QED BY <2>1, <2>2 DEF BallotAction <1>4. ASSUME NEW a \in Acceptor, NEW c \in Ballot, NEW w \in Value, ~VotedFor(a, c, w), VotedFor(a, c, w)' PROVE (a = self) /\ (c = b) /\ VoteFor(self, b, w) <2>1. CASE IncreaseMaxBal(self, b) BY <2>1, <1>4 DEF IncreaseMaxBal, VInv, TypeOK, VotedFor <2>2. CASE \E v \in Value : VoteFor(self, b, v) <3>1. PICK v \in Value : VoteFor(self, b, v) BY <2>2 <3>2. a = self BY <3>1, <1>4 DEF VoteFor, VInv, TypeOK, VotedFor <3>3. votes'[a] = votes[a] \cup {<>} BY <3>1, <3>2 DEF VoteFor, VInv, TypeOK <3>4. c = b /\ v = w BY <1>4, <3>3 DEF VotedFor <3>5. QED BY <3>1, <3>2, <3>4 <2>3. QED BY <2>1, <2>2 DEF BallotAction <1>5. ASSUME NEW a \in Acceptor PROVE /\ maxBal[a] \in Ballot \cup {-1} /\ maxBal'[a] \in Ballot \cup {-1} /\ maxBal'[a] >= maxBal[a] BY DEF VInv, TypeOK, IncreaseMaxBal, VInv, VoteFor, BallotAction, DidNotVoteIn, VotedFor, Ballot <1>6. ASSUME NEW c \in Ballot, NEW w \in Value, SafeAt(c, w) PROVE SafeAt(c, w)' <2> USE DEF Ballot <2> DEFINE P(i) == \A j \in 0..i : SafeAt(j, w) => SafeAt(j, w)' <2>1. P(0) BY SafeAtPropPrime, 0 .. 0 = {0}, Zenon <2>2. ASSUME NEW d \in Ballot, P(d) PROVE P(d+1) <3>1. SUFFICES ASSUME NEW e \in 0..(d+1), SafeAt(e, w) PROVE SafeAt(e, w)' OBVIOUS <3>2. CASE e \in 0..d BY <2>2, <3>1, <3>2 <3>3. CASE e = d+1 <4>. e \in Ballot \ {0} BY <3>3 <4>1. PICK Q \in Quorum : SafeAtProp!(e, w)!2!2!(Q) BY <3>1, SafeAtProp, Zenon <4>2. \A aa \in Q : maxBal'[aa] \geq e BY <1>5, <4>1, QA <4>3. \E cc \in -1..(e-1) : /\ (cc # -1) => /\ SafeAt(cc, w)' /\ \A ax \in Q : \A z \in Value : VotedFor(ax, cc, z)' => (z = w) /\ \A dd \in (cc+1)..(e-1), ax \in Q : DidNotVoteIn(ax, dd)' <5>1. ASSUME NEW cc \in 0..(e-1), NEW ax \in Q, NEW z \in Value, VotedFor(ax, cc, z)', ~ VotedFor(ax, cc, z) PROVE FALSE <6>1. (ax = self) /\ (cc = b) /\ VoteFor(self, b, z) BY <5>1, <1>4, QA <6>2. /\ maxBal[ax] \geq e /\ maxBal[self] \leq b BY <4>1, <6>1 DEF VoteFor <6>. QED BY <3>3, <6>1, <6>2 DEF VInv, TypeOK <5>2. PICK cc \in -1..(e-1) : SafeAtProp!(e, w)!2!2!(Q)!2!(cc) BY <4>1 <5>3. ASSUME cc # -1 PROVE /\ SafeAt(cc, w)' /\ \A ax \in Q : \A z \in Value : VotedFor(ax, cc, z)' => (z = w) <6>1. /\ SafeAt(cc, w) /\ \A ax \in Q : \A z \in Value : VotedFor(ax, cc, z) => (z = w) BY <5>2, <5>3 <6>2. SafeAt(cc, w)' BY <6>1, <5>3, <3>3, <2>2 <6>3. ASSUME NEW ax \in Q, NEW z \in Value, VotedFor(ax, cc, z)' PROVE z = w <7>1. CASE VotedFor(ax, cc, z) BY <6>1, <7>1 <7>2. CASE ~ VotedFor(ax, cc, z) BY <7>2, <6>3, <5>1, <5>3 <7>3. QED BY <7>1, <7>2 <6>4. QED BY <6>2, <6>3 <5>4. ASSUME NEW dd \in (cc+1)..(e-1), NEW ax \in Q, ~ DidNotVoteIn(ax, dd)' PROVE FALSE BY <5>2, <5>1, <5>4 DEF DidNotVoteIn <5>5. QED BY <5>3, <5>4 <4>4. \/ e = 0 \/ \E Q_1 \in Quorum : /\ \A aa \in Q_1 : maxBal'[aa] \geq e /\ \E c_1 \in -1..e - 1 : /\ c_1 # -1 => (/\ SafeAt(c_1, w)' /\ \A aa \in Q_1 : \A w_1 \in Value : VotedFor(aa, c_1, w_1)' => w_1 = w) /\ \A d_1 \in c_1 + 1..e - 1, aa \in Q_1 : DidNotVoteIn(aa, d_1)' BY <4>2, <4>3, <3>3 <4>6. SafeAt(e, w)' <=> <4>4 BY SafeAtPropPrime, <3>3, Zenon <4>7. QED BY <4>2, <4>3, <4>6 <3>4. QED BY <3>2, <3>3 <2>3. \A d \in Ballot : P(d) BY <2>1, <2>2, NatInduction, Isa <2>4. QED BY <2>3, <1>6 <1>7. VInv2' <2>1. SUFFICES ASSUME NEW a \in Acceptor, NEW c \in Ballot, NEW v \in Value, VotedFor(a, c, v)' PROVE SafeAt(c, v)' BY DEF VInv2 <2>2. CASE VotedFor(a, c, v) BY <1>6, <2>2 DEF VInv, VInv2 <2>3. CASE ~VotedFor(a, c, v) BY <1>6, <2>1, <2>3, <1>4 DEF VoteFor <2>4. QED BY <2>2, <2>3 <1>8. VInv3' <2>1. ASSUME NEW a1 \in Acceptor, NEW a2\in Acceptor, NEW c \in Ballot, NEW v1 \in Value, NEW v2 \in Value, VotedFor(a1, c, v1)', VotedFor(a2, c, v2)', VotedFor(a1, c, v1), VotedFor(a2, c, v2) PROVE v1 = v2 BY <2>1 DEF VInv, VInv3 <2>2. ASSUME NEW a1 \in Acceptor, NEW a2\in Acceptor, NEW c \in Ballot, NEW v1 \in Value, NEW v2 \in Value, VotedFor(a1, c, v1)', VotedFor(a2, c, v2)', ~ VotedFor(a1, c, v1) PROVE v1 = v2 <3>1. (a1 = self) /\ (c = b) /\ VoteFor(self, b, v1) BY <2>2, <1>4 <3>2. CASE a2 = self <4>1. ~VotedFor(self, b, v2) BY <3>1 DEF VoteFor, DidNotVoteIn <4>2. VoteFor(self, b, v2) BY <2>2, <3>1, <3>2, <4>1, <1>4 <4>. QED BY <3>1, <4>2, <2>2 DEF VotedFor, VoteFor, VInv, TypeOK <3>3. CASE a2 # self BY <3>1, <3>3, <2>2 DEF VotedFor, VoteFor, VInv, TypeOK <3>4. QED BY <3>2, <3>3 <2>3. QED BY <2>1, <2>2 DEF VInv3 <1>9. VInv4' <2>1. SUFFICES ASSUME NEW a \in Acceptor, NEW c \in Ballot, maxBal'[a] < c, ~ DidNotVoteIn(a, c)' PROVE FALSE BY DEF VInv4 <2>2. maxBal[a] < c BY <1>5, <2>1 DEF Ballot <2>3. DidNotVoteIn(a, c) BY <2>2 DEF VInv, VInv4 <2>4. PICK v \in Value : VotedFor(a, c, v)' BY <2>1 DEF DidNotVoteIn <2>5. (a = self) /\ (c = b) /\ VoteFor(self, b, v) BY <1>4, <2>1, <2>3, <2>4 DEF DidNotVoteIn <2>6. maxBal'[a] = c BY <2>5 DEF VoteFor, VInv, TypeOK <2>7. QED BY <2>1, <2>6 DEF Ballot <1>10. QED BY <1>2, <1>7, <1>8, <1>9 DEF VInv (***************************************************************************) (* The invariance of VInv follows easily from theorem InductiveInvariance *) (* and the following result, which is easy to prove with TLAPS. *) (***************************************************************************) THEOREM InitImpliesInv == Init => VInv BY DEF Init, VInv, TypeOK, ProcSet, VInv2, VInv3, VInv4, VotedFor, DidNotVoteIn (***************************************************************************) (* The following theorem asserts that VInv is an invariant of Spec. *) (***************************************************************************) THEOREM VT2 == Spec => []VInv BY InitImpliesInv, InductiveInvariance, PTL DEF Spec ----------------------------------------------------------------------------- (***************************************************************************) (* The following INSTANCE statement instantiates module Consensus with the *) (* following expressions substituted for the parameters (the CONSTANTS and *) (* VARIABLES) of that module: *) (* *) (* Parameter of Consensus Expression (of this module) *) (* ---------------------- --------------------------- *) (* Value Value *) (* chosen chosen *) (* *) (* (Note that if no substitution is specified for a parameter, the default *) (* is to substitute the parameter or defined operator of the same name.) *) (* More precisely, for each defined identifier id of module Consensus, *) (* this statement defines C!id to equal the value of id under these *) (* substitutions. *) (***************************************************************************) C == INSTANCE Consensus (***************************************************************************) (* The following theorem asserts that the safety properties of the voting *) (* algorithm (specified by formula Spec) of this module implement the *) (* consensus safety specification Spec of module Consensus under the *) (* substitution (refinement mapping) of the INSTANCE statement. *) (***************************************************************************) THEOREM VT3 == Spec => C!Spec <1>1. Init => C!Init <2> SUFFICES ASSUME Init PROVE C!Init OBVIOUS <2>1. SUFFICES ASSUME NEW v \in chosen PROVE FALSE BY DEF C!Init <2>2. PICK b \in Ballot, Q \in Quorum : \A a \in Q : VotedFor(a, b, v) BY <2>1 DEF chosen, ChosenIn <2>3. PICK a \in Q : <> \in votes[a] BY QuorumNonEmpty, <2>2 DEF VotedFor <2>4. QED BY <2>3, QA DEF Init <1>2. VInv /\ VInv'/\ [Next]_vars => [C!Next]_C!vars <2>. SUFFICES ASSUME VInv, VInv', [Next]_vars PROVE [C!Next]_C!vars OBVIOUS <2>1. CASE vars' = vars BY <2>1 DEF vars, C!vars, chosen, ChosenIn, VotedFor <2>2. SUFFICES ASSUME NEW self \in Acceptor, NEW b \in Ballot, BallotAction(self, b) PROVE [C!Next]_C!vars BY <2>1, NextDef DEF VInv <2>3. ASSUME IncreaseMaxBal(self, b) PROVE C!vars' = C!vars BY <2>3 DEF IncreaseMaxBal, C!vars, chosen, ChosenIn, VotedFor <2>4. ASSUME NEW v \in Value, VoteFor(self, b, v) PROVE [C!Next]_C!vars <3>3. ASSUME NEW w \in chosen PROVE w \in chosen' <4>1. PICK c \in Ballot, Q \in Quorum : \A a \in Q : <> \in votes[a] BY <3>3 DEF chosen, ChosenIn, VotedFor <4>2. SUFFICES ASSUME NEW a \in Q PROVE <> \in votes'[a] BY DEF chosen, ChosenIn, VotedFor <4>3. CASE a = self BY <2>4, <4>1, <4>3 DEF VoteFor, VInv, TypeOK <4>4. CASE a # self BY <2>4, <4>1, <4>4, QA DEF VoteFor, VInv, TypeOK <4>5. QED BY <4>3, <4>4 <3>1. ASSUME NEW w \in chosen, v \in chosen' PROVE w = v BY <3>3, <3>1, VT1Prime DEF VInv, VInv1, VInv3 <3>2. ASSUME NEW w, w \notin chosen, w \in chosen' PROVE w = v <4>2. PICK c \in Ballot, Q \in Quorum : \A a \in Q : <> \in votes'[a] BY <3>2 DEF chosen, ChosenIn, VotedFor <4>3. PICK a \in Q : <> \notin votes[a] BY <3>2 DEF chosen, ChosenIn, VotedFor <4>4. CASE a = self BY <2>4, <4>4, <4>2, <4>3 DEF VoteFor, VInv, TypeOK <4>5. CASE a # self BY <2>4, <4>2, <4>3, <4>5, QA DEF VoteFor, VInv, TypeOK <4>6. QED BY <4>4, <4>5 <3>. QED BY <3>3, <3>1, <3>2 DEF C!Next, C!vars <2>5. QED BY <2>2, <2>3, <2>4 DEF BallotAction <1>3. QED BY <1>1, <1>2, VT2, PTL DEF Spec, C!Spec ----------------------------------------------------------------------------- (***************************************************************************) (* Liveness *) (* *) (* We now state the liveness property required of our voting algorithm and *) (* prove that it and the safety property imply specification LiveSpec of *) (* module Consensus under our refinement mapping. *) (* *) (* We begin by stating two additional assumptions that are necessary for *) (* liveness. Liveness requires that some value eventually be chosen. *) (* This cannot hold with an infinite set of acceptors. More precisely, *) (* liveness requires the existence of a finite quorum. (Otherwise, it *) (* would be impossible for all acceptors of any quorum ever to have voted, *) (* so no value could ever be chosen.) Moreover, it is impossible to choose *) (* a value if there are no values. Hence, we make the following two *) (* assumptions. *) (***************************************************************************) ASSUME AcceptorFinite == IsFiniteSet(Acceptor) ASSUME ValueNonempty == Value # {} ----------------------------------------------------------------------------- LEMMA FiniteSetHasMax == ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), S # {} PROVE \E max \in S : \A x \in S : max >= x <1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E max \in T : \A x \in T : max >= x <1>1. P({}) OBVIOUS <1>2. ASSUME NEW T, NEW x, P(T), x \notin T PROVE P(T \cup {x}) BY <1>2 <1>3. \A T : IsFiniteSet(T) => P(T) <2>. HIDE DEF P <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") <1>. QED BY <1>3, Zenon ----------------------------------------------------------------------------- (***************************************************************************) (* The following theorem implies that it is always possible to find a *) (* ballot number b and a value v safe at b by choosing b large enough and *) (* then having a quorum of acceptors perform IncreaseMaxBal(b) actions. *) (* It will be used in the liveness proof. Observe that it is for *) (* liveness, not safety, that invariant VInv3 is required. *) (***************************************************************************) THEOREM VT4 == TypeOK /\ VInv2 /\ VInv3 => \A Q \in Quorum, b \in Ballot : (\A a \in Q : (maxBal[a] >= b)) => \E v \in Value : SafeAt(b,v) \* Checked as an invariant by TLC with 3 acceptors, 3 ballots, 2 values <1>. USE DEF Ballot <1>1. SUFFICES ASSUME TypeOK, VInv2, VInv3, NEW Q \in Quorum, NEW b \in Ballot, (\A a \in Q : (maxBal[a] >= b)) PROVE \E v \in Value : SafeAt(b, v) OBVIOUS <1>2. CASE b = 0 BY ValueNonempty, <1>1, SafeAtProp, <1>2, Zenon <1>4. SUFFICES ASSUME b # 0 PROVE \E v \in Value : \E c \in -1..(b-1) : /\ (c # -1) => /\ SafeAt(c, v) /\ \A a \in Q : \A w \in Value : VotedFor(a, c, w) => (w = v) /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteIn(a, d) BY <1>1, <1>2, SafeAtProp <1>5. CASE \A a \in Q, c \in 0..(b-1) : DidNotVoteIn(a, c) BY <1>5, ValueNonempty <1>6. CASE \E a \in Q, c \in 0..(b-1) : ~DidNotVoteIn(a, c) <2>1. PICK c \in 0..(b-1) : /\ \E a \in Q : ~DidNotVoteIn(a, c) /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteIn(a, d) <3> DEFINE S == {c \in 0..(b-1) : \E a \in Q : ~DidNotVoteIn(a, c)} <3>1. S # {} BY <1>6 <3>2. PICK c \in S : \A d \in S : c >= d <4>2. IsFiniteSet(S) BY FS_Interval, FS_Subset, 0 \in Int, b-1 \in Int, Zenon <4>3. QED BY <3>1, <4>2, FiniteSetHasMax <3>. QED BY <3>2 DEF Ballot <2>4. PICK a0 \in Q, v \in Value : VotedFor(a0, c, v) BY <2>1 DEF DidNotVoteIn <2>5. \A a \in Q : \A w \in Value : VotedFor(a, c, w) => (w = v) BY <2>4, QA, <1>1 DEF VInv3 <2>6. SafeAt(c, v) BY <1>1, <2>4, QA DEF VInv2 <2>7. QED BY <2>1, <2>5, <2>6 <1>7. QED BY <1>5, <1>6 ------------------------------------------------------------------------------- (***************************************************************************) (* The progress property we require of the algorithm is that a quorum of *) (* acceptors, by themselves, can eventually choose a value v. This means *) (* that, for some quorum Q and ballot b, the acceptors `a' of Q must make *) (* SafeAt(b, v) true by executing IncreaseMaxBal(a, b) and then must *) (* execute VoteFor(a, b, v) to choose v. In order to be able to execute *) (* VoteFor(a, b, v), acceptor `a' must not execute a Ballot(a, c) action *) (* for any c > b. *) (* *) (* These considerations lead to the following liveness requirement *) (* LiveAssumption. The WF condition ensures that the acceptors `a' in Q *) (* eventually execute the necessary BallotAction(a, b) actions if they are *) (* enabled, and the [][...]_vars condition ensures that they never perform *) (* BallotAction actions for higher-numbered ballots, so the necessary *) (* BallotAction(a, b) actions are enabled. *) (***************************************************************************) LiveAssumption == \E Q \in Quorum, b \in Ballot : /\ \A self \in Q : WF_vars(BallotAction(self, b)) /\ [] [\A self \in Q : \A c \in Ballot : (c > b) => ~ BallotAction(self, c)]_vars LiveSpec == Spec /\ LiveAssumption (***************************************************************************) (* LiveAssumption is stronger than necessary. Instead of requiring that *) (* an acceptor in Q never executes an action of a higher-numbered ballot *) (* than b, it suffices that it doesn't execute such an action until unless *) (* it has voted in ballot b. However, the natural liveness requirement *) (* for a Paxos consensus algorithm implies condition LiveAssumption. *) (* *) (* Condition LiveAssumption is a liveness property, constraining only what *) (* eventually happens. It is straightforward to replace "eventually *) (* happens" by "happens within some length of time" and convert *) (* LiveAssumption into a real-time condition. We have not done that for *) (* three reasons: *) (* *) (* 1. The real-time requirement and, we believe, the real-time reasoning *) (* will be more complicated, since temporal logic was developed to *) (* abstract away much of the complexity of reasoning about explicit *) (* times. *) (* *) (* 2. TLAPS does not yet support reasoning about real numbers. *) (* *) (* 3. Reasoning about real-time specifications consists entirely *) (* of safety reasoning, which is almost entirely action reasoning. *) (* We want to see how the TLA+ proof language and TLAPS do on *) (* temporal logic reasoning. *) (* *) (* *) (***************************************************************************) ----------------------------------------------------------------------------- (***************************************************************************) (* Here are two temporal-logic proof rules. Their validity is obvious *) (* when you understand what they mean. *) (***************************************************************************) THEOREM AlwaysForall == ASSUME NEW CONSTANT S, NEW TEMPORAL P(_) PROVE (\A s \in S : []P(s)) <=> [](\A s \in S : P(s)) OBVIOUS LEMMA EventuallyAlwaysForall == ASSUME NEW CONSTANT S, IsFiniteSet(S), NEW TEMPORAL P(_) PROVE (\A s \in S : <>[]P(s)) => <>[](\A s \in S : P(s)) <1>. DEFINE A(x) == <>[]P(x) L(T) == \A s \in T : A(s) R(T) == \A s \in T : P(s) Q(T) == L(T) => <>[]R(T) <1>1. Q({}) <2>1. R({}) OBVIOUS <2>2. <>[]R({}) BY <2>1, PTL <2>. QED BY <2>2 <1>2. ASSUME NEW T, NEW x PROVE Q(T) => Q(T \cup {x}) <2>1. L(T \cup {x}) => A(x) <3>. HIDE DEF A <3>. QED OBVIOUS <2>2. L(T \cup {x}) /\ Q(T) => <>[]R(T) OBVIOUS <2>3. <>[]R(T) /\ A(x) => <>[](R(T) /\ P(x)) BY PTL <2>4. R(T) /\ P(x) => R(T \cup {x}) OBVIOUS <2>5. <>[](R(T) /\ P(x)) => <>[]R(T \cup {x}) BY <2>4, PTL <2>. QED BY <2>1, <2>2, <2>3, <2>5 <1>. HIDE DEF Q <1>3. \A T : IsFiniteSet(T) => Q(T) BY <1>1, <1>2, FS_Induction, IsaM("blast") <1>4. Q(S) BY <1>3 <1>. QED BY <1>4 DEF Q ----------------------------------------------------------------------------- (***************************************************************************) (* Here is our proof that LiveSpec implements the specification LiveSpec *) (* of module Consensus under our refinement mapping. *) (***************************************************************************) THEOREM Liveness == LiveSpec => C!LiveSpec <1> SUFFICES ASSUME NEW Q \in Quorum, NEW b \in Ballot PROVE Spec /\ LiveAssumption!(Q, b) => C!LiveSpec BY Isa DEF LiveSpec, LiveAssumption <1>a. IsFiniteSet(Q) BY QA, AcceptorFinite, FS_Subset <1>1. C!LiveSpec <=> C!Spec /\ ([]<><>_C!vars \/ []<>(chosen # {})) BY ValueNonempty, C!LiveSpecEquals <1> DEFINE LNext == \E self \in Acceptor, c \in Ballot : /\ BallotAction(self, c) /\ (self \in Q) => (c =< b) <1>2. Spec /\ LiveAssumption!(Q, b) => [][LNext]_vars <2>1. /\ TypeOK /\ [Next]_vars /\ [\A self \in Q : \A c \in Ballot : (c > b) => ~ BallotAction(self, c)]_vars => [LNext]_vars BY NextDef DEF LNext, Ballot <2>2. /\ []TypeOK /\ [][Next]_vars /\ [][\A self \in Q : \A c \in Ballot : (c > b) => ~ BallotAction(self, c)]_vars => [][LNext]_vars BY <2>1, PTL <2>3. QED BY <2>2, VT2, Isa DEF Spec, VInv <1> DEFINE LNInv1 == \A a \in Q : maxBal[a] =< b LInv1 == VInv /\ LNInv1 <1>3. LInv1 /\ [LNext]_vars => LInv1' <2>1. SUFFICES ASSUME LInv1, [LNext]_vars PROVE LInv1' OBVIOUS <2>2. VInv' BY <2>1, NextDef, InductiveInvariance DEF LInv1, VInv <2>3. LNInv1' BY <2>1, QA DEF BallotAction, IncreaseMaxBal, VoteFor, VInv, TypeOK, vars <2>. QED BY <2>2, <2>3 <1>4. \A a \in Q : VInv /\ (maxBal[a] = b) /\ [LNext]_vars => VInv' /\ (maxBal'[a] = b) <2>1. SUFFICES ASSUME NEW a \in Q, VInv, maxBal[a] = b, [LNext]_vars PROVE VInv' /\ (maxBal'[a] = b) OBVIOUS <2>2. VInv' BY <2>1, NextDef, InductiveInvariance DEF VInv <2>3. maxBal'[a] = b BY <2>1, QA DEF BallotAction, IncreaseMaxBal, VoteFor, VInv, TypeOK, Ballot, vars <2>. QED BY <2>2, <2>3 <1>5. Spec /\ LiveAssumption!(Q, b) => <>[](\A self \in Q : maxBal[self] = b) <2>1. SUFFICES ASSUME NEW self \in Q PROVE Spec /\ LiveAssumption!(Q, b) => <>[](maxBal[self] = b) \* BY <1>a, EventuallyAlwaysForall \* doesn't check, even when introducing definitions PROOF OMITTED <2> DEFINE P == LInv1 /\ ~(maxBal[self] = b) QQ == LInv1 /\ (maxBal[self] = b) A == BallotAction(self, b) <2>2. [][LNext]_vars /\ WF_vars(A) => (LInv1 ~> QQ) <3>1. P /\ [LNext]_vars => (P' \/ QQ') BY <1>3 <3>2. P /\ <>_vars => QQ' <4>1. SUFFICES ASSUME LInv1, LNext, A PROVE QQ' OBVIOUS <4>2. LInv1' BY <4>1, <1>3 <4>3. CASE IncreaseMaxBal(self, b) BY <4>1, <4>2, <4>3, QA DEF IncreaseMaxBal, VInv, TypeOK <4>4. CASE \E v \in Value : VoteFor(self, b, v) BY <4>1, <4>2, <4>4, QA DEF VoteFor, VInv, TypeOK <4>5. QED BY <4>1, <4>3, <4>4 DEF BallotAction <3>3. P => ENABLED <>_vars <4>1. (ENABLED <>_vars) <=> \E votesp, maxBalp: /\ \/ /\ b > maxBal[self] /\ maxBalp = [maxBal EXCEPT ![self] = b] /\ votesp = votes \/ \E v \in Value : /\ maxBal[self] \leq b /\ DidNotVoteIn(self, b) /\ \A p \in Acceptor \ {self} : \A w \in Value : VotedFor(p, b, w) => (w = v) /\ SafeAt(b, v) /\ votesp = [votes EXCEPT ![self] = votes[self] \cup {<>}] /\ maxBalp = [maxBal EXCEPT ![self] = b] /\ <> # <> \* BY DEF BallotAction, IncreaseMaxBal, VoteFor, vars, SafeAt, \* DidNotVoteIn, VotedFor PROOF OMITTED <4>. SUFFICES ASSUME P PROVE \E votesp, maxBalp: /\ b > maxBal[self] /\ maxBalp = [maxBal EXCEPT ![self] = b] /\ votesp = votes /\ <> # <> BY <4>1 <4> WITNESS votes, [maxBal EXCEPT ![self] = b] <4>. QED BY QA DEF VInv, TypeOK, Ballot <3>. QED BY <3>1, <3>2, <3>3, PTL <2>3. QQ /\ [][LNext]_vars => []QQ <3>1. QQ /\ [LNext]_vars => QQ' BY <1>3, <1>4 <3>. QED BY <3>1, PTL <2>4. []QQ => [](maxBal[self] = b) BY PTL <2>5. LiveAssumption!(Q,b) => WF_vars(A) BY Isa <2>6. Spec => LInv1 <3>1. Init => VInv BY InitImpliesInv <3>2. Init => LNInv1 BY QA DEF Init, Ballot <3>. QED BY <3>1, <3>2 DEF Spec <2>. QED BY <2>2, <2>3, <2>4, <2>5, <2>6, <1>2, PTL <1> DEFINE LNInv2 == \A a \in Q : maxBal[a] = b LInv2 == VInv /\ LNInv2 <1>6. LInv2 /\ [LNext]_vars => LInv2' BY <1>4, QuorumNonEmpty <1>7. Spec /\ LiveAssumption!(Q, b) => <>[](chosen # {}) <2> DEFINE Voted(a) == \E v \in Value : VotedFor(a, b, v) <2>1. Spec /\ LiveAssumption!(Q, b) => <>[]LInv2 <3>1. Spec /\ LiveAssumption!(Q,b) => <>[]LNInv2 \* BY <1>5 \* doesn't check PROOF OMITTED <3>. QED BY <3>1, VT2, PTL <2>2. LInv2 /\ (\A a \in Q : Voted(a)) => (chosen # {}) <3>1. SUFFICES ASSUME LInv2, \A a \in Q : Voted(a) PROVE chosen # {} OBVIOUS <3>2. \E v \in Value : \A a \in Q : VotedFor(a, b, v) <4>2. PICK a0 \in Q, v \in Value : VotedFor(a0, b, v) BY <3>1, QuorumNonEmpty <4>3. ASSUME NEW a \in Q PROVE VotedFor(a, b, v) BY <3>1, <4>2, QA DEF VInv, VInv3 <4>4. QED BY <4>3 <3>3. QED BY <3>2 DEF chosen, ChosenIn <2>3. Spec /\ LiveAssumption!(Q, b) => (\A a \in Q : <>[]Voted(a)) <3>1. SUFFICES ASSUME NEW self \in Q PROVE Spec /\ LiveAssumption!(Q, b) => <>[]Voted(self) \* OBVIOUS \* doesn't check?! PROOF OMITTED <3>2. Spec /\ LiveAssumption!(Q, b) => <>Voted(self) <4>2. [][LNext]_vars /\ WF_vars(BallotAction(self, b)) => ((LInv2 /\ ~Voted(self)) ~> LInv2 /\ Voted(self)) <5> DEFINE P == LInv2 /\ ~Voted(self) QQ == LInv2 /\ Voted(self) A == BallotAction(self, b) <5>1. P /\ [LNext]_vars => (P' \/ QQ') BY <1>6 <5>2. P /\ <>_vars => QQ' <6>1. SUFFICES ASSUME P, LNext, A PROVE QQ' OBVIOUS <6>2. CASE \E v \in Value : VoteFor(self, b, v) BY <6>1, <6>2, <5>1, QA, Zenon DEF VoteFor, Voted, VotedFor, LInv2, VInv, TypeOK <6>3. CASE IncreaseMaxBal(self, b) BY <6>1, <6>3 DEF IncreaseMaxBal, Ballot <6>4. QED BY <6>1, <6>2, <6>3 DEF BallotAction <5>3. P => ENABLED <>_vars <6>1. SUFFICES ASSUME P PROVE ENABLED <>_vars OBVIOUS <6>2. (ENABLED <>_vars) <=> \E votesp, maxBalp : /\ \/ /\ b > maxBal[self] /\ maxBalp = [maxBal EXCEPT ![self] = b] /\ votesp = votes \/ \E v \in Value : /\ maxBal[self] \leq b /\ DidNotVoteIn(self, b) /\ \A p \in Acceptor \ {self} : \A w \in Value : VotedFor(p, b, w) => (w = v) /\ SafeAt(b, v) /\ votesp = [votes EXCEPT ![self] = votes[self] \cup {<>}] /\ maxBalp = [maxBal EXCEPT ![self] = b] /\ <> # <> \* BY DEF BallotAction, IncreaseMaxBal, VoteFor, vars, SafeAt, \* DidNotVoteIn, VotedFor PROOF OMITTED <6> SUFFICES \E votesp, maxBalp: /\ \E v \in Value : /\ maxBal[self] \leq b /\ DidNotVoteIn(self, b) /\ \A p \in Acceptor \ {self} : \A w \in Value : VotedFor(p, b, w) => (w = v) /\ SafeAt(b, v) /\ votesp = [votes EXCEPT ![self] = votes[self] \cup {<>}] /\ maxBalp = [maxBal EXCEPT ![self] = b] /\ <> # <> BY <6>2 <6> DEFINE someVoted == \E p \in Acceptor \ {self} : \E w \in Value : VotedFor(p, b, w) vp == CHOOSE p \in Acceptor \ {self} : \E w \in Value : VotedFor(p, b, w) vpval == CHOOSE w \in Value : VotedFor(vp, b, w) <6>3. someVoted => /\ vp \in Acceptor /\ vpval \in Value /\ VotedFor(vp, b, vpval) BY Zenon <6> DEFINE v == IF someVoted THEN vpval ELSE CHOOSE v \in Value : SafeAt(b, v) <6>4. (v \in Value) /\ SafeAt(b, v) BY <6>1, <6>3, VT4 DEF VInv, VInv2, Ballot <6> DEFINE votesp == [votes EXCEPT ![self] = votes[self] \cup {<>}] maxBalp == [maxBal EXCEPT ![self] = b] <6> WITNESS votesp, maxBalp <6> SUFFICES /\ maxBal[self] \leq b /\ DidNotVoteIn(self, b) /\ \A p \in Acceptor \ {self} : \A w \in Value : VotedFor(p, b, w) => (w = v) /\ votesp # votes BY <6>4, Zenon <6>5. maxBal[self] \leq b BY <6>1 DEF Ballot <6>6. DidNotVoteIn(self, b) BY <6>1 DEF Voted, DidNotVoteIn <6>7. ASSUME NEW p \in Acceptor \ {self}, NEW w \in Value, VotedFor(p, b, w) PROVE w = v BY <6>7, <6>3, <6>1 DEF VInv, VInv3 <6>8. votesp # votes <7>1. votesp[self] = votes[self] \cup {<>} BY <6>1, QA DEF LInv2, VInv, TypeOK <7>2. \A w \in Value : <> \notin votes[self] BY <6>6 DEF DidNotVoteIn, VotedFor <7>3. QED BY <7>1, <7>2, <6>4, Zenon <6>9. QED BY <6>5, <6>6, <6>7, <6>8, Zenon <5>4. QED BY <5>1, <5>2, <5>3, PTL <4>3. []LInv2 /\ ((LInv2 /\ ~Voted(self)) ~> LInv2 /\ Voted(self)) => <>Voted(self) BY PTL <4>4. LiveAssumption!(Q, b) => WF_vars(BallotAction(self,b)) BY Isa <4>. QED BY <1>2, <2>1, <4>2, <4>3, <4>4, PTL <3>3. Spec => [](Voted(self) => []Voted(self)) <4>1. (VInv /\ Voted(self)) /\ [Next]_vars => (VInv /\ Voted(self))' <5> SUFFICES ASSUME VInv, Voted(self), [Next]_vars PROVE VInv' /\ Voted(self)' OBVIOUS <5>1. VInv' BY InductiveInvariance <5>2. Voted(self)' <6> CASE vars' = vars BY DEF vars, Voted, VotedFor <6> CASE Next <7>2. PICK a \in Acceptor, c \in Ballot : BallotAction(a, c) BY NextDef DEF VInv <7>3. CASE IncreaseMaxBal(a, c) BY <7>3 DEF IncreaseMaxBal, Voted, VotedFor <7>4. CASE \E v \in Value : VoteFor(a, c, v) BY <7>4, QA DEF VInv, TypeOK, VoteFor, Voted, VotedFor <7>5. QED BY <7>2, <7>3, <7>4 DEF BallotAction <6> QED OBVIOUS <5>3. QED BY <5>1, <5>2 <4>3. QED BY <4>1, VT2, PTL DEF Spec <3>4. QED BY <3>2, <3>3, PTL <2>4. (\A a \in Q : <>[]Voted(a)) => <>[](\A a \in Q : Voted(a)) \* BY <1>a, EventuallyAlwaysForall \* doesn't check PROOF OMITTED <2>. QED BY <2>1, VT2, <2>2, <2>3, <2>4, PTL <1>. QED <2>1. Spec /\ LiveAssumption!(Q, b) => C!Spec /\ <>[](chosen # {}) BY VT3, <1>7, Isa <2>2. Spec /\ LiveAssumption!(Q, b) => C!Spec /\ []<>(chosen # {}) BY <2>1, PTL <2>. QED BY <2>2, <1>1, Isa =============================================================================== \* Modification History \* Last modified Fri Jul 24 18:20:31 CEST 2020 by merz \* Last modified Wed Apr 29 12:24:23 CEST 2020 by merz \* Last modified Mon May 28 08:53:38 PDT 2012 by lamport