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

chore(certora); add rule to verify slot is failed or free when request 

has failed
This commit is contained in:
r4bbit 2024-08-21 20:53:38 +02:00
parent 7dc5566cd9
commit 7c542e72b6
1 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
certora/specs/Marketplace.spec
View File

@ -222,6 +222,21 @@ rule totalSentCannotDecrease(env e, method f) {
assert total_after >= total_before; assert total_after >= total_before;
} }
rule slotIsFailedOrFreeIfRequestHasFailed(env e, method f) {
calldataarg args;
Marketplace.SlotId slotId;
requireInvariant paidSlotAlwaysHasFinishedOrCancelledRequest(e, slotId);
require currentContract.requestState(e, currentContract.slots(e, slotId).requestId) != Marketplace.RequestState.Failed;
f(e, args);
require currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Failed;
assert currentContract.slotState(e, slotId) == Marketplace.SlotState.Failed ||
currentContract.slotState(e, slotId) == Marketplace.SlotState.Free;
}
rule allowedRequestStateChanges(env e, method f) { rule allowedRequestStateChanges(env e, method f) {
calldataarg args; calldataarg args;
Marketplace.RequestId requestId; Marketplace.RequestId requestId;