@transmissions11 1/7 In theory, it should, because there is a rule for that in the list
(github.com/ethereum/solid…). In practice, this
isn't happening. This is a good place to introduce the difference between the legacy codegen and the
Yul codegen, and their corresponding optimizers.
@transmissions11 2/7 For the legacy codegen, the AST is translated directly into EVM instructions (with some caveats), whereas, for the Yul codegen, it gets translated to the intermediate language (Yul). In particular, Yul still has some
Jul 21, 2021 • 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
