Add logic for timed out vsc packets

tests/difference/core/quint_model/driver/core.go

@@ -260,14 +260,6 @@ func (s *Driver) updateClient(chain ChainId) error {
 	return s.path(chain).UpdateClient(string(chain), false)
 }
 
-// deliver numPackets packets from the network to chain
-func (s *Driver) deliver(chain ChainId, numPackets int) {
-	// Deliver any outstanding acks
-	s.path(chain).DeliverAcks(string(chain), 999999)
-	// Consume deliverable packets from the network
-	s.path(chain).DeliverPackets(string(chain), numPackets)
-}
-
 // packetQueue returns the queued packet sfrom sender to receiver,
 // where either sender or receiver must be the provider.
 func (s *Driver) packetQueue(sender ChainId, receiver ChainId) []simibc.Packet {
@@ -485,15 +477,15 @@ func (s *Driver) setAllTimes(newTimes map[ChainId]time.Time) {
 // DeliverPacketToConsumer delivers a packet from the provider to the given consumer recipient.
 // It updates the client before delivering the packet.
 // Since the channel is ordered, the packet that is delivered is the first packet in the outbox.
-func (s *Driver) DeliverPacketToConsumer(recipient ChainId) {
-	s.path(recipient).DeliverPackets(string(recipient), 1)
+func (s *Driver) DeliverPacketToConsumer(recipient ChainId, expectError bool) {
+	s.path(recipient).DeliverPackets(string(recipient), 1, expectError)
 }
 
 // DeliverPacketFromConsumer delivers a packet from the given consumer sender to the provider.
 // It updates the client before delivering the packet.
 // Since the channel is ordered, the packet that is delivered is the first packet in the outbox.
-func (s *Driver) DeliverPacketFromConsumer(sender ChainId) {
-	s.path(sender).DeliverPackets(P, 1) // deliver to the provider
+func (s *Driver) DeliverPacketFromConsumer(sender ChainId, expectError bool) {
+	s.path(sender).DeliverPackets(P, 1, expectError) // deliver to the provider
 }
 
 // DeliverAcks delivers, for each path,

tests/difference/core/quint_model/driver/generate_boundeddrift_traces.sh

@@ -1 +1 @@
-go run ./... -modelPath=../ccv_boundeddrift.qnt -step stepBoundedDrift  --inv CanTimeoutConsumer -traceFolder traces -numTraces 100
+go run ./... -modelPath=../ccv_boundeddrift.qnt -step stepBoundedDrift  -invariant CanTimeoutConsumer -traceFolder traces -numTraces 150 -numSteps 200 -numSamples 200

tests/difference/core/quint_model/driver/mbt_test.go

@@ -98,7 +98,7 @@ func RunItfTrace(t *testing.T, path string) {
 	t.Log("Chains are: ", chains)
 
 	// create params struct
-	vscTimeout := time.Duration(params["VscTimeout"].Value.(int64))
+	vscTimeout := time.Duration(params["VscTimeout"].Value.(int64)) * time.Second
 
 	unbondingPeriodPerChain := make(map[ChainId]time.Duration, len(consumers))
 	trustingPeriodPerChain := make(map[ChainId]time.Duration, len(consumers))
@@ -189,8 +189,24 @@ func RunItfTrace(t *testing.T, path string) {
 			// needs a header of height H+1 to accept the packet
 			// so we do one time advancement with a very small increment,
 			// and then increment the rest of the time]
+			runningConsumersBefore := driver.runningConsumers()
 			driver.endAndBeginBlock("provider", 1*time.Nanosecond)
 			driver.endAndBeginBlock("provider", time.Duration(timeAdvancement)*time.Second-1*time.Nanosecond)
+			runningConsumersAfter := driver.runningConsumers()
+
+			// the consumers that were running before but not after must have timed out
+			for _, consumer := range runningConsumersBefore {
+				found := false
+				for _, consumerAfter := range runningConsumersAfter {
+					if consumerAfter.ChainId == consumer.ChainId {
+						found = true
+						break
+					}
+				}
+				if !found {
+					stats.numTimeouts++
+				}
+			}
 
 			// save the last timestamp for runningConsumers,
 			// because setting up chains will modify timestamps
@@ -256,12 +272,36 @@ func RunItfTrace(t *testing.T, path string) {
 			consumerChain := lastAction["consumerChain"].Value.(string)
 			t.Log("DeliverVscPacket", consumerChain)
 
-			driver.DeliverPacketToConsumer(ChainId(consumerChain))
+			// delivering the packet should give an error
+			// if the consumer is timed out in the model
+			var expectError bool
+			if ConsumerStatus(currentModelState, consumerChain) == "timedout" {
+				expectError = true
+				driver.DeliverPacketToConsumer(ChainId(consumerChain), expectError)
+
+				// stop the consumer chain
+				driver.providerKeeper().StopConsumerChain(driver.providerCtx(), consumerChain, true)
+			} else {
+				expectError = false
+				driver.DeliverPacketToConsumer(ChainId(consumerChain), expectError)
+			}
 		case "DeliverVscMaturedPacket":
 			consumerChain := lastAction["consumerChain"].Value.(string)
 			t.Log("DeliverVscMaturedPacket", consumerChain)
 
-			driver.DeliverPacketFromConsumer(ChainId(consumerChain))
+			var expectError bool
+			if ConsumerStatus(currentModelState, consumerChain) == "timedout" {
+				expectError = true
+				// expectError is true, because we expect the consumer to have timed out.
+				// the call will fail if there is no error
+				driver.DeliverPacketFromConsumer(ChainId(consumerChain), expectError)
+
+				// stop the consumer chain on the provider
+				driver.providerKeeper().StopConsumerChain(driver.providerCtx(), consumerChain, true)
+			} else {
+				expectError = false
+				driver.DeliverPacketFromConsumer(ChainId(consumerChain), expectError)
+			}
 		default:
 
 			log.Fatalf("Error loading trace file %s, step %v: do not know action type %s",
@@ -397,7 +437,7 @@ func ComparePacketQueue(
 		actualPacket := actualSenderQueue[i]
 		modelPacket := modelSenderQueue[i].Value.(itf.MapExprType)
 
-		actualTimeout := int64(actualPacket.Packet.TimeoutTimestamp) - timeOffset.Unix()
+		actualTimeout := time.Unix(0, int64(actualPacket.Packet.TimeoutTimestamp)).Unix() - timeOffset.Unix()
 		modelTimeout := GetTimeoutForPacket(modelPacket)
 
 		require.Equal(t,

tests/difference/core/quint_model/driver/setup.go

@@ -357,6 +357,17 @@ func (s *Driver) ConfigureNewPath(consumerChain *ibctesting.TestChain, providerC
 
 	s.consumerKeeper(consumerChainId).InitGenesis(s.ctx(consumerChainId), consumerGenesis)
 
+	consumerGenesisForProvider := ccvtypes.ConsumerGenesisState{
+		Params:   consumerGenesis.Params,
+		Provider: consumerGenesis.Provider,
+		NewChain: consumerGenesis.NewChain,
+	}
+
+	s.providerKeeper().SetConsumerGenesis(
+		providerChain.GetContext(),
+		string(consumerChainId),
+		consumerGenesisForProvider)
+
 	// Client ID is set in InitGenesis and we treat it as a block box. So
 	// must query it to use it with the endpoint.
 	clientID, _ := s.consumerKeeper(consumerChainId).GetProviderClientID(s.ctx(consumerChainId))
@@ -408,6 +419,13 @@ func (s *Driver) setupProvider(
 	providerChain := newChain(s.t, params, s.coordinator, icstestingutils.ProviderAppIniter, "provider", valSet, signers, nodes, valNames)
 	s.coordinator.Chains["provider"] = providerChain
 
+	// set the VscTimeout
+	s.providerKeeper().SetVscTimeoutPeriod(s.ctx("provider"), params.VscTimeout)
+	// set the CcvTimeoutPeriod
+	providerParams := s.providerKeeper().GetParams(s.ctx("provider"))
+	providerParams.CcvTimeoutPeriod = params.CcvTimeout[ChainId(providerChain.ChainID)]
+	s.providerKeeper().SetParams(s.ctx("provider"), providerParams)
+
 	// produce a first block
 	simibc.EndBlock(providerChain, func() {})
 	simibc.BeginBlock(providerChain, 0)
@@ -444,18 +462,16 @@ func createConsumerGenesis(modelParams ModelParams, providerChain *ibctesting.Te
 		1000, // ignore distribution
 		"",   // ignore distribution
 		"",   // ignore distribution
-		ccv.DefaultCCVTimeoutPeriod,
+		modelParams.CcvTimeout[ChainId(consumerClientState.ChainId)],
 		ccv.DefaultTransferTimeoutPeriod,
 		ccv.DefaultConsumerRedistributeFrac,
 		ccv.DefaultHistoricalEntries,
-		consumerClientState.UnbondingPeriod,
+		modelParams.UnbondingPeriodPerChain[ChainId(consumerClientState.ChainId)],
 		"0", // disable soft opt-out
 		[]string{},
 		[]string{},
 		ccv.DefaultRetryDelayPeriod,
 	)
-	params.CcvTimeoutPeriod = modelParams.CcvTimeout[ChainId(consumerClientState.ChainId)]
-	params.UnbondingPeriod = modelParams.UnbondingPeriodPerChain[ChainId(consumerClientState.ChainId)]
 
 	return consumertypes.NewInitialGenesisState(consumerClientState, providerConsState, valUpdates, params)
 }

testutil/simibc/relay_util.go

@@ -68,7 +68,7 @@ func UpdateReceiverClient(sender, receiver *ibctesting.Endpoint, header *ibctmty
 // The packet must be sent from the sender chain to the receiver chain, and the
 // receiver chain must have a client for the sender chain which has been updated
 // to a recent height of the sender chain so that it can verify the packet.
-func TryRecvPacket(sender, receiver *ibctesting.Endpoint, packet channeltypes.Packet) (ack []byte, err error) {
+func TryRecvPacket(sender, receiver *ibctesting.Endpoint, packet channeltypes.Packet, expectError bool) (ack []byte, err error) {
 	packetKey := host.PacketCommitmentKey(packet.GetSourcePort(), packet.GetSourceChannel(), packet.GetSequence())
 	proof, proofHeight := sender.Chain.QueryProof(packetKey)
 
@@ -83,7 +83,7 @@ func TryRecvPacket(sender, receiver *ibctesting.Endpoint, packet channeltypes.Pa
 		receiver.Chain.ChainID,
 		[]uint64{receiver.Chain.SenderAccount.GetAccountNumber()},
 		[]uint64{receiver.Chain.SenderAccount.GetSequence()},
-		true, true, receiver.Chain.SenderPrivKey,
+		true, !expectError, receiver.Chain.SenderPrivKey,
 	)
 	if err != nil {
 		return nil, err

testutil/simibc/relayed_path.go

@@ -132,13 +132,16 @@ func (f *RelayedPath) UpdateClient(chainID string, expectExpiration bool) error
 //
 // In order to deliver packets, the chain must have an up-to-date client
 // of the counterparty chain. Ie. UpdateClient should be called before this.
-func (f *RelayedPath) DeliverPackets(chainID string, num int) {
+//
+// If expectError is true, we expect *each* packet to be delivered to cause an error.
+func (f *RelayedPath) DeliverPackets(chainID string, num int, expectError bool) {
 	for _, p := range f.Outboxes.ConsumePackets(f.Counterparty(chainID), num) {
-		ack, err := TryRecvPacket(f.endpoint(f.Counterparty(chainID)), f.endpoint(chainID), p.Packet)
-		if err != nil {
-			f.t.Fatal("deliver")
+		ack, err := TryRecvPacket(f.endpoint(f.Counterparty(chainID)), f.endpoint(chainID), p.Packet, expectError)
+		if err != nil && !expectError {
+			f.t.Fatal("Got an error from TryRecvPacket: ", err)
+		} else {
+			f.Outboxes.AddAck(chainID, ack, p.Packet)
 		}
-		f.Outboxes.AddAck(chainID, ack, p.Packet)
 	}
 }