Merge PR cosmos#222: Cleanup, clarification, formalization

ibc/2_IBC_DESIGN_PRINCIPLES.md

@@ -18,7 +18,7 @@ IBC is designed to be a *versatile* protocol. The protocol supports *heterogeneo
 
 ### Heterogeneity
 
-IBC can be implemented by any consensus algorithm and state machine with a basic set of requirements (fast finality & succinct state commitments). The protocol handles data authentication, transport, and ordering — common requirements of any multi-chain application — but is agnostic to the semantics of the application itself. Heterogeneous chains connected over IBC must understand a compatible application-layer "interface" (such as for transferring tokens), but once across the IBC interface handler, the state machines can support arbitrary bespoke functionality (such as shielded transactions).
+IBC can be implemented by any consensus algorithm and state machine with a basic set of requirements (fast finality, constant-size state commitments, and succinct commitment proofs). The protocol handles data authentication, transport, and ordering — common requirements of any multi-chain application — but is agnostic to the semantics of the application itself. Heterogeneous chains connected over IBC must understand a compatible application-layer "interface" (such as for transferring tokens), but once across the IBC interface handler, the state machines can support arbitrary bespoke functionality (such as shielded transactions).
 
 ### Composability
 
@@ -30,23 +30,23 @@ The "users", or "actors", in IBC — who initiate connections, create channels,
 
 ## Modularity
 
-IBC is designed to be a *modular* protocol. The protocol is constructed as a series of layered components with explicit security properties & requirements. Implementations of a component at a particular layer can vary (such as a different consensus algorithm or connection opening procedure) as long as they provide the requisite properties to the higher layers (such as finality, < 1/3 Byzantine safety, or embedded roots-of-trust on two chains). State machines need only understand compatible subsets of the IBC protocol (e.g. lite client verification algorithms for each other's consensus) in order to safely interact.
+IBC is designed to be a *modular* protocol. The protocol is constructed as a series of layered components with explicit security properties & requirements. Implementations of a component at a particular layer can vary (such as a different consensus algorithm or connection opening procedure) as long as they provide the requisite properties to the higher layers (such as finality, < 1/3 Byzantine safety, or embedded trusted states on two chains). State machines need only understand compatible subsets of the IBC protocol (e.g. lite client verification algorithms for each other's consensus) in order to safely interact.
 
 ## Locality
 
 IBC is designed to be a *local* protocol, meaning that only information about the two connected chains is necessary to reason about the security and correctness of a bidirectional IBC connection. Security requirements of the authentication primitives refer only to consensus algorithms and validator sets of the blockchains involved in the connection, and a blockchains maintaining a set of IBC connections need only understand the state of the chains to which it is connected (no matter which other chains those chains are connected to). 
 
 ### Locality of communication & information
 
-IBC makes no assumptions, and relies upon no characteristics, of the topological structure of the network of blockchains in which it is operating. No view of the global network-of-blockchains topology is required: security & correctness can be reasoned about at the level of a single connection between two chains, and by composition reasoned about for sub-graphs in the network topology. Users and chains can reason about their assumptions and risks given information about only part of the network graph of blockchains they know and trust (to variable degrees). There is no necessary "root chain" in IBC — some sub-graphs of the global network may evolve into a hub-spoke structure, others may remain tightly connected, others still may take on more exotic topologies.
+IBC makes no assumptions, and relies upon no characteristics, of the topological structure of the network of blockchains in which it is operating. No view of the global network-of-blockchains topology is required: security & correctness can be reasoned about at the level of a single connection between two chains, and by composition reasoned about for sub-graphs in the network topology. Users and chains can reason about their assumptions and risks given information about only part of the network graph of blockchains they know and assume to be correct (to variable degrees). There is no necessary "root chain" in IBC — some sub-graphs of the global network may evolve into a hub-spoke structure, others may remain tightly connected, others still may take on more exotic topologies.
 
-### Locality of trust & security
+### Locality of correctness assumptions & security
 
-Users of IBC — at the blockchain level and at the human or smart contract level — choose which consensus algorithms, state machines, and validator sets they "trust" (to behave in a particular way, e.g. < 1/3 Byzantine) and in which ways they trust them. Assuming the IBC protocol is implemented correctly, users are never exposed to risks of application-level invariant violations (such as asset inflation) due to Byzantine behaviour or faulty state machines transitions committed by validator sets or blockchains they did not explicitly decide to trust. This is particularly important in the expected large network topology of interconnected blockchains, where some number of blockchains and validator sets can be expected to be Byzantine occasionally — IBC, implemented conservatively, bounds the risk and limits the possible damage incurred.
+Users of IBC — at the blockchain level and at the human or smart contract level — choose which consensus algorithms, state machines, and validator sets they "assume to be correct" (to behave in a particular way, e.g. < 1/3 Byzantine) and in which ways they assume correctness. Assuming the IBC protocol is implemented correctly, users are never exposed to risks of application-level invariant violations (such as asset inflation) due to Byzantine behaviour or faulty state machines transitions committed by validator sets or blockchains they did not explicitly decide to assume to be correct. This is particularly important in the expected large network topology of interconnected blockchains, where some number of blockchains and validator sets can be expected to be Byzantine occasionally — IBC, implemented conservatively, bounds the risk and limits the possible damage incurred.
 
 ### Locality of permissioning
 
-Actions in IBC — such as opening a connection, creating a channel, or sending a packet — are permissioned locally by the state machines and actors involved in a particular connection between two chains. Individual chains could choose to require approval from a permissioning mechanism (such as governance) for specific application-layer actions (such as delegated-security slashing), but for the base protocol, actions are permissionless (modulo gas & storage costs) — by default, connections can be opened, channels created, and packets sent without any approval process. Of course, users themselves must inspect the state & consensus of each IBC connection and decide whether it is safe to used (based e.g. on the roots-of-trust stored).
+Actions in IBC — such as opening a connection, creating a channel, or sending a packet — are permissioned locally by the state machines and actors involved in a particular connection between two chains. Individual chains could choose to require approval from a permissioning mechanism (such as governance) for specific application-layer actions (such as delegated-security slashing), but for the base protocol, actions are permissionless (modulo gas & storage costs) — by default, connections can be opened, channels created, and packets sent without any approval process. Of course, users themselves must inspect the state & consensus of each IBC connection and decide whether it is safe to used (based e.g. on the trusted states stored).
 
 ## Efficiency
 

ibc/3_IBC_TERMINOLOGY.md

@@ -12,15 +12,15 @@
 
 This document provides definitions in plain English of key terms used throughout the IBC specification set.
 
-## Definitions
+## Abstraction definitions
 
 ### Actor
 
 An *actor*, or a *user* (used interchangeably), is an entity interacting with the IBC protocol. An actor can be a human end-user, a module or smart contract running on a blockchain, or an off-chain relayer process capable of signing transactions.
 
-### Chain / Ledger
+### Machine / Chain / Ledger
 
-A *chain*, *blockchain*, or *ledger* (used interchangeably), is a distributed ledger (or "blockchain", although a strict chain of blocks may not be required) implementing part or all of the IBC specification as a component or module within its state machine.
+A *machine*, *chain*, *blockchain*, or *ledger* (used interchangeably), is a state machine (which may be a distributed ledger, or "blockchain", although a strict chain of blocks may not be required) implementing part or all of the IBC specification.
 
 ### State Machine
 
@@ -32,27 +32,35 @@ A *consensus* algorithm is the protocol used by the set of processes operating a
 
 ### Consensus State
 
-The *consensus state*, or the *root-of-trust*, is the set of information about the state of a consensus algorithm required to verify proofs about the output of that consensus algorithm (e.g. commitment roots in signed headers).
+The *consensus state* is the set of information about the state of a consensus algorithm required to verify proofs about the output of that consensus algorithm (e.g. commitment roots in signed headers).
+
+### Trusted State
+
+A *trusted state* is a particular state which a machine has decided to assume to be correct, either a priori or having verified a progression from a preceding trusted state.
 
 ### Header
 
 A *header* is an update to the consensus state of a particular blockchain that can be verified in a well-defined fashion by a "light client" algorithm defined for that particular consensus algorithm.
 
-### Finality
+### Commitment 
 
-*Finality* is the guarantee provided by a consensus algorithm that a particular block will not be reverted, subject to certain assumptions about the behaviour of the validator set. The IBC protocol requires finality.
+A cryptographic *commitment* is a way to cheaply verify membership of a key => value pair in a mapping, where the mapping can be committed to with a short witness string.
 
-### Commitment 
+### CommitmentProof
 
-A cryptographic *commitment* is a way to cheaply verify membership of a key => value pair in a mapping, where the mapping can be committed to with a short witness string. An *vector commitment proof* refers to the proof structure which proves whether a particular key maps to a particular value in a committed-to set or not.
+A *commitment proof* refers to the proof structure which proves whether a particular key maps to a particular value in a committed-to set or not.
 
-### Handler
+### Handler Module
 
-An IBC *handler* is the module or sub-component within the state machine of a ledger responsible for implementing the IBC specification by "handling" datagrams, performing the appropriate checks, proof verifications, and/or storage alterations, and routing valid packets to other parts of the state machine, as defined by the application-layer semantics.
+The IBC *handler module* is the module within the state machine which implements [ICS 25](../spec/ics-025-handler-module), managing clients, connections, & channels, verifying proofs, and storing appropriate commitments for packets.
+
+### Relayer Module
+
+The IBC *relayer module* is the module within the state machine which implements [ICS 26](../spec/ics-026-relayer-module), routing packets between the handler module and other modules on the host state machine which utilise the relayer module's external interface.
 
 ### Datagram
 
-A *datagram* is an opaque bytestring transmitted over some physical network, and handled by the top-level IBC handler implemented in the ledger's state machine. In some implementations, the datagram may be a field in a ledger-specific transaction or message data structure which also contains other information (e.g. a fee for spam prevention, nonce for replay prevention, type identifier to route to the IBC handler, etc.). All IBC sub-protocols (such as opening a connection, creating a channel, sending a packet) are defined in terms of sets of datagrams and protocols for handling them.
+A *datagram* is an opaque bytestring transmitted over some physical network, and handled by the IBC relayer module implemented in the ledger's state machine. In some implementations, the datagram may be a field in a ledger-specific transaction or message data structure which also contains other information (e.g. a fee for spam prevention, nonce for replay prevention, type identifier to route to the IBC handler, etc.). All IBC sub-protocols (such as opening a connection, creating a channel, sending a packet) are defined in terms of sets of datagrams and protocols for handling them through the relayer module.
 
 ### Connection
 
@@ -70,28 +78,76 @@ A *packet* is a particular data structure with sequence-related metadata (define
 
 A *module* is a sub-component of the state machine of a particular blockchain which may interact with the IBC handler and alter state according to the *data* field of particular IBC packets sent or received (minting or burning tokens, for example).
 
-## Auxiliary Terms
-
 ### Handshake
 
-A *handshake* is a particular class of sub-protocol involving multiple datagrams, generally used to initialise some common state on the two involved chains such as roots-of-trust for each others' consensus algorithms.
+A *handshake* is a particular class of sub-protocol involving multiple datagrams, generally used to initialise some common state on the two involved chains such as trusted states for each others' consensus algorithms.
+
+### Sub-protocol
+
+Sub-protocols are defined as a set of datagram kinds and functions which must be implemented by the IBC handler module of the implementing blockchain.
 
-### Trust
+Datagrams must be relayed between chains by an external process. This process is assumed to behave in an arbitrary manner — no safety properties are dependent on its behaviour, although progress is generally dependent on the existence of at least one correct relayer process.
 
-To *trust* a blockchain or validator set means to expect that the validator set will behave in a particular way (such as < 1/3 Byzantine) relative to a well-defined consensus & state machine protocol.
+IBC sub-protocols are reasoned about as interactions between two chains `A` and `B` — there is no prior distinction between these two chains and they are assumed to be executing the same, correct IBC protocol. `A` is simply by convention the chain which goes first in the sub-protocol and `B` the chain which goes second. Protocol definitions should generally avoid including `A` and `B` in variable names to avoid confusion (as the chains themselves do not know whether they are `A` or `B` in the protocol).
 
 ### Authentication
 
 *Authentication* refers to the protocols used to ensure that datagrams were in fact sent by a particular chain and associated state alterations committed by it.
 
+## Property definitions
+
+### Finality
+
+*Finality* is the quantifiable assurance provided by a consensus algorithm that a particular block will not be reverted, subject to certain assumptions about the behaviour of the validator set. The IBC protocol requires finality, although it need not be absolute (for example, a threshold finality gadget for a Nakamoto consensus algorithm will provide finality subject to economic assumptions about how miners behave).
+
+### Misbehaviour
+
+*Misbehaviour* refers to a class of consensus fault defined by a consensus algorithm & detectable (possibly also attributable) by the light client of that consensus algorithm.
+
 ### Equivocation
 
-*Equivocation* refers to a particular class of consensus fault committed by a validator or validators which sign votes on multiple different successors to a single block.
+*Equivocation* refers to a particular class of consensus fault committed by a validator or validators which sign votes on multiple different successors to a single block. All equivocations are misbehaviours.
 
-### Sub-protocol
+### Data availability
 
-Sub-protocols are defined as a set of datagram types and functions which must be implemented by the IBC handler module of the implementing blockchain.
+*Data availability* refers to the ability of off-chain relayer processes to retrieve data in the state of a machine within some time bound.
 
-Datagrams must be relayed between chains by an external process. This process is assumed to behave in an arbitrary manner — no safety properties are dependent on its behaviour, although progress is generally dependent on the existence of at least one correct relayer process.
+### Data confidentiality
 
-IBC sub-protocols are reasoned about as interactions between two chains `A` and `B` — there is no prior distinction between these two chains and they are assumed to be executing the same, correct IBC protocol. `A` is simply by convention the chain which goes first in the sub-protocol and `B` the chain which goes second. Protocol definitions should generally avoid including `A` and `B` in variable names to avoid confusion (as the chains themselves do not know whether they are `A` or `B` in the protocol).
+*Data confidentiality* refers to the ability of the host state machine to refuse to make particular data available to particular parties without impairing the functionality of the IBC protocol.
+
+### Non-repudiability
+
+*Non-repudiability* refers to the inability of a machine to deny having sent a particular packet or committed a particular state. IBC is a non-repudiable protocol, modulo data availability choices made by state machines.
+
+### Consensus liveness
+
+*Consensus liveness* refers to the continuance of block production by the consensus algorithm of a particular machine.
+
+### Transactional liveness
+
+*Transactional liveness* refers to the confirmation of incoming transactions (which transactions should be clear by context) by the consensus algorithm of a particular machine. Transactional liveness requires consensus liveness, but consensus liveness does not necessarily provide transactional liveness.
+
+### Consensus synchrony
+
+*Consensus synchrony* refers to consensus liveness within a particular bound.
+
+### Transactional synchrony
+
+*Transactional synchrony* refers to transactional liveness within a particular bound.
+
+### Exactly-once safety
+
+*Exactly-once safety* refers to the property that a packet is confirmed no more than once (and generally exactly-once assuming eventual transactional liveness).
+
+### Deliver-or-timeout safety
+
+*Deliver-or-timeout safety* refers to the property that a packet will either be delivered & executed or will timeout in a way that can be proved back to the sender.
+
+### Constant (w.r.t. complexity)
+
+*Constant*, when referring to space or time complexity, means `O(1)`.
+
+### Succinct
+
+*Succinct*, when referring to space or time complexity, means `O(log n)` or better.

ibc/4_IBC_USECASES.md

@@ -34,7 +34,7 @@ There may be a starting "source zone", which starts with the entire token balanc
 
 #### Invariants
 
-Fungibility of any amount across all pegged representations, constant (or formulaic, in the case of a inflationary asset) total supply cumulative across chains.
+Fungibility of any amount across all pegged representations, constant (or formulaic, in the case of a inflationary asset) total supply cumulative across chains, and tokens only exist in a spendable form on one chain at once.
 
 ### Non-fungible tokens