Start refactoring relaying code

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

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",

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)
 	}
 }
 

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,47 +164,25 @@ 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 ""
 }
 
 // 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