From a821fe4a617f5195a83e11c869f6eaf632bf94f8 Mon Sep 17 00:00:00 2001 From: Andrey Kuprianov <59489470+andrey-kuprianov@users.noreply.github.com> Date: Fri, 11 Dec 2020 18:35:44 +0100 Subject: [PATCH] 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> --- .../transfer/keeper/MBT_README.md | 51 + .../transfer/keeper/keeper_test.go | 4 +- .../transfer/keeper/mbt_relay_test.go | 399 ++++++ .../model_based_tests/Test5Packets.json | 492 +++++++ .../keeper/model_based_tests/Test5Packets.tla | 1056 +++++++++++++++ .../Test5PacketsAllDifferentPass.json | 612 +++++++++ .../Test5PacketsAllDifferentPass.tla | 1188 +++++++++++++++++ .../TestOnRecvAcknowledgementErrorFail.json | 58 + .../TestOnRecvAcknowledgementErrorFail.tla | 159 +++ .../TestOnRecvAcknowledgementErrorPass.json | 159 +++ .../TestOnRecvAcknowledgementErrorPass.tla | 310 +++++ .../TestOnRecvAcknowledgementResultFail.json | 58 + .../TestOnRecvAcknowledgementResultFail.tla | 159 +++ .../TestOnRecvAcknowledgementResultPass.json | 58 + .../TestOnRecvAcknowledgementResultPass.tla | 159 +++ .../TestOnRecvPacketFail.json | 58 + .../TestOnRecvPacketFail.tla | 159 +++ .../TestOnRecvPacketPass.json | 73 + .../TestOnRecvPacketPass.tla | 174 +++ .../model_based_tests/TestOnTimeoutFail.json | 58 + .../model_based_tests/TestOnTimeoutFail.tla | 159 +++ .../model_based_tests/TestOnTimeoutPass.json | 159 +++ .../model_based_tests/TestOnTimeoutPass.tla | 310 +++++ .../TestSendTransferFail.json | 58 + .../TestSendTransferFail.tla | 159 +++ .../TestSendTransferPass.json | 174 +++ .../TestSendTransferPass.tla | 323 +++++ .../model_based_tests/TestUnescrowTokens.json | 305 +++++ .../model_based_tests/TestUnescrowTokens.tla | 563 ++++++++ .../transfer/keeper/relay_model/account.tla | 36 + .../keeper/relay_model/account_record.tla | 46 + .../relay_model/apalache-to-relay-test.json | 100 ++ .../relay_model/apalache-to-relay-test2.json | 104 ++ .../transfer/keeper/relay_model/denom.tla | 50 + .../keeper/relay_model/denom_record.tla | 53 + .../keeper/relay_model/denom_record2.tla | 114 ++ .../keeper/relay_model/denom_sequence.tla | 47 + .../keeper/relay_model/identifiers.tla | 10 + .../transfer/keeper/relay_model/relay.tla | 278 ++++ .../keeper/relay_model/relay_tests.tla | 96 ++ 40 files changed, 8587 insertions(+), 1 deletion(-) create mode 100644 x/ibc/applications/transfer/keeper/MBT_README.md create mode 100644 x/ibc/applications/transfer/keeper/mbt_relay_test.go create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/Test5Packets.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/Test5Packets.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/Test5PacketsAllDifferentPass.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/Test5PacketsAllDifferentPass.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorFail.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorFail.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorPass.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorPass.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultFail.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultFail.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultPass.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultPass.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketFail.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketFail.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutFail.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutFail.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutPass.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutPass.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferFail.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferFail.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferPass.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferPass.tla create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestUnescrowTokens.json create mode 100644 x/ibc/applications/transfer/keeper/model_based_tests/TestUnescrowTokens.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/account.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/account_record.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/apalache-to-relay-test.json create mode 100644 x/ibc/applications/transfer/keeper/relay_model/apalache-to-relay-test2.json create mode 100644 x/ibc/applications/transfer/keeper/relay_model/denom.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/denom_record.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/denom_record2.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/denom_sequence.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/identifiers.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/relay.tla create mode 100644 x/ibc/applications/transfer/keeper/relay_model/relay_tests.tla diff --git a/x/ibc/applications/transfer/keeper/MBT_README.md b/x/ibc/applications/transfer/keeper/MBT_README.md new file mode 100644 index 0000000000..8a5930f6d3 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/MBT_README.md @@ -0,0 +1,51 @@ +## Token Transfer Model-based Testing Guide + +In the process of IBC Audit performed by Informal Systems, we have implemented +a preliminary set of model-based tests for the ICS-20 Token Transfer implementation. + +Model-based tests are based on the formal `TLA+` model of the Token transfer relay functions: see [relay.tla](relay_model/relay.tla). +The tests themselves are simple `TLA+` assertions, that describe the desired shape of execution that send or receive tokens; +see [relay_tests.tla](relay_model/relay_tests.tla) for some examples. +To be able to specify test assertions the TLA+ model contains the `history` variable, +which records the whole execution history. +So, by way of referring to `history` you simply specify declaratively what execution history you want to see. + +After you have specified your `TLA+` test, you can run it using [Apalache model checker](https://github.com/informalsystems/apalache). +E.g. for the test `TestUnescrowTokens` run + +```bash +apalache-mc check --inv=TestUnescrowTokensInv relay_tests.tla +``` + +In case there are no error in the TLA+ model or in the test assertions, this will produce a couple of so-called _counterexamples_. +This is a terminology from the model-checking community; for the testing purposes they can be considered simply as model executions. +See the files `counterexample.tla` for human-readable representation, and `counterexample.json` for machine-readable one. + +In order to execute the produced test, you need to translate it into another format. +For that translation you need the tool [Jsonatr (JSON Arrifact Translator)](https://github.com/informalsystems/jsonatr). +It performs the translation using this [transformation spec](relay_model/apalache-to-relay-test2.json); + +To transform a counterexample into a test, run + +```bash +jsonatr --use apalache-to-relay-test2.json --in counterexample.json --out model_based_tests/YourTestName.json +``` + +Now, if you run `go test` in this directory, the file you have produced above should be picked up by the [model-based test driver](mbt_relay_test.go), +and executed automatically. + + +The easiest way to run Apalache is by +[using a Docker image](https://github.com/informalsystems/apalache/blob/master/docs/manual.md#useDocker); +to run Jsonatr you need to locally clone the repository, and then, +after building it, add the `target/debug` directory into your `PATH`. + +To wrap Apalache docker image into an executable you might create the following executable bash script `apalache-mc`: + +```bash +#!/bin/bash +docker run --rm -v $(pwd):/var/apalache apalache/mc $@ +``` + + +In case of any questions please don't hesitate to contact Andrey Kuprianov (andrey@informal.systems). \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/keeper_test.go b/x/ibc/applications/transfer/keeper/keeper_test.go index 0181c399ab..cce9cbccae 100644 --- a/x/ibc/applications/transfer/keeper/keeper_test.go +++ b/x/ibc/applications/transfer/keeper/keeper_test.go @@ -20,14 +20,16 @@ type KeeperTestSuite struct { // testing chains used for convenience and readability chainA *ibctesting.TestChain chainB *ibctesting.TestChain + chainC *ibctesting.TestChain queryClient types.QueryClient } func (suite *KeeperTestSuite) SetupTest() { - suite.coordinator = ibctesting.NewCoordinator(suite.T(), 2) + suite.coordinator = ibctesting.NewCoordinator(suite.T(), 3) suite.chainA = suite.coordinator.GetChain(ibctesting.GetChainID(0)) suite.chainB = suite.coordinator.GetChain(ibctesting.GetChainID(1)) + suite.chainC = suite.coordinator.GetChain(ibctesting.GetChainID(2)) queryHelper := baseapp.NewQueryServerTestHelper(suite.chainA.GetContext(), suite.chainA.App.InterfaceRegistry()) types.RegisterQueryServer(queryHelper, suite.chainA.App.TransferKeeper) diff --git a/x/ibc/applications/transfer/keeper/mbt_relay_test.go b/x/ibc/applications/transfer/keeper/mbt_relay_test.go new file mode 100644 index 0000000000..f6a30ceb7e --- /dev/null +++ b/x/ibc/applications/transfer/keeper/mbt_relay_test.go @@ -0,0 +1,399 @@ +package keeper_test + + +/// This file is a test driver for model-based tests generated from the TLA+ model of token transfer +/// Written by Andrey Kuprianov within the scope of IBC Audit performed by Informal Systems. +/// In case of any questions please don't hesitate to contact andrey@informal.systems. + + +import ( + "encoding/json" + "fmt" + sdk "github.com/cosmos/cosmos-sdk/types" + sdkerrors "github.com/cosmos/cosmos-sdk/types/errors" + "github.com/cosmos/cosmos-sdk/x/ibc/applications/transfer/types" + clienttypes "github.com/cosmos/cosmos-sdk/x/ibc/core/02-client/types" + channeltypes "github.com/cosmos/cosmos-sdk/x/ibc/core/04-channel/types" + "github.com/cosmos/cosmos-sdk/x/ibc/core/exported" + ibctesting "github.com/cosmos/cosmos-sdk/x/ibc/testing" + "github.com/tendermint/tendermint/crypto" + "io/ioutil" + "strconv" + "strings" +) + + +type TlaBalance struct { + Address []string `json:"address"` + Denom []string `json:"denom"` + Amount int64 `json:"amount"` +} + +type TlaFungibleTokenPacketData struct { + Sender string `json:"sender"` + Receiver string `json:"receiver"` + Amount int `json:"amount"` + Denom []string `json:"denom"` +} + +type TlaFungibleTokenPacket struct { + SourceChannel string `json:"sourceChannel"` + SourcePort string `json:"sourcePort"` + DestChannel string `json:"destChannel"` + DestPort string `json:"destPort"` + Data TlaFungibleTokenPacketData `json:"data"` +} + +type TlaOnRecvPacketTestCase = struct { + // The required subset of bank balances + BankBefore []TlaBalance `json:"bankBefore"` + // The packet to process + Packet TlaFungibleTokenPacket `json:"packet"` + // The handler to call + Handler string `json:"handler"` + // The expected changes in the bank + BankAfter []TlaBalance `json:"bankAfter"` + // Whether OnRecvPacket should fail or not + Error bool `json:"error"` +} + +type FungibleTokenPacket struct { + SourceChannel string + SourcePort string + DestChannel string + DestPort string + Data types.FungibleTokenPacketData +} + +type OnRecvPacketTestCase = struct { + description string + // The required subset of bank balances + bankBefore []Balance + // The packet to process + packet FungibleTokenPacket + // The handler to call + handler string + // The expected bank state after processing (wrt. bankBefore) + bankAfter []Balance + // Whether OnRecvPacket should pass or fail + pass bool +} + +type OwnedCoin struct { + Address string + Denom string +} + +type Balance struct { + Id string + Address string + Denom string + Amount sdk.Int +} + + +func AddressFromString(address string) string { + return sdk.AccAddress(crypto.AddressHash([]byte(address))).String() +} + +func AddressFromTla(addr []string) string { + if len(addr) != 3 { + panic("failed to convert from TLA+ address: wrong number of address components") + } + s := "" + if len(addr[0]) == 0 && len(addr[1]) == 0 { + // simple address: id + s = addr[2] + } else if len(addr[2]) == 0 { + // escrow address: ics20-1\x00port/channel + s = fmt.Sprintf("%s\x00%s/%s", types.Version, addr[0], addr[1]) + } else { + panic("failed to convert from TLA+ address: neither simple nor escrow address") + } + return s +} + +func DenomFromTla(denom []string) string { + var i int + for i = 0; i+1 < len(denom) && len(denom[i])==0 && len(denom[i+1])==0; i+=2 { + // skip empty prefixes + } + return strings.Join(denom[i:], "/") +} + +func BalanceFromTla(balance TlaBalance) Balance { + return Balance{ + Id: AddressFromTla(balance.Address), + Address: AddressFromString(AddressFromTla(balance.Address)), + Denom: DenomFromTla(balance.Denom), + Amount: sdk.NewInt(balance.Amount), + } +} + +func BalancesFromTla(tla []TlaBalance) []Balance { + balances := make([]Balance,0) + for _, b := range tla { + balances = append(balances, BalanceFromTla(b)) + } + return balances +} + +func FungibleTokenPacketFromTla(packet TlaFungibleTokenPacket) FungibleTokenPacket { + return FungibleTokenPacket{ + SourceChannel: packet.SourceChannel, + SourcePort: packet.SourcePort, + DestChannel: packet.DestChannel, + DestPort: packet.DestPort, + Data: types.NewFungibleTokenPacketData( + DenomFromTla(packet.Data.Denom), + uint64(packet.Data.Amount), + AddressFromString(packet.Data.Sender), + AddressFromString(packet.Data.Receiver)), + } +} + +func OnRecvPacketTestCaseFromTla(tc TlaOnRecvPacketTestCase) OnRecvPacketTestCase { + return OnRecvPacketTestCase{ + description: "auto-generated", + bankBefore: BalancesFromTla(tc.BankBefore), + packet: FungibleTokenPacketFromTla(tc.Packet), + handler: tc.Handler, + bankAfter: BalancesFromTla(tc.BankAfter), // TODO different semantics + pass: !tc.Error, + } +} + +var addressMap = make(map[string]string) + + + +type Bank struct { + balances map[OwnedCoin]sdk.Int +} + +// Make an empty bank +func MakeBank() Bank { + return Bank{ balances: make(map[OwnedCoin]sdk.Int) } +} + +// Subtract other bank from this bank +func (bank *Bank) Sub(other *Bank) Bank { + diff := MakeBank() + for coin, amount := range bank.balances { + otherAmount, exists := other.balances[coin] + if exists { + diff.balances[coin] = amount.Sub(otherAmount) + } else { + diff.balances[coin] = amount + } + } + for coin, amount := range other.balances { + if _, exists := bank.balances[coin]; !exists { + diff.balances[coin] = amount.Neg() + } + } + return diff +} + +// Set specific bank balance +func (bank *Bank) SetBalance(address string, denom string, amount sdk.Int) { + bank.balances[OwnedCoin{address, denom}] = amount +} + +// Set several balances at once +func (bank *Bank) SetBalances(balances []Balance) { + for _, balance := range balances { + bank.balances[OwnedCoin{balance.Address, balance.Denom}] = balance.Amount + addressMap[balance.Address] = balance.Id + } +} + +func NullCoin() OwnedCoin { + return OwnedCoin{ + Address: AddressFromString(""), + Denom: "", + } +} + +// Set several balances at once +func BankFromBalances(balances []Balance) Bank{ + bank := MakeBank() + for _, balance := range balances { + coin := OwnedCoin{balance.Address, balance.Denom} + if coin != NullCoin() { // ignore null coin + bank.balances[coin] = balance.Amount + addressMap[balance.Address] = balance.Id + } + } + return bank +} + + +// String representation of all bank balances +func (bank *Bank) String() string { + str := "" + for coin, amount := range bank.balances { + str += coin.Address; + if addressMap[coin.Address] != "" { + str += "(" + addressMap[coin.Address] + ")" + } + str += " : " + coin.Denom + " = " + amount.String() + "\n" } + return str +} + +// String representation of non-zero bank balances +func (bank *Bank) NonZeroString() string { + str := "" + for coin, amount := range bank.balances { + if !amount.IsZero() { + str += coin.Address + " : " + coin.Denom + " = " + amount.String() + "\n" + } + } + return str +} + +// Construct a bank out of the chain bank +func BankOfChain(chain *ibctesting.TestChain) Bank { + bank := MakeBank() + chain.App.BankKeeper.IterateAllBalances(chain.GetContext(), func(address sdk.AccAddress, coin sdk.Coin) (stop bool){ + fullDenom := coin.Denom + if strings.HasPrefix(coin.Denom, "ibc/") { + fullDenom, _ = chain.App.TransferKeeper.DenomPathFromHash(chain.GetContext(), coin.Denom) + } + bank.SetBalance(address.String(), fullDenom, coin.Amount) + return false + }) + return bank +} + +// Set balances of the chain bank for balances present in the bank +func (suite *KeeperTestSuite) SetChainBankBalances(chain *ibctesting.TestChain, bank *Bank) error { + for coin, amount := range bank.balances { + address, err := sdk.AccAddressFromBech32(coin.Address) + if err != nil { + return err + } + trace := types.ParseDenomTrace(coin.Denom) + err = chain.App.BankKeeper.SetBalance(chain.GetContext(), address, sdk.NewCoin(trace.IBCDenom(), amount)) + if err != nil { + return err + } + } + return nil +} + +// Check that the state of the bank is the bankBefore + expectedBankChange +func (suite *KeeperTestSuite) CheckBankBalances(chain *ibctesting.TestChain, bankBefore *Bank, expectedBankChange *Bank) error { + bankAfter := BankOfChain(chain) + bankChange := bankAfter.Sub(bankBefore) + diff := bankChange.Sub(expectedBankChange) + NonZeroString := diff.NonZeroString() + if len(NonZeroString) != 0 { + return sdkerrors.Wrap(sdkerrors.ErrInvalidCoins, "Unexpected changes in the bank: \n" + NonZeroString) + } + return nil +} + + +func (suite *KeeperTestSuite) TestModelBasedRelay() { + dirname := "model_based_tests/" + files,err := ioutil.ReadDir(dirname) + if err != nil { + panic(fmt.Errorf("Failed to read model-based test files: %w", err)) + } + for _, file_info := range files { + var tlaTestCases = []TlaOnRecvPacketTestCase{} + if ! strings.HasSuffix(file_info.Name(), ".json") { + continue + } + jsonBlob, err := ioutil.ReadFile(dirname + file_info.Name()) + if err != nil { + panic(fmt.Errorf("Failed to read JSON test fixture: %w", err)) + } + err = json.Unmarshal([]byte(jsonBlob), &tlaTestCases) + if err != nil { + panic(fmt.Errorf("Failed to parse JSON test fixture: %w", err)) + } + + suite.SetupTest() + _, _, connAB, connBA := suite.coordinator.SetupClientConnections(suite.chainA, suite.chainB, exported.Tendermint) + _, _, connBC, connCB := suite.coordinator.SetupClientConnections(suite.chainB, suite.chainC, exported.Tendermint) + suite.coordinator.CreateTransferChannels(suite.chainA, suite.chainB, connAB, connBA, channeltypes.UNORDERED) + suite.coordinator.CreateTransferChannels(suite.chainB, suite.chainC, connBC, connCB, channeltypes.UNORDERED) + + for i, tlaTc := range tlaTestCases { + tc := OnRecvPacketTestCaseFromTla(tlaTc) + registerDenom := func() { + denomTrace := types.ParseDenomTrace(tc.packet.Data.Denom) + traceHash := denomTrace.Hash() + if !suite.chainB.App.TransferKeeper.HasDenomTrace(suite.chainB.GetContext(), traceHash) { + suite.chainB.App.TransferKeeper.SetDenomTrace(suite.chainB.GetContext(), denomTrace) + } + } + + description := file_info.Name() + " # " + strconv.Itoa(i+1) + suite.Run(fmt.Sprintf("Case %s", description), func() { + seq := uint64(1) + packet := channeltypes.NewPacket(tc.packet.Data.GetBytes(), seq, tc.packet.SourcePort, tc.packet.SourceChannel, tc.packet.DestPort, tc.packet.DestChannel, clienttypes.NewHeight(0, 100), 0) + bankBefore := BankFromBalances(tc.bankBefore) + realBankBefore := BankOfChain(suite.chainB) + // First validate the packet itself (mimics what happens when the packet is being sent and/or received) + err := packet.ValidateBasic() + if err != nil { + suite.Require().False(tc.pass, err.Error()) + return + } + switch tc.handler { + case "SendTransfer": + var sender sdk.AccAddress; + sender, err = sdk.AccAddressFromBech32(tc.packet.Data.Sender); + if err != nil { + panic("MBT failed to convert sender address") + } + registerDenom(); + denomTrace := types.ParseDenomTrace(tc.packet.Data.Denom) + denom := denomTrace.IBCDenom() + err = sdk.ValidateDenom(denom); + if err == nil { + err = suite.chainB.App.TransferKeeper.SendTransfer( + suite.chainB.GetContext(), + tc.packet.SourcePort, + tc.packet.SourceChannel, + sdk.NewCoin(denom, sdk.NewIntFromUint64(tc.packet.Data.Amount)), + sender, + tc.packet.Data.Receiver, + clienttypes.NewHeight(0, 110), + 0) + } + case "OnRecvPacket": + err = suite.chainB.App.TransferKeeper.OnRecvPacket(suite.chainB.GetContext(), packet, tc.packet.Data) + case "OnTimeoutPacket": + registerDenom(); + err = suite.chainB.App.TransferKeeper.OnTimeoutPacket(suite.chainB.GetContext(), packet, tc.packet.Data) + case "OnRecvAcknowledgementResult": + err = suite.chainB.App.TransferKeeper.OnAcknowledgementPacket( + suite.chainB.GetContext(), packet, tc.packet.Data, + channeltypes.NewResultAcknowledgement(nil)) + case "OnRecvAcknowledgementError": + registerDenom(); + err = suite.chainB.App.TransferKeeper.OnAcknowledgementPacket( + suite.chainB.GetContext(), packet, tc.packet.Data, + channeltypes.NewErrorAcknowledgement("MBT Error Acknowledgement")) + default: + err = fmt.Errorf("Unknown handler: %s", tc.handler) + } + if err != nil { + suite.Require().False(tc.pass, err.Error()) + return + } + bankAfter := BankFromBalances(tc.bankAfter) + expectedBankChange := bankAfter.Sub(&bankBefore) + if err := suite.CheckBankBalances(suite.chainB, &realBankBefore, &expectedBankChange); err != nil { + suite.Require().False(tc.pass, err.Error()) + return + } + suite.Require().True(tc.pass) + }) + } + } +} diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/Test5Packets.json b/x/ibc/applications/transfer/keeper/model_based_tests/Test5Packets.json new file mode 100644 index 0000000000..6ccdccc8ae --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/Test5Packets.json @@ -0,0 +1,492 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-1", + "destPort": "transfer", + "data": { + "sender": "a3", + "receiver": "a3", + "amount": 2, + "denom": [ + "", + "", + "", + "", + "btc" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "ethereum-hub", + "sourcePort": "channel-0", + "destChannel": "channel-1", + "destPort": "transfer", + "data": { + "sender": "a1", + "receiver": "a3", + "amount": 1, + "denom": [ + "cosmos-hub", + "", + "", + "", + "btc" + ] + } + }, + "handler": "SendTransfer", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "error": true + }, + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-1", + "destPort": "transfer", + "data": { + "sender": "a2", + "receiver": "a2", + "amount": 4, + "denom": [ + "", + "", + "ethereum-hub", + "cosmos-hub", + "atom" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "ethereum-hub", + "cosmos-hub", + "atom" + ], + "amount": 4 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-1", + "destPort": "transfer", + "data": { + "sender": "", + "receiver": "a2", + "amount": 4, + "denom": [ + "", + "", + "ethereum-hub", + "cosmos-hub", + "atom" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "ethereum-hub", + "cosmos-hub", + "atom" + ], + "amount": 4 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "ethereum-hub", + "cosmos-hub", + "atom" + ], + "amount": 8 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "cosmos-hub", + "sourcePort": "bitcoin-hub", + "destChannel": "channel-0", + "destPort": "channel-1", + "data": { + "sender": "a1", + "receiver": "", + "amount": 1, + "denom": [ + "transfer", + "channel-0", + "transfer", + "channel-0", + "atom" + ] + } + }, + "handler": "SendTransfer", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "ethereum-hub", + "cosmos-hub", + "atom" + ], + "amount": 8 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "ethereum-hub", + "cosmos-hub", + "atom" + ], + "amount": 8 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-1", + "btc" + ], + "amount": 2 + } + ], + "error": true + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/Test5Packets.tla b/x/ibc/applications/transfer/keeper/model_based_tests/Test5Packets.tla new file mode 100644 index 0000000000..9691eec2f2 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/Test5Packets.tla @@ -0,0 +1,1056 @@ +------------------------- 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 |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 3 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 +/\ 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 |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> "cosmos-hub"]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "ethereum-hub", + sourcePort |-> "channel-0"] + +(* Transition 0 to State4 *) + +State4 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 +/\ count = 2 +/\ error = TRUE +/\ handler = "SendTransfer" +/\ 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 |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> TRUE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> "cosmos-hub"]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "ethereum-hub", + sourcePort |-> "channel-0"]] +/\ p = [data |-> + [amount |-> 4, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a2"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 5 to State5 *) + +State5 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 4 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 +/\ count = 3 +/\ 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 |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> TRUE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> "cosmos-hub"]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "ethereum-hub", + sourcePort |-> "channel-0"]] + @@ 3 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 4 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 4, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> + [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a2"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 4, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 5 to State6 *) + +State6 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 8 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 +/\ count = 4 +/\ 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 |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> TRUE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> "cosmos-hub"]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "ethereum-hub", + sourcePort |-> "channel-0"]] + @@ 3 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 4 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 4, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> + [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a2"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 4 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 8 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 4 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 4, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> + [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]], + receiver |-> "", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "channel-1", + sourceChannel |-> "cosmos-hub", + sourcePort |-> "bitcoin-hub"] + +(* Transition 0 to State7 *) + +State7 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 8 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 +/\ count = 5 +/\ error = TRUE +/\ handler = "SendTransfer" +/\ 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 |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> TRUE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> "cosmos-hub"]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "ethereum-hub", + sourcePort |-> "channel-0"]] + @@ 3 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 4 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 4, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> + [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a2"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 4 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 8 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 4 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 4, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> + [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 5 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 8 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "ethereum-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 8 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "channel-1", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + error |-> TRUE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]], + receiver |-> "", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "channel-1", + sourceChannel |-> "cosmos-hub", + sourcePort |-> "bitcoin-hub"]] +/\ 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 == + count >= 5 + /\ BMC!Skolem((\E s1$2 \in DOMAIN history: + BMC!Skolem((\E s2$2 \in DOMAIN history: + ~(history[s1$2]["handler"] = history[s2$2]["handler"]))))) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:52:41 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/Test5PacketsAllDifferentPass.json b/x/ibc/applications/transfer/keeper/model_based_tests/Test5PacketsAllDifferentPass.json new file mode 100644 index 0000000000..6a039f3eca --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/Test5PacketsAllDifferentPass.json @@ -0,0 +1,612 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a3", + "receiver": "a2", + "amount": 3, + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ] + } + }, + "handler": "OnTimeoutPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 3 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-1", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a2", + "receiver": "a1", + "amount": 3, + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "btc" + ] + } + }, + "handler": "OnRecvAcknowledgementError", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 3 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "btc" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 3 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-1", + "destPort": "transfer", + "data": { + "sender": "a1", + "receiver": "a2", + "amount": 3, + "denom": [ + "", + "", + "cosmos-hub", + "cosmos-hub", + "atom" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "btc" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 3 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "atom" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "btc" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 3 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "cosmos-hub", + "sourcePort": "bitcoin-hub", + "destChannel": "transfer", + "destPort": "cosmos-hub", + "data": { + "sender": "a1", + "receiver": "", + "amount": 2, + "denom": [ + "", + "channel-0", + "channel-1", + "channel-1", + "" + ] + } + }, + "handler": "OnRecvAcknowledgementResult", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "atom" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "btc" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 3 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "atom" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "btc" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 3 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-1", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a3", + "receiver": "a3", + "amount": 1, + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ] + } + }, + "handler": "SendTransfer", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "atom" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "btc" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 3 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "atom" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-1", + "cosmos-hub", + "cosmos-hub", + "btc" + ], + "amount": 3 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 2 + }, + { + "address": [ + "transfer", + "channel-1", + "" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "eth" + ], + "amount": 1 + } + ], + "error": false + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/Test5PacketsAllDifferentPass.tla b/x/ibc/applications/transfer/keeper/model_based_tests/Test5PacketsAllDifferentPass.tla new file mode 100644 index 0000000000..89e6d87be5 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/Test5PacketsAllDifferentPass.tla @@ -0,0 +1,1188 @@ +------------------------- 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 |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 6 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3 +/\ count = 1 +/\ error = FALSE +/\ handler = "OnTimeoutPacket" +/\ 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 |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + 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 |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnTimeoutPacket", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a2"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"] + +(* Transition 10 to State4 *) + +State4 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3 +/\ count = 2 +/\ error = FALSE +/\ handler = "OnRecvAcknowledgementError" +/\ 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 |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + 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 |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnTimeoutPacket", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvAcknowledgementError", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a2"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 5 to State5 *) + +State5 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3 +/\ count = 3 +/\ 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 |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + 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 |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnTimeoutPacket", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvAcknowledgementError", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a2"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"]] + @@ 3 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "", + prefix0 |-> [channel |-> "channel-1", port |-> "channel-1"], + prefix1 |-> [channel |-> "channel-0", port |-> ""]], + receiver |-> "", + sender |-> "a1"], + destChannel |-> "transfer", + destPort |-> "cosmos-hub", + sourceChannel |-> "cosmos-hub", + sourcePort |-> "bitcoin-hub"] + +(* Transition 12 to State6 *) + +State6 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3 +/\ count = 4 +/\ error = FALSE +/\ handler = "OnRecvAcknowledgementResult" +/\ 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 |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + 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 |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnTimeoutPacket", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvAcknowledgementError", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a2"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"]] + @@ 3 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 4 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvAcknowledgementResult", + packet |-> + [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "", + prefix0 |-> [channel |-> "channel-1", port |-> "channel-1"], + prefix1 |-> [channel |-> "channel-0", port |-> ""]], + receiver |-> "", + sender |-> "a1"], + destChannel |-> "transfer", + destPort |-> "cosmos-hub", + sourceChannel |-> "cosmos-hub", + sourcePort |-> "bitcoin-hub"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"] + +(* Transition 1 to State7 *) + +State7 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 1 +/\ count = 5 +/\ error = FALSE +/\ handler = "SendTransfer" +/\ 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 |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + 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 |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnTimeoutPacket", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvAcknowledgementError", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a2"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"]] + @@ 3 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 4 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvAcknowledgementResult", + packet |-> + [data |-> + [amount |-> 2, + denomTrace |-> + [denom |-> "", + prefix0 |-> [channel |-> "channel-1", port |-> "channel-1"], + prefix1 |-> [channel |-> "channel-0", port |-> ""]], + receiver |-> "", + sender |-> "a1"], + destChannel |-> "transfer", + destPort |-> "cosmos-hub", + sourceChannel |-> "cosmos-hub", + sourcePort |-> "bitcoin-hub"]] + @@ 5 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> + "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 1, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 3 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 0, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "cosmos-hub", port |-> "transfer"]], + receiver |-> "", + sender |-> ""], + destChannel |-> "bitcoin-hub", + destPort |-> "ethereum-hub", + sourceChannel |-> "transfer", + sourcePort |-> "channel-1"] + +(* The following formula holds true in the last state and violates the invariant *) + +InvariantViolation == + (count >= 5 + /\ (\A s1$2 \in DOMAIN history: + \A s2$2 \in DOMAIN history: + s1$2 = s2$2 \/ ~(history[s1$2]["handler"] = history[s2$2]["handler"]))) + /\ (\A s$2 \in DOMAIN history: + s$2 <= 0 + \/ (history[s$2]["error"] = FALSE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 12:49:42 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorFail.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorFail.json new file mode 100644 index 0000000000..f1f553210b --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorFail.json @@ -0,0 +1,58 @@ +[ + { + "packet": { + "sourceChannel": "", + "sourcePort": "", + "destChannel": "", + "destPort": "", + "data": { + "sender": "a1", + "receiver": "a2", + "amount": 1, + "denom": [ + "cosmos-hub", + "transfer", + "channel-0", + "cosmos-hub", + "btc" + ] + } + }, + "handler": "OnRecvAcknowledgementError", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "error": true + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorFail.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorFail.tla new file mode 100644 index 0000000000..583b3211dc --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorFail.tla @@ -0,0 +1,159 @@ +------------------------- 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 |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""] + +(* Transition 7 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 +/\ count = 1 +/\ error = TRUE +/\ handler = "OnRecvAcknowledgementError" +/\ 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 |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] + @@ 1 + :> [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 |-> TRUE, + handler |-> "OnRecvAcknowledgementError", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] +/\ 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"] = "OnRecvAcknowledgementError" + /\ history[s$2]["error"] = TRUE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:15:18 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorPass.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorPass.json new file mode 100644 index 0000000000..3fbfe7fdf0 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorPass.json @@ -0,0 +1,159 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-1", + "destPort": "transfer", + "data": { + "sender": "", + "receiver": "a1", + "amount": 1, + "denom": [ + "", + "", + "channel-0", + "ethereum-hub", + "btc" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a1" + ], + "denom": [ + "transfer", + "channel-1", + "channel-0", + "ethereum-hub", + "btc" + ], + "amount": 1 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-1", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a1", + "receiver": "a2", + "amount": 1, + "denom": [ + "transfer", + "channel-1", + "channel-0", + "ethereum-hub", + "btc" + ] + } + }, + "handler": "OnRecvAcknowledgementError", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a1" + ], + "denom": [ + "transfer", + "channel-1", + "channel-0", + "ethereum-hub", + "btc" + ], + "amount": 1 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a1" + ], + "denom": [ + "transfer", + "channel-1", + "channel-0", + "ethereum-hub", + "btc" + ], + "amount": 2 + } + ], + "error": false + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorPass.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorPass.tla new file mode 100644 index 0000000000..cd43eb2647 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementErrorPass.tla @@ -0,0 +1,310 @@ +------------------------- 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 |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 2 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "channel-1", 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 |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "channel-1", 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 |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"] + +(* Transition 11 to State4 *) + +State4 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 2 +/\ count = 2 +/\ error = FALSE +/\ handler = "OnRecvAcknowledgementError" +/\ 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 |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "channel-1", 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 |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> ""], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 1, + error |-> FALSE, + handler |-> "OnRecvAcknowledgementError", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "ethereum-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + 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"] = "OnRecvAcknowledgementError" + /\ history[s$2]["error"] = FALSE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:14:33 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultFail.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultFail.json new file mode 100644 index 0000000000..9110a38ab6 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultFail.json @@ -0,0 +1,58 @@ +[ + { + "packet": { + "sourceChannel": "", + "sourcePort": "", + "destChannel": "", + "destPort": "", + "data": { + "sender": "a1", + "receiver": "a2", + "amount": 1, + "denom": [ + "cosmos-hub", + "transfer", + "channel-0", + "cosmos-hub", + "btc" + ] + } + }, + "handler": "OnRecvAcknowledgementResult", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "error": true + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultFail.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultFail.tla new file mode 100644 index 0000000000..b97ec73a3d --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultFail.tla @@ -0,0 +1,159 @@ +------------------------- 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 |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""] + +(* Transition 13 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 +/\ count = 1 +/\ error = TRUE +/\ handler = "OnRecvAcknowledgementResult" +/\ 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 |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] + @@ 1 + :> [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 |-> TRUE, + handler |-> "OnRecvAcknowledgementResult", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] +/\ 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"] = "OnRecvAcknowledgementResult" + /\ history[s$2]["error"] = TRUE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:13:42 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultPass.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultPass.json new file mode 100644 index 0000000000..5215df7da3 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultPass.json @@ -0,0 +1,58 @@ +[ + { + "packet": { + "sourceChannel": "ethereum-hub", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "ethereum-hub", + "data": { + "sender": "a1", + "receiver": "a2", + "amount": 1, + "denom": [ + "cosmos-hub", + "transfer", + "channel-0", + "cosmos-hub", + "btc" + ] + } + }, + "handler": "OnRecvAcknowledgementResult", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "error": false + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultPass.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultPass.tla new file mode 100644 index 0000000000..f9d049c546 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvAcknowledgementResultPass.tla @@ -0,0 +1,159 @@ +------------------------- 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 |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "ethereum-hub", + sourceChannel |-> "ethereum-hub", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "ethereum-hub", + sourceChannel |-> "ethereum-hub", + sourcePort |-> "transfer"] + +(* Transition 12 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 +/\ count = 1 +/\ error = FALSE +/\ handler = "OnRecvAcknowledgementResult" +/\ 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 |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "ethereum-hub", + sourceChannel |-> "ethereum-hub", + sourcePort |-> "transfer"]] + @@ 1 + :> [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 |-> "OnRecvAcknowledgementResult", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "ethereum-hub", + sourceChannel |-> "ethereum-hub", + 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"] = "OnRecvAcknowledgementResult" + /\ history[s$2]["error"] = FALSE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:12:59 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketFail.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketFail.json new file mode 100644 index 0000000000..9a7e8c406e --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketFail.json @@ -0,0 +1,58 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "", + "receiver": "", + "amount": 1, + "denom": [ + "", + "", + "transfer", + "channel-0", + "" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "error": true + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketFail.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketFail.tla new file mode 100644 index 0000000000..980be28ae2 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketFail.tla @@ -0,0 +1,159 @@ +------------------------- 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 |-> "", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "", + sender |-> ""], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "", + sender |-> ""], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 3 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 +/\ count = 1 +/\ error = TRUE +/\ 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 |-> "", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "", + sender |-> ""], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [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 |-> TRUE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "", + 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"] = TRUE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:02:31 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.json new file mode 100644 index 0000000000..35f94c5720 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.json @@ -0,0 +1,73 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "", + "receiver": "a2", + "amount": 1, + "denom": [ + "", + "", + "ethereum-hub", + "cosmos-hub", + "btc" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-0", + "ethereum-hub", + "cosmos-hub", + "btc" + ], + "amount": 1 + } + ], + "error": false + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.tla new file mode 100644 index 0000000000..342b097feb --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnRecvPacketPass.tla @@ -0,0 +1,174 @@ +------------------------- 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 diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutFail.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutFail.json new file mode 100644 index 0000000000..a78ed85ca5 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutFail.json @@ -0,0 +1,58 @@ +[ + { + "packet": { + "sourceChannel": "", + "sourcePort": "", + "destChannel": "", + "destPort": "", + "data": { + "sender": "a1", + "receiver": "a2", + "amount": 1, + "denom": [ + "cosmos-hub", + "transfer", + "channel-0", + "cosmos-hub", + "btc" + ] + } + }, + "handler": "OnTimeoutPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "error": true + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutFail.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutFail.tla new file mode 100644 index 0000000000..1bc209d9d5 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutFail.tla @@ -0,0 +1,159 @@ +------------------------- 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 |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""] + +(* Transition 6 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 +/\ count = 1 +/\ error = TRUE +/\ handler = "OnTimeoutPacket" +/\ 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 |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] + @@ 1 + :> [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 |-> TRUE, + handler |-> "OnTimeoutPacket", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "channel-0"], + prefix1 |-> [channel |-> "transfer", port |-> "cosmos-hub"]], + receiver |-> "a2", + sender |-> "a1"], + destChannel |-> "", + destPort |-> "", + sourceChannel |-> "", + sourcePort |-> ""]] +/\ 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"] = "OnTimeoutPacket" + /\ history[s$2]["error"] = TRUE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:09:25 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutPass.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutPass.json new file mode 100644 index 0000000000..3136aace65 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutPass.json @@ -0,0 +1,159 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-1", + "destPort": "transfer", + "data": { + "sender": "a3", + "receiver": "a1", + "amount": 1, + "denom": [ + "", + "", + "bitcoin-hub", + "transfer", + "btc" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a1" + ], + "denom": [ + "transfer", + "channel-1", + "bitcoin-hub", + "transfer", + "btc" + ], + "amount": 1 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-1", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a1", + "receiver": "", + "amount": 1, + "denom": [ + "transfer", + "channel-1", + "bitcoin-hub", + "transfer", + "btc" + ] + } + }, + "handler": "OnTimeoutPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a1" + ], + "denom": [ + "transfer", + "channel-1", + "bitcoin-hub", + "transfer", + "btc" + ], + "amount": 1 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a1" + ], + "denom": [ + "transfer", + "channel-1", + "bitcoin-hub", + "transfer", + "btc" + ], + "amount": 2 + } + ], + "error": false + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutPass.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutPass.tla new file mode 100644 index 0000000000..5dc5a994ae --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestOnTimeoutPass.tla @@ -0,0 +1,310 @@ +------------------------- 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 |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 2 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-1", 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 |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-1", 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 |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"] + +(* Transition 10 to State4 *) + +State4 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 2 +/\ count = 2 +/\ error = FALSE +/\ handler = "OnTimeoutPacket" +/\ 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 |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-1", 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 |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]] + >> + :> 1, + error |-> FALSE, + handler |-> "OnTimeoutPacket", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-1", port |-> "transfer"]], + receiver |-> "", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + 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"] = "OnTimeoutPacket" + /\ history[s$2]["error"] = FALSE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:07:37 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferFail.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferFail.json new file mode 100644 index 0000000000..01d589d867 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferFail.json @@ -0,0 +1,58 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "", + "receiver": "", + "amount": 1, + "denom": [ + "", + "", + "", + "", + "" + ] + } + }, + "handler": "SendTransfer", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "error": true + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferFail.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferFail.tla new file mode 100644 index 0000000000..dc3a1c008b --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferFail.tla @@ -0,0 +1,159 @@ +------------------------- 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 |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "", + sender |-> ""], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "", + sender |-> ""], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 0 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 +/\ count = 1 +/\ error = TRUE +/\ handler = "SendTransfer" +/\ 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 |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "", + sender |-> ""], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 1 + :> [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 |-> TRUE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "", + 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"] = "SendTransfer" + /\ history[s$2]["error"] = TRUE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 11:00:34 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferPass.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferPass.json new file mode 100644 index 0000000000..452d2b3aa9 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferPass.json @@ -0,0 +1,174 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a3", + "receiver": "a2", + "amount": 1, + "denom": [ + "", + "", + "cosmos-hub", + "cosmos-hub", + "eth" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-0", + "cosmos-hub", + "cosmos-hub", + "eth" + ], + "amount": 1 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-1", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a2", + "receiver": "a1", + "amount": 1, + "denom": [ + "transfer", + "channel-0", + "cosmos-hub", + "cosmos-hub", + "eth" + ] + } + }, + "handler": "SendTransfer", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-0", + "cosmos-hub", + "cosmos-hub", + "eth" + ], + "amount": 1 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a2" + ], + "denom": [ + "transfer", + "channel-0", + "cosmos-hub", + "cosmos-hub", + "eth" + ], + "amount": 0 + }, + { + "address": [ + "transfer", + "channel-1", + "" + ], + "denom": [ + "transfer", + "channel-0", + "cosmos-hub", + "cosmos-hub", + "eth" + ], + "amount": 1 + } + ], + "error": false + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferPass.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferPass.tla new file mode 100644 index 0000000000..23c45c6773 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestSendTransferPass.tla @@ -0,0 +1,323 @@ +------------------------- 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 |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 2 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-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 |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + 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 |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-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 |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a2"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"] + +(* Transition 1 to State4 *) + +State4 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]] + >> + :> 0 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]] + >> + :> 1 +/\ count = 2 +/\ error = FALSE +/\ handler = "SendTransfer" +/\ 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 |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + 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 |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-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 |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a2", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]] + >> + :> 0 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> + "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]] + >> + :> 1, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a2", port |-> ""], [denom |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]] + >> + :> 1, + error |-> FALSE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "eth", + prefix0 |-> [channel |-> "cosmos-hub", port |-> "cosmos-hub"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a2"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + 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"] = "SendTransfer" + /\ history[s$2]["error"] = FALSE + /\ history[s$2]["packet"]["data"]["amount"] > 0)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 10:58:54 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestUnescrowTokens.json b/x/ibc/applications/transfer/keeper/model_based_tests/TestUnescrowTokens.json new file mode 100644 index 0000000000..9855220704 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestUnescrowTokens.json @@ -0,0 +1,305 @@ +[ + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a1", + "receiver": "a3", + "amount": 5, + "denom": [ + "", + "", + "", + "", + "atom" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 5 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-1", + "sourcePort": "transfer", + "destChannel": "channel-0", + "destPort": "transfer", + "data": { + "sender": "a3", + "receiver": "a1", + "amount": 3, + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ] + } + }, + "handler": "SendTransfer", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 5 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 2 + }, + { + "address": [ + "transfer", + "channel-1", + "" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 3 + } + ], + "error": false + }, + { + "packet": { + "sourceChannel": "channel-0", + "sourcePort": "transfer", + "destChannel": "channel-1", + "destPort": "transfer", + "data": { + "sender": "a1", + "receiver": "a1", + "amount": 1, + "denom": [ + "transfer", + "channel-0", + "transfer", + "channel-0", + "atom" + ] + } + }, + "handler": "OnRecvPacket", + "bankBefore": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 2 + }, + { + "address": [ + "transfer", + "channel-1", + "" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 3 + } + ], + "bankAfter": [ + { + "address": [ + "", + "", + "" + ], + "denom": [ + "", + "", + "", + "", + "" + ], + "amount": 0 + }, + { + "address": [ + "", + "", + "a1" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 1 + }, + { + "address": [ + "", + "", + "a3" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 2 + }, + { + "address": [ + "transfer", + "channel-1", + "" + ], + "denom": [ + "", + "", + "transfer", + "channel-0", + "atom" + ], + "amount": 2 + } + ], + "error": false + } +] \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/model_based_tests/TestUnescrowTokens.tla b/x/ibc/applications/transfer/keeper/model_based_tests/TestUnescrowTokens.tla new file mode 100644 index 0000000000..e99081c123 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/model_based_tests/TestUnescrowTokens.tla @@ -0,0 +1,563 @@ +------------------------- 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 |-> 5, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 5, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 3 to State3 *) + +State3 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 5 +/\ 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 |-> 5, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a1"], + 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 |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 5, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 5, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"] + +(* Transition 1 to State4 *) + +State4 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3 +/\ count = 2 +/\ error = FALSE +/\ handler = "SendTransfer" +/\ 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 |-> 5, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a1"], + 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 |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 5, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 5, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> + "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 5, + error |-> FALSE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* Transition 4 to State5 *) + +State5 == +/\ bank = << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 1 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 +/\ count = 3 +/\ 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 |-> 5, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a1"], + 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 |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 5, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 5, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a3", + sender |-> "a1"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] + @@ 2 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> + "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 5, + error |-> FALSE, + handler |-> "SendTransfer", + packet |-> + [data |-> + [amount |-> 3, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]], + receiver |-> "a1", + sender |-> "a3"], + destChannel |-> "channel-0", + destPort |-> "transfer", + sourceChannel |-> "channel-1", + sourcePort |-> "transfer"]] + @@ 3 + :> [bankAfter |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a1", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 1 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> + "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2, + bankBefore |-> + << + [channel |-> "", id |-> "", port |-> ""], [denom |-> "", + prefix0 |-> [channel |-> "", port |-> ""], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 0 + @@ << + [channel |-> "", id |-> "a3", port |-> ""], [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 2 + @@ << + [channel |-> "channel-1", id |-> "", port |-> "transfer"], [denom |-> + "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "", port |-> ""]] + >> + :> 3, + error |-> FALSE, + handler |-> "OnRecvPacket", + packet |-> + [data |-> + [amount |-> 1, + denomTrace |-> + [denom |-> "atom", + prefix0 |-> [channel |-> "channel-0", port |-> "transfer"], + prefix1 |-> [channel |-> "channel-0", port |-> "transfer"]], + receiver |-> "a1", + sender |-> "a1"], + destChannel |-> "channel-1", + destPort |-> "transfer", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"]] +/\ p = [data |-> + [amount |-> 0, + denomTrace |-> + [denom |-> "btc", + prefix0 |-> [channel |-> "transfer", port |-> "bitcoin-hub"], + prefix1 |-> [channel |-> "channel-0", port |-> "channel-1"]], + receiver |-> "a1", + sender |-> ""], + destChannel |-> "ethereum-hub", + destPort |-> "cosmos-hub", + sourceChannel |-> "channel-0", + sourcePort |-> "transfer"] + +(* The following formula holds true in the last state and violates the invariant *) + +InvariantViolation == + history[1]["handler"] = "OnRecvPacket" + /\ BMC!Skolem((\E s$2 \in DOMAIN history: + ((IF history[s$2]["packet"]["data"]["denomTrace"]["prefix0"] + = [port |-> "", channel |-> ""] + THEN [port |-> "", channel |-> ""] + ELSE IF history[s$2]["packet"]["data"]["denomTrace"]["prefix1"] + = [port |-> "", channel |-> ""] + THEN history[s$2]["packet"]["data"]["denomTrace"]["prefix0"] + ELSE history[s$2]["packet"]["data"]["denomTrace"]["prefix1"])[ + "port" + ] + = history[s$2]["packet"]["sourcePort"] + /\ (IF history[s$2]["packet"]["data"]["denomTrace"]["prefix0"] + = [port |-> "", channel |-> ""] + THEN [port |-> "", channel |-> ""] + ELSE IF history[s$2]["packet"]["data"]["denomTrace"]["prefix1"] + = [port |-> "", channel |-> ""] + THEN history[s$2]["packet"]["data"]["denomTrace"]["prefix0"] + ELSE history[s$2]["packet"]["data"]["denomTrace"]["prefix1"])[ + "channel" + ] + = history[s$2]["packet"]["sourceChannel"]) + /\ history[s$2]["handler"] = "OnRecvPacket" + /\ history[s$2]["error"] = FALSE)) + +================================================================================ +\* Created by Apalache on Thu Dec 10 13:38:11 CET 2020 +\* https://github.com/informalsystems/apalache diff --git a/x/ibc/applications/transfer/keeper/relay_model/account.tla b/x/ibc/applications/transfer/keeper/relay_model/account.tla new file mode 100644 index 0000000000..84d743f6da --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/account.tla @@ -0,0 +1,36 @@ +-------------------------- MODULE account ---------------------------- + +(** + The accounts interface; please ignore the definition bodies. +*) + +EXTENDS identifiers + +CONSTANT + AccountIds + +\* a non-account +NullAccount == "NullAccount" + +\* All accounts +Accounts == { NullAccount } + +\* Make an escrow account for the given port and channel +MakeEscrowAccount(port, channel) == NullAccount + +\* Make an account from the accound id +MakeAccount(accountId) == NullAccount + +\* Type constraints for accounts +AccountTypeOK == + /\ NullAccount \in Accounts + /\ \A p \in Identifiers, c \in Identifiers: + MakeEscrowAccount(p, c) \in Accounts + /\ \A a \in Identifiers: + MakeAccount(a) \in Accounts + +============================================================================= +\* Modification History +\* Last modified Thu Nov 19 18:21:10 CET 2020 by c +\* Last modified Thu Nov 05 14:44:18 CET 2020 by andrey +\* Created Thu Nov 05 13:22:40 CET 2020 by andrey diff --git a/x/ibc/applications/transfer/keeper/relay_model/account_record.tla b/x/ibc/applications/transfer/keeper/relay_model/account_record.tla new file mode 100644 index 0000000000..c7eed27af1 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/account_record.tla @@ -0,0 +1,46 @@ +-------------------------- MODULE account_record ---------------------------- + +(** + The most basic implementation of accounts, which is a union of normal and escrow accounts + Represented via records. +*) + +EXTENDS identifiers + +CONSTANT + AccountIds + +NullAccount == [ + port |-> NullId, + channel |-> NullId, + id |-> NullId +] + +Accounts == [ + port: Identifiers, + channel: Identifiers, + id: AccountIds +] + +MakeEscrowAccount(port, channel) == [ + port |-> port, + channel |-> channel, + id |-> NullId +] + +MakeAccount(accountId) == [ + port |-> NullId, + channel |-> NullId, + id |-> accountId +] + + +ACCOUNT == INSTANCE account +AccountTypeOK == ACCOUNT!AccountTypeOK + + +============================================================================= +\* Modification History +\* Last modified Thu Nov 19 18:21:46 CET 2020 by c +\* Last modified Thu Nov 05 14:49:10 CET 2020 by andrey +\* Created Thu Nov 05 13:22:40 CET 2020 by andrey diff --git a/x/ibc/applications/transfer/keeper/relay_model/apalache-to-relay-test.json b/x/ibc/applications/transfer/keeper/relay_model/apalache-to-relay-test.json new file mode 100644 index 0000000000..c8d70a3332 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/apalache-to-relay-test.json @@ -0,0 +1,100 @@ +{ + "description": "Transforms an Apalache counterexample into the test for ICS20 Token Transfer OnRecvPacket", + "usage": "jsonatr --use apalache-to-recv-test.json --in counterexample.json --out recv-test.json", + "input": [ + { + "name": "history", + "description": "extract history from the last state of Apalache CE", + "kind": "INLINE", + "source": "$.declarations[-2].body.and..[?(@.eq == 'history')].arg.atat..arg.record" + }, + { + "name": "bankRecordToBalance", + "description": "", + "kind": "INLINE", + "source": { + "address": [ + "$.colonGreater.tuple[0]..[?(@.key.str == 'port')].value.str | unwrap", + "$.colonGreater.tuple[0]..[?(@.key.str == 'channel')].value.str | unwrap", + "$.colonGreater.tuple[0]..[?(@.key.str == 'id')].value.str | unwrap" + ], + "denom": [ + "$.colonGreater.tuple[1]..[?(@.key.str == 'port')].value.str | unwrap", + "$.colonGreater.tuple[1]..[?(@.key.str == 'channel')].value.str | unwrap", + "$.colonGreater.tuple[1]..[?(@.key.str == 'denom')].value.str | unwrap" + ], + "amount": "$.arg | unwrap" + } + }, + { + "name": "bankBefore", + "description": "extract bankBefore from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'bankBefore')].value.atat | unwrap | map(bankRecordToBalance)" + }, + { + "name": "bankAfter", + "description": "extract bankAfter from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'bankAfter')].value.atat | unwrap | map(bankRecordToBalance)" + }, + { + "name": "packet", + "description": "extract packet from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'packet')].value.record" + }, + { + "name": "packetData", + "description": "extract bankAfter from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'data')].value.record" + }, + { + "name": "packetDataDenom", + "description": "extract bankAfter from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'data')].value.record.[?(@.key.str == 'denomTrace')].value.record" + }, + { + "name": "packetRecord", + "description": "decompose packet", + "kind": "INLINE", + "source": { + "sourceChannel" : "$.[?(@.key.str == 'sourceChannel')].value.str | unwrap", + "sourcePort" : "$.[?(@.key.str == 'sourcePort')].value.str | unwrap", + "destChannel" : "$.[?(@.key.str == 'destChannel')].value.str | unwrap", + "destPort" : "$.[?(@.key.str == 'destPort')].value.str | unwrap", + "data": { + "sender": "$packetData.[?(@.key.str == 'sender')].value.str | unwrap", + "receiver": "$packetData.[?(@.key.str == 'receiver')].value.str | unwrap", + "amount": "$packetData.[?(@.key.str == 'amount')].value | unwrap", + "denom": [ + "$packetDataDenom.[?(@.key.str == 'port')].value.str | unwrap", + "$packetDataDenom.[?(@.key.str == 'channel')].value.str | unwrap", + "$packetDataDenom.[?(@.key.str == 'denom')].value.str | unwrap" + ] + } + } + }, + { + "name": "handler", + "description": "extract handler from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'handler')].value.str" + }, + { + "name": "historyState", + "description": "decompose single history state", + "kind": "INLINE", + "source": { + "packet": "$packet | unwrap | packetRecord", + "handler": "$handler | unwrap", + "bankBefore": "$bankBefore", + "bankAfter": "$bankAfter", + "error": "$..[?(@.key.str == 'error')].value | unwrap" + } + } + ], + "output": "$history[1:] | map(historyState)" +} \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/relay_model/apalache-to-relay-test2.json b/x/ibc/applications/transfer/keeper/relay_model/apalache-to-relay-test2.json new file mode 100644 index 0000000000..a2c821c4db --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/apalache-to-relay-test2.json @@ -0,0 +1,104 @@ +{ + "description": "Transforms an Apalache counterexample into the test for ICS20 Token Transfer OnRecvPacket", + "usage": "jsonatr --use apalache-to-recv-test.json --in counterexample.json --out recv-test.json", + "input": [ + { + "name": "history", + "description": "extract history from the last state of Apalache CE", + "kind": "INLINE", + "source": "$.declarations[-2].body.and..[?(@.eq == 'history')].arg.atat..arg.record" + }, + { + "name": "bankRecordToBalance", + "description": "", + "kind": "INLINE", + "source": { + "address": [ + "$.colonGreater.tuple[0]..[?(@.key.str == 'port')].value.str | unwrap", + "$.colonGreater.tuple[0]..[?(@.key.str == 'channel')].value.str | unwrap", + "$.colonGreater.tuple[0]..[?(@.key.str == 'id')].value.str | unwrap" + ], + "denom": [ + "$.colonGreater.tuple[1]..[?(@.key.str == 'prefix1')].value..[?(@.key.str == 'port')].value.str | unwrap", + "$.colonGreater.tuple[1]..[?(@.key.str == 'prefix1')].value..[?(@.key.str == 'channel')].value.str | unwrap", + "$.colonGreater.tuple[1]..[?(@.key.str == 'prefix0')].value..[?(@.key.str == 'port')].value.str | unwrap", + "$.colonGreater.tuple[1]..[?(@.key.str == 'prefix0')].value..[?(@.key.str == 'channel')].value.str | unwrap", + "$.colonGreater.tuple[1]..[?(@.key.str == 'denom')].value.str | unwrap" + ], + "amount": "$.arg | unwrap" + } + }, + { + "name": "bankBefore", + "description": "extract bankBefore from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'bankBefore')].value.atat | unwrap | map(bankRecordToBalance)" + }, + { + "name": "bankAfter", + "description": "extract bankAfter from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'bankAfter')].value.atat | unwrap | map(bankRecordToBalance)" + }, + { + "name": "packet", + "description": "extract packet from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'packet')].value.record" + }, + { + "name": "packetData", + "description": "extract bankAfter from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'data')].value.record" + }, + { + "name": "packetDataDenom", + "description": "extract bankAfter from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'data')].value.record.[?(@.key.str == 'denomTrace')].value.record" + }, + { + "name": "packetRecord", + "description": "decompose packet", + "kind": "INLINE", + "source": { + "sourceChannel" : "$.[?(@.key.str == 'sourceChannel')].value.str | unwrap", + "sourcePort" : "$.[?(@.key.str == 'sourcePort')].value.str | unwrap", + "destChannel" : "$.[?(@.key.str == 'destChannel')].value.str | unwrap", + "destPort" : "$.[?(@.key.str == 'destPort')].value.str | unwrap", + "data": { + "sender": "$packetData.[?(@.key.str == 'sender')].value.str | unwrap", + "receiver": "$packetData.[?(@.key.str == 'receiver')].value.str | unwrap", + "amount": "$packetData.[?(@.key.str == 'amount')].value | unwrap", + "denom": [ + "$packetDataDenom.[?(@.key.str == 'prefix1')].value..[?(@.key.str == 'port')].value.str | unwrap", + "$packetDataDenom.[?(@.key.str == 'prefix1')].value..[?(@.key.str == 'channel')].value.str | unwrap", + "$packetDataDenom.[?(@.key.str == 'prefix0')].value..[?(@.key.str == 'port')].value.str | unwrap", + "$packetDataDenom.[?(@.key.str == 'prefix0')].value..[?(@.key.str == 'channel')].value.str | unwrap", + "$packetDataDenom.[?(@.key.str == 'denom')].value.str | unwrap" + ] + } + } + }, + { + "name": "handler", + "description": "extract handler from the history state", + "kind": "INLINE", + "source": "$..[?(@.key.str == 'handler')].value.str" + }, + { + "name": "historyState", + "description": "decompose single history state", + "kind": "INLINE", + "source": { + "packet": "$packet | unwrap | packetRecord", + "handler": "$handler | unwrap", + "bankBefore": "$bankBefore", + "bankAfter": "$bankAfter", + "error": "$..[?(@.key.str == 'error')].value | unwrap" + } + } + ], + "output": "$history[1:] | map(historyState)" +} \ No newline at end of file diff --git a/x/ibc/applications/transfer/keeper/relay_model/denom.tla b/x/ibc/applications/transfer/keeper/relay_model/denom.tla new file mode 100644 index 0000000000..f729e7e14f --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/denom.tla @@ -0,0 +1,50 @@ +-------------------------- MODULE denom ---------------------------- + +(** + The denomination traces interface; please ignore the definition bodies. +*) + +EXTENDS identifiers + +CONSTANT + Denoms + +\* A non-account +NullDenomTrace == "NullDenomTrace" + +\* All denomination traces +DenomTraces == {NullDenomTrace} + +\* Make a new denomination trace from the port/channel prefix and the basic denom +MakeDenomTrace(port, channel, denom) == NullDenomTrace + +\* Get the denomination trace port +GetPort(trace) == NullId + +\* Get the denomination trace port +GetChannel(trace) == NullId + +\* Get the denomination trace basic denomination +GetDenom(trace) == NullDenomTrace + +\* Is this denomination trace a native denomination, or is it a prefixed trace +\* Note that those cases are exclusive, but not exhaustive +IsNativeDenomTrace(trace) == GetPort(trace) = NullId /\ GetChannel(trace) = NullId +IsPrefixedDenomTrace(trace) == GetPort(trace) /= NullId /\ GetChannel(trace) /= NullId + +DenomTypeOK == + /\ NullDenomTrace \in DenomTraces + /\ \A p \in Identifiers, c \in Identifiers, d \in Denoms: + MakeDenomTrace(p, c, d) \in DenomTraces + /\ \A t \in DenomTraces: + /\ GetPort(t) \in Identifiers + /\ GetChannel(t) \in Identifiers + /\ GetDenom(t) \in DenomTraces + + + + +============================================================================= +\* Modification History +\* Last modified Thu Nov 05 15:49:23 CET 2020 by andrey +\* Created Thu Nov 05 13:22:40 CET 2020 by andrey diff --git a/x/ibc/applications/transfer/keeper/relay_model/denom_record.tla b/x/ibc/applications/transfer/keeper/relay_model/denom_record.tla new file mode 100644 index 0000000000..2eb0d06f1d --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/denom_record.tla @@ -0,0 +1,53 @@ +-------------------------- MODULE denom_record ---------------------------- + +(** + The most basic implementation of denomination traces that allows only one-step sequences + Represented via records +*) + +EXTENDS identifiers + +CONSTANT + Denoms + +MaxDenomLength == 3 + +DenomTraces == [ + port: Identifiers, + channel: Identifiers, + denom: Denoms +] + +NullDenomTrace == [ + port |-> NullId, + channel |-> NullId, + denom |-> NullId +] + +GetPort(trace) == trace.port +GetChannel(trace) == trace.channel +GetDenom(trace) == trace.denom + +IsNativeDenomTrace(trace) == GetPort(trace) = NullId /\ GetChannel(trace) = NullId /\ GetDenom(trace) /= NullId +IsPrefixedDenomTrace(trace) == GetPort(trace) /= NullId /\ GetChannel(trace) /= NullId /\ GetDenom(trace) /= NullId + +ExtendDenomTrace(port, channel, trace) == + IF GetPort(trace) = NullId /\ GetChannel(trace) = NullId + THEN + [ + port |-> port, + channel |-> channel, + denom |-> trace.denom + ] + ELSE + NullDenomTrace + + +DENOM == INSTANCE denom +DenomTypeOK == DENOM!DenomTypeOK + + +============================================================================= +\* Modification History +\* Last modified Thu Nov 05 16:41:47 CET 2020 by andrey +\* Created Thu Nov 05 13:22:40 CET 2020 by andrey diff --git a/x/ibc/applications/transfer/keeper/relay_model/denom_record2.tla b/x/ibc/applications/transfer/keeper/relay_model/denom_record2.tla new file mode 100644 index 0000000000..a49d6c98de --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/denom_record2.tla @@ -0,0 +1,114 @@ +-------------------------- MODULE denom_record2 ---------------------------- + +(** + The implementation of denomination traces that allows one- or two-step sequences + Represented via records +*) + +EXTENDS identifiers + +CONSTANT + Denoms + +MaxDenomLength == 5 + +DenomPrefixes == [ + port: Identifiers, + channel: Identifiers +] + +NullDenomPrefix == [ + port |-> NullId, + channel |-> NullId +] + +MakeDenomPrefix(port, channel) == [ + port |-> port, + channel |-> channel +] + +IsValidDenomPrefix(prefix) == + /\ prefix.port /= NullId + /\ prefix.channel /= NullId + +DenomTraces == [ + prefix1: DenomPrefixes, \* the most recent prefix + prefix0: DenomPrefixes, \* the deepest prefix + denom: Denoms +] + +NullDenomTrace == [ + prefix1 |-> NullDenomPrefix, + prefix0 |-> NullDenomPrefix, + denom |-> NullId +] + + +TraceLen(trace) == + IF trace.prefix0 = NullDenomPrefix + THEN 1 + ELSE IF trace.prefix1 = NullDenomPrefix + THEN 3 + ELSE 5 + +LatestPrefix(trace) == + IF trace.prefix0 = NullDenomPrefix + THEN NullDenomPrefix + ELSE IF trace.prefix1 = NullDenomPrefix + THEN trace.prefix0 + ELSE trace.prefix1 + + +ExtendDenomTrace(port, channel, trace) == + IF trace.prefix0 = NullDenomPrefix + THEN [ + prefix1 |-> NullDenomPrefix, + prefix0 |-> MakeDenomPrefix(port, channel), + denom |-> trace.denom + ] + ELSE IF trace.prefix1 = NullDenomPrefix + THEN [ + prefix1 |-> MakeDenomPrefix(port, channel), + prefix0 |-> trace.prefix0, + denom |-> trace.denom + ] + ELSE NullDenomTrace \* can extend only for two steps + +ReduceDenomTrace(trace) == + IF trace.prefix1 /= NullDenomPrefix + THEN [ + prefix1 |-> NullDenomPrefix, + prefix0 |-> trace.prefix0, + denom |-> trace.denom + ] + ELSE IF trace.prefix0 /= NullDenomPrefix + THEN [ + prefix1 |-> NullDenomPrefix, + prefix0 |-> NullDenomPrefix, + denom |-> trace.denom + ] + ELSE NullDenomTrace \* cannot reduce further + +GetPort(trace) == LatestPrefix(trace).port +GetChannel(trace) == LatestPrefix(trace).channel +GetDenom(trace) == trace.denom + +IsValidDenomTrace(trace) == + /\ GetDenom(trace) /= NullId + /\ IF IsValidDenomPrefix(trace.prefix1) + THEN IsValidDenomPrefix(trace.prefix0) + ELSE + /\ trace.prefix1 = NullDenomPrefix + /\ (IsValidDenomPrefix(trace.prefix0) \/ trace.prefix0 = NullDenomPrefix) + +IsNativeDenomTrace(trace) == LatestPrefix(trace) = NullDenomPrefix /\ GetDenom(trace) /= NullId +IsPrefixedDenomTrace(trace) == LatestPrefix(trace) /= NullDenomPrefix /\ GetDenom(trace) /= NullId + +DENOM == INSTANCE denom +DenomTypeOK == DENOM!DenomTypeOK + + +============================================================================= +\* Modification History +\* Last modified Fri Dec 04 10:38:10 CET 2020 by andrey +\* Created Fri Dec 04 10:22:10 CET 2020 by andrey diff --git a/x/ibc/applications/transfer/keeper/relay_model/denom_sequence.tla b/x/ibc/applications/transfer/keeper/relay_model/denom_sequence.tla new file mode 100644 index 0000000000..29b5f4edf2 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/denom_sequence.tla @@ -0,0 +1,47 @@ +-------------------------- MODULE denom_sequence ---------------------------- + +(** + The implementation of denomination traces via sequences +*) + +EXTENDS Integers, Sequences, identifiers + +CONSTANT + Denoms, + MaxDenomLength + + +a <: b == a +AsAddress(seq) == seq <: Seq(STRING) + +UNROLL_DEFAULT_GenSeq == { AsAddress(<< >>) } +UNROLL_TIMES_GenSeq == 5 + +\* This produces denomination sequences up to the given bound +RECURSIVE GenSeq(_) +GenSeq(n) == + IF n = 0 THEN { AsAddress(<< >>) } + ELSE LET Shorter == GenSeq(n-1) IN + { Append(s,x): x \in Identifiers, s \in Shorter } \union Shorter + +DenomTraces == GenSeq(MaxDenomLength) + +ExtendDenomTrace(port, channel, denom) == AsAddress(<>) \o denom + +GetPort(trace) == trace[1] +GetChannel(trace) == trace[2] +GetDenom(trace) == SubSeq(trace, 3, Len(trace)) + +NullDenomTrace == AsAddress(<< >>) + +IsNativeDenomTrace(trace) == GetPort(trace) = NullId /\ GetChannel(trace) = NullId /\ GetDenom(trace) /= NullDenomTrace +IsPrefixedDenomTrace(trace) == GetPort(trace) /= NullId /\ GetChannel(trace) /= NullId /\ GetDenom(trace) /= NullDenomTrace + +DENOM == INSTANCE denom +DenomTypeOK == DENOM!DenomTypeOK + + +============================================================================= +\* Modification History +\* Last modified Thu Nov 05 15:29:21 CET 2020 by andrey +\* Created Thu Nov 05 13:22:40 CET 2020 by andrey diff --git a/x/ibc/applications/transfer/keeper/relay_model/identifiers.tla b/x/ibc/applications/transfer/keeper/relay_model/identifiers.tla new file mode 100644 index 0000000000..089f276d8c --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/identifiers.tla @@ -0,0 +1,10 @@ +-------------------------- MODULE identifiers ---------------------------- + +CONSTANT + Identifiers, + NullId + +============================================================================= +\* Modification History +\* Last modified Thu Nov 05 13:23:12 CET 2020 by andrey +\* Created Thu Nov 05 13:22:40 CET 2020 by andrey diff --git a/x/ibc/applications/transfer/keeper/relay_model/relay.tla b/x/ibc/applications/transfer/keeper/relay_model/relay.tla new file mode 100644 index 0000000000..029df3d7c7 --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/relay.tla @@ -0,0 +1,278 @@ +-------------------------- MODULE relay ---------------------------- +(** + * A primitive model for account arithmetics and token movement + * of the Cosmos SDK ICS20 Token Transfer + * We completely abstract away many details, + * and want to focus on a minimal spec useful for testing + * + * We also try to make the model modular in that it uses + * denomination traces and accounts via abstract interfaces, + * outlined in denom.tla and account.tla + *) + +EXTENDS Integers, FiniteSets, Sequences, identifiers, denom_record2, account_record + +CONSTANT + MaxAmount + +VARIABLE + error, + bank, + p, \* we want to start with generating single packets, + handler, + history, + count + +Amounts == 0..MaxAmount + +GetSourceEscrowAccount(packet) == MakeEscrowAccount(packet.sourcePort, packet.sourceChannel) +GetDestEscrowAccount(packet) == MakeEscrowAccount(packet.destPort, packet.destChannel) + +FungibleTokenPacketData == [ + sender: AccountIds, + receiver: AccountIds, + denomTrace: DenomTraces, + amount: Amounts +] + +Packets == [ + \* We abstract those packet fields away + \* sequence: uint64 + \* timeoutHeight: Height + \* timeoutTimestamp: uint64 + sourcePort: Identifiers, + sourceChannel: Identifiers, + destPort: Identifiers, + destChannel: Identifiers, + data: FungibleTokenPacketData +] + + +IsSource(packet) == + /\ GetPort(packet.data.denomTrace) = packet.sourcePort + /\ GetChannel(packet.data.denomTrace) = packet.sourceChannel + +\* This function models the port and channel checks that happen when the packet is sent +IsValidSendChannel(packet) == + /\ packet.sourcePort = "transfer" + /\ (packet.sourceChannel = "channel-0" \/ packet.sourceChannel = "channel-1") + /\ packet.destPort = "transfer" + /\ packet.destChannel = "channel-0" + +\* This function models the port and channel checks that happen when relay gets the packet +IsValidRecvChannel(packet) == + /\ packet.sourcePort = "transfer" + /\ packet.sourceChannel = "channel-0" + /\ packet.destPort = "transfer" + /\ (packet.destChannel = "channel-0" \/ packet.destChannel = "channel-1") + + +WellFormedPacket(packet) == + /\ packet.sourcePort /= NullId + /\ packet.sourceChannel /= NullId + /\ packet.destPort /= NullId + /\ packet.destChannel /= NullId + +BankWithAccount(abank, account, denom) == + IF <> \in DOMAIN abank + THEN abank + ELSE [x \in DOMAIN bank \union { <> } + |-> IF x = <> + THEN 0 + ELSE bank[x] ] + +IsKnownDenomTrace(trace) == + \E account \in Accounts : + <> \in DOMAIN bank + + +SendTransferPre(packet, pbank) == + LET data == packet.data + trace == data.denomTrace + sender == data.sender + amount == data.amount + escrow == GetSourceEscrowAccount(packet) + IN + /\ WellFormedPacket(packet) + /\ IsValidSendChannel(packet) + /\ IsNativeDenomTrace(trace) \/ (IsValidDenomTrace(trace) /\ IsKnownDenomTrace(trace)) + /\ data.sender /= NullId + /\ <> \in DOMAIN pbank + /\ \/ amount = 0 \* SendTrasfer actually allows for 0 amount + \/ <> \in DOMAIN pbank /\ bank[MakeAccount(sender), trace] >= amount + +SendTransferNext(packet) == + LET data == packet.data IN + LET denom == GetDenom(data.denomTrace) IN + LET amount == data.amount IN + LET sender == data.sender IN + LET escrow == GetSourceEscrowAccount(packet) IN + LET bankwithescrow == BankWithAccount(bank, escrow, data.denomTrace) IN + IF SendTransferPre(packet,bankwithescrow) + THEN + /\ error' = FALSE + \*/\ IBCsend(chain, packet) + /\ IF ~IsSource(packet) + \* This is how the check is encoded in ICS20 and the implementation. + \* The meaning is "IF denom = AsAddress(NativeDenom)" because of the following argument: + \* observe that due to the disjunction in SendTransferPre(packet), we have + \* ~IsSource(packet) /\ SendTransferPre(packet) => denom = AsAddress(NativeDenom) + THEN + \* tokens are from this chain + \* transfer tokens from sender into escrow account + bank' = [bankwithescrow EXCEPT ![MakeAccount(sender), data.denomTrace] = @ - amount, + ![escrow, data.denomTrace] = @ + amount] + ELSE + \* tokens are from other chain. We forward them. + \* burn sender's money + bank' = [bankwithescrow EXCEPT ![MakeAccount(sender), data.denomTrace] = @ - amount] + ELSE + /\ error' = TRUE + /\ UNCHANGED bank + + +OnRecvPacketPre(packet) == + LET data == packet.data + trace == data.denomTrace + denom == GetDenom(trace) + amount == data.amount + IN + /\ WellFormedPacket(packet) + /\ IsValidRecvChannel(packet) + /\ IsValidDenomTrace(trace) + /\ amount > 0 + \* if there is no receiver account, it is created by the bank + /\ data.receiver /= NullId + /\ IsSource(packet) => + LET escrow == GetDestEscrowAccount(packet) IN + LET denomTrace == ReduceDenomTrace(trace) IN + /\ <> \in DOMAIN bank + /\ bank[escrow, denomTrace] >= amount + + +OnRecvPacketNext(packet) == + LET data == packet.data IN + LET trace == data.denomTrace IN + LET denom == GetDenom(trace) IN + LET amount == data.amount IN + LET receiver == data.receiver IN + /\ IF OnRecvPacketPre(packet) + THEN + \* This condition is necessary so that denomination traces do not exceed the maximum length + /\ (IsSource(packet) \/ TraceLen(trace) < MaxDenomLength) + /\ error' = FALSE + /\ IF IsSource(packet) + THEN + \* transfer from the escrow account to the receiver account + LET denomTrace == ReduceDenomTrace(trace) IN + LET escrow == GetDestEscrowAccount(packet) IN + LET bankwithreceiver == BankWithAccount(bank, MakeAccount(receiver), denomTrace) IN + bank' = [bankwithreceiver + EXCEPT ![MakeAccount(receiver), denomTrace] = @ + amount, + ![escrow, denomTrace] = @ - amount] + ELSE + \* create new tokens with new denomination and transfer it to the receiver account + LET denomTrace == ExtendDenomTrace(packet.destPort, packet.destChannel, trace) IN + LET bankwithreceiver == + BankWithAccount(bank, MakeAccount(receiver), denomTrace) IN + bank' = [bankwithreceiver + EXCEPT ![MakeAccount(receiver), denomTrace] = @ + amount] + ELSE + /\ error' = TRUE + /\ UNCHANGED bank + + +OnTimeoutPacketPre(packet) == + LET data == packet.data + trace == data.denomTrace + denom == GetDenom(trace) + amount == data.amount + IN + /\ WellFormedPacket(packet) + /\ IsValidSendChannel(packet) + /\ IsValidDenomTrace(trace) + /\ data.sender /= NullId + /\ ~IsSource(packet) => + LET escrow == GetSourceEscrowAccount(packet) + IN /\ <> \in DOMAIN bank + /\ bank[escrow, trace] >= amount + + +OnTimeoutPacketNext(packet) == + LET data == packet.data IN + LET trace == data.denomTrace IN + LET denom == GetDenom(data.denomTrace) IN + LET amount == data.amount IN + LET sender == data.sender IN + LET bankwithsender == BankWithAccount(bank, MakeAccount(sender), trace) IN + IF OnTimeoutPacketPre(packet) + THEN + /\ error' = FALSE + /\ IF ~IsSource(packet) + THEN + \* transfer from the escrow acount to the sender account + \* LET denomsuffix == SubSeq(denom, 3, Len(denom)) IN + LET escrow == GetSourceEscrowAccount(packet) IN + bank' = [bankwithsender + EXCEPT ![MakeAccount(sender), trace] = @ + amount, + ![escrow, trace] = @ - amount] + ELSE + \* mint back the money + bank' = [bankwithsender EXCEPT ![MakeAccount(sender), trace] = @ + amount] + + ELSE + /\ error' = TRUE + /\ UNCHANGED bank + + +OnAcknowledgementPacketResultNext(packet) == + IF WellFormedPacket(packet) + THEN + /\ error' = FALSE + /\ UNCHANGED bank + ELSE + /\ error' = TRUE + /\ UNCHANGED bank + + +OnAcknowledgementPacketErrorNext(packet) == + OnTimeoutPacketNext(packet) + +Init == + /\ p \in Packets + /\ bank = [ x \in {<>} |-> 0 ] + /\ count = 0 + /\ history = [ + n \in {0} |-> [ + error |-> FALSE, + packet |-> p, + handler |-> "", + bankBefore |-> bank, + bankAfter |-> bank + ] + ] + /\ error = FALSE + /\ handler = "" + +Next == + /\ p' \in Packets + /\ count'= count + 1 + /\ + \/ (SendTransferNext(p) /\ handler' = "SendTransfer") + \/ (OnRecvPacketNext(p) /\ handler' = "OnRecvPacket") + \/ (OnTimeoutPacketNext(p) /\ handler' = "OnTimeoutPacket") + \/ (OnAcknowledgementPacketResultNext(p) /\ handler' = "OnRecvAcknowledgementResult") + \/ (OnAcknowledgementPacketErrorNext(p) /\ handler' = "OnRecvAcknowledgementError") + /\ history' = [ n \in DOMAIN history \union {count'} |-> + IF n = count' THEN + [ packet |-> p, handler |-> handler', error |-> error', bankBefore |-> bank, bankAfter |-> bank' ] + ELSE history[n] + ] + +============================================================================= +\* Modification History +\* Last modified Wed Dec 2 10:15:45 CET 2020 by andrey +\* Last modified Fri Nov 20 12:37:38 CET 2020 by c +\* Last modified Thu Nov 05 20:56:37 CET 2020 by andrey +\* Last modified Fri Oct 30 21:52:38 CET 2020 by widder +\* Created Thu Oct 29 20:45:55 CET 2020 by andrey diff --git a/x/ibc/applications/transfer/keeper/relay_model/relay_tests.tla b/x/ibc/applications/transfer/keeper/relay_model/relay_tests.tla new file mode 100644 index 0000000000..7e7577526d --- /dev/null +++ b/x/ibc/applications/transfer/keeper/relay_model/relay_tests.tla @@ -0,0 +1,96 @@ +-------------------------- MODULE relay_tests ---------------------------- + +EXTENDS Integers, FiniteSets + +Identifiers == {"", "transfer", "channel-0", "channel-1", "cosmos-hub", "ethereum-hub", "bitcoin-hub"} +NullId == "" +MaxAmount == 5 +Denoms == {"", "atom", "eth", "btc" } +AccountIds == {"", "a1", "a2", "a3" } + +VARIABLES error, bank, p, count, history, handler + +INSTANCE relay + +\************************** Tests ****************************** + +\* Generic test for handler pass +TestHandlerPass(handlerName) == + \E s \in DOMAIN history : + /\ history[s].handler = handlerName + /\ history[s].error = FALSE + /\ history[s].packet.data.amount > 0 + +\* Generic test for handler fail +TestHandlerFail(handlerName) == + \E s \in DOMAIN history : + /\ history[s].handler = handlerName + /\ history[s].error = TRUE + /\ history[s].packet.data.amount > 0 + +TestSendTransferPass == TestHandlerPass("SendTransfer") +TestSendTransferPassInv == ~TestSendTransferPass + +TestSendTransferFail == TestHandlerFail("SendTransfer") +TestSendTransferFailInv == ~TestSendTransferFail + +TestOnRecvPacketPass == TestHandlerPass("OnRecvPacket") +TestOnRecvPacketPassInv == ~TestOnRecvPacketPass + +TestOnRecvPacketFail == TestHandlerFail("OnRecvPacket") +TestOnRecvPacketFailInv == ~TestOnRecvPacketFail + +TestOnTimeoutPass == TestHandlerPass("OnTimeoutPacket") +TestOnTimeoutPassInv == ~TestOnTimeoutPass + +TestOnTimeoutFail == TestHandlerFail("OnTimeoutPacket") +TestOnTimeoutFailInv == ~TestOnTimeoutFail + +TestOnRecvAcknowledgementResultPass == TestHandlerPass("OnRecvAcknowledgementResult") +TestOnRecvAcknowledgementResultPassInv == ~TestOnRecvAcknowledgementResultPass + +TestOnRecvAcknowledgementResultFail == TestHandlerFail("OnRecvAcknowledgementResult") +TestOnRecvAcknowledgementResultFailInv == ~TestOnRecvAcknowledgementResultFail + +TestOnRecvAcknowledgementErrorPass == TestHandlerPass("OnRecvAcknowledgementError") +TestOnRecvAcknowledgementErrorPassInv == ~TestOnRecvAcknowledgementErrorPass + +TestOnRecvAcknowledgementErrorFail == TestHandlerFail("OnRecvAcknowledgementError") +TestOnRecvAcknowledgementErrorFailInv == ~TestOnRecvAcknowledgementErrorFail + +Test5Packets == + count >= 5 + +Test5PacketsInv == ~Test5Packets + +Test5Packets2Different == + /\ count >= 5 + /\ \E s1, s2 \in DOMAIN history : + history[s1].handler /= history[s2].handler + +Test5Packets2DifferentInv == ~Test5Packets2Different + +Test5PacketsAllDifferent == + /\ count >= 5 + /\ \A s1, s2 \in DOMAIN history : + s1 /= s2 => history[s1].handler /= history[s2].handler + +Test5PacketsAllDifferentInv == ~Test5PacketsAllDifferent + +Test5PacketsAllDifferentPass == + /\ Test5PacketsAllDifferent + /\ \A s \in DOMAIN history : + s > 0 => + /\ history[s].error = FALSE + /\ history[s].packet.data.amount > 0 + +Test5PacketsAllDifferentPassInv == ~Test5PacketsAllDifferentPass + +TestUnescrowTokens == + \E s \in DOMAIN history : + /\ IsSource(history[s].packet) + /\ history[s].handler = "OnRecvPacket" + /\ history[s].error = FALSE +TestUnescrowTokensInv == ~TestUnescrowTokens + +=============================================================================