parametric.rst

.. index::
   single: parametric rule
   single: rule; parametric

Parametric rules

General

A :term:`parametric rule` is a rule that uses a :cvl:`method f` parameter. Such a rule will be tested against all possible methods :cvl:`f`, including methods from other contracts in the :term:`scene`. It is possible to limit the methods tested, see :ref:`parametric-rules`.

Parametric rules can be used to verify properties of the changes in storage values. The template for such checks is:

rule parametricExample(method f) {
    // Get storage values before
    uint before = ...;
    ...

    // Function call
    env e;
    calldataarg args;
    f(e, args)

    // Get storage values after
    uint after = ...;
    ...

    // Assert property of the change, e.g.:
    assert after - before == ...;
}

The main differences between parametric rules and invariants are:

1. Invariants are also tested after the constructor.
2. Invariants are used to assert properties of the storage (between function calls), while parametric rules are used to assert properties of changes in the storage (caused by function calls).

ERC20 example

Here is a parametric rule example from the spec file :clink:`ERC20Full.spec</DEFI/ERC20/certora/specs/ERC20Full.spec>` -- a spec for an ERC20 implementation. The parametric rule :cvl:`onlyAllowedMethodsMayChangeBalance` asserts two things:

1. A user's balance can increase only by calls to :solidity:`mint`, :solidity:`transfer`, and :solidity:`transferFrom`.
2. A user's balance can decrease only by calls to :solidity:`burn`, :solidity:`transfer`, and :solidity:`transferFrom`.

It follows that all other functions do not change balances. The rule is shown below, with the lines for getting the storage value before and after the function call highlighted. The two helper functions used in the rule are explained below the rule.

.. cvlinclude:: ../../Examples/DEFI/ERC20/certora/specs/ERC20Full.spec
   :cvlobject: onlyAllowedMethodsMayChangeBalance
   :emphasize-lines: 8, 10
   :caption: :clink:`onlyAllowedMethodsMayChangeBalance</DEFI/ERC20/certora/specs/ERC20Full.spec>`

• The function :cvl:`canIncreaseBalance(f)` returns true if :cvl:`f` is one of the functions :solidity:`mint`, :solidity:`transfer`, or :solidity:`transferFrom`.
• Similarly, :cvl:`canDecreaseBalance(f)` returns true if :cvl:`f` is one of :solidity:`burn`, :solidity:`transfer`, or :solidity:`transferFrom`.

.. dropdown:: The helper functions :cvl:`canIncreaseBalance` and :cvl:`canDecreaseBalance`

   .. cvlinclude:: ../../Examples/DEFI/ERC20/certora/specs/ERC20Full.spec
      :lines: 50-58

.. seealso::

   There is more information about parametric rules in :ref:`parametric-rules`.