Echidna is not able to break a property using `receive() external payable`

[Jaime-Iglesias]

So I think I've found something mildly interesting with Echidna (1.7.3 for now - would need to try with 2.0 ) and it's that it doesn't seem capable of breaking a property when there is a receive() external payable BUT if we change that for a fallback() external payable it is capable of it.

So I wonder:

• Is this known behavior?
• If it is, why does this happen?

The only reason that I can imagine for this to happen is that Echidna does not send empty calldata, since the main difference between receive() and fallback() is that the first is ONLY executed on empty calldata and the later is executed with the selector does not match or if there is no data and no receive() .

to replicate this behaviour you guys can try:

// SPDX-License-Identifier: MIT
pragma solidity ^0.6.0;

import './SafeMath.sol';

contract Fallback {

  using SafeMath for uint256;
  mapping(address => uint) public contributions;
  address payable public owner;

  constructor() public {
    owner = msg.sender;
    contributions[msg.sender] = 1000 * (1 ether);
  }

  modifier onlyOwner {
        require(
            msg.sender == owner,
            "caller is not the owner"
        );
        _;
    }

  function contribute() public payable {
    require(msg.value < 0.001 ether);
    contributions[msg.sender] += msg.value;
    if(contributions[msg.sender] > contributions[owner]) {
      owner = msg.sender;
    }
  }

  function getContribution() public view returns (uint) {
    return contributions[msg.sender];
  }

  function withdraw() public onlyOwner {
    owner.transfer(address(this).balance);
  }

  // Changing this for a fallback() would allow Echidna to break the property
  receive() external payable {
    require(msg.value > 0 && contributions[msg.sender] > 0);
    owner = msg.sender;
  }
}

And defining the following property:

// SPDX-License-Identifier: MIT
pragma solidity ^0.6.0;

import './Fallback.sol';

contract TestFallback is Fallback {

    constructor() Fallback() public payable {}

    // assuming the initial balance of the contract is 1 ETH
    function echidna_test_balance() public returns (bool) {
        return address(this).balance >= 1;
    }
}