From 319ff0a8cd4a9726fbf3238a77fc30c480933ffa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1s=20Gr=C3=BCner?= <47506558+MegaRedHand@users.noreply.github.com> Date: Mon, 6 Jul 2026 11:38:39 -0300 Subject: [PATCH 1/4] docs: add spec deviations page to the book Documents two performance-driven deviations from leanSpec (asynchronous signature aggregation with early stop; attestation scoring on block building) and registers the page in the mdBook SUMMARY under a new Development section so it renders in the book. Source references verified against current code: line numbers and the tier-dependent attestation tie-break (leanSpec #1149). --- docs/SUMMARY.md | 4 ++++ docs/spec_deviations.md | 24 ++++++++++++++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 docs/spec_deviations.md diff --git a/docs/SUMMARY.md b/docs/SUMMARY.md index 2c5a707d..ce8fc3a0 100644 --- a/docs/SUMMARY.md +++ b/docs/SUMMARY.md @@ -13,3 +13,7 @@ - [Metrics](./metrics.md) - [Checkpoint Sync](./checkpoint_sync.md) - [Fork Choice Visualization](./fork_choice_visualization.md) + +# Development + +- [Spec Deviations](./spec_deviations.md) diff --git a/docs/spec_deviations.md b/docs/spec_deviations.md new file mode 100644 index 00000000..a5836b8e --- /dev/null +++ b/docs/spec_deviations.md @@ -0,0 +1,24 @@ +# Spec Deviations + +ethlambda diverges from the [leanSpec](https://github.com/leanEthereum/leanSpec) +reference in a few places, mainly for performance reasons. This page lists those +deviations; each will be fleshed out with rationale, implementation notes, and +trade-offs over time. + +## Asynchronous signature aggregation with early stop + +Aggregation runs off the main BlockChainServer actor loop and stops early once it ran out of time. + +- **ethlambda:** at interval 2 the actor snapshots its state and spawns a `tokio::task::spawn_blocking` worker (`run_aggregation_worker`, `crates/blockchain/src/aggregation.rs:504`). The worker streams each finished group back as an `AggregateProduced` message; the actor loop is never blocked on XMSS work. +- **Early stop:** a `send_after(AGGREGATION_DEADLINE, ...)` timer cancels the session after 750ms (`AGGREGATION_DEADLINE`, `aggregation.rs:33`); the interval is 800ms (`MILLISECONDS_PER_INTERVAL`, `lib.rs:47`), leaving ~50ms for publish/propagation. The worker checks `cancel.is_cancelled()` before each job (`aggregation.rs:519`); in-flight jobs finish, remaining jobs are dropped. +- **leanSpec:** `aggregate()` is called inline and synchronously from `tick_interval` at interval 2 (`forks/lstar/spec.py`). It processes every group with no time budget, no worker, no cancellation. +- **Equivalence:** same XMSS proofs are produced; deviation is scheduling + a partial-result bound, not signature logic. + +## Attestation scoring on block building + +Attestations are scored and selected when packing a block, rather than greedily included as they arrive. + +- **ethlambda:** `select_attestations` (`crates/blockchain/src/block_builder.rs:170`) ranks candidate `AttestationData` entries by tier `Finalize > Justify > Build` (`enum Tier`, `block_builder.rs:473`). The within-tier order is tier-dependent (`EntryScore::ordering_key`, `block_builder.rs:517`): `Finalize`/`Justify` entries already cross 2/3, so newer chain progress leads (target slot, attestation slot, then new-voter count); `Build` entries only add marginal voters, so coverage leads (new-voter count, target slot, then attestation slot). `data_root` is the final deterministic tiebreak in both tiers. Each round picks the best candidate against a projected post-state, up to `MAX_ATTESTATIONS_DATA = 8` entries (`crates/common/types/src/block.rs:109`). +- **leanSpec:** `build_block` iterates entries sorted by `target.slot` (oldest first) and includes the first ones that pass filters (greedy, no scoring), re-running the loop as a fixed point when justification/finalization advances. Same cap: `MAX_ATTESTATIONS_DATA = 8` (`subspecs/chain/config.py`). +- **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order. + From c7c4371af11b832bc77bdeffb4af78e2eea14e58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1s=20Gr=C3=BCner?= <47506558+MegaRedHand@users.noreply.github.com> Date: Mon, 6 Jul 2026 12:50:39 -0300 Subject: [PATCH 2/4] docs: address review feedback on spec deviations - Drop drift-prone line numbers; keep symbol + file references. - Correct the aggregation equivalence: the interval-2 worker snapshots only current-slot raw gossip signatures (skips proof reuse / stale groups) and may emit a partial result on cancellation, so it does not reproduce leanSpec's full aggregate set. Note the subset still yields a valid block. - Clarify the attestation cap is 8 distinct AttestationData entries, with per-entry proofs compacted back to one-per-data later. - Grammar (ran -> runs); trailing-newline cleanup. --- docs/spec_deviations.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/docs/spec_deviations.md b/docs/spec_deviations.md index a5836b8e..3cd159aa 100644 --- a/docs/spec_deviations.md +++ b/docs/spec_deviations.md @@ -7,18 +7,17 @@ trade-offs over time. ## Asynchronous signature aggregation with early stop -Aggregation runs off the main BlockChainServer actor loop and stops early once it ran out of time. +Aggregation runs off the main BlockChainServer actor loop and stops early once it runs out of time. -- **ethlambda:** at interval 2 the actor snapshots its state and spawns a `tokio::task::spawn_blocking` worker (`run_aggregation_worker`, `crates/blockchain/src/aggregation.rs:504`). The worker streams each finished group back as an `AggregateProduced` message; the actor loop is never blocked on XMSS work. -- **Early stop:** a `send_after(AGGREGATION_DEADLINE, ...)` timer cancels the session after 750ms (`AGGREGATION_DEADLINE`, `aggregation.rs:33`); the interval is 800ms (`MILLISECONDS_PER_INTERVAL`, `lib.rs:47`), leaving ~50ms for publish/propagation. The worker checks `cancel.is_cancelled()` before each job (`aggregation.rs:519`); in-flight jobs finish, remaining jobs are dropped. +- **ethlambda:** at interval 2 the actor snapshots the current slot's raw gossip signatures (`snapshot_current_slot_aggregation_inputs`, `crates/blockchain/src/aggregation.rs`) and spawns a `tokio::task::spawn_blocking` worker (`run_aggregation_worker`, `aggregation.rs`). The snapshot deliberately covers only current-slot raw gossip signatures, skipping existing-proof reuse and stale-slot groups so the interval-2 budget is never spent re-aggregating past slots (proof reuse is handled later, at block build). The worker streams each finished group back as an `AggregateProduced` message; the actor loop is never blocked on XMSS work. +- **Early stop:** a `send_after(AGGREGATION_DEADLINE, ...)` timer cancels the session after 750ms (`AGGREGATION_DEADLINE`, `aggregation.rs`); the interval is 800ms (`MILLISECONDS_PER_INTERVAL`, `crates/blockchain/src/lib.rs`), leaving ~50ms for publish/propagation. The worker checks `cancel.is_cancelled()` before each job (`aggregation.rs`); in-flight jobs finish, remaining jobs are dropped. - **leanSpec:** `aggregate()` is called inline and synchronously from `tick_interval` at interval 2 (`forks/lstar/spec.py`). It processes every group with no time budget, no worker, no cancellation. -- **Equivalence:** same XMSS proofs are produced; deviation is scheduling + a partial-result bound, not signature logic. +- **Equivalence:** the per-group XMSS aggregation logic is the same as leanSpec's; the deviations are scheduling (off the actor loop), input scope (current-slot raw gossip only), and a partial-result bound. On cancellation the worker emits only the groups that finished, so a slot may pack fewer aggregates than the synchronous path would; any such subset still yields a valid block, affecting how many votes are included rather than signature validity. ## Attestation scoring on block building Attestations are scored and selected when packing a block, rather than greedily included as they arrive. -- **ethlambda:** `select_attestations` (`crates/blockchain/src/block_builder.rs:170`) ranks candidate `AttestationData` entries by tier `Finalize > Justify > Build` (`enum Tier`, `block_builder.rs:473`). The within-tier order is tier-dependent (`EntryScore::ordering_key`, `block_builder.rs:517`): `Finalize`/`Justify` entries already cross 2/3, so newer chain progress leads (target slot, attestation slot, then new-voter count); `Build` entries only add marginal voters, so coverage leads (new-voter count, target slot, then attestation slot). `data_root` is the final deterministic tiebreak in both tiers. Each round picks the best candidate against a projected post-state, up to `MAX_ATTESTATIONS_DATA = 8` entries (`crates/common/types/src/block.rs:109`). +- **ethlambda:** `select_attestations` (`crates/blockchain/src/block_builder.rs`) ranks candidate `AttestationData` entries by tier `Finalize > Justify > Build` (`enum Tier`, `block_builder.rs`). The within-tier order is tier-dependent (`EntryScore::ordering_key`, `block_builder.rs`): `Finalize`/`Justify` entries already cross 2/3, so newer chain progress leads (target slot, attestation slot, then new-voter count); `Build` entries only add marginal voters, so coverage leads (new-voter count, target slot, then attestation slot). `data_root` is the final deterministic tiebreak in both tiers. Each round picks the best candidate against a projected post-state, up to `MAX_ATTESTATIONS_DATA = 8` distinct `AttestationData` entries (`crates/common/types/src/block.rs`); a winning entry may carry several proofs, which a later compaction step (`compact_attestations`, `block_builder.rs`) merges back to one per `AttestationData`. - **leanSpec:** `build_block` iterates entries sorted by `target.slot` (oldest first) and includes the first ones that pass filters (greedy, no scoring), re-running the loop as a fixed point when justification/finalization advances. Same cap: `MAX_ATTESTATIONS_DATA = 8` (`subspecs/chain/config.py`). - **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order. - From af6e5df4014d119fa6eabd0452364ef65a579d4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1s=20Gr=C3=BCner?= <47506558+MegaRedHand@users.noreply.github.com> Date: Mon, 6 Jul 2026 15:37:21 -0300 Subject: [PATCH 3/4] docs: drop stale leanSpec file paths; fix spec pointer leanSpec pins no commit and refactored its module layout, so file paths into it rot. Remove the two leanSpec paths from spec_deviations.md (behavioral descriptions and symbol names stay). Update the CLAUDE.md spec pointer: source now lives under src/lean_spec/spec/forks//. --- CLAUDE.md | 2 +- docs/spec_deviations.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 17ac1b34..35631302 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -395,7 +395,7 @@ aggregation at interval 2). ## Resources -**Specs:** `leanSpec/src/lean_spec/` (Python reference implementation) +**Specs:** `leanSpec/src/lean_spec/spec/` (Python reference implementation; fork logic under `forks//`, e.g. `forks/lstar/`) **Devnet:** `lean-quickstart` (github.com/blockblaz/lean-quickstart) **Releases:** See `RELEASE.md` for release process documentation diff --git a/docs/spec_deviations.md b/docs/spec_deviations.md index 3cd159aa..453534b1 100644 --- a/docs/spec_deviations.md +++ b/docs/spec_deviations.md @@ -11,7 +11,7 @@ Aggregation runs off the main BlockChainServer actor loop and stops early once i - **ethlambda:** at interval 2 the actor snapshots the current slot's raw gossip signatures (`snapshot_current_slot_aggregation_inputs`, `crates/blockchain/src/aggregation.rs`) and spawns a `tokio::task::spawn_blocking` worker (`run_aggregation_worker`, `aggregation.rs`). The snapshot deliberately covers only current-slot raw gossip signatures, skipping existing-proof reuse and stale-slot groups so the interval-2 budget is never spent re-aggregating past slots (proof reuse is handled later, at block build). The worker streams each finished group back as an `AggregateProduced` message; the actor loop is never blocked on XMSS work. - **Early stop:** a `send_after(AGGREGATION_DEADLINE, ...)` timer cancels the session after 750ms (`AGGREGATION_DEADLINE`, `aggregation.rs`); the interval is 800ms (`MILLISECONDS_PER_INTERVAL`, `crates/blockchain/src/lib.rs`), leaving ~50ms for publish/propagation. The worker checks `cancel.is_cancelled()` before each job (`aggregation.rs`); in-flight jobs finish, remaining jobs are dropped. -- **leanSpec:** `aggregate()` is called inline and synchronously from `tick_interval` at interval 2 (`forks/lstar/spec.py`). It processes every group with no time budget, no worker, no cancellation. +- **leanSpec:** `aggregate()` is called inline and synchronously from `tick_interval` at interval 2. It processes every group with no time budget, no worker, no cancellation. - **Equivalence:** the per-group XMSS aggregation logic is the same as leanSpec's; the deviations are scheduling (off the actor loop), input scope (current-slot raw gossip only), and a partial-result bound. On cancellation the worker emits only the groups that finished, so a slot may pack fewer aggregates than the synchronous path would; any such subset still yields a valid block, affecting how many votes are included rather than signature validity. ## Attestation scoring on block building @@ -19,5 +19,5 @@ Aggregation runs off the main BlockChainServer actor loop and stops early once i Attestations are scored and selected when packing a block, rather than greedily included as they arrive. - **ethlambda:** `select_attestations` (`crates/blockchain/src/block_builder.rs`) ranks candidate `AttestationData` entries by tier `Finalize > Justify > Build` (`enum Tier`, `block_builder.rs`). The within-tier order is tier-dependent (`EntryScore::ordering_key`, `block_builder.rs`): `Finalize`/`Justify` entries already cross 2/3, so newer chain progress leads (target slot, attestation slot, then new-voter count); `Build` entries only add marginal voters, so coverage leads (new-voter count, target slot, then attestation slot). `data_root` is the final deterministic tiebreak in both tiers. Each round picks the best candidate against a projected post-state, up to `MAX_ATTESTATIONS_DATA = 8` distinct `AttestationData` entries (`crates/common/types/src/block.rs`); a winning entry may carry several proofs, which a later compaction step (`compact_attestations`, `block_builder.rs`) merges back to one per `AttestationData`. -- **leanSpec:** `build_block` iterates entries sorted by `target.slot` (oldest first) and includes the first ones that pass filters (greedy, no scoring), re-running the loop as a fixed point when justification/finalization advances. Same cap: `MAX_ATTESTATIONS_DATA = 8` (`subspecs/chain/config.py`). +- **leanSpec:** `build_block` iterates entries sorted by `target.slot` (oldest first) and includes the first ones that pass filters (greedy, no scoring), re-running the loop as a fixed point when justification/finalization advances. Same cap: `MAX_ATTESTATIONS_DATA = 8`. - **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order. From 706984cb23b0fab0d3fa73fbdeea86b33811db64 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1s=20Gr=C3=BCner?= <47506558+MegaRedHand@users.noreply.github.com> Date: Tue, 11 Aug 2026 15:38:46 -0300 Subject: [PATCH 4/4] docs: update spec deviations doc --- docs/spec_deviations.md | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/docs/spec_deviations.md b/docs/spec_deviations.md index 453534b1..8c7c6fa0 100644 --- a/docs/spec_deviations.md +++ b/docs/spec_deviations.md @@ -5,19 +5,25 @@ reference in a few places, mainly for performance reasons. This page lists those deviations; each will be fleshed out with rationale, implementation notes, and trade-offs over time. -## Asynchronous signature aggregation with early stop +## Asynchronous signature aggregation with an early start and an early stop -Aggregation runs off the main BlockChainServer actor loop and stops early once it runs out of time. +Aggregation runs off the main BlockChainServer actor loop, may start before its +interval, and stops early once it runs out of time. -- **ethlambda:** at interval 2 the actor snapshots the current slot's raw gossip signatures (`snapshot_current_slot_aggregation_inputs`, `crates/blockchain/src/aggregation.rs`) and spawns a `tokio::task::spawn_blocking` worker (`run_aggregation_worker`, `aggregation.rs`). The snapshot deliberately covers only current-slot raw gossip signatures, skipping existing-proof reuse and stale-slot groups so the interval-2 budget is never spent re-aggregating past slots (proof reuse is handled later, at block build). The worker streams each finished group back as an `AggregateProduced` message; the actor loop is never blocked on XMSS work. -- **Early stop:** a `send_after(AGGREGATION_DEADLINE, ...)` timer cancels the session after 750ms (`AGGREGATION_DEADLINE`, `aggregation.rs`); the interval is 800ms (`MILLISECONDS_PER_INTERVAL`, `crates/blockchain/src/lib.rs`), leaving ~50ms for publish/propagation. The worker checks `cancel.is_cancelled()` before each job (`aggregation.rs`); in-flight jobs finish, remaining jobs are dropped. -- **leanSpec:** `aggregate()` is called inline and synchronously from `tick_interval` at interval 2. It processes every group with no time budget, no worker, no cancellation. -- **Equivalence:** the per-group XMSS aggregation logic is the same as leanSpec's; the deviations are scheduling (off the actor loop), input scope (current-slot raw gossip only), and a partial-result bound. On cancellation the worker emits only the groups that finished, so a slot may pack fewer aggregates than the synchronous path would; any such subset still yields a valid block, affecting how many votes are included rather than signature validity. +- **ethlambda:** the actor snapshots everything aggregation needs (`snapshot_aggregation_inputs`, `crates/blockchain/src/aggregation.rs`) and spawns a `tokio::task::spawn_blocking` worker (`run_aggregation_worker`, `aggregation.rs`). Candidates are the store's gossip-signature groups plus payload-only groups (`new_payload_keys`, which need at least two existing proofs to merge). A tiered greedy selector orders them by consensus value (current-slot before stale, then `Finalize > Justify > Build`, mirroring the block builder) and emits at most `MAX_AGGREGATION_JOBS` jobs, dropping to a single job in the slot before one of our validators proposes. The worker streams each finished group back as an `AggregateProduced` message; the actor loop is never blocked on XMSS work. +- **Early start:** a session normally fires at interval 2, but may start up to `EARLY_AGGREGATION_WINDOW` earlier once the 2/3 signature threshold is already met (`maybe_start_early_aggregation`, `crates/blockchain/src/lib.rs`), so the proof lands earlier in the slot. +- **Early stop:** a `send_after(AGGREGATION_DEADLINE, ...)` timer cancels the session that long after **session start**, so a session that started early also ends early (`AGGREGATION_DEADLINE`, `aggregation.rs`). The worker checks `cancel.is_cancelled()` before each job (`aggregation.rs`); in-flight jobs finish, remaining jobs are dropped. +- **leanSpec:** `aggregate()` is called inline and synchronously from `tick_interval`, at interval 2 only. It walks every attestation data with fresh evidence, with no job cap, no time budget, no worker, and no cancellation. +- **Equivalence:** on cancellation the worker emits only the groups that finished, so a slot may pack fewer aggregates than the synchronous path would; any such subset still yields a valid block, affecting how many votes are included rather than signature validity. The job cap has the same character: it bounds prover work per slot, not what a block may carry. ## Attestation scoring on block building -Attestations are scored and selected when packing a block, rather than greedily included as they arrive. +Attestations are scored and selected when packing a block, rather than taken in +target-slot order as they are scanned. -- **ethlambda:** `select_attestations` (`crates/blockchain/src/block_builder.rs`) ranks candidate `AttestationData` entries by tier `Finalize > Justify > Build` (`enum Tier`, `block_builder.rs`). The within-tier order is tier-dependent (`EntryScore::ordering_key`, `block_builder.rs`): `Finalize`/`Justify` entries already cross 2/3, so newer chain progress leads (target slot, attestation slot, then new-voter count); `Build` entries only add marginal voters, so coverage leads (new-voter count, target slot, then attestation slot). `data_root` is the final deterministic tiebreak in both tiers. Each round picks the best candidate against a projected post-state, up to `MAX_ATTESTATIONS_DATA = 8` distinct `AttestationData` entries (`crates/common/types/src/block.rs`); a winning entry may carry several proofs, which a later compaction step (`compact_attestations`, `block_builder.rs`) merges back to one per `AttestationData`. -- **leanSpec:** `build_block` iterates entries sorted by `target.slot` (oldest first) and includes the first ones that pass filters (greedy, no scoring), re-running the loop as a fixed point when justification/finalization advances. Same cap: `MAX_ATTESTATIONS_DATA = 8`. -- **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order. +- **ethlambda:** `select_attestations` (`crates/blockchain/src/block_builder.rs`) ranks candidate `AttestationData` entries by tier `Finalize > Justify > Build` (`enum Tier`, `block_builder.rs`). The within-tier order is tier-dependent (`EntryScore::ordering_key`, `block_builder.rs`): `Finalize`/`Justify` entries already cross 2/3, so newer chain progress leads (target slot, attestation slot, then new-voter count); `Build` entries only add marginal voters, so coverage leads (new-voter count, target slot, then attestation slot). `data_root` is the final deterministic tiebreak in both tiers. Each round picks the best candidate against a projected post-state. +- **Proposer budget:** rounds stop at `max_attestations_per_block` distinct `AttestationData` entries (`--max-attestations-per-block`, default 3), clamped to `MAX_ATTESTATIONS_DATA`. The *consensus* cap is `MAX_ATTESTATIONS_DATA`, the same value leanSpec enforces in its state transition; only the proposer-side budget differs, and it is configurable. +- **Collapsing duplicate data:** a winning entry may carry several proofs, which must collapse to one proof per `AttestationData` before the block is valid. By default ethlambda keeps only the best-coverage proof and **drops** the rest (`keep_best_proof_per_data`, `block_builder.rs`), skipping the leanVM merge at the cost of the voters those proofs carried. With `--enable-proposer-aggregation`, `compact_attestations` (`block_builder.rs`) instead merges them through recursive proof aggregation, which is what leanSpec always does. +- **leanSpec:** `build_block` scans candidates sorted by `(target.slot, data_root)`, oldest target first, and includes the first ones that pass its filters (greedy, no scoring), re-running the scan as a fixed point when justification/finalization advances. Its proposer budget is `MAX_ATTESTATIONS_DATA` itself. +- **Equivalence:** both produce a valid block. ethlambda front-loads the attestations that advance justification and finality, and within those tiers prefers the *newest* target where leanSpec takes the *oldest*; combined with the smaller default budget, an older entry can be outranked by newer ones round after round, so which votes reach peers through blocks differs even though every block stays valid. The smaller budget yields smaller blocks and lower build times. +- **Upstream status:** the tiered strategy is proposed upstream as leanSpec [PR #1149](https://github.com/leanEthereum/leanSpec/pull/1149) (open at the time of writing), so this deviation may converge; the recursive-merge collapse follows leanSpec #510.