Merge PR cosmos#106: ICS 2 updates

spec/ics-2-consensus-verification/VERIFIER.md → spec/ics-2-consensus-verification/CONSENSUS.md

@@ -1,12 +1,14 @@
 ## Synopsis
 
-Full nodes are procedures which process a list of messages, `[Message]`, according to the
-`Consensus` algorithm. The lightclient `Verifier` does not process all messages, but
-it uses artifacts produced by execution of the `Consensus` algorithm, along with well-forumated security assumptions, to verify parts of a consensus execution transcript
-process. The `Verifier` MUST work identically to a full node, given that the
-security assumptions of `Consensus` are preserved. This means that if and only
+Full nodes are procedures which process a list of messages, `[Message]`, according to a
+defined algorithm `Consensus`. The light client `Verifier` does not process all messages, but
+it uses artifacts produced by execution of the `Consensus` algorithm,
+along with well-formulated security assumptions, to verify parts of a consensus execution transcript.
+The `Verifier` MUST work identically to a full node, given that the
+stated security assumptions of `Consensus` are preserved. This means that if and only
 if a full node accepts the new `Header` given a `ConsensusState` and
-`[Message]`, will the `Verifier` then also accept it.
+`[Message]`, will the `Verifier` then also accept it given the same
+`ConsensusState` and a list `[Header]` of message summaries.
 
 ### Definitions
 
@@ -21,7 +23,7 @@ type Consensus = (ConsensusState, [Message]) => Header
 
 ### Blockchain
 
-Defined as blockchain consensus algorithm which generates valid `Header`s.
+A blockchain is a consensus algorithm which generates valid `Header`s.
 It generates a unique list of headers starting from a genesis `ConsensusState` with arbitrary
 messages.
 
@@ -40,40 +42,38 @@ where
 
 #### Blockchain
 
-The headers generated from the `Blockchain` are expected to satisfy the
-followings:
+The headers generated from a `Blockchain` are expected to satisfy the following:
 
-1. The `Header`s MUST NOT have more than one direct child
+1. Each `Header` MUST NOT have more than one direct child
 
-* Satisfied if: deterministic safety
+* Satisfied if: finality & safety
 * Possible violation scenario: validator double signing, chain reorganization (Nakamoto consensus)
 
-2. The `Header`s MUST eventually have at least one direct child
+2. Each `Header` MUST eventually have at least one direct child
 
 * Satisfied if: liveness, light-client verifier continuity
 * Possible violation scenario: synchronised halt, incompatible hard fork
 
-3. The `Header`s MUST be generated from the `Consensus`, which ensures valid transition of the state
+3. Each `Header`s MUST be generated by `Consensus`, which ensures valid state transitions
 
 * Satisfied if: correct block generation & state machine
-* Possible violation scenario: invariant break, supermajor validator cartel
+* Possible violation scenario: invariant break, supermajority validator cartel
 
 If the blockchain does not satisfy any of the above then the IBC protocol
-may not work as intended; the chain can receive multiple conflicting
+may not work as intended: the chain can receive multiple conflicting
 packets, the chain cannot recover from the timeout event, the chain can
 steal the user's asset, etc.
 
 #### Verifier
 
 The validity of `Verifier` is dependent on the security model of the
 `Consensus`. For example, the `Consensus` can be a proof of authority with
-a trusted operator without legal binding, or the a proof of stake but with
+a trusted operator, or the a proof of stake but with
 insufficient value of stake. In such cases, it is possible that the
 security assumptions break, the correspondence between `Consensus` and
 `Verifier` no longer exists, and the behaviour of `Verifier` becomes
 undefined. Also, the `Blockchain` may not longer satisfy
-the requirements above, which leads the chain to be incompatible with IBC
-protocol. The equivocation proof have to be generated and submitted to the
-chain storing the `LightClient`, as defined in
-[ICS ?](https://github.com/cosmos/ics/issues/53), to safely disconnect the
-light client.
+the requirements above, which will cause the chain to be incompatible with the IBC
+protocol. In cases of attributable faults, an equivocation proof can be generated and submitted to the
+chain storing the `LightClient` to safely freeze the light client and
+prevent further IBC packet relay.