How to avoid Certora havocking on payable.transfer function


Hi, I am verifying a function using Certora and in that function there is a line

payable(msg.sender).transfer(ethBal)

It looks Certora doesn’t know how to execute that (which is surprising since this is a built-in function on payable type), hence it havocked the call.

Given the transfer is a built-in function on payable. How can we avoid the havocking?
A related question is if it’s possible to prevent Certora havocking on address.call{value: 0}(data)?

Thank you

I have the same problem with this function:

    function withdraw(uint amount) public {
        require(amount <= address(this).balance);

        (bool succ,) = msg.sender.call{value: amount}("");
        require(succ);	
    }

I am attempting to prove that the value of address(this).balance before the function call is expected to be equal to the sum of address(this).balance after the call and amount . However, balanceAfter exceeds balanceBefore after the havoc.

This is the link to the output:

https://prover.certora.com/output/49230/4d2abda9829e451f84bbaf6387d62497?anonymousKey=367da435adeeab915758463a9998bb1a0151a166

Because of the nature of low-level calls (you can do too many things with them) we havoc it (changing random variables to cause a violation) and raise some kind of a flag that you should be especially careful here. We don’t have a built-in solution yet. If you want to get rid of havocs, you can harness this call with the following steps (approximately):

  1. create a simple Receiver.sol contract
pragma solidity >=0.8.9;

contract Receiver {
    fallback() external payable { }

    function sendTo() external payable returns (bool) { return true; }

    receive() external payable { }
}
  1. add its path to your script/command you use to run the tool
  2. change low-level call in your contract from
    (bool succ,) = msg.sender.call{value: amount}("");
    to
    (bool succ) = Receiver(payable(msg.sender)).sendTo{value: amount}();
  3. add dispatcher summarization to your spec:
    function _.sendTo() external => DISPATCHER(true); (CVL 2 version of code)

You can use another contract with more complicated logic upon a call to mimic this behavior. It’s just a simple example

Thank you for your answer. Is it currently impossible for the tool to anticipate some post-call outcomes, considering that random code execution may occur, while ensuring properties such as the contract balance not increasing? It seems that several cases might be overlooked by providing an implementation of the function/contract to call.

Unfortunately, no. Not sure why, but I guess it’s a universal solution because different systems may require different settings of havocs.
You can find more info about what havocs are applied (It’s about methods block, but this is what havocs are doing): The Methods Block — Certora Prover Documentation 0.0 documentation

Instead of my previous solution, also try to add --settings -optimisticFallback=true, but it isn’t always helping. Not sure about the conditions when it works or not.