ABCDEFGHIJKLMNOPQRSTUVWXYZAAABACADAEAF
1
2
3
4
Solidity
DAY 1
Wednesday, 29th of April
5
Summit 2020
6
+ April 29-30
+ Join at interspace.solidity-summit.ethereum.org
7
8
TIMETITLESPEAKER / MODERATORFORMATCOLLABORATIVE NOTES
OTHER TIME ZONES
9
10
CESTGMT/UCTPDTEDTTW / CSTJST
11
13:0011:00Opening & WelcomeFranziska Heintel4:007:0019:0020:00
12
13:1011:10Solidity 2020 RoadmapChris ReitwiessnerLightning Talk4:107:1019:1020:10
13
Lorem ipsum dolor sit amet, consetetur sadipscing elitr, sed diam nonumy
14
13:3011:30Introduction to the K Framework and KSolidityRikard Hjort and Shang-Wei LinLightning Talk4:307:3019:3020:30
15
Learn about the K's background, and the Solidity semantics in the K framework.
16
13:5011:50Solc-verify, a source-level formal verification tool for Solidity smart contractsÁkos HajduTalk4:507:5019:5020:50
17
Solc-verify is a source-level formal verification tool for Soldity smart contracts, developed in collaboration with SRI International. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code. This enables solc-verify to effectively reason about high-level functional properties while modeling low-level language semantics (e.g., the memory model) precisely. The contract properties, such as contract invariants, loop invariants, function pre- and post-conditions and fine grained access control can be provided as in-code annotations by the developer. This enables automated, yet user-friendly formal verification for smart contracts.
18
14:2012:20Certora: Keeping your code secure forever: Move Fast and Break NothingShmuel SagivTalk5:208:2020:2021:20
19
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.
20
14:5012:50dType: distributed typing & Lens: functional programming lensing in Ethereum 1.x and 2.0Loredana CirsteaTalk5:508:5020:5021:50
21
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.
22
15:2013:20Thoughts on Language Design and FragmentationAlex BeregszasziLightning Talk6:209:2021:2022:20
23
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).
24
15:4013:40SafeMath by defaultChris ReitwiessnerOpen Discussion
https://hackmd.io/@dr56UxqwTjO-0LGQ1GS5Lw/B1QkhYTOI
6:409:4021:4022:40
25
The SafeMath library is commonplace among smart contracts and it makes sense to flag a runtime failure in case of arithmetic overflow as we already do for division by zero.
Since the checks have been implemented already for the Yul code generator, we can re-use them in the legacy code generator.
The idea is to provide a syntactic "unchecked { ... }"-area where overflow checks are not performed.

Since overflow failures can lead to a denial-of-service, developers still have to be aware of the exact situations in which overflows could occur.
The main open questions in this area are:
- should the error cause a revert or an invalid opcode?
- should there be a way to disable the checks on a whole source file?
- should we provide fine-grained access about which checks to disable (overflow, underflow, division by zero, array out of bounds, ...)?
26
16:1014:10SHORT BREAK (hang out in the lobby if you like)7:1010:1022:1023:10
27
16:2514:25Libraries 2.0Chris ReitwiessnerOpen Discussion
https://hackmd.io/@franzihei/BJn0z5pdU
7:2510:2522:2523:25
28
Libraries are the main way in Solidity to make use of the delegatecall opcode, but they are not very popular among developers.
Are deployed libraries re-used across multiple projects? Would it help to make the address changeable at runtime? How would that work? Is there any other problem with libraries?
Should libraries allow inheritance or state variables? Is there a better way to associate e.g. a data structure with library code similar to rust's ""impl"" keyword?
How can libraries make it possible to split a contract's code across multiple addresses to overcome the code size barrier?
29
17:1015:10Introduction to Yul+Nick DodsonTalk8:1011:1023:100:10
30
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
31
17:4015:40New features for YulAlex BeregszasziOpen Discussion
https://hackmd.io/@franzihei/SyIeE5TO8
8:4011:4023:400:40
32
Yul is a language that has developed out of the loose inline assembly introduced in Solidity 0.3.1. Since then it has come a long way and proven its usefulness. Earlier this year, we completed the type checking and are actively using that feature in the compilation pipeline to webassembly. Fuel Labs recently published an extension of Yul called Yul+ that adds several features.

This session is about discussing potential new features for Yul (and thus Solidity inline assembly):
- user-defined types - how would conversions work?
- stricter built-in type system for the EVM dialect: memory / storage and calldata pointers, address?
33
18:1016:10SOLL Compiler (for YUL and Solidity)Michael YuanLightning Talk9:1012:100:101:10
34
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.
35
18:3016:30Upgradable contractsChris ReitwiessnerOpen Discussion
https://hackmd.io/@franzihei/ByBTVcpuL
9:3012:300:301:30
36
Upgradability is a common topic for smart contracts. Yet there is no real support by the Solidity language or compiler. This open discussion group will be mostly concerned with gathering feedback about the various techniques currently used for upgradable and proxy contracts and how this could be streamlined by the Solidity language or supported by the Solidity compiler.
37
19:3017:30SHORT BREAK (hang out in the lobby if you like)10:3013:301:302:30
38
19:5017:50Fixed point typesChris ReitwiessnerOpen Discussion
https://hackmd.io/@franzihei/ry7kn5auI
10:5013:501:502:50
39
Fixed point types should allow a safe and straightforward way to work with non-integer values. They have been proposed and partly implemented for Solidity for a long time. The latest push in that direction was halted due to concerns from the community. We would like to take the Solidity Summit as an opportunity to get more feedback from the broader community: Would you use fixed point types? Which value range do you need? Should we use decimal or binary fixed point types?
40
20:2018:20Tracking mapping keys with the Truffle DebuggerHarry AltmanTalk11:2014:202:203:20
41
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.
42
20:5018:50Truffle Debugger Demo and Debugging Data DiscussionNick D'Andrea and Chris ReitwiessnerOpen Discussion
https://hackmd.io/@franzihei/rkJ_o9adU
11:5014:502:503:50
43
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 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 decypher 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.
46
21:3519:35End of Day 1 - Good night Europe!13:0016:004:005:00
47
48
Let's stay in touch!
49
50
Tweet: @solidity_lang
51
Read: solidity.ethereum.org
52
Chat: gitter.im/ethereum/solidity
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102