`vm.assume(bool)` should revert with `FOUNDRY::ASSUME` cheatcode when condition is false

[BowTiedRadone]

Currently, hevm's implementation of vm.assume(bool) returns successfully (via doStop) when the condition is false, rather than reverting with the magic code "FOUNDRY::ASSUME". This breaks Foundry test compatibility and makes it impossible for fuzzers to properly filter out invalid inputs:

hevm/src/EVM.hs

Lines 1833 to 1838 in 1f02fd8

	, action "assume(bool)" $
	\sig input -> case decodeStaticArgs 0 1 input of
	[c] -> do
	modifying #constraints ((:) (PEq (Lit 1) c))
	doStop
	_ -> vmError (BadCheatCode "assume(bool) parameter decoding failed." sig)

When vm.assume(false) is called, it should revert with the magic string "FOUNDRY::ASSUME\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0".

This is how Foundry implements it: https://github.com/foundry-rs/foundry/blob/e589ccfc404f878b77c1e6a5ea85023ad99482b6/crates/cheatcodes/src/test/assume.rs#L46-L51

Proposed fix:

vmError (Revert (ConcreteBuf "FOUNDRY::ASSUME\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0"))

Identified this together with @gustavo-grieco when working on Echdina's Foundry test generation feature.

[moodmosaic]

The real question is, does hevm primarily serve symbolic execution or foundry compatibility?

• If symbolic execution: I think current behavior is correct
• If foundry compatibility: Must revert with the magic code
• If both: Might need a mode flag or dual behavior

This is likely the right trade-off in the context of foundry/echidna, but it does mean assume no longer purely represents a logical constraint. 🤔

[BowTiedRadone]

@moodmosaic I had the same thought, but since the symbolic execution layer already handles this (assume adds a constraint that guides the SMT solver and does not affect concrete execution) and since this is a relatively small change, I think updating the concrete execution behavior makes sense.

[blishko]

hevm already knows if it is doing concrete or symbolic execution.
For symbolic execution the current behaviour should stay the same: just remember the logical constraint. Later, paths not satisfying the constraint are automatically excluded from analysis because of this.

For concrete execution, my understanding of the current behaviour is that the assumption is basically ignored.
I think reverting in case of failed assumption is a reasonable interpretation.
Is there any specification of assume cheatcode? Or is Foundry implementation THE specification?

Based on my background, I would expect a failed assume to terminate the whole VM immediately.
That would be my preferred interpretation.

[BowTiedRadone]

@blishko My understanding is that the Foundry implementation is indeed the specification regarding this cheatcode. Hence, mimicking the Foundry's Rust EVM behavior feels the natural approach. For more context, assume works like a discard mechanism, so it's not the a termination, but a revert.

[moodmosaic]

Why is foundry the spec? Where is that documented?

[BowTiedRadone]

@moodmosaic Here's where assume is defined: https://getfoundry.sh/reference/cheatcodes/assume#assume.

[blishko]

@BowTiedRadone, from your linked description:

If the boolean expression evaluates to false, the fuzzer will discard the current fuzz inputs and start a new fuzz run.

This is termination of the current run (whole EVM transaction), not just revert of the current frame.
This is the behaviour I would expect and is consistent with the behaviour of the symbolic execution.
I think hevm should implement this behaviour.
@msooseth , @gustavo-grieco, we could add a new EvmError to indicate failed assume and VM would terminate current run with VMFailure with the new error value. What do you think?

[gustavo-grieco]

@BowTiedRadone can you please check foundry/revm behavior and clarify how assume works in terms of failing?

[BowTiedRadone]

Full revm picture:

• cheatcode definition: MAGIC_ASSUME is defined -> https://github.com/foundry-rs/foundry/blob/8f0c8155bcef515279a3c341a6a4f41a6e964807/crates/evm/core/src/constants.rs#L36-L37
• cheatcode level: an error with the MAGIC_ASSUME content is returned for consumption -> https://github.com/foundry-rs/foundry/blob/8f0c8155bcef515279a3c341a6a4f41a6e964807/crates/cheatcodes/src/test/assume.rs#L46-L51
• revm/inspector (consumer) level: the error is caught by the cheatcode inspector and converted to a transaction revert with InstructionResult::Revert -> https://github.com/foundry-rs/foundry/blob/8f0c8155bcef515279a3c341a6a4f41a6e964807/crates/cheatcodes/src/inspector.rs#L752-L761
• fuzzer level: after revm execution completes, the fuzzer checks the revert data: https://github.com/foundry-rs/foundry/blob/8f0c8155bcef515279a3c341a6a4f41a6e964807/crates/evm/evm/src/executors/fuzz/mod.rs#L351-L354

This helps the (concrete execution) fuzzer to: discard the current fuzz input (not count it as a run), decrement the run counter, and continue with a new input. For invariant (stateful) fuzzing, a run discard behaves by "forgetting" the invalid call, rolling back to the previous step in the sequence, and continuing from that point. For regular (stateless) fuzzing, each run is independent, so it simply discards the input and tries a completely new one. If too many rejections occur, fail with "too many rejects" error.

If my understanding is correct, this is a revert, but @blishko @gustavo-grieco @moodmosaic please correct me if I'm wrong 🙏

[blishko]

I am not sure if we are using the same terminology, though I believe we are converging. I want to make sure that this is indeed "transaction-level revert", and not "call-frame revert" that we are talking about.
I agree with transaction-level revert. That should be consistent my suggestion to have a new EvmError in hevm to indicate a new kind of VMFailure (transaction result).