Thread by @_hrkrshnn

@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!