{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Local sortition used by non-persistent members of the voting committee.
--
-- Implements the @LS@ component of the @wFA^LS@ scheme from the Fait-Accompli
-- Committee Selection paper: (https://eprint.iacr.org/2023/1273.pdf, §2.3).
-- See also:
--  https://github.com/input-output-hk/ouroboros-leios/blob/c5658913221a7f58063bc4f82efaec0900e53dab/post-cip/weighted-fait-accompli.pdf
module Ouroboros.Consensus.Committee.LS
  ( -- * Local sortition check
    LocalSortitionNumSeats (..)
  , localSortitionNumSeats
  ) where

import Cardano.Ledger.BaseTypes (FixedPoint, HasZero)
import Data.Maybe (fromMaybe)
import Data.Word (Word64)
import Ouroboros.Consensus.Committee.Crypto (NormalizedVRFOutput (..))
import Ouroboros.Consensus.Committee.Types (Cumulative (..), LedgerStake (..))
import Ouroboros.Consensus.Committee.WFA
  ( NonPersistentCommitteeSize (..)
  , TotalNonPersistentStake (..)
  )

-- * Local sortition check

-- | Number of non-persistent seats granted by local sortition to a voter
newtype LocalSortitionNumSeats = LocalSortitionNumSeats
  { LocalSortitionNumSeats -> Word64
unLocalSortitionNumSeats :: Word64
  }
  deriving stock (Int -> LocalSortitionNumSeats -> ShowS
[LocalSortitionNumSeats] -> ShowS
LocalSortitionNumSeats -> String
(Int -> LocalSortitionNumSeats -> ShowS)
-> (LocalSortitionNumSeats -> String)
-> ([LocalSortitionNumSeats] -> ShowS)
-> Show LocalSortitionNumSeats
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LocalSortitionNumSeats -> ShowS
showsPrec :: Int -> LocalSortitionNumSeats -> ShowS
$cshow :: LocalSortitionNumSeats -> String
show :: LocalSortitionNumSeats -> String
$cshowList :: [LocalSortitionNumSeats] -> ShowS
showList :: [LocalSortitionNumSeats] -> ShowS
Show, LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
(LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool)
-> (LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool)
-> Eq LocalSortitionNumSeats
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
== :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
$c/= :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
/= :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
Eq, Eq LocalSortitionNumSeats
Eq LocalSortitionNumSeats =>
(LocalSortitionNumSeats -> LocalSortitionNumSeats -> Ordering)
-> (LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool)
-> (LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool)
-> (LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool)
-> (LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool)
-> (LocalSortitionNumSeats
    -> LocalSortitionNumSeats -> LocalSortitionNumSeats)
-> (LocalSortitionNumSeats
    -> LocalSortitionNumSeats -> LocalSortitionNumSeats)
-> Ord LocalSortitionNumSeats
LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
LocalSortitionNumSeats -> LocalSortitionNumSeats -> Ordering
LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Ordering
compare :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Ordering
$c< :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
< :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
$c<= :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
<= :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
$c> :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
> :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
$c>= :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
>= :: LocalSortitionNumSeats -> LocalSortitionNumSeats -> Bool
$cmax :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
max :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
$cmin :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
min :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
Ord)
  deriving newtype (Integer -> LocalSortitionNumSeats
LocalSortitionNumSeats -> LocalSortitionNumSeats
LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
(LocalSortitionNumSeats
 -> LocalSortitionNumSeats -> LocalSortitionNumSeats)
-> (LocalSortitionNumSeats
    -> LocalSortitionNumSeats -> LocalSortitionNumSeats)
-> (LocalSortitionNumSeats
    -> LocalSortitionNumSeats -> LocalSortitionNumSeats)
-> (LocalSortitionNumSeats -> LocalSortitionNumSeats)
-> (LocalSortitionNumSeats -> LocalSortitionNumSeats)
-> (LocalSortitionNumSeats -> LocalSortitionNumSeats)
-> (Integer -> LocalSortitionNumSeats)
-> Num LocalSortitionNumSeats
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
+ :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
$c- :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
- :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
$c* :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
* :: LocalSortitionNumSeats
-> LocalSortitionNumSeats -> LocalSortitionNumSeats
$cnegate :: LocalSortitionNumSeats -> LocalSortitionNumSeats
negate :: LocalSortitionNumSeats -> LocalSortitionNumSeats
$cabs :: LocalSortitionNumSeats -> LocalSortitionNumSeats
abs :: LocalSortitionNumSeats -> LocalSortitionNumSeats
$csignum :: LocalSortitionNumSeats -> LocalSortitionNumSeats
signum :: LocalSortitionNumSeats -> LocalSortitionNumSeats
$cfromInteger :: Integer -> LocalSortitionNumSeats
fromInteger :: Integer -> LocalSortitionNumSeats
Num, LocalSortitionNumSeats -> Bool
(LocalSortitionNumSeats -> Bool) -> HasZero LocalSortitionNumSeats
forall a. (a -> Bool) -> HasZero a
$cisZero :: LocalSortitionNumSeats -> Bool
isZero :: LocalSortitionNumSeats -> Bool
HasZero)

-- | Compute how many non-persistent seats can be granted by local sortition to
-- a voter given their normalized VRF output and stake
localSortitionNumSeats ::
  -- | Expected number of non-persistent voters in the committee
  NonPersistentCommitteeSize ->
  -- | Total stake of non-persistent voters
  TotalNonPersistentStake ->
  -- | Stake of the voter
  LedgerStake ->
  -- | Normalized VRF output from the participant
  NormalizedVRFOutput ->
  LocalSortitionNumSeats
localSortitionNumSeats :: NonPersistentCommitteeSize
-> TotalNonPersistentStake
-> LedgerStake
-> NormalizedVRFOutput
-> LocalSortitionNumSeats
localSortitionNumSeats
  (NonPersistentCommitteeSize Word64
numNonPersistentVoters)
  (TotalNonPersistentStake (Cumulative (LedgerStake Rational
totalNonPersistentStake)))
  (LedgerStake Rational
voterStake)
  (NormalizedVRFOutput Rational
normalizedVRFOutput)
    -- None of the non-persistent voters have any stake => nobody gets a seat.
    -- NOTE: this check avoids the expensive computation below and also prevents
    -- division by zero when computing @orders@.
    | Rational
voterStake Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
0 = Word64 -> LocalSortitionNumSeats
LocalSortitionNumSeats Word64
0
    -- If the voter has stake close to zero, the conversion from 'Rational' to
    -- 'FixedPoint' for 'lambda' might underflow to zero, which would cause the
    -- "orders" computation below to divide by zero.
    | FixedPoint
lambda FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
<= FixedPoint
0 = Word64 -> LocalSortitionNumSeats
LocalSortitionNumSeats Word64
0
    -- This voter might be entitled to some seats => run the local sortition.
    | Bool
otherwise = Word64 -> LocalSortitionNumSeats
LocalSortitionNumSeats (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
expectedSeats)
   where
    -- Expected number of seats granted by local sortition
    lambda :: FixedPoint
    lambda :: FixedPoint
lambda =
      Rational -> FixedPoint
forall a. Fractional a => Rational -> a
fromRational (Rational -> FixedPoint) -> Rational -> FixedPoint
forall a b. (a -> b) -> a -> b
$
        Word64 -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
numNonPersistentVoters
          Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
voterStake
          Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
totalNonPersistentStake

    -- Compute the "orders" of the Poisson distribution with parameter lambda,
    -- which are used as thresholds to determine how many seats we get based on
    -- the normalized VRF output
    orders :: [FixedPoint]
    orders :: [FixedPoint]
orders =
      (Rational -> FixedPoint
forall a. Fractional a => Rational -> a
fromRational Rational
normalizedVRFOutput FixedPoint -> FixedPoint -> FixedPoint
forall a. Fractional a => a -> a -> a
/ FixedPoint
lambda)
        FixedPoint -> [FixedPoint] -> [FixedPoint]
forall a. a -> [a] -> [a]
: (FixedPoint -> FixedPoint -> FixedPoint)
-> [FixedPoint] -> [FixedPoint] -> [FixedPoint]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
          (\FixedPoint
k FixedPoint
prev -> FixedPoint
k FixedPoint -> FixedPoint -> FixedPoint
forall a. Num a => a -> a -> a
* FixedPoint
prev FixedPoint -> FixedPoint -> FixedPoint
forall a. Fractional a => a -> a -> a
/ FixedPoint
lambda)
          [FixedPoint
2 ..]
          [FixedPoint]
orders

    -- Estimate how many seats we get by comparing the normalized VRF output
    -- against the thresholds defined by the orders.
    --
    -- TODO(peras): evaluate whether the limit used below (3) makes sense in
    -- this context. One possible starting point would be to understand why
    -- @checkLeaderNatValue@ (in Ledger) also uses 3 as its own limit when
    -- computing slot leadership proofs.
    --
    -- Tracked by this issue:
    -- https://github.com/tweag/cardano-peras/issues/234
    expectedSeats :: Int
    expectedSeats :: Int
expectedSeats =
      Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$
        FixedPoint -> [FixedPoint] -> FixedPoint -> Maybe Int
forall a. RealFrac a => a -> [a] -> a -> Maybe Int
taylorExpCmpFirstNonLower
          FixedPoint
3
          [FixedPoint]
orders
          (-FixedPoint
lambda)

-------------------------------------------------------------------------------
-- Helpers vendored from:
-- https://github.com/cardano-scaling/leios-wfa-ls-demo/blob/7bbd846d9765191ca83b58477dc1596f64ac80fd/leios-wfa-ls-demo/lib/Cardano/Leios/NonIntegral.hs#L227
--
-- TODO: merge these into @Cardano.Ledger.NonIntegral@ in @cardano-ledger@

data Step a
  = Stop
  | -- Here we have `Below n err acc divisor`
    Below Int a a a

-- Returns the index of the first element that is NOT certainly BELOW.
-- It evaluates cmps left-to-right, reusing the Taylor-expansion state
-- (acc/err/divisor/n) across elements so we don't redo work.
--
-- Behavior:
--   * If cmp_i is proven ABOVE -> return i
--   * If max iterations reached while testing cmp_i -> return i
--   * If every element is proven BELOW -> returns Nothing
--
-- IMPORTANT: boundX must be e^{|x|} for correct error bounds (see taylorExpCmp).
taylorExpCmpFirstNonLower ::
  forall a.
  RealFrac a =>
  -- | boundX = e^{|x|} for correct error estimation
  a ->
  -- | list of cmp thresholds (checked in order)
  [a] ->
  -- | x in e^x
  a ->
  Maybe Int
taylorExpCmpFirstNonLower :: forall a. RealFrac a => a -> [a] -> a -> Maybe Int
taylorExpCmpFirstNonLower a
boundX [a]
cmps a
x =
  Int -> Int -> a -> a -> a -> Int -> [a] -> Maybe Int
goList Int
1000 Int
0 a
x a
1 a
1 Int
0 [a]
cmps
 where
  -- Traverse the list of cmps, advancing the Taylor state as needed while
  -- checking if the current cmp is ABOVE or BELOW. If ABOVE, return the index.
  goList ::
    Int -> -- maxN
    Int -> -- n
    a -> -- err
    a -> -- acc
    a -> -- divisor
    Int -> -- current index
    [a] -> -- remaining cmps
    Maybe Int
  goList :: Int -> Int -> a -> a -> a -> Int -> [a] -> Maybe Int
goList Int
_ Int
_ a
_ a
_ a
_ Int
_ [] = Maybe Int
forall a. Maybe a
Nothing
  goList Int
maxN Int
n a
err a
acc a
divisor Int
i (a
cmp : [a]
rest) =
    case Int -> Int -> a -> a -> a -> a -> Step a
decideOne Int
maxN Int
n a
err a
acc a
divisor a
cmp of
      Step a
Stop ->
        Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
      Below Int
n' a
err' a
acc' a
divisor' ->
        Int -> Int -> a -> a -> a -> Int -> [a] -> Maybe Int
goList Int
maxN Int
n' a
err' a
acc' a
divisor' (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [a]
rest

  -- Decide current cmp by advancing the shared Taylor state as needed.
  -- If BELOW is established, returns the *advanced* state to continue with.
  -- If ABOVE is established or maxN reached, returns Stop.
  decideOne ::
    Int -> -- maxN
    Int -> -- n
    a -> -- err
    a -> -- acc
    a -> -- divisor
    a -> -- cmp
    Step a
  decideOne :: Int -> Int -> a -> a -> a -> a -> Step a
decideOne Int
maxN Int
n a
err a
acc a
divisor a
cmp
    | Int
maxN Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n = Step a
forall a. Step a
Stop
    | a
cmp a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
acc' a -> a -> a
forall a. Num a => a -> a -> a
+ a
errorTerm = Step a
forall a. Step a
Stop
    | a
cmp a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
acc' a -> a -> a
forall a. Num a => a -> a -> a
- a
errorTerm = Int -> a -> a -> a -> Step a
forall a. Int -> a -> a -> a -> Step a
Below (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
err' a
acc' a
divisor'
    | Bool
otherwise = Int -> Int -> a -> a -> a -> a -> Step a
decideOne Int
maxN (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
err' a
acc' a
divisor' a
cmp
   where
    divisor' :: a
divisor' = a
divisor a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
    nextX :: a
nextX = a
err
    acc' :: a
acc' = a
acc a -> a -> a
forall a. Num a => a -> a -> a
+ a
nextX
    err' :: a
err' = (a
err a -> a -> a
forall a. Num a => a -> a -> a
* a
x) a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
divisor'
    errorTerm :: a
errorTerm = a -> a
forall a. Num a => a -> a
abs (a
err' a -> a -> a
forall a. Num a => a -> a -> a
* a
boundX)