Specification of balance modifications.

[michael-emmi]

It would be nice to be able to say that balance cannot be changed arbitrarily by the given function.

$ cat a.sol && solc-verify.py a.sol 
pragma solidity ^0.5.0;

contract A {

    /// @notice modifies this(address).balance
    function f1() public payable { }

    /// @notice precondition address(this) != payee
    /// @notice modifies this(address).balance
    /// @notice modifies payee.balance
    function f2(address payable payee) public {
        payee.transfer(42);
    }
}
Error while running compiler, details:
Warning: This is a pre-release compiler version, please do not use it in production.

======= Converting to Boogie IVL =======

======= a.sol =======
Annotation:1:1: solc-verify error: Type is not callable
this(address).balance
^-----------^
Annotation:1:1: solc-verify error: Member "balance" not found or not visible after argument-dependent lookup in tuple().
this(address).balance
^-------------------^
a.sol:6:5: solc-verify error: Error while parsing annotation.
    function f1() public payable { }
    ^------------------------------^
Annotation:1:1: solc-verify error: Type is not callable
this(address).balance
^-----------^
Annotation:1:1: solc-verify error: Member "balance" not found or not visible after argument-dependent lookup in tuple().
this(address).balance
^-------------------^
a.sol:11:5: solc-verify error: Error while parsing annotation.
    function f2(address payable payee) public {
    ^ (Relevant source part starts here and spans across multiple lines).
a.sol:6:5: solc-verify error: Error(s) while processing annotation for node
    function f1() public payable { }
    ^------------------------------^
a.sol:11:5: solc-verify error: Error(s) while processing annotation for node
    function f2(address payable payee) public {
    ^ (Relevant source part starts here and spans across multiple lines).

[hajduakos]

Seems doable for simple cases (the syntax is actually address(this).balance instead of this(address).balance). I will try it on a branch soon.

[hajduakos]

The tricky part comes when there is an array of receivers and you want to specify that any of their balance can be modified (probably requires quantifiers).

[dddejan]

Another thing to consider is that the sender's balance is also going to be deduced by the gas amount after the transaction is completed. This could complicate things as we ignore gas consumption at the moment.

[hajduakos]

As discussed, we could have it with a warning that we are not considering balance modifications due to gas costs, miner rewards, etc.

[hajduakos]

Done with #70

[dddejan]

@michael-emmi please check and close issue if OK

[michael-emmi]

Works like a charm now!