3. transfer under insufficient funds

If from does not have sufficient balance, transfer of funds should not succeed. Write a rule to capture this behavior in the function transfer_fails_if_low_balance.

Once you have written the rule, you can run Certora Sunbeam to check it by running:

certoraSorobanProver exercise3.conf

from the projects/token/confs directory.

Solution

solution_specs.rs

// Exercise 3
#[rule]
fn transfer_fails_if_low_balance(e: Env, to: Address, from: Address, amount: i64) {
    cvlr_assume!(
        e.storage().persistent().has(&from)
            && e.storage().persistent().has(&to)
            && to != from
            && Token::balance(&e, from.clone()) < amount);
    Token::transfer(&e, from.clone(), to.clone(), amount);
    // should not reach and therefore rule must pass
    cvlr_assert!(false);
}