0. Warm up

Let’s make sure you are able to run Certora Sunbeam. Run the following:

cd projects/token/confs
certoraSorobanProver setup.conf

You should see an output like so:

INFO: Building from script ../certora_build.py

Connecting to server...

Job submitted to server

Manage your jobs at https://prover.certora.com
Follow your job and see verification results at <LINK>

Click on that link to see the report page generated by Certora Sunbeam. It will show you that a basic sanity check has passed, indicated by a green check mark next to “sanity” in the Rules list. You can see the set of Source Files that were used by clicking on the File Tree icon to the left of the Rules list. Now, click on the “satisfy” rule to display related information in the Call Trace panel that shows you the starting state and sequence of function calls that led to this outcome.

src/certora/spec.rs will show you the sanity rule we just ran. This rule simply calls Token::balance() and checks that the control reaches the cvlr_satisfy macro that follows. You can read more about the semantics of satisfy here.

Important

If you are not able to run certoraSorobanProver, see the Sunbeam Troubleshooting section in the Documentation.

Solution

solution_specs.rs

// Exercise 0
#[rule]
fn sanity(e: Env, addr: Address) {
    let balance = Token::balance(&e, addr);
    // Reachability check: is this satisfy reachable?
    cvlr_satisfy!(true);
}