Running Apalache on IBC TLA+ specs

[istoilkovska]

Thanks a lot for going through all that work! How about actual verification with Apalache? Do all or some of the specs go through? And if so, does you have a sense of how much time it takes?

Originally posted by @romac in informalsystems/ibc-rs#820 (comment)

[istoilkovska]

Current status of running Apalache on the TLA+ specs done in the branch ilina/running_apalache

There are .cfg and MC_*.tla files for all the specs. All specs contain type annotations for Apalache's type checker Snowcat and have been type-checked.

Running Apalache on the MC_*.tla files fails, as described here. Thus, I ran Apalache with the .cfg files and got the following output:

client

• running apalache-mc check --config=ICS02SingleChainEnvironment.cfg ICS02SingleChainEnvironment.tla and apalache-mc check --config=ICS02TwoChainsEnvironment.cfg ICS02TwoChainsEnvironment.tla produces the same error, but neither spec defines a recursive operator called clientNr:

PASS #4: UnrollPass                                               I@17:30:09.376
  > Unroller                                                      I@17:30:09.410
Input error (see the manual): Recursive operator clientNr requires an annotation UNROLL_DEFAULT_clientNr. See: https://apalache.informal.systems/docs/apalache/principles.html#recursion  E@17:30:09.460

fungible-token-transfer

• in this case, running apalache-mc typecheck MC_IBCTokenTransfer.tla succeeds, but running apalache-mc check MC_IBCTokenTransfer.tla produces an error, as described here
• running apalache-mc check --config=IBCTokenTransfer.cfg IBCTokenTransfer.tla reports an error about unexpected expressions:

...
PASS #12: AnalysisPass                                            I@17:45:04.020
 > Marking skolemizable existentials and sets to be expanded...   I@17:45:04.022
  > SkolemizationMarker                                           I@17:45:04.023
  > ExpansionMarker                                               I@17:45:04.032
IBCTokenTransferDefinitions.tla:187:24-187:36: unexpected expression: Seq(({"chanAtoB", "chanBtoA"} ∪ {"portA", "portB"}) ∪ {"atom", "eth"}) E@17:45:04.147
IBCTokenTransferDefinitions.tla:282:32-285:43: unexpected expression: Seq({<<t_73$1, t_74$1>> : t_73$1 ∈ ({["sequence" ↦ t_6w$1, "timeoutHeight" ↦ t_6x$1, "data" ↦ t_6y$1, "srcPortID" ↦ t_6z$1, "srcChannelID" ↦ t_70$1, "dstPortID" ↦ t_71$1, "dstChannelID" ↦ t_72$1] : t_6w$1 ∈ (1 .. 5), t_6x$1 ∈ (1 .. 5), t_6y$1 ∈ ({["denomination" ↦ t_6s$1, "amount" ↦ t_6t$1, "sender" ↦ t_6u$1, "receiver" ↦ t_6v$1] : t_6s$1 ∈ Seq(({"chanAtoB", "chanBtoA"} ∪ {"portA", "portB"}) ∪ {"atom", "eth"}), t_6t$1 ∈ (0 .. 5), t_6u$1 ∈ {"chainA", "chainB"}, t_6v$1 ∈ {"chainA", "chainB"}}), t_6z$1 ∈ {"portA", "portB"}, t_70$1 ∈ {"chanAtoB", "chanBtoA"}, t_71$1 ∈ {"portA", "portB"}, t_72$1 ∈ {"chanAtoB", "chanBtoA"}}), t_74$1 ∈ BOOLEAN}) E@17:45:04.195
Unexpected expressions in the specification (see the error messages) E@17:45:04.196
It took me 0 days  0 hours  0 min  6 sec                          I@17:45:04.197
Total time: 6.386 sec                                             I@17:45:04.198
EXITCODE: ERROR (99)

ibc-core

• running apalache-mc check --config=IBCCore.cfg IBCCore.tla reports an error about unexpected expressions:

...
PASS #12: AnalysisPass                                            I@17:45:04.020
 > Marking skolemizable existentials and sets to be expanded...   I@17:45:04.022
  > SkolemizationMarker                                           I@17:45:04.023
  > ExpansionMarker                                               I@17:45:04.032
IBCTokenTransferDefinitions.tla:187:24-187:36: unexpected expression: Seq(({"chanAtoB", "chanBtoA"} ∪ {"portA", "portB"}) ∪ {"atom", "eth"}) E@17:45:04.147
IBCTokenTransferDefinitions.tla:282:32-285:43: unexpected expression: Seq({<<t_73$1, t_74$1>> : t_73$1 ∈ ({["sequence" ↦ t_6w$1, "timeoutHeight" ↦ t_6x$1, "data" ↦ t_6y$1, "srcPortID" ↦ t_6z$1, "srcChannelID" ↦ t_70$1, "dstPortID" ↦ t_71$1, "dstChannelID" ↦ t_72$1] : t_6w$1 ∈ (1 .. 5), t_6x$1 ∈ (1 .. 5), t_6y$1 ∈ ({["denomination" ↦ t_6s$1, "amount" ↦ t_6t$1, "sender" ↦ t_6u$1, "receiver" ↦ t_6v$1] : t_6s$1 ∈ Seq(({"chanAtoB", "chanBtoA"} ∪ {"portA", "portB"}) ∪ {"atom", "eth"}), t_6t$1 ∈ (0 .. 5), t_6u$1 ∈ {"chainA", "chainB"}, t_6v$1 ∈ {"chainA", "chainB"}}), t_6z$1 ∈ {"portA", "portB"}, t_70$1 ∈ {"chanAtoB", "chanBtoA"}, t_71$1 ∈ {"portA", "portB"}, t_72$1 ∈ {"chanAtoB", "chanBtoA"}}), t_74$1 ∈ BOOLEAN}) E@17:45:04.195
Unexpected expressions in the specification (see the error messages) E@17:45:04.196
It took me 0 days  0 hours  0 min  6 sec                          I@17:45:04.197
Total time: 6.386 sec                                             I@17:45:04.198
EXITCODE: ERROR (99)

packet-delay

• running apalache-mc check --config=IBCPacketDelay.cfg IBCPacketDelay.tla reports an error about unexpected expressions:

...
PASS #12: AnalysisPass                                            I@17:51:04.047
 > Marking skolemizable existentials and sets to be expanded...   I@17:51:04.049
  > SkolemizationMarker                                           I@17:51:04.050
  > ExpansionMarker                                               I@17:51:04.053
IBCPacketDelayDefinitions.tla:390:8-390:22: unexpected expression: "UNORDERED"()() E@17:51:04.107
IBCPacketDelayDefinitions.tla:390:8-390:22: unexpected expression: "UNORDERED"()() E@17:51:04.141
Unexpected expressions in the specification (see the error messages) E@17:51:04.141
It took me 0 days  0 hours  0 min  4 sec                          I@17:51:04.142
Total time: 4.489 sec                                             I@17:51:04.143
EXITCODE: ERROR (99)

[adizere]

Closing: there are no plans to maintain or continue model-checking the docs/spec, and moving to MBT-based testing instead.

CC: @jtremback @andrey-kuprianov @konnov please update or re-open the issue if you find it necessary.