6ae0d85d4e
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 |
||
|---|---|---|
| .. | ||
| confs | ||
| harness | ||
| helpers | ||
| specs | ||