.yaml
file describing the target contract and the properties that the macro should insert#macro <name>(<var1>, <var2>...);
annotation on the target contract, that instantiates all the properties from the corresponding .yaml
file.
Lets explore this with ERC20
as an example.ERC20
tokens. All ERC20
tokens must for example define a transferFrom
and totalSupply
functions, and many implementations will have a internal map from addresses to balances. We may want to check several properties of such tokens. For example:transferFrom(from, to, amount)
is called, the balance of the sender decreases by amount, and the balance of the receiver increases by amounttotalSupply
is always equal to the sum of the balancesvariables
section (lines 2-3) we list the variables that we expect the target contract to have. Note that in the actual contract the variables can have different names! We will see how this renaming happens in the next sectionproperties
section, we have a list of "annotation targets" and for each target the list of annotations that must be applied to this target. An annotation target can be a function signature, state variable name, or <contract>
which applies to the whole contract.msg:
is the human readable label that should be applied to the property and prop:
is the actual scribble annotation.totalSupply()
in the target contract, and insert #if_succeeds {:msg "Result is equal to sum of balances" $result == unchecked_sum(balances);
right above it:MyToken
contract.#macro erc20(_balances)
annotation in the docstring above the target contract. The macro invocation gives the macro name (erc20
) and it lists the actual names of all variables required in the variables
section of the macro definition.variables
section of the erc20
macro definition we mentioned a balances
variable.
Some properties declared in the erc20
macro definition also talk about a balances
variable. However MyToken
doesn't have a balances
state variable - instead it has a state variable named _balances
. By specifying erc20(_balances)
in the macro invocation, we are telling scribble to replace all occurances of balances
in the macro definition with _balances
.
Additionally note that the arguments of transferFrom
in the definition are named from
, to
and amount
. On the other hand in MyToken
these same arguments are named sender
, receiver
and value
. Scribble will automatically rename the function arguments of function properties when instrumenting the contract.--macro-path
command line options.
As of Scribble v0.6.3 we also ship a small standard library of macros which is searched in addition to the explicit --macro-path
location. The standard macro library is located under SCRIBBLE_INSTALL_PATH/stdlib
where SCRIBBLE_INSTALL_PATH
is the location where npm has installed the eth-scribble
package.