Verifying Smart Contracts in Yul via Transformation to CHC by Interpreter Specialization

Yul is an intermediate representation that lies in between the (high-level) source code and the (low-level) bytecode languages for Ethereum smart contracts. Although it was proposed to favour the development of verification and optimization techniques, there exists no verifier that can be applied on Yul code directly yet. In this paper, we present a transformational approach to verifying Yul code by transforming it into an equivalent set of Constrained Horn Clauses (CHCs), leading, to the best of our knowledge, to the first approach to directly verify Yul code. Our transformational approach applies the first Futamura projection, i.e., specializes a Yul interpreter written in CHC with respect tothe Yul code to be verified. The verification of the transformed CHC code can rely on existing tools for CHC verification, namely we have used Z3 with the SPACER engine on our case studies.