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).

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)

module Ledger.Dijkstra.Specification.Leios
  (gs : GovStructure) (open GovStructure gs) where

open import Ledger.Prelude
open import Ledger.Prelude.Numeric.UnitInterval using (UnitInterval; fromUnitInterval)
open import Ledger.Dijkstra.Specification.Certs gs

open import Agda.Builtin.FromNat
open import Data.List.Sort
open import Data.Nat.Properties
  using (<⇒≤; >⇒≢; ≤∧≢⇒<)
  renaming (≤-decTotalOrder to ℕ-≤-decTotalOrder)
open import Data.Rational as ℚ using (ℚ)
open import Data.Rational.Literals using (number)
open import Relation.Binary.Bundles using (DecTotalOrder)
open import Relation.Binary.PropositionalEquality using () renaming (sym to ≡-sym)
open import Function using (case_of_)

open Number number renaming (fromNat to fromℚℕ)
open StakePoolState

Voting Committee¶

A committee seat holds a pool, its voting weight (the pool's 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  : Coin
    key     : Maybe BlsVKey

LeiosCommittee : Type
LeiosCommittee = List LeiosSeat

open LeiosSeat

instance
  unquoteDecl HasCast-LeiosSeat = derive-HasCast
    [ (quote LeiosSeat , HasCast-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

private
  ≼-DTO : DecTotalOrder 0ℓ 0ℓ 0ℓ
  ≼-DTO = decTotalOrder (×-decTotalOrder ≥-decTotalOrder DTO-KeyHash)
                        (λ ls → ls .weight , ls .pool)
    where
      open import Relation.Binary.Construct.On using (decTotalOrder)
      open import Data.Product.Relation.Binary.Lex.NonStrict using (×-decTotalOrder)
      open import Relation.Binary.Properties.DecTotalOrder ℕ-≤-decTotalOrder

  open DecTotalOrder ≼-DTO renaming (_≤_ to _≤DTO_) using ()

  ≼-DTO⇒≼ : ∀ {x y} → x ≼ y → x ≤DTO y
  ≼-DTO⇒≼ (inj₁ p)          = inj₁ (<⇒≤ p , >⇒≢ p)
  ≼-DTO⇒≼ (inj₂ (refl , q)) = inj₂ (refl , q)

  ≼⇒≼-DTO : ∀ {x y} → x ≤DTO y → x ≼ y
  ≼⇒≼-DTO (inj₁ (p  , q))     = inj₁ (≤∧≢⇒< p (λ r → q (≡-sym r)))
  ≼⇒≼-DTO (inj₂ (refl , snd)) = inj₂ (refl , snd)

module _ (pp : PParams)
         (let open PParams pp using (leiosCommitteeSize)) where

  selectCommittee : Epoch → (KeyHash ⇀ Coin) → Pools → LeiosCommittee
  selectCommittee e pd pools = take leiosCommitteeSize sortedLeiosSeats
    where
      allLeiosSeats : List LeiosSeat
      allLeiosSeats = map (λ (kh , c) → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Leios.html#4123}{\htmlId{4135}{\htmlClass{Bound}{\text{kh}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Leios.html#4128}{\htmlId{4140}{\htmlClass{Bound}{\text{c}}}}\, \\ \,\htmlId{4144}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{4145}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Axiom.Set.Map.html#17169}{\htmlId{4148}{\htmlClass{Function}{\text{lookupᵐ?}}}}\, \,\href{Ledger.Dijkstra.Specification.Leios.html#3997}{\htmlId{4157}{\htmlClass{Bound}{\text{pools}}}}\, \,\href{Ledger.Dijkstra.Specification.Leios.html#4123}{\htmlId{4163}{\htmlClass{Bound}{\text{kh}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{4166}{\htmlClass{Function Operator}{\text{then}}}}\, \,\htmlId{4171}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{4174}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Leios.html#4175}{\htmlId{4175}{\htmlClass{Bound}{\text{spp}}}}\,\,\htmlId{4178}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{4180}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Leios.html#2496}{\htmlId{4182}{\htmlClass{Function}{\text{honouredBlsKey}}}}\, \,\href{Ledger.Dijkstra.Specification.Leios.html#3992}{\htmlId{4197}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{4199}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Leios.html#4175}{\htmlId{4200}{\htmlClass{Bound}{\text{spp}}}}\, \,\htmlId{4204}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#1306}{\htmlId{4205}{\htmlClass{Field}{\text{bls}}}}\,\,\htmlId{4208}{\htmlClass{Symbol}{\text{))}}}\, \,\href{Class.ToBool.html#342}{\htmlId{4211}{\htmlClass{Function Operator}{\text{else}}}}\, \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{4216}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\,\,\htmlId{4223}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$)
                          (setToList (pd ˢ))

      sortedLeiosSeats : List LeiosSeat
      sortedLeiosSeats = sort ≼-DTO allLeiosSeats