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!(Token::balance(&e, from.clone()) < amount);
    Token::transfer(&e, from.clone(), to.clone(), amount);
    // Should not reach the next line due to expected revert in transfer(). Rule fails iff it can be reached.
    cvlr_assert!(false);
}