Vyper: Monday 7th Janurary 2019

[fubuloubu]

Start: Monday 7th Janurary 2019, 15:00 UTC (https://time.is/UTC)
Hangouts: https://meet.google.com/czc-kuep-jda

Agenda:

• #1150 (@charles-cooper)
• #1164 (@buckle2000)
• #1170 (@fubuloubu)
• #1176 (@GNSPS)
• #1177 (@GNSPS)
• Bytecode Optimization
• SlithIR, static analysis, and the Vyper AST (@montyly, see https://github.com/ethereum/vyper/issues/1140#issuecomment-446811611)

[jacqueswww]

AST output:

• Create a proof of concept for AST output.
• Then iterate on this implementation.
• Formalized grammer, see k semantics.

[fubuloubu]

Also, formalize the grammar (maybe in K?)

[nrryuya]

Great, you mean updating this work?
https://github.com/kframework/vyper-semantics

[fubuloubu]

Yes!

+10 Brownie points if we somehow pull that as a submodule and have a nightly CI test against it

[nrryuya]

Cool. Through FVyper project I thought formal verification of Vyper compiler is as important as verifying Vyper contracts so I verified clear function as a PoC.
https://github.com/LayerXcom/verified-vyper-contracts/tree/master/k/built-ins

This verification is working in CircleCI, with other verification including ERC20.

AFAIK https://github.com/kframework/vyper-semantics is another compiler based on K.

[nrryuya]

Just a note, there is a Python semantics in K.
https://github.com/kframework/python-semantics

[fubuloubu]

I would say if you want to do the work, the K setup gives you a template for how the larger build can work. One big note that came out of the meeting today is that we need to get better at documenting and testing against our grammar.

A good side effect is that can do formal verification of the compiler like this. Another good side effect is it makes refactoring WAY easier if we have test cases to run against our grammar (and we would like to do that). We found a LOT of very deep bugs from having this exercise performed by the Runtime Verification folks (creators of K) back in the springtime of last year.

[fubuloubu]

An ultimate goal that was being planned for the work with K is to have a mode that could do a triangular verification of the sourcecode and the bytecode of a program, proving semantic equivalence of a program in K after it has been compiled (since there is formal semantics for EVM execution).

[mihairaulea]

hey @fubuloubu -- i am helping Slither add support for Vyper, and i am proficient with compilers and ASTs. I understand what needs to be done here. Do you think i could help?

[jacqueswww]

@mihairaulea the biggest problem with getting this feature out at the moment is that we use the ast module of python 3 directly. As discussed in the call we probably want to put our own AST layer (could have a lot of replicated classes etc. but still unique concepts like payable and distinct types) in Vyper. Once we have this we can loop you in to do serialization thereof ?

Unless you are keen to do this conversion as well, o'course :)

[fubuloubu]

@mihairaulea first step in my book is to define the grammar in an executable format (like K) that we can refactor our front end against.

[montyly]

@jacqueswww @fubuloubu would it make sense if we go ahead and create a vyper_to_json utility, that takes a vyper code and outputs its representation to a json file?

From my (small) understanding of the vyper codebase, we could follow something similar to https://github.com/ethereum/vyper/blob/c558ce3d5e40ddeb95d583f6037c80ca9e40f94d/vyper/parser/parser.py#L205-L239
without the LLL part, and export global_ctx and the end.

Would that make sense and be helpful for your team?

[jacqueswww]

@montyly yes that would be roughly what needs to be done, additionally a local context gets produced with each parse_func call - actually for context info it's very similar to https://github.com/jacqueswww/vyper-debug/blob/master/vdb/source_map.py#L40