Could the backend report vacuous nodes through the execute response ?

[iFrostizz]

This issue originates from runtimeverification/evm-semantics#1944
We would like if possible the backend to report if the current executed node is vacuous.

A minimal example written in the Foundry integration of KEVM was tested.

// SPDX-License-Identifier: UNLICENSED
pragma solidity =0.8.13;

import "forge-std/Test.sol";

contract VacuousTest is Test {
    function test_unreachable(bool flag) public {
        vm.assume(false);
        assert(false);
    }
}

It can be stored in evm-semantics/tests/foundry/test
Then

kevm foundry-kompile
kevm foundry-prove --test VacuousTest.test_unreachable

It features a call to vm.assume(false) which stucks the execution at this line, when the K cell is roughly:

<k> #foundry_assume ~> false </k>

Currently, the next_cterms that is decoded from pyk is an empty list, so pyk deduces that the execution is stuck at this point. But we would like, if possible, the backend to be able to automatically return a new status code vacuous (or related) if the current node is vacuous.

I attached the return of the test ran with the kevm foundry integration and adding the --debug to be able to see the requests and response with the haskell backend (split in 2 to circumvent the Github file size limit). We can see that the depth-bound status code is returned with a first depth of 2, then of 0 in the last response that contains the depth-bound status code. In the two cases the response contains the #foundry_assume false.

dump_part1.txt
dump_part2.txt

Please ask me for additional information / files if needed.

Thanks !

[goodlyrottenapple]

Would you also happen to have the bug report tar file? This would make it easier to test and validate any changes.

[iFrostizz]

Thanks for looking into that @goodlyrottenapple !
Please find the bug report attached

bug_report.tar.gz

[ehildenb]

@iFrostizz it would be good to make an integration test in pyk, and generate the bug report for that integration test first. That way the test submitted to the backend can be much smaller and they can make a smaller test for this new feature. You can open a draft PR in pyk with the new test, nad it can be added here: https://github.com/runtimeverification/pyk/blob/1d76cf579daa3dc8f05a337dfce6cb925212d37d/src/tests/integration/kcfg/test_simple.py#L25

Then you can generate the bug report associated with it by running the test with this line uncommented: https://github.com/runtimeverification/pyk/blob/1d76cf579daa3dc8f05a337dfce6cb925212d37d/src/pyk/testing/_kompiler.py#L60

[ehildenb]

This minimal example should be against a much smaller definition than KEVM for the backend team to work with, so that the test is focused on just this particular issue.

[iFrostizz]

I pushed the minimal test on: https://github.com/runtimeverification/pyk/compare/master..vacuous-test-repro
And here is the bug-report

Please tell me if it doesn't describe the issue correctly, but it seems like applying a falsy constraint thanks to the ensures clause was close enough to a <k> foundry_assume ~> false </k> and we correctly get the depth-bound with a depth of 0 in the response.
We may want to modify the test so that it can include the ExecuteResult.reason = StopReason.VACUOUS or something related to make sure that the backend actually returns the expected stop reason.

[goodlyrottenapple]

I'm not sure we need a new stop reason. Surely the backend should just return stuck in this instance?

[ehildenb]

We want to be able to distinguish stuck and vacuous in the pyk libaryr because it affects the way the usre interprets the proof state. We can always feed the same result back into the simplify endpoint and see #Bottom come back, but the backend has already computed that it's vacuous so we should just report that information back.

So, short answer is that yes, we do want a separate return type if possible. A proof that passes because a branch becomes vacuous is something we want to warn the user of, because it could be an error in their specification.

[goodlyrottenapple]

From my investigation, the old backend cannot actually distinguish between stuck and vacuous. From the logs I can see that the backend checks the ensures predicate once unified and finds false and therefore aborts. However, as far as I can tell, it doesn't store this failure in any special way, compared to e.g. failing to unify with the LHS.

[anvacaru]

Closed by #3637