Ethereum's Recursive Length Prefix in ACL2
Alessandro Coglio (Kestrel Institute)
TL;DR
This paper presents a formal specification and verified implementation of Ethereum's Recursive Length Prefix encoding in ACL2, enhancing the reliability and documentation of Ethereum's data encoding processes.
Contribution
It provides the first formal ACL2-based specification and verified decoder for Ethereum's RLP, improving correctness and documentation.
Findings
Formal ACL2 specification of RLP encoding
Verified RLP decoding implementation in ACL2
Enhanced Ethereum documentation and testing suite
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Cryptography and Data Security · Distributed systems and fault tolerance