ICS4: Sequence should be fastforwarded even outside crossing hello in UPGRADE_TRY

[AdityaSripal]

If two crossing hellos are incompatible at the same sequence than they will not be able to proceed.

Suppose one side then makes itself compatible with a new INIT, then the sequences will mismatch but the upgrades are compatible. Then with the current spec, we will require that the sequences match exactly in the crossing hello case thus we cannot proceed. Note we only fastforward the sequence in the non-crossing-hello case.

The only way to progress in this case, would be for the other side to also RE-INIT or cancel the upgrade so that we can proceed.

This is quite inefficient.

The solution is to fastforward even in the non-crossing hello case in TRY.

If the upgrades are indeed incompatible, we still abort the transaction and revert state so we are not in danger of committing incorrect state. However, in this case when both upgrades are compatible and one sequence is higher we can fastforward and continue in the crossing hello case.

See the discovery and fix of this behaviour in the following commits on the quint tests:

https://github.com/cosmos/quint-channel-upgradability/pull/8/commits/4a21351b662c6028eae3ccf78fb0113187c97941

https://github.com/cosmos/quint-channel-upgradability/pull/8/commits/17095a1b0d5773575a532f0568f4577f5f379ae2

[sangier]

Thanks @AdityaSripal! I checked quint too and the proposed solution LGTM!