Vacuous rule in the documentation

CVL Support
1

Isn’t this rule defined in the documentation vacuous, since !contains(key)) will always be false whether the insert works or reverts, causing the precondition to always be false.

rule insertRevertConditions(uint key, uint value) {
    env e;
    insert@withrevert(e, key, value);
    bool succeeded = !lastReverted;

    assert (e.msg.value == 0 
        && value != 0
        && !contains(key))
        => succeeded;
}
2

Nice catch! the rule is indeed wrong, it should check the contains before the call to insert. However it is not vacuous as it does depend on the correctness of contains

1 Like
3

Yes, I thought the precondition as it is defined can never be true so the expression should be a tautology (not vacuous), but that is not the case. Thanks for the clarification.
As I understand now, the rule is wrong because if insert doesn’t add a value to the map, the rule succeeds while it fails when insert does add a value to the map.