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 paid slots always have a finished or cancelled request

This commit is contained in:
r4bbit 2024-08-21 20:48:47 +02:00
parent a1229b5af3
commit 0acb522fe7
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
certora/specs/Marketplace.spec
View File

@ -170,6 +170,18 @@ invariant finishedSlotAlwaysHasFinishedRequest(env e, Marketplace.SlotId slotId)
currentContract.slotState(e, slotId) == Marketplace.SlotState.Finished =>
currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Finished;
// STATUS - verified
// paid slot always has finished or cancelled request
// https://prover.certora.com/output/6199/6217a927ff2c43bea1124f6ae54a78fb?anonymousKey=d5e09d0d12658fd6b5f298fc04cea88da892c62d
invariant paidSlotAlwaysHasFinishedOrCancelledRequest(env e, Marketplace.SlotId slotId)
currentContract.slotState(e, slotId) == Marketplace.SlotState.Paid =>
currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Finished || currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled
{ preserved {
// ensures we start with a paid slot
require currentContract.slotState(e, slotId) == Marketplace.SlotState.Paid;
}
}
/*--------------------------------------------
| Properties |
--------------------------------------------*/