ICS28: Set initH in onChanOpenConfirm

spec/app/ics-028-cross-chain-validation/overview_and_basic_concepts.md

@@ -245,7 +245,9 @@ Thus, although the infractions are committed on the consumer chains and evidence
 
 The following figure shows the intuition behind such a mapping using the provided VSCs. 
 The four unbonding operations (i.e., undelegations) occur on the provider chain and, as a consequence, the provider chain provides VSCs to the consumer chain, e.g., `undelegate-3` results in `VSC3` being provided.
-The four colors (i.e., red, blue, green, and yellow) indicate the mapping of consumer chain heights to provider chain heights (note that on the provider chain there is only one block of a given color).  
+The four colors (i.e., red, blue, green, and yellow) indicate the mapping of consumer chain heights to provider chain heights. 
+Note that on the provider chain there is only one block of a given color. 
+Also, note that the three white blocks between the green and the yellow blocks on the provider chain have the same validator set.  
 As a result, a validator misbehaving on the consumer chain, e.g., in either of the two green blocks, is slashed the same as if misbehaving on the provider chain, e.g., in the green block. 
 This ensures that once unbonding operations are initiated, the corresponding unbonding tokens are not slashed for infractions committed in the subsequent blocks, e.g., the tokens unbonding due to `undelegate-3` are not slashed for infractions committed in or after the green blocks.
 
@@ -263,8 +265,9 @@ For clarity, we use `Hp*` and `Hc*` to denote block heights on the provider chai
   > **Note**: It is possible for multiple VSCs to be received by the consumer chain within the same block. For more details, take a look at the [Validator sets, validator updates and VSCs](./system_model_and_properties.md#validator-sets-validator-updates-and-vscs) section.
 - By default, every consumer CCV module maps any block height to `0` (i.e., VSC IDs start from `1`). 
   Intuitively, this means that the voting power on the consumer chain at height `Hc` with `HtoVSC(Hc) = 0` was setup at genesis during Channel Initialization. 
-- For every consumer chain, the provider CCV module sets `VSCtoH[0]` to the height at which the first VSC was provided to this consumer chain. 
-  Intuitively, this means that the validator set on the provider chain at height `VSCtoH[0]` matches the validator set on the consumer chain at all heights `Hc` with `HtoVSC[Hc] = 0`.
+- For every consumer chain, the provider CCV module sets `VSCtoH[0]` to the height when it establishes the CCV channel to this consumer chain. 
+  Note that the validator set on the provider chain at height `VSCtoH[0]` matches the validator set at the height when the first VSC is provided to this consumer chain. 
+  This means that this validator set on the provider chain matches the validator set on the consumer chain at all heights `Hc` with `HtoVSC[Hc] = 0`.
 
 The following figure shows an overview of the Consumer Initiated Slashing operation of CCV. 
 
@@ -277,7 +280,7 @@ The following figure shows an overview of the Consumer Initiated Slashing operat
 - The provider CCV module receives at (slashing) height `Hp1` the `SlashPacket` with `vscId = HtoVSC[Hc1]`. 
   As a result, it requests the provider Slashing module to slash `V`, but it set the infraction height to `VSCtoH[vscId]`, i.e., 
     - if `vscId != 0`, the height on the provider chain where the voting power was updated by the VSC with ID `vscId`;
-    - otherwise, the height at which the first VSC was provided to this consumer chain.
+    - otherwise, the height at which the CCV channel to this consumer chain was established.
   > **Note**: As a consequence of slashing (and potentially jailing) `V`, the Staking module updates accordingly `V`'s voting power. This update MUST be visible in the next VSC provided to the consumer chains.  
 
 For a more detailed description of Consumer Initiated Slashing, take a look at the [technical specification](./technical_specification.md#consumer-initiated-slashing).

spec/app/ics-028-cross-chain-validation/system_model_and_properties.md

@@ -138,6 +138,10 @@ CCV provides the following system properties.
   - `T` (equivalent) tokens MUST be eventually minted on the provider chain and then distributed among the validators that are part of the validator set;
   - the total supply of tokens MUST be preserved, i.e., the `T` (original) tokens are escrowed on the consumer chain.
 
+- ***Distribution Invariant***: If a consumer chain sends to the provider chain an amount `T` of tokens as reward for providing security, then
+  - `T` (equivalent) tokens are eventually minted on the provider chain and then distributed among the validators that are part of the validator set;
+  - the total supply of tokens is preserved, i.e., the `T` (original) tokens are escrowed on the consumer chain.
+
 ### CCV Channel
 [↑ Back to Outline](#outline)
 
@@ -230,7 +234,7 @@ The following properties define the guarantees of CCV on *registering* on the pr
 
 - ***Provider Slashing Warranty***: If the provider CCV module receives at height `hs` from a consumer chain `cc` a `SlashPacket` containing a validator `val` and a VSC ID `vscId`, 
   then it MUST make at height `hs` *exactly one* request to the provider Slashing module to slash `val` for misbehaving at height `h`, such that
-  - if `vscId = 0`, `h` is the height of the block when the provider chain provided to `cc` the first VSC;
+  - if `vscId = 0`, `h` is the height of the block when the provider chain established a CCV channel to `cc`;
   - otherwise, `h` is the height of the block immediately subsequent to the block when the provider chain provided to `cc` the VSC with ID `vscId`.
 
 - ***VSC Maturity and Slashing Order***: If a consumer chain sends to the provider chain a `SlashPacket` before a maturity notification of a VSC, then the provider chain MUST NOT receive the maturity notification before the `SlashPacket`.
@@ -387,4 +391,4 @@ i.e., we informally prove the properties described in the [previous section](#de
   This means that *exactly* the amount of tokens `Token(Power(cc,hi,val))` is slashed on the provider chain. 
 
 - ***Consumer Rewards Distribution***: The first part of the *Consumer Rewards Distribution* property (i.e., the tokens are eventually minted on the provider chain and then distributed among the validators) follows directly from *Distribution Liveness* and *Distribution Warranty*. 
-  The second part of the *Consumer Rewards Distribution* property (i.e., the total supply of tokens is preserved) follows directly from the *Supply* property of the Fungible Token Transfer protocol (see [ICS 20](../ics-020-fungible-token-transfer/README.md)). 
+  The second part of the *Consumer Rewards Distribution* property (i.e., the total supply of tokens is preserved) follows directly from the *Supply* property of the Fungible Token Transfer protocol (see [ICS 20](../ics-020-fungible-token-transfer/README.md)). 

spec/app/ics-028-cross-chain-validation/technical_specification.md

@@ -269,8 +269,9 @@ This section describes the internal state of the CCV module. For simplicity, the
   }
 - `vscId: uint64` is a monotonic strictly increasing and positive ID that is used to uniquely identify the VSCs sent to the consumer chains. 
   Note that `0` is used as a special ID for the mapping from consumer heights to provider heights.
-- `initH: Map<string, Height>` is a mapping from consumer chain IDs to the heights on the provider chain. 
-  For every consumer chain, the mapping stores the height when the first VSC was provided to that consumer chain. 
+- `initialHeights: Map<string, Height>` is a mapping from consumer chain IDs to the heights on the provider chain. 
+  For every consumer chain, the mapping stores the height when the CCV channel to that consumer chain is established. 
+  Note that the provider validator set at this height matches the validator set at the height when the first VSC is provided to that consumer chain.
   It enables the mapping from consumer heights to provider heights.
 - `VSCtoH: Map<uint64, Height>` is a mapping from VSC IDs to heights on the provider chain. It enables the mapping from consumer heights to provider heights, 
   i.e., the voting power at height `VSCtoH[id]` on the provider chain was last updated by the validator updates contained in the VSC with ID `id`.  
@@ -633,6 +634,8 @@ function onChanOpenConfirm(
     // set channel mappings
     chainToChannel[clientState.chainId] = channelIdentifier
     channelToChain[channelIdentifier] = clientState.chainId
+    // set initialHeights for this consumer chain
+    initialHeights[chainId] = getCurrentHeight()
 }
 ```
 - **Caller**
@@ -645,7 +648,9 @@ function onChanOpenConfirm(
   - If a CCV channel for this consumer chain already exists, then 
     - the channel closing handshake is initiated for the underlying channel;
     - the transaction is aborted.
-  - Otherwise, the channel mappings are set, i.e., `chainToChannel` and `channelToChain`.
+  - Otherwise, 
+    - the channel mappings are set, i.e., `chainToChannel` and `channelToChain`;
+    - `initialHeights[chainId]` is set to the current height.
 - **Error Condition**
   - None.
 
@@ -1213,11 +1218,6 @@ function EndBlock(): [ValidatorUpdate] {
 
     // check whether there is an established CCV channel to the consumer chain
     if chainId IN chainToChannel.Keys() {
-      // set initH for this consumer chain (if not done already)
-      if chainId NOT IN initH.Keys() {
-        initH[chainId] = getCurrentHeight()
-      }
-
       // get the channel ID for the given consumer chain ID
       channelId = chainToChannel[chainId]
 
@@ -1259,7 +1259,6 @@ function EndBlock(): [ValidatorUpdate] {
       - `slashRequests[chainId]` is emptied;
       - `packetData` is appended to the list of pending `VSCPacket`s associated to `chainId`, i.e., `pendingVSCPackets[chainId]`.
     - If there is an established CCV channel for the the consumer chain with `chainId`, then
-      - if `initH[chainId]` is not already set, then `initH[chainId]` is set to the current height;
       - for each `VSCPacketData` in the list of pending VSCPackets associated to `chainId`
         - a packet with the `VSCPacketData` is sent on the channel associated with the consumer chain with `chainId`;
       - all the pending VSCPackets associated to `chainId` are removed.
@@ -1745,7 +1744,7 @@ function onRecvSlashPacket(packet: Packet): bytes {
   if packet.data.vscId == 0 {
     // the infraction happened before sending any VSC to this chain
     chainId = channelToChain[packet.getDestinationChannel()]
-    infractionHeight = initH[chainId]
+    infractionHeight = initialHeights[chainId]
   }
   else {
     infractionHeight = VSCtoH[packet.data.vscId]
@@ -1779,7 +1778,7 @@ function onRecvSlashPacket(packet: Packet): bytes {
     - the channel closing handshake is initiated;
     - an error acknowledgment is returned.
   - Otherwise,
-    - if `packet.data.vscId == 0`, `infractionHeight` is set to `initH[chainId]`, with `chainId = channelToChain[packet.getDestinationChannel()]`, i.e., the height when the first VSC was provided to this consumer chain;
+    - if `packet.data.vscId == 0`, `infractionHeight` is set to `initialHeights[chainId]`, with `chainId = channelToChain[packet.getDestinationChannel()]`, i.e., the height when the CCV channel to this consumer chain is established;
     - otherwise, `infractionHeight` is set to `VSCtoH[packet.data.vscId]`, i.e., the height at which the voting power was last updated by the validator updates in the VSC with ID `packet.data.vscId`;
     - a request is made to the Slashing module to slash the validator with address `packet.data.valAddress` for misbehaving at height `infractionHeight`;
     - a request is made to the Slashing module to jail the validator with address `packet.data.valAddress` for a period `data.jailTime`;