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
// 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
cvt::assert!(false);
}