WIP -- [Leios] LLF1-3: the endorser block, its announcement, and the vote (#1301)

[williamdemeo]

This PR adds Ledger.Dijkstra.Specification.Leios.Types, the Leios primitive types of the design note and CIP-164 as amended by cardano-foundation/CIPs#1250: the endorser block, the announcement that names it, and the committee vote.

• EndorserBlock is the ordered list of transaction references, List (TxRefHash × ℕ). Duplicate-freedom of the reference hashes is a validity condition for the rules milestone, not a proof field, and the module prose records why (the rules must be able to mention a malformed object in order to reject it; a proof field would also forfeit derived decidable equality).
• hashEB fixes the EB identifier as the hash of the reference structure itself, via the abstract hashEBRefs; the byte-exact preimage stays deliberately unpinned, and the prose marks this boundary as the conformance cliff tracked in the design note.
• Announcement = EBHash × ℕ models the optional header group announced_eb/announced_eb_size; the wire's certified_eb bit is spec-derived and not modeled, which the prose also records.
• Vote follows the amended CIP: the hash of the announcing RB header (exactly the signed message), the voter_id seat index, and the BLS vote signature. No slot and no EB hash, which the amended Appendix B declares redundant on the wire. Consumed by no transition rule, per the design-note addendum; ValidVote and friends are later milestones.
• Both records carry derived DecEq instances, and Announcement inherits one from its components.

The one design call flagged for review is carrier placement: EBHash, TxRefHash, RBHeaderHash (each with DecEq) and hashEBRefs : List (TxRefHash × ℕ) → EBHash land as fields of the core CryptoStructure, in a short visible "Leios Hashes" block beside the Leios voting crypto, on the precedent that ScriptHash and VRF are protocol-specific hash types already carried by that record. The alternative was leaving them as parameters of the new module. TxRefHash is the hash of the complete transaction bytes, not the body-only transaction id, and the prose keeps that distinction (CIP-164 Appendix B).

There is deliberately no certificate type here: LeiosCert (signer set plus aggregate signature) belongs beside the committee that produces it, in the Ledger.Dijkstra.Specification.Leios module that #1300 introduces, and this module's prose points there, so the two PRs compose without duplication.

The Foreign crypto instance and formal-ledger-test's LedgerImplementation mirror the new fields; the latter typechecks locally (it is the surface only Hydra checks in CI).

Gates: agda src/Ledger/Dijkstra.lagda.md and agda src/Ledger.lagda.md both exit 0.

Stacked on #1298's PR; re-targets leios-main as the stack merges.

Closes #1301.

🤖 AI-assisted development: Claude Fable 5 (Anthropic)

[Copilot]

🟡 Changes recommended

The abstract API cannot pass RBHeaderHash to the Ser-based BLS verifier, and documentation links currently target the contradictory unamended CIP.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

Adds foundational Leios endorser-block, announcement, and vote types aligned with the amended CIP-164 design.

Changes:

• Defines Leios primitive types and decidable equality.
• Extends CryptoStructure with Leios hash abstractions.
• Integrates the module into documentation and test/foreign structures.

File summaries

File	Description
src/Ledger/Dijkstra/Specification/Leios/Types.lagda.md	Defines and documents Leios types.
src/Ledger/Dijkstra/Specification.lagda.md	Imports the Leios types module.
src/Ledger/Core/Specification/Crypto.lagda.md	Adds Leios hash carriers and equality instances.
src/Ledger/Core/Foreign/Crypto/Structure.agda	Implements foreign hash fields.
formal-ledger-test/src/Test/LedgerImplementation.lagda.md	Extends the test crypto implementation.
CHANGELOG.md	Records the new specification types.
build-tools/static/mkdocs/mkdocs.yml	Adds Leios types to documentation navigation.

Review details

Suppressed comments (2)

src/Ledger/Core/Specification/Crypto.lagda.md:138

• RBHeaderHash is independent of Ser, but the only BLS verifier accepts Ser (isSignedBy : BlsVKey → Ser → BlsSig → Type). Consequently, code parameterized by CryptoStructure cannot validate Vote.vSig against Vote.vAnn, despite that being the stated signed message. Add an abstract encoding such as RBHeaderHash → Ser (and implement it in each structure), or change the verification API so this carrier can be passed directly.

  field EBHash TxRefHash RBHeaderHash : Type
        hashEBRefs : List (TxRefHash × ℕ) → EBHash

src/Ledger/Dijkstra/Specification/Leios/Types.lagda.md:132

• This footnote points to master, where leios_vote still contains slot_no and endorser_block_hash; the announcing-header schema used above exists only in the open amendment PR. Link the amended document (or a pinned amendment commit) so the claimed wire-format mapping does not send readers to a contradictory schema.

[^1]: [CIP-164, Appendix B: Wire Format Specifications (CDDL)](https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#appendix-b-cddl).

• Files reviewed: 7/7 changed files
• Comments generated: 2
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[williamdemeo]

accidentally closed