Adds Validator Set Replication property check to core diff model

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

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

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

@@ -42,7 +42,11 @@ const MODEL_INIT_STATE: ModelInitState = {
   h: { provider: 0, consumer: 0 },
   t: { provider: 0, consumer: 0 },
   ccvC: {
-    hToVscID: { 0: 0, 1: 0 },
+    // The initial provider height is 0 but there must have been
+    // a vscid created at the previous height. However we do not
+    // use model this. Instead we use -1 to represent the phantom
+    // vscid.
+    hToVscID: { 0: -1, 1: -1 },
     pendingChanges: [],
     maturingVscs: new Map(),
     outstandingDowntime: [false, false, false, false],
@@ -51,7 +55,11 @@ const MODEL_INIT_STATE: ModelInitState = {
   ccvP: {
     initialHeight: 0,
     vscID: 0,
-    vscIDtoH: {},
+    // The initial provider height is 0 but there must have been
+    // a vscid created at the previous height. However we do not
+    // use model this. Instead we use -1 to represent the phantom
+    // vscid.
+    vscIDtoH: { [-1]: 0 },
     vscIDtoOpIDs: new Map(),
     downtimeSlashAcks: [],
     tombstoned: [false, false, false, false],

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

@@ -6,6 +6,7 @@ import {
   BlockHistory,
   stakingWithoutSlashing,
   bondBasedConsumerVotingPower,
+  validatorSetReplication,
 } from './properties.js';
 import { Model } from './model.js';
 import {
@@ -322,6 +323,10 @@ function gen(seconds: number, checkProperties: boolean) {
       if (checkProperties) {
         // Checking properties is flagged because it is computationally
         // expensive.
+        if (!validatorSetReplication(hist)) {
+          dumpTrace(`${DIR}trace_${i}.json`, actions, events);
+          throw 'validatorSetReplication property failure, trace written.';
+        }
         if (!bondBasedConsumerVotingPower(hist)) {
           dumpTrace(`${DIR}trace_${i}.json`, actions, events);
           throw 'bondBasedConsumerVotingPower property failure, trace written.';

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

@@ -636,6 +636,8 @@ class Model {
       undelegationQ: this.staking.undelegationQ,
       delegatorTokens: this.staking.delegatorTokens,
       consumerPower: this.ccvC.consumerPower,
+      vscIDtoH: this.ccvP.vscIDtoH,
+      hToVscID: this.ccvC.hToVscID
     });
   };
 

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

@@ -182,6 +182,65 @@ function stakingWithoutSlashing(hist: BlockHistory): boolean {
   return true;
 }
 
+/**
+ * Checks the validator set replication property as defined
+ * https://github.com/cosmos/ibc/blob/main/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md#system-properties
+ *
+ * @param hist A history of blocks.
+ * @returns Is the property satisfied?
+ */
+function validatorSetReplication(hist: BlockHistory): boolean {
+  // return true;
+  const blocks = hist.blocks;
+  let good = true;
+  blocks[C].forEach((b: CommittedBlock, hC: number) => {
+    if (hC < 1) {
+      // The model starts at consumer height 0, so there is
+      // no committed block at height - 1. This means it does
+      // not make sense to try to check the property for height 0.
+      return
+    }
+    const ss = b.invariantSnapshot;
+    // Get the vscid of the last update which dictated
+    // the consumer valset valsetC committed at hC-1
+    const vscid = ss.hToVscID[hC];
+    // The VSU packet was sent at height hP-1
+    const hP = ss.vscIDtoH[vscid];
+    // Compare the validator sets at hC-1 and hP-1
+    const valsetC = blocks[C].get(hC - 1)!.invariantSnapshot.consumerPower;
+    // The provider set is implicitly defined by the status and tokens (power)
+    if (hP < 1) {
+      // The model starts at provider height 0, so there is
+      // no committed block at height - 1. This means it does not
+      // make sense to try to check the property for height 0.
+      return
+    }
+    const statusP = blocks[P].get(hP - 1)!.invariantSnapshot.status;
+    const tokensP = blocks[P].get(hP - 1)!.invariantSnapshot.tokens;
+    assert(valsetC.length === statusP.length, 'this should never happen.');
+    assert(valsetC.length === tokensP.length, 'this should never happen.');
+    valsetC.forEach((power, i) => {
+      if (power !== undefined) { // undefined means the validator is not in the set
+        // Check that the consumer power is strictly equal to the provider power
+        good = good && (tokensP[i] === power);
+      }
+    })
+    statusP.forEach((status, i) => {
+      if (status === Status.BONDED) {
+        const power = tokensP[i];
+        // Check that the consumer power is strictly equal to the provider power
+        good = good && (valsetC[i] === power);
+      }
+      else {
+        // Ensure that the consumer validator set does not contain a non-bonded validator
+        good = good && (valsetC[i] === undefined);
+      }
+    })
+
+  })
+  return good;
+}
+
 /**
  * Checks the bond-based consumer voting power property as defined
  * in https://github.com/cosmos/ibc/blob/main/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md#system-properties
@@ -277,4 +336,5 @@ export {
   BlockHistory,
   stakingWithoutSlashing,
   bondBasedConsumerVotingPower,
+  validatorSetReplication,
 };