Writing quint tests, we realised that restoreChannel function should include in input the upgradeSequence parameter and update the channel.UpgradeSequence accordingly. This change aligns specs and implementation, since in the implementation we have a restoreChannel function with this additional parameter.
This way we can pass:
channel.UpgradeSequence to the restoreChannel in chanUpgradeAck, chanUpgradeConfirm and timeoutChannelUpgrade.
errorReceipt.Sequence to the restoreChannel in cancelChannelUpgrade, ensuring that we can start
a new handshake on a fresh sequence.
sangier
commented
9 months ago
Writing quint tests, we realised that
restoreChannelfunction should include in input theupgradeSequenceparameter and update thechannel.UpgradeSequenceaccordingly. This change aligns specs and implementation, since in the implementation we have arestoreChannelfunction with this additional parameter.This way we can pass:
channel.UpgradeSequenceto therestoreChannelinchanUpgradeAck,chanUpgradeConfirmandtimeoutChannelUpgrade.errorReceipt.Sequenceto therestoreChannelincancelChannelUpgrade, ensuring that we can start a new handshake on a fresh sequence.