Echidna模糊测试中ReceiveEther合约断言失败求助

你的断言assert(address(this).balance == amount);无法通过的核心问题是合约余额会累计所有转入的以太，而你的逻辑错误地认为每次调用receiveEther后，合约余额仅等于本次转入的msg.value。

测试失败的具体场景 #

从Echidna给出的调用序列可以清晰看到问题：

1. 第一次调用receiveEther()并转入0x1（1 wei），此时合约余额为1 wei，断言成立（1 wei == 1 wei）。
2. 第二次调用receiveEther()时，合约余额已经是第一次转入的1 wei（本次调用未额外转入以太，msg.value为0），此时断言要求1 wei == 0 wei，显然不成立，触发Panic(1)断言失败。

代码逻辑修正 #

根据你的实际需求，有两种常见修复方向：

1. 验证每次调用的余额增量正确

如果你的意图是确保每次转入的以太都正确计入合约余额，应该验证余额的变化量等于本次的msg.value：

contract ReceiveEther {
    uint256 public lastBalance;

    constructor() payable {}

    function receiveEther() public payable {
        uint256 amount = msg.value;
        uint256 currentBalance = address(this).balance;
        // 断言余额增量等于本次转入的以太
        assert(currentBalance == lastBalance + amount);
        lastBalance = currentBalance;
    }
}

2. 限制合约仅能接收一次以太

如果你的原本需求是合约只能接收一次以太，需要添加状态变量控制调用次数：

contract ReceiveEther {
    bool public hasReceived;

    constructor() payable {}

    function receiveEther() public payable {
        // 确保只能调用一次
        require(!hasReceived, "Ether already received");
        uint256 amount = msg.value;
        assert(address(this).balance == amount);
        hasReceived = true;
    }
}

额外说明 #

Echidna的模糊测试会自动生成多种调用序列来尝试打破断言，这次的两次调用场景正好暴露了你代码中未考虑余额累计的逻辑漏洞，这也是模糊测试的核心价值——找到人工容易忽略的边界场景。

内容的提问来源于stack exchange，提问作者최성훈