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 one being transferred to and from. Write another rule to encode the effect of transfer on some other address.

You can write these two properties in 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:

certoraRun confs/exercise2.conf

Solution

solution_specs.rs

// Exercise 2
#[rule]
fn transfer_is_correct(e: Env, to: Address, from: Address, amount: i64) {
    require!(
        e.storage().persistent().has(&from) && e.storage().persistent().has(&to) && to != from,
        "addresses exist and different"
    );
    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());
    certora::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) {
    require!(to != other && from != other, "addresses are all different");
    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());
    certora::assert!(balance_other_after == balance_other_before);
}