Reduce overapproximation for model consumer slashing

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

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

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

@@ -46,6 +46,8 @@ import {
 
 class ActionGenerator {
   model;
+  // the set of validators on the consumer at each vscid
+  validatorsKnownToConsumer = new Map<number, number[]>();
   // was the validator slashed?
   didSlash = new Array(NUM_VALIDATORS).fill(false);
   // the timestamp contained in the latest trusted header
@@ -115,7 +117,29 @@ class ActionGenerator {
       return true;
     }
     if (a.kind === 'ConsumerSlash') {
-      return 2 <= this.didSlash.filter((x) => !x).length;
+      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) {
+            slashableValidators.add(i);
+          }
+        });
+      });
+      return (
+        slashableValidators.has((a as ConsumerSlash).val) &&
+        2 <= this.didSlash.filter((x) => !x).length
+      );
     }
     if (a.kind === 'UpdateClient') {
       return true;

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

@@ -446,11 +446,6 @@ 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 {
@@ -601,15 +596,15 @@ class Model {
   staking: Staking;
   ccvP: CCVProvider;
   ccvC: CCVConsumer;
-  blocks: BlockHistory;
+  hist: BlockHistory;
   events: Event[];
 
   constructor(
-    blocks: BlockHistory,
+    hist: BlockHistory,
     events: Event[],
     state: ModelInitState,
   ) {
-    this.blocks = blocks;
+    this.hist = hist;
     this.events = events;
     this.h = state.h;
     this.t = state.t;
@@ -620,9 +615,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.blocks.partialOrder.deliver(C, 0, 0);
-    this.blocks.commitBlock(P, this.invariantSnapshot());
-    this.blocks.commitBlock(C, this.invariantSnapshot());
+    this.hist.partialOrder.deliver(C, 0, 0);
+    this.hist.commitBlock(P, this.invariantSnapshot());
+    this.hist.commitBlock(C, this.invariantSnapshot());
     this.beginBlock(P);
     this.beginBlock(C);
   }
@@ -636,6 +631,7 @@ class Model {
       undelegationQ: this.staking.undelegationQ,
       delegatorTokens: this.staking.delegatorTokens,
       consumerPower: this.ccvC.consumerPower,
+      hToVscID: this.ccvC.hToVscID,
     });
   };
 
@@ -662,13 +658,13 @@ class Model {
   deliver = (chain: Chain, num: number) => {
     if (chain === P) {
       this.outbox[C].consume(num).forEach((p) => {
-        this.blocks.partialOrder.deliver(P, p.sendHeight, this.h[P]);
+        this.hist.partialOrder.deliver(P, p.sendHeight, this.h[P]);
         this.ccvP.onReceive(p.data);
       });
     }
     if (chain === C) {
       this.outbox[P].consume(num).forEach((p) => {
-        this.blocks.partialOrder.deliver(C, p.sendHeight, this.h[C]);
+        this.hist.partialOrder.deliver(C, p.sendHeight, this.h[C]);
         this.ccvC.onReceive(p.data);
       });
     }
@@ -688,7 +684,7 @@ class Model {
       this.ccvC.endBlock();
     }
     this.outbox[chain].commit();
-    this.blocks.commitBlock(chain, this.invariantSnapshot());
+    this.hist.commitBlock(chain, this.invariantSnapshot());
   };
 
   beginBlock = (chain: Chain) => {

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

@@ -145,6 +145,31 @@ 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
+    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 commitH = h - 1;
+    return this.blocks[C].get(commitH)?.invariantSnapshot?.consumerPower!;
+  };
 }
 
 function sum(arr: number[]): number {