Specification language¶

VerX specification syntax is similar to Solidity’s syntax for expressions, with a few extension to support temporal logic. A property is defined with the property keyword and looks like

property property_name {
    always(property-formula);
    (extra-predicate-1);
    (extra-predicate-2);
    ...
    (extra-predicate-n);
}

The body of the property is expected to contain a list of Boolean expressions. The first expression is the property formula. If the property formula evaluates to false in some execution, then the property is violated. If the formula evaluates to true in all executions, then the property holds. The remaining Boolean expressions are extra predicates used to prove that the property formula holds. These expression must be enumerated in parenthesis,

Contracts are referenced by their name e.g A, B, C. As standard, contract fields are referenced with the . operator, e.g. A.x, B.y, C.z. Contract name without field access is equal to the address of the contract. Thus, the formula A.x == B means that the x field of A equals the address of the B contract.

LTL keywords¶

We support a part of the canonical safety fragment of linear temporal logic.

Syntax	Description	Note
`property name { always(formula); }`	property declaration	must include `always`
`! formula`	logical negation
`formula && formula`	logical and
`formula \|\| formula`	logical or
`formula ==> formula`	logical implication
`once(formula)`	formula holds or held	must be nested inside always
`prev(storageref)`	previous value	storage reference required
`contract.field`	storage reference
`expression + expression`	infix syntax	parenthesis might be needed
`(expression)`	grouping	use to fix priorities
`FUNCTION`	current function name	refers to top-level transaction
`Contract.function()`	function name literal
`Contract.function()[index]`	function argument	index must be constant
`BALANCE(Contract)`	contract balance
`msg.sender`	message sender
`now`	current time

Prev operator¶

prev(A.x) refers to the previous value of variable x in contract A. That is, the operator returns the variable’s value in the state prior to the transaction. Note that in the block where the contract is deployed, prev(A.a) equals A.a, since there is no prior block where A.a is defined.

Example.

contract A {
    uint a = 0;
    function foo() public {
        a = a + 1;
    }
}

A.a	0	1	2	3	4	5
(prev(A.a) + 1) == A.a	F	T	T	T	T	T

Always operator¶

always(formula) is true in a state if all subsequent states satisfy formula:

A.a	0	1	2	3	4	5
always(A.a > 2)	F	F	F	T	T	T

Once operator¶

once(formula) is true if formula holds in the current state or any previous states.

A.a	0	1	2	3	4	5
once(A.a == 2)	F	F	T	T	T	T

Referring to functions¶

The top-level function called in the current transaction can be referred to with the FUNCTION keyword. This keyword is expected to appear in a equality/non-equality Boolean expression where it is compared with an expression of the form of Contract.function_name(<list of canonical type names>), e.g. FUNCTION == A.foo(address). (See https://solidity.readthedocs.io/en/latest/abi-spec.html#function-selector)

Referring to function arguments¶

An argument of a function can be referred to with the Contract.function_name(<list of canonical type names>)[index] syntax. The index must be a constant, and is zero-based, i.e., the first index is 0. For example, the formula

always(FUNCTION == A.foo(address) ==> (A.foo(address)[0] == msg.sender))

states that the A.foo(address) function is always called with the message sender as a first argument.

Referring to balance¶

A contract’s balance can be referred to with the BALANCE(ContractName) expression, e.g. BALANCE(A) == prev(BALANCE(A)).

Extra free variables¶

A property can include free variables in order to specify that something holds for all values of these variables. The free variables must be declared as arguments to the property, e.g,

property all_balances_are_zero(X) {
    always(A.balance[X] == 0);
}

This property holds if all balances in the A contract are always 0.

Referring to enumeration elements¶

To refer to an enumeration element just use the corresponding integer value. For example, given the contract

contract Escrow {
    enum State { OPEN, SUCCESS, REFUND }
    State state;
    ...
}

we refer to OPEN, SUCCESS, and REFUND with the integers 0, 1, and 2 respectively.