Directives

%rk-assume

Description

This directive add one or many constraints to symbolic engine within current control flow path. RK87 will work with assumption that the given constraits most hold within current condition context.

Syntax

Single-line comment:

// %rk-assume <expr>;
// %rk-assume <expr>; <expr>;

Multi-line comment:

/** %rk-assume expr;
  * expr;
  * expr
  ********/

Example

Simple example:

pragma solidity ^0.4.25;

contract EToken {
    int256 my_money;
    function send_money(int256 a) public {
        int256 _current_money = my_money;
        /* %rk-assume _current_money >= 0 && _current_money <= 10 ; a > 0*/
        my_money += a;
        // %rk-assert my_money >= 0;
    }
}

More advanced example:

pragma solidity ^0.4.25;

contract EToken {
    int256 my_money;
    function send_money(int256 a, int256 b) public {
        int256 _current_money = my_money;
        if(b>=10) {
            /* %rk-assume
            * _current_money >= 0 && _current_money <= 10;
            * a > 0;
            * a < 100
            ***********/
        }
        
        if(b==3 || b==13) {
            my_money += a;
        }
        // %rk-assert my_money >= 0;
    }
}

%rk-for-all

Description

This directive add a universal quantification assumption.

Syntax

Single-line comment:

// %rk-for-all <type> <var>: <expr>

Multi-line comment:

/** %rk-for-all <type> <var>: <expr>
  ********/

Example

Simple example:

pragma solidity ^0.4.25;
contract EToken {
    mapping(address=>int256) balance;
    function send_money(address to, int256 a) public {
        // %rk-assume a > 0
        // %rk-for-all address x: balance[x] <= 1000
        // %rk-eval int256 _current_sender_balance = balance[msg.sender];
        // %rk-eval int256 _current_receiver_balance = balance[to];
        balance[msg.sender] -= a;
        balance[to] += a;
        // %rk-assert balance[to] >= _current_receiver_balance
    }
}

%rk-assert

Description

This directive add one or many goals to symbolic engine within current control flow path. RK87 will try to find counterexample that invalidate each goal, show that it’s always valid or timeout if the goal is too complex for the internal symbolic engine.

Syntax

Single-line comment:

// %rk-assert <expr>
// %rk-assert [[assert name]] <expr>
// %rk-assert <expr1> <expr2>
// %rk-assert [[assert name 1]] <expr1> [[assert name 2]] <expr2>

Multi-line comment:

/** %rk-assume expr;
  * expr;
  * expr
  ********/

Example

Simple example:

pragma solidity ^0.4.25;

contract EToken {
    int256 my_money;
    function send_money(int256 a) public {
        int256 _current_money = my_money;
        /* %rk-assume _current_money >= 0 && _current_money <= 10 ; a > 0*/
        my_money += a;
        // %rk-assert my_money >= 0;
    }
}

Assertions can be named:

pragma solidity ^0.4.25;
contract EToken {
    int256 my_money;
    function send_money(int256 a) public {
        int256 _current_money = my_money;
        /* %rk-assume _current_money >= 0 && _current_money <= 10 ; a > 0*/
        my_money += a;
        // %rk-assert [[money must not become negative]] my_money >= 0 [[must not overflow]] my_money >= _current_money
    }
}

You can use multiline comment syntax for better reading:

pragma solidity ^0.4.25;
contract EToken {
    int256 my_money;
    function send_money(int256 a) public {
        int256 _current_money = my_money;
        /* %rk-assume _current_money >= 0 && _current_money <= 10 ; a > 0*/
        my_money += a;
        /* %rk-assert
        * [[money must not become negative]] my_money >= 0
        * [[must not overflow]] my_money >= _current_money
        ***/
    }
}

%rk-eval

Description

This directive inject solidity code that will not be checked for errors. The given code will only be executed within rk87.

Syntax

Single-line comment:

// %rk-eval <expr>;
// %rk-eval <expr>; <expr>;

Multi-line comment:

/** %rk-eval expr;
  * expr;
  * expr
  ********/

Example

pragma solidity ^0.4.25;

contract EToken {
    int256 my_money;
    function send_money(int256 a) public {
        // %rk-eval int256 _current_money = my_money;
        /* %rk-assume _current_money >= 0 && _current_money <= 10 ; a > 0*/
        my_money += a;
        // %rk-assert my_money >= 0;
    }
}

%rk-check

Description

This directive add a universal quantification assumption.

Syntax

You can place %rk-check <name> anywhere within a method’s docblock to enable specific RK87’s check on that method.

Example

Simple example:

pragma solidity ^0.4.25;
contract EToken {
    mapping(address=>uint256) balance;
    /**
     * %rk-check no_overflow
     **/
    function send_money(address to, uint256 a) public {
        balance[msg.sender] -= a;
        balance[to] += a;
    }
}