在 Agda 中对 Bitcoin 建模

我们在交互式定理证明器 Agda 中给出了 Bitcoin 区块链的两种模型。第一种基于简单的银行账户模型，但具有多输入与多输出的交易。第二种模型对交易进行建模，其直接引用未花费交易输出而非用户账户。由此产生的区块链生成了一棵交易树。该模型使用 Agda 的独特特性之一——扩展形式的归纳-递归得以形式化：交易树与交易的集合被归纳地定义，同时递归地定义未花费交易输出的列表。两种结构均对标准交易、coinbase 交易、交易费、交易中花费方所需签署的确切消息、区块奖励、区块及区块链进行建模，且第二种结构还建模了 coinbase 交易的成熟时间以及 Merkle 树。哈希与密码学操作及其正确性通过公设相应操作来抽象处理。文中指出了如何在 Agda 中对该模型的正确性进行规约与证明。