编程语言与工具

Solidity

那天主会场Erik Kundt分享了Solidity的最新状况，对0.5.0的新特性做了一些介绍。在写这篇总结时solidity0.5.0也终于发布了: https://github.com/ethereum/solidity/releases/tag/v0.5.0

当时Solidity的核心团队几个人也都在现场，回答听众提问的时候看到solidity项目负责人Christian Reitwiessner在台下做了回复。

对于0.5.0新特性主要围绕下面几点：

• Explicit types
• Explicit visibility
• Explicit data locations
• Scoping rules for function local variables
• New constructor syntax
• emit for events
• address payable

总体而言就是更加严格了，增加了更多约束，让编译器能提前发现问题。这些例子我没有一一记录，感兴趣的话等youtube上视频出来了大家可以再去看一下视频。

函数的可见性变成了强制的，如下几个function的可见性修饰符是必须的：

contract Test{
  address owner;
  function Test() public {
    initialize();
  }
  function initialize() internal {
    owner = msg.sender;
  }
  function withdraw() public {
    //...
  }
}

实际上在0.4.24版本下对于可见性修饰符已经给出编译时警告了，对构造函数也建议使用constructor替代跟合约同名的函数了，只不过不是强制。

在0.5.0版本里 var已经不再允许使用，因为它可能在类型推导时产生问题。在0.4版本里它不需要SMTChecker编译器就已给出warning了：

 ➜  cat a.sol
pragma solidity ^0.4.24;

contract C {

  function f() public pure returns (uint) {
    for ( var i = 0; i < 2000; i++) {
      //...
    }
  }
}

 ➜  solc a.sol
a.sol:6:11: Warning: Use of the "var" keyword is deprecated.
    for ( var i = 0; i < 2000; i++) {
          ^---^
a.sol:6:11: Warning: The type of this variable was inferred as uint8, which can hold values between 0 and 255. This is probably not desired. Use an explicit type to silence this warning.
    for ( var i = 0; i < 2000; i++) {
          ^-------^

但对这个例子稍作改变，不使用var而是现实的类型声明，但在类型值边界存在判断问题的话就必须通过SMTChecker才能发现了：

 ➜  cat b.sol
pragma solidity ^0.4.24;
pragma experimental SMTChecker;

contract C {

  function f() public pure returns (uint) {
    for ( uint i = 200; i >= 0; i--) {
      //...
    }
  }
}

 ➜  solc b.sol
b.sol:7:25: Warning: For loop condition is always true.
    for ( uint i = 200; i >=0; i--) {
                        ^---^
b.sol:7:32: Warning: Underflow (resulting value less than 0) happens here for:
  value = (- 1)
  i = 0

    for ( uint i = 200; i >=0; i--) {
                               ^-^

对于存储引用必须初始化。

Yul之前也被称为Julia或Iulia是为了编译到各种不同后端而设计的中间语言，各类合约语言都先编译为Yul，这样不管后端是EVM还是eWASM都能很平滑。为Yul构建高级的优化器阶段也将会很容易。Yul作为通用的中间语言,本身不提供操作符，如果目标平台是EVM则操作码将作为内置函数提供，如果后端平台发生了变化可以重新实现它们。参看它的文档。

SMTChecker

在第二天有一个专门介绍SMTChecker的小会场，看一个例子：

 ➜  cat c.sol
pragma solidity ^0.4.24;
pragma experimental SMTChecker;

contract C {

  uint c;
  function f(uint x) public pure returns (uint) {
    return x * 42;
  }

  function g(uint a, uint b) public view {
    require(a >= b);
    require(b >= c);
    assert(f(a) >= f(c));
  }
}

上面的例子如果不使用SMTChecker编译过程不会给出任何警告，开启后则会看到详细的警告：

 ➜  solc c.sol
c.sol:8:12: Warning: Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here for:
  value = 0x01000000000000000000000000000000000000000000000000000000000000001a
  x = 0x0618618618618618618618618618618618618618618618618618618618618619
  c = 0

    return x * 42;
           ^----^
c.sol:14:12: Warning: Internal error: Expression undefined for SMT solver.
    assert(f(a) >= f(c));
           ^--^
c.sol:14:20: Warning: Internal error: Expression undefined for SMT solver.
    assert(f(a) >= f(c));
                   ^--^
c.sol:14:5: Warning: Assertion violation happens here for:
  a = 0
  b = 0
  c = 0

    assert(f(a) >= f(c));
    ^------------------^

SMTChecker最大优势是Solidity编译器直接集成了它。

AxLang

Athanasios Konstantinidis分享了Axoni公司的 AxLang 语言。它是一门基于Scala的带有形式化验证的智能合约语言，将scala语法树转换为中间语言，做健壮性分析和优化，然后再编译到后端EVM。我之前没有听说过，这家公司好像主要是面向金融领域。他们在devcon4的视频有人贴在了这里，感兴趣可以自己去看。

S-gram

S-gram是一个用于智能合约的Statistical Linter，这个topic是由清华大学的刘浛分享的。会后我们交流了一下，他当前在清华读博士后，主要方向在系统和安全领域。

Formality

Formality是一门新的函数式、无垃圾回收、面向EVM和GPU的形式验证语言，号称很快。因为给自己贴的标签太多，对他们的发展和进度不是很乐观。

ZeppelinOS

ZepplinOS 团队分享了一些合约开发的实用技巧，对于合约的升级问题可以借鉴。

其他

有一家名叫trail of bits的安全公司做了一个《区块链的验尸报告：selfdestructs分析》的分享，视角比较独特，他们在devcon4上有好几个安全相关的分享，感兴趣可以去找找他们的ppt。

Vyper 语言的开发者也有做一个分享，这个python风格的合约语言似乎欢迎度挺高，不过没有去这个会场，无法给出太多的信息。

面向合约的编程语言这几年百花齐放，毕竟还未形成一家独大的局面。另外之前看到devcon1上有一个《Monadic Design Patterns for the Blockchain》的分享也很有趣，可以在youtube上找到。

状态通道与Layer2

在devcon4的前一天晚上，Nervos在一家支付比特币的酒吧里组织过一个Layer2的聚会，参与的人也很多，其中有不少是投资人。

因为时差那天晚上没怎么听进去，celer的董沫主持，Jan做了一个简单的分享，介绍了Nervos是专为Layer2设计的 Layer1。在到布拉格之前从杭州到上海的大巴里碰到过Jan，当时简单聊过一些Nervos；他们设计的很独特，Layer1做的事情比较少，鼓励用户把计算放到Layer2上去；在Layer1的存储总量是有上限的，通过经济模型来调节在Layer1上的存储使用成本；共识方面仍采用POW，数据采用UTXO模型。

当时坐在我傍边的是loom network的开发者，一边很快捷的在tmux下敲打命令，一边去github他们的产品issue下回答问题。我去查了一下才知道loom是一套正式上线的以太坊第2层扩展解决方案。是一个DPoS侧链网络，允许高度可扩展的游戏和面向用户的 DApp 在其之上运行，同时仍然受到以太坊的安全支持。似乎在游戏领域很有名，在medium上有一个中文的博客：https://medium.com/@loomnetworkcn

引用节点研究中心蔡晨曦的这篇关于状态通道的分析里对各个项目方的一个介绍。基本上这次devcon4这些状态通道的项目方都来了，看得出是Layer2是当下寻求突破的共识，项目方们也都在相互追赶发力，不排除在可预期的时间内会有不错的效果。

SpankChain

SpankChain的几个人都染着红头发，很容易辨识他们。讲了他们被黑客攻击的过程，以及怎么又把钱给要了回来。支付通道这块主要是与Connext合作的，在后续计划里SpankChain打算集成Gnosis的多重签名钱包。

Perun

在波兰语里Perun是闪电之神，项目方是个学院派背景。他们的主要技术是虚拟通道(virtual channels)采用证明驱动(proof-driven)的方式实现。Virtual channels在Ledger state channels(一种双向支付通道)基础之上，在中心辐射(hub-and-spoke)拓扑下对两个节点(spoke)之间创建一个虚拟通道使得它们之间可以不依赖中心节点(hub)而进行交易。相对于Ledger state channel在创建和关闭的时候都在链上执行，只有在执行的时候在链下，virtual state channel这三个阶段都在链下执行。

FunFair

FunFair是面向博彩游戏的，他们在状态通道的基础上整合了随机数生成器。他们称之为“命运通道”(Fate Channels)，“命运通道”的证明机制可以逐步生成一个确定的且不可预测的随机数序列。更多信息可以通过他们的白皮书了解。

Celer

在Celer的主页上引用阿西莫夫的解释，celeritas是拉丁文速度的意思。Celer是分层架构最底层是通道(cChannel)，中间是路由层(cRouter)，上层是面向应用(cOS)。团队的背景比较豪华，核心成员基本都是名校博士，有博弈论和系统架构方面的工程背景。看到他们在路由层做了很多的事情，正是他们擅长的领域。在经济激励设计上，一方面是对流动性的激励，设计了多种激励模式(包含Proof of Liquidity Commitment和Liquidity Backing Auction)；另一方面是对状态守护(State Guardian)提供激励，这也是Layer2普遍采用的机制，让参与方参与检查或校验来获取激励。在会场碰到了Celer的co-founder李小舟，简单交流了一下。上周Celer团队来杭州时董沫和其他团队成员也过来给我们做了一个分享。

其他

光环最显著的plasma项目，因为时间冲突这次没有去听，loom也有个基于plasma cash的分享。当前二层网络是亟待突破的一个阶段，大家都在为产品的用户体验寻求突破，这也成了整个生态当下最显著的痛点，逼迫着Layer2加快发展。我们也在密切关注这个方向的技术进展。