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 should fix the bug of certora-cli not properly completing with non
zero exit codes on errors, which ultimately results in CI tasks to give
false positives.
* initial commit for splitting payouts
Collateral goes to slot's host address, while reward payouts go to the slot's host payoutAddress
* Add fillSlot overload to make payoutAddress "optional"
* add tests for payoutAddress
* add doc to patchFillSlotOverloads
* formatting
* remove optional payoutAddress parameter
* Move payoutAddress to freeSlot
- remove payoutAddress parameter from `fillSlot`
- remove `payoutAddress` from slot struct and storage
- add payoutAddress parameter to `freeSlot`, preventing the need for storage
* formatting
* update certora spec to match updated function signature
* Add withdrawAddress to withdrawFunds
- prevent erc20 msg.sender blacklisting
* Update tests for paying out to withdrawAddress
* formatting
* Add collateralRecipient
* refactor: change withdrawFunds and freeSlot overloads
- `withdrawFunds` now has an option withdrawRecipient parameter
- `freeSlot` now has two optional parameters: rewardRecipient, and collateralRecipient. Both or none must be specified.
* update certora spec for new sigs
This adds a rule to formally verify that the `SlotState` and
`RequestState` of any given `Slot` or `Request` does not change more
than once per function call.
Closes#129
This invariant ensures that the total supply of the used token in the
contract is always greater equal to the sum of all balances within the
token combined.
This commit adds CVL rule that formally verifies the state changes of
any given request in relation to the functions of the contract that can
cause them.
Closes#128
Rationale: subtracting 2000 from the provided gas seems
arbitrary, and doesn't provide any benefits. Whether
verify() fails with an out-of-gas error, or returns
'false', in both cases the proof is not verified.
Co-Authored-By: Balazs Komuves <bkomuves@gmail.com>
