钱长在(证明)树上:形式化FA1.2账本标准
计算机科学中的逻辑
2021-12-02 v2
摘要
一旦发明了数字资产,你可能需要一个账本来追踪谁拥有什么——以及该账本的接口,以便你的资产用户可以进行交易。在Tezos区块链上,这意味着:一个智能合约(分布式程序),在其状态中存储一个将所有者地址映射到代币数量的账本,以及用于账户交易的标准化入口点。银行做类似的工作——它将账号映射到账户数额并允许用户交易——但作为交换,银行要求信任,它承担维护中心化服务器与人员的开销,它使用专有接口……并且它可能用你的钱投机和/或表现出寻租行为。区块链账本按设计是去中心化、廉价、开放的,并且它不会拿你的代币去押注高风险衍生品(除非你要求)。FA1.2标准是Tezos区块链上账本维护智能合约的开放标准。若干FA1.2实现已经存在。或者它们真的存在?该标准是否合理且完整?这些实现是否正确?它们又究竟是实现的是什么?FA1.2标准以英文撰写,这是一种受湿人脑青睐但 notorious 在转为枯燥无情代码时不完整且模糊的规范语言。本文我们报告将FA1.2标准形式化为Coq规范,以及针对该规范对三个FA1.2兼容智能合约的形式化验证。我们发现了错误并解决了歧义;而且,现在存在一份数学精确且经实战检验的FA1.2账本标准规范。我们将描述FA1.2本身,概述Coq理论的结构——其本身捕捉了开发中一些非平凡且新颖的设计决策——并回顾对这些实现的详细验证。
引用
@article{arxiv.2109.09451,
title = {Money grows on (proof-)trees: the formal FA1.2 ledger standard},
author = {Murdoch Gabbay and Arvid Jakobsson and Kristina Sojakova},
journal= {arXiv preprint arXiv:2109.09451},
year = {2021}
}