mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2025-12-23 06:15:19 +00:00
Code Issues Packages Projects Releases Wiki Activity

spec: Sync Light Client TLA+ code with master (#9238)

Browse Source 
* Typo fix in README.md (#350)

* Updated Apalache type annotations (#395)

Co-authored-by: Prajjwol Gautam <prajjwol@gmail.com>
Co-authored-by: Kukovec <jure.kukovec@gmail.com>
This commit is contained in:
Thane Thomson
2022-08-12 14:33:47 -04:00
committed by GitHub
parent f36999e484
commit cbc7a1abcf
13 changed files with 429 additions and 94 deletions
Download Patch File Download Diff File Expand all files Collapse all files

30
spec/light-client/accountability/MC_n4_f1.tla
View File

@@ -1,10 +1,34 @@
----------------------------- MODULE MC_n4_f1 -------------------------------
CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
round, step, decision, lockedValue, lockedRound, validValue, validRound,
msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
\* @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
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2", "c3"},

30
spec/light-client/accountability/MC_n4_f2.tla
View File

@@ -1,10 +1,34 @@
----------------------------- MODULE MC_n4_f2 -------------------------------
CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
round, step, decision, lockedValue, lockedRound, validValue, validRound,
msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
\* @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
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2"},

36
spec/light-client/accountability/MC_n4_f2_amnesia.tla
View File

@@ -1,20 +1,42 @@
---------------------- MODULE MC_n4_f2_amnesia -------------------------------
EXTENDS Sequences
CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
round, step, decision, lockedValue, lockedRound, validValue, validRound,
msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
\* @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
\* the variable declared in TendermintAccTrace3
VARIABLE
\* @type: TRACE;
toReplay
\* old apalache annotations, fix with the new release
a <: b == a
INSTANCE TendermintAccTrace_004_draft WITH
Corr <- {"c1", "c2"},
Faulty <- {"f3", "f4"},
@@ -31,7 +53,7 @@ INSTANCE TendermintAccTrace_004_draft WITH
"UponProposalInPropose",
"UponProposalInPrevoteOrCommitAndPrevote",
"UponProposalInPrecommitNoDecision"
>> <: Seq(STRING)
>>
\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety

30
spec/light-client/accountability/MC_n4_f3.tla
View File

@@ -1,10 +1,34 @@
----------------------------- MODULE MC_n4_f3 -------------------------------
CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
round, step, decision, lockedValue, lockedRound, validValue, validRound,
msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
\* @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
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1"},

30
spec/light-client/accountability/MC_n5_f1.tla
View File

@@ -1,10 +1,34 @@
----------------------------- MODULE MC_n5_f1 -------------------------------
CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
round, step, decision, lockedValue, lockedRound, validValue, validRound,
msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
\* @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
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2", "c3", "c4"},

30
spec/light-client/accountability/MC_n5_f2.tla
View File

@@ -1,10 +1,34 @@
----------------------------- MODULE MC_n5_f2 -------------------------------
CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
round, step, decision, lockedValue, lockedRound, validValue, validRound,
msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
\* @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
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2", "c3"},

30
spec/light-client/accountability/MC_n6_f1.tla
View File

@@ -1,10 +1,34 @@
----------------------------- MODULE MC_n6_f1 -------------------------------
CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
\* the variables declared in TendermintAcc3
VARIABLES
round, step, decision, lockedValue, lockedRound, validValue, validRound,
msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
\* @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
INSTANCE TendermintAccDebug_004_draft WITH
Corr <- {"c1", "c2", "c3", "c4", "c5"},

2
spec/light-client/accountability/README.md
View File

@@ -22,7 +22,7 @@ The agreement property says that for a given height, any two correct validators
However, faulty nodes may forge blocks and try to convince users (light clients) that the blocks had been correctly generated. In addition, Tendermint agreement might be violated in the case where 1/3 or more of the voting power belongs to faulty validators: Two correct validators decide on different blocks. The latter case motivates the term "fork": as Tendermint consensus also agrees on the next validator set, correct validators may have decided on disjoint next validator sets, and the chain branches into two or more partitions (possibly having faulty validators in common) and each branch continues to generate blocks independently of the other.
We say that a fork is a case in which there are two commits for different blocks at the same height of the blockchain. The proplem is to ensure that in those cases we are able to detect faulty validators (and not mistakenly accuse correct validators), and incentivize therefore validators to behave according to the protocol specification.
We say that a fork is a case in which there are two commits for different blocks at the same height of the blockchain. The problem is to ensure that in those cases we are able to detect faulty validators (and not mistakenly accuse correct validators), and incentivize therefore validators to behave according to the protocol specification.
**Conceptual Limit.** In order to prove misbehavior of a node, we have to show that the behavior deviates from correct behavior with respect to a given algorithm. Thus, an algorithm that detects misbehavior of nodes executing some algorithm *A* must be defined with respect to algorithm *A*. In our case, *A* is Tendermint consensus (+ other protocols in the infrastructure; e.g.,full nodes and the Light Client). If the consensus algorithm is changed/updated/optimized in the future, we have to check whether changes to the accountability algorithm are also required. All the discussions in this document are thus inherently specific to Tendermint consensus and the Light Client specification.

9
spec/light-client/accountability/TendermintAccDebug_004_draft.tla
View File

@@ -19,6 +19,7 @@ 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;
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}]
@@ -50,14 +51,14 @@ InitFewFaults ==
/\ validValue = [p \in Corr |-> NilValue]
/\ validRound = [p \in Corr |-> NilRound]
/\ ProduceFaults(msgsPrevote',
SetOfMsgs([type: {"PREVOTE"}, src: Faulty, round: Rounds, id: Values]),
[type: {"PREVOTE"}, src: Faulty, round: Rounds, id: Values],
NFaultyPrevotes)
/\ ProduceFaults(msgsPrecommit',
SetOfMsgs([type: {"PRECOMMIT"}, src: Faulty, round: Rounds, id: Values]),
[type: {"PRECOMMIT"}, src: Faulty, round: Rounds, id: Values],
NFaultyPrecommits)
/\ ProduceFaults(msgsPropose',
SetOfMsgs([type: {"PROPOSAL"}, src: Faulty, round: Rounds,
proposal: Values, validRound: Rounds \cup {NilRound}]),
[type: {"PROPOSAL"}, src: Faulty, round: Rounds,
proposal: Values, validRound: Rounds \cup {NilRound}],
NFaultyProposals)
/\ evidence = EmptyMsgSet

34
spec/light-client/accountability/TendermintAccInv_004_draft.tla
View File

@@ -13,24 +13,27 @@ EXTENDS TendermintAcc_004_draft
(************************** TYPE INVARIANT ***********************************)
(* first, we define the sets of all potential messages *)
\* @type: Set(PROPMESSAGE);
AllProposals ==
SetOfMsgs([type: {"PROPOSAL"},
src: AllProcs,
round: Rounds,
proposal: ValuesOrNil,
validRound: RoundsOrNil])
[type: {"PROPOSAL"},
src: AllProcs,
round: Rounds,
proposal: ValuesOrNil,
validRound: RoundsOrNil]
\* @type: Set(PREMESSAGE);
AllPrevotes ==
SetOfMsgs([type: {"PREVOTE"},
src: AllProcs,
round: Rounds,
id: ValuesOrNil])
[type: {"PREVOTE"},
src: AllProcs,
round: Rounds,
id: ValuesOrNil]
\* @type: Set(PREMESSAGE);
AllPrecommits ==
SetOfMsgs([type: {"PRECOMMIT"},
src: AllProcs,
round: Rounds,
id: ValuesOrNil])
[type: {"PRECOMMIT"},
src: AllProcs,
round: Rounds,
id: ValuesOrNil]
(* the standard type invariant -- importantly, it is inductive *)
TypeOK ==
@@ -226,7 +229,7 @@ LatestPrecommitHasLockedRound(p) ==
LET pPrecommits ==
{mm \in UNION { msgsPrecommit[r]: r \in Rounds }: mm.src = p /\ mm.id /= NilValue }
IN
pPrecommits /= {} <: {MT}
pPrecommits /= {}
=> LET latest ==
CHOOSE m \in pPrecommits:
\A m2 \in pPrecommits:
@@ -242,6 +245,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;
NoEquivocationByCorrect(r, msgs) ==
\A p \in Corr:
\E v \in ValidValues \union {NilValue}:
@@ -250,6 +254,7 @@ NoEquivocationByCorrect(r, msgs) ==
\/ m.id = v
\* a proposer nevers sends two values
\* @type: (ROUND, ROUND -> Set(PROPMESSAGE)) => Bool;
ProposalsByProposer(r, msgs) ==
\* if the proposer is not faulty, it sends only one value
\E v \in ValidValues:
@@ -264,6 +269,7 @@ AllNoEquivocationByCorrect ==
/\ NoEquivocationByCorrect(r, msgsPrecommit)
\* construct the set of the message senders
\* @type: (Set(MESSAGE)) => Set(PROCESS);
Senders(M) == { m.src: m \in M }
\* The final piece by Josef Widder:

8
spec/light-client/accountability/TendermintAccTrace_004_draft.tla
View File

@@ -13,9 +13,13 @@ EXTENDS Sequences, Apalache, TendermintAcc_004_draft
\* a sequence of action names that should appear in the given order,
\* excluding "Init"
CONSTANT Trace
CONSTANT
\* @type: TRACE;
Trace
VARIABLE toReplay
VARIABLE
\* @type: TRACE;
toReplay
TraceInit ==
/\ toReplay = Trace

218
spec/light-client/accountability/TendermintAcc_004_draft.tla
View File

@@ -37,31 +37,43 @@
Zarko Milosevic, Igor Konnov, Informal Systems, 2019-2020.
*)
EXTENDS Integers, FiniteSets
EXTENDS Integers, FiniteSets, typedefs
(********************* PROTOCOL PARAMETERS **********************************)
CONSTANTS
\* @type: Set(PROCESS);
Corr, \* the set of correct processes
\* @type: Set(PROCESS);
Faulty, \* the set of Byzantine processes, may be empty
\* @type: Int;
N, \* the total number of processes: correct, defective, and Byzantine
\* @type: Int;
T, \* an upper bound on the number of Byzantine processes
\* @type: Set(VALUE);
ValidValues, \* the set of valid values, proposed both by correct and faulty
\* @type: Set(VALUE);
InvalidValues, \* the set of invalid values, never proposed by the correct ones
\* @type: ROUND;
MaxRound, \* the maximal round number
Proposer \* the proposer function from 0..NRounds to 1..N
\* @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);
Rounds == 0..MaxRound \* the set of potential rounds
\* @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;
NilValue == "None" \* a special value for a nil round, outside of Values
ValuesOrNil == Values \union {NilValue}
\* a value hash is modeled as identity
\* @type: (t) => t;
Id(v) == v
\* The validity predicate
@@ -72,36 +84,39 @@ 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 **************************)
\* the operator for type annotations
a <: b == a
\* the type of message records
MT == [type |-> STRING, src |-> STRING, round |-> Int,
proposal |-> STRING, validRound |-> Int, id |-> STRING]
\* a type annotation for a message
AsMsg(m) == m <: MT
\* a type annotation for a set of messages
SetOfMsgs(S) == S <: {MT}
\* a type annotation for an empty set of messages
EmptyMsgSet == SetOfMsgs({})
\* An empty set of messages
\* @type: Set(MESSAGE);
EmptyMsgSet == {}
(********************* PROTOCOL STATE VARIABLES ******************************)
VARIABLES
\* @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
\* book-keeping variables
VARIABLES
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: ROUND -> Set(PREMESSAGE);
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;
action \* we use this variable to see which action was taken
(* to see a type invariant, check TendermintAccInv3 *)
@@ -111,26 +126,63 @@ vars == <<round, step, decision, lockedValue, lockedRound,
validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit>>
(********************* PROTOCOL INITIALIZATION ******************************)
\* @type: (ROUND) => Set(PROPMESSAGE);
FaultyProposals(r) ==
SetOfMsgs([type: {"PROPOSAL"}, src: Faulty,
round: {r}, proposal: Values, validRound: RoundsOrNil])
[
type : {"PROPOSAL"},
src : Faulty,
round : {r},
proposal : Values,
validRound: RoundsOrNil
]
\* @type: Set(PROPMESSAGE);
AllFaultyProposals ==
SetOfMsgs([type: {"PROPOSAL"}, src: Faulty,
round: Rounds, proposal: Values, validRound: RoundsOrNil])
[
type : {"PROPOSAL"},
src : Faulty,
round : Rounds,
proposal : Values,
validRound: RoundsOrNil
]
\* @type: (ROUND) => Set(PREMESSAGE);
FaultyPrevotes(r) ==
SetOfMsgs([type: {"PREVOTE"}, src: Faulty, round: {r}, id: Values])
[
type : {"PREVOTE"},
src : Faulty,
round: {r},
id : Values
]
\* @type: Set(PREMESSAGE);
AllFaultyPrevotes ==
SetOfMsgs([type: {"PREVOTE"}, src: Faulty, round: Rounds, id: Values])
[
type : {"PREVOTE"},
src : Faulty,
round: Rounds,
id : Values
]
\* @type: (ROUND) => Set(PREMESSAGE);
FaultyPrecommits(r) ==
SetOfMsgs([type: {"PRECOMMIT"}, src: Faulty, round: {r}, id: Values])
[
type : {"PRECOMMIT"},
src : Faulty,
round: {r},
id : Values
]
\* @type: Set(PREMESSAGE);
AllFaultyPrecommits ==
SetOfMsgs([type: {"PRECOMMIT"}, src: Faulty, round: Rounds, id: Values])
[
type : {"PRECOMMIT"},
src : Faulty,
round: Rounds,
id : Values
]
\* @type: (ROUND -> Set(MESSAGE)) => Bool;
BenignRoundsInMessages(msgfun) ==
\* the message function never contains a message for a wrong round
\A r \in Rounds:
@@ -153,25 +205,49 @@ Init ==
/\ BenignRoundsInMessages(msgsPrevote)
/\ BenignRoundsInMessages(msgsPrecommit)
/\ evidence = EmptyMsgSet
/\ action' = "Init"
/\ action = "Init"
(************************ MESSAGE PASSING ********************************)
\* @type: (PROCESS, ROUND, VALUE, ROUND) => Bool;
BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
LET newMsg ==
AsMsg([type |-> "PROPOSAL", src |-> pSrc, round |-> pRound,
proposal |-> pProposal, validRound |-> pValidRound])
LET
\* @type: PROPMESSAGE;
newMsg ==
[
type |-> "PROPOSAL",
src |-> pSrc,
round |-> pRound,
proposal |-> pProposal,
validRound |-> pValidRound
]
IN
msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
\* @type: (PROCESS, ROUND, VALUE) => Bool;
BroadcastPrevote(pSrc, pRound, pId) ==
LET newMsg == AsMsg([type |-> "PREVOTE",
src |-> pSrc, round |-> pRound, id |-> pId])
LET
\* @type: PREMESSAGE;
newMsg ==
[
type |-> "PREVOTE",
src |-> pSrc,
round |-> pRound,
id |-> pId
]
IN
msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
\* @type: (PROCESS, ROUND, VALUE) => Bool;
BroadcastPrecommit(pSrc, pRound, pId) ==
LET newMsg == AsMsg([type |-> "PRECOMMIT",
src |-> pSrc, round |-> pRound, id |-> pId])
LET
\* @type: PREMESSAGE;
newMsg ==
[
type |-> "PRECOMMIT",
src |-> pSrc,
round |-> pRound,
id |-> pId
]
IN
msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
@@ -184,6 +260,7 @@ StartRound(p, r) ==
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
\* lines 14-19, a proposal may be sent later
\* @type: (PROCESS) => Bool;
InsertProposal(p) ==
LET r == round[p] IN
/\ p = Proposer[r]
@@ -192,8 +269,13 @@ InsertProposal(p) ==
\* by the correct processes for the same round
/\ \A m \in msgsPropose[r]: m.src /= p
/\ \E v \in ValidValues:
LET proposal == IF validValue[p] /= NilValue THEN validValue[p] ELSE v IN
BroadcastProposal(p, round[p], proposal, validRound[p])
LET
\* @type: VALUE;
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>>
/\ action' = "InsertProposal"
@@ -202,9 +284,17 @@ InsertProposal(p) ==
UponProposalInPropose(p) ==
\E v \in Values:
/\ step[p] = "PROPOSE" (* line 22 *)
/\ LET msg ==
AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
round |-> round[p], proposal |-> v, validRound |-> NilRound]) IN
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
src |-> Proposer[round[p]],
round |-> round[p],
proposal |-> v,
validRound |-> NilRound
]
IN
/\ msg \in msgsPropose[round[p]] \* line 22
/\ evidence' = {msg} \union evidence
/\ LET mid == (* line 23 *)
@@ -222,9 +312,16 @@ UponProposalInPropose(p) ==
UponProposalInProposeAndPrevote(p) ==
\E v \in Values, vr \in Rounds:
/\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part
/\ LET msg ==
AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
round |-> round[p], proposal |-> v, validRound |-> vr])
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
src |-> Proposer[round[p]],
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
@@ -260,9 +357,17 @@ UponQuorumOfPrevotesAny(p) ==
UponProposalInPrevoteOrCommitAndPrevote(p) ==
\E v \in ValidValues, vr \in RoundsOrNil:
/\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
/\ LET msg ==
AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
round |-> round[p], proposal |-> v, validRound |-> vr]) IN
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
src |-> Proposer[round[p]],
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
@@ -299,8 +404,17 @@ UponQuorumOfPrecommitsAny(p) ==
UponProposalInPrecommitNoDecision(p) ==
/\ decision[p] = NilValue \* line 49
/\ \E v \in ValidValues (* line 50*) , r \in Rounds, vr \in RoundsOrNil:
/\ LET msg == AsMsg([type |-> "PROPOSAL", src |-> Proposer[r],
round |-> r, proposal |-> v, validRound |-> vr]) IN
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
src |-> Proposer[r],
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
@@ -386,10 +500,18 @@ AmnesiaBy(p) ==
/\ r1 < r2
/\ \E v1, v2 \in ValidValues:
/\ v1 /= v2
/\ AsMsg([type |-> "PRECOMMIT", src |-> p,
round |-> r1, id |-> Id(v1)]) \in evidence
/\ AsMsg([type |-> "PREVOTE", src |-> p,
round |-> r2, id |-> Id(v2)]) \in evidence
/\ [
type |-> "PRECOMMIT",
src |-> p,
round |-> r1,
id |-> Id(v1)
] \in evidence
/\ [
type |-> "PREVOTE",
src |-> p,
round |-> r2,
id |-> Id(v2)
] \in evidence
/\ \A r \in { rnd \in Rounds: r1 <= rnd /\ rnd < r2 }:
LET prevotes ==
{ m \in evidence:

36
spec/light-client/accountability/typedefs.tla Normal file
View File

@@ -0,0 +1,36 @@
-------------------- 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
];
*)
TypeAliases == TRUE
=============================================================================