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.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 ****************************************************************** * 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