search

a16z / halmos

A symbolic testing tool for EVM smart contracts
GNU Affero General Public License v3.0
806 stars 67 forks source link

feat request: add support for user-defined objectives like optimization #397

Open 0xalpharush opened 1 week ago

0xalpharush commented 1 week ago

Is your feature request related to a problem? Please describe. For issues like rounding or trying to maximize the amount of an asset received, it would be nice to have an automated tool to exacerbate the rounding error or maximize the amount received.

Describe the solution you'd like Create a mode to find minimums/maximums instead of checking for reachability of assertions. Z3 seems to have built-in support for this but it's inner workings or limitations are a mystery to me...

Describe alternatives you've considered Using a fuzzer or effectively brute force search. It may be possible to repeatedly replace the value returned by Halmos and ask it for N+1 in a loop but I'd assume the SMT solvers have a better way to optimize than this

Additional context https://microsoft.github.io/z3guide/docs/optimization/arithmeticaloptimization/

karmacoma-eth commented 4 days ago

We could give this a try, but I'm not convinced that it would work well, if at all. Do you have a motivating example we could try it on?