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 .. code-block:: solidity 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 | +=============================================+=======================+=================================+ | :code:`property name { always(formula); }` | property declaration | must include ``always`` | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`! formula` | logical negation | | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`formula && formula` | logical and | | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`formula || formula` | logical or | | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`formula ==> formula` | logical implication | | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`once(formula)` | formula holds or held | must be nested inside always | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`prev(storageref)` | previous value | storage reference required | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`contract.field` | storage reference | | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`expression + expression` | infix syntax | parenthesis might be needed | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`(expression)` | grouping | use to fix priorities | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`FUNCTION` | current function name | refers to top-level transaction | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`Contract.function()` | function name literal | | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`Contract.function()[index]` | function argument | index must be constant | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`BALANCE(Contract)` | contract balance | | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`msg.sender` | message sender | | +---------------------------------------------+-----------------------+---------------------------------+ | :code:`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. .. code-block:: solidity 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()``, 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()[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 .. code-block:: solidity contract Escrow { enum State { OPEN, SUCCESS, REFUND } State state; ... } we refer to ``OPEN``, ``SUCCESS``, and ``REFUND`` with the integers ``0``, ``1``, and ``2`` respectively.