1. A property to check the initial balance of a new account

What should be the balance of a new address? Write a property to check that this is indeed the balance of a new address. You can write your property (or rule) in src/certora/spec.rs inside the function init_balance. We have already provided the right signature for this rule.

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

certoraRun confs/exercise1.conf

Hint

You’ll need to use require!(CONDITION, "address must not exists"); to ensure the address does not already exist.

Solution

solution_specs.rs

// Exercise 1
#[rule]
fn init_balance(e: Env, addr: Address) {
    // precondition macro
    certora::require!(!e.storage().persistent().has(&addr), "address must not exists");
    let balance = Token::balance(&e, addr);
    // use this macro to see additional information in the calltrace
    certora_print_i64!("value of balance is:", balance); 
    // postcondition macro
    certora::assert!(balance == 0);
}