Wonderful! Thanks guys. I came across your work when developing the translator @dddejan! @chriseth Nice to know Yul is stable now, I will look into it. And btw, @leonardoalt do you mean using different levels of verification to do translation validation and ultimately give a "verified" solidity compiler?
@sxysun the semantics of yul are very simple and have been documented in https://solidity.readthedocs.io/en/develop/yul.html#formal-specification
In addition to that, you mostly need the scoping rules which are unfortunately only described in text
"pure Yul" ist mostly useless, because you need a specification of the built-in functions, which then defines the so-called dialect of yul.
the builtin functions listed on the page behind the link are not implemented anywhere (we should really update that page)
instead, we use the bulitin functions defined in that table: https://solidity.readthedocs.io/en/develop/assembly.html#opcodes
they are identical to the EVM opcodes
the k yul semantics can be found here: https://github.com/ethereum/yul-semantics but I cannot tell how complete it is
@sxysun there's also a WIP isabelle semantics of yul that are further along than the
yul-semantics mentioned above in some regards. Check it out here https://github.com/mmalvarez/Yul-Isabelle
Wonderful! The formalized semantics could really help. And just to clarify, @chriseth isn't the EVM dialect of Yul with https://solidity.readthedocs.io/en/develop/assembly.html#opcodes as builtin functions the same as https://solidity.readthedocs.io/en/develop/yul.html#low-level-functions except they do not have types?
if anybody is interested in encoding the Solidity memory model into SMT, we have a new paper out describing how we do it in solc-verify. draft preprint available at https://arxiv.org/abs/2001.03256. any comments and suggestions very welcome.
not really, i'm not 100% with understanding the semantics of function types yet. also i'm not sure who's using them, why and how. seems like a lot of work to support properly, basically encode the integer value and then do manual dispatch. we just ignore for now. are there any interesting contracts that use it in practice?
Tomorrow Algorand is hosting a live webinar on implementing the world’s first CBDC. I have submitted a few questions and will be attending. This is a great way to spend your quarantine :)
Register and submit questions here: https://register.gotowebinar.com/register/5273854108710515471
There will be 3 PLDI talks devoted to smart-contract analysis / verification at 19 Jun. Check https://pldi20.sigplan.org/program/program-pldi-2020 for details. PLDI is online and free this year due to well known circumstances.
FYI: There will be a workshop on smart contract analysis techniques, including sound techniques soon. They still accept papers btw https://conf.researchr.org/track/issta-2020/issta-2020-wosca
@unboxedtype I haven’t tried myself, but you can take a look here https://github.com/boogie-org/boogie/blob/032700096179f5af1be4c50dd5ed8afb6b361e09/Test/smack/git-issue-203.bpl#L55. You should try and avoid if possible.
hevm now supports symbolic execution of EVM bytecode!
https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/
https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/
@leonardoalt Hi! I came across your issue in Z3 github related to proofs verification generated by Z3. Are you guys or someone you might know working on this problem? Seems like Z3 still does not implement proof checking in full. Other related SMT-proof-checking tools also avoid Z3 for some reason.
xvwx @leo put together a very nice overview here: https://github.com/leonardoalt/ethereum_formal_verification_overview
xvwx in terms of tools deployed in the wild, I would say that the k framework has seen the most usage