Hari Profile picture
21 Jul
@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
Read 7 tweets