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

What should be the balance of a new address? Write a property (rule) to check that the value you expect is indeed the balance of a new address. You can write your 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:

certoraSorobanProver exercise1.conf

from the projects/token/confs directory.

Hint

You’ll need to use cvlr_assume!(<boolean>, "address must not exist"); to ensure the address does not already exist. And cvlr_assert!(<boolean>); is needed to verify the expected state.

Solution

solution_specs.rs

// Exercise 1
#[rule]
fn init_balance(e: Env, addr: Address) {
    // precondition macro
    cvlr_assume!(!e.storage().persistent().has(&addr));
    let balance = Token::balance(&e, addr);
    // use this macro to see additional information in the calltrace
    clog!(balance);
    // postcondition macro
    cvlr_assert!(balance == 0);
}