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
6ae0d85d4e