docs: add spec deviations page#499
Conversation
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).
🤖 Claude Code ReviewReview: PR #499 — docs: add spec deviations pageThis is a documentation-only change (new Verification performed:
All line numbers and code references are accurate as of the current Assessment: No issues found. The content is accurate, well-sourced, and appropriately scoped (split cleanly from PR #498 per the description). Good practice documenting why each deviation exists rather than just what differs from leanSpec — useful for onboarding and future spec-conformance audits. Automated review by Claude (Anthropic) · sonnet · custom prompt |
🤖 Codex Code Review
Aside from those doc issues, I did not find code correctness, security, or performance regressions in this PR because it only changes documentation. I did not run tests. Automated review by OpenAI Codex · gpt-5.4 · custom prompt |
🤖 Kimi Code ReviewReview of PR #499: Spec Deviations Documentation Overall, this is valuable documentation for consensus auditability. However, several clarifications are needed regarding determinism, safety bounds, and documentation maintenance. Critical Concerns1. Wall-clock dependence in consensus-critical code (aggregation.rs)
2. "Same XMSS proofs are produced" contradiction
3. Determinism of attestation scoring (block_builder.rs)
Security & Performance4. Timing attack surface
5. Cancellation safety
Documentation Quality6. Fragile line number references
7. Missing equivalence proof for attestation scoring
Minor Issues8. Inconsistent formatting
9. XMSS context SummaryThe deviations described appear sound from a consensus perspective (partial aggregation produces valid states; scoring preserves validity), but the documentation should explicitly address determinism and timing assumptions. Request changes for Items 1, 2, and 6 before merge. Automated review by Kimi (Moonshot AI) · kimi-k2.5 · custom prompt |
Greptile SummaryThis PR adds a
Confidence Score: 5/5Documentation-only change with no impact on runtime behavior; safe to merge. All code cross-references (function names, constant values, line numbers) were verified against current source and are accurate. The only findings are a single-word grammar fix and a trailing blank line — neither affects the correctness or completeness of the documentation. No files require special attention.
|
| Filename | Overview |
|---|---|
| docs/spec_deviations.md | New documentation page; all symbol names and line numbers verified against current source. Minor grammar nit on line 10 ("ran" should be "runs") and two trailing blank lines at EOF. |
| docs/SUMMARY.md | Adds a new "Development" section with the Spec Deviations entry; change is minimal and correct. |
Flowchart
%%{init: {'theme': 'neutral'}}%%
flowchart TD
A[interval 2 tick] --> B[Actor snapshots state]
B --> C[spawn_blocking: run_aggregation_worker]
B --> D[send_after 750ms deadline]
C --> E{cancel.is_cancelled?}
E -- No --> F[aggregate_job]
F --> G[AggregateProduced to Actor]
G --> E
E -- Yes --> H[AggregationDone to Actor]
D --> I[cancel token set] --> E
%%{init: {'theme': 'base', 'themeVariables': {"darkMode": true, "background": "#0d1117", "primaryColor": "#21262d", "primaryTextColor": "#e6edf3", "primaryBorderColor": "#8b949e", "lineColor": "#8b949e", "textColor": "#e6edf3", "edgeLabelBackground": "#161b22", "actorBkg": "#21262d", "actorBorder": "#8b949e", "actorTextColor": "#e6edf3", "actorLineColor": "#8b949e", "signalColor": "#8b949e", "signalTextColor": "#e6edf3", "noteBkgColor": "#373320", "noteBorderColor": "#d4a72c", "noteTextColor": "#f0e6c0", "labelBoxBkgColor": "#21262d", "labelBoxBorderColor": "#8b949e", "labelTextColor": "#e6edf3", "loopTextColor": "#e6edf3", "activationBkgColor": "#30363d", "activationBorderColor": "#8b949e"}}}%%
flowchart TD
A[interval 2 tick] --> B[Actor snapshots state]
B --> C[spawn_blocking: run_aggregation_worker]
B --> D[send_after 750ms deadline]
C --> E{cancel.is_cancelled?}
E -- No --> F[aggregate_job]
F --> G[AggregateProduced to Actor]
G --> E
E -- Yes --> H[AggregationDone to Actor]
D --> I[cancel token set] --> E
Prompt To Fix All With AI
Fix the following 2 code review issues. Work through them one at a time, proposing concise fixes.
---
### Issue 1 of 2
docs/spec_deviations.md:10
Minor grammar issue: "ran" is past tense, but the sentence describes current, ongoing behavior. "runs" (or "has run") matches the present-tense framing used in the rest of the section.
```suggestion
Aggregation runs off the main BlockChainServer actor loop and stops early once it runs out of time.
```
### Issue 2 of 2
docs/spec_deviations.md:23-24
The file ends with two blank lines rather than one, which is inconsistent with other pages in the `docs/` directory.
```suggestion
- **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order.
```
Reviews (1): Last reviewed commit: "docs: add spec deviations page to the bo..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
|
|
||
| ## Asynchronous signature aggregation with early stop | ||
|
|
||
| Aggregation runs off the main BlockChainServer actor loop and stops early once it ran out of time. |
There was a problem hiding this comment.
| 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. |
Prompt To Fix With AI
This is a comment left during a code review.
Path: docs/spec_deviations.md
Line: 10
Comment:
Minor grammar issue: "ran" is past tense, but the sentence describes current, ongoing behavior. "runs" (or "has run") matches the present-tense framing used in the rest of the section.
```suggestion
Aggregation runs off the main BlockChainServer actor loop and stops early once it runs out of time.
```
How can I resolve this? If you propose a fix, please make it concise.Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
| - **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order. | ||
|
|
There was a problem hiding this comment.
docs/ directory.
| - **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order. | |
| - **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order. |
Prompt To Fix With AI
This is a comment left during a code review.
Path: docs/spec_deviations.md
Line: 23-24
Comment:
The file ends with two blank lines rather than one, which is inconsistent with other pages in the `docs/` directory.
```suggestion
- **Equivalence:** both produce a valid block; ethlambda prioritizes attestations that advance finality/justification rather than processing in slot order.
```
How can I resolve this? If you propose a fix, please make it concise.Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
- 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.
## Summary Clarifies the Docker image-tag wording in `README.md` and `RELEASE.md`: - `unstable` is built from the latest `main` commit. - `latest` / `devnetX` are the latest **stable** devnet images. - Bumped the stale `devnet3` "at the time of writing" and `docker pull` examples to `devnet5` (the current devnet). ## Notes - Left untouched: `Cargo.toml` `leansig` `devnet4` branch (real dependency), the `devnet3/devnet4` test-ignore comment in `encoding.rs`, and the README "Older devnets" list (`devnet1-4` are correctly the *older* ones; `devnet5` is current). - The new `docs/spec_deviations.md` page (and its `SUMMARY.md` index entry) was split into #499.
1 participant
Summary
Adds
docs/spec_deviations.mddocumenting where ethlambda intentionally diverges from the leanSpec reference, mainly for performance:spawn_blockingworker with a 750ms deadline, vs leanSpec's inline synchronousaggregate().Finalize > Justify > Build) and selected against a projected post-state when packing a block, vs leanSpec's greedy slot-ordered inclusion.Also registers the page in the mdBook
SUMMARY.mdunder a new Development section so it actually renders in the book.Source references were verified against current code (line numbers, and the tier-dependent attestation tie-break per leanSpec #1149).
Split out from #498, which now carries only the image-tag wording changes.