diff --git a/tests/difference/core/quint_model/driver/core.go b/tests/difference/core/quint_model/driver/core.go index d01ddab4a7..f88f68405e 100644 --- a/tests/difference/core/quint_model/driver/core.go +++ b/tests/difference/core/quint_model/driver/core.go @@ -55,6 +55,8 @@ func (s *Driver) ctx(chain ChainId) sdk.Context { // returns the path from the given chain to the provider. func (s *Driver) path(chain ChainId) *simibc.RelayedPath { + if s.isProviderChain(chain) { + } return s.simibcs[chain] } @@ -244,6 +246,15 @@ func (s *Driver) getStateString() string { state.WriteString(s.getChainStateString("provider")) state.WriteString("\n") + state.WriteString("Consumers Chains:\n") + consumerChains := s.providerKeeper().GetAllConsumerChains(s.providerCtx()) + chainIds := make([]string, len(consumerChains)) + for i, consumerChain := range consumerChains { + chainIds[i] = consumerChain.ChainId + } + state.WriteString(strings.Join(chainIds, ", ")) + state.WriteString("\n\n") + for chain := range s.simibcs { state.WriteString(fmt.Sprintf("Chain %s\n", chain)) state.WriteString(s.getChainStateString(chain)) @@ -300,14 +311,84 @@ func (s *Driver) getChainStateString(chain ChainId) string { chainInfo.WriteString(validatorInfo.String()) + if !s.isProviderChain(chain) { + var outboxInfo strings.Builder + outboxInfo.WriteString("OutboxPackets:\n") + + outboxInfo.WriteString("OutgoingPackets: \n") + outgoing := s.path(chain).Outboxes.OutboxPackets[string(chain)] + for _, packet := range outgoing { + outboxInfo.WriteString(fmt.Sprintf("%v\n", packet)) + } + + outboxInfo.WriteString("IncomingPackets: \n") + incoming := s.path(chain).Outboxes.OutboxPackets[P] + for _, packet := range incoming { + outboxInfo.WriteString(fmt.Sprintf("%v\n", packet)) + } + + outboxInfo.WriteString("utboxAcks:\n") + + outboxInfo.WriteString("OutgoingAcks: \n") + outgoingAcks := s.path(chain).Outboxes.OutboxAcks[string(chain)] + for _, packet := range outgoingAcks { + outboxInfo.WriteString(fmt.Sprintf("%v\n", packet)) + } + + outboxInfo.WriteString("IncomingAcks: \n") + incomingAcks := s.path(chain).Outboxes.OutboxAcks[P] + for _, packet := range incomingAcks { + outboxInfo.WriteString(fmt.Sprintf("%v\n", packet)) + } + + chainInfo.WriteString(outboxInfo.String()) + } + return chainInfo.String() } +// endAndBeginBlock ends the current block and begins a new one. +// Before Comitting, it runs the preCommitCallback, which allows +// checks to be run before the context of the old block is discarded. +// After comitting, it processes any packets that have been sent by the chain, +// as witnessed by events, and adds them to the correct paths. +// It also updates the client header on the paths +// that involve the chain. func (s *Driver) endAndBeginBlock(chain ChainId, timeAdvancement time.Duration, preCommitCallback func()) { - s.path(chain).EndAndBeginBlock(string(chain), timeAdvancement, func() { - }) + testChain, found := s.coordinator.Chains[string(chain)] + require.True(s.t, found, "chain %s not found", chain) + + header, packets := simibc.EndBlock(testChain, preCommitCallback) + + for _, path := range s.simibcs { + if path.InvolvesChain(string(chain)) { + path.AddClientHeader(string(chain), header) + path.Outboxes.Commit(string(chain)) + } + } + + // for each packet, find the path it should be sent on + for _, p := range packets { + found := false + for _, path := range s.simibcs { + if path.PacketBelongs(p) { + path.Outboxes.AddPacket(string(chain), p) + found = true + break + } + } + if !found { + s.t.Fatal("packet does not belong to any path: ", p) + } + } + + simibc.BeginBlock(testChain, timeAdvancement) } +// newDriver creates a new Driver object. +// It creates a new coordinator, but does not start any chains. +// The caller must call setupChains to start the chains and +// fully populate the Driver. func newDriver(t *testing.T, validators []*cmttypes.Validator, valNames []string) *Driver { t.Log("Creating coordinator") coordinator := ibctesting.NewCoordinator(t, 0) // start without chains, which we add later diff --git a/tests/difference/core/quint_model/driver/mbt_test.go b/tests/difference/core/quint_model/driver/mbt_test.go index ebece67ee6..1b9c84d629 100644 --- a/tests/difference/core/quint_model/driver/mbt_test.go +++ b/tests/difference/core/quint_model/driver/mbt_test.go @@ -125,9 +125,6 @@ func TestItfTrace(t *testing.T) { // dummyValSet is a valSet with the right validators, but not yet right powers valSet, addressMap, signers := CreateValSet(t, initialValSet) - t.Log("Initial validator set is: ", valSet) - t.Log(addressMap) - t.Log(signers) // get a slice of validators in the right order nodes := make([]*cmttypes.Validator, len(valNames)) @@ -156,34 +153,39 @@ func TestItfTrace(t *testing.T) { t.Log("Initializing...") case "VotingPowerChange": node := lastAction["validator"].Value.(string) - newVotingPower := lastAction["newVotingPower"].Value.(int64) - t.Logf("Setting provider voting power of %v to %v", node, newVotingPower) - - // valIndex := getIndexOfString(node, valNames) - - // // set the voting power of the validator - - // // get the previous voting power of that validator - // prevVotingPower := driver.validato - + changeAmount := lastAction["changeAmount"].Value.(int64) + t.Logf("Setting provider voting power of %v to %v", node, changeAmount) + + valIndex := getIndexOfString(node, valNames) + + if changeAmount > 0 { + // delegate to the validator + driver.delegate(int64(valIndex), changeAmount) + } else { + // undelegate from the validator + driver.undelegate(int64(valIndex), -changeAmount) + } case "EndAndBeginBlockForProvider": timeAdvancement := lastAction["timeAdvancement"].Value.(int64) consumersToStart := lastAction["consumersToStart"].Value.(itf.ListExprType) consumersToStop := lastAction["consumersToStop"].Value.(itf.ListExprType) - t.Log(timeAdvancement, consumersToStart, consumersToStop) + t.Log("EndAndBeginBlockForProvider", timeAdvancement, consumersToStart, consumersToStop) + + driver.endAndBeginBlock("provider", time.Duration(timeAdvancement)*time.Second, func() {}) case "EndAndBeginBlockForConsumer": consumerChain := lastAction["consumerChain"].Value.(string) timeAdvancement := lastAction["timeAdvancement"].Value.(int64) - t.Log(consumerChain, timeAdvancement) + driver.endAndBeginBlock(ChainId(consumerChain), time.Duration(timeAdvancement)*time.Second, func() {}) + t.Log("EndAndBeginBlockForConsumer", consumerChain, timeAdvancement) case "DeliverVscPacket": consumerChain := lastAction["consumerChain"].Value.(string) - t.Log(consumerChain) + t.Log("DeliverVscPacket", consumerChain) case "DeliverVscMaturedPacket": consumerChain := lastAction["consumerChain"].Value.(string) - t.Log(consumerChain) + t.Log("DeliverVscMaturedPacket", consumerChain) default: log.Fatalf("Error loading trace file %s, step %v: do not know action type %s", diff --git a/tests/difference/core/quint_model/driver/setup.go b/tests/difference/core/quint_model/driver/setup.go index b85b592cb5..76a48ddfd2 100644 --- a/tests/difference/core/quint_model/driver/setup.go +++ b/tests/difference/core/quint_model/driver/setup.go @@ -368,8 +368,7 @@ func (s *Driver) setupChains( s.coordinator.Chains[chain] = consumerChain path := s.ConfigureNewPath(consumerChain, providerChain, params, providerHeader) - relayedPath := simibc.MakeRelayedPath(s.t, path) - s.simibcs[ChainId(chain)] = &relayedPath + s.simibcs[ChainId(chain)] = simibc.MakeRelayedPath(s.t, path) } } diff --git a/testutil/simibc/relayed_path.go b/testutil/simibc/relayed_path.go index daf32f0c84..8105b7997e 100644 --- a/testutil/simibc/relayed_path.go +++ b/testutil/simibc/relayed_path.go @@ -1,9 +1,10 @@ package simibc import ( + "bytes" "testing" - "time" + channeltypes "github.com/cosmos/ibc-go/v7/modules/core/04-channel/types" ibctmtypes "github.com/cosmos/ibc-go/v7/modules/light-clients/07-tendermint" ibctesting "github.com/cosmos/ibc-go/v7/testing" ) @@ -16,7 +17,7 @@ import ( // new blocks on each chain. type RelayedPath struct { t *testing.T - path *ibctesting.Path + Path *ibctesting.Path // clientHeaders is a map from chainID to an ordered list of headers that // have been committed to that chain. The headers are used to update the // client of the counterparty chain. @@ -30,28 +31,85 @@ type RelayedPath struct { // MakeRelayedPath returns an initialized RelayedPath without any // packets, acks or headers. Requires a fully initialised path where // the connection and any channel handshakes have been COMPLETED. -func MakeRelayedPath(t *testing.T, path *ibctesting.Path) RelayedPath { +func MakeRelayedPath(t *testing.T, path *ibctesting.Path) *RelayedPath { t.Helper() - return RelayedPath{ + return &RelayedPath{ t: t, clientHeaders: map[string][]*ibctmtypes.Header{}, - path: path, + Path: path, Outboxes: MakeOrderedOutbox(), } } +// PacketBelongs returns true if the packet belongs to this relayed path. +func (f *RelayedPath) PacketBelongs(packet channeltypes.Packet) bool { + return f.PacketSentByA(packet) || f.PacketSentByB(packet) +} + +// PacketSentByA returns true if the given packet was sent by chain A on this path. +func (f *RelayedPath) PacketSentByA(packet channeltypes.Packet) bool { + committedByA := f.Path.EndpointA.Chain.App.GetIBCKeeper().ChannelKeeper.GetPacketCommitment( + f.Path.EndpointA.Chain.GetContext(), + f.Path.EndpointA.ChannelConfig.PortID, + f.Path.EndpointA.ChannelID, + packet.GetSequence(), + ) + + return bytes.Equal(committedByA, channeltypes.CommitPacket(f.Path.EndpointA.Chain.App.AppCodec(), packet)) +} + +// PacketSentByB returns true if the given packet was sent by chain B on this path. +func (f *RelayedPath) PacketSentByB(packet channeltypes.Packet) bool { + committedByB := f.Path.EndpointB.Chain.App.GetIBCKeeper().ChannelKeeper.GetPacketCommitment( + f.Path.EndpointB.Chain.GetContext(), + f.Path.EndpointB.ChannelConfig.PortID, + f.Path.EndpointB.ChannelID, + packet.GetSequence(), + ) + + return bytes.Equal(committedByB, channeltypes.CommitPacket(f.Path.EndpointB.Chain.App.AppCodec(), packet)) +} + +// AddPacket adds a packet to the outbox of the chain with chainID. +// It will fail if the chain is not involved in the relayed path, +// or if the packet does not belong to this path, +// i.e. if the pace +func (f *RelayedPath) AddPacket(chainID string, packet channeltypes.Packet) { + if !f.InvolvesChain(chainID) { + f.t.Fatal("in relayed path could not add packet to chain: ", chainID, " because it is not involved in the relayed path") + } + + f.Outboxes.AddPacket(chainID, packet) +} + +// AddClientHeader adds a client header to the chain with chainID. +// The header is used to update the client of the counterparty chain. +// It will fail if the chain is not involved in the relayed path. +func (f *RelayedPath) AddClientHeader(chainID string, header *ibctmtypes.Header) { + if !f.InvolvesChain(chainID) { + f.t.Fatal("in relayed path could not add client header to chain: ", chainID, " because it is not involved in the relayed path") + } + f.clientHeaders[chainID] = append(f.clientHeaders[chainID], header) +} + // Chain returns the chain with chainID func (f *RelayedPath) Chain(chainID string) *ibctesting.TestChain { - if f.path.EndpointA.Chain.ChainID == chainID { - return f.path.EndpointA.Chain + if f.Path.EndpointA.Chain.ChainID == chainID { + return f.Path.EndpointA.Chain } - if f.path.EndpointB.Chain.ChainID == chainID { - return f.path.EndpointB.Chain + if f.Path.EndpointB.Chain.ChainID == chainID { + return f.Path.EndpointB.Chain } f.t.Fatal("no chain found in relayed path with chainID: ", chainID) return nil } +// InvolvesChain returns true if the chain is involved in the relayed path, +// i.e. if it is either the source or destination chain. +func (f *RelayedPath) InvolvesChain(chainID string) bool { + return f.Path.EndpointA.Chain.ChainID == chainID || f.Path.EndpointB.Chain.ChainID == chainID +} + // UpdateClient updates the chain with the latest sequence // of available headers committed by the counterparty chain since // the last call to UpdateClient (or all for the first call). @@ -106,35 +164,13 @@ func (f *RelayedPath) DeliverAcks(chainID string, num int) { } } -// EndAndBeginBlock calls EndBlock and commits block state, storing the header which can later -// be used to update the client on the counterparty chain. After committing, the chain local -// time progresses by dt, and BeginBlock is called with a header timestamped for the new time. -// -// preCommitCallback is called after EndBlock and before Commit, allowing arbitrary access to -// the sdk.Context after EndBlock. The callback is useful for testing purposes to execute -// arbitrary code before the chain sdk context is cleared in .Commit(). -// For example, app.EndBlock may lead to a new state, which you would like to query -// to check that it is correct. However, the sdk context is cleared after .Commit(), -// so you can query the state inside the callback. -func (f *RelayedPath) EndAndBeginBlock(chainID string, dt time.Duration, preCommitCallback func()) { - c := f.Chain(chainID) - - header, packets := EndBlock(c, preCommitCallback) - f.clientHeaders[chainID] = append(f.clientHeaders[chainID], header) - for _, p := range packets { - f.Outboxes.AddPacket(chainID, p) - } - f.Outboxes.Commit(chainID) - BeginBlock(c, dt) -} - // counterparty is a helper returning the counterparty chainID func (f *RelayedPath) counterparty(chainID string) string { - if f.path.EndpointA.Chain.ChainID == chainID { - return f.path.EndpointB.Chain.ChainID + if f.Path.EndpointA.Chain.ChainID == chainID { + return f.Path.EndpointB.Chain.ChainID } - if f.path.EndpointB.Chain.ChainID == chainID { - return f.path.EndpointA.Chain.ChainID + if f.Path.EndpointB.Chain.ChainID == chainID { + return f.Path.EndpointA.Chain.ChainID } f.t.Fatal("no chain found in relayed path with chainID: ", chainID) return "" @@ -142,11 +178,11 @@ func (f *RelayedPath) counterparty(chainID string) string { // endpoint is a helper returning the endpoint for the chain func (f *RelayedPath) endpoint(chainID string) *ibctesting.Endpoint { - if chainID == f.path.EndpointA.Chain.ChainID { - return f.path.EndpointA + if chainID == f.Path.EndpointA.Chain.ChainID { + return f.Path.EndpointA } - if chainID == f.path.EndpointB.Chain.ChainID { - return f.path.EndpointB + if chainID == f.Path.EndpointB.Chain.ChainID { + return f.Path.EndpointB } f.t.Fatal("no chain found in relayed path with chainID: ", chainID) return nil