ICS04: Something confusing about function timeoutPacket and timeoutOnClose

[michwqy]

According to

function recvPacket(
  packet: OpaquePacket,
  proof: CommitmentProof,
  proofHeight: Height,
  relayer: string): Packet {
...
    switch channel.order {
...
      case ORDERED_ALLOW_TIMEOUT:
        if (getConsensusHeight() >= packet.timeoutHeight && packet.timeoutHeight != 0) || (currentTimestamp() >= packet.timeoutTimestamp && packet.timeoutTimestamp != 0) {
          nextSequenceRecv = nextSequenceRecv + 1
          provableStore.set(nextSequenceRecvPath(packet.destPort, packet.destChannel), nextSequenceRecv)
          provableStore.set(
          packetReceiptPath(packet.destPort, packet.destChannel, packet.sequence),
            TIMEOUT_RECEIPT
          )
        }
        return;
...
    }
...
    switch channel.order {
...
      case ORDERED_ALLOW_TIMEOUT:
        nextSequenceRecv = nextSequenceRecv + 1
        provableStore.set(nextSequenceRecvPath(packet.destPort, packet.destChannel), nextSequenceRecv)
        break;
...
}

As for packet, there are three scenarios (assume that all previous packets were successfully received).

• Function recvPacket has not been called. So nextSequenceRecv == packet.sequence whether timeout height/timestamp has passed on the counterparty chain or not.
• Function recvPacket has been called and timeout height/timestamp has passed on the counterparty chain. So nextSequenceRecv == packet.sequence +1 and verifyPacketReceipt(...packet.sequence, TIMEOUT_RECEIPT)) == True
• Function recvPacket has been called and timeout height/timestamp has not passed on the counterparty chain. So nextSequenceRecv == packet.sequence +1 and verifyPacketReceipt(...packet.sequence, TIMEOUT_RECEIPT)) == False

So in ORDERED_ALLOW_TIMEOUT channel, a module can claim a packet is timeout if

nextSequenceRecv  == packet.sequence

means function recvPacket has not been called.
or

(nextSequenceRecv  == packet.sequence + 1) &&  (verifyPacketReceipt(...packet.sequence, TIMEOUT_RECEIPT)) == True)

means function recvPacket has been called and timeout height/timestamp has passed.
But in

function timeoutPacket(
  packet: OpaquePacket,
  proof: CommitmentProof,
  proofHeight: Height,
  nextSequenceRecv: Maybe<uint64>,
  relayer: string): Packet {

...
    switch channel.order {
...
      case ORDERED_ALLOW_TIMEOUT:
        abortTransactionUnless(nextSequenceRecv == packet.sequence)
        abortTransactionUnless(connection.verifyPacketReceipt(
          proofHeight,
          proof,
          packet.destPort,
          packet.destChannel,
          packet.sequence
          TIMEOUT_RECEIPT,
        ))
        break;
...
    } 
...
}

I think it means

(nextSequenceRecv  == packet.sequence) &&  (verifyPacketReceipt(...packet.sequence, TIMEOUT_RECEIPT)) == True)

It may be a mistake.

And in

function timeoutOnClose(
  packet: Packet,
  proof: CommitmentProof,
  proofClosed: CommitmentProof,
  proofHeight: Height,
  nextSequenceRecv: Maybe<uint64>,
  relayer: string): Packet {
...

    if channel.order === ORDERED || channel.order == ORDERED_ALLOW_TIMEOUT {
      abortTransactionUnless(connection.verifyNextSequenceRecv(
        proofHeight,
        proof,
        packet.destPort,
        packet.destChannel,
        nextSequenceRecv
      ))
       abortTransactionUnless(nextSequenceRecv <= packet.sequence)
...
...
}

As

The timeoutOnClose function is called by a module in order to prove that the channel to which an unreceived packet was addressed has been closed, so the packet will never be received (even if the timeoutHeight or timeoutTimestamp has not yet been reached).

I don't know if the function timeoutOnClose is allowed to called if timeoutHeight or timeoutTimestamp has been reached. (Like channel is closed after recvPacket called on counterparty chain and before timeoutOnClose called on local chain). But If the answer is yes, the condition should be (nextSequenceRecv <= packet.sequence) || (verifyPacketReceipt(...packet.sequence, TIMEOUT_RECEIPT)) == True).

[crodriguezvega]

Hey @michwqy. Thanks for the questions. I will try to summarise the questions, just so that I can make sure that I understand them.

Question 1:

As you correctly point out, in recvPacket for an ORDERED_ALLOW_TIMEOUT channel the nextSequenceRecv is incremented by 1 both in the successful receive case as well as in the timeout case. So then in timeoutPacket you're suggesting that the check abortTransactionUnless(nextSequenceRecv == packet.sequence) is wrong because nextSequenceRecv was incremented in recvPacket. I think you're right.

Besides that I see that for ORDERED channels the check abortTransactionUnless(nextSequenceRecv == packet.sequence) might also be wrong. In ibc-go we abort the transaction for ORDERED channels if nextSequenceRecv is > the sequence of the packet. I think the same check should be done for ORDERED channels in the spec, since I see that the check is also abortTransactionUnless(nextSequenceRecv == packet.sequence) at the moment.

Question 2:

I think you're also right here and the condition should be fine-tuned to cover the situation you describe. If you have an ORDERED_ALLOW_TIMEOUT channel and a packet has been sent from chain A to chain B but recvPacket is executed on chain B after the timeout has passed (therefore a timeout receipt is written) and then the channel closes before the packet can be timed out on chain A, then if timeoutOnClose is called the nextSequenceRecv on chain B would have already been incremented and the check abortTransactionUnless(nextSequenceRecv <= packet.sequence) will abort the transaction.

I would appreciate if @AdityaSripal could double check both of the above.

[michwqy]

Thanks @crodriguezvega .

Question 1:

In the above discussion, I assumed that all previous packets had been received successfully.
Because I don't quite understand this comment:

only allow timeout on next sequence so all sequences before the timed out packet are processed (received/timed out) before this packet times out.

But if considering previous packets can also be timeout, I think the right code should be

 switch channel.order {
      case ORDERED:
        abortTransactionUnless(nextSequenceRecv <= packet.sequence)
        abortTransactionUnless(connection.verifyNextSequenceRecv(
          proofHeight,
          proof,
          packet.destPort,
          packet.destChannel,
          nextSequenceRecv
        ))
        break;

      case ORDERED_ALLOW_TIMEOUT:
        abortTransactionUnless(nextSequenceRecv > packet.sequence && connection.verifyPacketReceipt(...TIMEOUT_RECEIPT) == FALSE )
        // since nextSequenceRecv <= packet.sequence are right
        abortTransactionUnless(connection.verifyNextSequenceRecv(
          proofHeight,
          proof,
          packet.destPort,
          packet.destChannel,
          nextSequenceRecv
        ))
        break;

Question 2:

I agree what you said.

[crodriguezvega]

Thanks for the reply, @michwqy. Just a question: for ORDERED_ALLOW_TIMEOUT shouldn't the condition be abortTransactionUnless(nextSequenceRecv > packet.sequence && connection.verifyPacketReceipt(...TIMEOUT_RECEIPT) == TRUE)?

[michwqy]

Sorry, it is a mistake. To be honest, abortTransactionUnless is a little confusing. Function timeoutPacket only need to be aborted when nextSequenceRecv > packet.sequence && connection.verifyPacketReceipt(...TIMEOUT_RECEIPT) == FALSE , which means packet has been successfully received.

So the condition should be abortTransactionUnless(nextSequenceRecv <= packet.sequence || connection.verifyPacketReceipt(...TIMEOUT_RECEIPT) == TRUE ), which means the packet has either not been received after timeout height/timestamp reached or it has been received with a TIMEOUT_RECEIPT.

[crodriguezvega]

@michwqy I opened this PR to fix this issue. Let me know what you think, if you have some time to take a look at it.