Skip to content

Commit

Permalink
Fix broken links in repository (informalsystems#1394)
Browse files Browse the repository at this point in the history
* Fix broken links in repo

* Update docs/architecture/adr-002-ibc-relayer.md

Co-authored-by: Adi Seredinschi <[email protected]>
  • Loading branch information
romac and adizere authored Sep 29, 2021
1 parent 79210ec commit 7b76a1f
Show file tree
Hide file tree
Showing 19 changed files with 60 additions and 61 deletions.
1 change: 1 addition & 0 deletions .changelog/v0.7.1/bug-fixes/1312-fix-gm-stderr.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
<!-- markdown-link-check-disable-next-line -->
- [gm](scripts/gm)
- Fix gaiad keys add prints to stderr instead of stdout in SDK 0.43 ([#1312])
- Bumped default rpc_timeout in Hermes config to 5s ([#1312])
Expand Down
1 change: 1 addition & 0 deletions .changelog/v0.7.2/features/1371-gm-features.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
<!-- markdown-link-check-disable-next-line -->
- [gm](scripts/gm)
- Binaries in the config can be defined as URLs now.
- Add the option to set gm-lib path via the $GM_LIB environment variable ([#1365](https://github.com/informalsystems/ibc-rs/issues/1365))
16 changes: 8 additions & 8 deletions docs/architecture/adr-001-repo.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

This document provides a basic rundown of the structure of this repository, plus some plans for its evolution.

This repository comprises a Rust implementation of the [IBC](https://github.com/cosmos/ics) suite of protocols.
This repository comprises a Rust implementation of the [IBC](https://github.com/cosmos/ibc) suite of protocols.
To complement this implementation, this repository also comprises specifications, primarily written in TLA+, and
sometimes in English.

Expand Down Expand Up @@ -68,7 +68,7 @@ such as `SignedHeader`, `Validator`, or `ValidatorSet`.

#### Crate `relayer-modules`

The [canonical IBC specification](https://github.com/cosmos/ics/tree/master/spec/) is modular in the sense of grouping
The [canonical IBC specification](https://github.com/cosmos/ibc/tree/master/spec/) is modular in the sense of grouping
different components of the specification in modules; for instance, specification _ICS03_ pertains to the abstraction of
IBC connections and the IBC connection handshake protocol, while _ICS04_ pertains to IBC channels and packets.
We group the code in this crate to reflect the modular separation in the canonical IBC specification.
Expand Down Expand Up @@ -115,7 +115,7 @@ See the details for the crate `ibc-proto` [below](#crate-ibc-proto).
#### Crate `ibc_proto`

The `ibc-proto` library gives a developer access to the Cosmos SDK IBC proto-defined structs directly in Rust.
The canonical IBC structs reside presently in [cosmos-sdk](https://github.com/cosmos/cosmos-sdk/tree/master/proto/ibc),
The canonical IBC structs reside presently in [cosmos-sdk](https://github.com/cosmos/ibc-go/tree/main/proto/ibc),
defined in a proto3 syntax.
We compile these structs via prost directly to .rs files and import them into the other crates typically under the same
name prefixed with "Raw", for example:
Expand Down Expand Up @@ -158,18 +158,18 @@ For the IBC relayer:
- A first implementation of the IBC relayer in Golang is under active development at
[iqlusioninc/relayer](https://github.com/iqlusioninc/relayer).
- The English specification of the relayer algorithm is captured in the
[ICS018](https://github.com/cosmos/ics/tree/master/spec/ics-018-relayer-algorithms) spec.
[ICS018](https://github.com/cosmos/ibc/tree/master/spec/relayer/ics-018-relayer-algorithms) spec.

For IBC modules:

- A Golang implementation of IBC modules is under active development as part of the Cosmos SDK,
at [cosmos/cosmos-sdk/x/ibc](https://github.com/cosmos/cosmos-sdk/tree/master/x/ibc).
- The English specifications for IBC modules reside in [cosmos/ics](https://github.com/cosmos/ics/tree/master/spec).
- A Golang implementation of IBC modules is under active development
at [cosmos/ibc-go](https://github.com/cosmos/ibc-go/tree/main/modules).
- The English specifications for IBC modules reside in [cosmos/ibc](https://github.com/cosmos/ibc/tree/master/spec).

## Status

Proposed

## Consequences

Not applicable.
Not applicable.
8 changes: 3 additions & 5 deletions docs/architecture/adr-002-ibc-relayer.md
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,7 @@ This section covers assumptions and dependencies about the chains and their IBC
The relayer monitors the chain state to determine when packet forwarding is required. The relayer must be able to retrieve the data within some time bound. This is referred to as **data availability**.

#### Data Legibility
IBC protocol defines the minimal data set that must be made available to relayers for correct operation of the protocol. The relayer expects the data to be legible, i.e. **data should be serialized** according to the IBC specification format; this includes consensus state, client, connection, channel, and packet information, and any auxiliary state structure necessary to construct proofs of inclusion or exclusion of particular key/value pairs in state.
- [IBC Specification] some protobuf specifications can be found under individual ICS-es, for exmple [ICS-03 connection protobufs](https://github.com/cosmos/ics/blob/master/spec/ics-002-client-semantics/data-structures.proto)
Note: Some relayer development is blocked on SDK and Tendermint migration to protobuf encoding. Current work is done in [migration to protobuf](https://github.com/cosmos/cosmos-sdk/pull/6097)
IBC protocol defines the minimal data set that must be made available to relayers for correct operation of the protocol. The relayer expects the data to be legible, i.e. **data should be serialized** according to the IBC specification format; this includes consensus state, client, connection, channel, and packet information, and any auxiliary state structure necessary to construct proofs of inclusion or exclusion of particular key/value pairs in state.

#### Query Functionality
IBC host state machines MUST expose an interface for inspecting their state. For Cosmos/Tendermint chains this means:
Expand Down Expand Up @@ -74,7 +72,7 @@ The relay process must have access to its accounts with tokens on all destinatio

### Chain Transactions and Signing
The relayer must create chain specific signed transactions.
[Cosmos-Tx-Rust] For the first release Cosmos-SDK transaction signing is required. One possible implementation is [iqlusion's sdtx crate](https://github.com/iqlusioninc/crates/tree/develop/stdtx)
[Cosmos-Tx-Rust] For the first release Cosmos-SDK transaction signing is required. One possible implementation is [iqlusion's sdtx crate](https://github.com/iqlusioninc/crates/tree/main/stdtx)

#### Implementation of IBC "routing module"
The default IBC handler uses a receiver call pattern, where modules must individually call the IBC handler in order to bind to
Expand Down Expand Up @@ -297,7 +295,7 @@ Future versions may create multiple relay threads. One possibility is to create

### Relayer Algorithm

A relayer algorithm is described in [relayer algorithm described in IBC Specifigication](https://github.com/cosmos/ics/blame/master/spec/ics-018-relayer-algorithms/README.md#L47) and [Go relayer implementation ](https://github.com/cosmos/relayer/blob/f3a302df9e6e0c28883f5480199d3190821bcc06/relayer/strategies.go#L49.).
A relayer algorithm is described in [relayer algorithm described in IBC Specification](https://github.com/cosmos/ibc/blame/master/spec/relayer/ics-018-relayer-algorithms/README.md#L47) and [Go relayer implementation ](https://github.com/cosmos/relayer/blob/f3a302df9e6e0c28883f5480199d3190821bcc06/relayer/strategies.go#L49.).

This section describes some of the details of the realy thread algorithm in the Rust implementation. Inputs are the IBC Events and the events of interest are described in Appendix A.

Expand Down
4 changes: 2 additions & 2 deletions docs/architecture/adr-004-relayer-domain-decomposition.md
Original file line number Diff line number Diff line change
Expand Up @@ -299,5 +299,5 @@ fn main() -> Result<(), Box<dyn Error>> {

## References

[specs]: https://github.com/cosmos/ics/tree/master/spec
[#158]: https://github.com/informalsystems/ibc-rs/issues/158
[specs]: https://github.com/cosmos/ibc/tree/master/spec
[#158]: https://github.com/informalsystems/ibc-rs/issues/158
6 changes: 3 additions & 3 deletions docs/architecture/adr-005-relayer-v0-implementation.md
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@ Accepted
[ids]: https://github.com/cosmos/cosmos-sdk/pull/7993
[link]: https://github.com/informalsystems/ibc-rs/blob/master/docs/architecture/adr-004-relayer-domain-decomposition.md#link
[chain-req]: https://github.com/informalsystems/ibc-rs/blob/379dd9812f6e7a42b9428f64eb52fe292d417476/relayer/src/chain/handle.rs#L51
[ibc-relayer]: https://github.com/informalsystems/ibc-rs/relayer/
[ibc-relayer-cli]: https://github.com/informalsystems/ibc-rs/relayer-cli/
[ibc-relayer]: https://github.com/informalsystems/ibc-rs/tree/master/relayer/
[ibc-relayer-cli]: https://github.com/informalsystems/ibc-rs/tree/master/relayer-cli/
[hermes]: https://hermes.informal.systems
[features]: https://github.com/informalsystems/ibc-rs/blob/v0.1.0/guide/src/feature_matrix.md
[features]: https://github.com/informalsystems/ibc-rs/blob/v0.1.0/guide/src/feature_matrix.md
6 changes: 3 additions & 3 deletions docs/disclosure-log.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ This document is a record of all the bugs or issues we uncovered while specifyin
### 1. ICS3 liveness problem due to ICS018 relayer algorithm

The algorithm for relaying connection handshake datagrams of type `ConnOpenTry`does not handle the situation when both chains are in state `INIT`.
The current relayer algorithm in [ICS018](https://github.com/cosmos/ics/tree/master/spec/ics-018-relayer-algorithms) specifies that the `ConnOpenTry` datagram should be relayed only if one of the chains is in state `INIT` and the other chain is uninitialized (see the snippet below); this is not enough for guaranteeing liveness of the connection handshake protocol (ICS04).
The current relayer algorithm in [ICS018](https://github.com/cosmos/ibc/tree/master/spec/ics-018-relayer-algorithms) specifies that the `ConnOpenTry` datagram should be relayed only if one of the chains is in state `INIT` and the other chain is uninitialized (see the snippet below); this is not enough for guaranteeing liveness of the connection handshake protocol (ICS04).

```
if (localEnd.state === INIT && remoteEnd === null)
Expand Down Expand Up @@ -101,7 +101,7 @@ From this point on, the model stutters, i.e., is unable to progress further in t
### 3. ICS3 problems due to version negotiation

__Context__.
The original issue triggering this discussion is here: [cosmos/ics/#459](https://github.com/cosmos/ics/issues/459).
The original issue triggering this discussion is here: [cosmos/ics/#459](https://github.com/cosmos/ibc/issues/459).
Briefly, version negotiation in the ICS3 handshake can interfere in various ways, breaking either the safety or liveness of this protocol.
Several solution candidates exist, which we classify by their "mode", i.e., a strategy for picking the version at some point or another in the protocol.
For a full description of the modes, please consult [L2-tla/readme.md#version-negotiation-modes](spec/connection-handshake/L2-tla/README.md#version-negotiation-modes).
Expand All @@ -122,7 +122,7 @@ These are the main takeaways from this discussion:

1. The set of compatible versions that chains start off with (return values of `getCompatibleVersions()` in ICS3) have to intersect, otherwise a liveness issue occurs. This assumption is independent of the version negotiation mode. We report this in __case (a)__ below.
2. Modes "overwrite", "onTryNonDet", and "onAckNonDet" all result in breaking the handshake protocol. See __cases (b), (c), and (d)__ below for traces.
3. The deterministic modes "onTryDet" and "onAckDet" pass model checking, so a solution should be chosen among these two candidates (see the [original issue](https://github.com/cosmos/ics/issues/459) for follow-up on the solution).
3. The deterministic modes "onTryDet" and "onAckDet" pass model checking, so a solution should be chosen among these two candidates (see the [original issue](https://github.com/cosmos/ibc/issues/459) for follow-up on the solution).

##### Case (a). Empty version intersection causes liveness issue

Expand Down
9 changes: 4 additions & 5 deletions docs/spec/connection-handshake/L1_2.md
Original file line number Diff line number Diff line change
Expand Up @@ -617,13 +617,12 @@ The `clientConsensusState`, in particular, has an implicit requirement that it m

- How to capture aborts or incorrect termination? See [issue raised by Anca](https://github.com/informalsystems/ibc-rs/pull/42#discussion_r397077901). Is this necessary? To inform this discussion, more implementation details are needed.

- Verification of the unbonding period in `ConnTryHandler`. See [ICS/#403](https://github.com/cosmos/ics/issues/403).
- Verification of the unbonding period in `ConnTryHandler`. See [ICS/#403](https://github.com/cosmos/ibc/issues/403).

- Missing link to L3: what is the mechanism that implements the `pop` functionality at the implementation/L3 level (hint: it's in the SDK, the layer sitting between the consensus module and IBC Handler).

## References

- [ICS 003] Interchain Standards [ICS 003 Connection Semantics](https://github.com/cosmos/ics/tree/master/spec/ics-003-connection-semantics).
- [ICS 024] Interchain Standards [ICS 024 Host Requirements](https://github.com/cosmos/ics/tree/master/spec/ics-024-host-requirements).
- [ICS 018] Interchain Standards [ICS 024 Host Requirements](https://github.com/cosmos/ics/tree/master/spec/ics-018-relayer-algorithms).
- [IBC 1] Terminology. Interchain Standards [IBC 1 Terminology](https://github.com/cosmos/ics/blob/master/ibc/1_IBC_TERMINOLOGY.md#actor).
- [ICS 003] Interchain Standards [ICS 003 Connection Semantics](https://github.com/cosmos/ibc/tree/master/spec/core/ics-003-connection-semantics).
- [ICS 024] Interchain Standards [ICS 024 Host Requirements](https://github.com/cosmos/ibc/tree/master/spec/core/ics-024-host-requirements).
- [ICS 018] Interchain Standards [ICS 024 Host Requirements](https://github.com/cosmos/ibc/tree/master/spec/relayer/ics-018-relayer-algorithms).
4 changes: 2 additions & 2 deletions docs/spec/connection-handshake/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,10 @@

## Specification roadmap

In this folder you will find a collection of documents representing English & TLA+ specifications for the IBC connection handshake problem [[ICS-003](https://github.com/cosmos/ics/tree/master/spec/ics-003-connection-semantics)].
In this folder you will find a collection of documents representing English & TLA+ specifications for the IBC connection handshake problem [[ICS-003](https://github.com/cosmos/ibc/tree/master/spec/core/ics-003-connection-semantics)].

We currently cover two levels of abstraction of ICS2, in accordance with the [VDD workflow](https://github.com/informalsystems/VDD/blob/master/guide/guide.md): _level 1_ (abstract), _level 2_ (system model & distributed protocol).
Consequently, we break this work across the following documents:

- [L1_2.md](./L1_2.md) covers the highest level of abstraction (level 1) and also includes an English spec of the system model and protocol (level 2);
- [L2-tla](./L2-tla/) is a directory with the TLA+ spec for level 2.
- [L2-tla](./L2-tla/) is a directory with the TLA+ spec for level 2.
18 changes: 9 additions & 9 deletions docs/spec/tla/fungible-token-transfer/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

This document describes the TLA+ model of the core logic of the English
specification [ICS
20](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer). We
20](https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer). We
start by discussing [the model of the
protocol](#the-model-of-the-protocol).
Then this document provides links to our TLA+ formalization of [Properties and
Expand All @@ -24,16 +24,16 @@ modules](#helper-modules).
### Port and Channel Setup and Channel lifecycle management


In the model we assume that the [`setup()`](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#port--channel-setup) function has been called
In the model we assume that the [`setup()`](https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#port--channel-setup) function has been called
before. The [channel handshake
functions](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#channel-lifecycle-management)
functions](https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#channel-lifecycle-management)
are also considered being already executed. Our
model starts from a state where the channel handshake has completed
successfully.

### Packet Relay

The [core callback functions](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transferr#packet-relay)
The [core callback functions](https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#packet-relay)
`createOutgoingPacket()`, `onRecvPacket()`, `onRecvPacket()` and
`onTimeoutPacket()`, as well as the auxiliary function `refundTokens()`
are modeled in
Expand All @@ -53,7 +53,7 @@ discussed here. We will discuss it the last.

This module captures the functions
specifying packet flow and handling from [ICS
04](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics).
04](https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics).

#### [Bank.tla](Bank.tla)
The bank module encodes functions defined by the Cosmos bank
Expand Down Expand Up @@ -113,7 +113,7 @@ Next ==
### Properties and invariants

The English specification provides informal requirements as "[desired properties](
https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#desired-properties)".
https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#desired-properties)".

#### Preservation of fungibility

Expand All @@ -124,7 +124,7 @@ on chain B wants to return them, then the tokens can be returned.

For this we require the assumption (which is somewhat implicit it
its [correctness
argument](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#correctness)) that the source chain only performs valid transitions.
argument](https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#correctness)) that the source chain only performs valid transitions.

This is implemented in the property `ICS20Prop` in the file [IBCTokenTransfer.tla](IBCTokenTransfer.tla).

Expand Down Expand Up @@ -205,7 +205,7 @@ To import the specification in the TLA+ toolbox and run TLC:
We ran TLC using the constants defined in `IBCTokenTransfer.cfg` and verified the invariants `TypeOK` and `ICS20Inv` in 1min21s and the property `ICS20Prop` in 9min34s.
We note that the specification currently models two transfers: one from `ChainA` to `ChainB`, and vice versa, in their respective native denominations.
Both chains are correct, and there is no malicious relayer.
The relayer implements the logic from [ICS 18](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-018-relayer-algorithms), in particular, it does not
The relayer implements the logic from [ICS 18](https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-018-relayer-algorithms), in particular, it does not
relay timeouts.
However, the packet timeout handlers are specified in [`ICS04PacketHandlers.tla`](ICS04PacketHandlers.tla)
for future use.
Expand All @@ -215,4 +215,4 @@ for future use.
The specification contains type annotations for the
model checker [Apalache](https://github.com/informalsystems/apalache).
The specification passes the type check using the type checker [Snowcat](https://apalache.informal.systems/docs/apalache/typechecker-snowcat.html)
integrated in Apalache.
integrated in Apalache.
Loading

0 comments on commit 7b76a1f

Please sign in to comment.