mirror of
https://github.com/tendermint/tendermint.git
synced 2026-01-10 23:10:59 +00:00
Update type annotations in the TLA+ spec of Tendermint for accountability (#9263)
* update Apalache type annotations and split evidence into 3 variables * remove the duplicate of AllPrevotes, due to merge
This commit is contained in:
Igor Konnov
GitHub
@@ -1,34 +1,38 @@
|
||||
----------------------------- MODULE MC_n4_f1 -------------------------------
|
||||
CONSTANT
|
||||
\* @type: ROUND -> PROCESS;
|
||||
CONSTANT
|
||||
\* @type: $round -> $process;
|
||||
Proposer
|
||||
|
||||
\* the variables declared in TendermintAcc3
|
||||
VARIABLES
|
||||
\* @type: PROCESS -> ROUND;
|
||||
round,
|
||||
\* @type: PROCESS -> STEP;
|
||||
step,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
decision,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
lockedValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
lockedRound,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
validValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
validRound,
|
||||
\* @type: ROUND -> Set(PROPMESSAGE);
|
||||
msgsPropose,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrevote,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrecommit,
|
||||
\* @type: Set(MESSAGE);
|
||||
evidence,
|
||||
\* @type: ACTION;
|
||||
action
|
||||
\* @type: $process -> $round;
|
||||
round, \* a process round number: Corr -> Rounds
|
||||
\* @type: $process -> $step;
|
||||
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
|
||||
\* @type: $process -> $value;
|
||||
decision, \* process decision: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $value;
|
||||
lockedValue, \* a locked value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
lockedRound, \* a locked round: Corr -> RoundsOrNil
|
||||
\* @type: $process -> $value;
|
||||
validValue, \* a valid value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
validRound, \* a valid round: Corr -> RoundsOrNil
|
||||
\* @type: $round -> Set($proposeMsg);
|
||||
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: Set($proposeMsg);
|
||||
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
|
||||
\* @type: $action;
|
||||
action \* we use this variable to see which action was taken
|
||||
|
||||
INSTANCE TendermintAccDebug_004_draft WITH
|
||||
Corr <- {"c1", "c2", "c3"},
|
||||
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
|
||||
ConstInit == \* the proposer is arbitrary -- works for safety
|
||||
Proposer \in [Rounds -> AllProcs]
|
||||
|
||||
=============================================================================
|
||||
=============================================================================
|
||||
|
||||
@@ -1,34 +1,38 @@
|
||||
----------------------------- MODULE MC_n4_f2 -------------------------------
|
||||
CONSTANT
|
||||
\* @type: ROUND -> PROCESS;
|
||||
CONSTANT
|
||||
\* @type: $round -> $process;
|
||||
Proposer
|
||||
|
||||
\* the variables declared in TendermintAcc3
|
||||
VARIABLES
|
||||
\* @type: PROCESS -> ROUND;
|
||||
round,
|
||||
\* @type: PROCESS -> STEP;
|
||||
step,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
decision,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
lockedValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
lockedRound,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
validValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
validRound,
|
||||
\* @type: ROUND -> Set(PROPMESSAGE);
|
||||
msgsPropose,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrevote,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrecommit,
|
||||
\* @type: Set(MESSAGE);
|
||||
evidence,
|
||||
\* @type: ACTION;
|
||||
action
|
||||
\* @type: $process -> $round;
|
||||
round, \* a process round number: Corr -> Rounds
|
||||
\* @type: $process -> $step;
|
||||
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
|
||||
\* @type: $process -> $value;
|
||||
decision, \* process decision: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $value;
|
||||
lockedValue, \* a locked value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
lockedRound, \* a locked round: Corr -> RoundsOrNil
|
||||
\* @type: $process -> $value;
|
||||
validValue, \* a valid value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
validRound, \* a valid round: Corr -> RoundsOrNil
|
||||
\* @type: $round -> Set($proposeMsg);
|
||||
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: Set($proposeMsg);
|
||||
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
|
||||
\* @type: $action;
|
||||
action \* we use this variable to see which action was taken
|
||||
|
||||
INSTANCE TendermintAccDebug_004_draft WITH
|
||||
Corr <- {"c1", "c2"},
|
||||
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
|
||||
ConstInit == \* the proposer is arbitrary -- works for safety
|
||||
Proposer \in [Rounds -> AllProcs]
|
||||
|
||||
=============================================================================
|
||||
=============================================================================
|
||||
|
||||
@@ -1,40 +1,44 @@
|
||||
---------------------- MODULE MC_n4_f2_amnesia -------------------------------
|
||||
EXTENDS Sequences
|
||||
|
||||
CONSTANT
|
||||
\* @type: ROUND -> PROCESS;
|
||||
CONSTANT
|
||||
\* @type: $round -> $process;
|
||||
Proposer
|
||||
|
||||
\* the variables declared in TendermintAcc3
|
||||
VARIABLES
|
||||
\* @type: PROCESS -> ROUND;
|
||||
round,
|
||||
\* @type: PROCESS -> STEP;
|
||||
step,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
decision,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
lockedValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
lockedRound,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
validValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
validRound,
|
||||
\* @type: ROUND -> Set(PROPMESSAGE);
|
||||
msgsPropose,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrevote,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrecommit,
|
||||
\* @type: Set(MESSAGE);
|
||||
evidence,
|
||||
\* @type: ACTION;
|
||||
action
|
||||
\* @type: $process -> $round;
|
||||
round, \* a process round number: Corr -> Rounds
|
||||
\* @type: $process -> $step;
|
||||
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
|
||||
\* @type: $process -> $value;
|
||||
decision, \* process decision: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $value;
|
||||
lockedValue, \* a locked value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
lockedRound, \* a locked round: Corr -> RoundsOrNil
|
||||
\* @type: $process -> $value;
|
||||
validValue, \* a valid value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
validRound, \* a valid round: Corr -> RoundsOrNil
|
||||
\* @type: $round -> Set($proposeMsg);
|
||||
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: Set($proposeMsg);
|
||||
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
|
||||
\* @type: $action;
|
||||
action \* we use this variable to see which action was taken
|
||||
|
||||
\* the variable declared in TendermintAccTrace3
|
||||
VARIABLE
|
||||
\* @type: TRACE;
|
||||
\* @type: $trace;
|
||||
toReplay
|
||||
|
||||
INSTANCE TendermintAccTrace_004_draft WITH
|
||||
@@ -49,7 +53,7 @@ INSTANCE TendermintAccTrace_004_draft WITH
|
||||
"UponProposalInPropose",
|
||||
"UponProposalInPrevoteOrCommitAndPrevote",
|
||||
"UponProposalInPrecommitNoDecision",
|
||||
"OnRoundCatchup",
|
||||
"OnRoundCatchup",
|
||||
"UponProposalInPropose",
|
||||
"UponProposalInPrevoteOrCommitAndPrevote",
|
||||
"UponProposalInPrecommitNoDecision"
|
||||
@@ -59,4 +63,4 @@ INSTANCE TendermintAccTrace_004_draft WITH
|
||||
ConstInit == \* the proposer is arbitrary -- works for safety
|
||||
Proposer \in [Rounds -> AllProcs]
|
||||
|
||||
=============================================================================
|
||||
=============================================================================
|
||||
|
||||
@@ -1,34 +1,38 @@
|
||||
----------------------------- MODULE MC_n4_f3 -------------------------------
|
||||
CONSTANT
|
||||
\* @type: ROUND -> PROCESS;
|
||||
CONSTANT
|
||||
\* @type: $round -> $process;
|
||||
Proposer
|
||||
|
||||
\* the variables declared in TendermintAcc3
|
||||
VARIABLES
|
||||
\* @type: PROCESS -> ROUND;
|
||||
round,
|
||||
\* @type: PROCESS -> STEP;
|
||||
step,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
decision,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
lockedValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
lockedRound,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
validValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
validRound,
|
||||
\* @type: ROUND -> Set(PROPMESSAGE);
|
||||
msgsPropose,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrevote,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrecommit,
|
||||
\* @type: Set(MESSAGE);
|
||||
evidence,
|
||||
\* @type: ACTION;
|
||||
action
|
||||
\* @type: $process -> $round;
|
||||
round, \* a process round number: Corr -> Rounds
|
||||
\* @type: $process -> $step;
|
||||
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
|
||||
\* @type: $process -> $value;
|
||||
decision, \* process decision: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $value;
|
||||
lockedValue, \* a locked value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
lockedRound, \* a locked round: Corr -> RoundsOrNil
|
||||
\* @type: $process -> $value;
|
||||
validValue, \* a valid value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
validRound, \* a valid round: Corr -> RoundsOrNil
|
||||
\* @type: $round -> Set($proposeMsg);
|
||||
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: Set($proposeMsg);
|
||||
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
|
||||
\* @type: $action;
|
||||
action \* we use this variable to see which action was taken
|
||||
|
||||
INSTANCE TendermintAccDebug_004_draft WITH
|
||||
Corr <- {"c1"},
|
||||
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
|
||||
ConstInit == \* the proposer is arbitrary -- works for safety
|
||||
Proposer \in [Rounds -> AllProcs]
|
||||
|
||||
=============================================================================
|
||||
=============================================================================
|
||||
|
||||
@@ -1,34 +1,38 @@
|
||||
----------------------------- MODULE MC_n5_f1 -------------------------------
|
||||
CONSTANT
|
||||
\* @type: ROUND -> PROCESS;
|
||||
CONSTANT
|
||||
\* @type: $round -> $process;
|
||||
Proposer
|
||||
|
||||
\* the variables declared in TendermintAcc3
|
||||
VARIABLES
|
||||
\* @type: PROCESS -> ROUND;
|
||||
round,
|
||||
\* @type: PROCESS -> STEP;
|
||||
step,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
decision,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
lockedValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
lockedRound,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
validValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
validRound,
|
||||
\* @type: ROUND -> Set(PROPMESSAGE);
|
||||
msgsPropose,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrevote,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrecommit,
|
||||
\* @type: Set(MESSAGE);
|
||||
evidence,
|
||||
\* @type: ACTION;
|
||||
action
|
||||
\* @type: $process -> $round;
|
||||
round, \* a process round number: Corr -> Rounds
|
||||
\* @type: $process -> $step;
|
||||
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
|
||||
\* @type: $process -> $value;
|
||||
decision, \* process decision: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $value;
|
||||
lockedValue, \* a locked value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
lockedRound, \* a locked round: Corr -> RoundsOrNil
|
||||
\* @type: $process -> $value;
|
||||
validValue, \* a valid value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
validRound, \* a valid round: Corr -> RoundsOrNil
|
||||
\* @type: $round -> Set($proposeMsg);
|
||||
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: Set($proposeMsg);
|
||||
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
|
||||
\* @type: $action;
|
||||
action \* we use this variable to see which action was taken
|
||||
|
||||
INSTANCE TendermintAccDebug_004_draft WITH
|
||||
Corr <- {"c1", "c2", "c3", "c4"},
|
||||
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
|
||||
ConstInit == \* the proposer is arbitrary -- works for safety
|
||||
Proposer \in [Rounds -> AllProcs]
|
||||
|
||||
=============================================================================
|
||||
=============================================================================
|
||||
|
||||
@@ -1,34 +1,38 @@
|
||||
----------------------------- MODULE MC_n5_f2 -------------------------------
|
||||
CONSTANT
|
||||
\* @type: ROUND -> PROCESS;
|
||||
CONSTANT
|
||||
\* @type: $round -> $process;
|
||||
Proposer
|
||||
|
||||
\* the variables declared in TendermintAcc3
|
||||
VARIABLES
|
||||
\* @type: PROCESS -> ROUND;
|
||||
round,
|
||||
\* @type: PROCESS -> STEP;
|
||||
step,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
decision,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
lockedValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
lockedRound,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
validValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
validRound,
|
||||
\* @type: ROUND -> Set(PROPMESSAGE);
|
||||
msgsPropose,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrevote,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrecommit,
|
||||
\* @type: Set(MESSAGE);
|
||||
evidence,
|
||||
\* @type: ACTION;
|
||||
action
|
||||
\* @type: $process -> $round;
|
||||
round, \* a process round number: Corr -> Rounds
|
||||
\* @type: $process -> $step;
|
||||
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
|
||||
\* @type: $process -> $value;
|
||||
decision, \* process decision: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $value;
|
||||
lockedValue, \* a locked value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
lockedRound, \* a locked round: Corr -> RoundsOrNil
|
||||
\* @type: $process -> $value;
|
||||
validValue, \* a valid value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
validRound, \* a valid round: Corr -> RoundsOrNil
|
||||
\* @type: $round -> Set($proposeMsg);
|
||||
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: Set($proposeMsg);
|
||||
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
|
||||
\* @type: $action;
|
||||
action \* we use this variable to see which action was taken
|
||||
|
||||
INSTANCE TendermintAccDebug_004_draft WITH
|
||||
Corr <- {"c1", "c2", "c3"},
|
||||
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
|
||||
ConstInit == \* the proposer is arbitrary -- works for safety
|
||||
Proposer \in [Rounds -> AllProcs]
|
||||
|
||||
=============================================================================
|
||||
=============================================================================
|
||||
|
||||
@@ -1,34 +1,38 @@
|
||||
----------------------------- MODULE MC_n6_f1 -------------------------------
|
||||
CONSTANT
|
||||
\* @type: ROUND -> PROCESS;
|
||||
CONSTANT
|
||||
\* @type: $round -> $process;
|
||||
Proposer
|
||||
|
||||
\* the variables declared in TendermintAcc3
|
||||
VARIABLES
|
||||
\* @type: PROCESS -> ROUND;
|
||||
round,
|
||||
\* @type: PROCESS -> STEP;
|
||||
step,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
decision,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
lockedValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
lockedRound,
|
||||
\* @type: PROCESS -> VALUE;
|
||||
validValue,
|
||||
\* @type: PROCESS -> ROUND;
|
||||
validRound,
|
||||
\* @type: ROUND -> Set(PROPMESSAGE);
|
||||
msgsPropose,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrevote,
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
msgsPrecommit,
|
||||
\* @type: Set(MESSAGE);
|
||||
evidence,
|
||||
\* @type: ACTION;
|
||||
action
|
||||
\* @type: $process -> $round;
|
||||
round, \* a process round number: Corr -> Rounds
|
||||
\* @type: $process -> $step;
|
||||
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
|
||||
\* @type: $process -> $value;
|
||||
decision, \* process decision: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $value;
|
||||
lockedValue, \* a locked value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
lockedRound, \* a locked round: Corr -> RoundsOrNil
|
||||
\* @type: $process -> $value;
|
||||
validValue, \* a valid value: Corr -> ValuesOrNil
|
||||
\* @type: $process -> $round;
|
||||
validRound, \* a valid round: Corr -> RoundsOrNil
|
||||
\* @type: $round -> Set($proposeMsg);
|
||||
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: Set($proposeMsg);
|
||||
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
|
||||
\* @type: $action;
|
||||
action \* we use this variable to see which action was taken
|
||||
|
||||
INSTANCE TendermintAccDebug_004_draft WITH
|
||||
Corr <- {"c1", "c2", "c3", "c4", "c5"},
|
||||
@@ -43,4 +47,4 @@ INSTANCE TendermintAccDebug_004_draft WITH
|
||||
ConstInit == \* the proposer is arbitrary -- works for safety
|
||||
Proposer \in [Rounds -> AllProcs]
|
||||
|
||||
=============================================================================
|
||||
=============================================================================
|
||||
|
||||
@@ -19,7 +19,9 @@ NFaultyPrecommits == 6 \* the number of injected faulty PRECOMMIT messages
|
||||
\* rounds to sets of messages.
|
||||
\* Importantly, there will be exactly k messages in the image of msgFun.
|
||||
\* We use this action to produce k faults in an initial state.
|
||||
\* @type: (ROUND -> Set(MESSAGE), Set(MESSAGE), Int) => Bool;
|
||||
\* @type: ($round -> Set({ round: $round, a }),
|
||||
\* Set({ round: $round, a }), Int)
|
||||
\* => Bool;
|
||||
ProduceFaults(msgFun, From, k) ==
|
||||
\E f \in [1..k -> From]:
|
||||
msgFun = [r \in Rounds |-> {m \in {f[i]: i \in 1..k}: m.round = r}]
|
||||
@@ -33,10 +35,12 @@ InitNoFaults ==
|
||||
/\ lockedRound = [p \in Corr |-> NilRound]
|
||||
/\ validValue = [p \in Corr |-> NilValue]
|
||||
/\ validRound = [p \in Corr |-> NilRound]
|
||||
/\ msgsPropose = [r \in Rounds |-> EmptyMsgSet]
|
||||
/\ msgsPrevote = [r \in Rounds |-> EmptyMsgSet]
|
||||
/\ msgsPrecommit = [r \in Rounds |-> EmptyMsgSet]
|
||||
/\ evidence = EmptyMsgSet
|
||||
/\ msgsPropose = [r \in Rounds |-> {}]
|
||||
/\ msgsPrevote = [r \in Rounds |-> {}]
|
||||
/\ msgsPrecommit = [r \in Rounds |-> {}]
|
||||
/\ evidencePropose = {}
|
||||
/\ evidencePrevote = {}
|
||||
/\ evidencePrecommit = {}
|
||||
|
||||
(*
|
||||
A specialized version of Init that injects NFaultyProposals proposals,
|
||||
@@ -60,7 +64,9 @@ InitFewFaults ==
|
||||
[type: {"PROPOSAL"}, src: Faulty, round: Rounds,
|
||||
proposal: Values, validRound: Rounds \cup {NilRound}],
|
||||
NFaultyProposals)
|
||||
/\ evidence = EmptyMsgSet
|
||||
/\ evidencePropose = {}
|
||||
/\ evidencePrevote = {}
|
||||
/\ evidencePrecommit = {}
|
||||
|
||||
\* Add faults incrementally
|
||||
NextWithFaults ==
|
||||
@@ -68,7 +74,8 @@ NextWithFaults ==
|
||||
\/ Next
|
||||
\* or a faulty process sends a message
|
||||
\//\ UNCHANGED <<round, step, decision, lockedValue,
|
||||
lockedRound, validValue, validRound, evidence>>
|
||||
lockedRound, validValue, validRound,
|
||||
evidencePropose, evidencePrevote, evidencePrecommit>>
|
||||
/\ \E p \in Faulty:
|
||||
\E r \in Rounds:
|
||||
\//\ UNCHANGED <<msgsPrevote, msgsPrecommit>>
|
||||
|
||||
@@ -10,25 +10,22 @@
|
||||
*)
|
||||
|
||||
EXTENDS TendermintAcc_004_draft
|
||||
|
||||
|
||||
(************************** TYPE INVARIANT ***********************************)
|
||||
(* first, we define the sets of all potential messages *)
|
||||
\* @type: Set(PROPMESSAGE);
|
||||
AllProposals ==
|
||||
AllProposals ==
|
||||
[type: {"PROPOSAL"},
|
||||
src: AllProcs,
|
||||
round: Rounds,
|
||||
proposal: ValuesOrNil,
|
||||
validRound: RoundsOrNil]
|
||||
|
||||
\* @type: Set(PREMESSAGE);
|
||||
|
||||
AllPrevotes ==
|
||||
[type: {"PREVOTE"},
|
||||
src: AllProcs,
|
||||
round: Rounds,
|
||||
id: ValuesOrNil]
|
||||
|
||||
\* @type: Set(PREMESSAGE);
|
||||
AllPrecommits ==
|
||||
[type: {"PRECOMMIT"},
|
||||
src: AllProcs,
|
||||
@@ -50,7 +47,9 @@ TypeOK ==
|
||||
/\ BenignRoundsInMessages(msgsPrevote)
|
||||
/\ msgsPrecommit \in [Rounds -> SUBSET AllPrecommits]
|
||||
/\ BenignRoundsInMessages(msgsPrecommit)
|
||||
/\ evidence \in SUBSET (AllProposals \union AllPrevotes \union AllPrecommits)
|
||||
/\ evidencePropose \in SUBSET AllProposals
|
||||
/\ evidencePrevote \in SUBSET AllPrevotes
|
||||
/\ evidencePrecommit \in SUBSET AllPrecommits
|
||||
/\ action \in {
|
||||
"Init",
|
||||
"InsertProposal",
|
||||
@@ -69,13 +68,12 @@ TypeOK ==
|
||||
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]
|
||||
/\ \A m \in evidencePropose:
|
||||
m \in msgsPropose[m.round]
|
||||
/\ \A m \in evidencePrevote:
|
||||
m \in msgsPrevote[m.round]
|
||||
/\ \A m \in evidencePrecommit:
|
||||
m \in msgsPrecommit[m.round]
|
||||
|
||||
NoFutureMessagesForLargerRounds(p) ==
|
||||
\* a correct process does not send messages for the future rounds
|
||||
@@ -89,14 +87,14 @@ NoFutureMessagesForCurrentRound(p) ==
|
||||
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
|
||||
\/ \A m \in msgsPrevote[r]: m.src /= p
|
||||
/\ \/ step[p] \in {"PRECOMMIT", "DECIDED"}
|
||||
\/ \A m \in msgsPrecommit[r]: m.src /= p
|
||||
|
||||
\/ \A m \in msgsPrecommit[r]: m.src /= p
|
||||
|
||||
\* the correct processes never send future messages
|
||||
AllNoFutureMessagesSent ==
|
||||
\A p \in Corr:
|
||||
/\ NoFutureMessagesForCurrentRound(p)
|
||||
/\ NoFutureMessagesForCurrentRound(p)
|
||||
/\ NoFutureMessagesForLargerRounds(p)
|
||||
|
||||
\* a correct process in the PREVOTE state has sent a PREVOTE message
|
||||
@@ -105,9 +103,9 @@ IfInPrevoteThenSentPrevote(p) ==
|
||||
\E m \in msgsPrevote[round[p]]:
|
||||
/\ m.id \in ValidValues \cup { NilValue }
|
||||
/\ m.src = p
|
||||
|
||||
|
||||
AllIfInPrevoteThenSentPrevote ==
|
||||
\A p \in Corr: IfInPrevoteThenSentPrevote(p)
|
||||
\A p \in Corr: IfInPrevoteThenSentPrevote(p)
|
||||
|
||||
\* a correct process in the PRECOMMIT state has sent a PRECOMMIT message
|
||||
IfInPrecommitThenSentPrecommit(p) ==
|
||||
@@ -115,42 +113,44 @@ IfInPrecommitThenSentPrecommit(p) ==
|
||||
\E m \in msgsPrecommit[round[p]]:
|
||||
/\ m.id \in ValidValues \cup { NilValue }
|
||||
/\ m.src = p
|
||||
|
||||
|
||||
AllIfInPrecommitThenSentPrecommit ==
|
||||
\A p \in Corr: IfInPrecommitThenSentPrecommit(p)
|
||||
\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 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:
|
||||
/\ \E m \in msgsPropose[r] \intersect evidencePropose:
|
||||
/\ m.src = Proposer[r]
|
||||
/\ m.proposal = decision[p]
|
||||
\* not inductive: /\ m.src \in Corr => (m.validRound <= r)
|
||||
|
||||
|
||||
AllIfInDecidedThenReceivedProposal ==
|
||||
\A p \in Corr:
|
||||
IfInDecidedThenReceivedProposal(p)
|
||||
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] }
|
||||
LET PV == {
|
||||
m \in msgsPrecommit[r] \intersect evidencePrecommit:
|
||||
m.id = decision[p]
|
||||
}
|
||||
IN
|
||||
Cardinality(PV) >= THRESHOLD2
|
||||
|
||||
|
||||
AllIfInDecidedThenReceivedTwoThirds ==
|
||||
\A p \in Corr:
|
||||
IfInDecidedThenReceivedTwoThirds(p)
|
||||
IfInDecidedThenReceivedTwoThirds(p)
|
||||
|
||||
\* for a round r, there is proposal by the round proposer for a valid round vr
|
||||
ProposalInRound(r, proposedVal, vr) ==
|
||||
@@ -160,7 +160,7 @@ ProposalInRound(r, proposedVal, vr) ==
|
||||
/\ m.validRound = vr
|
||||
|
||||
TwoThirdsPrevotes(vr, v) ==
|
||||
LET PV == { mm \in msgsPrevote[vr] \intersect evidence: mm.id = v } IN
|
||||
LET PV == { mm \in msgsPrevote[vr] \intersect evidencePrevote: mm.id = v } IN
|
||||
Cardinality(PV) >= THRESHOLD2
|
||||
|
||||
\* if a process sends a PREVOTE, then there are three possibilities:
|
||||
@@ -189,8 +189,9 @@ IfSentPrecommitThenReceivedTwoThirds ==
|
||||
\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 }
|
||||
/\ LET PV == {
|
||||
m \in msgsPrevote[r] \intersect evidencePrevote: m.id = mpc.id
|
||||
}
|
||||
IN
|
||||
Cardinality(PV) >= THRESHOLD2
|
||||
\/ /\ mpc.id = NilValue
|
||||
@@ -208,22 +209,22 @@ IfSentPrecommitThenSentPrevote ==
|
||||
\* 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 ==
|
||||
@@ -237,7 +238,7 @@ LatestPrecommitHasLockedRound(p) ==
|
||||
IN
|
||||
/\ lockedRound[p] = latest.round
|
||||
/\ lockedValue[p] = latest.id
|
||||
|
||||
|
||||
AllLatestPrecommitHasLockedRound ==
|
||||
\A p \in Corr:
|
||||
LatestPrecommitHasLockedRound(p)
|
||||
@@ -245,7 +246,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(PREMESSAGE)) => Bool;
|
||||
\* @type: ($round, $round -> Set($preMsg)) => Bool;
|
||||
NoEquivocationByCorrect(r, msgs) ==
|
||||
\A p \in Corr:
|
||||
\E v \in ValidValues \union {NilValue}:
|
||||
@@ -254,22 +255,22 @@ NoEquivocationByCorrect(r, msgs) ==
|
||||
\/ m.id = v
|
||||
|
||||
\* a proposer nevers sends two values
|
||||
\* @type: (ROUND, ROUND -> Set(PROPMESSAGE)) => Bool;
|
||||
\* @type: ($round, $round -> Set($proposeMsg)) => Bool;
|
||||
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)
|
||||
/\ ProposalsByProposer(r, msgsPropose)
|
||||
/\ NoEquivocationByCorrect(r, msgsPrevote)
|
||||
/\ NoEquivocationByCorrect(r, msgsPrecommit)
|
||||
|
||||
\* construct the set of the message senders
|
||||
\* @type: (Set(MESSAGE)) => Set(PROCESS);
|
||||
\* @type: (Set({ src: $process, a })) => Set($process);
|
||||
Senders(M) == { m.src: m \in M }
|
||||
|
||||
\* The final piece by Josef Widder:
|
||||
@@ -286,15 +287,15 @@ PrecommitsLockValue ==
|
||||
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
|
||||
/\ AllIfInDecidedThenReceivedProposal
|
||||
/\ AllIfInDecidedThenReceivedTwoThirds
|
||||
/\ AllIfInDecidedThenValidDecision
|
||||
/\ AllLockedRoundIffLockedValue
|
||||
/\ AllIfLockedRoundThenSentCommit
|
||||
@@ -306,8 +307,8 @@ Inv ==
|
||||
/\ PrecommitsLockValue
|
||||
|
||||
\* this is the inductive invariant we like to check
|
||||
TypedInv == TypeOK /\ Inv
|
||||
|
||||
TypedInv == TypeOK /\ Inv
|
||||
|
||||
\* UNUSED FOR SAFETY
|
||||
ValidRoundNotSmallerThanLockedRound(p) ==
|
||||
validRound[p] >= lockedRound[p]
|
||||
@@ -325,10 +326,10 @@ 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 p \in Corr: IfValidRoundThenTwoThirds(p)
|
||||
|
||||
\* a valid round can be only set to a valid value that was proposed earlier
|
||||
IfValidRoundThenProposal(p) ==
|
||||
@@ -372,5 +373,5 @@ THEOREM AgreementWhenLessThanThirdFaulty ==
|
||||
THEOREM AgreementOrFork ==
|
||||
~FaultyQuorum /\ TypedInv => Accountability
|
||||
|
||||
=============================================================================
|
||||
|
||||
=============================================================================
|
||||
|
||||
|
||||
@@ -3,22 +3,22 @@
|
||||
When Apalache is running too slow and we have an idea of a counterexample,
|
||||
we use this module to restrict the behaviors only to certain actions.
|
||||
Once the whole trace is replayed, the system deadlocks.
|
||||
|
||||
|
||||
Version 1.
|
||||
|
||||
Igor Konnov, 2020.
|
||||
*)
|
||||
|
||||
EXTENDS Sequences, Apalache, TendermintAcc_004_draft
|
||||
EXTENDS Sequences, Apalache, typedefs, TendermintAcc_004_draft
|
||||
|
||||
\* a sequence of action names that should appear in the given order,
|
||||
\* excluding "Init"
|
||||
CONSTANT
|
||||
\* @type: TRACE;
|
||||
CONSTANT
|
||||
\* @type: $trace;
|
||||
Trace
|
||||
|
||||
VARIABLE
|
||||
\* @type: TRACE;
|
||||
VARIABLE
|
||||
\* @type: $trace;
|
||||
toReplay
|
||||
|
||||
TraceInit ==
|
||||
|
||||
@@ -21,7 +21,7 @@
|
||||
|
||||
Byzantine processes can demonstrate arbitrary behavior, including
|
||||
no communication. We show that if agreement is violated, then the Byzantine
|
||||
processes demonstrate one of the two behaviors:
|
||||
processes demonstrate one of the two behaviours:
|
||||
|
||||
- Equivocation: a Byzantine process may send two different values
|
||||
in the same round.
|
||||
@@ -29,6 +29,7 @@
|
||||
- Amnesia: a Byzantine process may lock a value without unlocking
|
||||
the previous value that it has locked in the past.
|
||||
|
||||
* Version 5. Refactor evidence, migrate to Apalache Type System 1.2.
|
||||
* Version 4. Remove defective processes, fix bugs, collect global evidence.
|
||||
* Version 3. Modular and parameterized definitions.
|
||||
* Version 2. Bugfixes in the spec and an inductive invariant.
|
||||
@@ -41,34 +42,34 @@ EXTENDS Integers, FiniteSets, typedefs
|
||||
|
||||
(********************* PROTOCOL PARAMETERS **********************************)
|
||||
CONSTANTS
|
||||
\* @type: Set(PROCESS);
|
||||
Corr, \* the set of correct processes
|
||||
\* @type: Set(PROCESS);
|
||||
\* @type: Set($process);
|
||||
Corr, \* the set of correct processes
|
||||
\* @type: Set($process);
|
||||
Faulty, \* the set of Byzantine processes, may be empty
|
||||
\* @type: Int;
|
||||
\* @type: Int;
|
||||
N, \* the total number of processes: correct, defective, and Byzantine
|
||||
\* @type: Int;
|
||||
\* @type: Int;
|
||||
T, \* an upper bound on the number of Byzantine processes
|
||||
\* @type: Set(VALUE);
|
||||
\* @type: Set($value);
|
||||
ValidValues, \* the set of valid values, proposed both by correct and faulty
|
||||
\* @type: Set(VALUE);
|
||||
\* @type: Set($value);
|
||||
InvalidValues, \* the set of invalid values, never proposed by the correct ones
|
||||
\* @type: ROUND;
|
||||
\* @type: $round;
|
||||
MaxRound, \* the maximal round number
|
||||
\* @type: ROUND -> PROCESS;
|
||||
\* @type: $round -> $process;
|
||||
Proposer \* the proposer function from Rounds to AllProcs
|
||||
|
||||
ASSUME(N = Cardinality(Corr \union Faulty))
|
||||
|
||||
(*************************** DEFINITIONS ************************************)
|
||||
AllProcs == Corr \union Faulty \* the set of all processes
|
||||
\* @type: Set(ROUND);
|
||||
\* @type: Set($round);
|
||||
Rounds == 0..MaxRound \* the set of potential rounds
|
||||
\* @type: ROUND;
|
||||
\* @type: $round;
|
||||
NilRound == -1 \* a special value to denote a nil round, outside of Rounds
|
||||
RoundsOrNil == Rounds \union {NilRound}
|
||||
Values == ValidValues \union InvalidValues \* the set of all values
|
||||
\* @type: VALUE;
|
||||
\* @type: $value;
|
||||
NilValue == "None" \* a special value for a nil round, outside of Values
|
||||
ValuesOrNil == Values \union {NilValue}
|
||||
|
||||
@@ -83,106 +84,105 @@ IsValid(v) == v \in ValidValues
|
||||
THRESHOLD1 == T + 1 \* at least one process is not faulty
|
||||
THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
|
||||
|
||||
(********************* TYPE ANNOTATIONS FOR APALACHE **************************)
|
||||
|
||||
\* An empty set of messages
|
||||
\* @type: Set(MESSAGE);
|
||||
EmptyMsgSet == {}
|
||||
|
||||
(********************* PROTOCOL STATE VARIABLES ******************************)
|
||||
VARIABLES
|
||||
\* @type: PROCESS -> ROUND;
|
||||
\* @type: $process -> $round;
|
||||
round, \* a process round number: Corr -> Rounds
|
||||
\* @type: PROCESS -> STEP;
|
||||
\* @type: $process -> $step;
|
||||
step, \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
|
||||
\* @type: PROCESS -> VALUE;
|
||||
\* @type: $process -> $value;
|
||||
decision, \* process decision: Corr -> ValuesOrNil
|
||||
\* @type: PROCESS -> VALUE;
|
||||
\* @type: $process -> $value;
|
||||
lockedValue, \* a locked value: Corr -> ValuesOrNil
|
||||
\* @type: PROCESS -> ROUND;
|
||||
\* @type: $process -> $round;
|
||||
lockedRound, \* a locked round: Corr -> RoundsOrNil
|
||||
\* @type: PROCESS -> VALUE;
|
||||
\* @type: $process -> $value;
|
||||
validValue, \* a valid value: Corr -> ValuesOrNil
|
||||
\* @type: PROCESS -> ROUND;
|
||||
\* @type: $process -> $round;
|
||||
validRound \* a valid round: Corr -> RoundsOrNil
|
||||
|
||||
\* book-keeping variables
|
||||
VARIABLES
|
||||
\* @type: ROUND -> Set(PROPMESSAGE);
|
||||
\* @type: $round -> Set($proposeMsg);
|
||||
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: ROUND -> Set(PREMESSAGE);
|
||||
\* @type: $round -> Set($preMsg);
|
||||
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
||||
\* @type: Set(MESSAGE);
|
||||
evidence, \* the messages that were used by the correct processes to make transitions
|
||||
\* @type: ACTION;
|
||||
\* @type: Set($proposeMsg);
|
||||
evidencePropose, \* the PROPOSE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrevote, \* the PREVOTE messages used by some correct processes to make transitions
|
||||
\* @type: Set($preMsg);
|
||||
evidencePrecommit, \* the PRECOMMIT messages used by some correct processes to make transitions
|
||||
\* @type: $action;
|
||||
action \* we use this variable to see which action was taken
|
||||
|
||||
(* to see a type invariant, check TendermintAccInv3 *)
|
||||
|
||||
(* to see a type invariant, check TendermintAccInv3 *)
|
||||
|
||||
\* a handy definition used in UNCHANGED
|
||||
vars == <<round, step, decision, lockedValue, lockedRound,
|
||||
validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit>>
|
||||
validValue, validRound, msgsPropose, msgsPrevote, msgsPrecommit,
|
||||
evidencePropose, evidencePrevote, evidencePrecommit>>
|
||||
|
||||
(********************* PROTOCOL INITIALIZATION ******************************)
|
||||
\* @type: (ROUND) => Set(PROPMESSAGE);
|
||||
\* @type: ($round) => Set($proposeMsg);
|
||||
FaultyProposals(r) ==
|
||||
[
|
||||
type : {"PROPOSAL"},
|
||||
type : {"PROPOSAL"},
|
||||
src : Faulty,
|
||||
round : {r},
|
||||
proposal : Values,
|
||||
round : {r},
|
||||
proposal : Values,
|
||||
validRound: RoundsOrNil
|
||||
]
|
||||
|
||||
\* @type: Set(PROPMESSAGE);
|
||||
\* @type: Set($proposeMsg);
|
||||
AllFaultyProposals ==
|
||||
[
|
||||
type : {"PROPOSAL"},
|
||||
type : {"PROPOSAL"},
|
||||
src : Faulty,
|
||||
round : Rounds,
|
||||
proposal : Values,
|
||||
round : Rounds,
|
||||
proposal : Values,
|
||||
validRound: RoundsOrNil
|
||||
]
|
||||
|
||||
\* @type: (ROUND) => Set(PREMESSAGE);
|
||||
\* @type: ($round) => Set($preMsg);
|
||||
FaultyPrevotes(r) ==
|
||||
[
|
||||
type : {"PREVOTE"},
|
||||
src : Faulty,
|
||||
round: {r},
|
||||
type : {"PREVOTE"},
|
||||
src : Faulty,
|
||||
round: {r},
|
||||
id : Values
|
||||
]
|
||||
|
||||
\* @type: Set(PREMESSAGE);
|
||||
AllFaultyPrevotes ==
|
||||
\* @type: Set($preMsg);
|
||||
AllFaultyPrevotes ==
|
||||
[
|
||||
type : {"PREVOTE"},
|
||||
src : Faulty,
|
||||
round: Rounds,
|
||||
type : {"PREVOTE"},
|
||||
src : Faulty,
|
||||
round: Rounds,
|
||||
id : Values
|
||||
]
|
||||
|
||||
\* @type: (ROUND) => Set(PREMESSAGE);
|
||||
\* @type: ($round) => Set($preMsg);
|
||||
FaultyPrecommits(r) ==
|
||||
[
|
||||
type : {"PRECOMMIT"},
|
||||
src : Faulty,
|
||||
round: {r},
|
||||
type : {"PRECOMMIT"},
|
||||
src : Faulty,
|
||||
round: {r},
|
||||
id : Values
|
||||
]
|
||||
|
||||
\* @type: Set(PREMESSAGE);
|
||||
\* @type: Set($preMsg);
|
||||
AllFaultyPrecommits ==
|
||||
[
|
||||
type : {"PRECOMMIT"},
|
||||
src : Faulty,
|
||||
round: Rounds,
|
||||
type : {"PRECOMMIT"},
|
||||
src : Faulty,
|
||||
round: Rounds,
|
||||
id : Values
|
||||
]
|
||||
|
||||
\* @type: (ROUND -> Set(MESSAGE)) => Bool;
|
||||
\* @type: ($round -> Set({ round: Int, a })) => Bool;
|
||||
BenignRoundsInMessages(msgfun) ==
|
||||
\* the message function never contains a message for a wrong round
|
||||
\A r \in Rounds:
|
||||
@@ -204,50 +204,43 @@ Init ==
|
||||
/\ BenignRoundsInMessages(msgsPropose)
|
||||
/\ BenignRoundsInMessages(msgsPrevote)
|
||||
/\ BenignRoundsInMessages(msgsPrecommit)
|
||||
/\ evidence = EmptyMsgSet
|
||||
/\ evidencePropose = {}
|
||||
/\ evidencePrevote = {}
|
||||
/\ evidencePrecommit = {}
|
||||
/\ action = "Init"
|
||||
|
||||
(************************ MESSAGE PASSING ********************************)
|
||||
\* @type: (PROCESS, ROUND, VALUE, ROUND) => Bool;
|
||||
\* @type: ($process, $round, $value, $round) => Bool;
|
||||
BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
|
||||
LET
|
||||
\* @type: PROPMESSAGE;
|
||||
newMsg ==
|
||||
[
|
||||
type |-> "PROPOSAL",
|
||||
src |-> pSrc,
|
||||
LET newMsg == [
|
||||
type |-> "PROPOSAL",
|
||||
src |-> pSrc,
|
||||
round |-> pRound,
|
||||
proposal |-> pProposal,
|
||||
proposal |-> pProposal,
|
||||
validRound |-> pValidRound
|
||||
]
|
||||
]
|
||||
IN
|
||||
msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
|
||||
|
||||
\* @type: (PROCESS, ROUND, VALUE) => Bool;
|
||||
\* @type: ($process, $round, $value) => Bool;
|
||||
BroadcastPrevote(pSrc, pRound, pId) ==
|
||||
LET
|
||||
\* @type: PREMESSAGE;
|
||||
newMsg ==
|
||||
[
|
||||
LET newMsg == [
|
||||
type |-> "PREVOTE",
|
||||
src |-> pSrc,
|
||||
round |-> pRound,
|
||||
src |-> pSrc,
|
||||
round |-> pRound,
|
||||
id |-> pId
|
||||
]
|
||||
]
|
||||
IN
|
||||
msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
|
||||
|
||||
\* @type: (PROCESS, ROUND, VALUE) => Bool;
|
||||
\* @type: ($process, $round, $value) => Bool;
|
||||
BroadcastPrecommit(pSrc, pRound, pId) ==
|
||||
LET
|
||||
\* @type: PREMESSAGE;
|
||||
newMsg ==
|
||||
[
|
||||
LET newMsg == [
|
||||
type |-> "PRECOMMIT",
|
||||
src |-> pSrc,
|
||||
round |-> pRound,
|
||||
src |-> pSrc,
|
||||
round |-> pRound,
|
||||
id |-> pId
|
||||
]
|
||||
]
|
||||
IN
|
||||
msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
|
||||
|
||||
@@ -257,46 +250,42 @@ BroadcastPrecommit(pSrc, pRound, pId) ==
|
||||
StartRound(p, r) ==
|
||||
/\ step[p] /= "DECIDED" \* a decided process does not participate in consensus
|
||||
/\ round' = [round EXCEPT ![p] = r]
|
||||
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
|
||||
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
|
||||
|
||||
\* lines 14-19, a proposal may be sent later
|
||||
\* @type: (PROCESS) => Bool;
|
||||
InsertProposal(p) ==
|
||||
\* @type: $process => Bool;
|
||||
InsertProposal(p) ==
|
||||
LET r == round[p] IN
|
||||
/\ p = Proposer[r]
|
||||
/\ step[p] = "PROPOSE"
|
||||
\* if the proposer is sending a proposal, then there are no other proposals
|
||||
\* by the correct processes for the same round
|
||||
/\ \A m \in msgsPropose[r]: m.src /= p
|
||||
/\ \E v \in ValidValues:
|
||||
LET
|
||||
\* @type: VALUE;
|
||||
proposal ==
|
||||
IF validValue[p] /= NilValue
|
||||
THEN validValue[p]
|
||||
ELSE v
|
||||
/\ \E v \in ValidValues:
|
||||
LET proposal ==
|
||||
IF validValue[p] /= NilValue
|
||||
THEN validValue[p]
|
||||
ELSE v
|
||||
IN BroadcastProposal(p, round[p], proposal, validRound[p])
|
||||
/\ UNCHANGED <<evidence, round, decision, lockedValue, lockedRound,
|
||||
validValue, step, validRound, msgsPrevote, msgsPrecommit>>
|
||||
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
|
||||
validValue, step, validRound, msgsPrevote, msgsPrecommit,
|
||||
evidencePropose, evidencePrevote, evidencePrecommit>>
|
||||
/\ action' = "InsertProposal"
|
||||
|
||||
\* lines 22-27
|
||||
UponProposalInPropose(p) ==
|
||||
\E v \in Values:
|
||||
/\ step[p] = "PROPOSE" (* line 22 *)
|
||||
/\ LET
|
||||
\* @type: PROPMESSAGE;
|
||||
msg ==
|
||||
[
|
||||
type |-> "PROPOSAL",
|
||||
/\ LET msg == [
|
||||
type |-> "PROPOSAL",
|
||||
src |-> Proposer[round[p]],
|
||||
round |-> round[p],
|
||||
proposal |-> v,
|
||||
round |-> round[p],
|
||||
proposal |-> v,
|
||||
validRound |-> NilRound
|
||||
]
|
||||
]
|
||||
IN
|
||||
/\ msg \in msgsPropose[round[p]] \* line 22
|
||||
/\ evidence' = {msg} \union evidence
|
||||
/\ evidencePropose' = {msg} \union evidencePropose
|
||||
/\ LET mid == (* line 23 *)
|
||||
IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
|
||||
THEN Id(v)
|
||||
@@ -305,28 +294,27 @@ UponProposalInPropose(p) ==
|
||||
BroadcastPrevote(p, round[p], mid) \* lines 24-26
|
||||
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
|
||||
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
|
||||
validValue, validRound, msgsPropose, msgsPrecommit>>
|
||||
validValue, validRound, msgsPropose, msgsPrecommit,
|
||||
evidencePrevote, evidencePrecommit>>
|
||||
/\ action' = "UponProposalInPropose"
|
||||
|
||||
\* lines 28-33
|
||||
\* lines 28-33
|
||||
UponProposalInProposeAndPrevote(p) ==
|
||||
\E v \in Values, vr \in Rounds:
|
||||
/\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part
|
||||
/\ LET
|
||||
\* @type: PROPMESSAGE;
|
||||
msg ==
|
||||
[
|
||||
type |-> "PROPOSAL",
|
||||
/\ LET msg == [
|
||||
type |-> "PROPOSAL",
|
||||
src |-> Proposer[round[p]],
|
||||
round |-> round[p],
|
||||
proposal |-> v,
|
||||
round |-> round[p],
|
||||
proposal |-> v,
|
||||
validRound |-> vr
|
||||
]
|
||||
]
|
||||
IN
|
||||
/\ msg \in msgsPropose[round[p]] \* line 28
|
||||
/\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(v) } IN
|
||||
/\ Cardinality(PV) >= THRESHOLD2 \* line 28
|
||||
/\ evidence' = PV \union {msg} \union evidence
|
||||
/\ evidencePropose' = {msg} \union evidencePropose
|
||||
/\ evidencePrevote' = PV \union evidencePrevote
|
||||
/\ LET mid == (* line 29 *)
|
||||
IF IsValid(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
|
||||
THEN Id(v)
|
||||
@@ -335,9 +323,10 @@ UponProposalInProposeAndPrevote(p) ==
|
||||
BroadcastPrevote(p, round[p], mid) \* lines 24-26
|
||||
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
|
||||
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
|
||||
validValue, validRound, msgsPropose, msgsPrecommit>>
|
||||
validValue, validRound, msgsPropose, msgsPrecommit,
|
||||
evidencePrecommit>>
|
||||
/\ action' = "UponProposalInProposeAndPrevote"
|
||||
|
||||
|
||||
\* lines 34-35 + lines 61-64 (onTimeoutPrevote)
|
||||
UponQuorumOfPrevotesAny(p) ==
|
||||
/\ step[p] = "PREVOTE" \* line 34 and 61
|
||||
@@ -346,32 +335,31 @@ UponQuorumOfPrevotesAny(p) ==
|
||||
LET Voters == { m.src: m \in MyEvidence } IN
|
||||
\* compare the number of the unique voters against the threshold
|
||||
/\ Cardinality(Voters) >= THRESHOLD2 \* line 34
|
||||
/\ evidence' = MyEvidence \union evidence
|
||||
/\ evidencePrevote' = MyEvidence \union evidencePrevote
|
||||
/\ BroadcastPrecommit(p, round[p], NilValue)
|
||||
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
|
||||
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
|
||||
validValue, validRound, msgsPropose, msgsPrevote>>
|
||||
validValue, validRound, msgsPropose, msgsPrevote,
|
||||
evidencePropose, evidencePrecommit>>
|
||||
/\ action' = "UponQuorumOfPrevotesAny"
|
||||
|
||||
|
||||
\* lines 36-46
|
||||
UponProposalInPrevoteOrCommitAndPrevote(p) ==
|
||||
\E v \in ValidValues, vr \in RoundsOrNil:
|
||||
/\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
|
||||
/\ LET
|
||||
\* @type: PROPMESSAGE;
|
||||
msg ==
|
||||
[
|
||||
type |-> "PROPOSAL",
|
||||
/\ LET msg == [
|
||||
type |-> "PROPOSAL",
|
||||
src |-> Proposer[round[p]],
|
||||
round |-> round[p],
|
||||
proposal |-> v,
|
||||
round |-> round[p],
|
||||
proposal |-> v,
|
||||
validRound |-> vr
|
||||
]
|
||||
]
|
||||
IN
|
||||
/\ msg \in msgsPropose[round[p]] \* line 36
|
||||
/\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(v) } IN
|
||||
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
|
||||
/\ evidence' = PV \union {msg} \union evidence
|
||||
/\ evidencePrevote' = PV \union evidencePrevote
|
||||
/\ evidencePropose' = {msg} \union evidencePropose
|
||||
/\ IF step[p] = "PREVOTE"
|
||||
THEN \* lines 38-41:
|
||||
/\ lockedValue' = [lockedValue EXCEPT ![p] = v]
|
||||
@@ -383,7 +371,8 @@ UponProposalInPrevoteOrCommitAndPrevote(p) ==
|
||||
\* lines 42-43
|
||||
/\ validValue' = [validValue EXCEPT ![p] = v]
|
||||
/\ validRound' = [validRound EXCEPT ![p] = round[p]]
|
||||
/\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote>>
|
||||
/\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote,
|
||||
evidencePrecommit>>
|
||||
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
|
||||
|
||||
\* lines 47-48 + 65-67 (onTimeoutPrecommit)
|
||||
@@ -393,40 +382,40 @@ 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
|
||||
/\ evidence' = MyEvidence \union evidence
|
||||
/\ evidencePrecommit' = MyEvidence \union evidencePrecommit
|
||||
/\ round[p] + 1 \in Rounds
|
||||
/\ StartRound(p, round[p] + 1)
|
||||
/\ StartRound(p, round[p] + 1)
|
||||
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
|
||||
validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
|
||||
validRound, msgsPropose, msgsPrevote, msgsPrecommit,
|
||||
evidencePropose, evidencePrevote>>
|
||||
/\ action' = "UponQuorumOfPrecommitsAny"
|
||||
|
||||
\* lines 49-54
|
||||
|
||||
\* lines 49-54
|
||||
UponProposalInPrecommitNoDecision(p) ==
|
||||
/\ decision[p] = NilValue \* line 49
|
||||
/\ \E v \in ValidValues (* line 50*) , r \in Rounds, vr \in RoundsOrNil:
|
||||
/\ LET
|
||||
\* @type: PROPMESSAGE;
|
||||
msg ==
|
||||
[
|
||||
type |-> "PROPOSAL",
|
||||
/\ LET msg == [
|
||||
type |-> "PROPOSAL",
|
||||
src |-> Proposer[r],
|
||||
round |-> r,
|
||||
proposal |-> v,
|
||||
round |-> r,
|
||||
proposal |-> v,
|
||||
validRound |-> vr
|
||||
]
|
||||
]
|
||||
IN
|
||||
/\ msg \in msgsPropose[r] \* line 49
|
||||
/\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(v) } IN
|
||||
/\ Cardinality(PV) >= THRESHOLD2 \* line 49
|
||||
/\ evidence' = PV \union {msg} \union evidence
|
||||
/\ evidencePrecommit' = PV \union evidencePrecommit
|
||||
/\ evidencePropose' = evidencePropose \union { msg }
|
||||
/\ decision' = [decision EXCEPT ![p] = v] \* update the decision, line 51
|
||||
\* The original algorithm does not have 'DECIDED', but it increments the height.
|
||||
\* We introduced 'DECIDED' here to prevent the process from changing its decision.
|
||||
/\ step' = [step EXCEPT ![p] = "DECIDED"]
|
||||
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
|
||||
validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
|
||||
validRound, msgsPropose, msgsPrevote, msgsPrecommit,
|
||||
evidencePrevote>>
|
||||
/\ action' = "UponProposalInPrecommitNoDecision"
|
||||
|
||||
|
||||
\* the actions below are not essential for safety, but added for completeness
|
||||
|
||||
\* lines 20-21 + 57-60
|
||||
@@ -436,7 +425,8 @@ OnTimeoutPropose(p) ==
|
||||
/\ BroadcastPrevote(p, round[p], NilValue)
|
||||
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
|
||||
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
|
||||
validRound, decision, evidence, msgsPropose, msgsPrecommit>>
|
||||
validRound, decision, msgsPropose, msgsPrecommit,
|
||||
evidencePropose, evidencePrevote, evidencePrecommit>>
|
||||
/\ action' = "OnTimeoutPropose"
|
||||
|
||||
\* lines 44-46
|
||||
@@ -444,21 +434,30 @@ OnQuorumOfNilPrevotes(p) ==
|
||||
/\ step[p] = "PREVOTE"
|
||||
/\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(NilValue) } IN
|
||||
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
|
||||
/\ evidence' = PV \union evidence
|
||||
/\ evidencePrevote' = PV \union evidencePrevote
|
||||
/\ BroadcastPrecommit(p, round[p], Id(NilValue))
|
||||
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
|
||||
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
|
||||
validRound, decision, msgsPropose, msgsPrevote>>
|
||||
validRound, decision, msgsPropose, msgsPrevote,
|
||||
evidencePropose, evidencePrecommit>>
|
||||
/\ action' = "OnQuorumOfNilPrevotes"
|
||||
|
||||
\* lines 55-56
|
||||
OnRoundCatchup(p) ==
|
||||
\E r \in {rr \in Rounds: rr > round[p]}:
|
||||
LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN
|
||||
\E MyEvidence \in SUBSET RoundMsgs:
|
||||
LET Faster == { m.src: m \in MyEvidence } IN
|
||||
\E EvPropose \in SUBSET msgsPropose[r],
|
||||
EvPrevote \in SUBSET msgsPrevote[r],
|
||||
EvPrecommit \in SUBSET msgsPrecommit[r]:
|
||||
LET \* @type: Set({ src: $process, a }) => Set($process);
|
||||
Src(E) == { m.src: m \in E }
|
||||
IN
|
||||
LET Faster ==
|
||||
Src(EvPropose) \union Src(EvPrevote) \union Src(EvPrecommit)
|
||||
IN
|
||||
/\ Cardinality(Faster) >= THRESHOLD1
|
||||
/\ evidence' = MyEvidence \union evidence
|
||||
/\ evidencePropose' = EvPropose \union evidencePropose
|
||||
/\ evidencePrevote' = EvPrevote \union evidencePrevote
|
||||
/\ evidencePrecommit' = EvPrecommit \union evidencePrecommit
|
||||
/\ StartRound(p, r)
|
||||
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
|
||||
validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
|
||||
@@ -482,17 +481,24 @@ Next ==
|
||||
\/ OnQuorumOfNilPrevotes(p)
|
||||
\/ OnRoundCatchup(p)
|
||||
|
||||
|
||||
|
||||
(**************************** FORK SCENARIOS ***************************)
|
||||
|
||||
\* equivocation by a process p
|
||||
EquivocationBy(p) ==
|
||||
\E m1, m2 \in evidence:
|
||||
/\ m1 /= m2
|
||||
/\ m1.src = p
|
||||
/\ m2.src = p
|
||||
/\ m1.round = m2.round
|
||||
/\ m1.type = m2.type
|
||||
LET
|
||||
\* @type: Set({ src: $process, a }) => Bool;
|
||||
EquivocationIn(S) ==
|
||||
\E m1, m2 \in S:
|
||||
/\ m1 /= m2
|
||||
/\ m1.src = p
|
||||
/\ m2.src = p
|
||||
/\ m1.round = m2.round
|
||||
/\ m1.type = m2.type
|
||||
IN
|
||||
\/ EquivocationIn(evidencePropose)
|
||||
\/ EquivocationIn(evidencePrevote)
|
||||
\/ EquivocationIn(evidencePrecommit)
|
||||
|
||||
\* amnesic behavior by a process p
|
||||
AmnesiaBy(p) ==
|
||||
@@ -501,21 +507,20 @@ AmnesiaBy(p) ==
|
||||
/\ \E v1, v2 \in ValidValues:
|
||||
/\ v1 /= v2
|
||||
/\ [
|
||||
type |-> "PRECOMMIT",
|
||||
type |-> "PRECOMMIT",
|
||||
src |-> p,
|
||||
round |-> r1,
|
||||
round |-> r1,
|
||||
id |-> Id(v1)
|
||||
] \in evidence
|
||||
] \in evidencePrecommit
|
||||
/\ [
|
||||
type |-> "PREVOTE",
|
||||
type |-> "PREVOTE",
|
||||
src |-> p,
|
||||
round |-> r2,
|
||||
round |-> r2,
|
||||
id |-> Id(v2)
|
||||
] \in evidence
|
||||
] \in evidencePrevote
|
||||
/\ \A r \in { rnd \in Rounds: r1 <= rnd /\ rnd < r2 }:
|
||||
LET prevotes ==
|
||||
{ m \in evidence:
|
||||
m.type = "PREVOTE" /\ m.round = r /\ m.id = Id(v2) }
|
||||
{ m \in evidencePrevote: m.round = r /\ m.id = Id(v2) }
|
||||
IN
|
||||
Cardinality(prevotes) < THRESHOLD2
|
||||
|
||||
@@ -545,7 +550,7 @@ Accountability ==
|
||||
EquivocationBy(p) \/ AmnesiaBy(p)
|
||||
|
||||
(****************** FALSE INVARIANTS TO PRODUCE EXAMPLES ***********************)
|
||||
|
||||
|
||||
\* This property is violated. You can check it to see how amnesic behavior
|
||||
\* appears in the evidence variable.
|
||||
NoAmnesia ==
|
||||
@@ -562,12 +567,12 @@ NoAgreement ==
|
||||
\A p, q \in Corr:
|
||||
(p /= q /\ decision[p] /= NilValue /\ decision[q] /= NilValue)
|
||||
=> decision[p] /= decision[q]
|
||||
|
||||
|
||||
\* Either agreement holds, or the faulty processes indeed demonstrate amnesia.
|
||||
\* This property is violated. A counterexample should demonstrate equivocation.
|
||||
AgreementOrAmnesia ==
|
||||
Agreement \/ (\A p \in Faulty: AmnesiaBy(p))
|
||||
|
||||
|
||||
\* We expect this property to be violated. It shows us a protocol run,
|
||||
\* where one faulty process demonstrates amnesia without equivocation.
|
||||
\* However, the absence of amnesia
|
||||
@@ -584,7 +589,7 @@ AmnesiaImpliesEquivocation ==
|
||||
|
||||
(*
|
||||
This property is violated. You can check it to see that all correct processes
|
||||
may reach MaxRound without making a decision.
|
||||
may reach MaxRound without making a decision.
|
||||
*)
|
||||
NeverUndecidedInMaxRound ==
|
||||
LET AllInMax == \A p \in Corr: round[p] = MaxRound
|
||||
@@ -592,5 +597,5 @@ NeverUndecidedInMaxRound ==
|
||||
IN
|
||||
AllInMax => AllDecided
|
||||
|
||||
=============================================================================
|
||||
|
||||
=============================================================================
|
||||
|
||||
|
||||
@@ -1,36 +1,27 @@
|
||||
-------------------- MODULE typedefs ---------------------------
|
||||
(*
|
||||
@typeAlias: PROCESS = Str;
|
||||
@typeAlias: VALUE = Str;
|
||||
@typeAlias: STEP = Str;
|
||||
@typeAlias: ROUND = Int;
|
||||
@typeAlias: ACTION = Str;
|
||||
@typeAlias: TRACE = Seq(Str);
|
||||
@typeAlias: PROPMESSAGE =
|
||||
[
|
||||
type: STEP,
|
||||
src: PROCESS,
|
||||
round: ROUND,
|
||||
proposal: VALUE,
|
||||
validRound: ROUND
|
||||
];
|
||||
@typeAlias: PREMESSAGE =
|
||||
[
|
||||
type: STEP,
|
||||
src: PROCESS,
|
||||
round: ROUND,
|
||||
id: VALUE
|
||||
];
|
||||
@typeAlias: MESSAGE =
|
||||
[
|
||||
type: STEP,
|
||||
src: PROCESS,
|
||||
round: ROUND,
|
||||
proposal: VALUE,
|
||||
validRound: ROUND,
|
||||
id: VALUE
|
||||
];
|
||||
@typeAlias: process = Str;
|
||||
@typeAlias: value = Str;
|
||||
@typeAlias: step = Str;
|
||||
@typeAlias: round = Int;
|
||||
@typeAlias: action = Str;
|
||||
@typeAlias: trace = Seq(Str);
|
||||
@typeAlias: proposeMsg =
|
||||
{
|
||||
type: $step,
|
||||
src: $process,
|
||||
round: $round,
|
||||
proposal: $value,
|
||||
validRound: $round
|
||||
};
|
||||
@typeAlias: preMsg =
|
||||
{
|
||||
type: $step,
|
||||
src: $process,
|
||||
round: $round,
|
||||
id: $value
|
||||
};
|
||||
*)
|
||||
TypeAliases == TRUE
|
||||
|
||||
=============================================================================
|
||||
=============================================================================
|
||||
|
||||
Reference in New Issue
Block a user