一句话：报告用 QuickChick 对高阶智能合约语言实现进行基于性质的随机测试，验证类型安全与编译器分析可靠性并发现缺陷。
本文是一篇经验报告，介绍在面向现代区块链、日均用户数千的高阶智能合约语言开发中，使用基于性质的测试（property-based testing）自动生成随机输入来检验可执行程序规约。作者将建立在 Coq 证明助手上的 QuickChick 框架集成到以 OCaml 实现的真实语言实现中，讨论为混合纯函数式与命令式计算、并带运行时资源计量的高阶合约语言生成良类型程序所面临的挑战。文中描述了所测试的语言实现性质及所需语义测试框架，范围从标准类型安全到优化编译器所用控制流与类型流分析的可靠性。最后列出 QuickChick 发现和重新发现的缺陷，并讨论其严重性与潜在影响。
We describe our experience of using property-based testing---an approach for automatically generating random inputs to check executable program specifications---in a development of a higher-order smart contract language that powers a state-of-the-art blockchain with thousands of active daily users. We outline the process of integrating QuickChick---a framework for property-based testing built on top of the Coq proof assistant---into a real-world language implementation in OCaml. We discuss the challenges we have encountered when generating well-typed programs for a realistic higher-order smart contract language, which mixes purely functional and imperative computations and features runtime resource accounting. We describe the set of the language implementation properties that we tested, as well as the semantic harness required to enable their validation. The properties range from the standard type safety to the soundness of a control- and type-flow analysis used by the optimizing compiler. Finally, we present the list of bugs discovered and rediscovered with the help of QuickChick and discuss their severity and possible ramifications.
@article{paperbot1510,
title = {Random testing of a higher-order blockchain language (experience report)},
author = {Tram Hoang and Anton Trunov and Leonidas Lampropoulos and Ilya Sergey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547653}
}