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 the implementation of the state machine in Solidity. We implement the approach in our prototype tool SCSynt, which - within seconds - automatically constructs Solidity code that realizes the specified control flow.

翻译：智能合约是小型但极易出错的程序，用于实现多方之间的协议。我们提出一种反应式综合方法，用于自动构建智能合约状态机。为此，我们将时间流逻辑（TSL）扩展至具有无限域上全称量化参数的形式。带参数的时间流逻辑是一种便捷的逻辑体系，可用于规约时间控制流（即交易的正确顺序）以及合约字段的数据流。我们开发了一种两步方法：1）综合出——通常为——无限状态系统的有限表示；2）将系统分解为紧凑的分层架构，从而能够在Solidity中实现状态机。我们通过原型工具SCSynt实现了该方法，该工具可在数秒内自动构建实现指定控制流的Solidity代码。