Ethereum Foundation / Solidity Summit

Introduction to ACT, followed by an open discussion around formal verification and language features to support more formal specifications inside Solidity.

We will describe a platform for formally verifying smart contract correctness that can be integrated in CI/CD. Smart contracts and their invariants are converted into SMT formulas and the SMT solvers automatically identify vulnerabilities or generate mathematical proofs of correctness. We describe our experience applying this technology in the development phase and present bugs found and smart contracts verified. Our hope is that this SaaS technology can speed up the development process. The secret sauce for integrating in the CI/CD is that the invariants are reusable across different versions of the code, and targeting the low level EVM bytecode. This raises various technical challenges both at the conceptual level of the specification and at the technical level.

Can the challenges of Solidity development — gas limitations, storage scarcity, and decentralized computation — create conditions for creative DApp development? Are the parts of Solidity that often confound developers actually starting points for creative thinking? This lightning talk will showcase a few novel applications of Solidity, from DApp layering and ERC721 art generation, to some of my personal projects, including a fruit-backed cryptocurrency, a blockchain treasure hunt, and an ERC721 Curry Generator. This talk will also provide insight into how Curvegrid builds DApps.

During our audits at Quantstamp, we often find functions written in Solidity which are prone to hit out of gas errors because they contain loops over a user defined/influenced value. However, these functions do not run out of gas all the time. It takes a certain input value or a certain contract state to run out of gas. The big question is: how can we identify that state/value? This presentation describes an approach to answering this question by using a smart contract fuzzing approach based on machine learning.

The Solidity compiler appends the hash of a json structure called the metadata to the deployed bytecode of each contract by default. The idea behind this feature is to hash-link the original source code into the bytecode, provide the ABI and other information and finally all settings that are required to re-compile the contract. Most of these features overlap with the EthPM project with the only difference that the compiler needs to generate this information before the contract has been deployed. Because of that, the EthPM team started an initiative to unify the two data formats. Until now, we already get pretty far and this session is mostly to agree on some final details of the combined metadata and EthPM3 specification.

In the early days, the Mix debugger shared the same code base as the Solidity compiler and thus it was easy for it to retrieve required information about the internals of a smart contract. Since then, the type system and the optimizer have become way more complex and it is not as easy anymore to decipher what is going on behind the scenes. Some months ago, the Truffle team has kicked off an initiative for the compiler to provide more detailed debugging information, but debugging information is not only relevant for debuggers, but also for general analysis tools. This discussion will be about collecting needs about debugging information and starting to standardize the data format.

The language server protocol is an initiative by Microsoft to standardize a communication protocol between IDEs and compilers. It does not only allow line-based error reporting, but also code completion, "jump to definition" and other features. While code completion might be rather far off since it has to cope with analysis on invalid source code, "jump to definition" and other features might be very useful for auditors and developers alike.

"Yul+ is an extension to Yul, an intermediate language for the Ethereum Virtual Machine. It adds several quality of language features such as enums, constants, memory structures and injected methods. Our talk will go over the motivations, objectives and the features that Yul+ brings to the Ethereum ecosystem.

1) Yul overview, what we liked and what we needed
2) Motivations for an extension language
3) Objectives for a new language
4) Yul+ feature overview
5) Roadmap and future language exploration"

Learn about the K's background and the Solidity semantics in the K framework.

An introduction to mutation testing and the tool Vertigo, including a discussion where solc, Truffle, and Vertigo could work together.

"In this talk you'll learn more about the Solang Compiler:
- Why Solang (rust, llvm)
- What targets are supported (substrate, ewasm)
- What is implemented
- Roadmap
- Compiler stages:
- parser (lalrpop)
- resolver
- code emitter
- standard library
- linker
- future ideas/directions"

Learn more about the evolution and current state of the SOLL compiler project, which builds compiler front ends for YUL and Solidity, and backends for Ewasm and EVM. This talk includes a report on the technical progress made so far as well as future roadmaps and collaborations. It also discussed the web-based IDE developed for Solidity that allows fast dapp development and deployment on Ethereum compatible blockchains.

Chris gives us a quick tour of the roadmap for Solidity Summit for 2020.

Franziska Heintel welcomes us to The Solidity Summit for April 2020 and gives us a quick overview of how to use the technology.

Solidity is a relatively young language in a rapidly evolving space. The challenges it faces changed over time, greatly influencing the language design. In this brief talk, we examine the current language design processes in place and compare it against other models (i.e. language design committees).

The Solidity language does not keep track of what keys are set in a given mapping. However, the Truffle Debugger can, when debugging a transaction, keep track of what keys have been accessed during that transaction, and it can do this even if the mappings are nested inside arrays, structs, or other mappings. In this talk, we will dissect Truffle Debugger's mapping key tracking system and learn how it works.

"In this talk you will learn about source verification. These topics will be covered:
- Why is it needed?
- How is it done?
- How can it be decentralized?
- How can you use it?
- What is wrong with NatSpec and RadSpec?
- What are the next steps?"

Gonçalo Sá and Martin Ortner Walk us through visualization of large codebases using the Solidity visual extension for VSCode!

"dType is a decentralized & distributed type system for interoperable protocols.
ChainLens: Lens implementation for Ethereum as a browser and fine-grained search for smart contracts with a distributed database cache of types, functions, ABIs, code sources, and other metadata information. Available as a Remix IDE plugin, interoperable with other plugins.

"SOLL 0.0.6 release(eta. 2020-03-06) will support Yul constructor and deployer. SOLL can compile both Solidity(partial of the grammar) and Yul(most of the major grammar) to LLVM IR. When the LLVM IR is generated, SOLL will apply LLVM optimization passes to reduce the code size, improve the performance, and eliminate redundant codes. And then SOLL transforms these optimized LLVM IR into Ewasm bytecodes.

In this topic, I want to share about how we optimize via LLVM framework and a new profile-guided optimization mechanism to analyze wasm runtime execution and adjust the optimization strategies back to the optimization phase to gain more improvement."