Merge PR cosmos#233: 1.0.0-rc2 feedback (1/x)

ibc/1_IBC_ARCHITECTURE.md

@@ -102,11 +102,11 @@ The network layer and relayer processes may behave in arbitrary ways, dropping,
 
 ### Flow control
 
-IBC does not require specific provision for computation-level flow control since the underlying machines will have throughput limitations and flow control mechanisms of their own (such as "gas" markets). Application-level flow control — limiting the rate of particular packets according to their content — may be useful to ensure security properties (limiting the value on a single machine) and contain damage from Byzantine faults (allowing a challenge period to prove an equivocation, then closing a connection). IBC provides facilities for modules to reject packets and leaves particulars up to the higher-level application protocols.
+IBC does not provide specific provisions for compute-level or economic-level flow control. The underlying machines will have compute throughput limitations and flow control mechanisms of their own (such as "gas" markets). Application-level economic flow control — limiting the rate of particular packets according to their content — may be useful to ensure security properties (limiting the value on a single machine) and contain damage from Byzantine faults (allowing a challenge period to prove an equivocation, then closing a connection). For example, an application transferring value over an IBC channel might want to limit the rate of value transfer per block to limit damage from potential Byzantine behaviour. IBC provides facilities for modules to reject packets and leaves particulars up to the higher-level application protocols.
 
 ### Authentication
 
-All datagrams in IBC are authenticated: a block finalised by the consensus algorithm of the sending machine must commit to the outgoing packet via a cryptographic commitment, and the receiving chain's IBC handler must verify both the consensus transcript and the cryptographic commitment proof that the datagram was sent (and associated actions executed) before acting upon it.
+All datagrams in IBC are authenticated: a block finalised by the consensus algorithm of the sending machine must commit to the outgoing packet via a cryptographic commitment, and the receiving chain's IBC handler must verify both the consensus transcript and the cryptographic commitment proof that the datagram was sent before acting upon it.
 
 ### Statefulness
 

ibc/2_IBC_DESIGN_PRINCIPLES.md

@@ -38,7 +38,11 @@ IBC is designed to be a *local* protocol, meaning that only information about th
 
 ### 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 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.
+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. Channels are end-to-end; in the first version IBC will only support one-hop paths, but multi-hop paths will be supported in the future (though automatic routing is not necessarily likely or safe due to the consensus algorithm correctness assumptions involved).
+
+Application data, however, may have salient non-local properties which users of the protocol will need to pay attention to, such as the original source zone of a token which might have been sent on a complex multi-hop path, the original stake & identity of a validator offering their services through cross-chain validation, or the original smart contract with which a particular object-capability key managing a non-fungible token is associated. These non-local properties do not need to be understood by the IBC protocol itself, but they will need to be reasoned about by users and higher-level applications.
 
 ### Locality of correctness assumptions & security
 

ibc/3_IBC_TERMINOLOGY.md

@@ -48,7 +48,7 @@ A cryptographic *commitment* is a way to cheaply verify membership of a key => v
 
 ### CommitmentProof
 
-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.
+A *commitment proof* is the proof structure which proves whether a particular key maps to a particular value in a committed-to set or not.
 
 ### Handler Module
 
@@ -92,7 +92,7 @@ IBC sub-protocols are reasoned about as interactions between two chains `A` and
 
 ### 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.
+*Authentication* is the property of ensuring that datagrams were in fact sent by a particular chain in the manner defined by the IBC handler.
 
 ## Property definitions
 
@@ -102,47 +102,47 @@ IBC sub-protocols are reasoned about as interactions between two chains `A` and
 
 ### 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.
+*Misbehaviour* is 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. All equivocations are misbehaviours.
+*Equivocation* is 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.
 
 ### Data availability
 
-*Data availability* refers to the ability of off-chain relayer processes to retrieve data in the state of a machine within some time bound.
+*Data availability* is the ability of off-chain relayer processes to retrieve data in the state of a machine within some time bound.
 
 ### Data confidentiality
 
-*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.
+*Data confidentiality* is 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.
+*Non-repudiability* is the inability of a machine to successfully dispute having sent a particular packet or committed a particular state. IBC is a non-repudiable protocol, modulo data confidentiality choices made by state machines.
 
 ### Consensus liveness
 
-*Consensus liveness* refers to the continuance of block production by the consensus algorithm of a particular machine.
+*Consensus liveness* is 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.
+*Transactional liveness* is the continued 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
+### Bounded consensus liveness
 
-*Consensus synchrony* refers to consensus liveness within a particular bound.
+*Bounded consensus liveness* is consensus liveness within a particular bound.
 
-### Transactional synchrony
+### Bounded transactional liveness
 
-*Transactional synchrony* refers to transactional liveness within a particular bound.
+*Bounded transactional liveness* is 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).
+*Exactly-once safety* is 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.
+*Deliver-or-timeout safety* is 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)
 

scripts/make_pdf.sh

@@ -16,7 +16,7 @@ find $DIR2 -type f -name "*.md.xfm" -exec awk -i inplace '/^##/{p=1}p' {} \;
 
 # pdf generation
 
-pandoc --pdf-engine=xelatex --template eisvogel --filter pandoc-include --mathjax --toc --number-sections -t latex -o spec.pdf spec.pdc
+pandoc --pdf-engine=xelatex --template eisvogel --filter pandoc-include --mathjax --toc --number-sections --listings -t latex -o spec.pdf spec.pdc
 
 # cleanup
 

spec.pdc

@@ -17,8 +17,32 @@ header-includes:
     - \usepackage{hyperref}
     - \usepackage[left]{lineno}
     - \linenumbers
+    - \usepackage{listings}
 ---
 
+\lstdefinelanguage{Typescript}{
+  morekeywords=[1]{break, continue, delete, else, for, function, if, in,
+    new, return, this, typeof, var, void, while, with},
+  % Literals, primitive types, and reference types.
+  morekeywords=[2]{false, null, true, boolean, number, undefined,
+    Array, Boolean, Date, Math, Number, String, Object},
+  % Built-ins.
+  morekeywords=[3]{eval, parseInt, parseFloat, escape, unescape},
+  sensitive,
+  morecomment=[s]{/*}{*/},
+  morecomment=[l]//,
+  morecomment=[s]{/**}{*/}, % JavaDoc style comments
+  morestring=[b]',
+  morestring=[b]"
+}[keywords, comments, strings]
+
+\lstset {
+  numbers = left,
+  stepnumber = 1,
+  numberstyle=\tiny\color{gray},
+  language = Typescript
+}
+
 \pagebreak
 
 # Architectural Overview
@@ -29,10 +53,6 @@ header-includes:
 
 !include ibc/3_IBC_TERMINOLOGY.md.xfm
 
-!include ibc/4_IBC_USECASES.md.xfm
-
-!include ibc/5_IBC_DESIGN_PATTERNS.md.xfm
-
 # ICS 001 - ICS Standard
 
 !include spec/ics-001-ics-standard/README.md.xfm
@@ -76,3 +96,11 @@ header-includes:
 # ICS 020 - Fungible Token Transfer
 
 !include spec/ics-020-fungible-token-transfer/README.md.xfm
+
+# Appendix A: Use-case Descriptions
+
+!include ibc/4_IBC_USECASES.md.xfm
+
+# Appendix B: Design Patterns
+
+!include ibc/5_IBC_DESIGN_PATTERNS.md.xfm

spec/ics-023-vector-commitments/README.md

@@ -151,7 +151,7 @@ The `batchVerifyNonMembership` function verifies a proof that many paths have no
 type batchVerifyNonMembership = (root: CommitmentRoot, proof: CommitmentProof, paths: Set<Path>) => boolean
 ```
 
-If defined, these functions MUST be computationally equivalent to the conjunctive union of `verifyMembership` and `verifyNonMembership` respectively (`proof` may vary):
+If defined, these functions MUST produce the same result as the conjunctive union of `verifyMembership` and `verifyNonMembership` respectively (efficiency may vary):
 
 ```typescript
 batchVerifyMembership(root, proof, items) ===
@@ -226,7 +226,7 @@ proof = createMembershipProof(acc, path, value)
 Probability(verifyMembership(root, proof, path, value) === false) negligible in k
 ```
 
-For all other values `otherValue` where `value /= otherValue`, for all values of `proof`,
+For all other values `otherValue` where `value !== otherValue`, for all values of `proof`,
 
 ```
 Probability(verifyMembership(root, proof, path, otherValue) === true) negligible in k

spec/ics-024-host-requirements/README.md

@@ -33,27 +33,21 @@ The IBC/TAO specifications define the implementations of two modules: the core "
 
 ### Paths, identifiers, separators
 
-A `Path` is a bytestring used as the key for an object stored in state. Paths MUST contain only alphanumeric characters and the separator `/`.
-
 An `Identifier` is a bytestring used as a key for an object stored in state, such as a connection, channel, or light client. Identifiers MUST consist of alphanumeric characters only. Identifiers MUST be non-empty (of positive integer length).
 
-Identifiers are not intended to be valuable resources — to prevent name squatting, minimum length requirements or pseudorandom generation MAY be implemented.
+A `Path` is a bytestring used as the key for an object stored in state. Paths MUST contain only identifiers, constant alphanumeric strings, and the separator `"/"`. 
+
+Identifiers are not intended to be valuable resources — to prevent name squatting, minimum length requirements or pseudorandom generation MAY be implemented, but particular restrictions are not imposed by this specification.
 
-The separator `/` is used to separate and concatenate two identifiers or an identifier and a constant bytestring. Identifiers MUST NOT contain the `/` character, which prevents ambiguity.
+The separator `"/"` is used to separate and concatenate two identifiers or an identifier and a constant bytestring. Identifiers MUST NOT contain the `"/"` character, which prevents ambiguity.
 
-Variable interpolation, denoted by curly braces, MAY be used as shorthand to define path formats, e.g. `client/{clientIdentifier}/consensusState`.
+Variable interpolation, denoted by curly braces, is used throughout this specification as shorthand to define path formats, e.g. `client/{clientIdentifier}/consensusState`.
 
 ### Key/value Store
 
 The host state machine MUST provide a key-value store interface 
 with three functions that behave in the standard way:
 
-```typescript
-type Path = string
-
-type Value = string
-```
-
 ```typescript
 type get = (path: Path) => Value | void
 ```
@@ -68,11 +62,12 @@ type delete = (path: Path) => void
 
 `Path` is as defined above. `Value` is an arbitrary bytestring encoding of a particular data structure. Encoding details are left to separate ICSs.
 
-These functions MUST be permissioned to the IBC handler module (the implementation of which is described in separate standards) only, so only the IBC handler module can `set` or `delete` the paths which can be read by `get`. This can possibly be implemented as a sub-store (prefixed key-space) of a larger key-value store used by the entire state machine.
+These functions MUST be permissioned to the IBC handler module (the implementation of which is described in separate standards) only, so only the IBC handler module can `set` or `delete` the paths that can be read by `get`. This can possibly be implemented as a sub-store (prefixed key-space) of a larger key-value store used by the entire state machine.
 
-Host state machines must provide two instances of this interface - 
+Host state machines MUST provide two instances of this interface -
 a `provableStore` for storage read by (i.e. proven to) other chains,
-and a `privateStore` for storage local to the host.
+and a `privateStore` for storage local to the host, upon which `get`
+, `set`, and `delete` can be called, e.g. `provableStore.set('some/path', 'value')`.
 
 The `provableStore`: