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 vacuous rule pass 

The rule `slotIsFailedOrFreeIfRequestHasFailed` currently has violations
as it is vacuous for some functions in the `Marketplace` contract.

The rule being vacuous means that the function on which the rule is
tested either doesn't have a case where the required conditions work (it
reverts), or, in this case, where any given function doesn't have a case
where it reaches the required state change.

There's various functions where this applies because the rule requires
that the request being tested is first any state that is `!= Failed`,
then for any function `f`, when `f` is executed, the required state of
the request is `Failed`.

Prover run that confirms this: https://prover.certora.com/output/6199/82ed96aac5014cb9a7485fc3752fb399?anonymousKey=28c97adbbe14ead331dc8e4b8ed05e94528075a3

There's two options to go about this:

1. Either filter out all functions from the rule where the rule is
   vacuous (this is dangerous because we'd exclude those functions
   entirely from the rule)
2. Or, rewrite the rule such that the requirements are relaxed

This commit implements option 2.
Instead of requiring that the starting request state has to be `!=
Failed`, we simply assert that **if** it **was** not `Failed` and then
**is** `Failed`, the corresponding slot is either failed or free.

Prover run that passes: https://prover.certora.com/output/6199/16fa074bd23146e59c21964c98bbb3e0?anonymousKey=229d721cf35873bed5eae67696eed803ce75fd18
This commit is contained in:
r4bbit 2024-08-27 10:52:56 +02:00
parent 50e90b6816
commit 6d319c76b9
1 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
certora/specs/Marketplace.spec
View File

@ -230,12 +230,11 @@ rule slotIsFailedOrFreeIfRequestHasFailed(env e, method f) {
requireInvariant paidSlotAlwaysHasFinishedOrCancelledRequest(e, slotId); requireInvariant paidSlotAlwaysHasFinishedOrCancelledRequest(e, slotId);
require currentContract.requestState(e, currentContract.slots(e, slotId).requestId) != Marketplace.RequestState.Failed; Marketplace.RequestState requestStateBefore = currentContract.requestState(e, currentContract.slots(e, slotId).requestId);
f(e, args); f(e, args);
require currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Failed; Marketplace.RequestState requestAfter = currentContract.requestState(e, currentContract.slots(e, slotId).requestId);
assert currentContract.slotState(e, slotId) == Marketplace.SlotState.Failed || assert requestStateBefore != Marketplace.RequestState.Failed && requestAfter == Marketplace.RequestState.Failed => currentContract.slotState(e, slotId) == Marketplace.SlotState.Failed || currentContract.slotState(e, slotId) == Marketplace.SlotState.Free;
currentContract.slotState(e, slotId) == Marketplace.SlotState.Free;
} }