ACL2 中的以太坊递归长度前缀
计算机科学中的逻辑
2020-09-30 v1
摘要
递归长度前缀（RLP）用于编码以太坊中的多种数据，包括交易。本文所述工作提供了 RLP 编码的形式化规范以及 RLP 解码的已验证实现，这些均在 ACL2 定理证明器中开发。该工作已促使以太坊文档得到改进，并增加了以太坊测试套件的内容。
引用
@article{arxiv.2009.13769,
title = {Ethereum's Recursive Length Prefix in ACL2},
author = {Alessandro Coglio},
journal= {arXiv preprint arXiv:2009.13769},
year = {2020}
}
备注
In Proceedings ACL2 2020, arXiv:2009.12521