From 806e33b95924c51b0039640ba3029c7253a61704 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 18 Aug 2026 22:52:54 -0600 Subject: [PATCH 01/12] Add the Leios design note (M1-1) docs/leios/design-note.md records the defaults the Leios skeleton builds on, one subsection per decision: module placement, full-rules certified application, the application ordering and the announcement pin, failure as underivability, the committee defaults, the protocol parameter table, the availability contract, and the consensus-to-ledger interface table. Every quotation is verified against the CIP-164 source text, the Leios design document, cardano-ledger 5626 and 5965, and the protocol-level Agda spec. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 309 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 309 insertions(+) create mode 100644 docs/leios/design-note.md diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md new file mode 100644 index 0000000000..5d89e34e4b --- /dev/null +++ b/docs/leios/design-note.md @@ -0,0 +1,309 @@ +# Leios ledger rules: the skeleton's default decisions + +This note records the defaults behind the skeleton formalization of the +Ouroboros Linear Leios ledger rules ([CIP-164]) in the Dijkstra-era +specification, so that the Agda encodes decisions instead of debating them. +Each subsection states one default, cites the source that fixes it, and gives +the rationale; where every source is silent, the note picks a default and says +so. Comments from the consensus and ledger implementers are welcome on all of +it; the skeleton proceeds on these defaults and folds corrections in as they +arrive. + +In CIP-164's protocol, a block producer may announce an *endorser block* (EB), +an ordered list of transaction references (hash and declared byte size), +alongside its ordinary *ranking block* (RB). A committee of stake pools votes +on the announced EB, a quorum of votes is aggregated into a *certificate*, and +the immediately following RB may carry that certificate, at which point the +EB's transactions enter the ledger. Throughout this note, the *closure* of an +EB means its referenced transactions, resolved and taken in reference order. + +The note draws on the following sources: [CIP-164] (the normative text), the +implementation team's [Leios design document][design-doc] with its requirement +register (REQ-…), the cardano-ledger prototype ([#5626][cl-5626]: +announcement, certificate bit, and voting-key carriage in the Dijkstra era) +and its parameter proposal ([#5965][cl-5965]), and the protocol-level Agda +specification [ouroboros-leios-formal-spec][leios-formal-spec], for which the +ledger is the base layer. + +## Module placement + +Leios lands in the Dijkstra era as an additive subtree +`Ledger.Dijkstra.Specification.Leios.*` plus minimal edits to five existing +modules; no separate era, and no change to `Ledger.Core`. CIP-164 requires a +new ledger era for the block-format change ([Versioning][cip-versioning]), and +the implementation prototypes Leios in Dijkstra ([#5626][cl-5626] targets +`eras/dijkstra`), so the Dijkstra specification is where the rules belong; +keeping the new material in its own subtree keeps merges from `master` cheap. +The abstract voting crypto is a `LeiosAbstract` record threaded as a new field +of `AbstractFunctions`, so the signatures of the edited modules do not change; +promoting the aggregate-signature abstraction into `Ledger.Core`, where Peras +could share it, is follow-up work. + +```text +src/Ledger/Dijkstra/Specification/ +├── Leios.lagda.md -- umbrella: overview prose, re-exports +├── Leios/ +│ ├── Abstract.lagda.md -- LeiosAbstract: abstract voting crypto +│ ├── Types.lagda.md -- EndorserBlock, Announcement, Vote, Certificate +│ ├── Committee.lagda.md -- Seat, Committee, quorum arithmetic +│ └── Validity.lagda.md -- ValidVote, ValidCert, ValidEB +├── Abstract.lagda.md -- edit: leiosAbstract field in AbstractFunctions +├── PParams.lagda.md -- edit: the Leios parameter block +├── Certs.lagda.md -- edit: voting key in StakePoolParams +├── BlockBody.lagda.md -- edit: announcement/certificate fields, BBODY premises +└── Chain.lagda.md -- edit: pending-announcement threading, window check +``` + +## Certified application uses the full rules + +The skeleton applies a certified EB's closure with the ordinary iterated +LEDGER relation (`LEDGERS`), exactly as `BBODY` applies a block's own +transactions. CIP-164 fixes what a vote attests: the closure forms "a valid +extension of the RB that announced it" ([vote condition 5][cip-step3]), under +"the same validation rules used in Praos, with phase-1 and phase-2 validation +applying equally to both RB and EB transactions" +([Ledger Management][cip-ledger]). `ValidEB`, the property a certificate +ultimately certifies, conjoins reference/closure agreement, nonemptiness +([vote condition 6][cip-step3]), the per-EB bounds, and this valid-extension +condition stated with `LEDGERS`. + +The implementation, by contrast, applies a certified closure by +"reapplication with minimal checks and UTxO updates", "omitting previously +performed phase 1 & 2 validation" ([CIP-164 Table 2][cip-params]; +[REQ-LedgerTxNoValidation and REQ-LedgerCheapReapply][dd-txlevels]). The +skeleton treats that as an optimization, not a semantics: the relation +defines certified application by the full rules, and the theorem that minimal +reapplication agrees with the full rules on a closure some quorum has +validated is exactly the soundness result the optimization needs — a +follow-up proof, not a skeleton input. Nothing in the skeleton therefore +needs a separate reapply relation. + +Phase-2 failures need no special account. Spec-level transactions carry +their `isValid` flag, so `LEDGERS` covers collateral-forfeiting transactions +in a closure exactly as it does in a block body. Whether the wire format +should carry those flags is an open upstream question (the CIP's EB +[CDDL][cip-cddl] has no validity bits, while the +[design document][dd-blockval] proposes adding them) and does not touch the +relational rules. + +## Environment and ordering + +For a block B at slot s_B carrying a certificate for the EB announced by its +predecessor A at slot s_A — admissible only when +s_B ≥ s_A + 3·L_hdr + L_vote + L_diff ([Step 5][cip-step5]) — the rules fix +the following total order: + +1. **EB application.** The closure applies via `LEDGERS` to the ledger + state left by A's block-body transition, in A's environment: slot s_A and + the protocol parameters in force at A. CIP-164: "EB transactions are + validated against the ledger state from the RB that announced the EB + (i.e., the predecessor RB of the certifying RB)" + ([Ledger Management][cip-ledger]); the design document requires the same + ("the ledger must validate endorsed transactions against the ledger state + before updating it with the new ranking block", + [REQ-LedgerUntickedEBValidation][dd-blockval]). +2. **Tick.** The chain ticks to s_B on the EB-updated state; if an epoch + boundary lies between the two blocks, the reward update, enactment, and + the snapshots all see the closure's effects. +3. **Block body.** B's `BBODY` runs on the ticked state. B carries no + transactions of its own — "When a certificate is included, no further + transactions are allowed in the RB" ([Step 5][cip-step5]) — so its body + contributes the certificate premises and the usual bookkeeping. + +A block may announce its own EB while certifying its predecessor's ("it may +optionally announce its own EB for future certification", +[Step 5][cip-step5]); it consumes A's announcement and records its own +afterwards. Relationally, the certificate premises and the application +premise are simultaneous conjuncts; only an executable implementation orders +certificate verification against closure application. + +One corollary settles the parameter-change question, on which the CIP is +silent: everything about an announced EB is evaluated in the announcing +world. The closure runs under A's parameters; the certificate is checked +against the committee, the total active stake, and the quorum threshold τ +pinned at announcement; the timing window uses the period lengths in force at +A. A certificate proves what the voters checked, and the voters could check +only A's world; validating it against data none of them could have seen would +break that reading. The vote signature is bound to s_A for the same reason: +the binding "ensures voters validated the EB against the same ledger state it +extends when certified on chain" ([Vote Structure][cip-vote]). This +corollary is a note-set default to confirm with the implementers. + +This ordering also answers the design document's open question — "how much of +the work lives in `BBODY` itself versus a dedicated EB-body rule, and the +precise ordering of applying the closure relative to verifying the +certificate" ([Certificate verification][dd-certver]). There is no dedicated +EB-body rule: the certificate checks and the closure's application are +premises of the existing block and chain transitions, with the pending +announcement threaded through the chain-level context and application ordered +before the tick as above. + +## Certificate failure is the absence of a transition + +CIP-164's [Certificate Validation][cip-certval] lists five checks that must +pass "before accepting the block". The skeleton renders failure the way the +spec renders every block fault: a block whose certificate fails a check, or +that pairs a certificate with transactions of its own, or that certifies +before the window opens, simply admits no `BBODY`/`CHAIN` derivation. The +block is invalid, and nothing in the relational spec distinguishes why; a +predicate-failure taxonomy belongs to the `Computational` instances and the +conformance work, deferred with the rest of executability, and the five +checks are its raw material when it comes. The missing-certificate case +needs no bookkeeping at all: only the immediate successor may certify, and +otherwise "the EB certificate cannot be included and the EB is discarded" +([Step 5][cip-step5]); the pending announcement is simply replaced by the +next one, with no ledger trace and no expiry accounting. For consensus, the +reading is the usual one: an invalid certificate makes an invalid block, +nothing more drastic. + +## The committee + +CIP-164 fixes the committee once per epoch by stake-based truncation: "pools +are ordered by stake in descending order and selected, in order, until the +cumulative selected stake reaches" the coverage target σ_c, and the resulting +committee "is fixed for the entire epoch", with no per-EB sortition and no +non-persistent voters ([Committee Structure][cip-committee]; the boundary +procedure in [Epoch Boundary][cip-epoch]). The skeleton adds the following +defaults, each grounded in the design document: + +- **Snapshot.** The committee for an epoch derives from the stake + distribution available at the epoch boundary — the pool-stake + distribution the ledger already maintains for leader election + (`PoolDistr` in the implementation; + [REQ-StakeBasedCommitteeSelection][dd-committee]) — and is materialized + into the epoch state at the boundary rather than recomputed per use + ([REQ-LedgerStateVotingCommittee][dd-certver]). +- **Order and indices.** The descending-stake order fixes the seat indices + that votes (`voter_id`) and certificate bitfields address. The CIP names + no tie-break; the design document breaks ties by pool id, and the + skeleton adopts that. Selection enters the skeleton abstractly, as a + function with stated laws (registered pools, descending stake, coverage + σ_c); the concrete construction can land later without disturbing + anything downstream of the laws. +- **Keyless seats.** Membership is by stake alone, "independent of key + registration" ([REQ-KeylessSeat][dd-committee]): a selected pool without + a registered voting key still occupies its seat and holds its weight, but + the seat cannot sign, and a certificate whose bitfield sets a keyless + seat is invalid ([REQ-LedgerCertificateVerification][dd-certver]). + Keyless stake can therefore lower the quorum a certificate is able to + reach, never inflate it. +- **Keys.** Pool registration carries the voting key with its proof of + possession, as in the prototype's `spsLeiosKey` ([#5626][cl-5626]), and + registration checks the proof + ([REQ-CheckProofOfPossession][dd-committee]); the prototype stores the + key without checking the proof, a divergence to flag upstream. Rotation + is re-registration, activated at an epoch boundary + ([REQ-RotateBLSKeys][dd-keys]); CIP-164 leaves the real rotation + mechanism "to a follow-up PR amending this CIP" + ([Design Decisions][cip-design]). +- **The pin.** A certificate is validated against the committee of the + epoch in which the announcing RB was produced; the CIP sizes the signer + bitfield by exactly that committee ([Appendix B][cip-cddl]). A + certificate landing just after an epoch boundary is therefore checked + against the announcing epoch's committee and total active stake, per the + ordering corollary above. + +## Protocol parameters + +CIP-164's [Table 3][cip-params] declares the Leios parameters +governance-tunable; cardano-ledger [#5965][cl-5965] maps them onto the +Dijkstra `PParams` and adds one bound the table lacks. The skeleton adds +nine fields, with the mechanical `PParamsUpdate` and group companions; every +field sits in the network and security groups, following [#5965][cl-5965] +(all of its proposed parameters are assigned to exactly those two groups). + +| Field | CIP-164 (Table 3) | Type | Notes | +| ----------------------------- | --------------------------------------- | ------------ | ----- | +| `leiosHeaderDiffusionPeriod` | L_hdr, header diffusion period | ℕ (slots) | | +| `leiosVotingPeriod` | L_vote, voting period | ℕ (slots) | | +| `leiosDiffusionPeriod` | L_diff, diffusion period | ℕ (slots) | [#5965][cl-5965] renames it the *additional* diffusion period | +| `leiosMaxEBSize` | S_EB, endorser block max size | ℕ (bytes) | bounds the reference structure itself, which [#5965][cl-5965] calls the EB *header* | +| `leiosMaxEBTxsSize` | S_EB-tx, referenceable transaction size | ℕ (bytes) | bounds the closure's total bytes, [#5965][cl-5965]'s EB *body* | +| `leiosCommitteeStakeCoverage` | σ_c, committee stake coverage | UnitInterval | | +| `leiosQuorumStakeThreshold` | τ, quorum stake threshold | UnitInterval | normative constraint τ < σ_c | +| `leiosMaxEBExUnits` | max Plutus steps and memory per EB | ExUnits | Table 3's two budget rows in one field, after [#5965][cl-5965]'s `OrdExUnits` | +| `leiosMaxRefScriptSizePerEB` | (not in the table) | ℕ (bytes) | from [#5965][cl-5965]; the per-EB analog of `maxRefScriptSizePerBlock` | + +Table 3's remaining row, the ranking-block max size S_RB, is the existing +`maxBlockSize`; there is no new field ([#5965][cl-5965] maps it to +`ppMaxBBSize`). Well-formedness: τ < σ_c is normative ("Must satisfy +τ < σ_c", [Table 3][cip-params]) and joins positivity of the periods and +sizes in the parameter well-formedness predicate; the constraint is what +keeps a quorum achievable inside the committee's guaranteed stake coverage. +Types follow the spec's house conventions; [#5965][cl-5965]'s `SlotInterval`, +`Word32`, and `OrdExUnits` are the Haskell counterparts, and name or type +divergences get recorded in module prose. The network characteristics of the +CIP's Tables 1 and 2 (the Δ quantities) are not protocol parameters and do +not enter the spec. + +## Availability + +The rules take the closure as input and never ask whether data is available. +The block, as the spec sees it, is the resolved block: alongside the +certificate it carries the certified EB and the closure ("the ledger must be +provided with all endorsed transactions resolved", +[REQ-LedgerResolvedBlockValidation][dd-blockval]), and a matching premise +checks the closure against the EB's references pointwise, hash and declared +size. Availability is a consensus and storage concern; CIP-164 keeps EBs out +of chain validity altogether ("EBs are treated as auxiliary data that do not +affect chain validity or selection decisions", +[Chain Selection][cip-chainsel]), and a certificate whose closure has not yet +arrived is a block consensus cannot yet hand to the ledger, not a new failure +mode. Two wire artifacts deliberately stay out of the rules: the header's +`certified_eb` bit is a syncing optimization, derived in the spec from the +presence of the body's certificate; and a wrong `announced_eb_size` makes +nothing invalid — "neither the RB header nor the RB are invalid. But no +honest node should vote for the EB" ([Inclusion Rules][cip-inclusion]) — so +announcement-size agreement belongs to the voters' checks, not to block +validity. + +## The consensus↔ledger interface + +The interface proposed by Nicolas Frisby in the implementation design +discussion shapes the consensus↔ledger boundary as eight functions. The +table maps each to its skeleton counterpart, or records what stays outside +the skeleton and why. + +| Proposed function | Skeleton counterpart | +| ----------------------------- | -------------------- | +| `applyCertifiedEb` | The certificate branch of the block and chain rules: `ValidCert` plus the closure applied via `LEDGERS` from the announcing state, per the ordering above. | +| `validateCertificate` | `ValidCert` (`Leios.Validity`): signers are seats of the pinned committee, the aggregate signature verifies over (slot, EB hash), and the signers' stake meets τ times the total active stake. The contextual half — agreement with the pending announcement, the timing window — sits as block/chain premises. | +| `validateVote` | `ValidVote` (`Leios.Validity`): the voter index denotes a keyed committee seat whose key verifies the signature over (slot, EB hash). Votes never appear on-chain individually; this is the meaning consensus uses to filter votes before aggregation. | +| `doesEpochCommitteeIncludeMe` | Decidable membership on `Committee` (`Leios.Committee`), a seat lookup by pool. The "me" binding is consensus-local; the ledger side is the seat lookup on the materialized committee ([REQ-LedgerStateVotingCommittee][dd-certver]). | +| `initializeVotingLedgerState` | Follow-up (the voting-state interface). Meaning fixed now: the announcing block's post-`BBODY` state paired with fresh EB accumulators (bytes, `ExUnits`). | +| `applyTxForVoting` | Follow-up. Meaning fixed now: one LEDGER step plus accumulator updates and bound checks; folding it over the closure from the initialized state succeeds exactly when `ValidEB`'s extension-and-bounds conjuncts hold. | +| `reapplyTxForVoting` | Follow-up. The minimal-checks variant; its agreement with `applyTxForVoting` on previously validated transactions is the certified-application soundness theorem. | +| `forgetVotingLedgerState` | Follow-up. The projection back to the ledger state, with the evident round-trip law against initialization. | + +The protocol-level Agda specification consumes exactly this division: its +base-layer interface submits ranking blocks carrying +`txsOrEbCert : List Tx ⊎ EBCert` and asks the base layer for a single +judgment, the certificate check `V-chkCerts`, which is `ValidCert`'s role +here. The node-local vote conditions (header arrival, equivocation, +deadlines, chain position: CIP [vote conditions 1–4][cip-step3]) stay on its +side of the line, and `ValidEB` carries the ledger-checkable remainder +(conditions 5 and 6). + +[CIP-164]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md +[cip-step3]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#step-3-committee-validation +[cip-step5]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#step-5-chain-inclusion +[cip-params]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#protocol-parameters +[cip-ledger]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#ledger-management +[cip-chainsel]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#chain-selection +[cip-epoch]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#epoch-boundary +[cip-certval]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#certificate-validation +[cip-committee]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#committee-structure +[cip-vote]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#vote-structure +[cip-inclusion]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#rb-inclusion-rules +[cip-cddl]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#appendix-b-cddl +[cip-design]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#design-decisions +[cip-versioning]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#versioning +[design-doc]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md +[dd-txlevels]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#transaction-validation-levels +[dd-keys]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#key-registration-and-rotation +[dd-committee]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#committee-selection +[dd-certver]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#certificate-verification +[dd-blockval]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#block-validation +[cl-5626]: https://github.com/IntersectMBO/cardano-ledger/pull/5626 +[cl-5965]: https://github.com/IntersectMBO/cardano-ledger/issues/5965 +[leios-formal-spec]: https://github.com/input-output-hk/ouroboros-leios-formal-spec From e4882de627426b1160d40279b782dd0f7a327ece Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 18 Aug 2026 23:38:13 -0600 Subject: [PATCH 02/12] style formatting --- docs/leios/design-note.md | 351 ++++++++++++++++++-------------------- 1 file changed, 168 insertions(+), 183 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index 5d89e34e4b..e093a07fa8 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -1,43 +1,43 @@ # Leios ledger rules: the skeleton's default decisions -This note records the defaults behind the skeleton formalization of the -Ouroboros Linear Leios ledger rules ([CIP-164]) in the Dijkstra-era -specification, so that the Agda encodes decisions instead of debating them. -Each subsection states one default, cites the source that fixes it, and gives -the rationale; where every source is silent, the note picks a default and says -so. Comments from the consensus and ledger implementers are welcome on all of -it; the skeleton proceeds on these defaults and folds corrections in as they -arrive. - -In CIP-164's protocol, a block producer may announce an *endorser block* (EB), -an ordered list of transaction references (hash and declared byte size), -alongside its ordinary *ranking block* (RB). A committee of stake pools votes -on the announced EB, a quorum of votes is aggregated into a *certificate*, and -the immediately following RB may carry that certificate, at which point the -EB's transactions enter the ledger. Throughout this note, the *closure* of an -EB means its referenced transactions, resolved and taken in reference order. +This note records the defaults behind the skeleton formalization of the Ouroboros +Linear Leios ledger rules ([CIP-164]) in the Dijkstra-era specification, so that the +Agda encodes decisions instead of debating them. + +Each subsection states one default, cites the source that fixes it, and gives the +rationale; where every source is silent, the note picks a default and says so. + +Comments from the consensus and ledger implementers are welcome on all of it; the +skeleton proceeds on these defaults and folds corrections in as they arrive. + +In CIP-164's protocol, a block producer may announce an *endorser block* (EB), an +ordered list of transaction references (hash and declared byte size), alongside its +ordinary *ranking block* (RB). A committee of stake pools votes on the announced EB, +a quorum of votes is aggregated into a *certificate*, and the immediately following +RB may carry that certificate, at which point the EB's transactions enter the ledger. +Throughout this note, the *closure* of an EB means its referenced transactions, +resolved and taken in reference order. The note draws on the following sources: [CIP-164] (the normative text), the implementation team's [Leios design document][design-doc] with its requirement -register (REQ-…), the cardano-ledger prototype ([#5626][cl-5626]: -announcement, certificate bit, and voting-key carriage in the Dijkstra era) -and its parameter proposal ([#5965][cl-5965]), and the protocol-level Agda -specification [ouroboros-leios-formal-spec][leios-formal-spec], for which the -ledger is the base layer. +register (REQ-…), the cardano-ledger prototype ([#5626][cl-5626]: announcement, +certificate bit, and voting-key carriage in the Dijkstra era) and its parameter +proposal ([#5965][cl-5965]), and the protocol-level Agda specification +[ouroboros-leios-formal-spec][leios-formal-spec], for which the ledger is the base +layer. ## Module placement Leios lands in the Dijkstra era as an additive subtree -`Ledger.Dijkstra.Specification.Leios.*` plus minimal edits to five existing -modules; no separate era, and no change to `Ledger.Core`. CIP-164 requires a -new ledger era for the block-format change ([Versioning][cip-versioning]), and -the implementation prototypes Leios in Dijkstra ([#5626][cl-5626] targets -`eras/dijkstra`), so the Dijkstra specification is where the rules belong; -keeping the new material in its own subtree keeps merges from `master` cheap. -The abstract voting crypto is a `LeiosAbstract` record threaded as a new field -of `AbstractFunctions`, so the signatures of the edited modules do not change; -promoting the aggregate-signature abstraction into `Ledger.Core`, where Peras -could share it, is follow-up work. +`Ledger.Dijkstra.Specification.Leios.*` plus minimal edits to five existing modules; +no separate era, and no change to `Ledger.Core`. CIP-164 requires a new ledger era +for the block-format change ([Versioning][cip-versioning]), and the implementation +prototypes Leios in Dijkstra ([#5626][cl-5626] targets `eras/dijkstra`), so the +Dijkstra specification is where the rules belong; keeping the new material in its own +subtree keeps merges from `master` cheap. The abstract voting crypto is a +`LeiosAbstract` record threaded as a new field of `AbstractFunctions`, so the +signatures of the edited modules do not change; promoting the aggregate-signature +abstraction into `Ledger.Core`, where Peras could share it, is follow-up work. ```text src/Ledger/Dijkstra/Specification/ @@ -56,138 +56,128 @@ src/Ledger/Dijkstra/Specification/ ## Certified application uses the full rules -The skeleton applies a certified EB's closure with the ordinary iterated -LEDGER relation (`LEDGERS`), exactly as `BBODY` applies a block's own -transactions. CIP-164 fixes what a vote attests: the closure forms "a valid -extension of the RB that announced it" ([vote condition 5][cip-step3]), under -"the same validation rules used in Praos, with phase-1 and phase-2 validation -applying equally to both RB and EB transactions" -([Ledger Management][cip-ledger]). `ValidEB`, the property a certificate -ultimately certifies, conjoins reference/closure agreement, nonemptiness +The skeleton applies a certified EB's closure with the ordinary iterated LEDGER +relation (`LEDGERS`), exactly as `BBODY` applies a block's own transactions. CIP-164 +fixes what a vote attests: the closure forms "a valid extension of the RB that +announced it" ([vote condition 5][cip-step3]), under "the same validation rules used +in Praos, with phase-1 and phase-2 validation applying equally to both RB and EB +transactions" ([Ledger Management][cip-ledger]). `ValidEB`, the property a +certificate ultimately certifies, conjoins reference/closure agreement, nonemptiness ([vote condition 6][cip-step3]), the per-EB bounds, and this valid-extension condition stated with `LEDGERS`. -The implementation, by contrast, applies a certified closure by -"reapplication with minimal checks and UTxO updates", "omitting previously -performed phase 1 & 2 validation" ([CIP-164 Table 2][cip-params]; -[REQ-LedgerTxNoValidation and REQ-LedgerCheapReapply][dd-txlevels]). The -skeleton treats that as an optimization, not a semantics: the relation -defines certified application by the full rules, and the theorem that minimal -reapplication agrees with the full rules on a closure some quorum has -validated is exactly the soundness result the optimization needs — a -follow-up proof, not a skeleton input. Nothing in the skeleton therefore -needs a separate reapply relation. - -Phase-2 failures need no special account. Spec-level transactions carry -their `isValid` flag, so `LEDGERS` covers collateral-forfeiting transactions -in a closure exactly as it does in a block body. Whether the wire format -should carry those flags is an open upstream question (the CIP's EB -[CDDL][cip-cddl] has no validity bits, while the -[design document][dd-blockval] proposes adding them) and does not touch the +The implementation, by contrast, applies a certified closure by "reapplication with +minimal checks and UTxO updates", "omitting previously performed phase 1 & 2 +validation" ([CIP-164 Table 2][cip-params]; [REQ-LedgerTxNoValidation and +REQ-LedgerCheapReapply][dd-txlevels]). The skeleton treats that as an optimization, +not a semantics: the relation defines certified application by the full rules, and +the theorem that minimal reapplication agrees with the full rules on a closure some +quorum has validated is exactly the soundness result the optimization needs — a +follow-up proof, not a skeleton input. Nothing in the skeleton therefore needs a +separate reapply relation. + +Phase-2 failures need no special account. Spec-level transactions carry their +`isValid` flag, so `LEDGERS` covers collateral-forfeiting transactions in a closure +exactly as it does in a block body. Whether the wire format should carry those flags +is an open upstream question (the CIP's EB [CDDL][cip-cddl] has no validity bits, +while the [design document][dd-blockval] proposes adding them) and does not touch the relational rules. ## Environment and ordering -For a block B at slot s_B carrying a certificate for the EB announced by its -predecessor A at slot s_A — admissible only when -s_B ≥ s_A + 3·L_hdr + L_vote + L_diff ([Step 5][cip-step5]) — the rules fix -the following total order: - -1. **EB application.** The closure applies via `LEDGERS` to the ledger - state left by A's block-body transition, in A's environment: slot s_A and - the protocol parameters in force at A. CIP-164: "EB transactions are - validated against the ledger state from the RB that announced the EB - (i.e., the predecessor RB of the certifying RB)" - ([Ledger Management][cip-ledger]); the design document requires the same - ("the ledger must validate endorsed transactions against the ledger state - before updating it with the new ranking block", +For a block `B` at slot `s_B` carrying a certificate for the EB announced by its +predecessor `A` at slot `s_A` (admissible only when +`s_B ≥ s_A + 3·L_hdr + L_vote + L_diff`; [Step 5][cip-step5]) the rules fix the +following total order: + +1. **EB application**. The closure applies via `LEDGERS` to the ledger state left + by A's block-body transition, in A's environment: slot `s_A` and the protocol + parameters in force at A. CIP-164: "EB transactions are validated against the + ledger state from the RB that announced the EB (i.e., the predecessor RB of the + certifying RB)" ([Ledger Management][cip-ledger]); the design document requires + the same ("the ledger must validate endorsed transactions against the ledger + state before updating it with the new ranking block", [REQ-LedgerUntickedEBValidation][dd-blockval]). -2. **Tick.** The chain ticks to s_B on the EB-updated state; if an epoch - boundary lies between the two blocks, the reward update, enactment, and - the snapshots all see the closure's effects. -3. **Block body.** B's `BBODY` runs on the ticked state. B carries no - transactions of its own — "When a certificate is included, no further - transactions are allowed in the RB" ([Step 5][cip-step5]) — so its body - contributes the certificate premises and the usual bookkeeping. +2. **Tick**. The chain ticks to `s_B` on the EB-updated state; if an epoch boundary + lies between the two blocks, the reward update, enactment, and the snapshots all + see the closure's effects. +3. **Block body**. B's `BBODY` runs on the ticked state. B carries no transactions + of its own — "When a certificate is included, no further transactions are allowed + in the RB" ([Step 5][cip-step5]) — so its body contributes the certificate + premises and the usual bookkeeping. A block may announce its own EB while certifying its predecessor's ("it may -optionally announce its own EB for future certification", -[Step 5][cip-step5]); it consumes A's announcement and records its own -afterwards. Relationally, the certificate premises and the application -premise are simultaneous conjuncts; only an executable implementation orders -certificate verification against closure application. - -One corollary settles the parameter-change question, on which the CIP is -silent: everything about an announced EB is evaluated in the announcing -world. The closure runs under A's parameters; the certificate is checked -against the committee, the total active stake, and the quorum threshold τ -pinned at announcement; the timing window uses the period lengths in force at -A. A certificate proves what the voters checked, and the voters could check -only A's world; validating it against data none of them could have seen would -break that reading. The vote signature is bound to s_A for the same reason: -the binding "ensures voters validated the EB against the same ledger state it -extends when certified on chain" ([Vote Structure][cip-vote]). This +optionally announce its own EB for future certification", [Step 5][cip-step5]); it +consumes A's announcement and records its own afterwards. Relationally, the +certificate premises and the application premise are simultaneous conjuncts; only an +executable implementation orders certificate verification against closure +application. + +One corollary settles the parameter-change question, on which the CIP is silent: +everything about an announced EB is evaluated in the announcing world. The closure +runs under A's parameters; the certificate is checked against the committee, the +total active stake, and the quorum threshold τ pinned at announcement; the timing +window uses the period lengths in force at A. A certificate proves what the voters +checked, and the voters could check only A's world; validating it against data none +of them could have seen would break that reading. The vote signature is bound to `s_A` +for the same reason: the binding "ensures voters validated the EB against the same +ledger state it extends when certified on chain" ([Vote Structure][cip-vote]). This corollary is a note-set default to confirm with the implementers. -This ordering also answers the design document's open question — "how much of -the work lives in `BBODY` itself versus a dedicated EB-body rule, and the -precise ordering of applying the closure relative to verifying the -certificate" ([Certificate verification][dd-certver]). There is no dedicated -EB-body rule: the certificate checks and the closure's application are -premises of the existing block and chain transitions, with the pending -announcement threaded through the chain-level context and application ordered -before the tick as above. +This ordering also answers the following open question of the design document: +"How much of the work lives in `BBODY` itself versus a dedicated EB-body rule, and +the precise ordering of applying the closure relative to verifying the certificate" +([Certificate verification][dd-certver]). There is no dedicated EB-body rule: the +certificate checks and the closure's application are premises of the existing block +and chain transitions, with the pending announcement threaded through the chain-level +context and application ordered before the tick as above. ## Certificate failure is the absence of a transition -CIP-164's [Certificate Validation][cip-certval] lists five checks that must -pass "before accepting the block". The skeleton renders failure the way the -spec renders every block fault: a block whose certificate fails a check, or -that pairs a certificate with transactions of its own, or that certifies -before the window opens, simply admits no `BBODY`/`CHAIN` derivation. The -block is invalid, and nothing in the relational spec distinguishes why; a -predicate-failure taxonomy belongs to the `Computational` instances and the -conformance work, deferred with the rest of executability, and the five -checks are its raw material when it comes. The missing-certificate case -needs no bookkeeping at all: only the immediate successor may certify, and -otherwise "the EB certificate cannot be included and the EB is discarded" -([Step 5][cip-step5]); the pending announcement is simply replaced by the -next one, with no ledger trace and no expiry accounting. For consensus, the -reading is the usual one: an invalid certificate makes an invalid block, -nothing more drastic. +CIP-164's [Certificate Validation][cip-certval] lists five checks that must pass +"before accepting the block". The skeleton renders failure the way the spec renders +every block fault: a block whose certificate fails a check, or that pairs a +certificate with transactions of its own, or that certifies before the window opens, +simply admits no `BBODY`/`CHAIN` derivation. The block is invalid, and nothing in +the relational spec distinguishes why; a predicate-failure taxonomy belongs to the +`Computational` instances and the conformance work, deferred with the rest of +executability, and the five checks are its raw material when it comes. The +missing-certificate case needs no bookkeeping at all: only the immediate successor +may certify, and otherwise "the EB certificate cannot be included and the EB is +discarded" ([Step 5][cip-step5]); the pending announcement is simply replaced by the +next one, with no ledger trace and no expiry accounting. For consensus, the reading +is the usual one: an invalid certificate makes an invalid block, nothing more drastic. ## The committee -CIP-164 fixes the committee once per epoch by stake-based truncation: "pools -are ordered by stake in descending order and selected, in order, until the -cumulative selected stake reaches" the coverage target σ_c, and the resulting -committee "is fixed for the entire epoch", with no per-EB sortition and no -non-persistent voters ([Committee Structure][cip-committee]; the boundary -procedure in [Epoch Boundary][cip-epoch]). The skeleton adds the following -defaults, each grounded in the design document: - -- **Snapshot.** The committee for an epoch derives from the stake - distribution available at the epoch boundary — the pool-stake - distribution the ledger already maintains for leader election - (`PoolDistr` in the implementation; - [REQ-StakeBasedCommitteeSelection][dd-committee]) — and is materialized - into the epoch state at the boundary rather than recomputed per use +CIP-164 fixes the committee once per epoch by stake-based truncation: "pools are +ordered by stake in descending order and selected, in order, until the cumulative +selected stake reaches" the coverage target `σ_c`, and the resulting committee "is +fixed for the entire epoch", with no per-EB sortition and no non-persistent voters +([Committee Structure][cip-committee]; the boundary procedure in [Epoch +Boundary][cip-epoch]). The skeleton adds the following defaults, each grounded in +the design document: + +- **Snapshot**. The committee for an epoch derives from the stake distribution + available at the epoch boundary, which is the pool-stake distribution the ledger + already maintains for leader election (`PoolDistr` in the implementation; + [REQ-StakeBasedCommitteeSelection][dd-committee]). This is materialized into the + epoch state at the boundary rather than recomputed per use ([REQ-LedgerStateVotingCommittee][dd-certver]). -- **Order and indices.** The descending-stake order fixes the seat indices - that votes (`voter_id`) and certificate bitfields address. The CIP names - no tie-break; the design document breaks ties by pool id, and the - skeleton adopts that. Selection enters the skeleton abstractly, as a - function with stated laws (registered pools, descending stake, coverage - σ_c); the concrete construction can land later without disturbing - anything downstream of the laws. -- **Keyless seats.** Membership is by stake alone, "independent of key +- **Order and indices**. The descending-stake order fixes the seat indices that + votes (`voter_id`) and certificate bitfields address. The CIP names no + tie-break; the design document breaks ties by pool id, and the skeleton adopts + that. Selection enters the skeleton abstractly, as a function with stated laws + (registered pools, descending stake, coverage `σ_c`); the concrete construction can + land later without disturbing anything downstream of the laws. +- **Keyless seats**. Membership is by stake alone, "independent of key registration" ([REQ-KeylessSeat][dd-committee]): a selected pool without a registered voting key still occupies its seat and holds its weight, but the seat cannot sign, and a certificate whose bitfield sets a keyless seat is invalid ([REQ-LedgerCertificateVerification][dd-certver]). Keyless stake can therefore lower the quorum a certificate is able to reach, never inflate it. -- **Keys.** Pool registration carries the voting key with its proof of +- **Keys**. Pool registration carries the voting key with its proof of possession, as in the prototype's `spsLeiosKey` ([#5626][cl-5626]), and registration checks the proof ([REQ-CheckProofOfPossession][dd-committee]); the prototype stores the @@ -196,7 +186,7 @@ defaults, each grounded in the design document: ([REQ-RotateBLSKeys][dd-keys]); CIP-164 leaves the real rotation mechanism "to a follow-up PR amending this CIP" ([Design Decisions][cip-design]). -- **The pin.** A certificate is validated against the committee of the +- **The pin**. A certificate is validated against the committee of the epoch in which the announcing RB was produced; the CIP sizes the signer bitfield by exactly that committee ([Appendix B][cip-cddl]). A certificate landing just after an epoch boundary is therefore checked @@ -212,22 +202,22 @@ nine fields, with the mechanical `PParamsUpdate` and group companions; every field sits in the network and security groups, following [#5965][cl-5965] (all of its proposed parameters are assigned to exactly those two groups). -| Field | CIP-164 (Table 3) | Type | Notes | -| ----------------------------- | --------------------------------------- | ------------ | ----- | -| `leiosHeaderDiffusionPeriod` | L_hdr, header diffusion period | ℕ (slots) | | -| `leiosVotingPeriod` | L_vote, voting period | ℕ (slots) | | -| `leiosDiffusionPeriod` | L_diff, diffusion period | ℕ (slots) | [#5965][cl-5965] renames it the *additional* diffusion period | -| `leiosMaxEBSize` | S_EB, endorser block max size | ℕ (bytes) | bounds the reference structure itself, which [#5965][cl-5965] calls the EB *header* | -| `leiosMaxEBTxsSize` | S_EB-tx, referenceable transaction size | ℕ (bytes) | bounds the closure's total bytes, [#5965][cl-5965]'s EB *body* | -| `leiosCommitteeStakeCoverage` | σ_c, committee stake coverage | UnitInterval | | -| `leiosQuorumStakeThreshold` | τ, quorum stake threshold | UnitInterval | normative constraint τ < σ_c | -| `leiosMaxEBExUnits` | max Plutus steps and memory per EB | ExUnits | Table 3's two budget rows in one field, after [#5965][cl-5965]'s `OrdExUnits` | -| `leiosMaxRefScriptSizePerEB` | (not in the table) | ℕ (bytes) | from [#5965][cl-5965]; the per-EB analog of `maxRefScriptSizePerBlock` | - -Table 3's remaining row, the ranking-block max size S_RB, is the existing +| Field | CIP-164 (Table 3) | Type | Notes | +| ----------------------------- | ----------------------------------------- | ------------ | ----- | +| `leiosHeaderDiffusionPeriod` | `L_hdr`, header diffusion period | ℕ (slots) | | +| `leiosVotingPeriod` | `L_vote`, voting period | ℕ (slots) | | +| `leiosDiffusionPeriod` | `L_diff`, diffusion period | ℕ (slots) | [#5965][cl-5965] renames it the *additional* diffusion period | +| `leiosMaxEBSize` | `S_EB`, endorser block max size | ℕ (bytes) | bounds the reference structure itself, which [#5965][cl-5965] calls the EB *header* | +| `leiosMaxEBTxsSize` | `S_EB-tx`, referenceable transaction size | ℕ (bytes) | bounds the closure's total bytes, [#5965][cl-5965]'s EB *body* | +| `leiosCommitteeStakeCoverage` | `σ_c`, committee stake coverage | UnitInterval | | +| `leiosQuorumStakeThreshold` | `τ`, quorum stake threshold | UnitInterval | normative constraint `τ < σ_c` | +| `leiosMaxEBExUnits` | max Plutus steps and memory per EB | ExUnits | Table 3's two budget rows in one field, after [#5965][cl-5965]'s `OrdExUnits` | +| `leiosMaxRefScriptSizePerEB` | (not in the table) | ℕ (bytes) | from [#5965][cl-5965]; the per-EB analog of `maxRefScriptSizePerBlock` | + +Table 3's remaining row, the ranking-block max size `S_RB`, is the existing `maxBlockSize`; there is no new field ([#5965][cl-5965] maps it to -`ppMaxBBSize`). Well-formedness: τ < σ_c is normative ("Must satisfy -τ < σ_c", [Table 3][cip-params]) and joins positivity of the periods and +`ppMaxBBSize`). Well-formedness: `τ < σ_c` is normative ("Must satisfy +`τ < σ_c`", [Table 3][cip-params]) and joins positivity of the periods and sizes in the parameter well-formedness predicate; the constraint is what keeps a quorum achievable inside the committee's guaranteed stake coverage. Types follow the spec's house conventions; [#5965][cl-5965]'s `SlotInterval`, @@ -238,31 +228,27 @@ not enter the spec. ## Availability -The rules take the closure as input and never ask whether data is available. -The block, as the spec sees it, is the resolved block: alongside the -certificate it carries the certified EB and the closure ("the ledger must be -provided with all endorsed transactions resolved", -[REQ-LedgerResolvedBlockValidation][dd-blockval]), and a matching premise -checks the closure against the EB's references pointwise, hash and declared -size. Availability is a consensus and storage concern; CIP-164 keeps EBs out -of chain validity altogether ("EBs are treated as auxiliary data that do not -affect chain validity or selection decisions", -[Chain Selection][cip-chainsel]), and a certificate whose closure has not yet -arrived is a block consensus cannot yet hand to the ledger, not a new failure -mode. Two wire artifacts deliberately stay out of the rules: the header's -`certified_eb` bit is a syncing optimization, derived in the spec from the -presence of the body's certificate; and a wrong `announced_eb_size` makes -nothing invalid — "neither the RB header nor the RB are invalid. But no -honest node should vote for the EB" ([Inclusion Rules][cip-inclusion]) — so -announcement-size agreement belongs to the voters' checks, not to block -validity. +The rules take the closure as input and never ask whether data is available. The +block, as the spec sees it, is the resolved block: alongside the certificate it +carries the certified EB and the closure ("the ledger must be provided with all +endorsed transactions resolved", [REQ-LedgerResolvedBlockValidation][dd-blockval]), +and a matching premise checks the closure against the EB's references pointwise, hash +and declared size. Availability is a consensus and storage concern; CIP-164 keeps +EBs out of chain validity altogether ("EBs are treated as auxiliary data that do not +affect chain validity or selection decisions", [Chain Selection][cip-chainsel]), and +a certificate whose closure has not yet arrived is a block consensus cannot yet hand +to the ledger, not a new failure mode. Two wire artifacts deliberately stay out of +the rules: the header's `certified_eb` bit is a syncing optimization, derived in the +spec from the presence of the body's certificate; and a wrong `announced_eb_size` +makes nothing invalid: "neither the RB header nor the RB are invalid, but no +honest node should vote for the EB" ([Inclusion Rules][cip-inclusion]). Thus, +announcement-size agreement belongs to the voters' checks, not to block validity. ## The consensus↔ledger interface -The interface proposed by Nicolas Frisby in the implementation design -discussion shapes the consensus↔ledger boundary as eight functions. The -table maps each to its skeleton counterpart, or records what stays outside -the skeleton and why. +The interface proposed by Nicolas Frisby in the implementation design discussion +shapes the consensus↔ledger boundary as eight functions. The table maps each to its +skeleton counterpart, or records what stays outside the skeleton and why. | Proposed function | Skeleton counterpart | | ----------------------------- | -------------------- | @@ -275,13 +261,12 @@ the skeleton and why. | `reapplyTxForVoting` | Follow-up. The minimal-checks variant; its agreement with `applyTxForVoting` on previously validated transactions is the certified-application soundness theorem. | | `forgetVotingLedgerState` | Follow-up. The projection back to the ledger state, with the evident round-trip law against initialization. | -The protocol-level Agda specification consumes exactly this division: its -base-layer interface submits ranking blocks carrying -`txsOrEbCert : List Tx ⊎ EBCert` and asks the base layer for a single -judgment, the certificate check `V-chkCerts`, which is `ValidCert`'s role -here. The node-local vote conditions (header arrival, equivocation, -deadlines, chain position: CIP [vote conditions 1–4][cip-step3]) stay on its -side of the line, and `ValidEB` carries the ledger-checkable remainder +The protocol-level Agda specification consumes exactly this division: its base-layer +interface submits ranking blocks carrying `txsOrEbCert : List Tx ⊎ EBCert` and asks +the base layer for a single judgment, the certificate check `V-chkCerts`, which is +`ValidCert`'s role here. The node-local vote conditions (header arrival, +equivocation, deadlines, chain position: CIP [vote conditions 1–4][cip-step3]) stay +on its side of the line, and `ValidEB` carries the ledger-checkable remainder (conditions 5 and 6). [CIP-164]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md From a658c89e4907f3746a816461960ab0fc1624626f Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 19 Aug 2026 00:02:42 -0600 Subject: [PATCH 03/12] Address review: committee pin, quorum rationale, isValid determinism Three review-driven clarifications. The committee snapshot bullet now says the skeleton consumes the committee through the announcement pin and defers epoch-state materialization (an implementation shape, per REQ-LedgerStateVotingCommittee) to follow-up, matching the module map. The tau < sigma_c rationale claims only reachability by a fully keyed committee, deferring to the keyless-seat caveat. The full-rules and availability sections record why certified application is unambiguous: the UTXOS premise ties isValid to actual phase-2 evaluation, and the CIP reference hash covers the complete transaction bytes. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 36 ++++++++++++++++++++++++------------ 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index e093a07fa8..142b73a765 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -78,10 +78,13 @@ separate reapply relation. Phase-2 failures need no special account. Spec-level transactions carry their `isValid` flag, so `LEDGERS` covers collateral-forfeiting transactions in a closure -exactly as it does in a block body. Whether the wire format should carry those flags -is an open upstream question (the CIP's EB [CDDL][cip-cddl] has no validity bits, -while the [design document][dd-blockval] proposes adding them) and does not touch the -relational rules. +exactly as it does in a block body. The flag is not a free input: the `UTXOS` rule +requires `evalP2Scripts … ≡ IsValidFlagOf txTop`, forcing the flag to agree with +actual phase-2 evaluation against the state the closure runs in, so a closure +matching an EB's references admits at most one derivable application. Whether the +wire format should carry those flags is an open upstream question (the CIP's EB +[CDDL][cip-cddl] has no validity bits, while the [design document][dd-blockval] +proposes adding them) and does not touch the relational rules. ## Environment and ordering @@ -161,9 +164,12 @@ the design document: - **Snapshot**. The committee for an epoch derives from the stake distribution available at the epoch boundary, which is the pool-stake distribution the ledger already maintains for leader election (`PoolDistr` in the implementation; - [REQ-StakeBasedCommitteeSelection][dd-committee]). This is materialized into the - epoch state at the boundary rather than recomputed per use - ([REQ-LedgerStateVotingCommittee][dd-certver]). + [REQ-StakeBasedCommitteeSelection][dd-committee]). The implementation + materializes the committee in the ledger state at the boundary rather than + recomputing it per use ([REQ-LedgerStateVotingCommittee][dd-certver]); the + skeleton's rules consume the committee only through the announcement pin, and + materializing it as an epoch-state field is follow-up work together with the + concrete construction, which is why the module map edits no epoch module. - **Order and indices**. The descending-stake order fixes the seat indices that votes (`voter_id`) and certificate bitfields address. The CIP names no tie-break; the design document breaks ties by pool id, and the skeleton adopts @@ -218,8 +224,11 @@ Table 3's remaining row, the ranking-block max size `S_RB`, is the existing `maxBlockSize`; there is no new field ([#5965][cl-5965] maps it to `ppMaxBBSize`). Well-formedness: `τ < σ_c` is normative ("Must satisfy `τ < σ_c`", [Table 3][cip-params]) and joins positivity of the periods and -sizes in the parameter well-formedness predicate; the constraint is what -keeps a quorum achievable inside the committee's guaranteed stake coverage. +sizes in the parameter well-formedness predicate. The constraint makes a quorum +arithmetically reachable by a fully keyed committee (truncation guarantees committee +stake of at least `σ_c` of the total, and `τ < σ_c` puts the threshold strictly +inside that coverage); keyless seats can still leave the signable stake short of `τ`, +as the committee section records. Types follow the spec's house conventions; [#5965][cl-5965]'s `SlotInterval`, `Word32`, and `OrdExUnits` are the Haskell counterparts, and name or type divergences get recorded in module prose. The network characteristics of the @@ -233,9 +242,12 @@ block, as the spec sees it, is the resolved block: alongside the certificate it carries the certified EB and the closure ("the ledger must be provided with all endorsed transactions resolved", [REQ-LedgerResolvedBlockValidation][dd-blockval]), and a matching premise checks the closure against the EB's references pointwise, hash -and declared size. Availability is a consensus and storage concern; CIP-164 keeps -EBs out of chain validity altogether ("EBs are treated as auxiliary data that do not -affect chain validity or selection decisions", [Chain Selection][cip-chainsel]), and +and declared size; the CIP documents the reference hash as covering the complete +transaction bytes ([Appendix B][cip-cddl]), so the references pin the closure's full +content, not only the transaction bodies. Availability is a consensus and storage +concern; CIP-164 keeps EBs out of chain validity altogether ("EBs are treated as +auxiliary data that do not affect chain validity or selection decisions", +[Chain Selection][cip-chainsel]), and a certificate whose closure has not yet arrived is a block consensus cannot yet hand to the ledger, not a new failure mode. Two wire artifacts deliberately stay out of the rules: the header's `certified_eb` bit is a syncing optimization, derived in the From e8dfdc85a41fe50c68379c949338e71c3503e591 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 19 Aug 2026 00:21:48 -0600 Subject: [PATCH 04/12] Address second review round: GovStructure threading, precision fixes The voting-crypto threading moves from AbstractFunctions to a GovStructure field supplied through TransactionStructure: Certs sees only GovStructure and sits upstream of AbstractFunctions (Abstract imports Certs), so the original threading could not express the proof-of-possession premise in POOL. The module map now edits Gov/Base and Transaction instead of Abstract, six modules in all. Also from review: the voting-state accumulators now name every cumulative ValidEB bound including reference-script bytes; the protocol-level spec note is an intended correspondence (V-chkCerts is declared there but not yet called by its rules); the registration field is sppLeiosKey on StakePoolParams, spsLeiosKey being the pool-state mirror. Self-review: restored the verbatim Inclusion Rules quotation, resolved an ambiguous pronoun in the threading rationale, and repaired two reflow seams. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 60 +++++++++++++++++++++++---------------- 1 file changed, 35 insertions(+), 25 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index 142b73a765..aef8dd8731 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -29,15 +29,22 @@ layer. ## Module placement Leios lands in the Dijkstra era as an additive subtree -`Ledger.Dijkstra.Specification.Leios.*` plus minimal edits to five existing modules; +`Ledger.Dijkstra.Specification.Leios.*` plus minimal edits to six existing modules; no separate era, and no change to `Ledger.Core`. CIP-164 requires a new ledger era for the block-format change ([Versioning][cip-versioning]), and the implementation prototypes Leios in Dijkstra ([#5626][cl-5626] targets `eras/dijkstra`), so the Dijkstra specification is where the rules belong; keeping the new material in its own subtree keeps merges from `master` cheap. The abstract voting crypto is a -`LeiosAbstract` record threaded as a new field of `AbstractFunctions`, so the -signatures of the edited modules do not change; promoting the aggregate-signature -abstraction into `Ledger.Core`, where Peras could share it, is follow-up work. +`LeiosAbstract` record threaded as a new field of `GovStructure`, the era's bundle of +abstract structures, and supplied through `TransactionStructure`. This placement is +forced by the import order: the proof-of-possession premise lives in `POOL`, inside +`Certs`, which sees only `GovStructure` and sits upstream of `AbstractFunctions`, so +threading the crypto through `AbstractFunctions` would leave registration unable to +state the check. A +`GovStructure` field reaches `Certs` and every rule module downstream of the +transaction telescope without changing any module signature. Promoting the +aggregate-signature abstraction into `Ledger.Core` (`CryptoStructure`), where Peras +could share it, stays follow-up work. ```text src/Ledger/Dijkstra/Specification/ @@ -47,7 +54,8 @@ src/Ledger/Dijkstra/Specification/ │ ├── Types.lagda.md -- EndorserBlock, Announcement, Vote, Certificate │ ├── Committee.lagda.md -- Seat, Committee, quorum arithmetic │ └── Validity.lagda.md -- ValidVote, ValidCert, ValidEB -├── Abstract.lagda.md -- edit: leiosAbstract field in AbstractFunctions +├── Gov/Base.lagda.md -- edit: leiosAbstract field in GovStructure +├── Transaction.lagda.md -- edit: supply leiosAbstract via TransactionStructure ├── PParams.lagda.md -- edit: the Leios parameter block ├── Certs.lagda.md -- edit: voting key in StakePoolParams ├── BlockBody.lagda.md -- edit: announcement/certificate fields, BBODY premises @@ -90,7 +98,7 @@ proposes adding them) and does not touch the relational rules. For a block `B` at slot `s_B` carrying a certificate for the EB announced by its predecessor `A` at slot `s_A` (admissible only when -`s_B ≥ s_A + 3·L_hdr + L_vote + L_diff`; [Step 5][cip-step5]) the rules fix the +`s_B ≥ s_A + 3·L_hdr + L_vote + L_diff`; [Step 5][cip-step5]), the rules fix the following total order: 1. **EB application**. The closure applies via `LEDGERS` to the ledger state left @@ -184,7 +192,8 @@ the design document: Keyless stake can therefore lower the quorum a certificate is able to reach, never inflate it. - **Keys**. Pool registration carries the voting key with its proof of - possession, as in the prototype's `spsLeiosKey` ([#5626][cl-5626]), and + possession, as in the prototype's `sppLeiosKey` on `StakePoolParams` + ([#5626][cl-5626]; `spsLeiosKey` is its pool-state mirror), and registration checks the proof ([REQ-CheckProofOfPossession][dd-committee]); the prototype stores the key without checking the proof, a divergence to flag upstream. Rotation @@ -204,9 +213,9 @@ the design document: CIP-164's [Table 3][cip-params] declares the Leios parameters governance-tunable; cardano-ledger [#5965][cl-5965] maps them onto the Dijkstra `PParams` and adds one bound the table lacks. The skeleton adds -nine fields, with the mechanical `PParamsUpdate` and group companions; every -field sits in the network and security groups, following [#5965][cl-5965] -(all of its proposed parameters are assigned to exactly those two groups). +nine fields, with the mechanical `PParamsUpdate` and group companions; every field +sits in the network and security groups, the assignment [#5965][cl-5965] gives all +of its proposed parameters. | Field | CIP-164 (Table 3) | Type | Notes | | ----------------------------- | ----------------------------------------- | ------------ | ----- | @@ -247,12 +256,12 @@ transaction bytes ([Appendix B][cip-cddl]), so the references pin the closure's content, not only the transaction bodies. Availability is a consensus and storage concern; CIP-164 keeps EBs out of chain validity altogether ("EBs are treated as auxiliary data that do not affect chain validity or selection decisions", -[Chain Selection][cip-chainsel]), and -a certificate whose closure has not yet arrived is a block consensus cannot yet hand -to the ledger, not a new failure mode. Two wire artifacts deliberately stay out of -the rules: the header's `certified_eb` bit is a syncing optimization, derived in the -spec from the presence of the body's certificate; and a wrong `announced_eb_size` -makes nothing invalid: "neither the RB header nor the RB are invalid, but no +[Chain Selection][cip-chainsel]), and a certificate whose closure has not yet +arrived is a block consensus cannot yet hand to the ledger, not a new failure mode. +Two wire artifacts deliberately stay out of the rules: the header's `certified_eb` +bit is a syncing optimization, derived in the spec from the presence of the body's +certificate; and a wrong `announced_eb_size` +makes nothing invalid: "neither the RB header nor the RB are invalid. But no honest node should vote for the EB" ([Inclusion Rules][cip-inclusion]). Thus, announcement-size agreement belongs to the voters' checks, not to block validity. @@ -267,19 +276,20 @@ skeleton counterpart, or records what stays outside the skeleton and why. | `applyCertifiedEb` | The certificate branch of the block and chain rules: `ValidCert` plus the closure applied via `LEDGERS` from the announcing state, per the ordering above. | | `validateCertificate` | `ValidCert` (`Leios.Validity`): signers are seats of the pinned committee, the aggregate signature verifies over (slot, EB hash), and the signers' stake meets τ times the total active stake. The contextual half — agreement with the pending announcement, the timing window — sits as block/chain premises. | | `validateVote` | `ValidVote` (`Leios.Validity`): the voter index denotes a keyed committee seat whose key verifies the signature over (slot, EB hash). Votes never appear on-chain individually; this is the meaning consensus uses to filter votes before aggregation. | -| `doesEpochCommitteeIncludeMe` | Decidable membership on `Committee` (`Leios.Committee`), a seat lookup by pool. The "me" binding is consensus-local; the ledger side is the seat lookup on the materialized committee ([REQ-LedgerStateVotingCommittee][dd-certver]). | -| `initializeVotingLedgerState` | Follow-up (the voting-state interface). Meaning fixed now: the announcing block's post-`BBODY` state paired with fresh EB accumulators (bytes, `ExUnits`). | +| `doesEpochCommitteeIncludeMe` | Decidable membership on `Committee` (`Leios.Committee`), a seat lookup by pool. The "me" binding is consensus-local; the ledger side is the seat lookup, which the implementation serves from its materialized committee ([REQ-LedgerStateVotingCommittee][dd-certver]). | +| `initializeVotingLedgerState` | Follow-up (the voting-state interface). Meaning fixed now: the announcing block's post-`BBODY` state paired with fresh EB accumulators, one per cumulative `ValidEB` bound: referenced-transaction bytes, `ExUnits`, and reference-script bytes. | | `applyTxForVoting` | Follow-up. Meaning fixed now: one LEDGER step plus accumulator updates and bound checks; folding it over the closure from the initialized state succeeds exactly when `ValidEB`'s extension-and-bounds conjuncts hold. | | `reapplyTxForVoting` | Follow-up. The minimal-checks variant; its agreement with `applyTxForVoting` on previously validated transactions is the certified-application soundness theorem. | | `forgetVotingLedgerState` | Follow-up. The projection back to the ledger state, with the evident round-trip law against initialization. | -The protocol-level Agda specification consumes exactly this division: its base-layer -interface submits ranking blocks carrying `txsOrEbCert : List Tx ⊎ EBCert` and asks -the base layer for a single judgment, the certificate check `V-chkCerts`, which is -`ValidCert`'s role here. The node-local vote conditions (header arrival, -equivocation, deadlines, chain position: CIP [vote conditions 1–4][cip-step3]) stay -on its side of the line, and `ValidEB` carries the ledger-checkable remainder -(conditions 5 and 6). +The protocol-level Agda specification is shaped for the same division: its +base-layer interface submits ranking blocks carrying `txsOrEbCert : List Tx ⊎ EBCert` +and declares a single base-layer judgment, the certificate check `V-chkCerts`, the +role `ValidCert` is intended to fill. (An intended correspondence: that +specification declares the hook but its transition rules do not yet call it.) The +node-local vote conditions (header arrival, equivocation, deadlines, chain position: +CIP [vote conditions 1–4][cip-step3]) stay on its side of the line, and `ValidEB` +carries the ledger-checkable remainder (conditions 5 and 6). [CIP-164]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md [cip-step3]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#step-3-committee-validation From 4f8b67f4e47e9877439ebd8d5c298aca240c5fe8 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 19 Aug 2026 19:54:30 -0600 Subject: [PATCH 05/12] Design note: fold in trace-verifier field review Amendments from the 2026-08-19 review grounded in three weeks of Musashi trace-verifier data: make the pending-announcement lifetime explicit (any applied block replaces it with its own announcement or clears it; protocol-spec cross-reference), state that parameter well-formedness does not imply certifiability (with the observed keyless-seat numbers), promote the pool-id tie-break to a stated law of the abstract selection function, record the minCertificationGap divergence (prototype 10 vs formula 14), mark the EB-identifier hash preimage as a named conformance prerequisite, and declare rewards and incentives out of scope with the CIP's own words. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 58 ++++++++++++++++++++++++++++++++++----- 1 file changed, 51 insertions(+), 7 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index aef8dd8731..3de04d1d7f 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -117,9 +117,16 @@ following total order: in the RB" ([Step 5][cip-step5]) — so its body contributes the certificate premises and the usual bookkeeping. +One implementation constant already diverges from this window: the prototype's +`minCertificationGap` is 10 slots where `3·L_hdr + L_vote + L_diff` gives 14 with +the Musashi parameters. Both sides are live and measured by the trace-verifier +work; the divergence is flagged upstream, like the proof-of-possession divergence in +the committee section. + A block may announce its own EB while certifying its predecessor's ("it may optionally announce its own EB for future certification", [Step 5][cip-step5]); it -consumes A's announcement and records its own afterwards. Relationally, the +consumes A's announcement and records its own afterwards; a block that neither +certifies nor announces still clears the pending announcement. Relationally, the certificate premises and the application premise are simultaneous conjuncts; only an executable implementation orders certificate verification against closure application. @@ -155,8 +162,14 @@ the relational spec distinguishes why; a predicate-failure taxonomy belongs to t executability, and the five checks are its raw material when it comes. The missing-certificate case needs no bookkeeping at all: only the immediate successor may certify, and otherwise "the EB certificate cannot be included and the EB is -discarded" ([Step 5][cip-step5]); the pending announcement is simply replaced by the -next one, with no ledger trace and no expiry accounting. For consensus, the reading +discarded" ([Step 5][cip-step5]). The pending announcement is a function of the +chain head alone: applying any block replaces it with that block's own announcement, +or clears it when the block announces nothing, so no announcement survives an +intervening block, with no ledger trace and no expiry accounting. The +protocol-level spec models the same rule: the certifiable EB is the one announced by +`currentRB`, the head (`Leios/Protocol.lagda.md`, with the `Base₂` certificate +premise in `Linear.lagda.md`; [ouroboros-leios-formal-spec][leios-formal-spec]). +For consensus, the reading is the usual one: an invalid certificate makes an invalid block, nothing more drastic. ## The committee @@ -181,16 +194,28 @@ the design document: - **Order and indices**. The descending-stake order fixes the seat indices that votes (`voter_id`) and certificate bitfields address. The CIP names no tie-break; the design document breaks ties by pool id, and the skeleton adopts - that. Selection enters the skeleton abstractly, as a function with stated laws - (registered pools, descending stake, coverage `σ_c`); the concrete construction can - land later without disturbing anything downstream of the laws. + that as a stated law, not a remark: equal-stake pools are common at the + committee tail, and two implementations that order ties differently disagree + about the validity of every certificate. Selection enters the skeleton + abstractly, as a function with stated laws (membership by stake truncation at + coverage `σ_c`, independent of key registration; descending stake with ties + broken by ascending pool id; determinism of the order); the concrete + construction can land later without disturbing anything downstream of the laws, + but the order itself cannot. The byte-exact comparison on pool ids is a + conformance detail to confirm upstream. - **Keyless seats**. Membership is by stake alone, "independent of key registration" ([REQ-KeylessSeat][dd-committee]): a selected pool without a registered voting key still occupies its seat and holds its weight, but the seat cannot sign, and a certificate whose bitfield sets a keyless seat is invalid ([REQ-LedgerCertificateVerification][dd-certver]). Keyless stake can therefore lower the quorum a certificate is able to - reach, never inflate it. + reach, never inflate it. Parameter well-formedness therefore does not imply + certifiability: the skeleton names the gap with a `certifiable` predicate (keyed + committee stake at least `τ` of the total active stake), so the condition + implementers must monitor has a name. The gap is not hypothetical: on the + Musashi testnet (2026-08, trace-verifier observations) 19 of 66 registered pools + had no voting key and certificates appeared on roughly 3% of blocks, with every + individual rule satisfied (cf. [ouroboros-leios #1046][ol-1046]). - **Keys**. Pool registration carries the voting key with its proof of possession, as in the prototype's `sppLeiosKey` on `StakePoolParams` ([#5626][cl-5626]; `spsLeiosKey` is its pool-state mirror), and @@ -258,6 +283,12 @@ concern; CIP-164 keeps EBs out of chain validity altogether ("EBs are treated as auxiliary data that do not affect chain validity or selection decisions", [Chain Selection][cip-chainsel]), and a certificate whose closure has not yet arrived is a block consensus cannot yet hand to the ledger, not a new failure mode. + +One boundary in this section deserves an explicit warning. The EB identifier is the +hash of the reference structure itself, which the skeleton abstracts as `hashEBRefs` +without pinning the byte-exact preimage. Cardano has been here before (the +block-body hash's segmented preimage exists only in implementation internals), so +pinning that preimage is a named conformance prerequisite, not an afterthought. Two wire artifacts deliberately stay out of the rules: the header's `certified_eb` bit is a syncing optimization, derived in the spec from the presence of the body's certificate; and a wrong `announced_eb_size` @@ -291,6 +322,17 @@ node-local vote conditions (header arrival, equivocation, deadlines, chain posit CIP [vote conditions 1–4][cip-step3]) stay on its side of the line, and `ValidEB` carries the ledger-checkable remainder (conditions 5 and 6). +## Out of scope: rewards and incentives + +The skeleton models no change to the reward calculation, and neither does the +protocol: "Leios does not require any changes to incentives in Cardano" +([Incentives][cip-incentives]); the CIP cites the existing ledger-specification +rewards module as "the current and unchanged specification of rewards". Blocks-made +accounting is likewise untouched (a certificate-bearing block counts like any +other). Should a Leios incentive mechanism ever become normative (rewards for +voting or EB production, tiered fees), it enters through the full roadmap, not this +skeleton. + [CIP-164]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md [cip-step3]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#step-3-committee-validation [cip-step5]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#step-5-chain-inclusion @@ -314,3 +356,5 @@ carries the ledger-checkable remainder (conditions 5 and 6). [cl-5626]: https://github.com/IntersectMBO/cardano-ledger/pull/5626 [cl-5965]: https://github.com/IntersectMBO/cardano-ledger/issues/5965 [leios-formal-spec]: https://github.com/input-output-hk/ouroboros-leios-formal-spec +[ol-1046]: https://github.com/input-output-hk/ouroboros-leios/issues/1046 +[cip-incentives]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#incentives From 561e2de61494520aa89f64a0d11c1207720c9c84 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 24 Aug 2026 20:56:31 -0600 Subject: [PATCH 06/12] improvements and clarifications --- docs/leios/design-note.md | 474 +++++++++++++++++++++----------------- 1 file changed, 263 insertions(+), 211 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index 3de04d1d7f..d33e142cd8 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -1,50 +1,59 @@ -# Leios ledger rules: the skeleton's default decisions - -This note records the defaults behind the skeleton formalization of the Ouroboros -Linear Leios ledger rules ([CIP-164]) in the Dijkstra-era specification, so that the -Agda encodes decisions instead of debating them. +# Leios ledger formalization (LLF) plan +This note records the defaults behind the formalization of the Ouroboros Linear +Leios ledger rules ([CIP-164]) in the Dijkstra-era specification, so that our +Agda work merely encodes these decisions instead of debating them. Each subsection states one default, cites the source that fixes it, and gives the rationale; where every source is silent, the note picks a default and says so. +We will refer to the plan that this note describes as the +**Leios Ledger Formalization** plan, or **LLF** for short. + Comments from the consensus and ledger implementers are welcome on all of it; the -skeleton proceeds on these defaults and folds corrections in as they arrive. +LLF plan proceeds on these defaults and folds corrections in as they arrive. -In CIP-164's protocol, a block producer may announce an *endorser block* (EB), an +In protocol of [CIP-164], a block producer may announce an *endorser block* (EB), an ordered list of transaction references (hash and declared byte size), alongside its ordinary *ranking block* (RB). A committee of stake pools votes on the announced EB, a quorum of votes is aggregated into a *certificate*, and the immediately following RB may carry that certificate, at which point the EB's transactions enter the ledger. -Throughout this note, the *closure* of an EB means its referenced transactions, +Throughout this note, the **closure** of an EB means its referenced transactions, resolved and taken in reference order. -The note draws on the following sources: [CIP-164] (the normative text), the -implementation team's [Leios design document][design-doc] with its requirement -register (REQ-…), the cardano-ledger prototype ([#5626][cl-5626]: announcement, -certificate bit, and voting-key carriage in the Dijkstra era) and its parameter -proposal ([#5965][cl-5965]), and the protocol-level Agda specification -[ouroboros-leios-formal-spec][leios-formal-spec], for which the ledger is the base -layer. +The note draws on the following sources: + ++ [CIP-164] (the normative text), ++ the implementation team's [Leios design document][design-doc] with its requirement + register (`REQ-…`), ++ the cardano-ledger prototype ([#5626][cl-5626]: announcement, certificate bit, + and voting-key carriage in the Dijkstra era) and its parameter proposal + ([#5965][cl-5965]); ++ the protocol-level Agda specification + [ouroboros-leios-formal-spec][leios-formal-spec], for which the ledger is the + base layer. ## Module placement Leios lands in the Dijkstra era as an additive subtree `Ledger.Dijkstra.Specification.Leios.*` plus minimal edits to six existing modules; -no separate era, and no change to `Ledger.Core`. CIP-164 requires a new ledger era -for the block-format change ([Versioning][cip-versioning]), and the implementation -prototypes Leios in Dijkstra ([#5626][cl-5626] targets `eras/dijkstra`), so the -Dijkstra specification is where the rules belong; keeping the new material in its own -subtree keeps merges from `master` cheap. The abstract voting crypto is a -`LeiosAbstract` record threaded as a new field of `GovStructure`, the era's bundle of -abstract structures, and supplied through `TransactionStructure`. This placement is -forced by the import order: the proof-of-possession premise lives in `POOL`, inside -`Certs`, which sees only `GovStructure` and sits upstream of `AbstractFunctions`, so -threading the crypto through `AbstractFunctions` would leave registration unable to -state the check. A -`GovStructure` field reaches `Certs` and every rule module downstream of the -transaction telescope without changing any module signature. Promoting the -aggregate-signature abstraction into `Ledger.Core` (`CryptoStructure`), where Peras -could share it, stays follow-up work. +no separate era, and no change to `Ledger.Core`. + +[CIP-164] requires a new ledger era for the block-format change +([Versioning][cip-versioning]), and the implementation prototypes Leios in +Dijkstra ([#5626][cl-5626] targets `eras/dijkstra`), so the Dijkstra specification +is where the rules belong; keeping the new material in its own subtree keeps +merges from `master` cheap. + +The abstract voting crypto is a `LeiosAbstract` record, included as a new field of +`GovStructure`, the era's bundle of abstract structures, and supplied through +`TransactionStructure`. This placement is forced by the import order: the +proof-of-possession premise lives in `POOL`, inside `Certs`, which sees only +`GovStructure` and sits upstream of `AbstractFunctions`. + +A `GovStructure` field reaches `Certs` and every rule module downstream of the +transaction telescope without changing any module signature.[^1] + +**Placement of new modules and which existing modules to touch**. ```text src/Ledger/Dijkstra/Specification/ @@ -64,27 +73,34 @@ src/Ledger/Dijkstra/Specification/ ## Certified application uses the full rules -The skeleton applies a certified EB's closure with the ordinary iterated LEDGER -relation (`LEDGERS`), exactly as `BBODY` applies a block's own transactions. CIP-164 -fixes what a vote attests: the closure forms "a valid extension of the RB that -announced it" ([vote condition 5][cip-step3]), under "the same validation rules used -in Praos, with phase-1 and phase-2 validation applying equally to both RB and EB -transactions" ([Ledger Management][cip-ledger]). `ValidEB`, the property a -certificate ultimately certifies, conjoins reference/closure agreement, nonemptiness -([vote condition 6][cip-step3]), the per-EB bounds, and this valid-extension -condition stated with `LEDGERS`. - -The implementation, by contrast, applies a certified closure by "reapplication with -minimal checks and UTxO updates", "omitting previously performed phase 1 & 2 +In this LLF plan, we will apply a certified EB's closure with the ordinary +iterated `LEDGER` relation (`LEDGERS`), exactly as `BBODY` applies a block's own +transactions. + +[CIP-164] fixes what a vote attests: + +> the closure forms "a valid extension of the RB that announced it" +> ([vote condition 5][cip-step3]), under "the same validation rules used +> in Praos, with phase-1 and phase-2 validation applying equally to both RB +> and EB transactions" ([Ledger Management][cip-ledger]). + +`ValidEB`, the property a certificate ultimately certifies, conjoins +reference/closure agreement, nonemptiness ([vote condition 6][cip-step3]), the +per-EB bounds, and this valid-extension condition stated with `LEDGERS`. + +The implementation, by contrast, applies a certified closure by "reapplication +with minimal checks and UTxO updates", "omitting previously performed phase 1 & 2 validation" ([CIP-164 Table 2][cip-params]; [REQ-LedgerTxNoValidation and -REQ-LedgerCheapReapply][dd-txlevels]). The skeleton treats that as an optimization, -not a semantics: the relation defines certified application by the full rules, and -the theorem that minimal reapplication agrees with the full rules on a closure some -quorum has validated is exactly the soundness result the optimization needs — a -follow-up proof, not a skeleton input. Nothing in the skeleton therefore needs a -separate reapply relation. - -Phase-2 failures need no special account. Spec-level transactions carry their +REQ-LedgerCheapReapply][dd-txlevels]). + +This LLF plan treats that as an optimization, not the semantics: the relation +defines certified application by the full rules, and the theorem that minimal +reapplication agrees with the full rules on a closure some quorum has validated is +exactly the soundness result the optimization needs. This would be a follow-up +proof, but not part of the initial LLF plan, so we will not include a separate +reapply relation. + +Phase-2 failures need no special accounting. Spec-level transactions carry their `isValid` flag, so `LEDGERS` covers collateral-forfeiting transactions in a closure exactly as it does in a block body. The flag is not a free input: the `UTXOS` rule requires `evalP2Scripts … ≡ IsValidFlagOf txTop`, forcing the flag to agree with @@ -101,146 +117,168 @@ predecessor `A` at slot `s_A` (admissible only when `s_B ≥ s_A + 3·L_hdr + L_vote + L_diff`; [Step 5][cip-step5]), the rules fix the following total order: -1. **EB application**. The closure applies via `LEDGERS` to the ledger state left - by A's block-body transition, in A's environment: slot `s_A` and the protocol - parameters in force at A. CIP-164: "EB transactions are validated against the - ledger state from the RB that announced the EB (i.e., the predecessor RB of the - certifying RB)" ([Ledger Management][cip-ledger]); the design document requires - the same ("the ledger must validate endorsed transactions against the ledger - state before updating it with the new ranking block", - [REQ-LedgerUntickedEBValidation][dd-blockval]). +1. **EB application**. The closure applies via `LEDGERS` to the ledger state + left by `A`'s block-body transition, in `A`'s environment: slot `s_A` and the + protocol parameters in force at `A`. + + [CIP-164][]: "EB transactions are validated against the ledger state from the + RB that announced the EB (i.e., the predecessor RB of the certifying RB)" + ([Ledger Management][cip-ledger]); the design document requires the same ("the + ledger must validate endorsed transactions against the ledger state before + updating it with the new ranking block", [REQ-LedgerUntickedEBValidation][dd-blockval]). + 2. **Tick**. The chain ticks to `s_B` on the EB-updated state; if an epoch boundary lies between the two blocks, the reward update, enactment, and the snapshots all see the closure's effects. -3. **Block body**. B's `BBODY` runs on the ticked state. B carries no transactions - of its own — "When a certificate is included, no further transactions are allowed - in the RB" ([Step 5][cip-step5]) — so its body contributes the certificate - premises and the usual bookkeeping. -One implementation constant already diverges from this window: the prototype's -`minCertificationGap` is 10 slots where `3·L_hdr + L_vote + L_diff` gives 14 with -the Musashi parameters. Both sides are live and measured by the trace-verifier -work; the divergence is flagged upstream, like the proof-of-possession divergence in -the committee section. +3. **Block body**. `B`'s `BBODY` runs on the ticked state. `B` carries no + transactions of its own: "When a certificate is included, no further + transactions are allowed in the RB" ([Step 5][cip-step5]); so its body + contributes the certificate premises and the usual bookkeeping. + +(The implementation already diverges from the lower bound +`s_B ≥ s_A + 3·L_hdr + L_vote + L_diff`. The prototype's `minCertificationGap` is +10 slots whereas `3·L_hdr + L_vote + L_diff` gives 14 with the Musashi parameters. +Both sides are live and measured by the trace-verifier work; the divergence is +flagged upstream, like the proof-of-possession divergence in the committee section.) A block may announce its own EB while certifying its predecessor's ("it may optionally announce its own EB for future certification", [Step 5][cip-step5]); it -consumes A's announcement and records its own afterwards; a block that neither +consumes `A`'s announcement and records its own afterwards; a block that neither certifies nor announces still clears the pending announcement. Relationally, the -certificate premises and the application premise are simultaneous conjuncts; only an -executable implementation orders certificate verification against closure +certificate premises and the application premise are simultaneous conjuncts; only +an executable implementation orders certificate verification against closure application. -One corollary settles the parameter-change question, on which the CIP is silent: -everything about an announced EB is evaluated in the announcing world. The closure -runs under A's parameters; the certificate is checked against the committee, the -total active stake, and the quorum threshold τ pinned at announcement; the timing -window uses the period lengths in force at A. A certificate proves what the voters -checked, and the voters could check only A's world; validating it against data none -of them could have seen would break that reading. The vote signature is bound to `s_A` -for the same reason: the binding "ensures voters validated the EB against the same -ledger state it extends when certified on chain" ([Vote Structure][cip-vote]). This -corollary is a note-set default to confirm with the implementers. +**Ordering corollary**. One corollary settles the parameter-change question, on +which the CIP is silent: everything about an announced EB is evaluated in the +announcing world. The closure runs under `A`'s parameters; the certificate is +checked against the committee, the total active stake, and the quorum threshold +`τ` pinned at announcement; the timing window uses the period lengths in force at +A. A certificate proves what the voters checked, and the voters could check only +`A`'s world; validating it against data none of them could have seen would break +that reading. The vote signature is bound to `s_A` for the same reason: the +binding "ensures voters validated the EB against the same ledger state it extends +when certified on chain" ([Vote Structure][cip-vote]). +*This corollary is assumed in order to fix this LLF plan, but it should be confirm with the implementers.* This ordering also answers the following open question of the design document: "How much of the work lives in `BBODY` itself versus a dedicated EB-body rule, and the precise ordering of applying the closure relative to verifying the certificate" ([Certificate verification][dd-certver]). There is no dedicated EB-body rule: the -certificate checks and the closure's application are premises of the existing block -and chain transitions, with the pending announcement threaded through the chain-level -context and application ordered before the tick as above. +certificate checks and the closure's application are premises of the existing +block and chain transitions, with the pending announcement carried through the +chain-level context and application ordered before the tick, as above. ## Certificate failure is the absence of a transition CIP-164's [Certificate Validation][cip-certval] lists five checks that must pass -"before accepting the block". The skeleton renders failure the way the spec renders -every block fault: a block whose certificate fails a check, or that pairs a -certificate with transactions of its own, or that certifies before the window opens, -simply admits no `BBODY`/`CHAIN` derivation. The block is invalid, and nothing in -the relational spec distinguishes why; a predicate-failure taxonomy belongs to the -`Computational` instances and the conformance work, deferred with the rest of -executability, and the five checks are its raw material when it comes. The -missing-certificate case needs no bookkeeping at all: only the immediate successor -may certify, and otherwise "the EB certificate cannot be included and the EB is -discarded" ([Step 5][cip-step5]). The pending announcement is a function of the -chain head alone: applying any block replaces it with that block's own announcement, -or clears it when the block announces nothing, so no announcement survives an -intervening block, with no ledger trace and no expiry accounting. The -protocol-level spec models the same rule: the certifiable EB is the one announced by -`currentRB`, the head (`Leios/Protocol.lagda.md`, with the `Base₂` certificate -premise in `Linear.lagda.md`; [ouroboros-leios-formal-spec][leios-formal-spec]). -For consensus, the reading -is the usual one: an invalid certificate makes an invalid block, nothing more drastic. +"before accepting the block." The LFF plan renders failure the way the spec +renders every block fault: a block whose certificate fails a check, or that pairs +a certificate with transactions of its own, or that certifies before the window +opens, simply admits no `BBODY`/`CHAIN` derivation. The block is invalid, and +nothing in the relational spec distinguishes why. + +A predicate-failure taxonomy belongs to the `Computational` instances and the +conformance work, deferred with the rest of executability, and the five checks are +its raw material if/when it arrives as follow-up work. + +The missing-certificate case needs no bookkeeping at all: only the immediate +successor may certify, and otherwise "the EB certificate cannot be included and +the EB is discarded" ([Step 5][cip-step5]). + +The pending announcement is a function of the chain head alone: applying any block +replaces it with that block's own announcement, or clears it when the block +announces nothing, so no announcement survives an intervening block, with no +ledger trace and no expiry accounting. The protocol-level spec models the same +rule: the certifiable EB is the one announced by `currentRB`, the head +(`Leios/Protocol.lagda.md`, with the `Base₂` certificate premise in +`Linear.lagda.md`; [ouroboros-leios-formal-spec][leios-formal-spec]). +For consensus, the reading is the usual one: an invalid certificate makes an +invalid block. ## The committee -CIP-164 fixes the committee once per epoch by stake-based truncation: "pools are +[CIP-164] fixes the committee once per epoch by stake-based truncation: "pools are ordered by stake in descending order and selected, in order, until the cumulative -selected stake reaches" the coverage target `σ_c`, and the resulting committee "is -fixed for the entire epoch", with no per-EB sortition and no non-persistent voters -([Committee Structure][cip-committee]; the boundary procedure in [Epoch -Boundary][cip-epoch]). The skeleton adds the following defaults, each grounded in -the design document: - -- **Snapshot**. The committee for an epoch derives from the stake distribution - available at the epoch boundary, which is the pool-stake distribution the ledger - already maintains for leader election (`PoolDistr` in the implementation; - [REQ-StakeBasedCommitteeSelection][dd-committee]). The implementation - materializes the committee in the ledger state at the boundary rather than - recomputing it per use ([REQ-LedgerStateVotingCommittee][dd-certver]); the - skeleton's rules consume the committee only through the announcement pin, and - materializing it as an epoch-state field is follow-up work together with the - concrete construction, which is why the module map edits no epoch module. -- **Order and indices**. The descending-stake order fixes the seat indices that - votes (`voter_id`) and certificate bitfields address. The CIP names no - tie-break; the design document breaks ties by pool id, and the skeleton adopts - that as a stated law, not a remark: equal-stake pools are common at the - committee tail, and two implementations that order ties differently disagree - about the validity of every certificate. Selection enters the skeleton - abstractly, as a function with stated laws (membership by stake truncation at - coverage `σ_c`, independent of key registration; descending stake with ties - broken by ascending pool id; determinism of the order); the concrete - construction can land later without disturbing anything downstream of the laws, - but the order itself cannot. The byte-exact comparison on pool ids is a - conformance detail to confirm upstream. -- **Keyless seats**. Membership is by stake alone, "independent of key - registration" ([REQ-KeylessSeat][dd-committee]): a selected pool without - a registered voting key still occupies its seat and holds its weight, but - the seat cannot sign, and a certificate whose bitfield sets a keyless - seat is invalid ([REQ-LedgerCertificateVerification][dd-certver]). - Keyless stake can therefore lower the quorum a certificate is able to - reach, never inflate it. Parameter well-formedness therefore does not imply - certifiability: the skeleton names the gap with a `certifiable` predicate (keyed - committee stake at least `τ` of the total active stake), so the condition - implementers must monitor has a name. The gap is not hypothetical: on the - Musashi testnet (2026-08, trace-verifier observations) 19 of 66 registered pools - had no voting key and certificates appeared on roughly 3% of blocks, with every - individual rule satisfied (cf. [ouroboros-leios #1046][ol-1046]). -- **Keys**. Pool registration carries the voting key with its proof of - possession, as in the prototype's `sppLeiosKey` on `StakePoolParams` - ([#5626][cl-5626]; `spsLeiosKey` is its pool-state mirror), and - registration checks the proof - ([REQ-CheckProofOfPossession][dd-committee]); the prototype stores the - key without checking the proof, a divergence to flag upstream. Rotation - is re-registration, activated at an epoch boundary - ([REQ-RotateBLSKeys][dd-keys]); CIP-164 leaves the real rotation - mechanism "to a follow-up PR amending this CIP" - ([Design Decisions][cip-design]). -- **The pin**. A certificate is validated against the committee of the - epoch in which the announcing RB was produced; the CIP sizes the signer - bitfield by exactly that committee ([Appendix B][cip-cddl]). A - certificate landing just after an epoch boundary is therefore checked - against the announcing epoch's committee and total active stake, per the - ordering corollary above. +selected stake reaches" the coverage target `σ_c`, and the resulting committee +"is fixed for the entire epoch", with no per-EB sortition and no non-persistent +voters ([Committee Structure][cip-committee]; the boundary procedure in [Epoch +Boundary][cip-epoch]). + +The LLF adds the following defaults, each grounded in the design document: + ++ **Snapshot**. The committee for an epoch derives from the stake distribution + available at the epoch boundary, which is the pool-stake distribution the + ledger already maintains for leader election (`PoolDistr` in the + implementation; [REQ-StakeBasedCommitteeSelection][dd-committee]). + + The implementation materializes the committee in the ledger state at the + boundary rather than recomputing it per use + ([REQ-LedgerStateVotingCommittee][dd-certver]); the LLF's rules consume the + committee only through the announcement pin, and materializing it as an + epoch-state field is follow-up work together with the concrete construction, + which is why no epoch module appears among the touched modules in the [Module + placement](#module-placement) section above. + ++ **Order and indices**. The descending-stake order fixes the seat indices that + votes (`voter_id`) and certificate bitfields address. + + The CIP names no tie-break; the design document breaks ties by pool id, and the + LLF plan adopts that as a stated law, not a remark: equal-stake pools are + common at the committee tail, and two implementations that order ties + differently disagree about the validity of every certificate. + + Selection enters the LLF abstractly, as a function with stated laws (membership + by stake truncation at coverage `σ_c`, independent of key registration; + descending stake with ties broken by ascending pool id; determinism of the + order); the concrete construction can land later without disturbing anything + downstream of the laws, but the order itself cannot. The byte-exact comparison + on pool ids is a conformance detail to confirm upstream. + ++ **Keyless seats**. Membership is by stake alone, "independent of key + registration" ([REQ-KeylessSeat][dd-committee]): a selected pool without a + registered voting key still occupies its seat and holds its weight, but the + seat cannot sign, and a certificate whose bitfield sets a keyless seat is + invalid ([REQ-LedgerCertificateVerification][dd-certver]). Keyless stake can + therefore lower the quorum a certificate is able to reach, never inflate it. + + Parameter well-formedness therefore does not imply certifiability: the LLF + names the gap with a `certifiable` predicate (keyed committee stake at least + `τ` of the total active stake), so the condition implementers must monitor has + a name. + + The gap is not hypothetical: on the Musashi testnet (2026-08, trace-verifier + observations) 19 of 66 registered pools had no voting key and certificates + appeared on roughly 3% of blocks, with every individual rule satisfied + (cf. [ouroboros-leios #1046][ol-1046]). + ++ **Keys**. Pool registration carries the voting key with its proof of + possession, as in the prototype's `sppLeiosKey` on `StakePoolParams` + ([#5626][cl-5626]; `spsLeiosKey` is its pool-state mirror), and *registration* + checks the proof ([REQ-CheckProofOfPossession][dd-committee]); however, the + prototype stores the key *without checking the proof*, which is a divergence to + flag upstream. + + Rotation is re-registration, activated at an epoch boundary + ([REQ-RotateBLSKeys][dd-keys]); CIP-164 leaves the real rotation mechanism + "to a follow-up PR amending this CIP" ([Design Decisions][cip-design]). + ++ **The pin**. A certificate is validated against the committee of the epoch in + which the announcing RB was produced; the CIP sizes the signer bitfield by + exactly that committee ([Appendix B][cip-cddl]). A certificate landing just + after an epoch boundary is therefore checked against the announcing epoch's + committee and total active stake, per the ordering corollary above. ## Protocol parameters -CIP-164's [Table 3][cip-params] declares the Leios parameters -governance-tunable; cardano-ledger [#5965][cl-5965] maps them onto the -Dijkstra `PParams` and adds one bound the table lacks. The skeleton adds -nine fields, with the mechanical `PParamsUpdate` and group companions; every field -sits in the network and security groups, the assignment [#5965][cl-5965] gives all -of its proposed parameters. +CIP-164's [Table 3][cip-params] declares the Leios parameters governance-tunable; +cardano-ledger [#5965][cl-5965] maps them onto the Dijkstra `PParams` and adds one +bound the table lacks. + +The LLF adds nine fields, with the mechanical `PParamsUpdate` and group +companions; every field sits in the network and security groups, the assignment +[#5965][cl-5965] gives all of its proposed parameters. | Field | CIP-164 (Table 3) | Type | Notes | | ----------------------------- | ----------------------------------------- | ------------ | ----- | @@ -255,54 +293,60 @@ of its proposed parameters. | `leiosMaxRefScriptSizePerEB` | (not in the table) | ℕ (bytes) | from [#5965][cl-5965]; the per-EB analog of `maxRefScriptSizePerBlock` | Table 3's remaining row, the ranking-block max size `S_RB`, is the existing -`maxBlockSize`; there is no new field ([#5965][cl-5965] maps it to -`ppMaxBBSize`). Well-formedness: `τ < σ_c` is normative ("Must satisfy -`τ < σ_c`", [Table 3][cip-params]) and joins positivity of the periods and -sizes in the parameter well-formedness predicate. The constraint makes a quorum -arithmetically reachable by a fully keyed committee (truncation guarantees committee -stake of at least `σ_c` of the total, and `τ < σ_c` puts the threshold strictly -inside that coverage); keyless seats can still leave the signable stake short of `τ`, -as the committee section records. +`maxBlockSize`; there is no new field ([#5965][cl-5965] maps it to `ppMaxBBSize`). + +Well-formedness: `τ < σ_c` is normative ("Must satisfy `τ < σ_c`", +[Table 3][cip-params]) and joins positivity of the periods and sizes in the +parameter well-formedness predicate. The constraint makes a quorum arithmetically +reachable by a fully keyed committee (truncation guarantees committee stake of at +least `σ_c` of the total, and `τ < σ_c` puts the threshold strictly inside that +coverage); keyless seats can still leave the signable stake short of `τ`, as the +committee section records. + Types follow the spec's house conventions; [#5965][cl-5965]'s `SlotInterval`, `Word32`, and `OrdExUnits` are the Haskell counterparts, and name or type divergences get recorded in module prose. The network characteristics of the -CIP's Tables 1 and 2 (the Δ quantities) are not protocol parameters and do -not enter the spec. +CIP's Tables 1 and 2 (the Δ quantities) are not protocol parameters and do not +enter the spec. ## Availability -The rules take the closure as input and never ask whether data is available. The -block, as the spec sees it, is the resolved block: alongside the certificate it -carries the certified EB and the closure ("the ledger must be provided with all +The rules take the closure as input and never ask whether data is available. +The block, as the spec sees it, is the resolved block: alongside the certificate +it carries the certified EB and the closure ("the ledger must be provided with all endorsed transactions resolved", [REQ-LedgerResolvedBlockValidation][dd-blockval]), -and a matching premise checks the closure against the EB's references pointwise, hash -and declared size; the CIP documents the reference hash as covering the complete -transaction bytes ([Appendix B][cip-cddl]), so the references pin the closure's full -content, not only the transaction bodies. Availability is a consensus and storage -concern; CIP-164 keeps EBs out of chain validity altogether ("EBs are treated as -auxiliary data that do not affect chain validity or selection decisions", -[Chain Selection][cip-chainsel]), and a certificate whose closure has not yet -arrived is a block consensus cannot yet hand to the ledger, not a new failure mode. - -One boundary in this section deserves an explicit warning. The EB identifier is the -hash of the reference structure itself, which the skeleton abstracts as `hashEBRefs` -without pinning the byte-exact preimage. Cardano has been here before (the -block-body hash's segmented preimage exists only in implementation internals), so -pinning that preimage is a named conformance prerequisite, not an afterthought. +and a matching premise checks the closure against the EB's references pointwise, +hash and declared size; the CIP documents the reference hash as covering the +complete transaction bytes ([Appendix B][cip-cddl]), so the references pin the +closure's full content, not only the transaction bodies. + +Availability is a consensus and storage concern; CIP-164 keeps EBs out of chain +validity altogether ("EBs are treated as auxiliary data that do not affect chain +validity or selection decisions", [Chain Selection][cip-chainsel]), and a +certificate whose closure has not yet arrived is a block that consensus cannot yet +hand to the ledger, not a new failure mode. + +One boundary in this section deserves an explicit warning. The EB identifier is +the hash of the reference structure itself, which the LLF abstracts as +`hashEBRefs` without pinning the byte-exact preimage. Cardano has been here +before (the block-body hash's segmented preimage exists only in implementation +internals), so pinning that preimage is a named conformance prerequisite, not an +afterthought. + Two wire artifacts deliberately stay out of the rules: the header's `certified_eb` bit is a syncing optimization, derived in the spec from the presence of the body's -certificate; and a wrong `announced_eb_size` -makes nothing invalid: "neither the RB header nor the RB are invalid. But no -honest node should vote for the EB" ([Inclusion Rules][cip-inclusion]). Thus, -announcement-size agreement belongs to the voters' checks, not to block validity. +certificate; a wrong `announced_eb_size` makes nothing invalid: "neither the RB +header nor the RB are invalid. But no honest node should vote for the EB" +([Inclusion Rules][cip-inclusion]). Thus, announcement-size agreement belongs to +the voters' checks, not to block validity. ## The consensus↔ledger interface The interface proposed by Nicolas Frisby in the implementation design discussion -shapes the consensus↔ledger boundary as eight functions. The table maps each to its -skeleton counterpart, or records what stays outside the skeleton and why. +shapes the consensus↔ledger boundary as eight functions. The table maps each to +its LLF counterpart, or records what stays outside the LLF and why. -| Proposed function | Skeleton counterpart | +| Proposed function | LLF counterpart | | ----------------------------- | -------------------- | | `applyCertifiedEb` | The certificate branch of the block and chain rules: `ValidCert` plus the closure applied via `LEDGERS` from the announcing state, per the ordering above. | | `validateCertificate` | `ValidCert` (`Leios.Validity`): signers are seats of the pinned committee, the aggregate signature verifies over (slot, EB hash), and the signers' stake meets τ times the total active stake. The contextual half — agreement with the pending announcement, the timing window — sits as block/chain premises. | @@ -314,24 +358,32 @@ skeleton counterpart, or records what stays outside the skeleton and why. | `forgetVotingLedgerState` | Follow-up. The projection back to the ledger state, with the evident round-trip law against initialization. | The protocol-level Agda specification is shaped for the same division: its -base-layer interface submits ranking blocks carrying `txsOrEbCert : List Tx ⊎ EBCert` -and declares a single base-layer judgment, the certificate check `V-chkCerts`, the -role `ValidCert` is intended to fill. (An intended correspondence: that -specification declares the hook but its transition rules do not yet call it.) The -node-local vote conditions (header arrival, equivocation, deadlines, chain position: -CIP [vote conditions 1–4][cip-step3]) stay on its side of the line, and `ValidEB` -carries the ledger-checkable remainder (conditions 5 and 6). +base-layer interface submits ranking blocks carrying +`txsOrEbCert : List Tx ⊎ EBCert` and declares a single base-layer judgment, +the certificate check `V-chkCerts`, the role `ValidCert` is intended to fill. +(An intended correspondence: that specification declares the hook but its +transition rules do not yet call it.) + +The node-local vote conditions (header arrival, equivocation, deadlines, chain +position: CIP [vote conditions 1–4][cip-step3]) stay on its side of the line, and +`ValidEB` carries the ledger-checkable remainder (conditions 5 and 6). ## Out of scope: rewards and incentives -The skeleton models no change to the reward calculation, and neither does the +The LLF plan models no change to the reward calculation, and neither does the protocol: "Leios does not require any changes to incentives in Cardano" ([Incentives][cip-incentives]); the CIP cites the existing ledger-specification -rewards module as "the current and unchanged specification of rewards". Blocks-made -accounting is likewise untouched (a certificate-bearing block counts like any -other). Should a Leios incentive mechanism ever become normative (rewards for -voting or EB production, tiered fees), it enters through the full roadmap, not this -skeleton. +rewards module as "the current and unchanged specification of rewards". +Blocks-made accounting is likewise untouched (a certificate-bearing block counts +like any other). Should a Leios incentive mechanism ever become normative +(rewards for voting or EB production, tiered fees), it enters through the full +roadmap, not this LLF. + +--- + +[^1]: Promoting the aggregate-signature abstraction into `Ledger.Core` + (`CryptoStructure`), where Peras could share it, could be done as follow-up + work. [CIP-164]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md [cip-step3]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#step-3-committee-validation From 519a68a01ac510ce2a2d1b3302c8f2b2b14dd05a Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 24 Aug 2026 21:14:22 -0600 Subject: [PATCH 07/12] Add file-path header comment to the design note --- docs/leios/design-note.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index d33e142cd8..39898fce85 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -1,3 +1,5 @@ + + # Leios ledger formalization (LLF) plan This note records the defaults behind the formalization of the Ouroboros Linear From bc4586f3db014b5045ab2b78087fde7e2d714eca Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 24 Aug 2026 21:14:51 -0600 Subject: [PATCH 08/12] Design note: clarity pass Define the LLF once (the formalization, in Agda, of the CIP-164 ledger rules) and use it consistently; repair the sentences a reader flagged as imprecise, chiefly the vote-condition split at the consensus-ledger boundary, which now names both sides instead of pointing at 'its side of the line'; spell out why the crypto record cannot thread through AbstractFunctions; fix the LFF typo, a comma splice in the parameter prose, and the double-colon sentence about wire artifacts; make list punctuation and the module-map lead-in uniform. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 106 ++++++++++++++++++++------------------ 1 file changed, 55 insertions(+), 51 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index 39898fce85..b591330f33 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -2,19 +2,18 @@ # Leios ledger formalization (LLF) plan -This note records the defaults behind the formalization of the Ouroboros Linear -Leios ledger rules ([CIP-164]) in the Dijkstra-era specification, so that our -Agda work merely encodes these decisions instead of debating them. -Each subsection states one default, cites the source that fixes it, and gives the -rationale; where every source is silent, the note picks a default and says so. - -We will refer to the plan that this note describes as the -**Leios Ledger Formalization** plan, or **LLF** for short. - -Comments from the consensus and ledger implementers are welcome on all of it; the -LLF plan proceeds on these defaults and folds corrections in as they arrive. - -In protocol of [CIP-164], a block producer may announce an *endorser block* (EB), an +The **Leios Ledger Formalization** (**LLF**) is the formalization, in Agda, of the +ledger rules of Ouroboros Linear Leios ([CIP-164]) within the Dijkstra-era +specification. This note is the LLF plan: it records the design decisions our Agda +work builds on, so that the code encodes settled decisions instead of debating open +questions. Each subsection states one decision, cites the source that fixes it, and +gives the rationale; where every source is silent, the note picks a default and says +so. + +Comments from the consensus and ledger implementers are welcome on all of it; work +proceeds on these decisions, and corrections are folded in as they arrive. + +In the protocol of [CIP-164], a block producer may announce an *endorser block* (EB), an ordered list of transaction references (hash and declared byte size), alongside its ordinary *ranking block* (RB). A committee of stake pools votes on the announced EB, a quorum of votes is aggregated into a *certificate*, and the immediately following @@ -24,9 +23,9 @@ resolved and taken in reference order. The note draws on the following sources: -+ [CIP-164] (the normative text), ++ [CIP-164] (the normative text); + the implementation team's [Leios design document][design-doc] with its requirement - register (`REQ-…`), + register (`REQ-…`); + the cardano-ledger prototype ([#5626][cl-5626]: announcement, certificate bit, and voting-key carriage in the Dijkstra era) and its parameter proposal ([#5965][cl-5965]); @@ -50,12 +49,14 @@ The abstract voting crypto is a `LeiosAbstract` record, included as a new field `GovStructure`, the era's bundle of abstract structures, and supplied through `TransactionStructure`. This placement is forced by the import order: the proof-of-possession premise lives in `POOL`, inside `Certs`, which sees only -`GovStructure` and sits upstream of `AbstractFunctions`. +`GovStructure` and sits upstream of `AbstractFunctions`, so nothing threaded +through `AbstractFunctions` is in scope where the registration rule states that +premise. -A `GovStructure` field reaches `Certs` and every rule module downstream of the -transaction telescope without changing any module signature.[^1] +A `GovStructure` field, by contrast, reaches `Certs` and every rule module +downstream of the transaction telescope without changing any module signature.[^1] -**Placement of new modules and which existing modules to touch**. +The new modules, and the edits to existing modules, are as follows: ```text src/Ledger/Dijkstra/Specification/ @@ -75,9 +76,8 @@ src/Ledger/Dijkstra/Specification/ ## Certified application uses the full rules -In this LLF plan, we will apply a certified EB's closure with the ordinary -iterated `LEDGER` relation (`LEDGERS`), exactly as `BBODY` applies a block's own -transactions. +The LLF applies a certified EB's closure with the ordinary iterated `LEDGER` +relation (`LEDGERS`), exactly as `BBODY` applies a block's own transactions. [CIP-164] fixes what a vote attests: @@ -95,12 +95,11 @@ with minimal checks and UTxO updates", "omitting previously performed phase 1 & validation" ([CIP-164 Table 2][cip-params]; [REQ-LedgerTxNoValidation and REQ-LedgerCheapReapply][dd-txlevels]). -This LLF plan treats that as an optimization, not the semantics: the relation -defines certified application by the full rules, and the theorem that minimal -reapplication agrees with the full rules on a closure some quorum has validated is -exactly the soundness result the optimization needs. This would be a follow-up -proof, but not part of the initial LLF plan, so we will not include a separate -reapply relation. +The LLF treats that as an optimization, not the semantics: the relation defines +certified application by the full rules, and the theorem that minimal reapplication +agrees with the full rules on a closure some quorum has validated is exactly the +soundness result the optimization needs. That theorem is follow-up work, outside +the initial LLF, so the rules include no separate reapply relation. Phase-2 failures need no special accounting. Spec-level transactions carry their `isValid` flag, so `LEDGERS` covers collateral-forfeiting transactions in a closure @@ -157,12 +156,13 @@ which the CIP is silent: everything about an announced EB is evaluated in the announcing world. The closure runs under `A`'s parameters; the certificate is checked against the committee, the total active stake, and the quorum threshold `τ` pinned at announcement; the timing window uses the period lengths in force at -A. A certificate proves what the voters checked, and the voters could check only +`A`. A certificate proves what the voters checked, and the voters could check only `A`'s world; validating it against data none of them could have seen would break that reading. The vote signature is bound to `s_A` for the same reason: the binding "ensures voters validated the EB against the same ledger state it extends when certified on chain" ([Vote Structure][cip-vote]). -*This corollary is assumed in order to fix this LLF plan, but it should be confirm with the implementers.* +*The LLF assumes this corollary as a working default, pending confirmation from +the implementers.* This ordering also answers the following open question of the design document: "How much of the work lives in `BBODY` itself versus a dedicated EB-body rule, and @@ -175,15 +175,15 @@ chain-level context and application ordered before the tick, as above. ## Certificate failure is the absence of a transition CIP-164's [Certificate Validation][cip-certval] lists five checks that must pass -"before accepting the block." The LFF plan renders failure the way the spec +"before accepting the block." The LLF renders failure the way the spec renders every block fault: a block whose certificate fails a check, or that pairs a certificate with transactions of its own, or that certifies before the window opens, simply admits no `BBODY`/`CHAIN` derivation. The block is invalid, and nothing in the relational spec distinguishes why. A predicate-failure taxonomy belongs to the `Computational` instances and the -conformance work, deferred with the rest of executability, and the five checks are -its raw material if/when it arrives as follow-up work. +conformance work, deferred with the rest of executability; the five checks are the +raw material for that follow-up work. The missing-certificate case needs no bookkeeping at all: only the immediate successor may certify, and otherwise "the EB certificate cannot be included and @@ -218,7 +218,8 @@ The LLF adds the following defaults, each grounded in the design document: The implementation materializes the committee in the ledger state at the boundary rather than recomputing it per use ([REQ-LedgerStateVotingCommittee][dd-certver]); the LLF's rules consume the - committee only through the announcement pin, and materializing it as an + committee only through the announcement pin (see **The pin** below), and + materializing it as an epoch-state field is follow-up work together with the concrete construction, which is why no epoch module appears among the touched modules in the [Module placement](#module-placement) section above. @@ -227,7 +228,7 @@ The LLF adds the following defaults, each grounded in the design document: votes (`voter_id`) and certificate bitfields address. The CIP names no tie-break; the design document breaks ties by pool id, and the - LLF plan adopts that as a stated law, not a remark: equal-stake pools are + LLF adopts it as a stated law, not a remark: equal-stake pools are common at the committee tail, and two implementations that order ties differently disagree about the validity of every certificate. @@ -235,8 +236,8 @@ The LLF adds the following defaults, each grounded in the design document: by stake truncation at coverage `σ_c`, independent of key registration; descending stake with ties broken by ascending pool id; determinism of the order); the concrete construction can land later without disturbing anything - downstream of the laws, but the order itself cannot. The byte-exact comparison - on pool ids is a conformance detail to confirm upstream. + downstream of the laws; the order itself, being a law, cannot be deferred. The + byte-exact comparison on pool ids is a conformance detail to confirm upstream. + **Keyless seats**. Membership is by stake alone, "independent of key registration" ([REQ-KeylessSeat][dd-committee]): a selected pool without a @@ -279,8 +280,8 @@ cardano-ledger [#5965][cl-5965] maps them onto the Dijkstra `PParams` and adds o bound the table lacks. The LLF adds nine fields, with the mechanical `PParamsUpdate` and group -companions; every field sits in the network and security groups, the assignment -[#5965][cl-5965] gives all of its proposed parameters. +companions; every field sits in the network and security groups, matching the +assignment [#5965][cl-5965] gives its proposed parameters. | Field | CIP-164 (Table 3) | Type | Notes | | ----------------------------- | ----------------------------------------- | ------------ | ----- | @@ -318,7 +319,7 @@ The block, as the spec sees it, is the resolved block: alongside the certificate it carries the certified EB and the closure ("the ledger must be provided with all endorsed transactions resolved", [REQ-LedgerResolvedBlockValidation][dd-blockval]), and a matching premise checks the closure against the EB's references pointwise, -hash and declared size; the CIP documents the reference hash as covering the +hash and declared size. The CIP documents the reference hash as covering the complete transaction bytes ([Appendix B][cip-cddl]), so the references pin the closure's full content, not only the transaction bodies. @@ -335,18 +336,18 @@ before (the block-body hash's segmented preimage exists only in implementation internals), so pinning that preimage is a named conformance prerequisite, not an afterthought. -Two wire artifacts deliberately stay out of the rules: the header's `certified_eb` +Two wire artifacts deliberately stay out of the rules. The header's `certified_eb` bit is a syncing optimization, derived in the spec from the presence of the body's -certificate; a wrong `announced_eb_size` makes nothing invalid: "neither the RB +certificate. A wrong `announced_eb_size` makes nothing invalid: "neither the RB header nor the RB are invalid. But no honest node should vote for the EB" -([Inclusion Rules][cip-inclusion]). Thus, announcement-size agreement belongs to -the voters' checks, not to block validity. +([Inclusion Rules][cip-inclusion]); announcement-size agreement therefore belongs +to the voters' checks, not to block validity. ## The consensus↔ledger interface The interface proposed by Nicolas Frisby in the implementation design discussion -shapes the consensus↔ledger boundary as eight functions. The table maps each to -its LLF counterpart, or records what stays outside the LLF and why. +shapes the consensus↔ledger boundary as eight functions. The following table maps +each to its LLF counterpart, or records what stays outside the LLF and why. | Proposed function | LLF counterpart | | ----------------------------- | -------------------- | @@ -366,20 +367,23 @@ the certificate check `V-chkCerts`, the role `ValidCert` is intended to fill. (An intended correspondence: that specification declares the hook but its transition rules do not yet call it.) -The node-local vote conditions (header arrival, equivocation, deadlines, chain -position: CIP [vote conditions 1–4][cip-step3]) stay on its side of the line, and -`ValidEB` carries the ledger-checkable remainder (conditions 5 and 6). +CIP-164's six vote-casting conditions split across the same boundary: conditions 1–4 +(header arrival, equivocation detection, validation deadlines, chain position) are +node-local, so they stay with the protocol-level specification and never enter the +ledger rules; conditions 5 (the closure is a valid extension) and 6 (the EB is +nonempty) are ledger-checkable and land in `ValidEB`, together with the +reference/closure agreement and the per-EB bounds ([vote conditions][cip-step3]). ## Out of scope: rewards and incentives -The LLF plan models no change to the reward calculation, and neither does the +The LLF models no change to the reward calculation, and neither does the protocol: "Leios does not require any changes to incentives in Cardano" ([Incentives][cip-incentives]); the CIP cites the existing ledger-specification rewards module as "the current and unchanged specification of rewards". Blocks-made accounting is likewise untouched (a certificate-bearing block counts like any other). Should a Leios incentive mechanism ever become normative (rewards for voting or EB production, tiered fees), it enters through the full -roadmap, not this LLF. +roadmap, not the LLF. --- From 76de59a80ae833c846f24c9fd3a31c6b07c1fbb9 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 24 Aug 2026 22:33:28 -0600 Subject: [PATCH 09/12] Design note: address upstream review round 1 Two corrections from the Copilot review of PR #1297. The module map now states that the derived layers (Computational instances, Properties proofs, the Foreign mirror) track the rule edits mechanically in the same PRs, with the full-closure typecheck as the unchanged gate; the six-module sentence no longer reads as the complete touched-file set. The certifiability paragraph replaces unpublished trace-verifier figures with the Musashi certification outage that ouroboros-leios issue 1046 documents (73% participating weight against a 75% quorum for almost seven hours), which supports the same point with reproducible numbers, and makes the registration-versus-participation distinction explicit. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index b591330f33..b81f8cd7ec 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -36,8 +36,8 @@ The note draws on the following sources: ## Module placement Leios lands in the Dijkstra era as an additive subtree -`Ledger.Dijkstra.Specification.Leios.*` plus minimal edits to six existing modules; -no separate era, and no change to `Ledger.Core`. +`Ledger.Dijkstra.Specification.Leios.*` plus edits to six existing modules and +their derived layers; no separate era, and no change to `Ledger.Core`. [CIP-164] requires a new ledger era for the block-format change ([Versioning][cip-versioning]), and the implementation prototypes Leios in @@ -74,6 +74,15 @@ src/Ledger/Dijkstra/Specification/ └── Chain.lagda.md -- edit: pending-announcement threading, window check ``` +The map lists the modules where design decisions land. The era's derived layers +construct and pattern-match the very records and premises these edits change — the +`Computational` instances (`Computational.lagda.md` and the per-rule +`*/Properties/Computational.lagda.md`), the `Properties` proofs, and the `Foreign` +mirror — so each rule change updates them mechanically in the same PR, as the +type-checker directs; the voting-crypto interface work already does this for +`Foreign`. The gate is unchanged either way: the full `Ledger.Dijkstra` import +closure type-checks before a PR is done. + ## Certified application uses the full rules The LLF applies a certified EB's closure with the ordinary iterated `LEDGER` @@ -251,10 +260,15 @@ The LLF adds the following defaults, each grounded in the design document: `τ` of the total active stake), so the condition implementers must monitor has a name. - The gap is not hypothetical: on the Musashi testnet (2026-08, trace-verifier - observations) 19 of 66 registered pools had no voting key and certificates - appeared on roughly 3% of blocks, with every individual rule satisfied - (cf. [ouroboros-leios #1046][ol-1046]). + The gap is not hypothetical. During the Musashi certification outage of + 2026-08-12/13 ([ouroboros-leios #1046][ol-1046]), the committee's participating + weight sat at 73% against a 75% quorum threshold for almost seven hours and only + two EBs certified, while Praos block production continued and every individual + rule was satisfied; the margin was consumed by deliberately withheld keys, + silent nodes, and a retired pool whose snapshot stake sat in the committee as + structurally un-voteable weight. Registration-side metrics showed full key + adoption throughout: on-chain registration and node-side participation are + different quantities, and `certifiable` names only the part the ledger can see. + **Keys**. Pool registration carries the voting key with its proof of possession, as in the prototype's `sppLeiosKey` on `StakePoolParams` From 992b4ee9e09cdc69f5b528df485cb9fe777f66e9 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 25 Aug 2026 17:28:46 -0600 Subject: [PATCH 10/12] Design note: three-module layout, seat definition, review addendum Incorporate the module-count concessions from the 2026-08-25 design discussion with Carlos and Andre: the umbrella re-export module is dropped and the committee definitions fold into Leios.Validity, leaving three new modules; the map and the interface table follow. Define 'seat' at first use (a position in the committee's canonical order, which votes and certificate bitfields address by index). Append an addendum answering the two review questions: why a Vote type exists (certificate meaning, the implementation's validateVote and REQ-LedgerSerializationVote, metatheory vocabulary) with the severable fallback and its owner made explicit, and why shared Leios definitions get their own subtree rather than folding into the rule modules. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 128 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 122 insertions(+), 6 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index b81f8cd7ec..d486e60093 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -29,6 +29,9 @@ The note draws on the following sources: + the cardano-ledger prototype ([#5626][cl-5626]: announcement, certificate bit, and voting-key carriage in the Dijkstra era) and its parameter proposal ([#5965][cl-5965]); ++ the consensus↔ledger interface proposal circulated by Nicolas Frisby in the + implementation team's design discussion (2026-08; quoted here because it is + not yet recorded in any public artifact); + the protocol-level Agda specification [ouroboros-leios-formal-spec][leios-formal-spec], for which the ledger is the base layer. @@ -60,12 +63,11 @@ The new modules, and the edits to existing modules, are as follows: ```text src/Ledger/Dijkstra/Specification/ -├── Leios.lagda.md -- umbrella: overview prose, re-exports ├── Leios/ │ ├── Abstract.lagda.md -- LeiosAbstract: abstract voting crypto │ ├── Types.lagda.md -- EndorserBlock, Announcement, Vote, Certificate -│ ├── Committee.lagda.md -- Seat, Committee, quorum arithmetic -│ └── Validity.lagda.md -- ValidVote, ValidCert, ValidEB +│ └── Validity.lagda.md -- Seat, Committee, quorum arithmetic; +│ -- ValidVote, ValidCert, ValidEB ├── Gov/Base.lagda.md -- edit: leiosAbstract field in GovStructure ├── Transaction.lagda.md -- edit: supply leiosAbstract via TransactionStructure ├── PParams.lagda.md -- edit: the Leios parameter block @@ -233,8 +235,10 @@ The LLF adds the following defaults, each grounded in the design document: which is why no epoch module appears among the touched modules in the [Module placement](#module-placement) section above. -+ **Order and indices**. The descending-stake order fixes the seat indices that - votes (`voter_id`) and certificate bitfields address. ++ **Order and indices**. A *seat* is a position in the committee's canonical + order, carrying its pool, its weight, and (optionally) its voting key. The + descending-stake order fixes the seat indices that votes (`voter_id`) and + certificate bitfields address. The CIP names no tie-break; the design document breaks ties by pool id, and the LLF adopts it as a stated law, not a remark: equal-stake pools are @@ -368,7 +372,7 @@ each to its LLF counterpart, or records what stays outside the LLF and why. | `applyCertifiedEb` | The certificate branch of the block and chain rules: `ValidCert` plus the closure applied via `LEDGERS` from the announcing state, per the ordering above. | | `validateCertificate` | `ValidCert` (`Leios.Validity`): signers are seats of the pinned committee, the aggregate signature verifies over (slot, EB hash), and the signers' stake meets τ times the total active stake. The contextual half — agreement with the pending announcement, the timing window — sits as block/chain premises. | | `validateVote` | `ValidVote` (`Leios.Validity`): the voter index denotes a keyed committee seat whose key verifies the signature over (slot, EB hash). Votes never appear on-chain individually; this is the meaning consensus uses to filter votes before aggregation. | -| `doesEpochCommitteeIncludeMe` | Decidable membership on `Committee` (`Leios.Committee`), a seat lookup by pool. The "me" binding is consensus-local; the ledger side is the seat lookup, which the implementation serves from its materialized committee ([REQ-LedgerStateVotingCommittee][dd-certver]). | +| `doesEpochCommitteeIncludeMe` | Decidable membership on `Committee` (`Leios.Validity`), a seat lookup by pool. The "me" binding is consensus-local; the ledger side is the seat lookup, which the implementation serves from its materialized committee ([REQ-LedgerStateVotingCommittee][dd-certver]). | | `initializeVotingLedgerState` | Follow-up (the voting-state interface). Meaning fixed now: the announcing block's post-`BBODY` state paired with fresh EB accumulators, one per cumulative `ValidEB` bound: referenced-transaction bytes, `ExUnits`, and reference-script bytes. | | `applyTxForVoting` | Follow-up. Meaning fixed now: one LEDGER step plus accumulator updates and bound checks; folding it over the closure from the initialized state succeeds exactly when `ValidEB`'s extension-and-bounds conjuncts hold. | | `reapplyTxForVoting` | Follow-up. The minimal-checks variant; its agreement with `applyTxForVoting` on previously validated transactions is the certified-application soundness theorem. | @@ -399,6 +403,117 @@ like any other). Should a Leios incentive mechanism ever become normative (rewards for voting or EB production, tiered fees), it enters through the full roadmap, not the LLF. +## Addendum: two design questions raised in review + +### Why a `Vote` type at all? + +No ledger transition rule consumes a `Vote`. Votes never reach the chain, and +CIP-164 draws the line accordingly: certificate validation is block validity, +while the vote-casting conditions are node behavior. If "consumed by a rule" +were the only criterion for a type's existence, `Vote` would fail it. + +But rules are not a specification's only consumers, and creation is no +criterion at all: the ledger creates neither votes nor certificates, yet +nobody disputes `Certificate`. Three consumers need the vote's fields. + +1. **The certificate's meaning**. A certificate is a compressed set of + votes: `cSig` is an aggregate signature over precisely the message each + vote signs, `(slot, EB-hash)`, under the keys of the seats named in the + bitfield (a bitfield index is a `voter_id` in another encoding). The + CIP's reason for signing the slot is a replay-protection argument about + votes ("binding the vote signature to `slot_no` … ensures voters validated + the EB against the same ledger state it extends"). Without a `Vote` type, + the aggregate check verifies an unexplained pair of bytes; with one, the + certificate is a definition instead of an incantation. The price is one + four-field record. + +2. **The implementation's own requirements**. The consensus↔ledger + interface proposed by Nicolas Frisby in the implementation team's design + discussion (2026-08; not yet recorded in a public artifact; the interface + section above gives it durable form) includes `validateVote`, with its + stated reason: "To receive/relay votes, we also need to validate them. + They're never in a block, but we get at least the epoch's committee + member's public key from the ledger state." And the design document's + requirement register includes + [`REQ-LedgerSerializationVote`][dd-serialization] ("The vote structure + must be deterministically de-/serializable from/to bytes using CBOR + encoding"): the ledger owns the vote wire format, alongside RB and EB. A + ledger spec without a vote type can give neither requirement a formal + counterpart. + +3. **Vocabulary for the metatheory**. Quorum safety, the statement that a + valid certificate implies some honest committee member attested `ValidEB`, + is the justification for certified application skipping re-validation, and + it is a statement about votes: honest voters vote only for valid EBs; a + quorum of stake signed; hence an honest vote exists. The proof is + deferred; the statement needs votes as objects. + +The design isolates the question by construction: `ValidCert` never mentions +`Vote`, so dropping `Vote` and `ValidVote` costs exactly one record and one +relation, and nothing else moves. The fallback is correspondingly principled: +the `validateVote` interface row becomes "consensus-side composition of +ledger-provided pieces, namely committee seat lookup plus `isSignedVote`, +which `LeiosAbstract` exports regardless". + +The fallback has an owner, though, and it is not this note. Whether the +ledger owns vote validation and serialization is fixed, today, in the +implementation team's own artifacts: `validateVote` in the proposed interface +and `REQ-LedgerSerializationVote` in the design document. If the answer is to +become "no", those artifacts must change first; a ledger spec that silently +drops `Vote` while they stand manufactures a spec–implementation divergence. + +**Recommendation**. Keep `Vote`/`ValidVote` as definitions serving the +interface and the metatheory, consumed by no rule; this is the framing the +note already uses for the protocol spec's declared-but-uncalled `V-chkCerts`. + +### Why a Leios subtree instead of folding into existing modules? + +One concession first, because it clarifies the question: the rule edits land +in `BlockBody`, `Chain`, `Certs`, and `PParams` regardless; premises live +where rules live. The question is only where the shared type definitions go. +One placement is already settled by constraint, not taste: the abstract crypto +cannot live in `AbstractFunctions`, because `Certs` sits upstream of it and +the proof-of-possession premise would be unstatable there. + +For the rest, every Leios type has more than one consumer, as follows: + ++ `Certificate`: `BlockBody`'s field and `ValidCert`; ++ `EndorserBlock`: `BlockBody`'s payload and `ValidEB`; ++ `Announcement`: `BlockBody`'s header and `Chain`'s `PendingEB`; ++ the committee: `Chain`'s pin and both validity relations. + +Shared definitions need one home upstream of their consumers, and the lowest +existing candidate is `BlockBody`. "Fold into existing modules" therefore +means "put essentially everything in `BlockBody.lagda.md`", which makes +`BlockBody` the Leios module in all but name: same content, worse label, and +entangled with a rule module that `master` actively churns. Hence the +practical arguments: + ++ **Merge economics**. `leios-main` lives by routine merges from `master`, + and the fold targets are `master`'s most active files: `Certs` and + `PParams` churn with parameter work, and the preservation-of-value stack is + touching the `*/Properties` families now. New files never conflict; edits + to shared files can. The subtree is the shape that keeps a long-lived + parallel branch's merges cheap. ++ **Ripple economics**. The derived layers (`Computational`, `Properties`, + `Foreign`) mirror the records and premises of the modules they shadow, so + adding fields to shared records breaks them immediately, while standalone + type modules defer that cost until a rule consumes the types. Both data + points exist on this branch: the `GovStructure` field needed only a + `Foreign` stub, while the `StakePoolParams` field, a fold-style edit, is + the one with real `Foreign` fallout. ++ **Reversibility asymmetry**. Inlining later is trivial: move each + definition into its consumer and delete the module. Extracting later means + editing the shared modules again, a second pass through the conflict + surface. Under residual doubt, the cheap-to-reverse choice is + separate-first. ++ **Precedent**. The consensus implementation keeps Leios in Leios-named + modules (`LeiosVoting.hs`, `Shelley/Ledger/Leios.hs`); the protocol-level + Agda spec has its own namespace; and this specification already organizes + by concern (`Gov/`, `Certs/`, `Utxo/`). A concern-scoped subtree is the + house style. The protocol has also pivoted once (Full → Linear); if it + moves again, a subtree contains the blast radius. + --- [^1]: Promoting the aggregate-signature abstraction into `Ledger.Core` @@ -425,6 +540,7 @@ roadmap, not the LLF. [dd-committee]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#committee-selection [dd-certver]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#certificate-verification [dd-blockval]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#block-validation +[dd-serialization]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#serialization [cl-5626]: https://github.com/IntersectMBO/cardano-ledger/pull/5626 [cl-5965]: https://github.com/IntersectMBO/cardano-ledger/issues/5965 [leios-formal-spec]: https://github.com/input-output-hk/ouroboros-leios-formal-spec From 004735fe33415b787a256036f426c881267fded3 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Fri, 28 Aug 2026 14:45:11 -0600 Subject: [PATCH 11/12] Design note: align with CIP-164 as amended by CIPs PR 1250 The revision in review moves the goalposts the note was written against, so every affected decision is restated on the new text: + The three periods are wall-clock durations (seconds in Table 3, carried as Milliseconds); slot granularity enters only at the certification window, now written with the CIP's ceiling division. + The committee is sized directly by committeeSize (N_c); the CIP itself now pins the tie-break and the fewer-than-N_c case, so selection becomes concrete (sort-free seat-index construction) with the former laws downgraded to provable lemmas. + tau's constraint is 0.5 < tau < sigma(N_c): the lower bound stays parameter-local and imposed; the upper bound lives in the stake distribution, so parameter well-formedness no longer claims any reachability, which strengthens the certifiable predicate's role. + The Leios parameters leave the positivity predicate: zero values are the rollout's off state and governance must be able to reach it. + Votes bind the announcing RB header hash, not (slot, EB hash); the Vote addendum and the interface rows are restated accordingly. + Key registration (bls_key in pool registration, mandatory proof of possession) is now CIP-normative; the dedicated-certificate-with- expiry alternative under discussion is recorded, with the CIP text as the LLF default until it lands. + All cip-* links resolve on the amended revision's branch, moving back to master when the PR merges; the sources list says so. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 229 +++++++++++++++++++++++--------------- 1 file changed, 137 insertions(+), 92 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index d486e60093..0d57f26fdc 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -23,7 +23,10 @@ resolved and taken in reference order. The note draws on the following sources: -+ [CIP-164] (the normative text); ++ [CIP-164] (the normative text), as amended by + [cardano-foundation/CIPs #1250][cip-1250], the revision this note quotes: the + `cip-…` links resolve on that revision's branch and move back to `master` when + it merges; + the implementation team's [Leios design document][design-doc] with its requirement register (`REQ-…`); + the cardano-ledger prototype ([#5626][cl-5626]: announcement, certificate bit, @@ -126,8 +129,9 @@ proposes adding them) and does not touch the relational rules. For a block `B` at slot `s_B` carrying a certificate for the EB announced by its predecessor `A` at slot `s_A` (admissible only when -`s_B ≥ s_A + 3·L_hdr + L_vote + L_diff`; [Step 5][cip-step5]), the rules fix the -following total order: +`s_B ≥ s_A + ⌈(3·L_hdr + L_vote + L_diff) / slotLength⌉` — the periods being +wall-clock durations, rounded up to whole slots exactly here; [Step 5][cip-step5]), +the rules fix the following total order: 1. **EB application**. The closure applies via `LEDGERS` to the ledger state left by `A`'s block-body transition, in `A`'s environment: slot `s_A` and the @@ -148,9 +152,10 @@ following total order: transactions are allowed in the RB" ([Step 5][cip-step5]); so its body contributes the certificate premises and the usual bookkeeping. -(The implementation already diverges from the lower bound -`s_B ≥ s_A + 3·L_hdr + L_vote + L_diff`. The prototype's `minCertificationGap` is -10 slots whereas `3·L_hdr + L_vote + L_diff` gives 14 with the Musashi parameters. +(The implementation already diverges from the lower bound. The prototype's +`minCertificationGap` is 10 slots whereas the formula gives 14 with the Musashi +parameters, whose slot and wall-clock readings coincide at a one-second +`slotLength`. Both sides are live and measured by the trace-verifier work; the divergence is flagged upstream, like the proof-of-possession divergence in the committee section.) @@ -169,9 +174,10 @@ checked against the committee, the total active stake, and the quorum threshold `τ` pinned at announcement; the timing window uses the period lengths in force at `A`. A certificate proves what the voters checked, and the voters could check only `A`'s world; validating it against data none of them could have seen would break -that reading. The vote signature is bound to `s_A` for the same reason: the -binding "ensures voters validated the EB against the same ledger state it extends -when certified on chain" ([Vote Structure][cip-vote]). +that reading. The vote signature is bound to the hash of `A`'s header for the +same reason: the binding "ensures voters validated the EB against the same ledger +state it extends when certified on chain", and it also disambiguates among +multiple headers announcing the same EB ([Vote Structure][cip-vote]). *The LLF assumes this corollary as a working default, pending confirmation from the implementers.* @@ -212,12 +218,16 @@ invalid block. ## The committee -[CIP-164] fixes the committee once per epoch by stake-based truncation: "pools are -ordered by stake in descending order and selected, in order, until the cumulative -selected stake reaches" the coverage target `σ_c`, and the resulting committee -"is fixed for the entire epoch", with no per-EB sortition and no non-persistent -voters ([Committee Structure][cip-committee]; the boundary procedure in [Epoch -Boundary][cip-epoch]). +[CIP-164] fixes the committee once per epoch by stake-based truncation: the "top +`N_c` pools by active stake", where `N_c` is the `committeeSize` protocol +parameter, "ordered by active stake in descending order (ties broken by pool ID +in ascending order)", all of them if fewer than `N_c` are registered; the +resulting committee "is fixed for the entire epoch", with no per-EB sortition and +no non-persistent voters ([Committee Structure][cip-committee]; the boundary +procedure in [Epoch Boundary][cip-epoch]). Earlier revisions sized the committee +by a cumulative-stake coverage target `σ_c`; [#1250][cip-1250] replaced it with +the seat count, whose coverage `σ(N_c)` is read off the stake distribution rather +than declared. The LLF adds the following defaults, each grounded in the design document: @@ -229,10 +239,9 @@ The LLF adds the following defaults, each grounded in the design document: The implementation materializes the committee in the ledger state at the boundary rather than recomputing it per use ([REQ-LedgerStateVotingCommittee][dd-certver]); the LLF's rules consume the - committee only through the announcement pin (see **The pin** below), and - materializing it as an - epoch-state field is follow-up work together with the concrete construction, - which is why no epoch module appears among the touched modules in the [Module + committee only through the announcement pin (see **The pin** below). Whether + the LLF also stores the committee in the epoch state is a representation + choice; if it does, the epoch module joins the touched modules of the [Module placement](#module-placement) section above. + **Order and indices**. A *seat* is a position in the committee's canonical @@ -240,28 +249,35 @@ The LLF adds the following defaults, each grounded in the design document: descending-stake order fixes the seat indices that votes (`voter_id`) and certificate bitfields address. - The CIP names no tie-break; the design document breaks ties by pool id, and the - LLF adopts it as a stated law, not a remark: equal-stake pools are - common at the committee tail, and two implementations that order ties - differently disagree about the validity of every certificate. - - Selection enters the LLF abstractly, as a function with stated laws (membership - by stake truncation at coverage `σ_c`, independent of key registration; - descending stake with ties broken by ascending pool id; determinism of the - order); the concrete construction can land later without disturbing anything - downstream of the laws; the order itself, being a law, cannot be deferred. The - byte-exact comparison on pool ids is a conformance detail to confirm upstream. + The CIP now pins the tie-break itself, byte-wise ascending on the pool's key + hash, together with the fewer-than-`N_c` case ([Epoch Boundary][cip-epoch]); + the design document had the same order, and the LLF still states it as a law, + not a remark: equal-stake pools are common at the committee tail, and two + implementations that order ties differently disagree about the validity of + every certificate. + + Selection entered the LLF plan abstractly, as a function with stated laws, + when the CIP fixed only the coverage target and left the rest underdetermined. + [#1250][cip-1250] specifies the whole procedure, and a sort-free construction + exists (a pool's seat index is the number of pools strictly ahead of it in the + committee order), so the LLF takes selection concretely; the former laws + (membership by top-`N_c` truncation independent of key registration, + descending stake with the pinned tie-break, determinism) become provable + lemmas rather than assumptions. + **Keyless seats**. Membership is by stake alone, "independent of key - registration" ([REQ-KeylessSeat][dd-committee]): a selected pool without a + registration" ([REQ-KeylessSeat][dd-committee]), a requirement [#1250][cip-1250] + adopts into the CIP: a selected pool without a registered voting key still occupies its seat and holds its weight, but the - seat cannot sign, and a certificate whose bitfield sets a keyless seat is - invalid ([REQ-LedgerCertificateVerification][dd-certver]). Keyless stake can + seat "cannot sign, and any certificate marking a keyless seat as a signer must + be rejected" ([Key Registration and Rotation][cip-keyreg]; + [REQ-LedgerCertificateVerification][dd-certver]). Keyless stake can therefore lower the quorum a certificate is able to reach, never inflate it. - Parameter well-formedness therefore does not imply certifiability: the LLF + No parameter constraint implies certifiability (with the committee sized by + seats, even the coverage `σ(N_c)` is emergent), so the LLF names the gap with a `certifiable` predicate (keyed committee stake at least - `τ` of the total active stake), so the condition implementers must monitor has + `τ` of the total active stake), and the condition implementers must monitor has a name. The gap is not hypothetical. During the Musashi certification outage of @@ -274,16 +290,24 @@ The LLF adds the following defaults, each grounded in the design document: adoption throughout: on-chain registration and node-side participation are different quantities, and `certifiable` names only the part the ledger can see. -+ **Keys**. Pool registration carries the voting key with its proof of - possession, as in the prototype's `sppLeiosKey` on `StakePoolParams` - ([#5626][cl-5626]; `spsLeiosKey` is its pool-state mirror), and *registration* - checks the proof ([REQ-CheckProofOfPossession][dd-committee]); however, the - prototype stores the key *without checking the proof*, which is a divergence to - flag upstream. - - Rotation is re-registration, activated at an epoch boundary - ([REQ-RotateBLSKeys][dd-keys]); CIP-164 leaves the real rotation mechanism - "to a follow-up PR amending this CIP" ([Design Decisions][cip-design]). ++ **Keys**. [#1250][cip-1250] makes registration normative: the pool + registration certificate carries an optional `bls_key`, the public key with its + proof of possession, and the proof "is mandatory and verified at registration", + against rogue-key attacks on BLS aggregation ([Key Registration and + Rotation][cip-keyreg]; [REQ-CheckProofOfPossession][dd-committee]). The + prototype's `sppLeiosKey` on `StakePoolParams` ([#5626][cl-5626]; + `spsLeiosKey` is its pool-state mirror) stores the key *without checking the + proof*, a divergence to flag with the implementers. + + Rotation is re-registration ([REQ-RotateBLSKeys][dd-keys]), on a cadence + comparable to KES rotation, with activation at an epoch boundary aligned to + VRF-key rotation ([Key Registration and Rotation][cip-keyreg]). A competing + design is in active discussion: a dedicated registration certificate with a + ledger-enforced key expiry, its TTL a genesis constant + ([cardano-scaling/CIPs #38][cs-38]; [ouroboros-leios #1024][ol-1024]), moving + the key from the registration parameters into its own certificate and + pool-state field. The LLF's default follows the CIP text and switches if the + amendment lands. + **The pin**. A certificate is validated against the committee of the epoch in which the announcing RB was produced; the CIP sizes the signer bitfield by @@ -294,41 +318,57 @@ The LLF adds the following defaults, each grounded in the design document: ## Protocol parameters CIP-164's [Table 3][cip-params] declares the Leios parameters governance-tunable; -cardano-ledger [#5965][cl-5965] maps them onto the Dijkstra `PParams` and adds one -bound the table lacks. +cardano-ledger [#5965][cl-5965] maps an earlier revision of the table onto the +Dijkstra `PParams`. The LLF adds nine fields, with the mechanical `PParamsUpdate` and group companions; every field sits in the network and security groups, matching the assignment [#5965][cl-5965] gives its proposed parameters. -| Field | CIP-164 (Table 3) | Type | Notes | -| ----------------------------- | ----------------------------------------- | ------------ | ----- | -| `leiosHeaderDiffusionPeriod` | `L_hdr`, header diffusion period | ℕ (slots) | | -| `leiosVotingPeriod` | `L_vote`, voting period | ℕ (slots) | | -| `leiosDiffusionPeriod` | `L_diff`, diffusion period | ℕ (slots) | [#5965][cl-5965] renames it the *additional* diffusion period | -| `leiosMaxEBSize` | `S_EB`, endorser block max size | ℕ (bytes) | bounds the reference structure itself, which [#5965][cl-5965] calls the EB *header* | -| `leiosMaxEBTxsSize` | `S_EB-tx`, referenceable transaction size | ℕ (bytes) | bounds the closure's total bytes, [#5965][cl-5965]'s EB *body* | -| `leiosCommitteeStakeCoverage` | `σ_c`, committee stake coverage | UnitInterval | | -| `leiosQuorumStakeThreshold` | `τ`, quorum stake threshold | UnitInterval | normative constraint `τ < σ_c` | -| `leiosMaxEBExUnits` | max Plutus steps and memory per EB | ExUnits | Table 3's two budget rows in one field, after [#5965][cl-5965]'s `OrdExUnits` | -| `leiosMaxRefScriptSizePerEB` | (not in the table) | ℕ (bytes) | from [#5965][cl-5965]; the per-EB analog of `maxRefScriptSizePerBlock` | +| Field | CIP-164 (Table 3) | Type | Notes | +| ---------------------------- | ------------------------------------------ | ------------ | ----- | +| `leiosHeaderPeriod` | `L_hdr`, header diffusion period length | Milliseconds | | +| `leiosVotingPeriod` | `L_vote`, voting period length | Milliseconds | | +| `leiosDiffusionPeriod` | `L_diff`, diffusion period length | Milliseconds | [#5965][cl-5965] names it the *additional* diffusion period | +| `leiosMaxEBSize` | `S_EB`, endorser block max size | ℕ (bytes) | bounds the reference structure itself, which [#5965][cl-5965] calls the EB *header* | +| `leiosMaxEBTxsSize` | `S_EB-tx`, referenceable transaction size | ℕ (bytes) | bounds the closure's total bytes, [#5965][cl-5965]'s EB *body* | +| `leiosCommitteeSize` | `N_c`, committee size | ℕ (seats) | replaced the stake-coverage target `σ_c` of earlier revisions ([#1250][cip-1250]) | +| `leiosQuorumStakeThreshold` | `τ`, quorum stake threshold | UnitInterval | normative constraint `0.5 < τ < σ(N_c)` | +| `leiosMaxEBExUnits` | max Plutus steps and memory per EB | ExUnits | Table 3's two budget rows in one field, after [#5965][cl-5965]'s `OrdExUnits` | +| `leiosMaxRefScriptSizePerEB` | `S_EB-ref`, reference script size per EB | ℕ (bytes) | entered as [#5965][cl-5965]'s own addition; a Table 3 row since [#1250][cip-1250] | Table 3's remaining row, the ranking-block max size `S_RB`, is the existing `maxBlockSize`; there is no new field ([#5965][cl-5965] maps it to `ppMaxBBSize`). -Well-formedness: `τ < σ_c` is normative ("Must satisfy `τ < σ_c`", -[Table 3][cip-params]) and joins positivity of the periods and sizes in the -parameter well-formedness predicate. The constraint makes a quorum arithmetically -reachable by a fully keyed committee (truncation guarantees committee stake of at -least `σ_c` of the total, and `τ < σ_c` puts the threshold strictly inside that -coverage); keyless seats can still leave the signable stake short of `τ`, as the -committee section records. +The three periods are wall-clock durations, stated in Table 3 in seconds the way +the genesis `slotLength` is, so that Leios timing does not silently retune when +`slotLength` changes ([Timing parameters][cip-params]). The LLF carries them as +`Milliseconds`, the fixed-precision form of those fractional seconds. Slot +granularity enters the timing rules in exactly one place, the certification +window's `⌈(3·L_hdr + L_vote + L_diff) / slotLength⌉`, rounded up so a +certificate cannot land before the durations have elapsed ([Step 5][cip-step5]); +the voters' own deadlines are node-local timers and never convert +([Step 3][cip-step3]). + +Well-formedness: the Leios parameters stay outside the positivity predicate, +because zero values are the protocol's off state and governance must be able to +reach it: a zero voting window admits no votes and hence no certificates. Of the +CIP's quorum constraint `0.5 < τ < σ(N_c)`, only the lower bound is a property of +the parameters; the upper bound compares `τ` against the committee's emergent +coverage, which lives in the stake distribution, so it cannot sit in a parameter +predicate ([choosing the quorum threshold][cip-quorum]). The LLF imposes +`0.5 < τ` in the parameter well-formedness predicate (the disabled state never +needs `τ ≡ 0`) and leaves `τ < σ(N_c)` to the CIP's operational guidance for +choosing `N_c`. The earlier revisions' `τ < σ_c`, which made a quorum +arithmetically reachable by a fully keyed committee, has no seat-count +counterpart at the parameter level; reachability is exactly what the committee +section's `certifiable` predicate names. Types follow the spec's house conventions; [#5965][cl-5965]'s `SlotInterval`, -`Word32`, and `OrdExUnits` are the Haskell counterparts, and name or type -divergences get recorded in module prose. The network characteristics of the -CIP's Tables 1 and 2 (the Δ quantities) are not protocol parameters and do not -enter the spec. +`Word32`, and `OrdExUnits` lenses track the earlier table revision, and name or +type divergences get recorded in module prose. The network characteristics of +the CIP's Tables 1 and 2 (the Δ quantities) are not protocol parameters and do +not enter the spec. ## Availability @@ -370,8 +410,8 @@ each to its LLF counterpart, or records what stays outside the LLF and why. | Proposed function | LLF counterpart | | ----------------------------- | -------------------- | | `applyCertifiedEb` | The certificate branch of the block and chain rules: `ValidCert` plus the closure applied via `LEDGERS` from the announcing state, per the ordering above. | -| `validateCertificate` | `ValidCert` (`Leios.Validity`): signers are seats of the pinned committee, the aggregate signature verifies over (slot, EB hash), and the signers' stake meets τ times the total active stake. The contextual half — agreement with the pending announcement, the timing window — sits as block/chain premises. | -| `validateVote` | `ValidVote` (`Leios.Validity`): the voter index denotes a keyed committee seat whose key verifies the signature over (slot, EB hash). Votes never appear on-chain individually; this is the meaning consensus uses to filter votes before aggregation. | +| `validateCertificate` | `ValidCert` (`Leios.Validity`): signers are keyed seats of the pinned committee, the aggregate signature verifies over the announcing header's hash, and the signers' stake meets τ times the total active stake. The contextual half — agreement with the pending announcement, the timing window — sits as block/chain premises. | +| `validateVote` | `ValidVote` (`Leios.Validity`): the voter index denotes a keyed committee seat whose key verifies the signature over the announcing header's hash. Votes never appear on-chain individually; this is the meaning consensus uses to filter votes before aggregation. | | `doesEpochCommitteeIncludeMe` | Decidable membership on `Committee` (`Leios.Validity`), a seat lookup by pool. The "me" binding is consensus-local; the ledger side is the seat lookup, which the implementation serves from its materialized committee ([REQ-LedgerStateVotingCommittee][dd-certver]). | | `initializeVotingLedgerState` | Follow-up (the voting-state interface). Meaning fixed now: the announcing block's post-`BBODY` state paired with fresh EB accumulators, one per cumulative `ValidEB` bound: referenced-transaction bytes, `ExUnits`, and reference-script bytes. | | `applyTxForVoting` | Follow-up. Meaning fixed now: one LEDGER step plus accumulator updates and bound checks; folding it over the closure from the initialized state succeeds exactly when `ValidEB`'s extension-and-bounds conjuncts hold. | @@ -418,14 +458,14 @@ nobody disputes `Certificate`. Three consumers need the vote's fields. 1. **The certificate's meaning**. A certificate is a compressed set of votes: `cSig` is an aggregate signature over precisely the message each - vote signs, `(slot, EB-hash)`, under the keys of the seats named in the - bitfield (a bitfield index is a `voter_id` in another encoding). The - CIP's reason for signing the slot is a replay-protection argument about - votes ("binding the vote signature to `slot_no` … ensures voters validated + vote signs, the hash of the announcing RB's header, under the keys of the + seats named in the bitfield (a bitfield index is a `voter_id` in another + encoding). The CIP's reason for the message choice is an argument about + votes ("binding the vote to `announcing_rb_hash` ensures voters validated the EB against the same ledger state it extends"). Without a `Vote` type, - the aggregate check verifies an unexplained pair of bytes; with one, the + the aggregate check verifies an unexplained hash; with one, the certificate is a definition instead of an incantation. The price is one - four-field record. + three-field record. 2. **The implementation's own requirements**. The consensus↔ledger interface proposed by Nicolas Frisby in the implementation team's design @@ -520,20 +560,25 @@ practical arguments: (`CryptoStructure`), where Peras could share it, could be done as follow-up work. -[CIP-164]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md -[cip-step3]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#step-3-committee-validation -[cip-step5]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#step-5-chain-inclusion -[cip-params]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#protocol-parameters -[cip-ledger]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#ledger-management -[cip-chainsel]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#chain-selection -[cip-epoch]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#epoch-boundary -[cip-certval]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#certificate-validation -[cip-committee]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#committee-structure -[cip-vote]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#vote-structure -[cip-inclusion]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#rb-inclusion-rules -[cip-cddl]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#appendix-b-cddl -[cip-design]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#design-decisions -[cip-versioning]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#versioning +[CIP-164]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md +[cip-step3]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#step-3-committee-validation +[cip-step5]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#step-5-chain-inclusion +[cip-params]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#protocol-parameters +[cip-ledger]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#ledger-management +[cip-chainsel]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#chain-selection +[cip-epoch]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#epoch-boundary +[cip-certval]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#certificate-validation +[cip-committee]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#committee-structure +[cip-vote]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#vote-structure +[cip-inclusion]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#rb-inclusion-rules +[cip-cddl]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#appendix-b-cddl +[cip-design]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#design-decisions +[cip-versioning]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#versioning +[cip-keyreg]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#key-registration +[cip-quorum]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#choosing-quorum-threshold +[cip-1250]: https://github.com/cardano-foundation/CIPs/pull/1250 +[cs-38]: https://github.com/cardano-scaling/CIPs/pull/38 +[ol-1024]: https://github.com/input-output-hk/ouroboros-leios/issues/1024 [design-doc]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md [dd-txlevels]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#transaction-validation-levels [dd-keys]: https://github.com/input-output-hk/ouroboros-leios/blob/main/docs/leios-design/README.md#key-registration-and-rotation @@ -545,4 +590,4 @@ practical arguments: [cl-5965]: https://github.com/IntersectMBO/cardano-ledger/issues/5965 [leios-formal-spec]: https://github.com/input-output-hk/ouroboros-leios-formal-spec [ol-1046]: https://github.com/input-output-hk/ouroboros-leios/issues/1046 -[cip-incentives]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md#incentives +[cip-incentives]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#incentives From 6d3d19f1bdb2be9f5d2d6d83a87406305c5c2b75 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 31 Aug 2026 21:16:18 -0600 Subject: [PATCH 12/12] Design note: record the crypto-placement and vote-type resolutions Settled with Sebastian Nagel, 2026-08-31. The BLS voting primitives live in the core CryptoStructure rather than a Dijkstra-local LeiosAbstract record threaded through GovStructure: the structure is ambient in every rule module, so the proof-of-possession premise stays statable with no signature changes, the governance-named home and its confusion go away, and Peras sharing needs no later migration (the Peras footnote is absorbed into the placement paragraph). Vote and ValidVote stay as rule-free definitions; a transition rule would have no transition to gate. The module map now shows the as-built shape: the core crypto edit, the Leios committee/validity module, Leios/Types for the primitive types, and the epoch-boundary materialization, with the key-registration mechanism deferred to the committee section's Keys bullet. The subtree addendum gains an as-built postscript. AI-assisted development: Claude Fable 5 (Anthropic) --- docs/leios/design-note.md | 70 +++++++++++++++++++++------------------ 1 file changed, 38 insertions(+), 32 deletions(-) diff --git a/docs/leios/design-note.md b/docs/leios/design-note.md index 0d57f26fdc..a02ea1da2d 100644 --- a/docs/leios/design-note.md +++ b/docs/leios/design-note.md @@ -41,9 +41,10 @@ The note draws on the following sources: ## Module placement -Leios lands in the Dijkstra era as an additive subtree -`Ledger.Dijkstra.Specification.Leios.*` plus edits to six existing modules and -their derived layers; no separate era, and no change to `Ledger.Core`. +Leios lands in the Dijkstra era as additive Leios modules plus edits to +existing modules and their derived layers; no separate era. The one +`Ledger.Core` change is deliberate: the BLS voting primitives join the core +`CryptoStructure`, where Peras can share them. [CIP-164] requires a new ledger era for the block-format change ([Versioning][cip-versioning]), and the implementation prototypes Leios in @@ -51,30 +52,31 @@ Dijkstra ([#5626][cl-5626] targets `eras/dijkstra`), so the Dijkstra specificati is where the rules belong; keeping the new material in its own subtree keeps merges from `master` cheap. -The abstract voting crypto is a `LeiosAbstract` record, included as a new field of -`GovStructure`, the era's bundle of abstract structures, and supplied through -`TransactionStructure`. This placement is forced by the import order: the -proof-of-possession premise lives in `POOL`, inside `Certs`, which sees only -`GovStructure` and sits upstream of `AbstractFunctions`, so nothing threaded -through `AbstractFunctions` is in scope where the registration rule states that -premise. - -A `GovStructure` field, by contrast, reaches `Certs` and every rule module -downstream of the transaction telescope without changing any module signature.[^1] +The abstract voting crypto lives in `Ledger.Core.Specification.Crypto`: the +`CryptoStructure` gains the BLS carriers and verification predicates (keys, +signatures, proofs of possession, aggregate verification over the +serialization type) and a strict total order on key hashes, the committee +tie-break. `CryptoStructure` is ambient in every rule module, `Certs` +included, so the proof-of-possession premise is statable with no module +signature changing, and the core placement lets Peras share the +aggregate-signature abstraction instead of migrating it later. (Settled +2026-08-31 with Sebastian Nagel; an earlier draft threaded a Dijkstra-local +`LeiosAbstract` record through `GovStructure`, which also reached `Certs` but +overloaded a governance-named structure with voting crypto.) The new modules, and the edits to existing modules, are as follows: ```text +src/Ledger/Core/Specification/ +└── Crypto.lagda.md -- edit: BLS primitives; key-hash order (the tie-break) src/Ledger/Dijkstra/Specification/ -├── Leios/ -│ ├── Abstract.lagda.md -- LeiosAbstract: abstract voting crypto -│ ├── Types.lagda.md -- EndorserBlock, Announcement, Vote, Certificate -│ └── Validity.lagda.md -- Seat, Committee, quorum arithmetic; -│ -- ValidVote, ValidCert, ValidEB -├── Gov/Base.lagda.md -- edit: leiosAbstract field in GovStructure -├── Transaction.lagda.md -- edit: supply leiosAbstract via TransactionStructure +├── Leios.lagda.md -- seats, committee selection, quorum arithmetic; +│ -- certificate, vote, and EB validity +├── Leios/Types.lagda.md -- EndorserBlock, Announcement, Vote ├── PParams.lagda.md -- edit: the Leios parameter block -├── Certs.lagda.md -- edit: voting key in StakePoolParams +├── Certs.lagda.md -- edit: voting-key registration (mechanism per the +│ -- Keys bullet of the committee section) +├── Epoch.lagda.md -- edit: the committee materialized at the boundary ├── BlockBody.lagda.md -- edit: announcement/certificate fields, BBODY premises └── Chain.lagda.md -- edit: pending-announcement threading, window check ``` @@ -410,9 +412,9 @@ each to its LLF counterpart, or records what stays outside the LLF and why. | Proposed function | LLF counterpart | | ----------------------------- | -------------------- | | `applyCertifiedEb` | The certificate branch of the block and chain rules: `ValidCert` plus the closure applied via `LEDGERS` from the announcing state, per the ordering above. | -| `validateCertificate` | `ValidCert` (`Leios.Validity`): signers are keyed seats of the pinned committee, the aggregate signature verifies over the announcing header's hash, and the signers' stake meets τ times the total active stake. The contextual half — agreement with the pending announcement, the timing window — sits as block/chain premises. | -| `validateVote` | `ValidVote` (`Leios.Validity`): the voter index denotes a keyed committee seat whose key verifies the signature over the announcing header's hash. Votes never appear on-chain individually; this is the meaning consensus uses to filter votes before aggregation. | -| `doesEpochCommitteeIncludeMe` | Decidable membership on `Committee` (`Leios.Validity`), a seat lookup by pool. The "me" binding is consensus-local; the ledger side is the seat lookup, which the implementation serves from its materialized committee ([REQ-LedgerStateVotingCommittee][dd-certver]). | +| `validateCertificate` | `ValidCert` (`Leios`): signers are keyed seats of the pinned committee, the aggregate signature verifies over the announcing header's hash, and the signers' stake meets τ times the total active stake. The contextual half — agreement with the pending announcement, the timing window — sits as block/chain premises. | +| `validateVote` | `ValidVote` (`Leios`): the voter index denotes a keyed committee seat whose key verifies the signature over the announcing header's hash. Votes never appear on-chain individually; this is the meaning consensus uses to filter votes before aggregation. | +| `doesEpochCommitteeIncludeMe` | Decidable membership on `Committee` (`Leios`), a seat lookup by pool. The "me" binding is consensus-local; the ledger side is the seat lookup, which the implementation serves from its materialized committee ([REQ-LedgerStateVotingCommittee][dd-certver]). | | `initializeVotingLedgerState` | Follow-up (the voting-state interface). Meaning fixed now: the announcing block's post-`BBODY` state paired with fresh EB accumulators, one per cumulative `ValidEB` bound: referenced-transaction bytes, `ExUnits`, and reference-script bytes. | | `applyTxForVoting` | Follow-up. Meaning fixed now: one LEDGER step plus accumulator updates and bound checks; folding it over the closure from the initialized state succeeds exactly when `ValidEB`'s extension-and-bounds conjuncts hold. | | `reapplyTxForVoting` | Follow-up. The minimal-checks variant; its agreement with `applyTxForVoting` on previously validated transactions is the certified-application soundness theorem. | @@ -493,7 +495,7 @@ The design isolates the question by construction: `ValidCert` never mentions relation, and nothing else moves. The fallback is correspondingly principled: the `validateVote` interface row becomes "consensus-side composition of ledger-provided pieces, namely committee seat lookup plus `isSignedVote`, -which `LeiosAbstract` exports regardless". +which the core crypto structure exports regardless". The fallback has an owner, though, and it is not this note. Whether the ledger owns vote validation and serialization is fixed, today, in the @@ -505,15 +507,18 @@ drops `Vote` while they stand manufactures a spec–implementation divergence. **Recommendation**. Keep `Vote`/`ValidVote` as definitions serving the interface and the metatheory, consumed by no rule; this is the framing the note already uses for the protocol spec's declared-but-uncalled `V-chkCerts`. +Settled 2026-08-31 with Sebastian Nagel: the definitions stay, and they stay +rule-free, since a transition rule would have no transition to gate; votes +never reach the chain. ### Why a Leios subtree instead of folding into existing modules? One concession first, because it clarifies the question: the rule edits land in `BlockBody`, `Chain`, `Certs`, and `PParams` regardless; premises live where rules live. The question is only where the shared type definitions go. -One placement is already settled by constraint, not taste: the abstract crypto -cannot live in `AbstractFunctions`, because `Certs` sits upstream of it and -the proof-of-possession premise would be unstatable there. +One placement is settled elsewhere: the abstract crypto lives in the core +`CryptoStructure` (see [Module placement](#module-placement)), which every +rule module already sees, so reachability constrains nothing here. For the rest, every Leios type has more than one consumer, as follows: @@ -554,11 +559,12 @@ practical arguments: house style. The protocol has also pivoted once (Full → Linear); if it moves again, a subtree contains the blast radius. ---- +*Postscript, 2026-08-31.* As built, the shape is two Leios-named modules +(`Leios` for the committee and the validity relations, `Leios/Types` for the +primitive types) with the crypto in the core structure: flatter than the +subtree argued for above, Leios-named as it argues, and inlined nowhere. -[^1]: Promoting the aggregate-signature abstraction into `Ledger.Core` - (`CryptoStructure`), where Peras could share it, could be done as follow-up - work. +--- [CIP-164]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md [cip-step3]: https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md#step-3-committee-validation