message: Refinement on the freshness of proofs
diff: @@ -63,6 +63,7 @@ We identify two basic (high-level) requirements that a connection handshake shou
  In other words, if a connection handshake finishes, the two parties have a consistent view of this connection. We say that Alice stores one end of the connection, label `c1`, and Bob stores the other end of the same connection, label `c2`.
  - **[ICS3-Seq-2-Termination]** Eventually, the modules of Alice and Bob should both finish the handshake, opening a connection.
  +Opening a connection means that Alice and Bob both allocate in their local store a new connection.
  Requirement **[ICS3-Seq-1-Agreement]** represents the basic safety guarantee, while **[ICS3-Seq-2-Termination]** is the basic liveness guarantee we would like to have.
  @@ -240,9 +241,9 @@ If any two modules open a connection, then the client in the first module is con
  The liveness property below is equivalent to **[ICS3-Seq-2-Termination]** (the livenes property in the sequential specification above):
  -- **[ICS3-Proto-5-Termination]**
  +- **[ICS3-Proto-4-Termination]**
  If the two parties involved in a connection handshake are correct, then the connection handshake eventually terminates.
  -Specifically, termination implies that each module allocates in the local state a new `ConnectionEnd` object with `state` field set to `OPEN`.
  +Specifically, termination implies that each module allocates in the local store a new `ConnectionEnd` object with `state` field set to `OPEN`.
  _Remarks_:
  @@ -253,7 +254,7 @@ _Remarks_:
  - One of the mechanisms that enforces the connection integrity property consists of cryptographic proofs, specifically the `ConnProof` type, which asserts that a certain chain stores a certain connection in a certain state.
  -- The `ClientProof` type helps guarantee the state consistency property, by asserting that the client of a certain chain is updated to a certain height of the remote chain.
  +- The `ClientProof` type guarantees the state consistency property, by asserting that the client on a chain is updated to a consensus state of the remote chain.
  - Note that the consistency property works both ways.
  This property applies to _any two modules_ (there is no predefined "first" or "second" module here).
  @@ -585,7 +586,7 @@ Notice that the fields in each datagram match with the corresponding protocol ha
  #### Helper functions & application-level predicates
  -##### `matchingEnds(endLocal, endRemote)`
  +###### `matchingEnds(endLocal, endRemote)`
  Checks that the connection ends in the local and remote arguments match.
  (NB: This does not check the connection state, only the connection parties).
  @@ -610,6 +611,7 @@ This function is analogous to `verifyMembership` of the [ICS 023](#references),
  ###### `localConsensusState` and `clientConsensusState`
  These are analogous to `getConsensusState` and `queryClient` functions.
  +The `clientConsensusState`, in particular, has an implicit requirement that it may not return the consensus state of a client if the height is older than a certain threshold; the `proofsHeight` should not be outdated by more than `100` heights, specifically. (This means that proofs must not be too old.)
  ### Open questions:
  