cp

.gitignore

@@ -6,3 +6,5 @@ docs/tla/states/
 *.out
 vendor/
 .vscode
+tests/difference/core/driver/traceAlt.json
+tests/difference/core/driver/tracesAlt.json

tests/difference/core/driver/core_test.go

@@ -31,8 +31,8 @@ import (
 
 type KeyMapHelp struct {
 	// Map validators to the consumer pub key at a particular time
-	mapping   map[int64]providerkeeper.ConsumerPubKey
-	valBonded map[int64]bool
+	mapping          map[int64]providerkeeper.ConsumerPubKey
+	valPositivePower map[int64]bool
 }
 
 type CoreSuite struct {
@@ -94,6 +94,20 @@ func (b *CoreSuite) consumerKeeper() consumerkeeper.Keeper {
 	return b.consumerChain().App.(*appConsumer.App).ConsumerKeeper
 }
 
+func (s *CoreSuite) consumerGreatestVscID() int64 {
+	// TODO: clean up..
+	unmaturedVscIDs := []int{}
+	s.consumerKeeper().IteratePacketMaturityTime(s.ctx(C), func(vscId, timeNs uint64) bool {
+		unmaturedVscIDs = append(unmaturedVscIDs, int(vscId)) // TODO: check validity of conversion
+		return false
+	})
+	sort.Ints(unmaturedVscIDs)
+	if 0 < len(unmaturedVscIDs) {
+		return int64(unmaturedVscIDs[len(unmaturedVscIDs)-1])
+	}
+	return -1
+}
+
 // height returns the height of the current header of chain
 func (s *CoreSuite) height(chain string) int64 {
 	return s.chain(chain).CurrentHeader.GetHeight()
@@ -213,13 +227,13 @@ func (s *CoreSuite) consumerSlash(val int64, h int64, isDowntime bool) {
 			return false
 		})
 		sort.Ints(unmaturedVscIDs)
-		if 0 < len(unmaturedVscIDs) {
-			unmaturedVscIDs = unmaturedVscIDs[:len(unmaturedVscIDs)-1]
-		}
+		// if 0 < len(unmaturedVscIDs) {
+		// unmaturedVscIDs = unmaturedVscIDs[:len(unmaturedVscIDs)-1]
+		// }
 		choices := map[string]bool{}
 		for _, vscid := range unmaturedVscIDs {
 			help := s.keymapHelp[uint64(vscid)]
-			if help.valBonded[val] {
+			if help.valPositivePower[val] {
 				ck := help.mapping[val]
 				cca := providerkeeper.PubKeyToConsAddr(ck)
 				choices[string(cca)] = true
@@ -270,11 +284,8 @@ func (s *CoreSuite) deliver(chain string, numPackets int) {
 	s.simibc.DeliverPackets(s.chainID(chain), numPackets)
 }
 
-func (s *CoreSuite) fillKeymapHelp() {
-	// If the provider ended a block then we should query the current vscid
+func (s *CoreSuite) getKeymapHelp() KeyMapHelp {
 	k := s.providerKeeper()
-	vscid := k.GetValidatorSetUpdateId(s.ctx(P))
-	vscid -= 1 // The provider EndBlock does +=1 as a final step
 	mapping := map[int64]providerkeeper.ConsumerPubKey{}
 	k.KeyMap(s.ctx(P), s.chainID(C)).Store.IteratePcaToCk(func(pca providerkeeper.ProviderConsAddr, ck providerkeeper.ConsumerPubKey) bool {
 		for i := int64(0); i < int64(initState.NumValidators); i++ {
@@ -285,15 +296,11 @@ func (s *CoreSuite) fillKeymapHelp() {
 		}
 		return false
 	})
-	// if len(mapping) < initState.NumValidators {
-	// panic("not a full mapping")
-	// }
-	valBonded := map[int64]bool{}
+	valPositivePower := map[int64]bool{}
 	for j := int64(0); j < int64(initState.NumValidators); j++ {
-		status := s.validatorStatus(j)
-		valBonded[j] = status == stakingtypes.Bonded
+		valPositivePower[j] = 0 < s.providerTokens(j)
 	}
-	s.keymapHelp[vscid] = KeyMapHelp{mapping: mapping, valBonded: valBonded}
+	return KeyMapHelp{mapping: mapping, valPositivePower: valPositivePower}
 }
 
 func (s *CoreSuite) endAndBeginBlock(chain string) {
@@ -304,7 +311,10 @@ func (s *CoreSuite) endAndBeginBlock(chain string) {
 			if !good {
 				panic("not good internal invariants")
 			}
-			s.fillKeymapHelp()
+			k := s.providerKeeper()
+			vscid := k.GetValidatorSetUpdateId(s.ctx(P))
+			vscid -= 1 // The provider EndBlock does +=1 as a final step, TODO: think need to move this
+			s.keymapHelp[vscid] = s.getKeymapHelp()
 		}
 	})
 }
@@ -428,6 +438,8 @@ func (s *CoreSuite) TestAssumptions() {
 	s.Require().Equal(stakeParams.UnbondingTime, initState.UnbondingP)
 	// Consumer unbonding period is correct
 	s.Require().Equal(s.consumerKeeper().UnbondingTime(s.ctx(C)), initState.UnbondingC)
+	// Consumer last vscid seen is correct
+	s.Require().Equal(s.consumerGreatestVscID(), 42)
 
 	// Each validator has signing info
 	for i := 0; i < len(initState.ValStates.Tokens); i++ {
@@ -534,12 +546,12 @@ func (s *CoreSuite) TestTraces() {
 	s.traces = Traces{
 		Data: LoadTraces("tracesAlt.json"),
 	}
-	s.traces.Data = []TraceData{s.traces.Data[74]}
+	// s.traces.Data = []TraceData{s.traces.Data[74]}
 	for i := range s.traces.Data {
 		s.Run(fmt.Sprintf("Trace num: %d", i), func() {
 			// Setup a new pair of chains for each trace
 			s.SetupTest()
-			s.fillKeymapHelp()
+			s.keymapHelp = map[uint64]KeyMapHelp{}
 
 			s.traces.CurrentTraceIx = i
 			defer func() {
@@ -572,5 +584,4 @@ func (s *CoreSuite) SetupTest() {
 	s.offsetHeight = offsetHeight
 	s.offsetTimeUnix = offsetTimeUnix
 	s.simibc = simibc.MakeRelayedPath(s.Suite.T(), path)
-	s.keymapHelp = map[uint64]KeyMapHelp{}
 }

tests/difference/core/model/src/common.ts

@@ -112,7 +112,6 @@ type InvariantSnapshot = {
   undelegationQ: Undelegation[];
   delegatorTokens: number;
   consumerPower: (number | undefined)[];
-  hToVscID: Record<number, number>;
 };
 
 /**

tests/difference/core/model/src/constants.ts

@@ -100,6 +100,7 @@ enum Event {
   SEND_VSC_WITHOUT_DOWNTIME_ACK = 'send_vsc_without_downtime_ack',
   SOME_UNDELS_EXPIRED_BUT_NOT_COMPLETED = 'some_undels_expired_but_not_completed',
   RECEIVE_DOUBLE_SIGN_SLASH_REQUEST = 'receive_double_sign_slash_request',
+  RECEIVE_SLASH_REQUEST_UNBONDED = 'receive_slash_request_unbonded',
   DOWNTIME_SLASH_REQUEST_OUTSTANDING = 'downtime_slash_request_outstanding',
   CONSUMER_UPDATE_VAL = 'consumer_update_val',
   CONSUMER_DEL_VAL = 'consumer_del_val',

tests/difference/core/model/src/main.ts

@@ -115,28 +115,10 @@ class ActionGenerator {
       return true;
     }
     if (a.kind === 'ConsumerSlash') {
-      const maturingVscs = Array.from(
-        this.model.ccvC.maturingVscs.keys(),
-      );
-      const valSets = maturingVscs
-        .sort()
-        .slice(1, -1)
-        .map((vscid) => this.model.hist.getConsumerValset(vscid))
-        .filter((valset) => valset !== undefined) as (
-        | number
-        | undefined
-      )[][];
-      const slashableValidators = new Set();
-      valSets.forEach((valset) => {
-        valset.forEach((power, i) => {
-          if (power !== undefined) {
-            console.log(`powa`, power);
-            slashableValidators.add(i);
-          }
-        });
-      });
       return (
-        slashableValidators.has((a as ConsumerSlash).val) &&
+        this.model.blocks
+          .getSlashableValidators()
+          .has((a as ConsumerSlash).val) &&
         2 <= this.didSlash.filter((x) => !x).length
       );
     }

tests/difference/core/model/src/model.ts

@@ -446,6 +446,11 @@ class CCVProvider {
       infractionHeight = this.vscIDtoH[data.vscID];
     }
 
+    if (this.m.staking.status[data.val] === Status.UNBONDED) {
+      this.m.events.push(Event.RECEIVE_SLASH_REQUEST_UNBONDED);
+      return;
+    }
+
     if (data.isDowntime) {
       this.m.events.push(Event.RECEIVE_DOWNTIME_SLASH_REQUEST);
     } else {
@@ -596,15 +601,15 @@ class Model {
   staking: Staking;
   ccvP: CCVProvider;
   ccvC: CCVConsumer;
-  hist: BlockHistory;
+  blocks: BlockHistory;
   events: Event[];
 
   constructor(
-    hist: BlockHistory,
+    blocks: BlockHistory,
     events: Event[],
     state: ModelInitState,
   ) {
-    this.hist = hist;
+    this.blocks = blocks;
     this.events = events;
     this.h = state.h;
     this.t = state.t;
@@ -615,9 +620,9 @@ class Model {
     // model initial blocks on P and C because C starts with
     // the same validator set as P (and thus must have received
     // a packet from P).
-    this.hist.partialOrder.deliver(C, 0, 0);
-    this.hist.commitBlock(P, this.invariantSnapshot());
-    this.hist.commitBlock(C, this.invariantSnapshot());
+    this.blocks.partialOrder.deliver(C, 0, 0);
+    this.blocks.commitBlock(P, this.invariantSnapshot());
+    this.blocks.commitBlock(C, this.invariantSnapshot());
     this.beginBlock(P);
     this.beginBlock(C);
   }
@@ -631,7 +636,6 @@ class Model {
       undelegationQ: this.staking.undelegationQ,
       delegatorTokens: this.staking.delegatorTokens,
       consumerPower: this.ccvC.consumerPower,
-      hToVscID: this.ccvC.hToVscID,
     });
   };
 
@@ -658,13 +662,13 @@ class Model {
   deliver = (chain: Chain, num: number) => {
     if (chain === P) {
       this.outbox[C].consume(num).forEach((p) => {
-        this.hist.partialOrder.deliver(P, p.sendHeight, this.h[P]);
+        this.blocks.partialOrder.deliver(P, p.sendHeight, this.h[P]);
         this.ccvP.onReceive(p.data);
       });
     }
     if (chain === C) {
       this.outbox[P].consume(num).forEach((p) => {
-        this.hist.partialOrder.deliver(C, p.sendHeight, this.h[C]);
+        this.blocks.partialOrder.deliver(C, p.sendHeight, this.h[C]);
         this.ccvC.onReceive(p.data);
       });
     }
@@ -684,7 +688,7 @@ class Model {
       this.ccvC.endBlock();
     }
     this.outbox[chain].commit();
-    this.hist.commitBlock(chain, this.invariantSnapshot());
+    this.blocks.commitBlock(chain, this.invariantSnapshot());
   };
 
   beginBlock = (chain: Chain) => {

tests/difference/core/model/src/properties.ts

@@ -146,29 +146,27 @@ class BlockHistory {
     this.blocks[chain].set(h, b);
   };
 
-  /**
-   * Get the valset on the consumer chain when the consumer
-   * was up-to-date to vscid, in a committed block.
-   * @param vscid
-   */
-  getConsumerValset = (
-    vscid: number,
-  ): (number | undefined)[] | undefined => {
-    // TODO: this and it's usage is extremely inefficient
+  getSlashableValidators = (): Set<number> => {
     const greatestCommittedConsumerHeight = _.max(
       Array.from(this.blocks[C].keys()),
     );
-    const hToVscID = this.blocks[C].get(greatestCommittedConsumerHeight)
-      ?.invariantSnapshot?.hToVscID!;
-    let h = -1;
-    for (const [key, value] of Object.entries(hToVscID)) {
-      if (value === vscid) {
-        h = parseInt(key);
-        break;
+    const lastBlockSnapshot = this.blocks[C].get(
+      greatestCommittedConsumerHeight,
+    )?.invariantSnapshot!;
+    const greatestCommittedConsumerTime = lastBlockSnapshot.t[C];
+    const validators = new Set<number>();
+    for (let [_, block] of this.blocks[C]) {
+      const t = block.invariantSnapshot.t[C];
+      if (greatestCommittedConsumerTime < t + UNBONDING_SECONDS_C) {
+        block.invariantSnapshot.consumerPower.forEach((power, i) => {
+          if (power !== undefined) {
+            validators.add(i);
+          }
+        });
       }
     }
-    const commitH = h - 1;
-    return this.blocks[C].get(commitH)?.invariantSnapshot?.consumerPower!;
+    // console.log(Array.from(validators.values()));
+    return validators;
   };
 }