English spec for SendPacketEvent handling

docs/spec/relayer/Packets.md

@@ -0,0 +1,267 @@
+# IBC packet handling
+
+This document specifies datagram creation logic for packets. It is used by the relayer.
+
+## Data Types
+
+```go
+type Packet {
+    sequence           uint64
+    timeoutHeight      Height
+    timeoutTimestamp   uint64
+    sourcePort         Identifier
+    sourceChannel      Identifier
+    destPort           Identifier
+    destChannel        Identifier
+    data               bytes	
+}
+```
+
+```go
+type PacketRecv {
+     packet          Packet
+     proof           CommitmentProof
+     proofHeight     Height
+}
+```
+
+```go
+type SendPacketEvent {
+    height             Height
+    sequence           uint64
+    timeoutHeight      Height
+    timeoutTimestamp   uint64
+    sourcePort         Identifier
+    sourceChannel      Identifier
+    destPort           Identifier
+    destChannel        Identifier
+    data               bytes	
+}
+```
+
+```go
+type ChannelEnd {
+    state                           ChannelState
+    ordering                        ChannelOrder
+    counterpartyPortIdentifier      Identifier
+    counterpartyChannelIdentifier   Identifier
+    connectionHops                  [Identifier]
+    version                         string
+}
+
+enum ChannelState {
+  INIT,
+  TRYOPEN,
+  OPEN,
+  CLOSED,
+}
+
+enum ChannelOrder {
+  ORDERED,
+  UNORDERED,
+}
+```
+
+```go
+type ConnectionEnd {
+    state                               ConnectionState
+    counterpartyConnectionIdentifier    Identifier
+    counterpartyPrefix                  CommitmentPrefix
+    clientIdentifier                    Identifier
+    counterpartyClientIdentifier        Identifier
+    version                             []string
+}
+
+enum ConnectionState {
+  INIT,
+  TRYOPEN,
+  OPEN,
+}
+```
+
+```go
+type ClientState {
+  chainID                       string
+  validatorSet                  List<Pair<Address, uint64>>
+  trustLevel                    Rational
+  trustingPeriod                uint64
+  unbondingPeriod               uint64
+  latestHeight                  Height
+  latestTimestamp               uint64
+  frozenHeight                  Maybe<uint64>
+  upgradeCommitmentPrefix       CommitmentPrefix
+  upgradeKey                    []byte
+  maxClockDrift                 uint64
+  proofSpecs                    []ProofSpec
+}
+```
+## Helper functions
+
+We assume the existence of the following helper functions:
+
+```go
+// Returns channel end with a commitment proof. 
+GetChannel(chain Chain, 
+           portId Identifier, 
+           channelId Identifier,  
+           proofHeight Height) (ChannelEnd, CommitmentProof)
+
+// Returns connection end with a commitment proof. 
+GetConnection(chain Chain, 
+              connectionId Identifier, 
+              proofHeight Height) (ConnectionEnd, CommitmentProof)
+
+
+// Returns client state with a commitment proof. 
+GetClientState(chain Chain, 
+               clientId Identifier, 
+               proofHeight Height) (ClientState, CommitmentProof)
+
+// Returns packet commitment with a commitment proof. 
+GetPacketCommitment(chain Chain, 
+                    portId Identifier, 
+                    channelId Identifier, 
+                    sequence uint64, 
+                    proofHeight Height) (bytes, CommitmentProof)
+
+// Returns next recv sequence number with a commitment proof. 
+GetNextSequenceRecv(chain Chain, 
+                    portId Identifier, 
+                    channelId Identifier,  
+                    proofHeight Height) (uint64, CommitmentProof)
+
+// Returns packet acknowledgment with a commitment proof. 
+GetPacketAcknowledgement(chain Chain, 
+                         portId Identifier, 
+                         channelId Identifier, 
+                         sequence uint64, 
+                         proofHeight Height) (bytes, CommitmentProof)
+
+// Returns estimate of the consensus height on the given chain. 
+GetConsensusHeight(chain Chain) Height
+
+// Returns estimate of the current time on the given chain. 
+GetCurrentTimestamp(chainB) uint64
+
+```
+
+For functions that return proof, if proof != nil, then the returned value is being verified. 
+The value is being verified using the header's app hash that is provided by the corresponding light client.
+We now show the pseudocode for one of those functions:
+
+```go
+GetChannel(chain Chain, 
+           portId Identifier, 
+           channelId Identifier,  
+           proofHeight Height) (ChannelEnd, CommitmentProof) {
+
+    // Query provable store exposed by the full node of chain. 
+    // The path for the channel end is at channelEnds/ports/{portId}/channels/{channelId}".
+    // The membership proof returned is read at height proofHeight. 
+    channel, proof = QueryChannel(chain, portId, channelId, proofHeight) 
+    if proof == nil return { (nil, nil) }
+
+    header = GetHeader(chain.lc, proofHeight) // get header for height proofHeight using light client of the given chain
+
+    // verify membership of the channel at path channelEnds/ports/{portId}/channels/{channelId} using 
+    // the root hash header.AppHash
+    if verifyMembership(header.AppHash, proofHeight, proof, channelPath(portId, channelId), channel) {
+        return channel, proof
+    } else { return (nil, nil) }
+}
+```
+If LATEST_HEIGHT is passed as a parameter, the data should be read (and the corresponding proof created) 
+at the most recent height. 
+
+
+## Computing destination chain
+
+```golang
+func GetDestinationInfo(ev IBCEvent, chainA Chain) Chain {
+    switch ev.type {
+        case SendPacketEvent: 
+            channel, proof = GetChannel(chain, ev.sourcePort, ev.sourceChannel, ev.Height)
+            if proof == nil return nil
+
+            connectionId = channel.connectionHops[0]
+            connection, proof = GetConnection(chain, connectionId, ev.Height) 
+            if proof == nil return nil
+
+            clientState = GetClientState(chain, connection.clientIdentifier, ev.Height) 
+            return getHostInfo(clientState.chainID) 
+        ...    
+    }
+}
+```
+
+## Datagram creation logic
+
+### PacketRecv datagram creation
+
+```golang
+func createPacketRecvDatagram(ev SendPacketEvent, chainA Chain, chainB Chain, installedHeight Height) PacketRecv {        
+
+    // Stage 1 
+    // Verify if packet is committed to chain A and it is still pending (commitment exists)
+
+    proofHeight = installedHeight - 1
+    packetCommitment, packetCommitmentProof = 
+        GetPacketCommitment(chainA, ev.sourcePort, ev.sourceChannel, ev.sequence, proofHeight)     
+    if packetCommitmentProof != nil { return nil }
+
+    if packetCommitment == null OR
+       packetCommitment != hash(concat(ev.data, ev.timeoutHeight, ev.timeoutTimestamp)) { return nil }
+
+    // Stage 2 
+    // Execute checks IBC handler on chainB will execute
+
+    channel, proof = GetChannel(chainB, ev.destPort, ev.destChannel, LATEST_HEIGHT)
+    if proof != nil { return nil }
+
+    if channel == null OR
+       channel.state != OPEN OR
+       ev.sourcePort != channel.counterpartyPortIdentifier OR
+       ev.sourceChannel != channel.counterpartyChannelIdentifier { return nil }
+
+    connectionId = channel.connectionHops[0]
+    connection, proof = GetConnection(chainB, connectionId, LATEST_HEIGHT) 
+    if proof != nil { return nil }
+
+    if connection == null OR connection.state != OPEN { return nil } 
+
+    if ev.timeoutHeight != 0 AND GetConsensusHeight(chainB) >= ev.timeoutHeight { return nil }
+    if ev.timeoutTimestamp != 0 AND GetCurrentTimestamp(chainB) >= ev.timeoutTimestamp { return nil }
+
+    // we now check if this packet is already received by the destination chain
+    if (channel.ordering === ORDERED) {    
+        nextSequenceRecv, proof = GetNextSequenceRecv(chainB, ev.destPort, ev.destChannel, LATEST_HEIGHT) 
+        if proof != nil { return nil }
+
+        if ev.sequence != nextSequenceRecv { return nil } // packet has already been delivered by another relayer
+
+    } else {
+        packetAcknowledgement, proof = 
+            GetPacketAcknowledgement(chainB, ev.destPort, ev.destChannel, ev.sequence, LATEST_HEIGHT)
+        if proof != nil { return nil }
+
+        if packetAcknowledgement != nil { return nil }
+    }
+
+    // Stage 3
+    // Build datagram as all checks has passed  
+    packet = Packet {
+                sequence: ev.sequence,
+                timeoutHeight: ev.timeoutHeight,
+                timeoutTimestamp: ev.timeoutTimestamp,
+                sourcePort: ev.sourcePort,          
+                sourceChannel: ev.sourceChannel,
+                destPort: ev.destPort,           
+                destChannel: ev.destChannel,        
+                data: ev.data
+    }   
+
+    return PacketRecv { packet, packetCommitmentProof, proofHeight }
+}    
+```
+
+

docs/spec/relayer/Relayer.md

@@ -74,11 +74,15 @@ succeed. The interface between stage 2 and stage 3 is a set of datagrams.
 We assume that the corresponding light client is correctly installed on each chain. 
 
 ```golang
-func handleEvent(ev, chainA, chainB) {
+func handleEvent(ev, chainA) {
     // NOTE: we don't verify if event data are valid at this point. We trust full node we are connected to
     // until some verification fails. Otherwise, we can have Stage 2 (datagram creation being done first).
-
+    
     // Stage 1.
+    // Determine destination chain
+    chainB = GetDestinationInfo(ev, chainA)   
+
+    // Stage 2.
     // Update on `chainB` the IBC client for `chainA` to height `>= targetHeight`.
     targetHeight = ev.height + 1
     // See the code for `updateIBCClient` below.
@@ -87,22 +91,15 @@ func handleEvent(ev, chainA, chainB) {
        return error
     }
 
-    // Stage 2.
+    // Stage 3.
     // Create the IBC datagrams including `ev` & verify them.
+    datagram = createDatagram(ev, chainA, chainB, installedHeight)
 
-    sh = chainA.lc.get_header(installedHeight)
-    while (true) { 
-        datagrams = pendingDatagrams(installedHeight - 1, chainA, chainB)
-        if verifyProof(datagrams, sh.appHash) {
-            break;  
-        }
-        // Full node for `chainA` is faulty. Connect to different node of `chainA` and retry.
-        replaceFullNode(src)        
-     }
-
-    // Stage 3.
+    // Stage 4.
     // Submit datagrams.
-    chainB.submit(datagrams)
+    if datagram != nil {
+        chainB.submit(datagram)
+    }   
 }
 
 
@@ -199,12 +196,12 @@ will eventually have access to a correct full node.
 
 ### Data availability
 
-Note that data written to a store at height h as part of executing block b (b.Height = h) is effectively committed by 
+Note that data written to a store at height *h* as part of executing block *b* (`b.Height = h`) is effectively committed by 
 the next block (at height h+1). The reason is the fact that the data store root hash as an effect of executing block at 
-height h is part of the block header at height h+1. Therefore data read at height h is available until time 
-`t = b.Header.Time + UNBONDING_PERIOD`, where `b.Header.Height = h+1`. After time t we cannot trust that data anymore.
-Note that data present in the store are re-validated by each new block: data added/modified at block h are still 
-valid even if not altered after as they are still "covered" by the root hash of the store. 
+height h is part of the block header at height h+1. Therefore, data read at height h is available until time 
+`t = b.Header.Time + UNBONDING_PERIOD`, where `b.Header.Height = h+1`. After time *t* we cannot trust that data anymore.
+Note that data present in the store are re-validated by each new block: data added/modified at block *h* are still 
+valid even if not altered after, as they are still "covered" by the root hash of the store. 
 
 Therefore UNBONDING_PERIOD gives absolute time bound during which relayer needs to transfer data read at source chain
 to the destination chain. As we will explain below, due to fork detection and accountability protocols, the effective 
@@ -213,17 +210,19 @@ data availability period will be shorter than UNBONDING_PERIOD.
 ### Data verification
 
 As connected chains in IBC do not blindly trust each other, data coming from the opposite chain must be verified at
-the destination before being acted upon. If we assume that data d is read from the data store of a chain at height h,
-
-
-Data verification in IBC is implemented by relying on the concept of light client.
+the destination before being acted upon. Data verification in IBC is implemented by relying on the concept of light client.
 Light client is a process that by relying on an initial trusted header (subjective initialisation), verifies and maintains 
 set of trusted headers. Note that a light client does not maintain full blockchain and does not execute (verify) application
 transitions. It operates by relying on the Tendermint security model, and by applying header verification logic that operates
 only on signed headers (header + corresponding commit). 
 
-More details about light client assumptions and protocols can be found here. For the purpose of this document, we assume
-that a relayer has access to the light client node that provides trusted headers.  
+More details about light client assumptions and protocols can be found 
+[here](https://github.com/tendermint/spec/tree/master/rust-spec/lightclient). For the purpose of this document, we assume
+that a relayer has access to the light client node that provides trusted headers.
+Given a data d read at a given path at height h with a proof p, we assume existence of a function 
+`verifyMembership(header.AppHash, h, proof, path, d)` that returns `true` if data was committed by the corresponding
+chain at height *h*. The trusted header is provided by the corresponding light client. 
+