Why assertion is used on this Smart Contract?

Question

contract Sharer {
    function sendHalf(address payable addr) public payable returns (uint balance) {
        require(msg.value % 2 == 0, "Even value required.");
        uint balanceBeforeTransfer = address(this).balance;
        addr.transfer(msg.value / 2);
        // Since transfer throws an exception on failure and
        // cannot call back here, there should be no way for us to
        // still have half of the money.
        assert(address(this).balance == balanceBeforeTransfer - msg.value / 2);
        return address(this).balance;
    }
}

For contract above, on which condition the assertion fails / address(this).balance is not decreased by (msg.value / 2)? Why we need assertion here?

Answer 1

The assertion is true, which is exactly why it's there. You use assert() to declare things that you think will always hold. If they turn out to be false, you have a bug in your contract.

An assertion is not just a fancy if. While it does perform a runtime check, it's also one of the ways to provide a target for formal verification. Tools such as the SMTChecker built into the Solidity compiler can detect bugs by trying to prove various statements about your code. The thing is - how can such a tool tell that the result you got is not the result you wanted? Documenting your assumptions with assertions is a very straightforward way to give the tool extra information needed to discern expected behavior from a buggy one.

Also, while the contract is simple now and it's easy to see that it won't fail, code does not stay simple forever. The condition is only true under the assumption that the contract has no other payable functions. Will you remember to revise this function every time when you add a payable function? What if the contract grows and the function is buried at the bottom of the file under several other functions? Most importantly - what about other people modifying the code in the future? Will they even notice this limitation? An assertion is a good way not to have to rely on anyone noticing this and turn it into an automated check.

Finally, the assertion is true but is it obvious? There are actually quite a few assumptions that go into it:

• Contract can receive ether only in a few specific ways:
  1. through a call of its payable function - sendHalf() is the only one here
  2. call of its receive() or fallback() function - there are none
  3. being the recipient of selfdestruct of another contract
  4. being the recipient of the ether mined in a block
• The callee of transfer() cannot call back sendHalf() because transfer() forwards only 2300 gas and an external call costs more.
• The callee of transfer() cannot execute selfdestruct because it costs 5000 gas.
• Reverts inside transfer() are not silenced in any way so even if the cost of selfdestruct changed the future to be <= 2300 gas, issuing it would terminate the execution anyway.
• Transactions on Ethereum are only executed sequentially and mined ether cannot be transferred in the middle of a contract execution.

There are enough assumptions here that the author of the code might simply not have been 100% certain that he did not miss some obscure corner case that might turn into a security hole. An assertion can be a simple and effective way to definitively exclude such a possibility.