booster-dev crashes on simple test

[ehildenb]

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.

[jberthold]

I took a quick look at this.

• I don't know where the Unknown predicate: None comes from, but it is definitely on the client side. I would guess it is output for the special case of an SMT problem (which this is not, hence None).
• The rewrite aborts indeed because _<Int_(lengthBytes(_)_BYTES-HOOKED_Int_Bytes(abiCallData("execute", typedArgs(abi_type_address(VarA0:SortInt{}), .List{"typedArgs"}()))), "4") cannot be decided.

Looking at the definition of abiCallData(NAME, ARGS):

• abiCallData(NAME, ARGS) => signatureCallData(NAME, ARGS) +Bytes encodeArgs(ARGS)
• and signatureCallData(NAME, ARGS) => generateSignature(NAME, ARGS),
• and rule #signatureCallData( FNAME , ARGS ) => parseByteStack(substrString(Keccak256(String2Bytes(#generateSignature(FNAME, ARGS))), 0, 8))
• The first 8 characters of Keccak256(_) are parsed with #parseByteStack, length of which should be 4 bytes.

However, I did not find any simplifications that would allow us to conclude all of that together directly.

Maybe a simplification rule lengthBytes(#abiCallData(_, _)) <Int N => false requires N <=Int 4 ?
(after signatureCallData, the encoded arguments follow, so this is quite a rough estimate)

kore-rpc simplifies abiCallData("execute", ( #address ( A0:Int ) , .TypedArgs )) to "Kd\228\146" +Bytes buf(32, A0), which booster does not because bufStrict and #enc are not total.