Pure Lean 4 implementations of Ethereum Recursive Length Prefix (RLP), the Solidity ABI, and Simple Serialize (SSZ). There is no FFI, no opaque definition, and no project-defined axiom. Most proofs are kernel checked; the theorems that use native_decide additionally trust Lean's generated-code evaluator (Lean.ofReduceBool/Lean.trustCompiler).
| Encoding | Purpose | Files |
|---|---|---|
| RLP | Ethereum execution-layer recursive byte/list encoding | RLP.lean + RLP/Proofs.lean |
| ABI | Solidity ABI encoding, strict decoding, signatures, and selectors | ABI/ + Keccak256.lean |
| SSZ | Ethereum consensus-layer serialization | SSZ/Core.lean + SSZ/Validity.lean |
| SSZ hash-tree-root | Schema-directed SSZ Merkleization | SSZ/HashTreeRoot.lean |
| SSZ Merkle proofs | Generalized indices, branches, and multiproofs | SSZ/Merkle.lean |
| SSZ progressive types | Progressive lists, bitlists, containers, and compatible unions | SSZ/Progressive.lean |
| SHA-256 | Pure hash implementation used by SSZ Merkleization | SSZ/SHA256.lean |
The RLP codec handles byte strings, lists, and natural numbers. It rejects noncanonical input and includes proofs for round trips, injectivity, and canonical encoding.
Raw RLP and integer interpretation are deliberately separate. The byte string 0x00 is valid raw RLP, but it is rejected as a nonminimal integer encoding.
import ETHEncodingLean.RLP
open ETHEncodingLean
#eval RLP.encode (.bytes [0x64, 0x6f, 0x67])
-- [0x83, 0x64, 0x6f, 0x67]#eval RLP.decode [0xc8, 0x83, 0x63, 0x61, 0x74,
0x83, 0x64, 0x6f, 0x67]
-- .ok (.list [.bytes "cat", .bytes "dog"])#eval RLP.encodeNat 1024-- [0x82, 0x04, 0x00]The SSZ codec supports the core and progressive consensus types, strict offset decoding, hash-tree roots, Merkle proofs, and SHA-256. Its proofs cover round trips, canonical encoding, sizes, and proof verification.
import ETHEncodingLean.SSZ
open ETHEncodingLean
#eval SSZ.serialize (SSZ.Value.uint 20x1234)
-- .ok [0x34, 0x12]#eval SSZ.serialize
(SSZ.Value.vector (.uint 2) 2
[SSZ.Value.uint 21, SSZ.Value.uint 22])
-- .ok [0x01, 0x00, 0x02, 0x00]#eval SSZ.hashTreeRoot SSZ.SHA256.hash (SSZ.Value.boolean true)The Ethereum Foundation vectors are implemented with a nonzero exit status on any mismatch: https://github.com/ethereum/tests/tree/develop/RLPTests
- All 28 valid cases from
ethereum/tests/RLPTests/rlptest.json - All 26 invalid cases from
ethereum/tests/RLPTests/invalidRLPTest.json - A pinned decoded selection of valid and invalid SSZ fixtures from the consensus-specs v1.6.1
general.tar.gzrelease asset - SSZ fixture checks include decoding, rejection, and hash-tree roots
- Targeted regression vectors cover ABI worked examples, strict decoding, progressive SSZ packing, compatible-union legality, optional-union roots, SHA-256, and Keccak-256
lake build Test
lake testIt follows ETHCryptoLean's root Test.lean and vectors/ conventions. Unlike a print-only test runner, these tests throw on failure, so CI cannot report success after a failed vector.
ETHEncodingLean/
Bytes.lean Shared byte and endian operations
RLP.lean RLP values, encoder, and strict decoder
RLP/
Proofs.lean RLP correctness and canonicality theorems
SSZ.lean SSZ aggregate import
SSZ/
Core.lean Schemas, values, serialization, deserialization
Fuel.lean Fuel stability and offset/splitting proofs
Validity.lean Semantic validity and codec correctness
Merkle.lean Merkleization and proof APIs
HashTreeRoot.lean Schema-directed hash-tree-root
SHA256.lean Pure SHA-256
Progressive.lean Progressive SSZ extensions
ABI/
Core.lean ABI types and encoder
Decode.lean Strict decoder and codec theorems
Signature.lean Canonical signature spelling
Selector.lean Keccak-256 function selectors
vectors/
rlp/ Official valid and invalid RLP JSON corpora
ssz/ Pinned decoded consensus SSZ fixtures
Tests/
OfficialVectors.lean JSON loaders and official-vector runners
Main.lean Hard-failing executable test suite
Test.lean Root test entry point
- Ethereum Yellow Paper, Appendix B
- Ethereum execution tests, RLPTests
- Ethereum consensus SSZ specification v1.6.1
- SSZ Merkle proof specification v1.6.1
MIT