5. Assessing your specs through mutation testing

How do you know if your rules are good enough to catch potential bugs? One technique for assessing the quality of a specification is called “mutation testing”. Small modifications (mutations) are intentionally made, one at a time, in the contract source code to cause logic faults. The modified code is checked using your existing rules. It is important that your rules pass with the original contract code before applying any mutations so that you can safely draw conclusions from the mutation tests. With a mutation in the code, verification will fail if the coverage of your rule set is good enough to catch the fault. If verification still passes, that likely means your rules have a gap that must be addressed.

We have provided 3 hand-written mutants in src/certora/mutants. Copy them one at a time to src/ and rename them to lib.rs to replace the original src/lib.rs. Then run the rules you wrote above for transfer on these mutants. Are they caught?

Can you detect what the mutation was, for each mutant? You can see the solution in solutions/bugs-in-mutants.md.

Note that there are other ways to assess the quality of your rule. You can mutate the rule to see if it is vacuous, and you can check if the rule is a tautology.

Mutant 1. Solution

The bug is that the value read when the addr key is not present in storage is 1 but it should be 0.

pub fn read_balance(e: &Env, addr: &Address) -> i64 {
    e.storage().persistent().get(&addr).unwrap_or(1)
}

Mutant 2. Solution

The bug is that transfer calls spend_balance twice instead of calling it once followed by a receive_balance.

    pub fn transfer(e: &Env, from: Address, to: Address, amount: i64) {
        from.require_auth();
        check_nonnegative_amount(amount);
        spend_balance(&e, from.clone(), amount);
        spend_balance(&e, to.clone(), amount);
    }

Mutant 3. Solution

The bug is that transfer calls spend_balance(&e, from.clone(), amount + 1); instead of spend_balance(&e, from.clone(), amount);.

    pub fn transfer(e: &Env, from: Address, to: Address, amount: i64) {
        from.require_auth();
        check_nonnegative_amount(amount);
        spend_balance(&e, from.clone(), amount + 1);
        receive_balance(&e, to.clone(), amount);
    }