diff --git a/tests/difference/core/model/src/constants.ts b/tests/difference/core/model/src/constants.ts index e6e5cad9f5..a06af28e20 100644 --- a/tests/difference/core/model/src/constants.ts +++ b/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], diff --git a/tests/difference/core/model/src/properties.ts b/tests/difference/core/model/src/properties.ts index c7957ee171..65d7bff86f 100644 --- a/tests/difference/core/model/src/properties.ts +++ b/tests/difference/core/model/src/properties.ts @@ -190,38 +190,50 @@ function stakingWithoutSlashing(hist: BlockHistory): boolean { * @returns Is the property satisfied? */ function validatorSetReplication(hist: BlockHistory): boolean { + // return true; const blocks = hist.blocks; let good = true; - blocks[C].forEach((b: CommittedBlock) => { - const ss = b.invariantSnapshot; - if (ss.h[C] === 0) { + 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[ss.h[C]]; + 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(ss.h[C] - 1)!.invariantSnapshot.consumerPower; + const valsetC = blocks[C].get(hC - 1)!.invariantSnapshot.consumerPower; // The provider set is implicitly defined by the status and tokens (power) - console.log(`hP: ${hP}`); + 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 - good = good && tokensP[i] === power; + // 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]; - good = good && valsetC[i] === power; + // Check that the consumer power is strictly equal to the provider power + good = good && (valsetC[i] === power); } else { - good = good && valsetC[i] === undefined; + // Ensure that the consumer validator set does not contain a non-bonded validator + good = good && (valsetC[i] === undefined); } })