Hari Profile picture
21 Jul, 7 tweets, 3 min read
@tarunchitra 1/n Currently there is a Yul optimization step (mainly relevant for the upcoming Yul based pipeline) that uses an SMTSolver for removing some redundant checks. The step is disabled by default. In short, it encodes Yul in SMT (we use Z3) and the infeasibility of the system can be
@tarunchitra 2/n used to perform an optimisation. However this makes compilation slow and dependent on an external tool (Z3). For the latter issue, it's unfortunately not possible to easily verify 'proofs' of infeasibility provided by Z3. We tried to explore SMT solvers with a focus on
@tarunchitra 3/n external verification of proofs. However, we didn't really find a satisfactory tool for this. The other approach is to try to work with an easier set of constraints. None of EVM arithmetic is linear (even add has wrapping behaviour.) Another approach is for the compiler to
@tarunchitra 4/n store a relaxed system of linear equations, then use Z3 to check it's infeasibility. Then, the compiler can make Z3 produce a feasibility proof for its dual using Z3. This would produce proofs that can be verified by the compiler. Another approach is to directly use a
@tarunchitra 5/n Simplex solver and directly check the dual proofs or perhaps trust it for the time being. Unfortunately we couldn't find a solver that would fit our requirements--can do rational solve, can deal with large numbers (evm numbers are too big for most solvers) and license.
@tarunchitra 6/n We experimented with implementing a simple Simplex solver on rationals. This could, in the future, be used for some clever optimizations. This is currently not being actively pursued, owing to more important features elsewhere. But something we have in our mind for future!
@tarunchitra 7/n To summarize, pure SMT in optimization doesn't seem to be the way ahead. Small custom solvers maybe useful!

• • •

Missing some Tweet in this thread? You can try to force a refresh

Keep Current with Hari

Hari Profile picture

Stay in touch and get notified when new unrolls are available from this author!

Read all threads

This Thread may be Removed Anytime!


Twitter may remove this content at anytime! Save it as PDF for later use!

Try unrolling a thread yourself!

how to unroll video
  1. Follow @ThreadReaderApp to mention us!

  2. From a Twitter thread mention us with a keyword "unroll"
@threadreaderapp unroll

Practice here first or read more on our help page!

Did Thread Reader help you today?

Support us! We are indie developers!

This site is made by just two indie developers on a laptop doing marketing, support and development! Read more about the story.

Become a Premium Member ($3/month or $30/year) and get exclusive features!

Become Premium

Too expensive? Make a small donation by buying us coffee ($5) or help with server cost ($10)

Donate via Paypal Become our Patreon

Thank you for your support!

Follow Us on Twitter!