Partial refactor some model parts

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

@@ -105,7 +105,7 @@ type EndAndBeginBlock = {
   chain: Chain;
 };
 
-type InvariantSnapshot = {
+type SystemSnapshot = {
   h: Record<Chain, number>;
   t: Record<Chain, number>;
   lastVscid: Record<Chain, number>;
@@ -122,7 +122,7 @@ type InvariantSnapshot = {
  */
 interface CommittedBlock {
   chain: Chain;
-  invariantSnapshot: InvariantSnapshot;
+  systemSnapshot: SystemSnapshot;
 }
 
 /**
@@ -200,7 +200,7 @@ export {
   UpdateClient,
   Deliver,
   EndAndBeginBlock,
-  InvariantSnapshot,
+  SystemSnapshot,
   Status,
   Undelegation,
   Unval,

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

@@ -35,8 +35,9 @@ const DELEGATE_AMT_MIN = 1000;
 const DELEGATE_AMT_MAX = 5000;
 const UNDELEGATE_AMT_MIN = 1000;
 const UNDELEGATE_AMT_MAX = 5000;
-const ISDOWNTIME_PROBABILITY = 0;
 const MAX_NUM_PACKETS_FOR_DELIVER = 6;
+const ENABLE_DOWNTIME = false;
+const ENABLE_KEY_ASSIGNMENT = false;
 
 const MODEL_INIT_STATE: ModelInitState = {
   h: { provider: 0, consumer: 0 },
@@ -125,7 +126,8 @@ export {
   DELEGATE_AMT_MAX,
   UNDELEGATE_AMT_MIN,
   UNDELEGATE_AMT_MAX,
-  ISDOWNTIME_PROBABILITY,
+  ENABLE_DOWNTIME,
+  ENABLE_KEY_ASSIGNMENT,
   MAX_NUM_PACKETS_FOR_DELIVER,
   Event,
   MODEL_INIT_STATE,

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

@@ -36,7 +36,8 @@ import {
   DELEGATE_AMT_MAX,
   UNDELEGATE_AMT_MIN,
   UNDELEGATE_AMT_MAX,
-  ISDOWNTIME_PROBABILITY,
+  ENABLE_DOWNTIME,
+  ENABLE_KEY_ASSIGNMENT,
   TRUSTING_SECONDS,
   BLOCK_SECONDS,
   MAX_NUM_PACKETS_FOR_DELIVER,
@@ -58,14 +59,18 @@ class ActionGenerator {
   }
 
   create = (): Action => {
-    const kind = _.sample([
+    const actionTypes = [
       'Delegate',
       'Undelegate',
       'ConsumerSlash',
       'EndAndBeginBlock',
       'Deliver',
       'UpdateClient',
-    ]);
+    ];
+    if (ENABLE_KEY_ASSIGNMENT) {
+      actionTypes.push('KeyAssignment');
+    }
+    const kind = _.sample(actionTypes);
     if (kind === 'Delegate') {
       return {
         kind,
@@ -85,7 +90,7 @@ class ActionGenerator {
         kind,
         val: _.random(0, NUM_VALIDATORS - 1),
         infractionHeight: Math.floor(Math.random() * this.model.h[C]),
-        isDowntime: Math.random() < ISDOWNTIME_PROBABILITY,
+        isDowntime: Math.random() < (ENABLE_DOWNTIME ? 0.5 : 0),
       } as ConsumerSlash;
     }
     if (kind === 'UpdateClient') {
@@ -115,9 +120,11 @@ class ActionGenerator {
       return true;
     }
     if (a.kind === 'ConsumerSlash') {
+      // The consumer can only slash validators who were validating
+      // since the last maturity.
       return (
         this.model.blocks
-          .getSlashableValidators()
+          .getNonMaturedRecentConsumerValidators()
           .has((a as ConsumerSlash).val) &&
         2 <= this.didSlash.filter((x) => !x).length
       );
@@ -149,7 +156,9 @@ class ActionGenerator {
     if (a.kind === 'ConsumerSlash') {
       const val = (a as ConsumerSlash).val;
       this.didSlash[val] = true;
-      const vscids = this.model.blocks.getSlashableValidators().get(val);
+      const vscids = this.model.blocks
+        .getNonMaturedRecentConsumerValidators()
+        .get(val);
       const items = Array.from(vscids as Set<number>);
       const vscid = items[Math.floor(Math.random() * items.length)];
       (a as ConsumerSlash).vscid = vscid;

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

@@ -32,7 +32,7 @@ import {
   Validator,
   PacketData,
   Slash,
-  InvariantSnapshot,
+  SystemSnapshot,
   Status,
   ModelInitState,
 } from './common.js';
@@ -621,13 +621,13 @@ class Model {
     // 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.blocks.commitBlock(P, this.snapshot());
+    this.blocks.commitBlock(C, this.snapshot());
     this.beginBlock(P);
     this.beginBlock(C);
   }
 
-  invariantSnapshot = (): InvariantSnapshot => {
+  snapshot = (): SystemSnapshot => {
     return cloneDeep({
       h: this.h,
       t: this.t,
@@ -692,7 +692,7 @@ class Model {
       this.ccvC.endBlock();
     }
     this.outbox[chain].commit();
-    this.blocks.commitBlock(chain, this.invariantSnapshot());
+    this.blocks.commitBlock(chain, this.snapshot());
   };
 
   beginBlock = (chain: Chain) => {

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

@@ -7,10 +7,10 @@ import {
   NUM_VALIDATORS,
 } from './constants.js';
 import {
-  InvariantSnapshot,
   Chain,
   CommittedBlock,
   Status,
+  SystemSnapshot,
 } from './common.js';
 
 /**
@@ -135,45 +135,51 @@ class BlockHistory {
   /**
    * Mark state as permanently committed to the blockchain.
    * @param chain
-   * @param invariantSnapshot
+   * @param systemSnapshot
    */
-  commitBlock = (chain: Chain, invariantSnapshot: InvariantSnapshot) => {
-    const h = invariantSnapshot.h[chain];
+  commitBlock = (chain: Chain, systemSnapshot: SystemSnapshot) => {
+    const h = systemSnapshot.h[chain];
     const b: CommittedBlock = {
       chain,
-      invariantSnapshot,
+      systemSnapshot: systemSnapshot,
     };
     this.blocks[chain].set(h, b);
   };
 
-  getSlashableValidators = (): Map<number, Set<number>> => {
+  /**
+   * @returns Get a map of vscid to the set of validators
+   * who were validating at that vscid on the consumer chain.
+   */
+  getNonMaturedRecentConsumerValidators = (): Map<
+    number,
+    Set<number>
+  > => {
     const greatestCommittedConsumerHeight = _.max(
       Array.from(this.blocks[C].keys()),
     );
-    const lastBlockSS = this.blocks[C].get(
+    const lastSnapshot = this.blocks[C].get(
       greatestCommittedConsumerHeight,
-    )?.invariantSnapshot!;
+    )?.systemSnapshot!;
 
-    const validators = new Map<number, Set<number>>();
+    const ret = new Map<number, Set<number>>();
 
     for (let [_, block] of this.blocks[C]) {
-      const ss = block.invariantSnapshot;
-      const t = ss.t[C];
-      if (lastBlockSS.t[C] < t + UNBONDING_SECONDS_C) {
+      const ss = block.systemSnapshot;
+      if (lastSnapshot.t[C] < ss.t[C] + UNBONDING_SECONDS_C) {
         ss.consumerPower.forEach((power, i) => {
+          // If the validator had power.
           if (power !== undefined) {
-            if (!validators.has(i)) {
-              validators.set(i, new Set<number>());
+            if (!ret.has(i)) {
+              ret.set(i, new Set<number>());
             }
-            const set = validators.get(i);
+            const set = ret.get(i);
             const vscid = ss.lastVscid[C];
             set?.add(vscid);
           }
         });
       }
     }
-    // console.log(Array.from(validators.values()));
-    return validators;
+    return ret;
   };
 }
 
@@ -194,9 +200,9 @@ function stakingWithoutSlashing(hist: BlockHistory): boolean {
   const blocks = Array.from(hist.blocks[P].entries())
     .sort((a, b) => a[0] - b[0])
     .map((e) => e[1])
-    .map((b) => b.invariantSnapshot);
+    .map((b) => b.systemSnapshot);
 
-  function value(e: InvariantSnapshot) {
+  function value(e: SystemSnapshot) {
     let x = e.delegatorTokens;
     x += sum(e.tokens);
     x += sum(e.undelegationQ.map((e) => e.balance));
@@ -231,11 +237,11 @@ function bondBasedConsumerVotingPower(hist: BlockHistory): boolean {
   function powerProvider(block: CommittedBlock, hp: number): number[] {
     return _.range(NUM_VALIDATORS).map((i) => {
       let x = 0;
-      if (block.invariantSnapshot.status[i] !== Status.UNBONDED) {
-        x += block.invariantSnapshot.tokens[i];
+      if (block.systemSnapshot.status[i] !== Status.UNBONDED) {
+        x += block.systemSnapshot.tokens[i];
       }
       x += sum(
-        block.invariantSnapshot.undelegationQ
+        block.systemSnapshot.undelegationQ
           .filter((e) => e.val === i)
           .filter((e) => hp <= e.creationHeight)
           .map((e) => e.initialBalance),
@@ -244,22 +250,23 @@ function bondBasedConsumerVotingPower(hist: BlockHistory): boolean {
     });
   }
   function powerConsumer(block: CommittedBlock) {
-    return block.invariantSnapshot.consumerPower;
+    return block.systemSnapshot.consumerPower;
   }
   function inner(hc: number): boolean {
     const hp = partialOrder.getGreatestPred(C, hc);
     assert(hp !== undefined, 'this should never happen.');
     function getHC_() {
-      const tsHC = (blocks[C].get(hc) as CommittedBlock).invariantSnapshot
-        .t[C];
+      const tsHC = (blocks[C].get(hc) as CommittedBlock).systemSnapshot.t[
+        C
+      ];
       // Get earliest height on consumer
       // that a VSC received at hc could mature
       const heights = Array.from(blocks[C].keys()).sort((a, b) => a - b);
       for (let i = 0; i < heights.length; i++) {
         const hc_ = heights[i];
         if (
           tsHC + UNBONDING_SECONDS_C <=
-          (blocks[C].get(hc_) as CommittedBlock).invariantSnapshot.t[C]
+          (blocks[C].get(hc_) as CommittedBlock).systemSnapshot.t[C]
         ) {
           return hc_;
         }

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

@@ -21,7 +21,8 @@ import {
   DELEGATE_AMT_MAX,
   UNDELEGATE_AMT_MIN,
   UNDELEGATE_AMT_MAX,
-  ISDOWNTIME_PROBABILITY,
+  ENABLE_DOWNTIME,
+  ENABLE_KEY_ASSIGNMENT,
   MAX_NUM_PACKETS_FOR_DELIVER,
 } from './constants.js';
 
@@ -78,8 +79,9 @@ function dumpTrace(fn: string, actions: TraceAction[], events: Event[]) {
       DELEGATE_AMT_MAX,
       UNDELEGATE_AMT_MIN,
       UNDELEGATE_AMT_MAX,
-      ISDOWNTIME_PROBABILITY,
       MAX_NUM_PACKETS_FOR_DELIVER,
+      ENABLE_DOWNTIME,
+      ENABLE_KEY_ASSIGNMENT,
     },
     // Record which actions occurred
     actions,