Metadata-Version: 2.4
Name: ethlib
Version: 0.2.0
Summary: Ethereum specifications, written in Lean
Author: ethereum
License-Expression: CC0-1.0
Project-URL: homepage, https://github.com/ethereum/ethlib
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Provides-Extra: test
Requires-Dist: pytest==9.0.3; extra == "test"
Requires-Dist: ruamel.yaml==0.19.1; extra == "test"
Requires-Dist: py_ecc==8.0.0; extra == "test"
Dynamic: license-file

# EthLib

Formally verified Ethereum primitives, written in Lean. EthLib is intended to be
the shared home for Ethereum definitions and proofs, so that Lean projects can
build on a common implementation instead of each maintaining its own. Some of
these primitives can also be used by Ethereum clients via bindings. Clients may
use the bindings temporarily until a native implementation exists, or
permanently if the performance of this library is sufficient.

## Primitives

### Cryptography

- [BLS12-381 signatures](EthLib/Cryptography/Bls/)
- [KZG polynomial commitments](EthLib/Cryptography/Kzg/)
- [XMSS signatures](EthLib/Cryptography/Xmss/)

## Contributing

### Prerequisites

Install [elan](https://github.com/leanprover/elan):

```bash
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
```

Download [Mathlib](https://github.com/leanprover-community/mathlib4):

```bash
lake exe cache get
```

### Building

Compile the primitives and check every proof:

```bash
lake build
```

XMSS serialization uses the pinned Lean codec from [ethereum/ssz-specs](https://github.com/ethereum/ssz-specs).
The codec builds with this project's Lean 4.29.1 toolchain.
When refreshing dependencies, use `lake --keep-toolchain update` to retain the toolchain matching Mathlib.

### Testing

Run the test suite:

```bash
python3 -m venv .venv
source .venv/bin/activate
pip install -e '.[test]'
pytest
```
