diff --git a/rust-spec/lightclient/README.md b/rust-spec/lightclient/README.md index 4f30ed5db..9dbc81f3b 100644 --- a/rust-spec/lightclient/README.md +++ b/rust-spec/lightclient/README.md @@ -12,8 +12,9 @@ verifying a minimal set of data from a network of full nodes (at least one of wh The light client is decomposed into three components: -- Commit Verification - verify signed headers and associated validator set changes from a single full node -- Fork Detection - verify commits across multiple full nodes and detect conflicts (ie. the existence of forks) +- Commit Verification - verify signed headers and associated validator + set changes from a single full node, called primary +- Fork Detection - verify commits across multiple full nodes (called secondaries) and detect conflicts (ie. the existence of forks) - Fork Accountability - given a fork, which validators are responsible for it. ## Commit Verification @@ -75,12 +76,21 @@ no bug is reported up to depth k. ## Attack Detection -This is a work-in-progress draft. - -The [English specification](detection/detection_001_reviewed.md) -defines blockchain forks and light client attacks, and describes -the problem of a light client detecting them from communication with a network -of full nodes, where at least one is correct. +The [English specification](detection/detection_003_reviewed.md) +defines light client attacks (and how they differ from blockchain + forks), and describes the problem of a light client detecting + these attacks by communicating with a network of full nodes, + where at least one is correct. + +The specification also contains a detection protocol that checks +whether the header obtained from the primary via the verification +protocol matches corresponding headers provided by the secondaries. +If this is not the case, the protocol analyses the verification traces +of the involved full nodes +and generates +[evidence](detection/detection_003_reviewed.md#tmbc-lc-evidence-data1) +of misbehavior that can be submitted to a full node so that +the faulty validators can be punished. There is no TLA+ yet. diff --git a/rust-spec/lightclient/detection/detection_002_draft.md b/rust-spec/lightclient/detection/detection_003_reviewed.md similarity index 79% rename from rust-spec/lightclient/detection/detection_002_draft.md rename to rust-spec/lightclient/detection/detection_003_reviewed.md index 6eab312d8..89e920f19 100644 --- a/rust-spec/lightclient/detection/detection_002_draft.md +++ b/rust-spec/lightclient/detection/detection_003_reviewed.md @@ -1,25 +1,3 @@ -# ***This an unfinished draft. Comments are welcome!*** - -**TODO:** We will need to do small adaptations to the verification -spec to reflect the semantics in the LightStore (verified, trusted, -untrusted, etc. not needed anymore). In more detail: - -- The state of the Lightstore needs to go. Functions like `LatestVerified` can -keep the name but will ignore state as it will not exist anymore. - -- verification spec should be adapted to the second parameter of -`VerifyToTarget` -being a lightblock; new version number of function tag; - -- We should clarify what is the expectation of VerifyToTarget -so if it returns TimeoutError it can be assumed faulty. I guess that -VerifyToTarget with correct full node should never terminate with -TimeoutError. - -- We need to introduce a new version number for the new -specification. So we should decide how - to handle that. - # Light Client Attack Detector In this specification, we strengthen the light client to be resistant @@ -28,15 +6,16 @@ the correct Tendermint full nodes agree on the sequence of generated blocks (no fork), but a set of faulty full nodes attack a light client by generating (signing) a block that deviates from the block of the same height on the blockchain. In order to do so, some of these faulty -full nodes must have been validators before and violate -[[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link), as otherwise, if -[[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link) would hold, -[verification](verification) would satisfy -[[LCV-SEQ-SAFE.1]](LCV-SEQ-SAFE-link). +full nodes must have been validators before and violate the assumption +of more than two thirds of "correct voting power" +[[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link], as otherwise, if +[[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link] would hold, +[verification][verification] would satisfy +[[LCV-SEQ-SAFE.1]][LCV-SEQ-SAFE-link]. An attack detector (or detector for short) is a mechanism that is used -by the light client [supervisor](supervisor) after -[verification](verification) of a new light block +by the light client [supervisor][supervisor] after +[verification][verification] of a new light block with the primary, to cross-check the newly learned light block with other peers (secondaries). It expects as input a light block with some height *root* (that serves as a root of trust), and a verification @@ -45,20 +24,22 @@ trace (a sequence of lightblocks) that the primary provided. In case the detector observes a light client attack, it computes evidence data that can be used by Tendermint full nodes to isolate a set of faulty full nodes that are still within the unbonding period -(more than 1/3 of the voting power of the validator set at some block of the chain), -and report them via ABCI to the application of a Tendermint blockchain -in order to punish faulty nodes. +(more than 1/3 of the voting power of the validator set at some block +of the chain), and report them via ABCI (application/blockchain +interface) +to the application of a +Tendermint blockchain in order to punish faulty nodes. ## Context of this document -The light client [verification](verification) specification is +The light client [verification][verification] specification is designed for the Tendermint failure model (1/3 assumption) -[[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link). It is safe under this +[[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link]. It is safe under this assumption, and live if it can reliably (that is, no message loss, no duplication, and eventually delivered) and timely communicate with a -correct full node. If [[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link) assumption is violated, the light client -can be fooled to trust a light block that was not generated by -Tendermint consensus. +correct full node. If [[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link] +assumption is violated, the light client can be fooled to trust a +light block that was not generated by Tendermint consensus. This specification, the attack detector, is a "second line of defense", in case the 1/3 assumption is violated. Its goal is to @@ -73,21 +54,54 @@ project. The light client maintains a simple address book containing addresses of full nodes that it can pick as primary and secondaries. To obtain a new light block, the light client first does -[verification](verification) with the primary, and then cross-checks +[verification][verification] with the primary, and then cross-checks the light block (and the trace of light blocks that led to it) with the secondaries using this specification. -## Tendermint Consensus and Light Client Attacks + +# Outline + +- [Part I](#part-i---Tendermint-Consensus-and-Light-Client-Attacks): + Formal definitions of lightclient attacks, based on basic + properties of Tendermint consensus. + - [Node-based characterization of + attacks](#Node-based-characterization-of-attacks). The + definition of attacks used in the problem statement of + this specification. + + - [Block-based characterization of attacks](#Block-based-characterization-of-attacks). Alternative definitions + provided for future reference. + + +- [Part II](#part-ii---problem-statement): Problem statement of + lightclient attack detection + + - [Informal Problem Statement](#informal-problem-statement) + - [Assumptions](#Assumptions) + - [Definitions](#definitions) + - [Distributed Problem statement](#Distributed-Problem-statement) + +- [Part III](#part-iii---protocol): The protocol + + - [Functions and Data defined in other Specifications](#Functions-and-Data-defined-in-other-Specifications) + - [Outline of Solution](#Outline-of-solution) + - [Details of the functions](#Details-of-the-functions) + - [Correctness arguments](#Correctness-arguments) + + + +# Part I - Tendermint Consensus and Light Client Attacks In this section we will give some mathematical definitions of what we mean by light client attacks (that are considered in this -specification) and how they differ from main-chain forks. To this end +specification) and how they differ from main-chain forks. To this end, we start by defining some properties of the sequence of blocks that is decided upon by Tendermint consensus in normal operation (if the Tendermint failure model holds -[[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link)), +[[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link]), and then define different -deviations that correspond to attack scenarios. +deviations that correspond to attack scenarios. We consider the notion +of [light blocks][LCV-LB-link] and [headers][LVC-HD-link]. #### **[TMBC-GENESIS.1]** @@ -98,11 +112,11 @@ Let *Genesis* be the agreed-upon initial block (file). Let *b* and *c* be two light blocks with *b.Header.Height + 1 = c.Header.Height*. We define the predicate **signs(b,c)** to hold iff *c.Header.LastCommit* is in *PossibleCommit(b)*. -[[TMBC-SOUND-DISTR-POSS-COMMIT.1]](TMBC-SOUND-DISTR-POSS-COMMIT-link). +[[TMBC-SOUND-DISTR-POSS-COMMIT.1]][TMBC-SOUND-DISTR-POSS-COMMIT-link]. > The above encodes sequential verification, that is, intuitively, > b.Header.NextValidators = c.Header.Validators and 2/3 of -> these Validators signed c? +> these Validators signed c. #### **[TMBC-FUNC-SUPPORT.1]** @@ -113,11 +127,11 @@ Let *b* and *c* be two light blocks. We define the predicate - the voting power in *b.NextValidators* of nodes in *c.Commit* is more than 1/3 of *TotalVotingPower(b.Header.NextValidators)* -> That is, if the [Tendermint failure model](TMBC-FM-2THIRDS-link) +> That is, if the [Tendermint failure model][TMBC-FM-2THIRDS-link] > holds, then *c* has been signed by at least one correct full node, cf. -> [[TMBC-VAL-CONTAINS-CORR.1]](TMBC-VAL-CONTAINS-CORR-link). +> [[TMBC-VAL-CONTAINS-CORR.1]][TMBC-VAL-CONTAINS-CORR-link]. > The following formalizes that *b* was properly generated by -> Tendermint; *b* can be traced back to genesis +> Tendermint; *b* can be traced back to genesis. #### **[TMBC-SEQ-ROOTED.1]** @@ -136,7 +150,7 @@ there exist light blocks *a(i)* s.t. #### **[TMBC-SKIP-TRACE.1]** Let *b* and *c* be light blocks. We define *skip-trace(b,c,t)* if at -time t there exists an *h* and a sequence *a(1)*, ... *a(h)* s.t. +time t there exists an integer *h* and a sequence *a(1)*, ... *a(h)* s.t. - *a(1) = b* and - *a(h) = c* and @@ -147,7 +161,7 @@ We call such a sequence *a(1)*, ... *a(h)* a **verification trace**. > The following formalizes that two light blocks of the same height > should agree on the content of the header. Observe that *b* and *c* > may disagree on the Commit. This is a special case if the canonical -> commit has not been decided on, that is, if b.Header.Height is the +> commit has not been decided on yet, that is, if b.Header.Height is the > maximum height of all blocks decided upon by Tendermint at this > moment. @@ -199,7 +213,7 @@ affected (light nodes vs. full nodes). For future reference and discussion we also provide a "block-based characterization of attacks" below. -### Node-based characterization of attacks +## Node-based characterization of attacks #### **[TMBC-MC-FORK.1]** @@ -238,7 +252,7 @@ We consider the following case of a light client attack - *skip-trace(a,c,t)*: by [[TMBC-SKIP-TRACE.1]](#TMBC-SKIP-TRACE1) there is a verification trace *v* of the form *a = v(1)*, ... *v(h) = c* -Evidence for p1 (that proves an attack) consists for index i +Evidence for p1 (that proves an attack to p1) consists for index i of v(i) and v(i+1) such that - E1(i). v(i) is equal to the block of *chain* at height v(i).Height, and @@ -250,19 +264,6 @@ of v(i) and v(i+1) such that > - check that v(i+1) differs from its block at that height, and > - verify v(i+1) in one step from v(i) as v is a verification trace. -**Proposition.** In the case of attack, evidence exists. -*Proof.* First observe that - -- (A). (NOT E2(i)) implies E1(i+1) - -Now by contradiction assume there is no evidence. Thus - -- for all i, we have NOT E1(i) or NOT E2(i) -- for i = 1 we have E1(1) and thus NOT E2(1) - thus by induction on i, by (A) we have for all i that **E1(i)** -- from attack we have E2(h-1), and as there is no evidence for - i = h - 1 we get **NOT E1(h-1)**. Contradiction. -QED. #### **[TMBC-LC-EVIDENCE-DATA.1]** @@ -274,7 +275,7 @@ submit This information is *evidence for height v(i).Height*. -### Block-based characterization of attacks +## Block-based characterization of attacks In this section we provide a different characterization of attacks. It is not defined on the nodes that are affected but purely on the @@ -336,7 +337,9 @@ Let *b* be a light block and *t* a time. We define *bogus(b,t)* iff - *sequ-rooted(b) = false* and - for all *a*, *sequ-rooted(a)* implies *skip-trace(a,b,t) = false* -### Informal Problem statement +# Part II - Problem Statement + +## Informal Problem statement There is no sequential specification: the detector only makes sense in a distributed systems where some nodes misbehave. @@ -358,7 +361,7 @@ also be processed by the Tendermint blockchain. The detector is designed under the assumption that -- [[TMBC-FM-2THIRDS]](TMBC-FM-2THIRDS-link) may be violated +- [[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link] may be violated - there is no fork on the main chain. > As a result some faulty full nodes may launch an attack on a light @@ -369,7 +372,7 @@ things should be done, rather than what should be done. However, they do not constitute temporal logic verification conditions. For those, see [LCD-DIST-*] below. -The detector is called in the [supervisor](supervisor) as follows +The detector is called in the [supervisor][supervisor] as follows ```go Evidences := AttackDetector(root_of_trust, verifiedLS);` @@ -389,7 +392,10 @@ agreed on in the past), and #### **[LCD-IP-STATEMENT.1]** Whenever AttackDetector is called, the detector should for each -secondary try to replay the verification trace `verifiedLS` with the +secondary cross check the largest header in verifiedLS with the +corresponding header of the same height provided by the secondary. If +there is a deviation, the detector should +try to replay the verification trace `verifiedLS` with the secondary - in case replaying leads to detection of a light client attack @@ -399,7 +405,7 @@ secondary proof for an attack. Block *b* may be bogus. In this case the secondary is faulty and it should be replaced. -## Assumptions/Incentives/Environment +## Assumptions It is not in the interest of faulty full nodes to talk to the detector as long as the detector is connected to at least one @@ -414,7 +420,6 @@ one. We can thus base liveness arguments of the detector on the assumptions that correct full nodes reliably talk to the detector. -### Assumptions #### **[LCD-A-CorrFull.1]** @@ -487,10 +492,11 @@ func submitEvidence(Evidences []InternalEvidence) ### LightStore Lightblocks and LightStores are defined in the verification -specification [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See +specification [[LCV-DATA-LIGHTBLOCK.1]][LCV-LB-link] +and [[LCV-DATA-LIGHTSTORE.2]][LCV-LS-link]. See the [verification specification][verification] for details. -## (Distributed) Problem statement +## Distributed Problem statement > As the attack detector is there to reduce the impact of faulty > nodes, and faulty nodes imply that there is a distributed system, @@ -557,34 +563,33 @@ If then the secondary is replaced before the detector terminates. -> The above property is quite operational ("reports"), but it captures -> quite closely the requirement. As the -> detector only makes sense in a distributed setting, and does -> not have a sequential specification, less "pure" -> specification are acceptable. +> The above property is quite operational (e.g., the usage of +> "reports"), but it captures closely the requirement. As the +> detector only makes sense in a distributed setting, and does not +> have a sequential specification, a less "pure" specification are +> acceptable. -# Protocol +# Part III - Protocol ## Functions and Data defined in other Specifications -### From the supervisor +### From the [supervisor][supervisor] +[[LC-FUNC-REPLACE-SECONDARY.1]][repl] ```go Replace_Secondary(addr Address, root-of-trust LightBlock) ``` -### From the verifier +### From the [verifier][verification] +[[LCV-FUNC-MAIN.2]][vtt] ```go func VerifyToTarget(primary PeerID, root LightBlock, targetHeight Height) (LightStore, Result) ``` -> Note: the above differs from the current version in the second -> parameter. verification will be revised. - Observe that `VerifyToTarget` does communication with the secondaries -via the function [FetchLightBlock](fetch). +via the function [FetchLightBlock][fetch]. ### Shared data of the light client @@ -594,14 +599,14 @@ via the function [FetchLightBlock](fetch). > Note that the lightStore is not needed to be shared. -## Outline +## Outline of solution The problem laid out is solved by calling the function `AttackDetector` with a lightstore that contains a light block that has just been verified by the verifier. Then `AttackDetector` downloads headers from the secondaries. In case -a conflicting header is downloaded from a secondary, +a conflicting header is downloaded from a secondary, it calls `CreateEvidenceForPeer` which computes evidence in the case that indeed an attack is confirmed. It could be that the secondary reports a bogus block, which means that there need not be an attack, and the @@ -618,15 +623,15 @@ func AttackDetector(root LightBlock, primary_trace []LightBlock) Evidences := new []InternalEvidence; for each secondary in Secondaries { - lb, result := FetchLightBlock(secondary,primary_trace.Latest().Header.Height); - if result != ResultSuccess { - Replace_Secondary(root); - } - else if lb.Header != primary_trace.Latest().Header { + lb, result := FetchLightBlock(secondary,primary_trace.Latest().Header.Height); + if result != ResultSuccess { + Replace_Secondary(root); + } + else if lb.Header != primary_trace.Latest().Header { // we replay the primary trace with the secondary, in // order to generate evidence that we can submit to the - // secodary. We return the evidence + the trace the + // secondary. We return the evidence + the trace the // secondary told us that spans the evidence at its local store EvidenceForSecondary, newroot, secondary_trace, result := @@ -641,9 +646,9 @@ func AttackDetector(root LightBlock, primary_trace []LightBlock) Evidences.Add(EvidenceForSecondary); // we replay the secondary trace with the primary, ... EvidenceForPrimary, _, result := - CreateEvidenceForPeer(primary, - newroot, - secondary_trace); + CreateEvidenceForPeer(primary, + newroot, + secondary_trace); if result == FoundEvidence { Evidences.Add(EvidenceForPrimary); } @@ -656,10 +661,10 @@ func AttackDetector(root LightBlock, primary_trace []LightBlock) } // In the case where the secondary reports NoEvidence // after initially it reported a conflicting header. - // secondary is faulty - Replace_Secondary(root); + // secondary is faulty + Replace_Secondary(root); } - } + } return Evidences; } ``` @@ -670,7 +675,7 @@ func AttackDetector(root LightBlock, primary_trace []LightBlock) - solves the problem statement (if attack found, then evidence is reported) - Error condition - `ErrorTrustExpired`: fails if root expires (outside trusting - period) [[LCV-INV-TP.1]](LCV-INV-TP1-link) + period) [[LCV-INV-TP.1]][LCV-INV-TP1-link] - `ErrorNoPeers`: if no peers are left to replace secondaries, and no evidence was found before that happened @@ -686,7 +691,7 @@ func CreateEvidenceForPeer(peer PeerID, root LightBlock, trace LightStore) auxLS, result := VerifyToTarget(peer, common, trace[i].Header.Height) if result != ResultSuccess { - // something went wrong; peer did not provide a verifyable block + // something went wrong; peer did not provide a verifiable block return (nil, nil, nil, FaultyPeer) } else { @@ -702,7 +707,7 @@ func CreateEvidenceForPeer(peer PeerID, root LightBlock, trace LightStore) return (ev, common, auxLS, FoundEvidence) } else { - // the peer agrees with the trace, we move common forward + // the peer agrees with the trace, we move common forward. // we could delete auxLS as it will be overwritten in // the next iteration common := trace[i] @@ -719,7 +724,7 @@ func CreateEvidenceForPeer(peer PeerID, root LightBlock, trace LightStore) - finds evidence where trace and peer diverge - Error condition - `ErrorTrustExpired`: fails if root expires (outside trusting - period) [[LCV-INV-TP.1]](LCV-INV-TP1-link) + period) [[LCV-INV-TP.1]][LCV-INV-TP1-link] - If `VerifyToTarget` returns error but root is not expired then return `FaultyPeer` @@ -727,25 +732,44 @@ func CreateEvidenceForPeer(peer PeerID, root LightBlock, trace LightStore) ## Correctness arguments +#### On the existence of evidence + +**Proposition.** In the case of attack, +evidence [[TMBC-LC-ATTACK-EVIDENCE.1]](#TMBC-LC-ATTACK-EVIDENCE1) + exists. +*Proof.* First observe that + +- (A). (NOT E2(i)) implies E1(i+1) + +Now by contradiction assume there is no evidence. Thus + +- for all i, we have NOT E1(i) or NOT E2(i) +- for i = 1 we have E1(1) and thus NOT E2(1) + thus by induction on i, by (A) we have for all i that **E1(i)** +- from attack we have E2(h-1), and as there is no evidence for + i = h - 1 we get **NOT E1(h-1)**. Contradiction. +QED. + + #### Argument for [[LCD-DIST-INV-ATTACK.1]](#LCD-DIST-INV-ATTACK1) Under the assumption that root and trace are a verification trace, -when in `CreateEvidenceForPeer` the detector the detector creates +when in `CreateEvidenceForPeer` the detector creates evidence, then the lightclient has seen two different headers (one via -`trace` and one via `VerifyToTarget` for the same height that can both +`trace` and one via `VerifyToTarget`) for the same height that can both be verified in one step. #### Argument for [[LCD-DIST-INV-STORE.1]](#LCD-DIST-INV-STORE1) We assume that there is at least one correct peer, and there is no -fork. As a result the correct peer has the correct sequence of +fork. As a result, the correct peer has the correct sequence of blocks. Since the primary_trace is checked block-by-block also against each secondary, and at no point evidence was generated that means at no point there were conflicting blocks. #### Argument for [[LCD-DIST-LIVE.1]](#LCD-DIST-LIVE1) -At the latest when [[LCV-INV-TP.1]](LCV-INV-TP1-link) is violated, +At the latest when [[LCV-INV-TP.1]][LCV-INV-TP1-link] is violated, `AttackDetector` terminates. #### Argument for [[LCD-DIST-TERM-NORMAL.1]](#LCD-DIST-TERM-NORMAL1) @@ -775,23 +799,38 @@ Once a bogus block is recognized as such the secondary is removed. [[supervisor]] The specification of the light client supervisor. -[verification]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md +[verification]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md -[supervisor]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/supervisor/supervisor.md +[supervisor]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/supervisor/supervisor_001_draft.md [block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md -[TMBC-FM-2THIRDS-link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#tmbc-fm-2thirds1 +[TMBC-FM-2THIRDS-link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#tmbc-fm-2thirds1 -[TMBC-SOUND-DISTR-POSS-COMMIT-link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#tmbc-sound-distr-poss-commit1 +[TMBC-SOUND-DISTR-POSS-COMMIT-link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#tmbc-sound-distr-poss-commit1 -[LCV-SEQ-SAFE-link]:https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#lcv-seq-safe1 +[LCV-SEQ-SAFE-link]:https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-seq-safe1 [TMBC-VAL-CONTAINS-CORR-link]: -https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#tmbc-val-contains-corr1 +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#tmbc-val-contains-corr1 [fetch]: -https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#lcv-func-fetch1 +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-func-fetch1 [LCV-INV-TP1-link]: -https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification.md#lcv-inv-tp1 +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-inv-tp1 + +[LCV-LB-link]: +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-data-lightblock1 + +[LCV-LS-link]: +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-data-lightstore2 + +[LVC-HD-link]: +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#tmbc-header-fields2 + +[repl]: +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/supervisor/supervisor_001_draft.md#lc-func-replace-secondary1 + +[vtt]: +https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-func-main2 diff --git a/rust-spec/lightclient/verification/verification_002_draft.md b/rust-spec/lightclient/verification/verification_002_draft.md index 80a1890c4..08bf0a807 100644 --- a/rust-spec/lightclient/verification/verification_002_draft.md +++ b/rust-spec/lightclient/verification/verification_002_draft.md @@ -646,9 +646,9 @@ func (ls LightStore) TraceTo(lightBlock LightBlock) (LightBlock, LightStore) ### Invariants -#### **[LCV-INV-TP.2]** +#### **[LCV-INV-TP.1]** -It is always the case that *LightStore.LatestVerified.Header.Time > now - trustingPeriod*. +It is always the case that *LightStore.LatestTrusted.Header.Time > now - trustingPeriod*. > If the invariant is violated, the light client does not have a > header it can trust. A trusted header must be obtained externally,