From 3003e05581f8f88ac4ecf6c60068b1d0fb64efd6 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 16 Aug 2022 16:12:04 +0200 Subject: [PATCH] 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 --- spec/light-client/accountability/MC_n4_f1.tla | 58 +-- spec/light-client/accountability/MC_n4_f2.tla | 58 +-- .../accountability/MC_n4_f2_amnesia.tla | 62 +-- spec/light-client/accountability/MC_n4_f3.tla | 58 +-- spec/light-client/accountability/MC_n5_f1.tla | 58 +-- spec/light-client/accountability/MC_n5_f2.tla | 58 +-- spec/light-client/accountability/MC_n6_f1.tla | 58 +-- .../TendermintAccDebug_004_draft.tla | 21 +- .../TendermintAccInv_004_draft.tla | 111 +++--- .../TendermintAccTrace_004_draft.tla | 12 +- .../TendermintAcc_004_draft.tla | 361 +++++++++--------- spec/light-client/accountability/typedefs.tla | 53 ++- 12 files changed, 500 insertions(+), 468 deletions(-) diff --git a/spec/light-client/accountability/MC_n4_f1.tla b/spec/light-client/accountability/MC_n4_f1.tla index 62bcb30de..00444c24c 100644 --- a/spec/light-client/accountability/MC_n4_f1.tla +++ b/spec/light-client/accountability/MC_n4_f1.tla @@ -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] -============================================================================= +============================================================================= diff --git a/spec/light-client/accountability/MC_n4_f2.tla b/spec/light-client/accountability/MC_n4_f2.tla index baab2a21d..df6813816 100644 --- a/spec/light-client/accountability/MC_n4_f2.tla +++ b/spec/light-client/accountability/MC_n4_f2.tla @@ -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] -============================================================================= +============================================================================= diff --git a/spec/light-client/accountability/MC_n4_f2_amnesia.tla b/spec/light-client/accountability/MC_n4_f2_amnesia.tla index 940903a76..186bdacee 100644 --- a/spec/light-client/accountability/MC_n4_f2_amnesia.tla +++ b/spec/light-client/accountability/MC_n4_f2_amnesia.tla @@ -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] -============================================================================= +============================================================================= diff --git a/spec/light-client/accountability/MC_n4_f3.tla b/spec/light-client/accountability/MC_n4_f3.tla index d4c64e6d0..eb54c573c 100644 --- a/spec/light-client/accountability/MC_n4_f3.tla +++ b/spec/light-client/accountability/MC_n4_f3.tla @@ -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] -============================================================================= +============================================================================= diff --git a/spec/light-client/accountability/MC_n5_f1.tla b/spec/light-client/accountability/MC_n5_f1.tla index 3d7ff979e..4238ab87d 100644 --- a/spec/light-client/accountability/MC_n5_f1.tla +++ b/spec/light-client/accountability/MC_n5_f1.tla @@ -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] -============================================================================= +============================================================================= diff --git a/spec/light-client/accountability/MC_n5_f2.tla b/spec/light-client/accountability/MC_n5_f2.tla index 24400dc07..e928b1929 100644 --- a/spec/light-client/accountability/MC_n5_f2.tla +++ b/spec/light-client/accountability/MC_n5_f2.tla @@ -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] -============================================================================= +============================================================================= diff --git a/spec/light-client/accountability/MC_n6_f1.tla b/spec/light-client/accountability/MC_n6_f1.tla index a58f8c78a..5941ada33 100644 --- a/spec/light-client/accountability/MC_n6_f1.tla +++ b/spec/light-client/accountability/MC_n6_f1.tla @@ -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] -============================================================================= +============================================================================= diff --git a/spec/light-client/accountability/TendermintAccDebug_004_draft.tla b/spec/light-client/accountability/TendermintAccDebug_004_draft.tla index 9281b8726..ab72f9616 100644 --- a/spec/light-client/accountability/TendermintAccDebug_004_draft.tla +++ b/spec/light-client/accountability/TendermintAccDebug_004_draft.tla @@ -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 <> + lockedRound, validValue, validRound, + evidencePropose, evidencePrevote, evidencePrecommit>> /\ \E p \in Faulty: \E r \in Rounds: \//\ UNCHANGED <> diff --git a/spec/light-client/accountability/TendermintAccInv_004_draft.tla b/spec/light-client/accountability/TendermintAccInv_004_draft.tla index 2eeec1fb2..5f9bfcf4e 100644 --- a/spec/light-client/accountability/TendermintAccInv_004_draft.tla +++ b/spec/light-client/accountability/TendermintAccInv_004_draft.tla @@ -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 -============================================================================= - +============================================================================= + diff --git a/spec/light-client/accountability/TendermintAccTrace_004_draft.tla b/spec/light-client/accountability/TendermintAccTrace_004_draft.tla index bbc708063..decd6b733 100644 --- a/spec/light-client/accountability/TendermintAccTrace_004_draft.tla +++ b/spec/light-client/accountability/TendermintAccTrace_004_draft.tla @@ -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 == diff --git a/spec/light-client/accountability/TendermintAcc_004_draft.tla b/spec/light-client/accountability/TendermintAcc_004_draft.tla index fccf993d4..0749e1b49 100644 --- a/spec/light-client/accountability/TendermintAcc_004_draft.tla +++ b/spec/light-client/accountability/TendermintAcc_004_draft.tla @@ -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 == <> + 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 <> + /\ UNCHANGED <> /\ 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 <> + 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 <> + 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 <> + 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 <> + /\ UNCHANGED <> /\ 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 <> + 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 <> + 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 <> + 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 <> + 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 <> @@ -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 -============================================================================= - +============================================================================= + diff --git a/spec/light-client/accountability/typedefs.tla b/spec/light-client/accountability/typedefs.tla index 5b4f7de52..ce232f9e9 100644 --- a/spec/light-client/accountability/typedefs.tla +++ b/spec/light-client/accountability/typedefs.tla @@ -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 -============================================================================= \ No newline at end of file +=============================================================================