Clarify connections intro, Byzantine recovery strategies

docs/spec/ibc/README.md

@@ -6,9 +6,9 @@ This paper specifies the Cosmos Inter-Blockchain Communication (IBC) protocol. T
 
 The core IBC protocol is payload-agnostic. On top of IBC, developers can implement the semantics of a particular application, enabling users to transfer valuable assets between different blockchains while preserving, under particular security assumptions of the underlying blockchains, the contractual guarantees of the asset in question - such as scarcity and fungibility for a currency or global uniqueness for a digital kitty-cat. 
 
-IBC requires two blockchains with cheaply verifiable rapid finality and Merkle tree substate proofs. The protocol makes no assumptions of block confirmation times or maximum network latency of packet transmissions, and the two consensus algorithms remain completely independent. Each chain maintains a local partial order and inter-chain message sequencing ensures cross-chain linearity. Once the two chains have registered a trust relationship, cryptographically verifiable packets can be sent between the chains.
+IBC requires two blockchains with cheaply verifiable rapid finality and Merkle tree substate proofs. The protocol makes no assumptions of block confirmation times or maximum network latency of packet transmissions, and the two consensus algorithms remain completely independent. Each chain maintains a local partial order and inter-chain message sequencing ensures cross-chain linearity. Once the two chains have registered a trust relationship, cryptographically verifiable packets can be sent between them.
 
-IBC was first outlined in the [Cosmos Whitepaper](https://github.com/cosmos/cosmos/blob/master/WHITEPAPER.md#inter-blockchain-communication-ibc), and later described in more detail by the [IBC specification paper](https://github.com/cosmos/ibc/raw/master/CosmosIBCSpecification.pdf). This document replaces and supersedes both. It explains the requirements and structure of the protocol and provides sufficient detail for both analysis and implementation, including example pseudocode.
+IBC was first outlined in the [Cosmos Whitepaper](https://github.com/cosmos/cosmos/blob/master/WHITEPAPER.md#inter-blockchain-communication-ibc), and later described in more detail by the [IBC specification paper](https://github.com/cosmos/ibc/raw/master/CosmosIBCSpecification.pdf). This document supersedes both. It explains the requirements and structure of the protocol and provides sufficient detail for both analysis and implementation.
 
 ## Contents
 
@@ -44,5 +44,6 @@ IBC was first outlined in the [Cosmos Whitepaper](https://github.com/cosmos/cosm
     1. [Appendix A: Encoding Libraries](appendices.md#appendix-a-encoding-libraries)
     1. [Appendix B: IBC Queue Format](appendices.md#appendix-b-ibc-queue-format)
     1. [Appendix C: Merkle Proof Format](appendices.md#appendix-c-merkle-proof-formats)
-    1. [Appendix D: Universal IBC Packets](appendices.md#appendix-d-universal-ibc-packets)
-    1. [Appendix E: Tendermint Header Proofs](appendices.md#appendix-e-tendermint-header-proofs)
+    1. [Appendix D: Byzantine Recovery Strategies](appendices.md#appendix-d-byzantine-recovery-strategies)
+    1. [Appendix E: Universal IBC Packets](appendices.md#appendix-e-universal-ibc-packets)
+    1. [Appendix F: Tendermint Header Proofs](appendices.md#appendix-f-tendermint-header-proofs)

docs/spec/ibc/appendices.md

@@ -48,7 +48,13 @@ For those who wish to minimize the size of their merkle proofs, we recommend usi
 
 See [binary format as protobuf specification](./protobuf/merkle.proto)
 
-## Appendix D: Universal IBC Packets
+## Appendix D: Byzantine Recovery Strategies
+
+- Goal: keep application invariants
+- Plasma-like fraud proofs
+- Trusted entity - governance
+
+## Appendix E: Universal IBC Packets
 
 { what is this }
 
@@ -56,7 +62,7 @@ The structures above can be used to define standard encodings for the basic IBC
 
 See [binary format as protobuf specification](./protobuf/messages.proto)
 
-## Appendix E: Tendermint Header Proofs
+## Appendix F: Tendermint Header Proofs
 
 { is this finalized? }
 

docs/spec/ibc/channels-and-packets.md

@@ -10,7 +10,7 @@ The IBC protocol as defined here is payload-agnostic. The packet receiver on cha
 
 To facilitate useful application logic, we introduce an IBC *channel*: a set of reliable messaging queues that allows us to guarantee a cross-chain causal ordering[[5](./references.md#5)] of IBC packets. Causal ordering means that if packet _x_ is processed before packet _y_ on chain _A_, packet _x_ must also be processed before packet _y_ on chain _B_.
 
-IBC channels implement a [vector clock](https://en.wikipedia.org/wiki/Vector_clock) for the restricted case of two processes (in our case, blockchains). Given _x_ → _y_ means _x_ is causally before _y_, and chains A and B, and _a_ ⇒ _b_ means _a_ implies _b_:
+IBC channels implement a vector clock [2](references.md#2) for the restricted case of two processes (in our case, blockchains). Given _x_ → _y_ means _x_ is causally before _y_, and chains A and B, and _a_ ⇒ _b_ means _a_ implies _b_:
 
 _A:send(msg<sub>i </sub>)_ &#8594; _B:receive(msg<sub>i </sub>)_
 
@@ -125,6 +125,8 @@ Each incoming & outgoing queue for each connection must be provably associated w
 
 ### 3.4 Sending a packet
 
+{ todo: unify terms, clarify }
+
 To send an IBC packet, an application module on the source chain must call the send method of the IBC module, providing a packet as defined above. The IBC module must ensure that the destination chain was already properly registered and that the calling module has permission to write this packet. If all is in order, the IBC module simply pushes the packet to the tail of _Outgoing<sub>A</sub>_, which enables all the proofs described above.
 
 If desired, the packet payload can contain additional module routing information in the form of a _kind_, so that different modules can write different kinds of packets and maintain any application-level invariants related to this area. For example, a "coin" module can ensure a fixed supply, or a "NFT" module can ensure token uniqueness. The IBC module must associate every supported message with a particular handler (_f<sub>kind</sub>_) and return an error for unsupported types.
@@ -134,6 +136,8 @@ _(IBCsend(D, type, data)_ &#8658; _Success)_
 
 ### 3.5 Receiving a packet
 
+{ todo: unify terms }
+
 We also consider how a given blockchain _A_ is expected to receive the packet from a source chain _S_ with a merkle proof, given the current set of trusted headers for that chain, _T<sub>S</sub>_:
 
 _A:IBCreceive(S, M<sub>k,v,h</sub>)_ &#8658; _match_
@@ -174,7 +178,7 @@ This enforces that the receipts are processed in order, to allow some the applic
 
 ### 3.7 Packet relayer
 
-{ todo: cleanup wording }
+{ todo: cleanup wording & terms }
 
 The blockchain itself only records the _intention_ to send the given message to the recipient chain, it doesn't make any network connections as that would add unbounded delays and non-determinism into the state machine. We define the concept of a _relay_ process that connects two chain by querying one for all proofs needed to prove outgoing messages and submit these proofs to the recipient chain.
 

docs/spec/ibc/connections.md

@@ -2,7 +2,9 @@
 
 ([Back to table of contents](README.md#contents))
 
-The basis of IBC is the ability to verify in the on-chain consensus ruleset of chain _B_ that a message packet received on chain _B_ was correctly generated on chain _A_. This establishes a cross-chain linearity guarantee: upon validation of that packet on chain _B_ we know that the packet has been executed on chain _A_ and any associated logic resolved (such as assets being escrowed), and we can safely perform application logic on chain _B_ (such as generating vouchers on chain _B_ for the chain _A_ assets which can later be redeemed with a packet in the opposite direction).
+The basis of IBC is the ability to verify in the on-chain consensus ruleset of chain _B_ that a data packet received on chain _B_ was correctly generated on chain _A_. This establishes a cross-chain linearity guarantee: upon validation of that packet on chain _B_ we know that the packet has been executed on chain _A_ and any associated logic resolved (such as assets being escrowed), and we can safely perform application logic on chain _B_ (such as generating vouchers on chain _B_ for the chain _A_ assets which can later be redeemed with a packet in the opposite direction).
+
+This section outlines the abstraction of an IBC _connection_: the state and consensus ruleset necessary to perform IBC packet verification. 
 
 ### 2.1 Definitions
 
@@ -38,9 +40,9 @@ _valid(H<sub>h </sub>,M<sub>k,v,h </sub>)_ &#8658; _[true | false]_
 
 All proofs require an initial _H<sub>h</sub>_ and _C<sub>h</sub>_ for some _h_, where &#916;_(now, H<sub>h</sub>) < P_.
 
-Establishing a bidirectional initial root-of-trust between the two blockchains (_A_ to _B_ and _B_ to _A_) — _HA<sub>h</sub>_ and _CA<sub>h</sub>_ stored on chain _B_, and _HB<sub>h</sub>_ and _CB<sub>h</sub_ stored on chain _A_ — is necessary before any IBC packets can be sent. 
+Establishing a bidirectional initial root-of-trust between the two blockchains (_A_ to _B_ and _B_ to _A_) — _HA<sub>h</sub>_ and _CA<sub>h</sub>_ stored on chain _B_, and _HB<sub>h</sub>_ and _CB<sub>h</sub>_ stored on chain _A_ — is necessary before any IBC packets can be sent. 
 
-Any header may be from a malicious chain (e.g. shadowing a real chain state with a fake validator set), so a subjective decision is required before establishing a connection. This can be performed permissionlessly, in which case users later utilizing the IBC channel must check the root-of-trust themselves, or authorized by on-chain governance.
+Any header may be from a malicious chain (e.g. shadowing a real chain state with a fake validator set), so a subjective decision is required before establishing a connection. This can be performed permissionlessly, in which case users later utilizing the IBC channel must check the root-of-trust themselves, or authorized by on-chain governance for additional assurance.
 
 #### 2.3.2 Following Block Headers
 
@@ -79,4 +81,4 @@ IBC implementations may optionally include the ability to close an IBC connectio
 
 Closing a connection may break application invariants (such as fungiblity - token vouchers on chain _B_ will no longer be redeemable for tokens on chain _A_) and should only be undertaken in extreme circumstances such as Byzantine behavior of the connected chain.
 
-Closure may be permissioned to an on-chain governance system, an identifiable party on the other chain (such as a signer quorum, although this will not work in some Byzantine cases), or any user who submits a connection-specific fraud proof of Byzantine behavior. When a connection is closed, application-specific measures may be undertaken to recover assets held on a Byzantine chain. We defer further discussion to { an appendix }.
+Closure may be permissioned to an on-chain governance system, an identifiable party on the other chain (such as a signer quorum, although this will not work in some Byzantine cases), or any user who submits an application-specific fraud proof. When a connection is closed, application-specific measures may be undertaken to recover assets held on a Byzantine chain. We defer further discussion to [Appendix D](appendices.md#appendix-d-byzantine-recovery-strategies).