Skip to content

Commit

Permalink
spec/rename: update branch links main -> v0.37.x
Browse files Browse the repository at this point in the history
  • Loading branch information
cason committed Jan 24, 2023
1 parent dc49c67 commit 5609de6
Show file tree
Hide file tree
Showing 17 changed files with 82 additions and 82 deletions.
2 changes: 1 addition & 1 deletion spec/consensus/light-client/accountability.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
# Fork accountability

Deprecated, please see [light-client/accountability](https://github.com/cometbft/cometbft/blob/main/spec/light-client/accountability).
Deprecated, please see [light-client/accountability](https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/accountability).
2 changes: 1 addition & 1 deletion spec/consensus/light-client/detection.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
# Detection

Deprecated, please see [light-client/detection](https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection).
Deprecated, please see [light-client/detection](https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection).
2 changes: 1 addition & 1 deletion spec/consensus/light-client/verification.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
# Core Verification

Deprecated, please see [light-client/verification](https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification).
Deprecated, please see [light-client/verification](https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification).
Original file line number Diff line number Diff line change
Expand Up @@ -188,4 +188,4 @@ Back to [main document][main].

[arXiv]: https://arxiv.org/abs/1807.04938

[CMBC-FM-2THIRDS-link]: https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#cmbc-fm-2thirds1
[CMBC-FM-2THIRDS-link]: https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#cmbc-fm-2thirds1
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
A TLA+ specification of a simplified Tendermint consensus algorithm, with added clocks
and proposer-based timestamps. This TLA+ specification extends and modifies
the Tendermint TLA+ specification for fork accountability:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/accountability/TendermintAcc_004_draft.tla
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/accountability/TendermintAcc_004_draft.tla
* Version 1. A preliminary specification.
Expand Down
4 changes: 2 additions & 2 deletions spec/core/data_structures.md
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ 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 CometBFT. | 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/cometbft/cometbft/blob/main/spec/abci/abci%2B%2B_methods.md#checktx).
| Data | [Data](#data) | Data contains a list of transactions. The contents of the transaction is unknown to CometBFT. | 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/cometbft/cometbft/blob/v0.37.x/spec/abci/abci%2B%2B_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). |

Expand Down Expand Up @@ -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](https://github.com/cometbft/cometbft/blob/main/spec/abci/abci++_app_requirements.md) | `block.Version.App == state.Version.Consensus.App` |
| App | uint64 | App version is decided on by the application. Read [here](https://github.com/cometbft/cometbft/blob/v0.37.x/spec/abci/abci++_app_requirements.md) | `block.Version.App == state.Version.Consensus.App` |

## BlockID

Expand Down
4 changes: 2 additions & 2 deletions spec/light-client/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,8 @@ In case a lightclient attack is detected, the lightclient submits evidence to a

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/cometbft/cometbft/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-safe1) and
[LCV-DIST-LIVE.1](https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_001_published.md#lcv-dist-live1).
[LCV-DIST-SAFE.1](https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_001_published.md#lcv-dist-safe1) and
[LCV-DIST-LIVE.1](https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_001_published.md#lcv-dist-live1).
Commit verification is assumed to operate within the Cosmos Failure Model, where +2/3 of validators are correct for some time period and
validator sets can change arbitrarily at each height.

Expand Down
2 changes: 1 addition & 1 deletion spec/light-client/attacks/Isolation_001_draft.tla
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
*
* It follows the English specification:
*
* https://github.com/cometbft/cometbft/blob/main/spec/light-client/attacks/isolate-attackers_001_draft.md
* https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/attacks/isolate-attackers_001_draft.md
*
* The assumptions made in this specification:
*
Expand Down
20 changes: 10 additions & 10 deletions spec/light-client/attacks/isolate-attackers_001_draft.md
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ This specification considers how a full node in a Cosmos blockchain can isolate

# Part I - Basics

For definitions of data structures used here, in particular LightBlocks [[LCV-DATA-LIGHTBLOCK.1]](https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#lcv-data-lightblock1), cf. [Light Client Verification][verification].
For definitions of data structures used here, in particular LightBlocks [[LCV-DATA-LIGHTBLOCK.1]](https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#lcv-data-lightblock1), cf. [Light Client Verification][verification].

# Part II - Definition of the Problem

Expand Down Expand Up @@ -191,7 +191,7 @@ The main function `isolateMisbehavingProcesses` distinguishes three kinds of wro
The question is whether this captures all attacks.
First observe that the first checking in `isolateMisbehavingProcesses` is `violatesTMValidity`. It takes care of lunatic attacks. If this check passes, that is, if `violatesTMValidity` returns `FALSE` this means that [FN-NONVALID-OUTPUT] evaluates to false, which implies that `ref.ValidatorsHash = ev.ValidatorsHash`. Hence after `violatesTMValidity`, all the involved validators are the ones from the blockchain. It is thus sufficient to analyze one instance of Tendermint consensus with a fixed group membership (set of validators). Also it is sufficient to consider two different valid consensus values, that is, binary consensus.

**TODO** we have analyzed Tendermint consensus algorithm with TLA+ and have accompanied Galois in an independent study of the protocol based on [Ivy proofs](https://github.com/cometbft/cometbft/tree/main/spec/ivy-proofs).
**TODO** we have analyzed Tendermint consensus algorithm with TLA+ and have accompanied Galois in an independent study of the protocol based on [Ivy proofs](https://github.com/cometbft/cometbft/tree/v0.37.x/spec/ivy-proofs).

# References

Expand All @@ -202,22 +202,22 @@ First observe that the first checking in `isolateMisbehavingProcesses` is `viola
[[detection]] The specification of the light client attack detection mechanism.

[supervisor]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/supervisor/supervisor_001_draft.md
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/supervisor/supervisor_001_draft.md

[verification]: https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md
[verification]: https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md

[detection]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md

[LC-DATA-EVIDENCE-link]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md#lc-data-evidence1
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md#lc-data-evidence1

[CMBC-LC-EVIDENCE-DATA-link]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md#cmbc-lc-evidence-data1
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md#cmbc-lc-evidence-data1

[node-based-attack-characterization]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md#block-based-characterization-of-attacks
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md#block-based-characterization-of-attacks

[CMBC-FM-2THIRDS-link]: https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#cmbc-fm-2thirds1
[CMBC-FM-2THIRDS-link]: https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#cmbc-fm-2thirds1

[LCV-FUNC-VALID.link]: https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#lcv-func-valid2
[LCV-FUNC-VALID.link]: https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#lcv-func-valid2
22 changes: 11 additions & 11 deletions spec/light-client/attacks/isolate-attackers_002_reviewed.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ After providing the [problem statement](#Part-I---Basics-and-Definition-of-the-P

# Part I - Basics and Definition of the Problem

For definitions of data structures used here, in particular LightBlocks [[LCV-DATA-LIGHTBLOCK.1]](https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#lcv-data-lightblock1), we refer to the specification of [Light Client Verification][verification].
For definitions of data structures used here, in particular LightBlocks [[LCV-DATA-LIGHTBLOCK.1]](https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#lcv-data-lightblock1), we refer to the specification of [Light Client Verification][verification].

The specification of the [detection mechanism][detection] describes

Expand Down Expand Up @@ -189,7 +189,7 @@ The main function `isolateMisbehavingProcesses` distinguishes three kinds of wro
The question is whether this captures all attacks.
First observe that the first check in `isolateMisbehavingProcesses` is `violatesTMValidity`. It takes care of lunatic attacks. If this check passes, that is, if `violatesTMValidity` returns `FALSE` this means that [[LCAI-NONVALID-OUTPUT.1]](#LCAI-FUNC-NONVALID1]) evaluates to false, which implies that `ref.ValidatorsHash = ev.ValidatorsHash`. Hence, after `violatesTMValidity`, all the involved validators are the ones from the blockchain. It is thus sufficient to analyze one instance of Tendermint consensus with a fixed group membership (set of validators). Also, as we have two different blocks for the same height, it is sufficient to consider two different valid consensus values, that is, binary consensus.

For this fixed group membership, we have analyzed the attacks using the TLA+ specification of [Tendermint Consensus in TLA+][tendermint-accountability]. We checked that indeed the only possible scenarios that can lead to violation of agreement are **equivocation** and **amnesia**. An independent study by Galois of the protocol based on [Ivy proofs](https://github.com/cometbft/cometbft/tree/main/spec/ivy-proofs) led to the same conclusion.
For this fixed group membership, we have analyzed the attacks using the TLA+ specification of [Tendermint Consensus in TLA+][tendermint-accountability]. We checked that indeed the only possible scenarios that can lead to violation of agreement are **equivocation** and **amnesia**. An independent study by Galois of the protocol based on [Ivy proofs](https://github.com/cometbft/cometbft/tree/v0.37.x/spec/ivy-proofs) led to the same conclusion.

# References

Expand All @@ -201,25 +201,25 @@ For this fixed group membership, we have analyzed the attacks using the TLA+ spe


[tendermint-accountability]:
https://github.com/cometbft/cometbft/tree/main/spec/light-client/accountability
https://github.com/cometbft/cometbft/tree/v0.37.x/spec/light-client/accountability

[supervisor]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/supervisor/supervisor_001_draft.md
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/supervisor/supervisor_001_draft.md

[verification]: https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md
[verification]: https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md

[detection]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md

[LC-DATA-EVIDENCE-link]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md#lc-data-evidence1
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md#lc-data-evidence1

[CMBC-LC-EVIDENCE-DATA-link]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md#cmbc-lc-evidence-data1
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md#cmbc-lc-evidence-data1

[node-based-attack-characterization]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md#block-based-characterization-of-attacks
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md#block-based-characterization-of-attacks

[CMBC-FM-2THIRDS-link]: https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#cmbc-fm-2thirds1
[CMBC-FM-2THIRDS-link]: https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#cmbc-fm-2thirds1

[LCV-FUNC-VALID.link]: https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#lcv-func-valid2
[LCV-FUNC-VALID.link]: https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#lcv-func-valid2
4 changes: 2 additions & 2 deletions spec/light-client/attacks/notes-on-evidence-handling.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ detects an attack, it needs to send to a witness only missing data (common heigh
and conflicting light block) as it has its trace. Keeping light client attack data of constant size
saves bandwidth and reduces an attack surface. As we will explain below, although in the context of
light client core
[verification](https://github.com/cometbft/cometbft/tree/main/spec/light-client/verification)
[verification](https://github.com/cometbft/cometbft/tree/v0.37.x/spec/light-client/verification)
the roles of primary and witness are clearly defined,
in case of the attack, we run the same attack detection procedure twice where the roles are swapped.
The rationale is that the light client does not know what peer is correct (on a right main branch)
Expand Down Expand Up @@ -68,7 +68,7 @@ The following invariant holds for the primary trace:
### Witness with a conflicting header

The verified header at height `h` is cross-checked with every witness as part of
[detection](https://github.com/cometbft/cometbft/tree/main/spec/light-client/detection).
[detection](https://github.com/cometbft/cometbft/tree/v0.37.x/spec/light-client/detection).
If a witness returns the conflicting header at the height `h` the following procedure is executed to verify
if the conflicting header comes from the valid trace and if that's the case to create an attack evidence:

Expand Down
2 changes: 1 addition & 1 deletion spec/light-client/detection/LCDetector_003_draft.tla
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
* This is a specification of the light client detector module.
* It follows the English specification:
*
* https://github.com/cometbft/cometbft/blob/main/spec/light-client/detection/detection_003_reviewed.md
* https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/detection/detection_003_reviewed.md
*
* The assumptions made in this specification:
*
Expand Down
10 changes: 5 additions & 5 deletions spec/light-client/detection/detection_001_reviewed.md
Original file line number Diff line number Diff line change
Expand Up @@ -767,19 +767,19 @@ Once a bogus block is recognized as such the secondary is removed.

[[supervisor]] The specification of the light client supervisor.

[verification]: https://github.com/cometbft/cometbft/tree/main/spec/light-client/verification
[verification]: https://github.com/cometbft/cometbft/tree/v0.37.x/spec/light-client/verification

[supervisor]: https://github.com/cometbft/cometbft/tree/main/spec/light-client/supervisor
[supervisor]: https://github.com/cometbft/cometbft/tree/v0.37.x/spec/light-client/supervisor





[CMBC-VAL-CONTAINS-CORR-link]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#cmbc-val-contains-corr1
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#cmbc-val-contains-corr1

[fetch]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#lcv-func-fetch1
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#lcv-func-fetch1

[LCV-INV-TP1-link]:
https://github.com/cometbft/cometbft/blob/main/spec/light-client/verification/verification_002_draft.md#lcv-inv-tp1
https://github.com/cometbft/cometbft/blob/v0.37.x/spec/light-client/verification/verification_002_draft.md#lcv-inv-tp1
Loading

0 comments on commit 5609de6

Please sign in to comment.