Leios¶
This module defines the ledger-side building blocks of Ouroboros Leios (CIP-0164): the stake-based voting committee and the certificate that attests a quorum of committee votes for an endorser block (EB).
Voting Committee¶
A committee seat holds a pool, its voting weight (the pool's fraction
of total active stake) and the pool's honoured voting key —
nothing makes a keyless seat, which
counts for committee membership but can never sign. The committee
maps each seat index (the voter_id of CIP-0164) to its seat.
record LeiosSeat : Type where field pool : KeyHash weight : UnitInterval key : Maybe BlsVKey LeiosCommittee : Type LeiosCommittee = List LeiosSeat
A registered voting key is honoured until maxKeyAge
epochs after its registration: the KES key lifetime rounded up to
whole epochs, plus two epochs of activation delay (a registered key
enters the mark snapshot at the next boundary and the committee at the
one after).
maxKeyAge : Epoch maxKeyAge = ℕtoEpoch ((MaxKESEvoᶜ * SlotsPerKESPeriodᶜ + SlotsPerEpochᶜ ∸ 1) / SlotsPerEpochᶜ + 2)
Expiry is judged against the epoch the committee is selected for, not the epoch its stake snapshot was taken in: the seat's key comes from a snapshot and may therefore have been registered several epochs ago.
honouredBlsKey : Epoch → Maybe (BlsVKey × Epoch) → Maybe BlsVKey honouredBlsKey e nothing = nothing honouredBlsKey e (just (k , e')) = if e < e' + maxKeyAge then just k else nothing
The committee for an epoch consists of the leiosCommitteeSize
pools with the most active stake, ties broken by ascending pool keyhash.
_≼_ : LeiosSeat → LeiosSeat → Type ls₁ ≼ ls₂ = c₂ <ᵘⁱ c₁ ⊎ (c₁ ≡ c₂ × ls₁ .pool ≤ᵏʰ ls₂ .pool) where c₁ = ls₁ .weight c₂ = ls₂ .weight
selectCommittee : Epoch → (KeyHash ⇀ Coin) → Pools → LeiosCommittee selectCommittee e pd pools = take leiosCommitteeSize sortedLeiosSeats where totalStake : Coin totalStake = ∑[ c ← pd ] c leiosSeatMap : KeyHash ⇀ UnitInterval × Maybe BlsVKey leiosSeatMap = flip mapWithKey pools λ kh spp → let vkey = honouredBlsKey e (spp .bls) weight = if lookupᵐ? pd kh then (λ {c} → clamp (c /₀ totalStake)) else 0ᵘⁱ in weight , vkey allLeiosSeats : List LeiosSeat allLeiosSeats = map (λ (kh , (w , vk)) → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Leios.html#4965}{\htmlId{4984}{\htmlClass{Bound}{\text{kh}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Leios.html#4971}{\htmlId{4989}{\htmlClass{Bound}{\text{w}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Leios.html#4975}{\htmlId{4993}{\htmlClass{Bound}{\text{vk}}}}\, \end{pmatrix}$) (setToList (leiosSeatMap ˢ)) sortedLeiosSeats : List LeiosSeat sortedLeiosSeats = sort ≼-DTO allLeiosSeats
Certification Delay¶
CIP-0164 admits a certificate only when the certifying block is at least
⌈(3·L_hdr + L_vote + L_diff) / slotLength⌉ slots after the announcing block
(Step 5). certificationDelay computes that bound
from the protocol parameters: three header diffusion periods, the voting
period, and the additional diffusion period, summed in milliseconds and
converted to whole slots by slotsFromDuration through the genesis
slot length SlotLengthᶜ. The conversion rounds up, since
rounding down would admit a certificate before the durations the security
argument relies on have elapsed. The chain rule decides which block's
parameters the function is applied to.
certificationDelay : Slot certificationDelay = slotsFromDuration (3 * leiosHeaderPeriod + leiosVotingPeriod + leiosDiffusionPeriod)
Leios Certificates¶
An EB certificate (eb_certificate in CIP-0164's CDDL) stands in for a quorum
of votes on an EB announcement: the set of seat indices that signed (the CIP's
bitfield) and their aggregate BLS signature.
It is part of the body of the ranking block that certifies the EB.
record EBCert : Type where field signers : ℙ ℕ sig : BlsSig
A seat index is a position in the committee list. signersSeats
collects, in seat order, the seats whose index the certificate names, and the
weight a set of signers carries is the sum of those seats' weights, each the
pool's share of the total active stake.
signersSeats : LeiosCommittee → ℙ ℕ → List LeiosSeat signersSeats cmt signers = map proj₂ (filter (λ (i , _) → i ∈ signers) (L.zip (upTo (length cmt)) cmt))
A certificate is valid for a message, the hash of the announcing block's header,
when every signer names a seat and every such seat holds a key (a keyless seat
cannot sign), the aggregate signature verifies under those keys, and the
signers' summed weight meets the quorum threshold τ. Since each weight is a
share of the total active stake, the comparison is against the whole stake,
not merely the seated stake, as CIP-0164 requires.
record ValidEBCert (cmt : LeiosCommittee) (τ : UnitInterval) (msg : Ser) (cert : EBCert) : Type where seats = signersSeats cmt (cert .signers) field signersSeated : cert .signers ⊆ fromList (upTo (length cmt)) signersKeyed : Allˡ (λ s → Is-just (s .key)) seats validSignature : isSignedByAggregate (fromList (mapMaybe key seats)) msg (cert .sig) quorum : fromUnitInterval τ ℚ.≤ ∑ˡ[ s ← seats ] fromUnitInterval (s .weight)
Of the five checks of CIP-0164's Certificate Validation, the
first, that the certificate conforms to the CDDL, is the type
EBCert itself; the second is validSignature; the
third, that every signer is a committee member able to sign, is
signersSeated with signersKeyed; the fourth is
quorum; and the fifth, that the message is the hash of the
announcing header taken from the chain context, is supplied by the chain rule
that applies the certificate, through msg.