Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: set upgrade timeout after startFlushUpgradeHandshake in chanUpgradeAck #1040

Merged
merged 2 commits into from
Nov 27, 2023

Conversation

crodriguezvega
Copy link
Contributor

Found this small bug when run the happy path quint test.

cc @AdityaSripal @sangier

Copy link
Contributor

@sangier sangier left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually this is really important. Since we are overriding the upgrade at line 708 in chanUpgradeAck, without the proposed change we are violating the invariant that the upgrade.timeout MUST be set when we move to FLUSHING or directly to FLUSHING_COMPLETE. Indeed we would be storing the upgrade during the startFlushUpgradeHandshake (which contains the timeout value) and then override this value with an upgrade instance which contains the final agreed version but that does not contain the timeout at line 708.

Really good catch! Thank you!

@crodriguezvega
Copy link
Contributor Author

Actually this is really important. Since we are overriding the upgrade at line 708 in chanUpgradeAck, without the proposed change we are violating the invariant that the upgrade.timeout MUST be set when we move to FLUSHING or directly to FLUSHING_COMPLETE. Indeed we would be storing the upgrade during the startFlushUpgradeHandshake (which contains the timeout value) and then override this value with an upgrade instance which contains the final agreed version but that does not contain the timeout at line 708.

Really good catch! Thank you!

Yes, correct! I checked ibc-go and we are good there. :)

@crodriguezvega crodriguezvega changed the title fix: set upgrade timeout after startFlushUpgradeHandshake in chanUpgradeAck` fix: set upgrade timeout after startFlushUpgradeHandshake in chanUpgradeAck Nov 21, 2023
Copy link
Member

@AdityaSripal AdityaSripal left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the catch @crodriguezvega ! Really happy that the formal verification work is paying off!

@AdityaSripal AdityaSripal merged commit 7e9fd7d into main Nov 27, 2023
@AdityaSripal AdityaSripal deleted the carlos/set-upgrade-timeout-chanupgradeack branch November 27, 2023 10:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Archived in project
Development

Successfully merging this pull request may close these issues.

3 participants