[Leios] LLF1-1: the design note (#1296) - #1297
Open
williamdemeo wants to merge 12 commits into
Open
Conversation
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)
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)
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)
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)
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)
williamdemeo
marked this pull request as ready for review
August 25, 2026 04:01
williamdemeo
added a commit
to williamdemeo/formal-ledger-specifications
that referenced
this pull request
Aug 25, 2026
The m1-2 review established that EB references must hash the complete transaction bytes (TxRefHash), not the body-identity TxId, which cannot pin witnesses; update the type sketches and the M1-3 issue accordingly, and correct the M1-2 issue's superseded AbstractFunctions threading bullet to the GovStructure design. Regions refreshed from the fork, recording issue #2 closed after its migration to IntersectMBO#1296 (delivered by IntersectMBO#1297). AI-assisted development: Claude Fable 5 (Anthropic)
Contributor
There was a problem hiding this comment.
Pull request overview
Adds the LLF design note defining how Leios integrates with the Dijkstra ledger specification.
Changes:
- Documents module placement, transition ordering, certificate semantics, committees, and parameters.
- Defines availability and consensus–ledger interface boundaries.
- Records implementation divergences and deferred work.
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Open
4 tasks
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)
williamdemeo
added a commit
to williamdemeo/formal-ledger-specifications
that referenced
this pull request
Aug 25, 2026
The upstream review of PR IntersectMBO#1297 established that the 19-of-66 and 3%-of-blocks figures are unpublished trace-verifier measurements that ouroboros-leios issue 1046 does not substantiate; the design note and the M2-1 worked example now cite the 2026-08-12/13 Musashi certification outage that issue documents instead. AI-assisted development: Claude Fable 5 (Anthropic)
williamdemeo
force-pushed
the
1296-llf-design-note
branch
from
August 26, 2026 14:07
5a42102 to
969d627
Compare
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)
williamdemeo
force-pushed
the
1296-llf-design-note
branch
from
August 26, 2026 14:32
969d627 to
992b4ee
Compare
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)
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)
14 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
This PR adds the design note,
docs/leios/design-note.md, the main [LLF1-1] deliverable.The design note records the design decisions the Leios Ledger Formalization (LLF) builds on, so later issues encode rather than debate.
There is one short subsection per decision, each with its CIP-164 citation and rationale; every quotation is verified against the CIP-164 source, the Leios design document, IntersectMBO/cardano-ledger#5626 and IntersectMBO/cardano-ledger#5965, and the protocol-level Agda spec.
The decisions, in brief:
Module placement. Additive
Leiossubtree ofLedger.Dijkstra.Specificationplus minimal edits to six existing modules; the abstract voting crypto is aLeiosAbstractfield ofGovStructure, supplied throughTransactionStructure(anAbstractFunctionsfield cannot reach the registration rule); noLedger.Corechange.Full rules. Certified application uses the ordinary
LEDGERSrelation; reapply is an implementation optimization to be justified by a follow-up soundness theorem.Environment and ordering.
A corollary pins committee, total stake, τ, and window lengths at announcement (a note-set default flagged for implementer confirmation).
Failure. An invalid, early, or transaction-accompanied certificate admits no
BBODY/CHAINderivation; the predicate-failure taxonomy is deferred toComputational/conformance work.Committee.
certifiablepredicate records the gap);Parameters. Nine new
PParamsfields (CIP-164 Table 3 plus the per-EB reference-script bound from Add Leios related protocol parameters cardano-ledger#5965), all in the network and security groups;S_RBis the existingmaxBlockSize;τ < σ_cin well-formedness.Availability. The rules take the resolved closure as input with a pointwise matching premise; no availability obligations. The byte-exact preimage of the EB-reference hash is deliberately unpinned and flagged as a conformance prerequisite.
Interface table. All eight proposed consensus↔ledger functions mapped: four to initial LLF definitions, four to the follow-up voting-state interface with their meanings fixed now.
Out of scope. Rewards and incentives, with the CIP's own words ("Leios does not require any changes to incentives in Cardano").
The note also folds in a field review grounded in the Musashi trace-verifier work: the pending-announcement lifetime (no announcement survives an intervening block), the
minCertificationGapdivergence (prototype 10 slots versus the formula's 14), and the certifiability gap observed live (19 of 66 pools keyless, certificates on roughly 3% of blocks).Developed in williamdemeo#15 through two Copilot review rounds and a field review; the full commit history is preserved on this branch.
Closes #1296.
🤖 AI-assisted development: Claude Fable 5 (Anthropic)
🧑 Human-curated/revised: @williamdemeo
Checklist
Any semantic changes to the specifications are documented inN/ACHANGELOG.mdCode is formatted according to CONTRIBUTING.mdN/A