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

fix(certora): make rule for allowed request state changes work again

This commit is contained in:
r4bbit 2024-08-21 21:31:56 +02:00
parent 7dc26ccc47
commit 3a6249e886
2 changed files with 42 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
certora/specs/Marketplace.spec
View File

@ -241,15 +241,53 @@ rule slotIsFailedOrFreeIfRequestHasFailed(env e, method f) {
rule allowedRequestStateChanges(env e, method f) {
calldataarg args;
Marketplace.RequestId requestId;
Marketplace.SlotId slotId;
Marketplace.RequestId requestId = currentContract.slots(e, slotId).requestId;
// needed, otherwise it finds counter examples where
// `SlotState.Cancelled` and `RequestState.New`
requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId);
// needed, otherwise it finds counter example where
// `SlotState.Finished` and `RequestState.New`
requireInvariant finishedSlotAlwaysHasFinishedRequest(e, slotId);
// Without this, the prover will find counter examples with `requestId == 0`,
// which are unlikely in practice as `requestId` is a hash from a request object.
// However, `requestId == 0` enforces `SlotState.Free` in the `fillSlot` function regardless,
// which ultimately results in counter examples where we have a state change
// RequestState.Cancelled -> RequestState.Finished, which is forbidden.
//
// COUNTER EXAMPLE: https://prover.certora.com/output/6199/3a4f410e6367422ba60b218a08c04fae?anonymousKey=0d7003af4ee9bc18c0da0c80a216a6815d397370
//
// The `require` below is a hack to ensure we exclude such cases as the code
// reverts in `requestIsKnown()` modifier (simply `require requestId != 0` isn't
// sufficient here)
require requestId == to_bytes32(0) => currentContract._requests[requestId].client == 0;
Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
// we need to check for `freeSlot(slotId)` here to ensure it's being called with
// the slotId we're interested in and not any other slotId (that may not pass the
// required invariants)
if (f.selector == sig:freeSlot(Marketplace.SlotId).selector || f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector) {
freeSlot(e, slotId);
} else {
f(e, args);
}
Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
// RequestState.New -> RequestState.Started
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Started => requestStateBefore == Marketplace.RequestState.New;
// RequestState.Started -> RequestState.Finished
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Finished => requestStateBefore == Marketplace.RequestState.Started;
// RequestState.Started -> RequestState.Failed
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Failed => requestStateBefore == Marketplace.RequestState.Started;
// RequestState.New -> RequestState.Cancelled
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Cancelled => requestStateBefore == Marketplace.RequestState.New;
}

3
contracts/Marketplace.sol
View File

@ -468,7 +468,8 @@ contract Marketplace is Proofs, StateRetrieval, Endian {
) {
return RequestState.Cancelled;
} else if (
context.state == RequestState.Started && block.timestamp > context.endsAt
(context.state == RequestState.Started ||
context.state == RequestState.New) && block.timestamp > context.endsAt
) {
return RequestState.Finished;
} else {