Rule Sanity Checks (Solana)

The rule_sanity option enables automatic checks that warn about potential problems in the specification. Currently the only supported sanity check is the one called vacuity.

Note

This is the documentation for the sanity checks for Solana. If you are looking for the Sanity checks for Solidity, please refer to this section.

The --rule_sanity option can be set to none or basic and controls whether the sanity checks should be executed:

• With --rule_sanity none or without passing --rule_sanity, no sanity check is performed.

• With --rule_sanity basic or simply --rule_sanity without a mode, the sanity checks are executed.

Each sanity check adds a new child node to every rule in the rule tree of the rule report. Each check transforms the the original program into a variant where cvlr_satisfy!(true) is inserted at the end of the program, and all calls to cvlr_assert are removed. If the sanity check fails on a rule, the sanity node in the rule report is displayed as a yellow icon, and its status propagates to the parent rule’s node (see below for an example).

The remainder of this document describes the vacuity check in detail.

Vacuity checks

The vacuity sanity check ensures that even when ignoring all the user-provided assertions, the end of the rule is reachable. This check ensures that the combination of cvlr_assume! statements and implicit panics are not contradictory. Rules that are satisfied due to contradictory assumptions are called vacuous. Since vacuous rules do not actually check any assertion, they are almost certainly incorrect.

For example, the following rule is vacuous (and is flagged by the vacuity check):

#[rule]
pub fn rule_vacuity_test_expect_sanity_failure() {
    let amount: u64 = nondet();

    cvlr_assume!(amount >= 2);
    cvlr_assume!(amount <= 1);
    cvlr_assert!(amount == 1); 
    // Expect a sanity failure here as the assumptions are conflicting
}

Since the two assumes amount >= 2 and amount <= 1 contradict each other, this rule always passes, regardless of the content of the assertion. This is an example of a vacuous rule — one that passes only because the preconditions are contradictory.

In the rule report, a vacuity check adds a node called rule_not_vacuous_cvlr to each rule. For example, see how the rule rule_vacuity_test_expect_sanity_failure from above is reported as failing sanity, as rule_not_vacuous_cvlr fails. Below you see an example of a rule without the contradicting assumes that does not fail vacuity.