Vacuity refers to the state where we have a spec reported to be correct by the Prover, even for assertions that are obviously wrong. To be more precise, an assertion in the spec is effectively not checked because no input satisfies all requirements defined by the spec.
An obvious example of vacuity is the following rule:
No input x ever satisfies x != x, but the assert false is expected to trigger a failure. The vacuity of the require statement implies our assertion is not reachable, thus the rule is proven.
Vacuity is problematic because it indicates that the spec itself is wrong. Usually, vacuity is not as blatantly visible as in the above example, and thus we should take precautions to avoid writing vacuous specs.
Basic vacuity checking
Run the certora-cli with the following additional option: --rule_sanity to run a basic vacuity check. This option will instruct the tool to prove each rule twice: First time with the original spec, Second time with all assertions removed, and a single assert false statement in the end instead. If the second run of the rule does not fail, then a successful result of the original run is meaningless.
Below we present a few examples of vacuous specs.
Raw arguments (soon to be solved!)
The calldataarg type represents the full byte array passed as "calldata" to the EVM bytecode. It includes, in particular, the 4-byte sighash used by the ABI specification to identify the high-level function executed. Therefore, the following spec will pass vacuously:
The spec writer intended to check that foo() reverted if bar() returns true. But since bar() appears before lastReverted, it means lastReverted refers to whether bar() reverted or not. A corrected version of the spec should like this: