Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of smart contract state machines. Towards this end, we extend temporal stream logic (TSL) with universally quantified parameters over infinite domains. Parameterized TSL is a convenient logic to specify the temporal control flow, i.e., the correct order of transactions, as well as the data flow of the contract's fields. We develop a two-step approach that 1) synthesizes a finite representation of the - in general - infinite-state system and 2) splits the system into a compact hierarchical architecture that enables efficient handling of the state machine in Solidity. We implement the approach in our tool ScSynt, which leverages efficient symbolic algorithms based on the observation that smart contract specifications naturally fall into the safety fragment. As a result, ScSynt synthesizes correct-by-design Solidity code from various specifications within seconds.

翻译：智能合约是多方协议的小型但高度易错程序。我们提出一种反应式综合方法，用于自动构建智能合约状态机。为此，我们将时间流逻辑（TSL）扩展至包含无限域上的全称量化参数。参数化TSL是一种便捷的逻辑，用于规约时间控制流（即交易的正确顺序）以及合约字段的数据流。我们开发了一种两步法：1）综合出一般无限状态系统的有限表示；2）将该系统分解为紧凑的分层架构，从而在Solidity中高效处理状态机。我们在工具ScSynt中实现了该方法，其基于智能合约规约自然属于安全片段的观察，利用高效的符号算法。最终，ScSynt可在数秒内从各种规约综合出正确性有保证的Solidity代码。