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:

certoraRun confs/exercise3.conf

Solution

solution_specs.rs

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