From 17a197929c74c3679b5db6f86286821c8030e6aa Mon Sep 17 00:00:00 2001 From: Kukovec Date: Tue, 1 Feb 2022 19:49:18 +0100 Subject: [PATCH] Updated Apalache type annotations (#395) --- spec/light-client/accountability/MC_n4_f1.tla | 30 ++- spec/light-client/accountability/MC_n4_f2.tla | 30 ++- .../accountability/MC_n4_f2_amnesia.tla | 36 ++- spec/light-client/accountability/MC_n4_f3.tla | 30 ++- spec/light-client/accountability/MC_n5_f1.tla | 30 ++- spec/light-client/accountability/MC_n5_f2.tla | 30 ++- spec/light-client/accountability/MC_n6_f1.tla | 30 ++- .../TendermintAccDebug_004_draft.tla | 9 +- .../TendermintAccInv_004_draft.tla | 34 +-- .../TendermintAccTrace_004_draft.tla | 8 +- .../TendermintAcc_004_draft.tla | 230 ++++++++++++++---- spec/light-client/accountability/typedefs.tla | 36 +++ 12 files changed, 434 insertions(+), 99 deletions(-) create mode 100644 spec/light-client/accountability/typedefs.tla diff --git a/spec/light-client/accountability/MC_n4_f1.tla b/spec/light-client/accountability/MC_n4_f1.tla index 7a828b498..62bcb30de 100644 --- a/spec/light-client/accountability/MC_n4_f1.tla +++ b/spec/light-client/accountability/MC_n4_f1.tla @@ -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"}, diff --git a/spec/light-client/accountability/MC_n4_f2.tla b/spec/light-client/accountability/MC_n4_f2.tla index 893f18db6..baab2a21d 100644 --- a/spec/light-client/accountability/MC_n4_f2.tla +++ b/spec/light-client/accountability/MC_n4_f2.tla @@ -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"}, diff --git a/spec/light-client/accountability/MC_n4_f2_amnesia.tla b/spec/light-client/accountability/MC_n4_f2_amnesia.tla index 434fffaeb..940903a76 100644 --- a/spec/light-client/accountability/MC_n4_f2_amnesia.tla +++ b/spec/light-client/accountability/MC_n4_f2_amnesia.tla @@ -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 diff --git a/spec/light-client/accountability/MC_n4_f3.tla b/spec/light-client/accountability/MC_n4_f3.tla index b794fff5e..d4c64e6d0 100644 --- a/spec/light-client/accountability/MC_n4_f3.tla +++ b/spec/light-client/accountability/MC_n4_f3.tla @@ -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"}, diff --git a/spec/light-client/accountability/MC_n5_f1.tla b/spec/light-client/accountability/MC_n5_f1.tla index d65673a58..3d7ff979e 100644 --- a/spec/light-client/accountability/MC_n5_f1.tla +++ b/spec/light-client/accountability/MC_n5_f1.tla @@ -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"}, diff --git a/spec/light-client/accountability/MC_n5_f2.tla b/spec/light-client/accountability/MC_n5_f2.tla index c19aa98cc..24400dc07 100644 --- a/spec/light-client/accountability/MC_n5_f2.tla +++ b/spec/light-client/accountability/MC_n5_f2.tla @@ -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"}, diff --git a/spec/light-client/accountability/MC_n6_f1.tla b/spec/light-client/accountability/MC_n6_f1.tla index 2e992974f..a58f8c78a 100644 --- a/spec/light-client/accountability/MC_n6_f1.tla +++ b/spec/light-client/accountability/MC_n6_f1.tla @@ -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"}, diff --git a/spec/light-client/accountability/TendermintAccDebug_004_draft.tla b/spec/light-client/accountability/TendermintAccDebug_004_draft.tla index deaa990ea..9281b8726 100644 --- a/spec/light-client/accountability/TendermintAccDebug_004_draft.tla +++ b/spec/light-client/accountability/TendermintAccDebug_004_draft.tla @@ -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 diff --git a/spec/light-client/accountability/TendermintAccInv_004_draft.tla b/spec/light-client/accountability/TendermintAccInv_004_draft.tla index 5dd15396d..2eeec1fb2 100644 --- a/spec/light-client/accountability/TendermintAccInv_004_draft.tla +++ b/spec/light-client/accountability/TendermintAccInv_004_draft.tla @@ -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: diff --git a/spec/light-client/accountability/TendermintAccTrace_004_draft.tla b/spec/light-client/accountability/TendermintAccTrace_004_draft.tla index 436c2275a..bbc708063 100644 --- a/spec/light-client/accountability/TendermintAccTrace_004_draft.tla +++ b/spec/light-client/accountability/TendermintAccTrace_004_draft.tla @@ -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 diff --git a/spec/light-client/accountability/TendermintAcc_004_draft.tla b/spec/light-client/accountability/TendermintAcc_004_draft.tla index 9d3a543d4..c542f4641 100644 --- a/spec/light-client/accountability/TendermintAcc_004_draft.tla +++ b/spec/light-client/accountability/TendermintAcc_004_draft.tla @@ -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 == <> (********************* 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 <> /\ 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: diff --git a/spec/light-client/accountability/typedefs.tla b/spec/light-client/accountability/typedefs.tla new file mode 100644 index 000000000..5b4f7de52 --- /dev/null +++ b/spec/light-client/accountability/typedefs.tla @@ -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 + +============================================================================= \ No newline at end of file