Spurious CEx for both Halmos and hevm

[msooseth]

Describe the bug

This code:

import {Test} from "forge-std/Test.sol";

contract MyContract is Test {
  mapping (uint => uint) balances;
  function setUp() public {
    balances[0xfaaaaaffafafafafaaaaa472134] = 50;
  }
  function prove_keccak_wrong(uint amt) public view {
    bytes32 hash = keccak256(abi.encodePacked(amt));
    uint balance = balances[uint(hash)];
    assert(balance != 50);
  }
}

Will find a CEx with latest halmos:

$ halmos --function "prove_keccak_wrong"
[⠒] Compiling...
No files changed, compilation skipped

Running 1 tests for src/contract-keccak.sol:MyContract
Counterexample:
    p_amt_uint256_928e027_00 = 0x00
[FAIL] prove_keccak_wrong(uint256) (paths: 2, time: 0.12s, bounds: [])
Symbolic test result: 0 passed; 1 failed; time: 0.13s

The CEx is wrong. The issue is that due to uninterpreted function of Keccak, our systems both imagine that keccak(0) is 0xfaaaaaffafafafafaaaaa472134. It's hard to fix this, and it can unfortunately be triggered in a real-world scenario. If you look at the issue as tracked by us below, it starts with a real-world contract, that actually triggers this issue. The contract I wrote above this text is a minimized version of the problem.

Our issue tracker for this is here: argotorg/hevm#770 (comment)

To Reproduce
Reproducible as per above. I compiled with forge build --ast. Should work as-is. Let me know if it doesn't!

Environment:

• OS: Linux
• Python version: Python 3.13.5
• Halmos and other dependency versions: installed via uv tool install --python 3.12 halmos, just today. halmos --version says: halmos 0.3.0

Additional context
It would be interesting to brainstorm how to solve this issue. It's non-trivial, I think, and it seems like both of our tools fail the same way :S

Let me know what you think! Would be nice to solve it, perhaps together :)

[msooseth]

PS: also, congrats on the 0.3.0 release, it looks and works awesome!

[0xkarmacoma]

Yeah we have generally the same issue with things like signatures too for instance. I wouldn't say that this is a spurious CEx, even if the actual value is wrong. If we returned PASS, it would be saying that there is no amt that hashes to 0xfaaaaaffafafafafaaaaa472134. If I cook up an example where I know the pre-image of the hash, that's obviously not true.

So the way I see it, we are responding that yes in fact there may be a pre-image for 0xfaaaaaffafafafafaaaaa472134, but since we don't know what it is we say "0 I guess", which is a little weird.

So we could say well that's not cool returning CEx with clearly wrong values, so maybe we should validate the model first. Trying to run again with the concrete values from the model would show that 0 does not hash to 0xfaaaaaffafafafafaaaaa472134, but now we're back to square one. There may be a model (or not!), but we can't know for.

Zooming out, I guess the question is whether we're trying to verify the program or find bugs:

• in the context of verification, I think this is sort of fine ("we can't verify the program because of the possibility of a pre-image")
• in the context of bug finding, this is frustrating because we're not able to actually produce values that demonstrate the bug

Maybe we should squelch by default (only produce valid bugs), unless you pass a --strict flag or something like that, where you accept potentially invalid models if safety can not be guaranteed. WDYT?

[msooseth]

That's a good analysis. Returning PASS would be wrong without at least some warning/option flag. In the case that we had, argotorg/hevm#770 it was really annoying, because the "mistake" was not so obvious, the input domain was only 2^24, an int24 and the keccak store&lookup of course was "hidden" by a bunch of code.

You do raise good points. The issue is that when the keccak() is not so trivial, it's hard to try to explain to the user that hey, we are not sure, we can't construct an input, but there may be an input to this expression that keccak's to xyz: [expr]. So it's a bit tricky. I guess some user-digestible explanation could be helpful.

Not the most important issue of all, that's for sure :) It was only a bit of a revelation I had after digging for days why that complicated contract was giving us an incorrect CEx (found many issues while digging, so it wasn't a waste). I just wanted to share :)

PS: We are planning to validate our CEx-es soon. We will definitely bump into this issue when we do.

[gustavo-grieco]

I think showing the user a clear warning is essential, specially when doing verification. For the upcoming echidna PR on symbolic execution, when running in verification mode, the user will see that a final test is "passed" instead of "verified" when an invalid CEX is found.