diff --git a/spec/light-client/verification/Blockchain_003_draft.tla b/spec/light-client/verification/Blockchain_003_draft.tla index 2b37c1b18..fe7c273ae 100644 --- a/spec/light-client/verification/Blockchain_003_draft.tla +++ b/spec/light-client/verification/Blockchain_003_draft.tla @@ -6,52 +6,63 @@ voting powers, introduce multiple copies of the same validator (do not forget to give them unique names though). *) -EXTENDS Integers, FiniteSets +EXTENDS Integers, FiniteSets, typedefs Min(a, b) == IF a < b THEN a ELSE b CONSTANT + \* a set of all nodes that can act as validators (correct and faulty) + \* @type: Set(NODE); AllNodes, - (* a set of all nodes that can act as validators (correct and faulty) *) + \* the maximal height that can be ever reached (modelling artifact) + \* @type: Int; ULTIMATE_HEIGHT, - (* a maximal height that can be ever reached (modelling artifact) *) + \* the period within which the validators are trusted + \* @type: Int; TRUSTING_PERIOD - (* the period within which the validators are trusted *) -Heights == 1..ULTIMATE_HEIGHT (* possible heights *) +\* possible heights +Heights == 1..ULTIMATE_HEIGHT (* A commit is just a set of nodes who have committed the block *) Commits == SUBSET AllNodes (* The set of all block headers that can be on the blockchain. - This is a simplified version of the Block data structure in the actual implementation. *) + This is a simplified version of the Block data structure in the + actual implementation. *) BlockHeaders == [ + \* the block height height: Heights, - \* the block height + \* the block timestamp in some integer units time: Int, - \* the block timestamp in some integer units + \* the nodes who have voted on the previous block, the set itself + \* instead of a hash in the implementation, only the hashes of + \* V and NextV are stored in a block, as V and NextV are stored + \* in the application state lastCommit: Commits, - \* the nodes who have voted on the previous block, the set itself instead of a hash - (* in the implementation, only the hashes of V and NextV are stored in a block, - as V and NextV are stored in the application state *) + \* the validators of this bloc. We store the validators instead of the hash VS: SUBSET AllNodes, - \* the validators of this bloc. We store the validators instead of the hash. + \* the validators of the next block. + \* We store the next validators instead of the hash. NextVS: SUBSET AllNodes - \* the validators of the next block. We store the next validators instead of the hash. ] (* A signed header is just a header together with a set of commits *) LightBlocks == [header: BlockHeaders, Commits: Commits] VARIABLES + \* Current global time in integer units as perceived by the reference chain + \* @type: Int; refClock, - (* the current global time in integer units as perceived by the reference chain *) + \* A function of heights to BlockHeaders, + \* which gives us a bird view of the blockchain. + \* @type: $blockchain; blockchain, - (* A sequence of BlockHeaders, which gives us a bird view of the blockchain. *) + \* A set of faulty nodes, which can act as validators. + \* We assume that the set of faulty processes is non-decreasing. + \* If a process has recovered, it should connect using a different id. + \* @type: Set(NODE); Faulty - (* A set of faulty nodes, which can act as validators. We assume that the set - of faulty processes is non-decreasing. If a process has recovered, it should - connect using a different id. *) (* all variables, to be used with UNCHANGED *) vars == <> @@ -59,21 +70,11 @@ vars == <> (* The set of all correct nodes in a state *) Corr == AllNodes \ Faulty -(* APALACHE annotations *) -a <: b == a \* type annotation - -NT == STRING -NodeSet(S) == S <: {NT} -EmptyNodeSet == NodeSet({}) - -BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}] - -LBT == [header |-> BT, Commits |-> {NT}] -(* end of APALACHE annotations *) - (****************************** BLOCKCHAIN ************************************) -(* the header is still within the trusting period *) +\* the header is still within the trusting period +\* +\* @type: $blockHeader => Bool; InTrustingPeriod(header) == refClock < header.time + TRUSTING_PERIOD @@ -97,6 +98,8 @@ TwoThirds(pVS, pNodes) == - pVS is a set of all validators, maybe including Faulty, intersecting with it, etc. - pMaxFaultRatio is a pair <> that limits the ratio a / b of the faulty validators from above (exclusive) + + @type: (Set(NODE), Set(NODE), <>) => Bool; *) FaultyValidatorsFewerThan(pFaultyNodes, pVS, maxRatio) == LET FN == pFaultyNodes \intersect pVS \* faulty nodes in pNodes @@ -108,7 +111,11 @@ FaultyValidatorsFewerThan(pFaultyNodes, pVS, maxRatio) == LET TP == CP + FP IN FP * maxRatio[2] < TP * maxRatio[1] -(* Can a block be produced by a correct peer, or an authenticated Byzantine peer *) +(* + Can a block be produced by a correct peer, or an authenticated Byzantine peer? + + @type: (Int, $lightBlock) => Bool; + *) IsLightBlockAllowedByDigitalSignatures(ht, block) == \/ block.header = blockchain[ht] \* signed by correct and faulty (maybe) \/ /\ block.Commits \subseteq Faulty @@ -122,7 +129,9 @@ IsLightBlockAllowedByDigitalSignatures(ht, block) == Parameters: - pMaxFaultyRatioExclusive is a pair <> that bound the number of faulty validators in each block by the ratio a / b (exclusive) - *) + + @type: <> => Bool; + *) InitToHeight(pMaxFaultyRatioExclusive) == /\ Faulty \in SUBSET AllNodes \* some nodes may fail \* pick the validator sets and last commits @@ -133,7 +142,7 @@ InitToHeight(pMaxFaultyRatioExclusive) == \* the genesis starts on day 1 /\ timestamp[1] = 1 /\ vs[1] = AllNodes - /\ lastCommit[1] = EmptyNodeSet + /\ lastCommit[1] = {} /\ \A h \in Heights \ {1}: /\ lastCommit[h] \subseteq vs[h - 1] \* the non-validators cannot commit /\ TwoThirds(vs[h - 1], lastCommit[h]) \* the commit has >2/3 of validator votes diff --git a/spec/light-client/verification/LCVerificationApi_003_draft.tla b/spec/light-client/verification/LCVerificationApi_003_draft.tla index 909eab92b..5637b45ad 100644 --- a/spec/light-client/verification/LCVerificationApi_003_draft.tla +++ b/spec/light-client/verification/LCVerificationApi_003_draft.tla @@ -2,42 +2,66 @@ (** * The common interface of the light client verification and detection. *) -EXTENDS Integers, FiniteSets +EXTENDS Integers, FiniteSets, typedefs \* the parameters of Light Client CONSTANTS + \* the period within which the validators are trusted + \* + \* @type: Int; TRUSTING_PERIOD, - (* the period within which the validators are trusted *) + \* the assumed precision of the clock + \* + \* @type: Int; CLOCK_DRIFT, - (* the assumed precision of the clock *) + \* the actual clock drift, which under normal circumstances should not + \* be larger than CLOCK_DRIFT (otherwise, there will be a bug) + \* + \* @type: Int; REAL_CLOCK_DRIFT, - (* the actual clock drift, which under normal circumstances should not - be larger than CLOCK_DRIFT (otherwise, there will be a bug) *) - FAULTY_RATIO - (* a pair <> that limits that ratio of faulty validator in the blockchain - from above (exclusive). Tendermint security model prescribes 1 / 3. *) + \* a pair <> that limits that ratio of faulty validator in the blockchain + \* from above (exclusive). Tendermint security model prescribes 1 / 3. + \* + \* @type: <>; +FAULTY_RATIO VARIABLES - localClock (* current time as measured by the light client *) + \* the local clock of the light client + \* @type: Int; + localClock -(* the header is still within the trusting period *) +(** + * Is the header within the trusting period? + * + * @type: $blockHeader => Bool; + *) InTrustingPeriodLocal(header) == \* note that the assumption about the drift reduces the period of trust localClock < header.time + TRUSTING_PERIOD - CLOCK_DRIFT -(* the header is still within the trusting period, even if the clock can go backwards *) +(* + * Is the header within the trusting period, even if the clock can go backwards? + * + * @type: $blockHeader => Bool; + *) InTrustingPeriodLocalSurely(header) == \* note that the assumption about the drift reduces the period of trust localClock < header.time + TRUSTING_PERIOD - 2 * CLOCK_DRIFT -(* ensure that the local clock does not drift far away from the global clock *) +(** + * Is the local clock not too far away from the global clock? + * + * @type: (Int, Int) => Bool; + *) IsLocalClockWithinDrift(local, global) == /\ global - REAL_CLOCK_DRIFT <= local /\ local <= global + REAL_CLOCK_DRIFT (** - * Check that the commits in an untrusted block form 1/3 of the next validators - * in a trusted header. + * Check that the commits in an untrusted block form 1/3 of the next validators + * in a trusted header. + * + * @type: ($lightBlock, $lightBlock) => Bool; *) SignedByOneThirdOfTrusted(trusted, untrusted) == LET TP == Cardinality(trusted.header.NextVS) @@ -46,10 +70,12 @@ SignedByOneThirdOfTrusted(trusted, untrusted) == 3 * SP > TP (** - The first part of the precondition of ValidAndVerified, which does not take - the current time into account. - - [LCV-FUNC-VALID.1::TLA-PRE-UNTIMED.1] + * The first part of the precondition of ValidAndVerified, which does not take + * the current time into account. + * + * [LCV-FUNC-VALID.1::TLA-PRE-UNTIMED.1] + * + * @type: ($lightBlock, $lightBlock) => Bool; *) ValidAndVerifiedPreUntimed(trusted, untrusted) == LET thdr == trusted.header @@ -73,9 +99,11 @@ ValidAndVerifiedPreUntimed(trusted, untrusted) == *) (** - Check the precondition of ValidAndVerified, including the time checks. - - [LCV-FUNC-VALID.1::TLA-PRE.1] + * Check the precondition of ValidAndVerified, including the time checks. + * + * [LCV-FUNC-VALID.1::TLA-PRE.1] + * + * @type: ($lightBlock, $lightBlock, Bool) => Bool; *) ValidAndVerifiedPre(trusted, untrusted, checkFuture) == LET thdr == trusted.header @@ -89,10 +117,13 @@ ValidAndVerifiedPre(trusted, untrusted, checkFuture) == (** - Check, whether an untrusted block is valid and verifiable w.r.t. a trusted header. - This test does take current time into account, but only looks at the block structure. - - [LCV-FUNC-VALID.1::TLA-UNTIMED.1] + * Check, whether an untrusted block is valid and verifiable + * w.r.t. a trusted header. This test does take current time into account, + * but only looks at the block structure. + * + * [LCV-FUNC-VALID.1::TLA-UNTIMED.1] + * + * @type: ($lightBlock, $lightBlock) => Str; *) ValidAndVerifiedUntimed(trusted, untrusted) == IF ~ValidAndVerifiedPreUntimed(trusted, untrusted) @@ -103,10 +134,13 @@ ValidAndVerifiedUntimed(trusted, untrusted) == ELSE "NOT_ENOUGH_TRUST" (** - Check, whether an untrusted block is valid and verifiable w.r.t. a trusted header. - - [LCV-FUNC-VALID.1::TLA.1] - *) + * Check, whether an untrusted block is valid and verifiable + * w.r.t. a trusted header. + * + * [LCV-FUNC-VALID.1::TLA.1] + * + * @type: ($lightBlock, $lightBlock, Bool) => Str; + *) ValidAndVerified(trusted, untrusted, checkFuture) == IF ~ValidAndVerifiedPre(trusted, untrusted, checkFuture) THEN "INVALID" @@ -123,7 +157,9 @@ ValidAndVerified(trusted, untrusted, checkFuture) == (** - The invariant of the light store that is not related to the blockchain + * The invariant of the light store that is not related to the blockchain. + * + * @type: ($lightBlockMap, $lightBlockStatus) => Bool; *) LightStoreInv(fetchedLightBlocks, lightBlockStatus) == \A lh, rh \in DOMAIN fetchedLightBlocks: @@ -142,12 +178,14 @@ LightStoreInv(fetchedLightBlocks, lightBlockStatus) == "SUCCESS" = ValidAndVerifiedUntimed(lhdr, rhdr) (** - Correctness states that all the obtained headers are exactly like in the blockchain. - - It is always the case that every verified header in LightStore was generated by - an instance of Tendermint consensus. - - [LCV-DIST-SAFE.1::CORRECTNESS-INV.1] + * Correctness states that all the obtained headers are exactly like in the blockchain. + * + * It is always the case that every verified header in LightStore was + * generated by an instance of Tendermint consensus. + * + * [LCV-DIST-SAFE.1::CORRECTNESS-INV.1] + * + * @type: ($blockchain, $lightBlockMap, $lightBlockStatus) => Bool; *) CorrectnessInv(blockchain, fetchedLightBlocks, lightBlockStatus) == \A h \in DOMAIN fetchedLightBlocks: @@ -157,13 +195,17 @@ CorrectnessInv(blockchain, fetchedLightBlocks, lightBlockStatus) == (** * When the light client terminates, there are no failed blocks. * (Otherwise, someone lied to us.) + * + * @type: ($lightBlockMap, $lightBlockStatus) => Bool; *) NoFailedBlocksOnSuccessInv(fetchedLightBlocks, lightBlockStatus) == \A h \in DOMAIN fetchedLightBlocks: lightBlockStatus[h] /= "StateFailed" (** - The expected post-condition of VerifyToTarget. + * The expected post-condition of VerifyToTarget. + * + * @type: ($blockchain, Bool, $lightBlockMap, $lightBlockStatus, Int, Int, Str) => Bool; *) VerifyToTargetPost(blockchain, isPeerCorrect, fetchedLightBlocks, lightBlockStatus, @@ -189,4 +231,4 @@ VerifyToTargetPost(blockchain, isPeerCorrect, /\ LightStoreInv(fetchedLightBlocks, lightBlockStatus) -================================================================================== +================================================================================ diff --git a/spec/light-client/verification/Lightclient_003_draft.tla b/spec/light-client/verification/Lightclient_003_draft.tla index e17a88491..bf8b6ede4 100644 --- a/spec/light-client/verification/Lightclient_003_draft.tla +++ b/spec/light-client/verification/Lightclient_003_draft.tla @@ -6,38 +6,73 @@ * https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md *) -EXTENDS Integers, FiniteSets +EXTENDS Integers, FiniteSets, typedefs \* the parameters of Light Client CONSTANTS + \* an index of the block header that the light client trusts by social consensus + \* + \* @type: Int; TRUSTED_HEIGHT, - (* an index of the block header that the light client trusts by social consensus *) + \* an index of the block header that the light client tries to verify + \* + \* @type: Int; TARGET_HEIGHT, - (* an index of the block header that the light client tries to verify *) + \* the period within which the validators are trusted + \* + \* @type: Int; TRUSTING_PERIOD, - (* the period within which the validators are trusted *) + \* the assumed precision of the clock + \* + \* @type: Int; CLOCK_DRIFT, - (* the assumed precision of the clock *) + \* the actual clock drift, which under normal circumstances should not + \* be larger than CLOCK_DRIFT (otherwise, there will be a bug) + \* + \* @type: Int; REAL_CLOCK_DRIFT, - (* the actual clock drift, which under normal circumstances should not - be larger than CLOCK_DRIFT (otherwise, there will be a bug) *) + \* is primary correct? + \* + \* @type: Bool; IS_PRIMARY_CORRECT, - (* is primary correct? *) + \* a pair <> that limits that ratio of faulty validator in the blockchain + \* from above (exclusive). Tendermint security model prescribes 1 / 3. + \* + \* @type: <>; FAULTY_RATIO - (* a pair <> that limits that ratio of faulty validator in the blockchain - from above (exclusive). Tendermint security model prescribes 1 / 3. *) -VARIABLES (* see TypeOK below for the variable types *) - localClock, (* the local clock of the light client *) - state, (* the current state of the light client *) - nextHeight, (* the next height to explore by the light client *) - nprobes (* the lite client iteration, or the number of block tests *) +VARIABLES + \* the local clock of the light client + \* + \* @type: Int; + localClock, + \* the current state of the light client + \* + \* @type: Str; + state, + \* the next height to explore by the light client + \* + \* @type: Int; + nextHeight, + \* the light client iteration, or the number of block tests + \* + \* @type: Int; + nprobes (* the light store *) VARIABLES - fetchedLightBlocks, (* a function from heights to LightBlocks *) - lightBlockStatus, (* a function from heights to block statuses *) - latestVerified (* the latest verified block *) + \* a function from heights to LightBlocks + \* + \* @type: Int -> $lightBlock; + fetchedLightBlocks, + \* a function from heights to block statuses + \* + \* @type: Int -> Str; + lightBlockStatus, + \* the latest verified block + \* + \* @type: $lightBlock; + latestVerified (* the variables of the lite client *) lcvars == < $blockHeader; + blockchain, + \* @type: Set(NODE); + Faulty \* All the variables of Blockchain. For some reason, BC!vars does not work bcvars == <> @@ -118,7 +166,12 @@ LCInit == /\ latestVerified = trustedLightBlock /\ InitMonitor(trustedLightBlock, trustedLightBlock, localClock, "SUCCESS") -\* block should contain a copy of the block from the reference chain, with a matching commit +(* + Block should contain a copy of the block from the reference chain, + with a matching commit. + + @type: ($lightBlock, Int) => Bool; + *) CopyLightBlockFromChain(block, height) == LET ref == blockchain[height] lastCommit == @@ -141,6 +194,8 @@ FetchLightBlockInto(block, height) == \* add a block into the light store \* \* [LCV-FUNC-UPDATE.1::TLA.1] +\* +\* @type: ($lightBlockMap, $lightBlock) => $lightBlockMap; LightStoreUpdateBlocks(lightBlocks, block) == LET ht == block.header.height IN [h \in DOMAIN lightBlocks \union {ht} |-> @@ -149,6 +204,8 @@ LightStoreUpdateBlocks(lightBlocks, block) == \* update the state of a light block \* \* [LCV-FUNC-UPDATE.1::TLA.1] +\* +\* @type: ($lightBlockStatus, Int, Str) => $lightBlockStatus; LightStoreUpdateStates(statuses, ht, blockState) == [h \in DOMAIN statuses \union {ht} |-> IF h = ht THEN blockState ELSE statuses[h]] @@ -156,6 +213,8 @@ LightStoreUpdateStates(statuses, ht, blockState) == \* Check, whether newHeight is a possible next height for the light client. \* \* [LCV-FUNC-SCHEDULE.1::TLA.1] +\* +\* @type: (Int, $lightBlock, Int, Int) => Bool; CanScheduleTo(newHeight, pLatestVerified, pNextHeight, pTargetHeight) == LET ht == pLatestVerified.header.height IN \/ /\ ht = pNextHeight diff --git a/spec/light-client/verification/MC4_3_correct.tla b/spec/light-client/verification/MC4_3_correct.tla index a27d8de05..238d5020b 100644 --- a/spec/light-client/verification/MC4_3_correct.tla +++ b/spec/light-client/verification/MC4_3_correct.tla @@ -1,26 +1,15 @@ ---------------------------- MODULE MC4_3_correct --------------------------- +EXTENDS MC_vars -AllNodes == {"n1", "n2", "n3", "n4"} +AllNodes == {"1_OF_NODE", "2_OF_NODE", "3_OF_NODE", "4_OF_NODE"} TRUSTED_HEIGHT == 1 TARGET_HEIGHT == 3 TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) CLOCK_DRIFT == 10 \* how much we assume the local clock is drifting REAL_CLOCK_DRIFT == 3 \* how much the local clock is actually drifting IS_PRIMARY_CORRECT == TRUE +\* @type: <>; FAULTY_RATIO == <<1, 3>> \* < 1 / 3 faulty validators -VARIABLES - state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, - nprobes, - localClock, - refClock, blockchain, Faulty - -(* the light client previous state components, used for monitoring *) -VARIABLES - prevVerified, - prevCurrent, - prevLocalClock, - prevVerdict - INSTANCE Lightclient_003_draft ============================================================================== diff --git a/spec/light-client/verification/MC_vars.tla b/spec/light-client/verification/MC_vars.tla new file mode 100644 index 000000000..b2ed21bb7 --- /dev/null +++ b/spec/light-client/verification/MC_vars.tla @@ -0,0 +1,38 @@ +------------------------- MODULE MC_vars -------------------------------------- +\* group variable definitions to avoid repetition in MC_*.tla files. + +EXTENDS typedefs + +\* see Lightclient_003_draft.tla for the detailed description + +VARIABLES + \* @type: Int; + localClock, + \* @type: Str; + state, + \* @type: Int; + nextHeight, + \* @type: Int; + nprobes, + \* @type: Int -> $lightBlock; + fetchedLightBlocks, + \* @type: Int -> Str; + lightBlockStatus, + \* @type: $lightBlock; + latestVerified, + \* @type: $lightBlock; + prevVerified, + \* @type: $lightBlock; + prevCurrent, + \* @type: Int; + prevLocalClock, + \* @type: Str; + prevVerdict, + \* @type: Int; + refClock, + \* @type: Int -> $blockHeader; + blockchain, + \* @type: Set(NODE); + Faulty + +=============================================================================== diff --git a/spec/light-client/verification/typedefs.tla b/spec/light-client/verification/typedefs.tla new file mode 100644 index 000000000..24201b460 --- /dev/null +++ b/spec/light-client/verification/typedefs.tla @@ -0,0 +1,24 @@ +----------------------------- MODULE typedefs --------------------------------- + +(* + @typeAlias: blockHeader = { + height: Int, + time: Int, + lastCommit: Set(NODE), + VS: Set(NODE), + NextVS: Set(NODE) + }; + + @typeAlias: lightBlock = { + header: $blockHeader, + Commits: Set(NODE) + }; + + @typeAlias: blockchain = Int -> $blockHeader; + + @typeAlias: lightBlockMap = Int -> $lightBlock; + + @typeAlias: lightBlockStatus = Int -> Str; + *) +typedefs_aliases == TRUE +===============================================================================