This documentation has been moved to https://docs.certora.com/
The Anatomy of a Specification
A specification file is made up of several parts, each of which serves some purpose to interact with a contract or refine specifications in some way. The following shows an overview of the different parts of a specification file.
******************************************************************
* IMPORTS/SETUP *
******************************************************************
methods {
some_function_from_the_contract(address) returns (uint256)
}
******************************************************************
* USEFUL CONSTRUCTS. *
******************************************************************
// advanced use for SMT speedup with ghosts
sort MyUninterpretedSort;
// uninterpreted functions, useful for describing contract state
ghost myGhostFunction(uint256, address) returns bool {
axiom forall uint256 n. myGhostFunction(n, 0x0) == false;
}
// a way to interact with state changes in the contract via storage
// reads and writes
hook Sstore my_storage_mapping[KEY address key] uint256 value STORAGE {
havoc myGhostFunction assuming myGhostFunction@new(value, key);
}
// encapsulation of some commonly reused computation
function myCVLFunction(uint256 x, uint256 y) returns uint256 {
if (x > y) {
return x - y;
} else {
return y - x;
}
}
******************************************************************
* MEAT AND POTATOES: *
******************************************************************
// the basic unit of a spec: the rule is how we actually specify
// behavior, typically by
// 1. making some assumptions on "unconstrained" variables
// 2. invoking a contract function
// 3. making some assertion about the result of that function
rule my_rule(address a) {
require a != owner();
some_function_from_the_contract(a);
assert lastReverted;
}
// like super-rules, these automatically generate a base-case
// and inductive case for inductive invariants (rules are only
// really equipped to handle the inductive case)
invariant address_zero_gets_nothing_ever()
some_function_from_the_contract(0) == 0