certusone
/
cosmos-sdk
mirror of https://github.com/certusone/cosmos-sdk.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
cosmos-sdk/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.tla

175 lines
5.4 KiB
Plaintext
Raw Normal View History

Model-based tests for relay functions of ICS-20 token transfer (#8145) * start on MBT for ICS20: setting and checking bank balances * add bank struct for subtracting banks * reconstruct ibc denominations in the bank * add some static tests with bank changes tracking * small fixes * better error handling * add Jsonatr transform from Apalache conterexample into OnRecvPacket test * add example Apalache CE and transformed test * changed apalache-to-recv-test.json to output arrays instead of records * add datastructures for parsing TLA+ tests * remove accidentally committed code * add conversion from TLA+ structs to Go structs * encode abstract ids into addresses via hashes * first run of auto-generated MBT tests * first run of auto-generated MBT tests: fix ports and channels * fix small inconsistencies * fix mbt_relay_test by not setting the bank balances in every iteration * add test for onTimeoutPacket * add handling of OnRecvAcknowledgement to mbt relay test * add handling of SendTransfer * add relay-test.json * revert manual changes in relay-test.json * fix handling of denominations for SendTransfer * setup two test channels A-B, B-C; fix escrow address encoding * a test for all handlers passing * generalize denom handling to arbitrary length + failing denom test * rename test function * MBT test for unsecrow tokens * add model-based generated tests * add model-based tests (prev commit: addded model) * transformed json tests with jsonatr * modify mbt_relay_test.go to execute all MBT tests * cleanup * move jsonatr transforms into another dir * add MBT_README.md Co-authored-by: Federico Kunze <31522760+fedekunze@users.noreply.github.com>
2020-12-11 09:35:44 -08:00
------------------------- MODULE counterexample -------------------------
EXTENDS relay_tests
(* Initial state *)
State1 ==
TRUE
(* Transition 0 to State2 *)
State2 ==
/\ bank = <<
[channel |-> "", id |-> "", port |-> ""], [denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]]
>>
:> 0
/\ count = 0
/\ error = FALSE
/\ handler = ""
/\ history = 0
:> [bankAfter |->
<<
[channel |-> "", id |-> "", port |-> ""], [denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]]
>>
:> 0,
bankBefore |->
<<
[channel |-> "", id |-> "", port |-> ""], [denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]]
>>
:> 0,
error |-> FALSE,
handler |-> "",
packet |->
[data |->
[amount |-> 1,
denomTrace |->
[denom |-> "btc",
prefix0 |->
[channel |-> "cosmos-hub", port |-> "ethereum-hub"],
prefix1 |-> [channel |-> "", port |-> ""]],
receiver |-> "a2",
sender |-> ""],
destChannel |-> "channel-0",
destPort |-> "transfer",
sourceChannel |-> "channel-0",
sourcePort |-> "transfer"]]
/\ p = [data |->
[amount |-> 1,
denomTrace |->
[denom |-> "btc",
prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"],
prefix1 |-> [channel |-> "", port |-> ""]],
receiver |-> "a2",
sender |-> ""],
destChannel |-> "channel-0",
destPort |-> "transfer",
sourceChannel |-> "channel-0",
sourcePort |-> "transfer"]
(* Transition 5 to State3 *)
State3 ==
/\ bank = <<
[channel |-> "", id |-> "", port |-> ""], [denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]]
>>
:> 0
@@ <<
[channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc",
prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"],
prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]]
>>
:> 1
/\ count = 1
/\ error = FALSE
/\ handler = "OnRecvPacket"
/\ history = 0
:> [bankAfter |->
<<
[channel |-> "", id |-> "", port |-> ""], [denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]]
>>
:> 0,
bankBefore |->
<<
[channel |-> "", id |-> "", port |-> ""], [denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]]
>>
:> 0,
error |-> FALSE,
handler |-> "",
packet |->
[data |->
[amount |-> 1,
denomTrace |->
[denom |-> "btc",
prefix0 |->
[channel |-> "cosmos-hub", port |-> "ethereum-hub"],
prefix1 |-> [channel |-> "", port |-> ""]],
receiver |-> "a2",
sender |-> ""],
destChannel |-> "channel-0",
destPort |-> "transfer",
sourceChannel |-> "channel-0",
sourcePort |-> "transfer"]]
@@ 1
:> [bankAfter |->
<<
[channel |-> "", id |-> "", port |-> ""], [denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]]
>>
:> 0
@@ <<
[channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc",
prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"],
prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]]
>>
:> 1,
bankBefore |->
<<
[channel |-> "", id |-> "", port |-> ""], [denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]]
>>
:> 0,
error |-> FALSE,
handler |-> "OnRecvPacket",
packet |->
[data |->
[amount |-> 1,
denomTrace |->
[denom |-> "btc",
prefix0 |->
[channel |-> "cosmos-hub", port |-> "ethereum-hub"],
prefix1 |-> [channel |-> "", port |-> ""]],
receiver |-> "a2",
sender |-> ""],
destChannel |-> "channel-0",
destPort |-> "transfer",
sourceChannel |-> "channel-0",
sourcePort |-> "transfer"]]
/\ p = [data |->
[amount |-> 0,
denomTrace |->
[denom |-> "",
prefix0 |-> [channel |-> "", port |-> ""],
prefix1 |-> [channel |-> "", port |-> ""]],
receiver |-> "",
sender |-> ""],
destChannel |-> "",
destPort |-> "",
sourceChannel |-> "",
sourcePort |-> ""]
(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation ==
BMC!Skolem((\E s$2 \in DOMAIN history:
history[s$2]["handler"] = "OnRecvPacket"
/\ history[s$2]["error"] = FALSE
/\ history[s$2]["packet"]["data"]["amount"] > 0))
================================================================================
\* Created by Apalache on Thu Dec 10 11:01:28 CET 2020
\* https://github.com/informalsystems/apalache