ICS2: Expand definitions and remove cycles (#716)

* improve Definitions and Desired Properties

* revert Header to UpdateMessage change

* add note about additional properties

spec/core/ics-002-client-semantics/README.md

@@ -71,37 +71,72 @@ could be provided as executable WASM functions when the client instance is creat
 
 * `get`, `set`, `Path`, and `Identifier` are as defined in [ICS 24](../ics-024-host-requirements).
 
-* `CommitmentRoot` is as defined in [ICS 23](../ics-023-vector-commitments). It must provide an inexpensive way for
-  downstream logic to verify whether key/value pairs are present in state at a particular height.
-
-* `ConsensusState` is an opaque type representing the state of a validity predicate.
-  `ConsensusState` must be able to verify state updates agreed upon by the associated consensus algorithm.
-  It must also be serialisable in a canonical fashion so that third parties, such as remote state machines,
-  can check that a particular state machine has stored a particular `ConsensusState`. It must finally be
-  introspectable by the state machine which it is for, such that the state machine can look up its
-  own `ConsensusState` at a past height.
-
-* `ClientState` is an opaque type representing the state of a client.
-  A `ClientState` must expose query functions to verify membership or non-membership of
-  key/value pairs in state at particular heights and to retrieve the current `ConsensusState`.
+* `Consensus` is a state update generating algorithm. It takes the previous state of a state machine together 
+  with a set of messages (i.e., state machine transactions) and generates a valid state update of the state machine.
+  Every state machine MUST have a `Consensus` that generates a unique, ordered list of state updates 
+  starting from a genesis state. 
+
+  This specification expects that the state updates generated by `Consensus` 
+  satisfy the following properties:
+  * Every state update MUST NOT have more than one direct successor in the list of state updates. 
+    In other words, the state machine MUST guarantee *finality* and *safety*. 
+  * Every state update MUST eventually have a successor in the list of state updates. 
+    In other words, the state machine MUST guarantee *liveness*.
+  * Every state update MUST be valid (i.e., valid state transitions).
+    In other words, `Consensus` MUST be *honest*, 
+    e.g., in the case `Consensus` is a Byzantine fault-tolerant consensus algorithm, 
+    such as Tendermint, less than a third of block producers MAY be Byzantine.
+
+  Unless the state machine satisfies all of the above properties, the IBC protocol
+may not work as intended, e.g., users' assets might be stolen. Note that specific client 
+types may require additional properties. 
+
+* `Height` specifies the order of the state updates of a state machine, e.g., a sequence number. 
+  This entails that each state update is mapped to a `Height`.
+
+* `CommitmentRoot` is as defined in [ICS 23](../ics-023-vector-commitments). 
+  It provides an efficient way for higher-level protocol abstractions to verify whether
+  a particular state transition has occurred on the remote state machine, i.e.,
+  it enables proofs of inclusion or non-inclusion of particular values at particular paths 
+  in the state of the remote state machine at particular `Height`s.
+
+* `ValidityPredicate` is a function that validates state updates. 
+  Using the `ValidityPredicate` SHOULD be more computationally efficient than executing `Consensus`.
+
+* `ConsensusState` is the *trusted view* of the state of a state machine at a particular `Height`.
+  It MUST contain sufficient information to enable the `ValidityPredicate` to validate state updates, 
+  which can then be used to generate new `ConsensusState`s. 
+  It MUST be serialisable in a canonical fashion so that remote parties, such as remote state machines,
+  can check whether a particular `ConsensusState` was stored by a particular state machine.
+  It MUST be introspectable by the state machine whose view it represents, 
+  i.e., a state machine can look up its own `ConsensusState`s at past `Height`s.
+
+* `ClientState` is the state of a client. It MUST expose an interface to higher-level protocol abstractions, 
+  e.g., functions to verify proofs of the existence of particular values at particular paths at particular `Height`s.
+
+* `MisbehaviourPredicate` is a that checks whether the rules of `Consensus` were broken, 
+  in which case the client MUST be *frozen*, i.e., no subsequent `ConsensusState`s can be generated.
+
+* `Misbehaviour` is the proof needed by the `MisbehaviourPredicate` to determine whether 
+  a violation of the consensus protocol occurred. For example, in the case the state machine 
+  is a blockchain, a `Misbehaviour` might consist of two signed block headers with 
+  different `CommitmentRoot`s, but the same `Height`.
 
 ### Desired Properties
 
-Light clients must provide a secure algorithm to verify other chains' canonical headers,
-using the existing `ConsensusState`. The higher level abstractions will then be able to verify
-sub-components of the state with the `CommitmentRoot`s stored in the `ConsensusState`, which are
-guaranteed to have been committed by the other chain's consensus algorithm.
+Light clients MUST provide state verification functions that provide a secure way 
+to verify the state of the remote state machines using the existing `ConsensusState`s. 
+These state verification functions enable higher-level protocol abstractions to 
+verify sub-components of the state of the remote state machines.
 
-Validity predicates are expected to reflect the behaviour of the full nodes which are running the
-corresponding consensus algorithm. Given a `ConsensusState` and a list of messages, if a full node
-accepts the new `Header` generated with `Commit`, then the light client MUST also accept it,
-and if a full node rejects it, then the light client MUST also reject it.
+`ValidityPredicate`s MUST reflect the behaviour of the remote state machine and its `Consensus`, i.e.,
+`ValidityPredicate`s accept *only* state updates that contain state updates generated by 
+the `Consensus` of the remote state machine.
 
-Light clients are not replaying the whole message transcript, so it is possible under cases of
-consensus misbehaviour that the light clients' behaviour differs from the full nodes'.
-In this case, a misbehaviour proof which proves the divergence between the validity predicate
-and the full node can be generated and submitted to the chain so that the chain can safely deactivate the
-light client, invalidate past state roots, and await higher-level intervention.
+In case of misbehavior, the behaviour of the `ValidityPredicate` might differ from the behaviour of 
+the remote state machine and its `Consensus` (since clients do not execute the `Consensus` of the 
+remote state machine). In this case, a `Misbehaviour` SHOULD be submitted to the host state machine, 
+which would result in the client being frozen and higher-level intervention being necessary.
 
 ## Technical Specification
 
@@ -155,67 +190,6 @@ a commitment root, and possibly updates to the validity predicate.
 type Header = bytes
 ```
 
-#### Consensus
-
-`Consensus` is a `Header` generating function which takes the previous
-`ConsensusState` with the messages and returns the result.
-
-```typescript
-type Consensus = (ConsensusState, [Message]) => Header
-```
-
-### Blockchain
-
-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.
-
-`Blockchain` is defined as
-
-```typescript
-interface Blockchain {
-  genesis: ConsensusState
-  consensus: Consensus
-}
-```
-where
-  * `Genesis` is the genesis `ConsensusState`
-  * `Consensus` is the header generating function
-
-The headers generated from a `Blockchain` are expected to satisfy the following:
-
-1. Each `Header` MUST NOT have more than one direct child
-
-* Satisfied if: finality & safety
-* Possible violation scenario: validator double signing, chain reorganisation (Nakamoto consensus)
-
-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. 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, super-majority validator cartel
-
-Unless the blockchain satisfies all of the above the IBC protocol
-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.
-
-The validity of the validity predicate is dependent on the security model of the
-`Consensus`. For example, the `Consensus` can be a proof of authority with
-a trusted operator, or 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
-the validity predicate no longer exists, and the behaviour of the validity predicate becomes
-undefined. Also, the `Blockchain` may no longer satisfy
-the requirements above, which will cause the chain to be incompatible with the IBC
-protocol. In cases of attributable faults, a misbehaviour proof can be generated and submitted to the
-chain storing the client to safely freeze the light client and
-prevent further IBC packet relay.
-
 #### Validity predicate
 
 A validity predicate is an opaque function defined by a client type to verify `Header`s depending on the current `ConsensusState`.