Upgrade IBC-rs TLA+ MBT models to modern Apalache type annotations

[andrey-kuprianov]

Current TLA+ models in IBC-rs are using old-style Apalache type annotations, which makes it impossible to model-check them with the recent Apalache versions.

We address the problem with this issue, and upgrade the IBC-rs TLA+ specs to use the modern Apalache type annotations 😸.

This will also allow to upgrade later to the recent version of Modelator.

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate milestone (priority) applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned