WARNING:halmos:path.append(false) in Damn Vulnerable Defi - NaiveReceiver.t.sol

[karmacoma-eth]

Describe the bug

As reported by https://t.me/c/1815219512/2277 and easily reproducible. We get the following warnings during the execution of setUp():

WARNING:halmos:path.append(false)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:halmos:path.append(false)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)

With some extra debug info:

Running 1 tests for test/naive-receiver/NaiveReceiver.t.sol:NaiveReceiverChallenge
Constructor trace:
    CREATE NaiveReceiverChallenge::<0 bytes of initcode>
    ↩ RETURN <20027 bytes of code>

  File "halmos/.venv/bin/halmos", line 8, in <module>
    sys.exit(main())
  File "halmos/src/halmos/__main__.py", line 1677, in main
    return _main().exitcode
  File "halmos/src/halmos/__main__.py", line 1641, in _main
    test_results = run_method(run_args)
  File "halmos/src/halmos/__main__.py", line 1019, in run_sequential
    setup_ex = setup(
  File "halmos/src/halmos/__main__.py", line 520, in setup
    for idx, setup_ex in enumerate(setup_exs_all):
  File "halmos/src/halmos/sevm.py", line 2415, in run
    self.create(ex, opcode, stack, step_id)
  File "halmos/src/halmos/sevm.py", line 1913, in create
    self.transfer_value(ex, caller, new_addr, value)
  File "halmos/src/halmos/sevm.py", line 1528, in transfer_value
    balance_cond = simplify(UGE(ex.balance_of(caller), value))
  File "halmos/src/halmos/sevm.py", line 817, in balance_of
    self.path.append(ULT(value, con(2**96)))
  File "halmos/src/halmos/sevm.py", line 598, in append
    import traceback; traceback.print_stack()
WARNING:halmos:path.append(false) orig_cond=ULT(340282366920938463463374607431768211456, 79228162514264337593543950336)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
  File "halmos/.venv/bin/halmos", line 8, in <module>
    sys.exit(main())
  File "halmos/src/halmos/__main__.py", line 1677, in main
    return _main().exitcode
  File "halmos/src/halmos/__main__.py", line 1641, in _main
    test_results = run_method(run_args)
  File "halmos/src/halmos/__main__.py", line 1019, in run_sequential
    setup_ex = setup(
  File "halmos/src/halmos/__main__.py", line 520, in setup
    for idx, setup_ex in enumerate(setup_exs_all):
  File "halmos/src/halmos/sevm.py", line 2415, in run
    self.create(ex, opcode, stack, step_id)
  File "halmos/src/halmos/sevm.py", line 1913, in create
    self.transfer_value(ex, caller, new_addr, value)
  File "halmos/src/halmos/sevm.py", line 1537, in transfer_value
    ex.balance_update(caller, self.arith(ex, EVM.SUB, ex.balance_of(caller), value))
  File "halmos/src/halmos/sevm.py", line 817, in balance_of
    self.path.append(ULT(value, con(2**96)))
  File "halmos/src/halmos/sevm.py", line 598, in append
    import traceback; traceback.print_stack()
WARNING:halmos:path.append(false) orig_cond=ULT(340282366920938463463374607431768211456, 79228162514264337593543950336)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
[console.log] msg.sender 0x00000000000000000000000000000000000000000000000000000000de4107e4
[console.log] trustedForwarder 0x00000000000000000000000000000000000000000000000000000000aaaa0003
Error: setUp() failed: HalmosException: No successful path found in setUp()
Traceback (most recent call last):
  File "halmos/src/halmos/__main__.py", line 1019, in run_sequential
    setup_ex = setup(
               ^^^^^^
  File "halmos/src/halmos/__main__.py", line 560, in setup
    raise HalmosException(f"No successful path found in {setup_sig}")
halmos.exceptions.HalmosException: No successful path found in setUp()
Symbolic test result: 0 passed; 1 failed; time: 0.49s

To Reproduce

Check out https://github.com/igorganich/damn-vulnerable-defi-halmos/blob/master/test/naive-receiver/NaiveReceiver.t.sol

Run halmos --function test_naiveReceiver

Environment:

• OS: mac
• Python version: Python 3.12.1
• Halmos and other dependency versions: f7ff1f8

[karmacoma-eth]

startHoax(deployer) does the following (in StdCheats.sol)

    // Start perpetual prank from an address that has some ether
    // tx.origin is set to the origin parameter
    function startHoax(address msgSender, address origin) internal virtual {
        vm.deal(msgSender, 1 << 128);
        vm.startPrank(msgSender, origin);
    }

This deals 3.4e+20 ether to the recipient (!)

But in halmos' balance_of, we make the following assumption:

        # practical assumption on the max balance per account
        self.path.append(ULT(value, con(2**96)))

And because 1<<128 is in fact bigger than 1<<96, we end up adding false to the path condition, hence the warning

[karmacoma-eth]

Workaround: for now, don't use startHoax(address msgSender) but instead use a version with an explicit amount like startHoax(address msgSender, uint256 give)

[karmacoma-eth]

We should deal with this more gracefully on the halmos side, some ideas:

• add an explicit warning when we vm.deal an amount too large
• increase the tolerance in balance_of?
• detect that the condition is false in balance_of and give a more explicit error message
• ...

[Elyx0]

Took me an hour before I checked in here!! Was doing vm.deal(address(this),10**75); and was filled with

WARNING:halmos:path.append(false)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:halmos:path.append(false)

just lowering the deal solved it. Might be worth a readme adjustement! on #

[karmacoma-eth]

Took me an hour before I checked in here!! Was doing vm.deal(address(this),10**75); and was filled with

WARNING:halmos:path.append(false)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:halmos:path.append(false)

just lowering the deal solved it. Might be worth a readme adjustement! on #

some alternative ideas:

• introducing an MAX_ETH constant in SymTest that can safely be dealt to an address (vm.deal(addr, MAX_ETH))
• introducing a little svm helper: svm.dealMax(addr)