status-im
/
dagger-contracts
mirror of https://github.com/status-im/dagger-contracts.git
2
0
Fork 0
Code Issues Projects Releases Wiki Activity

chore(certora): add invariant that cancelled requests are always expired

This commit is contained in:
r4bbit 2024-08-21 20:37:43 +02:00
parent ebdf9ed366
commit 7ce7a5dda0
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
certora/specs/Marketplace.spec
View File

@ -149,6 +149,13 @@ invariant slotMissedShouldBeEqualToNumberOfMissedPeriods(env e, Marketplace.Slot
invariant cantBeMissedIfInPeriod(MarketplaceHarness.SlotId slotId, Periods.Period period)
lastBlockTimestampGhost <= publicPeriodEnd(period) => !_missingMirror[slotId][period];
// STATUS - verified
// cancelled request is always expired
// https://prover.certora.com/output/6199/36b12b897f3941faa00fb4ab6871be8e?anonymousKey=de98a02041b841fb2fa67af4222f29fac258249f
invariant cancelledRequestAlwaysExpired(env e, Marketplace.RequestId requestId)
currentContract.requestState(e, requestId) == Marketplace.RequestState.Cancelled =>
currentContract.requestExpiry(e, requestId) < lastBlockTimestampGhost;
/*--------------------------------------------
| Properties |
--------------------------------------------*/