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;
}
}