You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 

370 lines
13 KiB

------------------- MODULE TendermintAccInv_004_draft --------------------------
(*
An inductive invariant for TendermintAcc3, which capture the forked
and non-forked cases.
* Version 3. Modular and parameterized definitions.
* Version 2. Bugfixes in the spec and an inductive invariant.
Igor Konnov, 2020.
*)
EXTENDS TendermintAcc_004_draft
(************************** TYPE INVARIANT ***********************************)
(* first, we define the sets of all potential messages *)
AllProposals ==
SetOfMsgs([type: {"PROPOSAL"},
src: AllProcs,
round: Rounds,
proposal: ValuesOrNil,
validRound: RoundsOrNil])
AllPrevotes ==
SetOfMsgs([type: {"PREVOTE"},
src: AllProcs,
round: Rounds,
id: ValuesOrNil])
AllPrecommits ==
SetOfMsgs([type: {"PRECOMMIT"},
src: AllProcs,
round: Rounds,
id: ValuesOrNil])
(* the standard type invariant -- importantly, it is inductive *)
TypeOK ==
/\ round \in [Corr -> Rounds]
/\ step \in [Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }]
/\ decision \in [Corr -> ValidValues \union {NilValue}]
/\ lockedValue \in [Corr -> ValidValues \union {NilValue}]
/\ lockedRound \in [Corr -> RoundsOrNil]
/\ validValue \in [Corr -> ValidValues \union {NilValue}]
/\ validRound \in [Corr -> RoundsOrNil]
/\ msgsPropose \in [Rounds -> SUBSET AllProposals]
/\ BenignRoundsInMessages(msgsPropose)
/\ msgsPrevote \in [Rounds -> SUBSET AllPrevotes]
/\ BenignRoundsInMessages(msgsPrevote)
/\ msgsPrecommit \in [Rounds -> SUBSET AllPrecommits]
/\ BenignRoundsInMessages(msgsPrecommit)
/\ evidence \in SUBSET (AllProposals \union AllPrevotes \union AllPrecommits)
/\ action \in {
"Init",
"InsertProposal",
"UponProposalInPropose",
"UponProposalInProposeAndPrevote",
"UponQuorumOfPrevotesAny",
"UponProposalInPrevoteOrCommitAndPrevote",
"UponQuorumOfPrecommitsAny",
"UponProposalInPrecommitNoDecision",
"OnTimeoutPropose",
"OnQuorumOfNilPrevotes",
"OnRoundCatchup"
}
(************************** INDUCTIVE INVARIANT *******************************)
EvidenceContainsMessages ==
\* evidence contains only the messages from:
\* msgsPropose, msgsPrevote, and msgsPrecommit
\A m \in evidence:
LET r == m.round
t == m.type
IN
CASE t = "PROPOSAL" -> m \in msgsPropose[r]
[] t = "PREVOTE" -> m \in msgsPrevote[r]
[] OTHER -> m \in msgsPrecommit[r]
NoFutureMessagesForLargerRounds(p) ==
\* a correct process does not send messages for the future rounds
\A r \in { rr \in Rounds: rr > round[p] }:
/\ \A m \in msgsPropose[r]: m.src /= p
/\ \A m \in msgsPrevote[r]: m.src /= p
/\ \A m \in msgsPrecommit[r]: m.src /= p
NoFutureMessagesForCurrentRound(p) ==
\* a correct process does not send messages in the future
LET r == round[p] IN
/\ Proposer[r] = p \/ \A m \in msgsPropose[r]: m.src /= p
/\ \/ step[p] \in {"PREVOTE", "PRECOMMIT", "DECIDED"}
\/ \A m \in msgsPrevote[r]: m.src /= p
/\ \/ step[p] \in {"PRECOMMIT", "DECIDED"}
\/ \A m \in msgsPrecommit[r]: m.src /= p
\* the correct processes never send future messages
AllNoFutureMessagesSent ==
\A p \in Corr:
/\ NoFutureMessagesForCurrentRound(p)
/\ NoFutureMessagesForLargerRounds(p)
\* a correct process in the PREVOTE state has sent a PREVOTE message
IfInPrevoteThenSentPrevote(p) ==
step[p] = "PREVOTE" =>
\E m \in msgsPrevote[round[p]]:
/\ m.id \in ValidValues \cup { NilValue }
/\ m.src = p
AllIfInPrevoteThenSentPrevote ==
\A p \in Corr: IfInPrevoteThenSentPrevote(p)
\* a correct process in the PRECOMMIT state has sent a PRECOMMIT message
IfInPrecommitThenSentPrecommit(p) ==
step[p] = "PRECOMMIT" =>
\E m \in msgsPrecommit[round[p]]:
/\ m.id \in ValidValues \cup { NilValue }
/\ m.src = p
AllIfInPrecommitThenSentPrecommit ==
\A p \in Corr: IfInPrecommitThenSentPrecommit(p)
\* a process in the PRECOMMIT state has sent a PRECOMMIT message
IfInDecidedThenValidDecision(p) ==
step[p] = "DECIDED" <=> decision[p] \in ValidValues
AllIfInDecidedThenValidDecision ==
\A p \in Corr: IfInDecidedThenValidDecision(p)
\* a decided process should have received a proposal on its decision
IfInDecidedThenReceivedProposal(p) ==
step[p] = "DECIDED" =>
\E r \in Rounds: \* r is not necessarily round[p]
/\ \E m \in msgsPropose[r] \intersect evidence:
/\ m.src = Proposer[r]
/\ m.proposal = decision[p]
\* not inductive: /\ m.src \in Corr => (m.validRound <= r)
AllIfInDecidedThenReceivedProposal ==
\A p \in Corr:
IfInDecidedThenReceivedProposal(p)
\* a decided process has received two-thirds of precommit messages
IfInDecidedThenReceivedTwoThirds(p) ==
step[p] = "DECIDED" =>
\E r \in Rounds:
LET PV ==
{ m \in msgsPrecommit[r] \intersect evidence: m.id = decision[p] }
IN
Cardinality(PV) >= THRESHOLD2
AllIfInDecidedThenReceivedTwoThirds ==
\A p \in Corr:
IfInDecidedThenReceivedTwoThirds(p)
\* for a round r, there is proposal by the round proposer for a valid round vr
ProposalInRound(r, proposedVal, vr) ==
\E m \in msgsPropose[r]:
/\ m.src = Proposer[r]
/\ m.proposal = proposedVal
/\ m.validRound = vr
TwoThirdsPrevotes(vr, v) ==
LET PV == { mm \in msgsPrevote[vr] \intersect evidence: mm.id = v } IN
Cardinality(PV) >= THRESHOLD2
\* if a process sends a PREVOTE, then there are three possibilities:
\* 1) the process is faulty, 2) the PREVOTE cotains Nil,
\* 3) there is a proposal in an earlier (valid) round and two thirds of PREVOTES
IfSentPrevoteThenReceivedProposalOrTwoThirds(r) ==
\A mpv \in msgsPrevote[r]:
\/ mpv.src \in Faulty
\* lockedRound and lockedValue is beyond my comprehension
\/ mpv.id = NilValue
\//\ mpv.src \in Corr
/\ mpv.id /= NilValue
/\ \/ ProposalInRound(r, mpv.id, NilRound)
\/ \E vr \in { rr \in Rounds: rr < r }:
/\ ProposalInRound(r, mpv.id, vr)
/\ TwoThirdsPrevotes(vr, mpv.id)
AllIfSentPrevoteThenReceivedProposalOrTwoThirds ==
\A r \in Rounds:
IfSentPrevoteThenReceivedProposalOrTwoThirds(r)
\* if a correct process has sent a PRECOMMIT, then there are two thirds,
\* either on a valid value, or a nil value
IfSentPrecommitThenReceivedTwoThirds ==
\A r \in Rounds:
\A mpc \in msgsPrecommit[r]:
mpc.src \in Corr =>
\/ /\ mpc.id \in ValidValues
/\ LET PV ==
{ m \in msgsPrevote[r] \intersect evidence: m.id = mpc.id }
IN
Cardinality(PV) >= THRESHOLD2
\/ /\ mpc.id = NilValue
/\ Cardinality(msgsPrevote[r]) >= THRESHOLD2
\* if a correct process has sent a precommit message in a round, it should
\* have sent a prevote
IfSentPrecommitThenSentPrevote ==
\A r \in Rounds:
\A mpc \in msgsPrecommit[r]:
mpc.src \in Corr =>
\E m \in msgsPrevote[r]:
m.src = mpc.src
\* there is a locked round if a only if there is a locked value
LockedRoundIffLockedValue(p) ==
(lockedRound[p] = NilRound) <=> (lockedValue[p] = NilValue)
AllLockedRoundIffLockedValue ==
\A p \in Corr:
LockedRoundIffLockedValue(p)
\* when a process locked a round, it must have sent a precommit on the locked value.
IfLockedRoundThenSentCommit(p) ==
lockedRound[p] /= NilRound
=> \E r \in { rr \in Rounds: rr <= round[p] }:
\E m \in msgsPrecommit[r]:
m.src = p /\ m.id = lockedValue[p]
AllIfLockedRoundThenSentCommit ==
\A p \in Corr:
IfLockedRoundThenSentCommit(p)
\* a process always locks the latest round, for which it has sent a PRECOMMIT
LatestPrecommitHasLockedRound(p) ==
LET pPrecommits ==
{mm \in UNION { msgsPrecommit[r]: r \in Rounds }: mm.src = p /\ mm.id /= NilValue }
IN
pPrecommits /= {} <: {MT}
=> LET latest ==
CHOOSE m \in pPrecommits:
\A m2 \in pPrecommits:
m2.round <= m.round
IN
/\ lockedRound[p] = latest.round
/\ lockedValue[p] = latest.id
AllLatestPrecommitHasLockedRound ==
\A p \in Corr:
LatestPrecommitHasLockedRound(p)
\* Every correct process sends only one value or NilValue.
\* This test has quantifier alternation -- a threat to all decision procedures.
\* Luckily, the sets Corr and ValidValues are small.
NoEquivocationByCorrect(r, msgs) ==
\A p \in Corr:
\E v \in ValidValues \union {NilValue}:
\A m \in msgs[r]:
\/ m.src /= p
\/ m.id = v
\* a proposer nevers sends two values
ProposalsByProposer(r, msgs) ==
\* if the proposer is not faulty, it sends only one value
\E v \in ValidValues:
\A m \in msgs[r]:
\/ m.src \in Faulty
\/ m.src = Proposer[r] /\ m.proposal = v
AllNoEquivocationByCorrect ==
\A r \in Rounds:
/\ ProposalsByProposer(r, msgsPropose)
/\ NoEquivocationByCorrect(r, msgsPrevote)
/\ NoEquivocationByCorrect(r, msgsPrecommit)
\* construct the set of the message senders
Senders(M) == { m.src: m \in M }
\* The final piece by Josef Widder:
\* if T + 1 processes precommit on the same value in a round,
\* then in the future rounds there are less than 2T + 1 prevotes for another value
PrecommitsLockValue ==
\A r \in Rounds:
\A v \in ValidValues \union {NilValue}:
\/ LET Precommits == {m \in msgsPrecommit[r]: m.id = v}
IN
Cardinality(Senders(Precommits)) < THRESHOLD1
\/ \A fr \in { rr \in Rounds: rr > r }: \* future rounds
\A w \in (ValuesOrNil) \ {v}:
LET Prevotes == {m \in msgsPrevote[fr]: m.id = w}
IN
Cardinality(Senders(Prevotes)) < THRESHOLD2
\* a combination of all lemmas
Inv ==
/\ EvidenceContainsMessages
/\ AllNoFutureMessagesSent
/\ AllIfInPrevoteThenSentPrevote
/\ AllIfInPrecommitThenSentPrecommit
/\ AllIfInDecidedThenReceivedProposal
/\ AllIfInDecidedThenReceivedTwoThirds
/\ AllIfInDecidedThenValidDecision
/\ AllLockedRoundIffLockedValue
/\ AllIfLockedRoundThenSentCommit
/\ AllLatestPrecommitHasLockedRound
/\ AllIfSentPrevoteThenReceivedProposalOrTwoThirds
/\ IfSentPrecommitThenSentPrevote
/\ IfSentPrecommitThenReceivedTwoThirds
/\ AllNoEquivocationByCorrect
/\ PrecommitsLockValue
\* this is the inductive invariant we like to check
TypedInv == TypeOK /\ Inv
\* UNUSED FOR SAFETY
ValidRoundNotSmallerThanLockedRound(p) ==
validRound[p] >= lockedRound[p]
\* UNUSED FOR SAFETY
ValidRoundIffValidValue(p) ==
(validRound[p] = NilRound) <=> (validValue[p] = NilValue)
\* UNUSED FOR SAFETY
AllValidRoundIffValidValue ==
\A p \in Corr: ValidRoundIffValidValue(p)
\* if validRound is defined, then there are two-thirds of PREVOTEs
IfValidRoundThenTwoThirds(p) ==
\/ validRound[p] = NilRound
\/ LET PV == { m \in msgsPrevote[validRound[p]]: m.id = validValue[p] } IN
Cardinality(PV) >= THRESHOLD2
\* UNUSED FOR SAFETY
AllIfValidRoundThenTwoThirds ==
\A p \in Corr: IfValidRoundThenTwoThirds(p)
\* a valid round can be only set to a valid value that was proposed earlier
IfValidRoundThenProposal(p) ==
\/ validRound[p] = NilRound
\/ \E m \in msgsPropose[validRound[p]]:
m.proposal = validValue[p]
\* UNUSED FOR SAFETY
AllIfValidRoundThenProposal ==
\A p \in Corr: IfValidRoundThenProposal(p)
(******************************** THEOREMS ***************************************)
(* Under this condition, the faulty processes can decide alone *)
FaultyQuorum == Cardinality(Faulty) >= THRESHOLD2
(* The standard condition of the Tendermint security model *)
LessThanThirdFaulty == N > 3 * T /\ Cardinality(Faulty) <= T
(*
TypedInv is an inductive invariant, provided that there is no faulty quorum.
We run Apalache to prove this theorem only for fixed instances of 4 to 10 processes.
(We run Apalache manually, as it does not parse theorem statements at the moment.)
To get a parameterized argument, one has to use a theorem prover, e.g., TLAPS.
*)
THEOREM TypedInvIsInductive ==
\/ FaultyQuorum \* if there are 2 * T + 1 faulty processes, we give up
\//\ Init => TypedInv
/\ TypedInv /\ [Next]_vars => TypedInv'
(*
There should be no fork, when there are less than 1/3 faulty processes.
*)
THEOREM AgreementWhenLessThanThirdFaulty ==
LessThanThirdFaulty /\ TypedInv => Agreement
(*
In a more general case, when there are less than 2/3 faulty processes,
there is either Agreement (no fork), or two scenarios exist:
equivocation by Faulty, or amnesia by Faulty.
*)
THEOREM AgreementOrFork ==
~FaultyQuorum /\ TypedInv => Accountability
=============================================================================