Adds Validator Set Replication property check to core diff model (#589)

* Adds h-vscid maps to snapshot

* Calls ValidatorSetReplication in main

* Writes bulk of VSR property logic

* Fills snapshot with h-vscid mappings

* Implements the ValidatorSetReplication property

* Clarify hToVscID negative comment

* Delete accidental comment

* Improve clarity of height -1

* Use for loop

* bump

* bump

* Add comment tests/difference/core/model/src/properties.ts

Co-authored-by: Marius Poke <[email protected]>

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

Co-authored-by: Simon Noetzlin <[email protected]>

Co-authored-by: Daniel <[email protected]>
Co-authored-by: Marius Poke <[email protected]>
Co-authored-by: Simon Noetzlin <[email protected]>

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,13 @@ const MODEL_INIT_STATE: ModelInitState = {
   h: { provider: 0, consumer: 0 },
   t: { provider: 0, consumer: 0 },
   ccvC: {
-    hToVscID: { 0: 0, 1: 0 },
+    // We model a consumer chain that has already been established,
+    // but we model starting from height 0. It is necessary to have
+    // a vscid from the previous block, as is always the case in the
+    // real system and algorithm once a consumer has been added.
+    // Therefore we use -1 to represent the phantom vscid from the height
+    // before the first modelled height.
+    hToVscID: { 0: -1, 1: -1 },
     pendingChanges: [],
     maturingVscs: new Map(),
     outstandingDowntime: [false, false, false, false],
@@ -51,7 +57,8 @@ const MODEL_INIT_STATE: ModelInitState = {
   ccvP: {
     initialHeight: 0,
     vscID: 0,
-    vscIDtoH: {},
+    // See ccvC.hToVscID
+    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

@@ -657,6 +657,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,84 @@ 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 {
+  const blocks = hist.blocks;
+  let good = true;
+
+  // Each committed block on the consumer chain has a last vscID
+  // received that informs the validator set at the NEXT height.
+  // Thus, on every received VSCPacket with vscID at height H, 
+  // the consumer sets hToVscID[H+1] to vscID. 
+  //
+  // The consumer valset is exactly the valset on the provider
+  // at the NEXT height after the vscID was sent.
+  // Thus, on every sent VSCPacket with vscID at height H,
+  // the provider sets vscIDtoH[vscID] to H+1 
+  //
+  // As a result, for every height hC on the consumer, the active 
+  // valset was last updated by the VSCPacket with ID vscID = hToVscID[hc]. 
+  // This packet was sent by the provider at height hP-1, with hP = vscIDtoH[vscID]. 
+  // This means that the consumer valset at height hC MUST match
+  // the provider valset at height hP.
+  // 
+  // We compare these valsets, which are committed in blocks 
+  // hC-1 and hP-1, respectively (the valset is always used at the NEXT height).
+  for (const [hC, b] of blocks[C]) {
+    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.
+      continue
+    }
+    const snapshotC = b.invariantSnapshot;
+    // Get the vscid of the last update which dictated
+    // the consumer valset valsetC committed at hC-1
+    const vscid = snapshotC.hToVscID[hC];
+    // The VSU packet was sent at height hP-1
+    const hP = snapshotC.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.
+      continue
+    }
+    const snapshotP = blocks[P].get(hP - 1)!.invariantSnapshot;
+    const statusP = snapshotP.status;
+    const tokensP = snapshotP.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 +355,5 @@ export {
   BlockHistory,
   stakingWithoutSlashing,
   bondBasedConsumerVotingPower,
+  validatorSetReplication,
 };