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): introduce invariant that failed requests are always ended

This commit is contained in:
r4bbit 2024-08-21 20:45:49 +02:00
parent 7ce7a5dda0
commit 5b5a3c9e2e
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

@ -156,6 +156,13 @@ invariant cancelledRequestAlwaysExpired(env e, Marketplace.RequestId requestId)
currentContract.requestState(e, requestId) == Marketplace.RequestState.Cancelled => currentContract.requestState(e, requestId) == Marketplace.RequestState.Cancelled =>
currentContract.requestExpiry(e, requestId) < lastBlockTimestampGhost; currentContract.requestExpiry(e, requestId) < lastBlockTimestampGhost;
// STATUS - verified
// failed request is always ended
// https://prover.certora.com/output/6199/902ffe4a83a9438e9860655446b46a74?anonymousKey=47b344024bbfe84a649bd1de44d7d243ce8dbc21
invariant failedRequestAlwaysEnded(env e, Marketplace.RequestId requestId)
currentContract.requestState(e, requestId) == Marketplace.RequestState.Failed =>
currentContract.requestContext(e, requestId).endsAt < lastBlockTimestampGhost;
/*-------------------------------------------- /*--------------------------------------------
| Properties | | Properties |
--------------------------------------------*/ --------------------------------------------*/