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 slots always belong to cancelled requests

This commit is contained in:
r4bbit 2024-08-21 20:49:33 +02:00
parent 0acb522fe7
commit 7dc5566cd9
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

@ -182,6 +182,13 @@ invariant paidSlotAlwaysHasFinishedOrCancelledRequest(env e, Marketplace.SlotId
}
}
// STATUS - verified
// cancelled slot always belongs to cancelled request
// https://prover.certora.com/output/6199/80d5dc73d406436db166071e277283f1?anonymousKey=d5d175960dc40f72e22ba8e31c6904a488277e57
invariant cancelledSlotAlwaysHasCancelledRequest(env e, Marketplace.SlotId slotId)
currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled =>
currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled;
/*--------------------------------------------
| Properties |
--------------------------------------------*/