论文标题
以太坊的递归长度前缀ACL2
Ethereum's Recursive Length Prefix in ACL2
论文作者
论文摘要
递归长度前缀（RLP）用于编码以太坊中的各种数据，包括交易。本文所述的工作提供了RLP编码的正式规范，并在ACL2定理供摩鞋中开发的RLP解码实现了经过验证的实现。这项工作导致了以太坊文档和以太坊测试套件的增加的改进。
Recursive Length Prefix (RLP) is used to encode a wide variety of data in Ethereum, including transactions. The work described in this paper provides a formal specification of RLP encoding and a verified implementation of RLP decoding, developed in the ACL2 theorem prover. This work has led to improvements to the Ethereum documentation and additions to the Ethereum test suite.
