hevm: unexpected counterexample

[d-xo]

When I try to prove the following spec:

constructor of Simple
interface constructor()

creates

  mapping (uint=>uint) store := []

behaviour set of Simple
interface set(uint x, uint y)

storage

  store[x] => y

returns y

Against the following contract:

// SPDX-License-Identifier: AGPL3+
pragma solidity ^0.8.6;

contract Simple {
    mapping(uint=>uint) public store;

    function set(uint x, uint y) external payable returns (uint) {
        store[x] = y;
        return y;
    }
}

I get:

checking postcondition...
Calldata:
0x1ab06ee5ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
Caller:
0x0000000000000000000000000000000000000000
Callvalue:
0
Failed to prove set(Pass)

and I'm not sure why, given that the following two tests pass:

// SPDX-License-Identifier: AGPL3+
pragma solidity ^0.8.6;

import {DSTest} from "ds-test/test.sol";
import {Simple} from "./simple.sol";

contract Test is DSTest {
    Simple simple = new Simple();

    function testCex() public {
        (bool ok, bytes memory ret) = address(simple).call(hex'1ab06ee5fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7fffffffffffff7ffffffffffffffffffffffffffffffffffffffffffffffffff');
        assertTrue(ok);

        uint x = uint(bytes32(hex'fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7'));
        uint y = uint(bytes32(hex'fffffffffffff7ffffffffffffffffffffffffffffffffffffffffffffffffff'));
        assertEq(simple.store(x), y);

        uint out = abi.decode(ret, (uint));
        assertEq(out, y);
    }

    function proveSet(uint x, uint y) public {
        uint ret = simple.set(x, y);

        assertEq(simple.store(x), y);
        assertEq(ret, y);
    }
}

[rdotterer09]

sorry not a coder and I don't understand, what do I need to do?

[zoep]

This now works (modulo some minor changes to actually match the spec with the code):

constructor of Simple
interface constructor()

iff
   CALLVALUE == 0

creates

  mapping (uint=>uint) store := []

behaviour set of Simple
interface set(uint x, uint y)

storage

  store[x] => y

returns y

// SPDX-License-Identifier: AGPL3+
pragma solidity ^0.8.6;

contract Simple {
    mapping(uint=>uint) store;

    function set(uint x, uint y) external payable returns (uint) {
        store[x] = y;
        return y;
    }
}