Specification language

Extended Solidity language. The property is defined with property keyword. The body of the property is expected to contain list of boolean expression. First boolean expression in a list - the checked predicate. Evaluation of this predicate to False is equal to property being violated. All bool expression in property body are used to capture the contract storage detail in a form of constraint.

Contracts are referenced by their name e.g A, B. Referencing a variable in the contract done with `.` operation e.g. A.b, A.a, B.x . Contract name without field access is equal to the address of the contract, thus predicate (A.b == B); will capture the equality of b variable in the contract A to the address of contract B.

LTL keywords.

We support following ltl function: prev(StorageRef) -> StorageRef, always(bool)->bool, once(bool)->bool. Prev function: prev(A.a) will reference the previous value of variable a in contract A. That is intuitively a reference to the variable prior to the execution of transaction. Note that for the first block after the deployment the predicate prev(A.a) == A.a is always evaluated to True.

Contracts source code

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 T T T T T T

Always function

always(A.a == 5)

always(foo) will be true until in the execution trace appears the block where the foo could be evaluated to False. Then the evaluation of always(foo) will stay False for any further state in the trace.

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

Once function

once(A.a == 5)

once(foo) will be False until in the execution trace appears the block where the foo could be evaluated to True. Then the evaluation of once(foo) will stay True for any further state in the trace. once(foo) in equivalent to !(always(!foo))

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

Function referencing

The function can be referenced with FUNCTION keyword. This keyword is expected to appear in a equality/inequality boolean expression where the other part is in a form of Contract.function_name(<list of canonical type names>) e.g. FUNCTION==A.foo(uint x). | https://solidity.readthedocs.io/en/latest/abi-spec.html#function-selector

Balance referencing

The balance can be referenced with BALANCE(ContractName) function. E.g. BALANCE(A) == prev(BALANCE(A))