Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Oct 21 2017 21:21
    @jpitts banned @Musk55
chriseth
@chriseth
About the stability of Yul: It has been stable for over a year. We added a new construct recently called "leave", which makes the control-flow exit the current function. Planned for "soon" is a type system, but that should be mostly irrelevant for such a translation
Leonardo
@leonardoalt
@sxysun @chriseth
I also think it'd be great to have that done for Yul. Having a verifier for each translation level means we can also try to verify the translation themselves, and of course each one will have its own strengths.
sxysun
@sxysun
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
@sxysun
And is the latest stable semantics of Yul in the K-formalization repo? or do you guys have other docs. We have previously followed the Solidity website and solc compiled results
chriseth
@chriseth
@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
Leonardo
@leonardoalt
@endorphin @MrChico
River
@endorphin
o/
MrChico
@MrChico
@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
sxysun
@sxysun
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?
chriseth
@chriseth
@sxysun there are some other small differences, but essentially yes
Sumit Lahiri
@codersguild
We are actively working on making a theorem solver that runs on a blockchain and can be used to verify a wide range of smart contracts.
chriseth
@chriseth
@codersguild nice! Is it bytecode- or high-level-language based?
Sumit Lahiri
@codersguild
High-level language as of now but will soon move to EVM bytecode.
Evgeniy Shishkin
@unboxedtype
@codersguild Hi! By theorem solver you mean some form of SMT-solver or automatic theorem prover, like Vampire et al? Do you have any materials on the subject?
Dejan Jovanović
@dddejan
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.
Leonardo
@leonardoalt
@dddejan nice, thanks for sharing the paper. Do you have any plans for function types? I'm currently only abstracting them as integers, without reasoning properly about them.
Dejan Jovanović
@dddejan
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?
Leonardo
@leonardoalt
not that I know, I also think it's not really worth it for now
Dejan Jovanović
@dddejan
for example, seems complicated to figure out given a function type which internal functions can be called and what are their values.
chriseth
@chriseth
@dddejan without having read the paper - do you have any feedback concerning language or compiler design?
River
@endorphin
@leonardoalt @MrChico requesting push access for git@github.com:ethereum/act.git
Leonardo
@leonardoalt
@endorphin sent invite
Dejan Jovanović
@dddejan
@chriseth we do have some thoughts. mainly things that makes semantics very complicated or very diffucult to analyze.
chriseth
@chriseth
please feel free to pour specific suggestions into issues on github.com/ethereum/solidity !
Dejan Jovanović
@dddejan
can do, it's a good idea. at least to get a rationale for some of the design decisions that are probably driven by practicall issues we don't see.
Ada922
@Ada922

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

Greg Colvin
@gcolvin
This would be Naveed’s work with the Marshall islands. Interesting stuff.
Evgeniy Shishkin
@unboxedtype
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.
Leonardo
@leonardoalt
Thanks @unboxedtype !
Evgeniy Shishkin
@unboxedtype
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
Evgeniy Shishkin
@unboxedtype
Hey Boogie experts, how to convert bit vector into int and probably other way around?
Dejan Jovanović
@dddejan
@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.
Evgeniy Shishkin
@unboxedtype
@dddejan Thanks a lot!
MrChico
@MrChico
hevm now supports symbolic execution of EVM bytecode!
https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/
Ben Siraphob
@siraben
@MrChico Will symbolic execution be able to detect bugs caused by integer over/underflow?
MrChico
@MrChico
@siraben not directly with this release, but if you add overflow checks like assert(x + y >= x), it would
Ben Siraphob
@siraben
@MrChico I see.
Evgeniy Shishkin
@unboxedtype
@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.
Leonardo
@leonardoalt
@unboxedtype we're not working directly on proof checking. We would like to have it though, since it would be necessary in case the Solidity compiler decides to use SMT solvers for Yul optimization
Evgeniy Shishkin
@unboxedtype
@leonardoalt Got it, thanks!
Raitonvortex
@Raitonvortex
Hey, I'm researching formal methods for smart contracts on Ethereum for my masters degree thesis, does anyone have an index summarizing research on this area? And/or an opinion on leading projects and research? Thanks a lot!
matrixbot
@matrixbot
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
Raitonvortex
@Raitonvortex
Thank you!