Solver timeout when attempting to prove mint(Pass)
koolexcrypto opened this issue · 4 comments
What could be the reason to get such an error message?
Solver timeout when attempting to prove mint(Pass)
I get this when there is incrementing logic in the tested behaviour and solidity function.
I'm running:
act hevm --spec <act-spec-file> --soljson <output-json-of-contract>
The current hevm backend is unfortunately only able to successfully discharge proofs for very trivial contracts (e.g. anything involving checked arithmetic is currently too hard). This is due to some frustrating smt encoding issues related to differences in numeric types used in hevm and act.
If you hit a solver timeout it's probably because the problem is too difficult :(.
We're currently working hard in hevm to rewrite the symbolic execution engine and hope that this rewrite will let us make the bytecode proof engine in act significantly more powerful. We also want to integrate with kevm to allow bytecode level proofs using the k framework proof engine.
Is the limitation by hevm its self or integrating it into act?
from what I understand, there is a mismatch when it comes to numeric types?
That would be interesting to see how act would work with kevm :D
The issue is that Act represents numbers using mathemaical integers (i.e. unbounded, no wrapping), whereas hevm uses 256bit bitvectors (i.e. bounded size, wrapping on overflow). When checking equivalence between a symbolic representation of an evm bytecode object produced with hevm and an act spec, we therefore have to introduce many instances of the int_to_bv and bv_to_int operations in the smt encoding. This is very expensive and is the main cause of the performance issues.
The rewrite to hevm that we are currently working on will give us greater control over the smt encoding, and we intend to introduce a stage in the equivalence checking engine that will convert the symbolic representation of the evm bytecode from a bitvector based encoding to an integer based one, avoiding this issue.
Gotcha! wow .. there seems to be a lot to do. Much appreciation for you guys