yul-semantics

K formalization of the Yul language

Requires the same dependencies as evm-semantics

Build with:

make

The main goal of this repository is to verify optimizations done by the Solidity compiler via translation validation. In other words, given a yul program, A and the optimized version, A', we prove the an equivalence of programs A <=> A' through bisimulation.

Try the example tests/proofs/sstoreloop-spec.k by running:

./kyul prove tests/proofs/sstoreloop-spec.k

If you want to explore the proof, run:

./kyul klab-prove tests/proofs/sstoreloop-spec.k

followed by:

./kyul klab-view tests/proofs/sstoreloop-spec.k