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
// Exercise 0
#[rule]
fn sanity(e: Env, addr: Address) {
let balance = Token::balance(&e, addr);
// Reachability check: is this satisfy reachable?
certora::satisfy!(true);
}