2. Effect of transfer on the balances of various addresses

What should be the effect of a transfer of amount between two addresses, to and from? Write a rule to capture the correct behavior. Whose balance should change by what amount?

Note that transfer should not affect any address other than the ones specified in the transfer. Write another rule to verify that transfer has no effect on some other address.

You can write these two properties in the existing rules transfer_is_correct and transfer_no_effect_on_other in src/certora/spec.rs.

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

certoraSorobanProver exercise2.conf

from the projects/token/confs directory.

Solution

solution_specs.rs

// Exercise 2
#[rule]
fn transfer_is_correct(e: Env, to: Address, from: Address, amount: i64) {
    let balance_from_before = Token::balance(&e, from.clone());
    let balance_to_before = Token::balance(&e, to.clone());
    Token::transfer(&e, from.clone(), to.clone(), amount);
    let balance_from_after = Token::balance(&e, from.clone());
    let balance_to_after = Token::balance(&e, to.clone());
    cvlr_assert!(
        (balance_to_after == balance_to_before + amount)
            && (balance_from_after == balance_from_before - amount)
    );
}

// Exercise 2
#[rule]
fn transfer_no_effect_on_other(e: Env, amount: i64, from: Address, to: Address, other: Address) {
    cvlr_assume!(to != other && from != other);
    let balance_other_before = Token::balance(&e, other.clone());
    Token::transfer(&e, from.clone(), to.clone(), amount);
    let balance_other_after = Token::balance(&e, other.clone());
    cvlr_assert!(balance_other_after == balance_other_before);
}