![Clear - Github (1)](https://private-user-images.githubusercontent.com/114106639/347780053-9d92cbbc-5a55-4808-ae48-525647c1c0d6.png?jwt=eyJhbGciOiJIUzI1NiIsInR5cCI6IkpXVCJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmF3LmdpdGh1YnVzZXJjb250ZW50LmNvbSIsImtleSI6ImtleTUiLCJleHAiOjE3MjU5NjQzNTcsIm5iZiI6MTcyNTk2NDA1NywicGF0aCI6Ii8xMTQxMDY2MzkvMzQ3NzgwMDUzLTlkOTJjYmJjLTVhNTUtNDgwOC1hZTQ4LTUyNTY0N2MxYzBkNi5wbmc_WC1BbXotQWxnb3JpdGhtPUFXUzQtSE1BQy1TSEEyNTYmWC1BbXotQ3JlZGVudGlhbD1BS0lBVkNPRFlMU0E1M1BRSzRaQSUyRjIwMjQwOTEwJTJGdXMtZWFzdC0xJTJGczMlMkZhd3M0X3JlcXVlc3QmWC1BbXotRGF0ZT0yMDI0MDkxMFQxMDI3MzdaJlgtQW16LUV4cGlyZXM9MzAwJlgtQW16LVNpZ25hdHVyZT03ZDgwMTNiZTE1NGNhNTYxODIyYTY1ZjhiOTI3NTRmZDY5ZTYzOWM0YTZlNmRhOWEyOTQzZmQxZmYzNTI2ZWU2JlgtQW16LVNpZ25lZEhlYWRlcnM9aG9zdCZhY3Rvcl9pZD0wJmtleV9pZD0wJnJlcG9faWQ9MCJ9.gkaDRpjjNOEEdca8T3zwG6Hg7JyKs3vwVS5Ce292DM4)
Prove anything* about Yul programs.
There are two parts.
- A Lean framework with a Yul model.
- A verification condition generator.
Download and install Lean 4. One can follow https://lean-lang.org/lean4/doc/quickstart.html.
Then simply run the following in the root directory:
lake build
Download and install Stack. One can follow https://docs.haskellstack.org/en/stable/install_and_upgrade/.
Then simply run the following in the vc
directory:
stack build
In the vc
directory, run:
stack run vc ../out/peano.yul
You should get a Generated
folder corresponding with the structure of the Peano example
in the out/peano.yul
file.