IntersectMBO / IntersectMBO/formal-ledger-specifications

[LLF1-3] `Leios.Types`: the endorser block, its announcement, and the vote

Open
#1,301 0 comments 0 reactions 0 assignees View on GitHub
era: dijkstra Leios
Dominant language
Agda
Stars
52
Forks
20
Avg merge
6d 14h
Merged PRs (30d)
7

Description

## Description

New Leios primitive types for the Dijkstra specification, per the design note and CIP-164 as amended by cardano-foundation/CIPs#1250: the endorser block, its announcement, and the vote.

*The certificate is deliberately absent*: `LeiosCert` (signer bitfield plus aggregate signature) lives in the committee module introduced by #1300, and this issue coordinates with that module rather than duplicating it.

- [ ] `EndorserBlock`: an ordered list of transaction references, `List (TxRefHash × ℕ)` (hash of the complete transaction bytes plus declared size, CIP-164 Appendix B); duplicate-freedom is a validity condition, not a proof field (decision recorded during the fork trial's M1-3 review).
- [ ] `hashEB`: the EB identifier as the hash of the reference structure itself, via an abstract `hashEBRefs`; the byte-exact preimage stays deliberately unpinned (the conformance cliff tracked in the design note).
- [ ] `Announcement = EBHash × ℕ`: the header's `announced_eb` and `announced_eb_size`; the wire's `certified_eb` bit is spec-derived and not modeled.
- [ ] `Vote`, per the amended CIP: the hash of the announcing RB header (the signed message), the `voter_id` seat index, and the BLS vote signature. Consumed by no transition rule; kept as a definition serving `validateVote` and the quorum-safety metatheory (design-note addendum; agreed with Sebastian on Slack, 2026-08-31).
- [ ] Carrier placement, the first thing to settle in review: `TxRefHash`, `EBHash`, and `hashEBRefs` need a home now that the `LeiosAbstract` record is dissolved in favour of the core crypto structure; candidates are fields on `CryptoStructure` next to the BLS primitives, or parameters of this module.
- [ ] `DecEq` instances for all records; module prose maps each type to its CDDL counterpart (Appendix B).

Subissue of #1295.

**Note**. The branch for work on this issue should stack on #1300's crypto commit (the vote's signature type is BlsSig), which is another reason to split #1300.

Contributor guide

Open the contributing guide

Research direction

Start with the #1300 crypto commit, then read the design note and CIP-164 Appendix B to map the EndorserBlock, Announcement, and Vote fields. Resolve where TxRefHash, EBHash, and hashEBRefs belong in CryptoStructure or this module before implementing the types. Done means the records, DecEq instances, hashEB abstraction, BlsSig vote, and CDDL-mapping prose are integrated without duplicating LeiosCert.

Written by the indexing model from the issue text.

Assessment

Domain
cryptography
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Active
Clarity
Mostly clear
Newbie friendliness
42/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.