0. Warm up

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

cd meridian2024-workshop
certoraRun confs/setup.conf

You should see an output like so:

INFO: Executing build process...
Executing:  cargo build --target=wasm32-unknown-unknown --release  --features cvt

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. You can see the Source Files on the report page. There is also a Call Trace that shows you what sequence of function calls 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 satisfy statement that follows. You can read more about satisfy here.

Important

If you are not able to run certoraRun, 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?
    cvt::satisfy!(true);
}