Coq 中的智能合约交互

我们给出了 Coq 中智能合约执行的一个模型/可执行规约。我们的形式化允许合约间通信，并通过允许对深度优先执行区块链（如 Ethereum）与广度优先执行区块链（如 Tezos）进行建模，推广了已有工作。我们在 Coq 的函数式语言 Gallina 中表示智能合约程序，相较于其他方法，能更便捷地对具体合约的功能正确性进行推理。特别地，我们以这种风格开发了一个 Congress 合约。该合约——声名狼藉的 DAO 的简化版本——因其与其他合约极其动态的通信模式而引人关注。我们给出了 Congress 行为的高层部分规约，涉及重入（reentrancy），并证明对于所有可能的智能合约执行顺序，Congress 均满足该规约。