`booster-dev` crashes on simple test

booster-dev-crash.tar.gz

Here I've taken a test from KEVM: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/benchmarks/address00-spec.k, and run it with the booster-dev instead of with the proxy. It gets to the point where it's trying to evaluate the expression:

JUMPI 63 bool2Word ( lengthBytes ( #abiCallData ( "execute" , ( #address ( A0:Int ) , .TypedArgs ) ) ) <Int 4 )

This should pretty easily evaluate to:

JUMPI 63 bool2Word ( False )

But instead, I get a crash, with this result:

INFO 2024-08-08 22:26:31,734 pyk.kore.rpc - Sending request to localhost:36943: 140462604214544-049 - execute
INFO 2024-08-08 22:26:31,845 pyk.kore.rpc - Received response from localhost:36943: 140462604214544-049 - execute
ERROR 2024-08-08 22:26:31,851 kevm_pyk.utils - Proof crashed: 37ec95640f959842344f43a07ced4a5b909f213b0e5840b1662836069d32f3dd
Backend responded with aborted state. Unknown predicate: None
Traceback (most recent call last):
  File "/home/dev/src/evm-semantics/kevm-pyk/src/kevm_pyk/utils.py", line 150, in run_prover
    parallel_advance_proof(
  File "/home/dev/.cache/pypoetry/virtualenvs/kevm-pyk-kMaowF10-py3.10/lib/python3.10/site-packages/pyk/proof/proof.py", line 378, in parallel_advance_proof
    proof_results = future.result()
  File "/usr/lib/python3.10/concurrent/futures/_base.py", line 451, in result
    return self.__get_result()
  File "/usr/lib/python3.10/concurrent/futures/_base.py", line 403, in __get_result
    raise self._exception
  File "/usr/lib/python3.10/concurrent/futures/thread.py", line 58, in run
    result = self.fn(*self.args, **self.kwargs)
  File "/home/dev/.cache/pypoetry/virtualenvs/kevm-pyk-kMaowF10-py3.10/lib/python3.10/site-packages/pyk/proof/proof.py", line 457, in step
    return prover.step_proof(proof_step)
  File "/home/dev/.cache/pypoetry/virtualenvs/kevm-pyk-kMaowF10-py3.10/lib/python3.10/site-packages/pyk/proof/reachability.py", line 795, in step_proof
    extend_result = self.kcfg_explore.extend_cterm(
  File "/home/dev/.cache/pypoetry/virtualenvs/kevm-pyk-kMaowF10-py3.10/lib/python3.10/site-packages/pyk/kcfg/explore.py", line 235, in extend_cterm
    cterm, next_states, depth, vacuous, next_node_logs = self.cterm_symbolic.execute(
  File "/home/dev/.cache/pypoetry/virtualenvs/kevm-pyk-kMaowF10-py3.10/lib/python3.10/site-packages/pyk/cterm/symbolic.py", line 121, in execute
    raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}')
ValueError: Backend responded with aborted state. Unknown predicate: None

Not sure why there is Unknown predicate: None. At the very least, I would expect the booster-dev to report back to me the branch on the JUMPI instruction instead, so that the proof can continue.

Start by reproducing the crash with the attached archive and the KEVM address00-spec.k test, using booster-dev instead of the proxy. Read the run_prover traceback in kevm-pyk/src/kevm_pyk/utils.py and inspect the backend response that produces “Unknown predicate: None.” Done means the expression is handled without aborting and the JUMPI branch is returned so the proof can continue.