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

wip: new type annotations for the light client

Browse Source
This commit is contained in:
Igor Konnov
2022-08-16 15:12:47 +02:00
parent cbc7a1abcf
commit b2d3a05f7b
6 changed files with 269 additions and 108 deletions
Download Patch File Download Diff File Expand all files Collapse all files

77
spec/light-client/verification/Blockchain_003_draft.tla
View File

@@ -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 == <<refClock, blockchain, Faulty>>
@@ -59,21 +70,11 @@ vars == <<refClock, blockchain, Faulty>>
(* 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 <<a, b>> that limits the ratio a / b of the faulty
validators from above (exclusive)
@type: (Set(NODE), Set(NODE), <<Int, Int>>) => 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 <<a, b>> that bound the number of
faulty validators in each block by the ratio a / b (exclusive)
*)
@type: <<Int, Int>> => 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

118
spec/light-client/verification/LCVerificationApi_003_draft.tla
View File

@@ -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 <<a, b>> that limits that ratio of faulty validator in the blockchain
from above (exclusive). Tendermint security model prescribes 1 / 3. *)
\* a pair <<a, b>> that limits that ratio of faulty validator in the blockchain
\* from above (exclusive). Tendermint security model prescribes 1 / 3.
\*
\* @type: <<Int, Int>>;
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)
==================================================================================
================================================================================

103
spec/light-client/verification/Lightclient_003_draft.tla
View File

@@ -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 <<a, b>> that limits that ratio of faulty validator in the blockchain
\* from above (exclusive). Tendermint security model prescribes 1 / 3.
\*
\* @type: <<Int, Int>>;
FAULTY_RATIO
(* a pair <<a, b>> 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 == <<localClock, state, nextHeight,
@@ -45,9 +80,13 @@ lcvars == <<localClock, state, nextHeight,
(* the light client previous state components, used for monitoring *)
VARIABLES
\* @type: $lightBlock;
prevVerified,
\* @type: $lightBlock;
prevCurrent,
\* @type: Int;
prevLocalClock,
\* @type: Str;
prevVerdict
InitMonitor(verified, current, pLocalClock, verdict) ==
@@ -67,11 +106,20 @@ NextMonitor(verified, current, pLocalClock, verdict) ==
\* the parameters that are propagated into Blockchain
CONSTANTS
AllNodes
(* a set of all nodes that can act as validators (correct and faulty) *)
\* A set of all nodes that can act as validators (correct and faulty).
\*
\* @type: Set(NODE);
AllNodes
\* the state variables of Blockchain, see Blockchain.tla for the details
VARIABLES refClock, blockchain, Faulty
VARIABLES
\* @type: Int;
refClock,
\* @type: Int -> $blockHeader;
blockchain,
\* @type: Set(NODE);
Faulty
\* All the variables of Blockchain. For some reason, BC!vars does not work
bcvars == <<refClock, blockchain, Faulty>>
@@ -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

17
spec/light-client/verification/MC4_3_correct.tla
View File

@@ -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: <<Int, Int>>;
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
==============================================================================

38
spec/light-client/verification/MC_vars.tla Normal file
View File

@@ -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
===============================================================================

24
spec/light-client/verification/typedefs.tla Normal file
View File

@@ -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
===============================================================================