Hornet节点与Hornet DSL：比特币共识的最小化可执行规范

比特币的共识规则编码在其参考客户端的实现中：“代码即规范”。然而，由于副作用、可变状态、并发和遗留设计，该代码不适合进行形式化验证。一个独立的形式化规范将能够跨参考客户端的版本以及针对新的客户端实现进行验证，通过降低共识分裂漏洞的风险来增强去中心化。然而，鉴于比特币共识逻辑的复杂性，这样的规范长期以来被认为是难以实现的。我们展示了一个紧凑、可执行、声明式的C++比特币共识规则规范，它能在单线程上几小时内将主网同步至最新区块。我们还引入了专门设计的Hornet领域特定语言 (DSL)，用于无歧义地编码这些规则以供执行，从而实现形式化推理、共识代码生成和AI驱动的对抗性测试。我们的规范驱动客户端Hornet Node为参考客户端提供了一个现代且模块化的补充。其清晰、惯用的风格使其适合教育，而其性能使其非常适合实验。我们强调了其架构贡献，如分层设计、高效的数据结构和严格的关注点分离，并辅以生产质量的代码示例。我们认为，Hornet Node和Hornet DSL共同为比特币共识的纯粹、形式化、可执行规范提供了首条可信路径。