mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-01-06 05:25:35 +00:00
Code Issues Packages Projects Releases Wiki Activity

Update to markdown links (#9384)

Browse Source 
* first correction of markdown links

* Review updates
This commit is contained in:
samricotta
2022-09-08 10:31:35 +02:00
committed by GitHub
parent 59a711eabe
commit 5013bc3f4a
50 changed files with 154 additions and 167 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -1,3 +1,3 @@
# Fork accountability
Deprecated, please see [light-client/accountability](../../light-client/accountability.md).
Deprecated, please see [light-client/accountability](https://github.com/tendermint/tendermint/blob/main/spec/consensus/light-client/accountability.md).

2
spec/consensus/light-client/detection.md
View File

@@ -1,3 +1,3 @@
# Detection
Deprecated, please see [light-client/detection](../../light-client/detection.md).
Deprecated, please see [light-client/detection](https://github.com/tendermint/tendermint/blob/main/spec/consensus/light-client/accountability.md).

2
spec/consensus/light-client/verification.md
View File

@@ -1,3 +1,3 @@
# Core Verification
Deprecated, please see [light-client/accountability](../../light-client/verification.md).
Deprecated, please see [light-client/accountability](https://github.com/tendermint/tendermint/blob/main/spec/consensus/light-client/verification.md).

2
spec/consensus/proposer-based-timestamp/pbts-sysmodel_001_draft.md
View File

@@ -73,7 +73,7 @@ Finally, observe that the agreement ([Agreement] and [Time-Agreement]) propertie
### SAFETY
Here we will provide specifications that relate local time to block time. However, since we do not assume (by now) that local time is linked to real-time, these specifications also do not provide a relation between block time and real-time. Such properties are given [later](#REAL-TIME-SAFETY).
Here we will provide specifications that relate local time to block time. However, since we do not assume (by now) that local time is linked to real-time, these specifications also do not provide a relation between block time and real-time. Such properties are given [later](#real-time-safety).
For a correct validator `V`, let `beginConsensus(V,k)` be the local time when it sets its height to `k`, and let `endConsensus(V,k)` be the time when it sets its height to `k + 1`.

3
spec/consensus/readme.md
View File

@@ -25,8 +25,5 @@ Specification of the Tendermint consensus protocol.
- [Write Ahead Log](./wal.md) - Write ahead log used by the
consensus state machine to recover from crashes.
The protocol used to gossip consensus messages between peers, which is critical
for liveness, is described in the [reactors section](../reactors/consensus/consensus.md).
There is also a [stale markdown description](consensus.md) of the consensus state machine
(TODO update this).

22
spec/core/data_structures.md
View File

@@ -47,8 +47,8 @@ and a list of evidence of malfeasance (ie. signing conflicting votes).
| Name | Type | Description | Validation |
|--------|-------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------|
| Header | [Header](#header) | Header corresponding to the block. This field contains information used throughout consensus and other areas of the protocol. To find out what it contains, visit [header] (#header) | Must adhere to the validation rules of [header](#header) |
| Data | [Data](#data) | Data contains a list of transactions. The contents of the transaction is unknown to Tendermint. | This field can be empty or populated, but no validation is performed. Applications can perform validation on individual transactions prior to block creation using [checkTx](../abci/abci.md#checktx).
| Evidence | [EvidenceList](#evidence_list) | Evidence contains a list of infractions committed by validators. | Can be empty, but when populated the validations rules from [evidenceList](#evidence_list) apply |
| Data | [Data](#data) | Data contains a list of transactions. The contents of the transaction is unknown to Tendermint. | This field can be empty or populated, but no validation is performed. Applications can perform validation on individual transactions prior to block creation using [checkTx](https://github.com/tendermint/tendermint/blob/main/spec/abci/abci++_methods.md#checktx).
| Evidence | [EvidenceList](#evidencelist) | Evidence contains a list of infractions committed by validators. | Can be empty, but when populated the validations rules from [evidenceList](#evidencelist) apply |
| LastCommit | [Commit](#commit) | `LastCommit` includes one vote for every validator. All votes must either be for the previous block, nil or absent. If a vote is for the previous block it must have a valid signature from the corresponding validator. The sum of the voting power of the validators that voted must be greater than 2/3 of the total voting power of the complete validator set. The number of votes in a commit is limited to 10000 (see `types.MaxVotesCount`). | Must be empty for the initial height and must adhere to the validation rules of [commit](#commit). |
## Execution
@@ -142,7 +142,7 @@ versioning that this can refer to)
| Name | type | Description | Validation |
|-------|--------|-----------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------|
| Block | uint64 | This number represents the version of the block protocol and must be the same throughout an operational network | Must be equal to protocol version being used in a network (`block.Version.Block == state.Version.Consensus.Block`) |
| App | uint64 | App version is decided on by the application. Read [here](../abci/abci.md#info) | `block.Version.App == state.Version.Consensus.App` |
| App | uint64 | App version is decided on by the application. Read [here](https://github.com/tendermint/tendermint/blob/main/spec/abci/abci++_app_requirements.md) | `block.Version.App == state.Version.Consensus.App` |
## BlockID
@@ -151,7 +151,7 @@ The `BlockID` contains two distinct Merkle roots of the block. The `BlockID` inc
| Name | Type | Description | Validation |
|---------------|---------------------------------|------------------------------------------------------------------------------------------------------------------------------------------------------------------|------------------------------------------------------------------------|
| Hash | slice of bytes (`[]byte`) | MerkleRoot of all the fields in the header (ie. `MerkleRoot(header)`. | hash must be of length 32 |
| PartSetHeader | [PartSetHeader](#PartSetHeader) | Used for secure gossiping of the block during consensus, is the MerkleRoot of the complete serialized block cut into parts (ie. `MerkleRoot(MakeParts(block))`). | Must adhere to the validation rules of [PartSetHeader](#PartSetHeader) |
| PartSetHeader | [PartSetHeader](#partsetheader) | Used for secure gossiping of the block during consensus, is the MerkleRoot of the complete serialized block cut into parts (ie. `MerkleRoot(MakeParts(block))`). | Must adhere to the validation rules of [PartSetHeader](#partsetheader) |
See [MerkleRoot](./encoding.md#MerkleRoot) for details.
@@ -236,7 +236,7 @@ The vote includes information about the validator signing it. When stored in the
| Height | uint64 | Height for which this vote was created for | Must be > 0 |
| Round | int32 | Round that the commit corresponds to. | Must be > 0 |
| BlockID | [BlockID](#blockid) | The blockID of the corresponding block. | [BlockID](#blockid) |
| Timestamp | [Time](#Time) | Timestamp represents the time at which a validator signed. | [Time](#time) |
| Timestamp | [Time](#time) | Timestamp represents the time at which a validator signed. | [Time](#time) |
| ValidatorAddress | slice of bytes (`[]byte`) | Address of the validator | Length must be equal to 20 |
| ValidatorIndex | int32 | Index at a specific block height that corresponds to the Index of the validator in the set. | must be > 0 |
| Signature | slice of bytes (`[]byte`) | Signature by the validator if they participated in consensus for the associated bock. | Length of signature must be > 0 and < 64 |
@@ -291,7 +291,7 @@ is locked in POLRound. The message is signed by the validator private key.
| Round | int32 | Round that the commit corresponds to. | Must be > 0 |
| POLRound | int64 | Proof of lock | Must be > 0 |
| BlockID | [BlockID](#blockid) | The blockID of the corresponding block. | [BlockID](#blockid) |
| Timestamp | [Time](#Time) | Timestamp represents the time at which a validator signed. | [Time](#time) |
| Timestamp | [Time](#time) | Timestamp represents the time at which a validator signed. | [Time](#time) |
| Signature | slice of bytes (`[]byte`) | Signature by the validator if they participated in consensus for the associated bock. | Length of signature must be > 0 and < 64 |
## SignedMsgType
@@ -342,7 +342,7 @@ in the same round of the same height. Votes are lexicographically sorted on `Blo
| VoteB | [Vote](#vote) | The second vote submitted by a validator when they equivocated | VoteB must adhere to [Vote](#vote) validation rules |
| TotalVotingPower | int64 | The total power of the validator set at the height of equivocation | Must be equal to nodes own copy of the data |
| ValidatorPower | int64 | Power of the equivocating validator at the height | Must be equal to the nodes own copy of the data |
| Timestamp | [Time](#Time) | Time of the block where the equivocation occurred | Must be equal to the nodes own copy of the data |
| Timestamp | [Time](#time) | Time of the block where the equivocation occurred | Must be equal to the nodes own copy of the data |
### LightClientAttackEvidence
@@ -353,11 +353,11 @@ and Amnesia. These attacks are exhaustive. You can find a more detailed overview
| Name | Type | Description | Validation |
|----------------------|------------------------------------|----------------------------------------------------------------------|------------------------------------------------------------------|
| ConflictingBlock | [LightBlock](#LightBlock) | Read Below | Must adhere to the validation rules of [lightBlock](#lightblock) |
| ConflictingBlock | [LightBlock](#lightblock) | Read Below | Must adhere to the validation rules of [lightBlock](#lightblock) |
| CommonHeight | int64 | Read Below | must be > 0 |
| Byzantine Validators | Array of [Validators](#Validators) | validators that acted maliciously | Read Below |
| Byzantine Validators | Array of [Validators](#validator) | validators that acted maliciously | Read Below |
| TotalVotingPower | int64 | The total power of the validator set at the height of the infraction | Must be equal to the nodes own copy of the data |
| Timestamp | [Time](#Time) | Time of the block where the infraction occurred | Must be equal to the nodes own copy of the data |
| Timestamp | [Time](#time) | Time of the block where the infraction occurred | Must be equal to the nodes own copy of the data |
## LightBlock
@@ -376,7 +376,7 @@ The SignedhHeader is the [header](#header) accompanied by the commit to prove it
| Name | Type | Description | Validation |
|--------|-------------------|-------------------|-----------------------------------------------------------------------------------|
| Header | [Header](#Header) | [Header](#header) | Header cannot be nil and must adhere to the [Header](#Header) validation criteria |
| Header | [Header](#header) | [Header](#header) | Header cannot be nil and must adhere to the [Header](#header) validation criteria |
| Commit | [Commit](#commit) | [Commit](#commit) | Commit cannot be nil and must adhere to the [Commit](#commit) criteria |
## ValidatorSet

12
spec/light-client/README.md
View File

@@ -19,20 +19,20 @@ verifying a minimal set of data from a network of full nodes (at least one of wh
The light client is decomposed into two main components:
- [Commit Verification](#Commit-Verification) - verify signed headers and associated validator
- [Commit Verification](#commit-verification) - verify signed headers and associated validator
set changes from a single full node, called primary
- [Attack Detection](#Attack-Detection) - verify commits across multiple full nodes (called secondaries) and detect conflicts (ie. the existence of a lightclient attack)
- [Attack Detection](#attack-detection) - verify commits across multiple full nodes (called secondaries) and detect conflicts (ie. the existence of a lightclient attack)
In case a lightclient attack is detected, the lightclient submits evidence to a full node which is responsible for "accountability", that is, punishing attackers:
- [Accountability](#Accountability) - given evidence for an attack, compute a set of validators that are responsible for it.
- [Accountability](#accountability) - given evidence for an attack, compute a set of validators that are responsible for it.
## Commit Verification
The [English specification](verification/verification_001_published.md) describes the light client
commit verification problem in terms of the temporal properties
[LCV-DIST-SAFE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification_001_published.md#lcv-dist-safe1) and
[LCV-DIST-LIVE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification_001_published.md#lcv-dist-live1).
[LCV-DIST-SAFE.1](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe1) and
[LCV-DIST-LIVE.1](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-live1).
Commit verification is assumed to operate within the Tendermint Failure Model, where +2/3 of validators are correct for some time period and
validator sets can change arbitrarily at each height.
@@ -136,7 +136,7 @@ termination, which can be model checked with Apalache.
The `LCD_MC*.tla` files contain concrete parameters for the
[TLA+ specification](detection/LCDetector_003_draft.tla),
in order to run the model checker.
For instance, [LCD_MC4_4_faulty.tla](detection/MC4_4_faulty.tla)
For instance, [LCD_MC4_4_faulty.tla](./verification/MC4_4_faulty.tla)
contains the following parameters
for the nodes, heights, the trusting period, the clock drifts,
correctness of the nodes, and the ratio of the faulty processes:

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

@@ -207,7 +207,9 @@ Execution:
*Remark.* In this case, the more than 1/3 of faulty validators do not need to commit an equivocation (F1) as they only vote once per round in the execution.
Detecting faulty validators in the case of such an attack can be done by the fork accountability mechanism described in: <https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit?usp=sharing>.
Detecting faulty validators in the case of such an attack can be done by the fork accountability mechanism described in:
<!-- markdown-link-check-disable-next-line -->
<https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit?usp=sharing>.
If a light client is attacked using this attack with 1/3 or more of voting power (and less than 2/3), the attacker cannot change the application state arbitrarily. Rather, the attacker is limited to a state a correct validator finds acceptable: In the execution above, correct validators still find the value acceptable, however, the block the light client trusts deviates from the one on the main chain.
@@ -231,7 +233,7 @@ Consequences:
* The validators in F1 will be detectable by the the fork accountability mechanisms.
* The validators in F2 cannot be detected using this mechanism.
Only in case they signed something which conflicts with the application this can be used against them. Otherwise they do not do anything incorrect.
Only in case they signed something which conflicts with the application this can be used against them. Otherwise they do not do anything incorrect. <!-- markdown-link-check-disable-next-line -->
* This case is not covered by the report <https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit?usp=sharing> as it only assumes at most 2/3 of faulty validators.
**Q:** do we need to define a special kind of attack for the case where a validator sign arbitrarily state? It seems that detecting such attack requires a different mechanism that would require as an evidence a sequence of blocks that led to that state. This might be very tricky to implement.

8
spec/light-client/attacks/isolate-attackers_001_draft.md
View File

@@ -1,4 +1,4 @@
<!-- markdown-link-check-disable -->
# Lightclient Attackers Isolation
> Warning: This is the beginning of an unfinished draft. Don't continue reading!
@@ -200,12 +200,12 @@ First observe that the first checking in `isolateMisbehavingProcesses` is `viola
[[detection]] The specification of the light client attack detection mechanism.
[supervisor]:
https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/supervisor/supervisor_001_draft.md
https://github.com/tendermint/tendermint/tree/main/spec/light-client/supervisor
[verification]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md
[verification]: https://github.com/tendermint/tendermint/tree/main/spec/light-client/verification
[detection]:
https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md
https://github.com/tendermint/tendermint/tree/main/spec/light-client/detection
[LC-DATA-EVIDENCE-link]:
https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md#lc-data-evidence1

5
spec/light-client/attacks/isolate-attackers_002_reviewed.md
View File

@@ -1,3 +1,4 @@
<!-- markdown-link-check-disable -->
# Lightclient Attackers Isolation
Adversarial nodes may have the incentive to lie to a lightclient about the state of a Tendermint blockchain. An attempt to do so is called attack. Light client [verification][verification] checks incoming data by checking a so-called "commit", which is a forwarded set of signed messages that is (supposedly) produced during executing Tendermint consensus. Thus, an attack boils down to creating and signing Tendermint consensus messages in deviation from the Tendermint consensus algorithm rules.
@@ -65,7 +66,7 @@ Here we discuss how to solve the problem of isolating misbehaving processes. We
### Outline
We first check whether the conflicting block can indeed be verified from the common height. We then first check whether it was a lunatic attack (violating validity). If this is not the case, we check for equivocation. If this also is not the case, we start the on-chain [accountability protocol](https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit).
We first check whether the conflicting block can indeed be verified from the common height. We then first check whether it was a lunatic attack (violating validity). If this is not the case, we check for equivocation. If this also is not the case, we start the on-chain <!-- markdown-link-check-disable-next-line -->[accountability protocol](https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit).
#### **[LCAI-FUNC-MAIN.1]**
@@ -144,7 +145,7 @@ func violatesTMValidity(ref Header, ev Header) boolean
func IsolateAmnesiaAttacker(ev LightClientAttackEvidence, bc Blockchain) []ValidatorAddress
```
- Implementation remarks
- Implementation remarks <!-- markdown-link-check-disable-next-line -->
- This triggers the [query/response protocol](https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit).
- Expected postcondition
- returns attackers according to [LCAI-INV-Output.1].

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

@@ -14,7 +14,7 @@ This directory captures the ongoing work and discussion on fork
detection both in the context of a Tendermint light node and in the
context of IBC. It contains the following files
### [detection.md](./detection.md)
### [detection.md](./detection_003_reviewed.md)
a draft of the light node fork detection including "proof of fork"
definition, that is, the data structure to submit evidence to full

1
spec/light-client/detection/detection_001_reviewed.md
View File

@@ -1,3 +1,4 @@
<!-- markdown-link-check-disable -->
# ***This an unfinished draft. Comments are welcome!***
**TODO:** We will need to do small adaptations to the verification

1
spec/light-client/detection/detection_003_reviewed.md
View File

@@ -1,3 +1,4 @@
<!-- markdown-link-check-disable -->
# Light Client Attack Detector
In this specification, we strengthen the light client to be resistant

2
spec/light-client/detection/draft-functions.md
View File

@@ -3,7 +3,7 @@
This document collects drafts of function for generating and
submitting proof of fork in the IBC context
- [IBC](#on---chain-ibc-component)
- [IBC](#on-chain-ibc-component)
- [Relayer](#relayer)

2
spec/light-client/detection/req-ibc-detection.md
View File

@@ -4,7 +4,7 @@
In the following, I distilled what I considered relevant from
<https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics>
<https://github.com/cosmos/ibc>
### Components and their interface

2
spec/light-client/supervisor/supervisor_001_draft.md
View File

@@ -7,7 +7,7 @@ verification specification. So some hyperlinks have to be placed to
the correct files eventually.
# Light Client Sequential Supervisor
<!-- markdown-link-check-disable -->
The light client implements a read operation of a
[header](TMBC-HEADER-link) from the [blockchain](TMBC-SEQ-link), by
communicating with full nodes, a so-called primary and several

4
spec/light-client/verification/README.md
View File

@@ -27,7 +27,7 @@ Given a known bound `TRUSTED_PERIOD`, and a block `b` with header `h` generated
in `validators(b.Header.NextValidatorsHash)` is correct until time `b.Header.Time + TRUSTED_PERIOD`.
*Assumption*: "correct" is defined w.r.t. realtime (some Newtonian global notion of time, i.e., wall time),
while `Header.Time` corresponds to the [BFT time](../consensus/bft-time.md). In this note, we assume that clocks of correct processes
while `Header.Time` corresponds to the [BFT time](../../consensus/bft-time.md). In this note, we assume that clocks of correct processes
are synchronized (for example using NTP), and therefore there is bounded clock drift (`CLOCK_DRIFT`) between local clocks and
BFT time. More precisely, for every correct light client process and every `header.Time` (i.e. BFT Time, for a header correctly
generated by the Tendermint consensus), the following inequality holds: `Header.Time < now + CLOCK_DRIFT`,
@@ -47,7 +47,7 @@ Mechanisms like `fork accountability` and `evidence submission` are defined in t
they incentivize validators to follow the protocol specification defined in this document. If they don't,
and we have 1/3 (or more) faulty validators, safety may be violated. Our approach then is
to *detect* these cases (after the fact), and take suitable repair actions (automatic and social).
This is discussed in document on [Fork accountability](./accountability.md).
This is discussed in document on [Fork accountability](../../consensus/light-client/accountability.md).
The term "trusted" above indicates that the correctness of the protocol depends on
this assumption. It is in the responsibility of the user that runs the light client to make sure that the risk

52
spec/light-client/verification/verification_001_published.md
View File

@@ -1,14 +1,14 @@
# Light Client Verification
The light client implements a read operation of a
[header][TMBC-HEADER-link] from the [blockchain][TMBC-SEQ-link], by
[header][#tmbc-header1] from the [blockchain][tmbc-seq1], by
communicating with full nodes. As some full nodes may be faulty, this
functionality must be implemented in a fault-tolerant way.
In the Tendermint blockchain, the validator set may change with every
new block. The staking and unbonding mechanism induces a [security
model][TMBC-FM-2THIRDS-link]: starting at time *Time* of the
[header][TMBC-HEADER-link],
[header][#tmbc-header1],
more than two-thirds of the next validators of a new block are correct
for the duration of *TrustedPeriod*. The fault-tolerant read
operation is designed for this security model.
@@ -19,7 +19,7 @@ greater than *h1*. Checking all headers of heights from *h1* to *h2*
might be too costly (e.g., in terms of energy for mobile devices).
This specification tries to reduce the number of intermediate blocks
that need to be checked, by exploiting the guarantees provided by the
[security model][TMBC-FM-2THIRDS-link].
[security model][tmbc-fm-2thirds1].
# Status
@@ -46,10 +46,10 @@ blockchain.
- [Part II](#part-ii---sequential-definition-of-the-verification-problem): Introduction
of the problem addressed by the Lightclient Verification protocol.
- [Verification Informal Problem
statement](#Verification-Informal-Problem-statement): For the general
statement](#verification-informal-problem-statement): For the general
audience, that is, engineers who want to get an overview over what
the component is doing from a bird's eye view.
- [Sequential Problem statement](#Sequential-Problem-statement):
- [Sequential Problem statement](#sequential-problem-statement):
Provides a mathematical definition of the problem statement in
its sequential form, that is, ignoring the distributed aspect of
the implementation of the blockchain.
@@ -61,17 +61,17 @@ of the problem addressed by the Lightclient Verification protocol.
- [Incentives](#incentives): how faulty full nodes may benefit from
misbehaving and how correct full nodes benefit from cooperating.
- [Computational Model](#Computational-Model):
- [Computational Model](#computational-model):
timing and correctness assumptions.
- [Distributed Problem Statement](#Distributed-Problem-Statement):
- [Distributed Problem Statement](#distributed-problem-statement):
temporal properties that formalize safety and liveness
properties in the distributed setting.
- [Part IV](#part-iv---light-client-verification-protocol):
Specification of the protocols.
- [Definitions](#Definitions): Describes inputs, outputs,
- [Definitions](#definitions): Describes inputs, outputs,
variables used by the protocol, auxiliary functions
- [Core Verification](#core-verification): gives an outline of the solution,
@@ -406,9 +406,9 @@ Each instance must eventually terminate.
> These definitions imply that if the primary is faulty, a header may or
> may not be added to *LightStore*. In any case,
> [**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) must hold.
> The invariant [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe) and the liveness
> requirement [**[LCV-DIST-LIVE.1]**](#lcv-dist-life)
> [**[LCV-DIST-SAFE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe1) must hold.
> The invariant [**[LCV-DIST-SAFE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe1) and the liveness
> requirement [**[LCV-DIST-LIVE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-life1)
> allow that verified headers are added to *LightStore* whose
> height was not passed
> to the verifier (e.g., intermediate headers used in bisection; see below).
@@ -425,16 +425,16 @@ Each instance must eventually terminate.
This specification provides a partial solution to the sequential specification.
The *Verifier* solves the invariant of the sequential part
[**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) => [**[LCV-SEQ-SAFE.1]**](#lcv-seq-inv)
[**[LCV-DIST-SAFE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe1) => [**[LCV-SEQ-SAFE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-seq-inv)
In the case the primary is correct, and there is a recent header in *LightStore*, the verifier satisfies the liveness requirements.
⋀ *primary is correct*
⋀ always ∃ verified header in LightStore. *header.Time* > *now* - *trustingPeriod*
⋀ [**[LCV-A-Comm.1]**](#lcv-a-comm) ⋀ (
⋀ [**[LCV-A-Comm.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-a-comm) ⋀ (
( [**[TMBC-CorrFull.1]**][TMBC-CorrFull-link] ⋀
[**[LCV-DIST-LIVE.1]**](#lcv-vc-live) )
⟹ [**[LCV-SEQ-LIVE.1]**](#lcv-seq-live)
[**[LCV-DIST-LIVE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-live1) )
⟹ [**[LCV-SEQ-LIVE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-seq-live1)
)
# Part IV - Light Client Verification Protocol
@@ -767,7 +767,7 @@ func VerifyToTarget(primary PeerID, lightStore LightStore,
- Error conditions
- if the precondition is violated
- if `ValidAndVerified` or `FetchLightBlock` report an error
- if [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) is violated
- if [**[LCV-INV-TP.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-inv-tp1) is violated
### Details of the Functions
@@ -854,7 +854,7 @@ func Schedule(lightStore, nextHeight, targetHeight) Height
*trustedStore* is implemented by the light blocks in lightStore that
have the state *StateVerified*.
#### Argument for [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe)
#### Argument for [**[LCV-DIST-SAFE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe)
- `ValidAndVerified` implements the soundness checks and the checks
[**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] and
@@ -863,7 +863,7 @@ have the state *StateVerified*.
- Only if `ValidAndVerified` returns with `SUCCESS`, the state of a light block is
set to *StateVerified*.
#### Argument for [**[LCV-DIST-LIVE.1]**](#lcv-dist-life)
#### Argument for [**[LCV-DIST-LIVE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-life)
- If *primary* is correct,
- `FetchLightBlock` will always return a light block consistent
@@ -871,7 +871,7 @@ have the state *StateVerified*.
- `ValidAndVerified` either verifies the header using the trusting
period or falls back to sequential
verification
- If [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) holds, eventually every
- If [**[LCV-INV-TP.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-inv-tp1) holds, eventually every
header will be verified and core verification **terminates successfully**.
- successful termination depends on the age of *lightStore.LatestVerified*
(for instance, initially on the age of *trustedHeader*) and the
@@ -887,7 +887,7 @@ have the state *StateVerified*.
## Liveness Scenarios
The liveness argument above assumes [**[LCV-INV-TP.1]**](#LCV-INV-TP.1)
The liveness argument above assumes [**[LCV-INV-TP.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-inv-tp1)
which requires that there is a header that does not expire before the
target height is reached. Here we discuss scenarios to ensure this.
@@ -1163,16 +1163,12 @@ func Main (primary PeerID, lightStore LightStore, targetHeight Height)
[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1
[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md
[fork-detector]: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/detection.md
[fullnode]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/fullnode.md
[fork-detector]: https://github.com/tendermint/tendermint/tree/main/spec/light-client/detection
[fullnode]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain
[ibc-rs]:https://github.com/informalsystems/ibc-rs
[FN-LuckyCase-link]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/fullnode.md#fn-luckycase
[blockchain-validator-set]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/blockchain.md#data-structures
[fullnode-data-structures]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/fullnode.md#data-structures
[FN-ManifestFaulty-link]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/fullnode.md#fn-manifestfaulty
[blockchain-validator-set]: https://github.com/tendermint/tendermint/blob/main/spec/core/data_structures.md#validatorset
[fullnode-data-structures]: https://github.com/tendermint/tendermint/blob/main/spec/core/data_structures.md
[arXiv]: https://arxiv.org/abs/1807.04938

40
spec/light-client/verification/verification_002_draft.md
View File

@@ -63,10 +63,10 @@ blockchain.
- [Part II](#part-ii---sequential-definition-of-the-verification-problem): Introduction
of the problem addressed by the Lightclient Verification protocol.
- [Verification Informal Problem
statement](#Verification-Informal-Problem-statement): For the general
statement](#verification-informal-problem-statement): For the general
audience, that is, engineers who want to get an overview over what
the component is doing from a bird's eye view.
- [Sequential Problem statement](#Sequential-Problem-statement):
- [Sequential Problem statement](#sequential-problem-statement):
Provides a mathematical definition of the problem statement in
its sequential form, that is, ignoring the distributed aspect of
the implementation of the blockchain.
@@ -78,17 +78,17 @@ of the problem addressed by the Lightclient Verification protocol.
- [Incentives](#incentives): how faulty full nodes may benefit from
misbehaving and how correct full nodes benefit from cooperating.
- [Computational Model](#Computational-Model):
- [Computational Model](#computational-model):
timing and correctness assumptions.
- [Distributed Problem Statement](#Distributed-Problem-Statement):
- [Distributed Problem Statement](#distributed-problem-statement):
temporal properties that formalize safety and liveness
properties in the distributed setting.
- [Part IV](#part-iv---light-client-verification-protocol):
Specification of the protocols.
- [Definitions](#Definitions): Describes inputs, outputs,
- [Definitions](#definitions): Describes inputs, outputs,
variables used by the protocol, auxiliary functions
- [Core Verification](#core-verification): gives an outline of the solution,
@@ -420,9 +420,9 @@ must eventually terminate.
> These definitions imply that if the primary is faulty, a header may or
> may not be added to *LightStore*. In any case,
> [**[LCV-DIST-SAFE.2]**](#lcv-dist-safe2) must hold.
> The invariant [**[LCV-DIST-SAFE.2]**](#lcv-dist-safe2) and the liveness
> requirement [**[LCV-DIST-LIVE.2]**](#lcv-dist-life)
> [**[LCV-DIST-SAFE.2]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe2) must hold.
> The invariant [**[LCV-DIST-SAFE.2]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe2) and the liveness
> requirement [**[LCV-DIST-LIVE.2]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-life)
> allow that verified headers are added to *LightStore* whose
> height was not passed
> to the verifier (e.g., intermediate headers used in bisection; see below).
@@ -439,16 +439,16 @@ must eventually terminate.
This specification provides a partial solution to the sequential specification.
The *Verifier* solves the invariant of the sequential part
[**[LCV-DIST-SAFE.2]**](#lcv-dist-safe2) => [**[LCV-SEQ-SAFE.1]**](#lcv-seq-safe1)
[**[LCV-DIST-SAFE.2]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe2) => [**[LCV-SEQ-SAFE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe1)
In the case the primary is correct, and *root* is a recent header in *LightStore*, the verifier satisfies the liveness requirements.
⋀ *primary is correct*
⋀ *root.header.Time* > *now* - *trustingPeriod*
⋀ [**[LCV-A-Comm.1]**](#lcv-a-comm) ⋀ (
⋀ [**[LCV-A-Comm.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-a-comm) ⋀ (
( [**[TMBC-CorrFull.1]**][TMBC-CorrFull-link] ⋀
[**[LCV-DIST-LIVE.2]**](#lcv-dist-live2) )
⟹ [**[LCV-SEQ-LIVE.1]**](#lcv-seq-live1)
[**[LCV-DIST-LIVE.2]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-live2) )
⟹ [**[LCV-SEQ-LIVE.1]**](https://github.com/tendermint/tendermint/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-live1)
)
# Part IV - Light Client Verification Protocol
@@ -612,7 +612,7 @@ func (ls LightStore) TraceTo(lightBlock LightBlock) (LightBlock, LightStore)
- returns a **trusted** lightblock `root` from the lightstore with a height
less than `lightBlock`
- returns a lightstore that contains lightblocks that constitute a
[verification trace](TODOlinkToDetectorSpecOnceThere) from
[verification trace](https://github.com/tendermint/tendermint/tree/main/spec/light-client/detection) from
`root` to `lightBlock` (including `lightBlock`)
### Inputs
@@ -823,7 +823,7 @@ func VerifyToTarget(primary PeerID, root LightBlock,
- Error conditions
- if the precondition is violated
- if `ValidAndVerified` or `FetchLightBlock` report an error
- if [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) is violated
- if [**[LCV-INV-TP.1]**](#lcv-inv-tp1) is violated
### Details of the Functions
@@ -927,14 +927,14 @@ For [IBC][ibc-rs] there are two additional challenges:
1. it might be that some "older" header is needed, that is,
*targetHeight < lightStore.LatestVerified()*. The
[supervisor](../supervisor/supervisor.md) checks whether it is in this
[supervisor](../supervisor/supervisor_002_draft.md) checks whether it is in this
case by calling `LatestPrevious` and `MinVerified` and if so it calls
`Backwards`. All these functions are specified below.
2. In order to submit proof of a light client attack, a relayer may
need to submit a verification trace. This it is important to
compute such a trace efficiently. That it can be done is based on
the invariant [[LCV-INV-LS-ROOT.2]](#LCV-INV-LS-ROOT2) that needs
the invariant [[LCV-INV-LS-ROOT.2]](#lcv-inv-ls-root2) that needs
to be maintained by the light client. In particular
`VerifyToTarget` and `Backwards` need to take care of setting
`verification-root`.
@@ -1048,14 +1048,12 @@ func Backwards (primary PeerID, root LightBlock, targetHeight Height)
[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1
[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md
[attack-detector]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_001_reviewed.md
[fullnode]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/fullnode.md
[attack-detector]: https://github.com/tendermint/tendermint/blob/main/spec/light-client/detection/detection_001_reviewed.md
[fullnode]: https://github.com/tendermint/tendermint/tree/main/spec/core
[ibc-rs]:https://github.com/informalsystems/ibc-rs
[blockchain-validator-set]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/blockchain.md#data-structures
[fullnode-data-structures]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/fullnode.md#data-structures
[FN-ManifestFaulty-link]: https://github.com/tendermint/tendermint/blob/main/spec/blockchain/fullnode.md#fn-manifestfaulty
[fullnode-data-structures]: https://github.com/tendermint/tendermint/blob/main/spec/core/data_structures.md
[arXiv]: https://arxiv.org/abs/1807.04938

2
spec/p2p/messages/consensus.md
View File

@@ -144,6 +144,6 @@ Message is a [`oneof` protobuf type](https://developers.google.com/protocol-buff
| proposal_pol | [ProposalPOL](#proposalpol) | | 4 |
| block_part | [BlockPart](#blockpart) | | 5 |
| vote | [Vote](#vote) | | 6 |
| received_vote | [ReceivedVote](#ReceivedVote) | | 7 |
| received_vote | [ReceivedVote](#receivedvote) | | 7 |
| vote_set_maj23 | [VoteSetMaj23](#votesetmaj23) | | 8 |
| vote_set_bits | [VoteSetBits](#votesetbits) | | 9 |

12
spec/p2p/messages/pex.md
View File

@@ -29,7 +29,7 @@ PexResponse is an list of net addresses provided to a peer to dial.
| Name | Type | Description | Field Number |
|-------|------------------------------------|------------------------------------------|--------------|
| addresses | repeated [PexAddress](#PexAddress) | List of peer addresses available to dial | 1 |
| addresses | repeated [PexAddress](#pexaddress) | List of peer addresses available to dial | 1 |
### PexAddress
@@ -54,7 +54,7 @@ PexResponse is an list of net addresses provided to a peer to dial.
| Name | Type | Description | Field Number |
|-------|------------------------------------|------------------------------------------|--------------|
| addresses | repeated [PexAddressV2](#PexAddressV2) | List of peer addresses available to dial | 1 |
| addresses | repeated [PexAddressV2](#pexresponsev2) | List of peer addresses available to dial | 1 |
### PexAddressV2
@@ -70,7 +70,7 @@ Message is a [`oneof` protobuf type](https://developers.google.com/protocol-buff
| Name | Type | Description | Field Number |
|--------------|---------------------------|------------------------------------------------------|--------------|
| pex_request | [PexRequest](#PexRequest) | Empty request asking for a list of addresses to dial | 1 |
| pex_response | [PexResponse](#PexResponse) | List of addresses to dial | 2 |
| pex_request_v2 | [PexRequestV2](#PexRequestV2) | Empty request asking for a list of addresses to dial | 3 |
| pex_response_v2 | [PexRespinseV2](#PexResponseV2) | List of addresses to dial | 4 |
| pex_request | [PexRequest](#pexrequest) | Empty request asking for a list of addresses to dial | 1 |
| pex_response | [PexResponse](#pexresponse)| List of addresses to dial | 2 |
| pex_request_v2| [PexRequestV2](#pexrequestv2)| Empty request asking for a list of addresses to dial| 3 |
| pex_response_v2| [PexRespinseV2](#pexresponsev2)| List of addresses to dial | 4 |

3
spec/p2p/messages/state-sync.md
View File

@@ -91,10 +91,9 @@ if necessary. The light block at the height of the snapshot will be used to veri
|---------------|---------------------------------------------------------|--------------------------------------|--------------|
| light_block | [LightBlock](../../core/data_structures.md#lightblock) | Light block at the height requested | 1 |
State sync will use [light client verification](../../light-client/verification/README.md) to verify
State sync will use [light client verification](../../../spec/light-client/verification/README.md) to verify
the light blocks.
If no state sync is in progress (i.e. during normal operation), any unsolicited response messages
are discarded.