Relayer TLA+: Support for running Apalache #224
Conversation
There was a problem hiding this comment.
The spec looks amazing, but the complexity is above my level, so it's difficult to review.
Maybe it would be a good idea to have a call where Ilina offers a walk-through some parts of the design here, because I don't understand it enough to leave meaningful PR comments.
Apalache gets killed at 10 steps. I'm able to check 9 steps on my machine, in 49 min. TLC checks the spec with the same constant values, up to diameter 38, in 3 min 😐 |
|
Did you try to increase the parameters and see, whether it degrades? How about proving an inductive invariant with Apalache. Do you think it would be an insane task? |
|
If we can model check it with TLC, I think that's fine. We should wrap this up and work on packets. |
* expriments with apalache * apalache file * Type annotations for Apalache * apalache type annotations * final apalache type annotations * removed PacketHandlers.tla and dependencies
Closes: #165
Description
Added support for running Apalache on the relayer spec. Currently, we can check the invariant
ICS18Invup to 9 steps with Apalache, for height 2 and two concurrent relayers.Most of the changes are done in
RelayerDefinitions.tla, where the appropriate types and operators for type annotattions are defined. These are then used in various places throught the spec.Note: the branch is called ilina/packets, but there isn't any support for packet handling yet.
For contributor use:
docs/) and code commentsFiles changedin the Github PR explorer