This pr adds an smt level optimization that generates a unique smt array for each logically seperate region in storage (i.e. each solidity level map / array will get it's own smt level array). This allows us to completely eliminate invocations of keccak from many of our smt queries, which gives a huge speedup on all storage related operations.
The code here is still somewhat primitive, and seems to choke on more complex cases involving multiple reads / writes from nested arrays, but already gives a very satisfying speedup on storage related benchmarks.
Notes
Found and fixed a minor bug in readStorage -- the a and b of Lit + Array / Array + Lit were copy-pasted and the guard conditions were hence swapped around.
Array separation does not work currently. Added a NOTE to readStorage that indicates why. It also leads to decompose-3-mixed is failing. Basically, a of potentially large offset allowing full overwrite of the storage. Maybe we need to discuss about this?
The fuzz testing load-decompose is currently turned off because we need to have more constraints on the generated query, or the counterexamples it gives as error are actually fine.
Description
This pr adds an smt level optimization that generates a unique smt array for each logically seperate region in storage (i.e. each solidity level map / array will get it's own smt level array). This allows us to completely eliminate invocations of keccak from many of our smt queries, which gives a huge speedup on all storage related operations.
The code here is still somewhat primitive, and seems to choke on more complex cases involving multiple reads / writes from nested arrays, but already gives a very satisfying speedup on storage related benchmarks.
Notes
readStorage-- theaandbof Lit + Array / Array + Lit were copy-pasted and the guard conditions were hence swapped around.readStoragethat indicates why. It also leads todecompose-3-mixedis failing. Basically, a of potentially large offset allowing full overwrite of the storage. Maybe we need to discuss about this?load-decomposeis currently turned off because we need to have more constraints on the generated query, or the counterexamples it gives as error are actually fine.Checklist