KEVM gets stuck on #assume(false) #1944
Description
KEVM seems to get stuck when it hits an #assume(false). For example, the following minimal example fails because it branches inside the atLeastOneIsValidAddress function, with two of the branches evaluating to #assume(true) and the last one evaluating to #assume(false). The #assume(false) branch then gets stuck.
function atLeastOneIsValidAddress(address alice, address bob)
internal
returns (bool)
{
if (alice != address(0)) {
return true;
} else if (bob != address(0)) {
return true;
} else {
return false;
}
}
function test_assume_return(address alice, address bob) public {
vm.assume(atLeastOneIsValidAddress(alice, bob));
assert(true);
}
In a situation like this, we would want #assume(false) to add #Bottom to the constraints, which would cause the branch where it happens to be vacuously satisfied. This would be consistent with the behavior in Foundry, which ignores inputs for which the assume evaluates to false.
#assume is implemented as rule <k> #assume(B) => . ... </k> ensures B in foundry.md, but KEVM gets stuck on #assume(false), so is this a restriction on the ensures clause? Is ensures false not allowed? If this is the case, is there a way to implement an alternative rule for #assume(false) that will have the behavior that we need (discarding the vacuous branch)?
On the other hand, as @ehildenb pointed out, this can cause issues where a proof might vacuously pass because the user accidentally added contradictory assumptions:
But you could also have something like
vm.assume(pred1); vm.assume(pred2);(separated by a large chunk of code, even) and as a user you don't realize thatpred1 /\ pred2 == false, so it vacuously discards that branch and leads to the proof passing, even though it didn't actually prove anything.
To prevent this from happening accidentally, we might want to do one of the following:
- Create a separate cheatcode, like
vm.assume_allow_vacuous, that allows this behavior, so that the user needs to explicitly say when they want to accept vacuous branches. - Another option is to mark branches that passed because they are vacuous and report that to the user. This way the user will know if a branch became vacuous accidentally.