ETHEncodingLean

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).

Encodings

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

RLP

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]

SSZ

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 2 0x1234)
-- .ok [0x34, 0x12]

#eval SSZ.serialize
  (SSZ.Value.vector (.uint 2) 2
    [SSZ.Value.uint 2 1, SSZ.Value.uint 2 2])
-- .ok [0x01, 0x00, 0x02, 0x00]

#eval SSZ.hashTreeRoot SSZ.SHA256.hash (SSZ.Value.boolean true)

Ethereum Foundation test vectors

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.gz release 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

Tests

lake build Test
lake test

It 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.

Structure

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

Specification baseline

• Ethereum Yellow Paper, Appendix B
• Ethereum execution tests, RLPTests
• Ethereum consensus SSZ specification v1.6.1
• SSZ Merkle proof specification v1.6.1

License

MIT