mirror of
https://github.com/tendermint/tendermint.git
synced 2026-01-12 07:42:48 +00:00
Compare commits
8 Commits
sam/abci++
...
igor/tende
| Author | SHA1 | Date | |
|---|---|---|---|
|
7f14e3200a | ||
|
|
3ec96cf44c | ||
|
|
31b8021672 | ||
|
|
e15483dcc6 | ||
|
|
3ea3515fea | ||
|
|
7886f520c5 | ||
|
|
945d9a7eec | ||
|
|
8737003f94 |
@@ -1,5 +1,5 @@
|
||||
---------------------- MODULE MC_n4_f2_amnesia -------------------------------
|
||||
EXTENDS Sequences
|
||||
EXTENDS Sequences, typedefs
|
||||
|
||||
CONSTANT
|
||||
\* @type: $round -> $process;
|
||||
|
||||
@@ -306,3 +306,306 @@ Note that detecting this behavior require application knowledge. Detecting this
|
||||
referring to the block before the one in which height happen.
|
||||
|
||||
**Q:** can we say that in this case a validator declines to check if a proposed value is valid before voting for it?
|
||||
|
||||
## Specification and verification
|
||||
|
||||
### Specification in TLA+
|
||||
|
||||
We have written a specification of Tendermint consensus, following the
|
||||
pseudo-code of [BKM19][]. This specification is written for safety of
|
||||
consensus, e.g., for checking the safety property called [Agreement][], which
|
||||
says that no two processes can decide differently. As we were interested in
|
||||
accountability, we have extended the specification as follows:
|
||||
|
||||
- We have added ghost variables that keep track of the evidence collected by
|
||||
the correct validators: `evidencePropose`, `evidencePrevote`, and
|
||||
`evidencePrecommit`. Note that these evidence variables are global, so we
|
||||
do not fix an algorithm for collecting evidence in the specification.
|
||||
|
||||
- We have added the safety property [Accountability][] that requires the
|
||||
evidence to contain messages from at least `T + 1` validators, when
|
||||
[Agreement][] is violated.
|
||||
|
||||
The specification is organized in the following files:
|
||||
|
||||
- [TendermintAcc_004_draft.tla][] is the main file that contains the
|
||||
protocol specification.
|
||||
|
||||
- [typedefs.tla][] contains auxiliary type definitions for [Apalache][].
|
||||
|
||||
- [TendermintAccInv_004_draft.tla][] contains an inductive invariant
|
||||
for proving safety of unbounded executions with [Apalache][].
|
||||
|
||||
- [TendermintAccTrace_004_draft.tla][] contains an auxiliary module
|
||||
that lets one execute a predefined sequence of actions (without specifying
|
||||
concrete inputs for every action).
|
||||
|
||||
|
||||
### Model checking
|
||||
|
||||
We have checked the safety properties [Agreement][] and [Accountability][]
|
||||
with the symbolic model checker [Apalache][] v0.27.0. As Apalache works on
|
||||
bounded data structures, we have introduced several instances of the
|
||||
specification:
|
||||
|
||||
- [MC_n4_f1.tla][], [MC_n4_f2.tla][], and [MC_n4_f3.tla][] define instances
|
||||
of four validators, of which one, two, and three validators are faulty,
|
||||
respectively.
|
||||
|
||||
- [MC_n5_f1.tla][] and [MC_n5_f2.tla][] define instances of five validators,
|
||||
of which one and two validators are faulty, respectively.
|
||||
|
||||
- [MC_n6_f1.tla][] defines the instance of six validators, of which one is
|
||||
faulty.
|
||||
|
||||
- [MC_n4_f2_amnesia.tla][] defines the instance of four validators, of which
|
||||
two are faulty. This model demonstrates an execution, in which the faulty
|
||||
validators exercise the amnesia attack.
|
||||
|
||||
If you want to reproduce the model checking runs, check the [Installation][]
|
||||
and [Running Apalache][] pages first.
|
||||
|
||||
#### Evidence of an amnesia attack
|
||||
|
||||
In this run, we fix the trace of actions, in order to quickly violate
|
||||
`Agreement`. For details, check the [MC_n4_f2_amnesia.tla][] model.
|
||||
We ran Apalache as follows:
|
||||
|
||||
```sh
|
||||
$ apalache-mc check --cinit=ConstInit \
|
||||
--init=TraceInit --next=TraceNext --inv=Agreement MC_n4_f2_amnesia.tla
|
||||
...
|
||||
Found 1 error(s)
|
||||
...
|
||||
Total time: 10.416 sec
|
||||
```
|
||||
|
||||
The trace `violation1.tla` contains a concrete execution of the protocol
|
||||
that leads to `State7`, in which two validators decide differently
|
||||
(this is expected behavior for `N=4` and `F=2`):
|
||||
|
||||
```tla
|
||||
State7 ==
|
||||
...
|
||||
/\ decision = SetAsFun({ <<"c1", "v0">>, <<"c2", "v1">> })
|
||||
...
|
||||
/\ step = SetAsFun({ <<"c1", "DECIDED">>, <<"c2", "DECIDED">> })
|
||||
...
|
||||
```
|
||||
|
||||
By inspecting the evidence, we can see that the correct validators have
|
||||
collected an evidence of the amnesia attack by the two faulty processes:
|
||||
|
||||
```tla
|
||||
State7 ==
|
||||
...
|
||||
/\ evidencePrevote
|
||||
= { [id |-> "v0", round |-> 2, src |-> "c1", type |-> "PREVOTE"],
|
||||
[id |-> "v0", round |-> 2, src |-> "f3", type |-> "PREVOTE"],
|
||||
[id |-> "v0", round |-> 2, src |-> "f4", type |-> "PREVOTE"],
|
||||
[id |-> "v1", round |-> 0, src |-> "c2", type |-> "PREVOTE"],
|
||||
[id |-> "v1", round |-> 0, src |-> "f3", type |-> "PREVOTE"],
|
||||
[id |-> "v1", round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
|
||||
/\ evidencePrecommit
|
||||
= { [id |-> "v0", round |-> 2, src |-> "c1", type |-> "PRECOMMIT"],
|
||||
[id |-> "v0", round |-> 2, src |-> "f3", type |-> "PRECOMMIT"],
|
||||
[id |-> "v0", round |-> 2, src |-> "f4", type |-> "PRECOMMIT"],
|
||||
[id |-> "v1", round |-> 0, src |-> "c2", type |-> "PRECOMMIT"],
|
||||
[id |-> "v1", round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
|
||||
[id |-> "v1", round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
|
||||
...
|
||||
```
|
||||
|
||||
#### Violation of Agreement when 2 out of 4 validators are faulty
|
||||
|
||||
To quickly get an example of `Agreement` violation for the case of two out of
|
||||
four validators being faulty (this is expected behavior), we run symbolic
|
||||
execution:
|
||||
|
||||
```sh
|
||||
$ apalache-mc simulate --cinit=ConstInit --no-deadlock \
|
||||
--inv=Agreement --length=20 MC_n4_f2.tla
|
||||
...
|
||||
Found 1 error(s)
|
||||
...
|
||||
It took me 0 days 0 hours 3 min 43 sec
|
||||
```
|
||||
|
||||
The trace `violation1.tla` contains a concrete execution of the protocol
|
||||
that leads to `State7`, in which two validators decide differently
|
||||
(this is expected behavior for `N=4` and `F=2`):
|
||||
|
||||
```tla
|
||||
State18 ==
|
||||
...
|
||||
/\ decision = SetAsFun({ <<"c1", "v1">>, <<"c2", "v0">> })
|
||||
...
|
||||
/\ step = SetAsFun({ <<"c1", "DECIDED">>, <<"c2", "DECIDED">> })
|
||||
...
|
||||
```
|
||||
|
||||
With symbolic execution, the run times may vary significantly, as Apalache
|
||||
is randomly choosing actions to try. To get an example for sure, we run
|
||||
bounded model checking:
|
||||
|
||||
```sh
|
||||
$ apalache-mc check --cinit=ConstInit \
|
||||
--inv=Agreement MC_n4_f2.tla
|
||||
...
|
||||
Found 1 error(s)
|
||||
...
|
||||
It took me 0 days 0 hours 56 min 38 sec
|
||||
```
|
||||
|
||||
This usually takes longer than randomized symbolic execution, as bounded model
|
||||
checking checks **all** symbolic executions up to the given length, as
|
||||
opposite to a **fixed number** of symbolic executions.
|
||||
|
||||
#### Agreement holds true when 1 out of 4 validators is faulty
|
||||
|
||||
In case when only one of the four validators is faulty, we expect `Agreement`
|
||||
to hold true. Before trying to prove it, we can quickly check that it does
|
||||
hold true for 100 symbolic executions, each having up to 10 steps:
|
||||
|
||||
```sh
|
||||
$ apalache-mc simulate --cinit=ConstInit --inv=Agreement \
|
||||
--length=10 MC_n4_f1.tla
|
||||
...
|
||||
It took me 0 days 0 hours 2 min 54 sec
|
||||
```
|
||||
|
||||
To get a better guarantee that `Agreement` holds true for all executions
|
||||
that contain up to 10 steps, we run bounded model checking:
|
||||
|
||||
|
||||
```sh
|
||||
$ apalache-mc check --cinit=ConstInit \
|
||||
--inv=Agreement --length=10 MC_n4_f1.tla
|
||||
...
|
||||
Checker reports no error up to computation length 10
|
||||
...
|
||||
It took me 0 days 21 hours 8 min 48 sec
|
||||
```
|
||||
|
||||
Finally, to prove that `Agreement` holds true for arbitrarily long executions,
|
||||
we show that `TypedInv` is an inductive invariant of the specification. For
|
||||
details, see [Checking inductive invariants][].
|
||||
|
||||
Proving that `TypedInv` is inductive and using it to show `Agreement` requires
|
||||
three steps.
|
||||
|
||||
First, we check that the initial states satisfy `TypedInv` (the induction base):
|
||||
|
||||
```sh
|
||||
$ apalache-mc check --cinit=ConstInit --init=TypedInv \
|
||||
--inv=Init MC_n4_f1.tla
|
||||
...
|
||||
The outcome is: NoError
|
||||
...
|
||||
It took me 0 days 0 hours 0 min 8 sec
|
||||
```
|
||||
|
||||
Second, we show the inductive step:
|
||||
|
||||
```sh
|
||||
$ apalache-mc check --cinit=ConstInit \
|
||||
--init=TypedInv --inv=TypedInv \
|
||||
--length=1 MC_n4_f1.tla
|
||||
...
|
||||
The outcome is: NoError
|
||||
...
|
||||
It took me 0 days 3 hours 46 min 13 sec
|
||||
```
|
||||
|
||||
Third, we show that `Agreement` holds in the states, where `TypedInv` holds
|
||||
true:
|
||||
|
||||
```sh
|
||||
$ apalache-mc check --cinit=ConstInit \
|
||||
--init=TypedInv --inv=Agreement --length=0 MC_n4_f1.tla
|
||||
...
|
||||
The outcome is: NoError
|
||||
...
|
||||
It took me 0 days 0 hours 6 min 50 sec
|
||||
```
|
||||
|
||||
Interestingly, this proof is faster (and more complete) than bounded model
|
||||
checking up to 10 steps. However, it requires an additional predicate
|
||||
`TypedInv`.
|
||||
|
||||
#### Accountability holds true when 1 out of 4 validators is faulty
|
||||
|
||||
As we have proven that `TypedInv` is inductive in the previous step, we use it
|
||||
to show that `Accountability` holds for arbitrarily long executions:
|
||||
|
||||
```sh
|
||||
$ apalache-mc check --cinit=ConstInit --init=TypedInv \
|
||||
--inv=Accountability --length=0 MC_n4_f1.tla
|
||||
...
|
||||
The outcome is: NoError
|
||||
...
|
||||
It took me 0 days 0 hours 7 min 49 sec
|
||||
```
|
||||
|
||||
This case of `Accountability` is not that interesting, as `Agreement` holds
|
||||
true, and `Agreement` is a part of accountability.
|
||||
|
||||
#### Accountability holds true when 2 out of 4 validators are faulty
|
||||
|
||||
Similar to how we have proven the inductiveness of `TypedInv` on
|
||||
`MC_n4_f1.tla`, we show that `TypedInv` is inductive on `MC_n4_f2.tla` too:
|
||||
|
||||
```
|
||||
$ apalache-mc check --cinit=ConstInit --init=TypedInv \
|
||||
--inv=Init MC_n4_f2.tla
|
||||
...
|
||||
The outcome is: NoError
|
||||
...
|
||||
$ apalache-mc check --cinit=ConstInit \
|
||||
--init=TypedInv --inv=TypedInv --length=1 MC_n4_f2.tla
|
||||
...
|
||||
The outcome is: NoError
|
||||
...
|
||||
```
|
||||
|
||||
As we have proven that `TypedInv` is inductive, we use it to show that
|
||||
`Accountability` holds for arbitrarily long executions, even if the number of
|
||||
faults is over $\frac{1}{3}$ (but below $\frac{2}{3}$):
|
||||
|
||||
```sh
|
||||
$ apalache-mc check --cinit=ConstInit --init=TypedInv \
|
||||
--inv=Accountability --length=0 MC_n4_f2.tla
|
||||
...
|
||||
The outcome is: NoError
|
||||
...
|
||||
It took me 0 days 0 hours 14 min 17 sec
|
||||
```
|
||||
|
||||
#### Other instances
|
||||
|
||||
The instances [MC_n4_f3.tla][], [MC_n5_f1.tla][], [MC_n5_f2.tla][],
|
||||
and [MC_n6_f1.tla][] were checked similar to how we did it
|
||||
for [MC_n4_f1.tla][] and [MC_n4_f2.tla][].
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
[BKM19]: https://arxiv.org/abs/1807.04938
|
||||
[Apalache]: https://github.com/informalsystems/apalache
|
||||
[TendermintAcc_004_draft.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/TendermintAcc_004_draft.tla
|
||||
[typedefs.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/typedefs.tla
|
||||
[TendermintAccInv_004_draft.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/TendermintAccInv_004_draft.tla
|
||||
[TendermintAccTrace_004_draft.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/TendermintAccTrace_004_draft.tla
|
||||
[MC_n4_f1.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n4_f1.tla
|
||||
[MC_n4_f2.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n4_f2.tla
|
||||
[MC_n4_f2_amnesia.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n4_f2.tla
|
||||
[MC_n4_f3.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n4_f3.tla
|
||||
[MC_n5_f1.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n5_f1.tla
|
||||
[MC_n5_f2.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n5_f2.tla
|
||||
[MC_n6_f1.tla]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/accountability/MC_n6_f1.tla
|
||||
[Installation]: https://apalache.informal.systems/docs/apalache/installation/index.html
|
||||
[Running Apalache]: https://apalache.informal.systems/docs/apalache/running.html
|
||||
[Checking inductive invariants]: https://apalache.informal.systems/docs/apalache/running.html#15-checking-an-inductive-invariant
|
||||
[Accountability]: https://github.com/tendermint/tendermint/blob/c8302c5fcb7f1ffafdefc5014a26047df1d27c99/spec/light-client/accountability/TendermintAcc_004_draft.tla#L545-L550
|
||||
[Agreement]: https://github.com/tendermint/tendermint/blob/c8302c5fcb7f1ffafdefc5014a26047df1d27c99/spec/light-client/accountability/TendermintAcc_004_draft.tla#L530-L534
|
||||
|
||||
@@ -3,16 +3,19 @@
|
||||
An inductive invariant for TendermintAcc3, which capture the forked
|
||||
and non-forked cases.
|
||||
|
||||
* Version 4. Fix the inductive invariant,
|
||||
* as violations were found by Apalache v0.27.
|
||||
* Version 3. Modular and parameterized definitions.
|
||||
* Version 2. Bugfixes in the spec and an inductive invariant.
|
||||
|
||||
Igor Konnov, 2020.
|
||||
Igor Konnov, Josef Widder, 2020-2022.
|
||||
*)
|
||||
|
||||
EXTENDS TendermintAcc_004_draft
|
||||
|
||||
(************************** TYPE INVARIANT ***********************************)
|
||||
(* first, we define the sets of all potential messages *)
|
||||
\* @type: Set($proposeMsg);
|
||||
AllProposals ==
|
||||
[type: {"PROPOSAL"},
|
||||
src: AllProcs,
|
||||
@@ -20,12 +23,14 @@ AllProposals ==
|
||||
proposal: ValuesOrNil,
|
||||
validRound: RoundsOrNil]
|
||||
|
||||
\* @type: Set($preMsg);
|
||||
AllPrevotes ==
|
||||
[type: {"PREVOTE"},
|
||||
src: AllProcs,
|
||||
round: Rounds,
|
||||
id: ValuesOrNil]
|
||||
|
||||
\* @type: Set($preMsg);
|
||||
AllPrecommits ==
|
||||
[type: {"PRECOMMIT"},
|
||||
src: AllProcs,
|
||||
@@ -66,8 +71,8 @@ TypeOK ==
|
||||
|
||||
(************************** INDUCTIVE INVARIANT *******************************)
|
||||
EvidenceContainsMessages ==
|
||||
\* evidence contains only the messages from:
|
||||
\* msgsPropose, msgsPrevote, and msgsPrecommit
|
||||
\* evidence contains only the messages from:
|
||||
\* msgsPropose, msgsPrevote, and msgsPrecommit
|
||||
/\ \A m \in evidencePropose:
|
||||
m \in msgsPropose[m.round]
|
||||
/\ \A m \in evidencePrevote:
|
||||
@@ -154,7 +159,7 @@ AllIfInDecidedThenReceivedTwoThirds ==
|
||||
|
||||
\* 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]:
|
||||
\E m \in msgsPropose[r] \intersect evidencePropose:
|
||||
/\ m.src = Proposer[r]
|
||||
/\ m.proposal = proposedVal
|
||||
/\ m.validRound = vr
|
||||
@@ -164,18 +169,25 @@ TwoThirdsPrevotes(vr, v) ==
|
||||
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
|
||||
\* 1) the process is faulty,
|
||||
\* 2) the PREVOTE contains Nil,
|
||||
\* 3) a) there is a proposal in an earlier (valid) round,
|
||||
\* b) there are two thirds of PREVOTES in that round.
|
||||
IfSentPrevoteThenReceivedProposalOrTwoThirds(r) ==
|
||||
\A mpv \in msgsPrevote[r]:
|
||||
\* case 1
|
||||
\/ mpv.src \in Faulty
|
||||
\* lockedRound and lockedValue is beyond my comprehension
|
||||
\* case 2
|
||||
\/ mpv.id = NilValue
|
||||
\* case 3
|
||||
\//\ mpv.src \in Corr
|
||||
/\ mpv.id /= NilValue
|
||||
/\ \/ ProposalInRound(r, mpv.id, NilRound)
|
||||
\/ \E vr \in { rr \in Rounds: rr < r }:
|
||||
\/ \E vr \in Rounds:
|
||||
\* condition 3a
|
||||
/\ vr < r
|
||||
/\ ProposalInRound(r, mpv.id, vr)
|
||||
\* condition 3b
|
||||
/\ TwoThirdsPrevotes(vr, mpv.id)
|
||||
|
||||
AllIfSentPrevoteThenReceivedProposalOrTwoThirds ==
|
||||
@@ -188,14 +200,14 @@ 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 evidencePrevote: m.id = mpc.id
|
||||
}
|
||||
IN
|
||||
Cardinality(PV) >= THRESHOLD2
|
||||
\/ /\ mpc.id = NilValue
|
||||
/\ Cardinality(msgsPrevote[r]) >= THRESHOLD2
|
||||
\/ /\ mpc.id \in ValidValues
|
||||
/\ LET PV == {
|
||||
m \in msgsPrevote[r] \intersect evidencePrevote: m.id = mpc.id
|
||||
}
|
||||
IN
|
||||
Cardinality(PV) >= THRESHOLD2
|
||||
\/ /\ mpc.id = NilValue
|
||||
/\ Cardinality(msgsPrevote[r] \intersect evidencePrevote) >= THRESHOLD2
|
||||
|
||||
\* if a correct process has sent a precommit message in a round, it should
|
||||
\* have sent a prevote
|
||||
@@ -227,15 +239,17 @@ AllIfLockedRoundThenSentCommit ==
|
||||
|
||||
\* 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 }
|
||||
LET pPrecommits == {
|
||||
mm \in UNION { msgsPrecommit[r]: r \in Rounds }:
|
||||
mm.src = p /\ mm.id /= NilValue
|
||||
}
|
||||
IN
|
||||
pPrecommits /= {}
|
||||
=> LET latest ==
|
||||
CHOOSE m \in pPrecommits:
|
||||
\A m2 \in pPrecommits:
|
||||
m2.round <= m.round
|
||||
IN
|
||||
IN
|
||||
/\ lockedRound[p] = latest.round
|
||||
/\ lockedValue[p] = latest.id
|
||||
|
||||
@@ -246,6 +260,7 @@ AllLatestPrecommitHasLockedRound ==
|
||||
\* 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.
|
||||
\*
|
||||
\* @type: ($round, $round -> Set($preMsg)) => Bool;
|
||||
NoEquivocationByCorrect(r, msgs) ==
|
||||
\A p \in Corr:
|
||||
@@ -273,20 +288,79 @@ AllNoEquivocationByCorrect ==
|
||||
\* @type: (Set({ src: $process, a })) => Set($process);
|
||||
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
|
||||
\* A crucial lemma 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 v \in ValidValues:
|
||||
\/ LET Precommits == {
|
||||
m \in msgsPrecommit[r] \intersect evidencePrecommit:
|
||||
m.id = v /\ m.src \in Corr
|
||||
}
|
||||
IN
|
||||
Cardinality(Senders(Precommits)) < THRESHOLD1
|
||||
\/ \A fr \in Rounds, w \in Values:
|
||||
LET Prevotes == {
|
||||
m \in msgsPrevote[fr] \intersect evidencePrevote: m.id = w
|
||||
} IN
|
||||
(fr > r /\ w /= v) => (Cardinality(Senders(Prevotes)) < THRESHOLD2)
|
||||
|
||||
\* Another lemma by Josef Widder:
|
||||
\* If a correct process precommits and locks a value,
|
||||
\* it can later prevote on another value, only if it has seen 2T + 1 prevotes.
|
||||
RelockValueIfEnoughPrevotes ==
|
||||
\A r1, r2 \in Rounds, p \in Corr, v1, v2 \in ValidValues:
|
||||
LET m1 == [ type |-> "PRECOMMIT", src |-> p, id |-> v1, round |-> r1 ] IN
|
||||
LET m2 == [ type |-> "PREVOTE", src |-> p, id |-> v2, round |-> r2 ] IN
|
||||
LET RelockedValue ==
|
||||
/\ r1 < r2
|
||||
/\ v1 /= v2
|
||||
/\ m1 \in msgsPrecommit[r1]
|
||||
/\ m2 \in msgsPrevote[r2]
|
||||
IN
|
||||
LET EnoughPrevotesInMiddle ==
|
||||
\E vr \in Rounds:
|
||||
/\ r1 <= vr /\ vr <= r2
|
||||
\* count prevotes in the middle round, excluding p
|
||||
/\ LET Prevotes == {
|
||||
m \in msgsPrevote[vr] \intersect evidencePrevote:
|
||||
m.id = v2 /\ (m.src /= p \/ vr < r2)
|
||||
}
|
||||
IN
|
||||
/\ Cardinality(Prevotes) >= THRESHOLD2
|
||||
\* this majority must be backed by a proposal!
|
||||
/\ LET proposal == [
|
||||
type |-> "PROPOSE", src |-> Proposer[r2], round |-> r2,
|
||||
proposal |-> v2, validRound |-> vr
|
||||
] IN
|
||||
proposal \in msgsPropose[r2]
|
||||
IN
|
||||
RelockedValue => EnoughPrevotesInMiddle
|
||||
|
||||
\* if validRound is defined, then there are two-thirds of PREVOTEs
|
||||
AllIfValidRoundThenTwoThirds ==
|
||||
\A p \in Corr:
|
||||
LET vr == validRound[p] IN
|
||||
\/ vr = NilRound /\ validValue[p] = NilValue
|
||||
\/ LET PV == {
|
||||
m \in msgsPrevote[vr] \intersect evidencePrevote:
|
||||
m.id = validValue[p]
|
||||
} IN
|
||||
Cardinality(PV) >= THRESHOLD2
|
||||
|
||||
AllValidAndLocked ==
|
||||
\A p \in Corr:
|
||||
/\ validRound[p] >= lockedRound[p]
|
||||
/\ validRound[p] /= NilRound <=> validValue[p] /= NilValue
|
||||
/\ lockedValue[p] /= NilValue => validValue[p] /= NilValue
|
||||
|
||||
\* a valid round can be only set to a valid value that was proposed earlier
|
||||
AllIfValidRoundThenProposal ==
|
||||
\A p \in Corr:
|
||||
\/ validRound[p] = NilRound
|
||||
\/ \E m \in msgsPropose[validRound[p]] \intersect evidencePropose:
|
||||
m.proposal = validValue[p]
|
||||
|
||||
\* a combination of all lemmas
|
||||
Inv ==
|
||||
@@ -304,44 +378,16 @@ Inv ==
|
||||
/\ IfSentPrecommitThenSentPrevote
|
||||
/\ IfSentPrecommitThenReceivedTwoThirds
|
||||
/\ AllNoEquivocationByCorrect
|
||||
/\ RelockValueIfEnoughPrevotes
|
||||
/\ AllIfValidRoundThenTwoThirds
|
||||
/\ AllValidAndLocked
|
||||
/\ AllIfValidRoundThenProposal
|
||||
/\ 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 ***************************************)
|
||||
(******************************** THEOREMS ************************************)
|
||||
(* Under this condition, the faulty processes can decide alone *)
|
||||
FaultyQuorum == Cardinality(Faulty) >= THRESHOLD2
|
||||
|
||||
|
||||
@@ -23,7 +23,7 @@ VARIABLE
|
||||
|
||||
TraceInit ==
|
||||
/\ toReplay = Trace
|
||||
/\ action' := "Init"
|
||||
/\ action = "Init"
|
||||
/\ Init
|
||||
|
||||
TraceNext ==
|
||||
@@ -31,7 +31,7 @@ TraceNext ==
|
||||
/\ toReplay' = Tail(toReplay)
|
||||
\* Here is the trick. We restrict the action to the expected one,
|
||||
\* so the other actions will be pruned
|
||||
/\ action' := Head(toReplay)
|
||||
/\ action' = Head(toReplay)
|
||||
/\ Next
|
||||
|
||||
================================================================================
|
||||
|
||||
@@ -382,7 +382,8 @@ UponQuorumOfPrecommitsAny(p) ==
|
||||
LET Committers == { m.src: m \in MyEvidence } IN
|
||||
\* compare the number of the unique committers against the threshold
|
||||
/\ Cardinality(Committers) >= THRESHOLD2 \* line 47
|
||||
/\ evidencePrecommit' = MyEvidence \union evidencePrecommit
|
||||
\*/\ evidencePrecommit' = MyEvidence \union evidencePrecommit
|
||||
/\ UNCHANGED evidencePrecommit
|
||||
/\ round[p] + 1 \in Rounds
|
||||
/\ StartRound(p, round[p] + 1)
|
||||
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
|
||||
@@ -434,7 +435,8 @@ OnQuorumOfNilPrevotes(p) ==
|
||||
/\ step[p] = "PREVOTE"
|
||||
/\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(NilValue) } IN
|
||||
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
|
||||
/\ evidencePrevote' = PV \union evidencePrevote
|
||||
\*/\ evidencePrevote' = PV \union evidencePrevote
|
||||
/\ UNCHANGED evidencePrevote
|
||||
/\ BroadcastPrecommit(p, round[p], Id(NilValue))
|
||||
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
|
||||
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
|
||||
@@ -455,9 +457,10 @@ OnRoundCatchup(p) ==
|
||||
Src(EvPropose) \union Src(EvPrevote) \union Src(EvPrecommit)
|
||||
IN
|
||||
/\ Cardinality(Faster) >= THRESHOLD1
|
||||
/\ evidencePropose' = EvPropose \union evidencePropose
|
||||
/\ evidencePrevote' = EvPrevote \union evidencePrevote
|
||||
/\ evidencePrecommit' = EvPrecommit \union evidencePrecommit
|
||||
/\ UNCHANGED <<evidencePropose, evidencePrevote, evidencePrecommit>>
|
||||
\*/\ evidencePropose' = EvPropose \union evidencePropose
|
||||
\*/\ evidencePrevote' = EvPrevote \union evidencePrevote
|
||||
\*/\ evidencePrecommit' = EvPrecommit \union evidencePrecommit
|
||||
/\ StartRound(p, r)
|
||||
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
|
||||
validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
|
||||
@@ -494,7 +497,6 @@ EquivocationBy(p) ==
|
||||
/\ m1.src = p
|
||||
/\ m2.src = p
|
||||
/\ m1.round = m2.round
|
||||
/\ m1.type = m2.type
|
||||
IN
|
||||
\/ EquivocationIn(evidencePropose)
|
||||
\/ EquivocationIn(evidencePrevote)
|
||||
@@ -519,8 +521,12 @@ AmnesiaBy(p) ==
|
||||
id |-> Id(v2)
|
||||
] \in evidencePrevote
|
||||
/\ \A r \in { rnd \in Rounds: r1 <= rnd /\ rnd < r2 }:
|
||||
LET prevotes ==
|
||||
{ m \in evidencePrevote: m.round = r /\ m.id = Id(v2) }
|
||||
LET prevotes == {
|
||||
m \in evidencePrevote:
|
||||
/\ m.round = r
|
||||
/\ m.id = Id(v2)
|
||||
/\ m.src /= p
|
||||
}
|
||||
IN
|
||||
Cardinality(prevotes) < THRESHOLD2
|
||||
|
||||
|
||||
@@ -1,11 +1,18 @@
|
||||
-------------------- MODULE typedefs ---------------------------
|
||||
(*
|
||||
// the process type
|
||||
@typeAlias: process = Str;
|
||||
// the value type
|
||||
@typeAlias: value = Str;
|
||||
// the type of step labels
|
||||
@typeAlias: step = Str;
|
||||
// the type of round numbers
|
||||
@typeAlias: round = Int;
|
||||
// the type of action labels
|
||||
@typeAlias: action = Str;
|
||||
// the type of action traces
|
||||
@typeAlias: trace = Seq(Str);
|
||||
// the type of PROPOSE messages
|
||||
@typeAlias: proposeMsg =
|
||||
{
|
||||
type: $step,
|
||||
@@ -14,6 +21,7 @@
|
||||
proposal: $value,
|
||||
validRound: $round
|
||||
};
|
||||
// the type of PRECOMMIT messages
|
||||
@typeAlias: preMsg =
|
||||
{
|
||||
type: $step,
|
||||
|
||||
Reference in New Issue
Block a user