codex-storage
/
codex-contracts-eth
mirror of https://github.com/codex-storage/codex-contracts-eth.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

chore(certora): introduce invariant that finished slots always belong to finished requests

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

@ -163,6 +163,13 @@ invariant failedRequestAlwaysEnded(env e, Marketplace.RequestId requestId)
currentContract.requestState(e, requestId) == Marketplace.RequestState.Failed =>
currentContract.requestContext(e, requestId).endsAt < lastBlockTimestampGhost;
// STATUS - verified
// finished slot always has finished request
// https://prover.certora.com/output/6199/3371ee4f80354ac9b05b1c84c53b6154?anonymousKey=eab83785acb61ccd31ed0c9d5a2e9e2b24099156
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;
/*--------------------------------------------
| Properties |
--------------------------------------------*/