From 9cf0596661b996df6b8b449e4e4070e72b80c9e1 Mon Sep 17 00:00:00 2001 From: Daniel Date: Wed, 26 Oct 2022 14:02:39 +0100 Subject: [PATCH] Reduce overapproximation for model consumer slashing --- tests/difference/core/model/src/common.ts | 1 + tests/difference/core/model/src/main.ts | 26 ++++++++++++++++++- tests/difference/core/model/src/model.ts | 24 +++++++---------- tests/difference/core/model/src/properties.ts | 25 ++++++++++++++++++ 4 files changed, 61 insertions(+), 15 deletions(-) diff --git a/tests/difference/core/model/src/common.ts b/tests/difference/core/model/src/common.ts index 1c414f179f..e689e54ce5 100644 --- a/tests/difference/core/model/src/common.ts +++ b/tests/difference/core/model/src/common.ts @@ -112,6 +112,7 @@ type InvariantSnapshot = { undelegationQ: Undelegation[]; delegatorTokens: number; consumerPower: (number | undefined)[]; + hToVscID: Record; }; /** diff --git a/tests/difference/core/model/src/main.ts b/tests/difference/core/model/src/main.ts index f982bd30f7..e9418be0fb 100644 --- a/tests/difference/core/model/src/main.ts +++ b/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(); // 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; diff --git a/tests/difference/core/model/src/model.ts b/tests/difference/core/model/src/model.ts index 4ba2e9f464..480f1752ff 100644 --- a/tests/difference/core/model/src/model.ts +++ b/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) => { diff --git a/tests/difference/core/model/src/properties.ts b/tests/difference/core/model/src/properties.ts index 951298d44a..a8ce588f90 100644 --- a/tests/difference/core/model/src/properties.ts +++ b/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 {