Unified Binary Tree (UBT)

A Rust implementation of EIP-7864: Ethereum state using a unified binary tree.

Overview

This crate provides a binary tree structure intended to replace Ethereum's hexary patricia trees. Key features:

• Single tree: Account and storage tries are merged into a single tree with 32-byte keys
• Code chunking: Contract bytecode is chunked and stored in the tree
• Data co-location: Related data (nonce, balance, first storage slots, first code chunks) are grouped together in 256-value subtrees to reduce branch openings
• ZK-friendly: Designed for efficient proving in ZK circuits
• Parallel hashing: Uses rayon for concurrent stem hash computation (enabled by default)
• Incremental updates: O(D*C) root updates instead of O(S log S) full rebuilds
• Formally verified: Core operations proven correct using the Rocq proof assistant

Tree Structure

The tree uses 32-byte keys where:

• First 31 bytes: stem (defines the subtree path)
• Last byte: subindex (position within the 256-value subtree)

Node Types

Tree Embedding (State Layout)

Each Ethereum account maps to tree keys as follows:

Storage slots >= 64 and code chunks >= 128 are stored in separate stems.

Usage

use ubt::{UnifiedBinaryTree, TreeKey, Blake3Hasher, B256};

// Create a new tree
let mut tree: UnifiedBinaryTree<Blake3Hasher> = UnifiedBinaryTree::new();

// Insert a value
let key = TreeKey::from_bytes(B256::repeat_byte(0x01));
tree.insert(key, B256::repeat_byte(0x42));

// Get the root hash
let root = tree.root_hash();

// Retrieve a value
let value = tree.get(&key);

Batch Operations

For inserting many values efficiently, use batch operations:

use ubt::{UnifiedBinaryTree, TreeKey, Blake3Hasher, B256, Stem};

// Pre-allocate for known capacity
let mut tree: UnifiedBinaryTree<Blake3Hasher> = UnifiedBinaryTree::with_capacity(1_000_000);

// Batch insert (single tree rebuild at the end)
let entries: Vec<(TreeKey, B256)> = vec![/* ... */];
tree.insert_batch(entries);

Streaming Tree Builder (Memory-Efficient)

For large migrations where memory is constrained, use the streaming builder:

use ubt::{StreamingTreeBuilder, TreeKey, Blake3Hasher, B256, Stem};

// Entries MUST be sorted by (stem, subindex)
let mut entries: Vec<(TreeKey, B256)> = vec![/* ... */];
entries.sort_by(|a, b| (a.0.stem, a.0.subindex).cmp(&(b.0.stem, b.0.subindex)));

let builder: StreamingTreeBuilder<Blake3Hasher> = StreamingTreeBuilder::new();
let root = builder.build_root_hash(entries);

The streaming builder computes the root hash without keeping the full tree in memory.

Incremental Mode

For block-by-block state updates where only a small subset of stems change:

use ubt::{UnifiedBinaryTree, Blake3Hasher, TreeKey, B256};

let mut tree: UnifiedBinaryTree<Blake3Hasher> = UnifiedBinaryTree::new();
// ... initial inserts ...
tree.root_hash(); // Full rebuild

// Enable incremental mode for subsequent updates
tree.enable_incremental_mode();
tree.root_hash(); // Populates intermediate node cache

// Future updates reuse cached intermediate hashes: O(D*C) hashing work
// (root_hash() still does O(S log S) stem sort; D=248, C=changed stems)
tree.insert(TreeKey::from_bytes(B256::repeat_byte(0x02)), B256::repeat_byte(0x43));
tree.root_hash(); // Only recomputes paths to changed stems

See docs/incremental-updates.md for benchmarks and when to use each mode.

Working with Accounts

use ubt::{AccountStem, BasicDataLeaf, chunkify_code, Address, U256};

let address = Address::repeat_byte(0x42);
let account = AccountStem::new(address);

// Get tree key for basic data (nonce, balance)
let basic_data_key = account.basic_data_key();

// Get tree key for storage slot
let storage_key = account.storage_key(U256::from(0));

// Chunkify contract code
let bytecode = vec![0x60, 0x80, 0x60, 0x40, 0x52];
let chunks = chunkify_code(&bytecode);

Features

To disable default features:

[dependencies]
ubt = { version = "0.2", default-features = false }

To run the simulation stress-test binary:

cargo run --bin simulate --features simulate -- --seed 12345 --ops 10000

Hash Function

Note: The hash function is not finalized per EIP-7864. This implementation uses BLAKE3 as a reference. Candidates include Keccak and Poseidon2.

The hasher is abstracted via the Hasher trait, allowing different implementations:

use ubt::{Hasher, Blake3Hasher};

// Custom hasher implementation
struct MyHasher;
impl Hasher for MyHasher {
    // ... implement hash methods
}

Formal Verification Status

Status: VERIFICATION COMPLETE (December 2024)

This crate includes formal verification using rocq-of-rust and the Rocq proof assistant.

Key Metrics

Operation Verification Summary

Proven Properties

Note: Properties marked "Formal model" are proven in the Rocq formal verification but the corresponding Rust APIs (batch verification, accumulators) are not yet exposed.

Axiom Classification

Trust assumptions:

• Monad Laws: Standard mathematical properties (high confidence)
• RocqOfRust Translation: Assumes correct Rust-to-Rocq translation
• HashMap/Iterator Semantics: Standard library behavior

Future work: Full M monad interpreter to eliminate simulation axioms (tracked in rocq-of-rust-interp#1).

See formal/docs/VERIFICATION_SUMMARY.md for complete verification summary.

Building Proofs

# Activate Rocq environment
eval $(opam env --switch=rocq-9)

# Build proofs
cd formal
make

# Build linking layer
make linking

# Run axiom audit
bash scripts/count_axioms.sh

See formal/README.md for detailed setup instructions.

Verification Structure

formal/
├── specs/           # Mathematical specifications
├── simulations/     # Idiomatic Rocq implementation + security proofs
├── proofs/          # Correctness proofs + QuickChick tests
├── linking/         # Rust-to-Rocq refinement (complete)
├── lib/             # Reusable libraries (submodules)
└── src/             # Auto-generated translation (24k lines)

Dependencies

• rocq-of-rust - Rust to Rocq translation
• rocq-of-rust-interp - M monad interpreter library (submodule)

Comparison with MPT

Project Structure

ubt/
├── src/             # Rust implementation
│   ├── tree.rs      # Main tree structure
│   ├── node.rs      # Node types
│   ├── key.rs       # Tree keys and stems
│   ├── hash.rs      # Hash trait and implementations
│   ├── embedding.rs # State embedding
│   ├── streaming.rs # Streaming tree builder
│   └── ...
├── formal/          # Formal verification
│   ├── specs/       # Rocq specifications
│   ├── simulations/ # Idiomatic Rocq
│   ├── proofs/      # Correctness proofs
│   └── src/         # Translated Rust
└── spec/            # EIP-7864 specification

Contributing

When contributing to this project, please follow these style guidelines:

• No emojis: Use ASCII symbols instead of unicode emojis
  • Use [x] or (done) instead of checkmarks
  • Use [!] or (warn) instead of warning signs
  • Use -> instead of arrows

License

Licensed under either of Apache License, Version 2.0 or MIT license at your option.