Skip to content

Latest commit

 

History

History
28 lines (20 loc) · 808 Bytes

README.md

File metadata and controls

28 lines (20 loc) · 808 Bytes
Raw

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