{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.State.SnapShotsSpec (spec) where

import Cardano.Ledger.BaseTypes (
  BoundedRational (..),
  NonNegativeInterval,
  NonZero,
  StrictMaybe (..),
  knownNonZeroBounded,
  nonZeroOr,
  unNonZero,
 )
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core (MaxPledgeLeverage (..))
import Cardano.Ledger.State (maxPool')
import Data.Ratio ((%))
import Data.Word (Word16)
import Test.Cardano.Ledger.Common
import Test.Cardano.Ledger.Core.Arbitrary ()
import Test.Cardano.Ledger.Core.Rational ((%!))

-- | A frozen copy of the reward pot formula as it was before the maximum pledge
-- leverage was introduced in Dijkstra. Used to ensure that a pool that is not
-- subject to a leverage cap is rewarded exactly as it was in the previous eras.
preDijkstraMaxPool ::
  NonNegativeInterval ->
  NonZero Word16 ->
  Coin ->
  Rational ->
  Rational ->
  Coin
preDijkstraMaxPool :: NonNegativeInterval
-> NonZero Word16 -> Coin -> Rational -> Rational -> Coin
preDijkstraMaxPool NonNegativeInterval
a0 NonZero Word16
nOpt (Coin Integer
r) Rational
sigma Rational
pR = Integer -> Coin
Coin (Integer -> Coin) -> Integer -> Coin
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational
factor1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
factor2)
  where
    z0 :: Rational
z0 = NonZero Word16 -> Rational
z0Of NonZero Word16
nOpt
    sigma' :: Rational
sigma' = Rational -> Rational -> Rational
forall a. Ord a => a -> a -> a
min Rational
sigma Rational
z0
    p' :: Rational
p' = Rational -> Rational -> Rational
forall a. Ord a => a -> a -> a
min Rational
pR Rational
z0
    factor1 :: Rational
factor1 = (Integer
r Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ (Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ NonNegativeInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational NonNegativeInterval
a0)
    factor2 :: Rational
factor2 = Rational
sigma' Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
p' Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* NonNegativeInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational NonNegativeInterval
a0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
factor3
    factor3 :: Rational
factor3 = (Rational
sigma' Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
p' Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
factor4) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
z0
    factor4 :: Rational
factor4 = (Rational
z0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
sigma') Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
z0

-- | @z0 = 1/k@, the global saturation point.
z0Of :: NonZero Word16 -> Rational
z0Of :: NonZero Word16 -> Rational
z0Of NonZero Word16
nOpt = Integer
1 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (NonZero Word16 -> Word16
forall a. NonZero a -> a
unNonZero NonZero Word16
nOpt)

genNOpt :: Gen (NonZero Word16)
genNOpt :: Gen (NonZero Word16)
genNOpt = do
  n <- (Word16, Word16) -> Gen Word16
forall a. Random a => (a, a) -> Gen a
choose (Word16
1, Word16
2000)
  pure (n `nonZeroOr` knownNonZeroBounded @1)

-- | A pool's relative stake σ together with its relative pledge.
--
-- Both are generated the way they actually occur on chain, otherwise the leverage
-- cap almost never binds and the properties below become vacuous:
--
-- * σ is generated around the saturation point @z0 = 1/k@, rather than uniformly in
--   [0, 1], since @z0@ is where the reward pot stops growing.
-- * the pledge is a fraction of the stake, since a pool that pledges more than its
--   own stake receives no rewards at all. The leverage of the pool, σ over the
--   pledge, ranges over the whole interval that the maximum pledge leverage can be
--   set to, and beyond.
genSigmaAndRelativePledge :: NonZero Word16 -> Gen (Rational, Rational)
genSigmaAndRelativePledge :: NonZero Word16 -> Gen (Rational, Rational)
genSigmaAndRelativePledge NonZero Word16
nOpt = do
  saturation <- (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
2_000)
  leverage <- choose (1, 20_000)
  let sigma = NonZero Word16 -> Rational
z0Of NonZero Word16
nOpt Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* (Integer
saturation Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1_000)
  pure (sigma, sigma / (leverage % 1))

genMaxPledgeLeverage :: Gen NonNegativeInterval
genMaxPledgeLeverage :: Gen NonNegativeInterval
genMaxPledgeLeverage = do
  l <- (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
1, Integer
10_000)
  pure (l %! 1)

-- | No maximum pledge leverage, ie. the behavior of all the eras prior to Dijkstra.
noLeverageCap :: MaxPledgeLeverage
noLeverageCap :: MaxPledgeLeverage
noLeverageCap = StrictMaybe NonNegativeInterval -> MaxPledgeLeverage
MaxPledgeLeverage StrictMaybe NonNegativeInterval
forall a. StrictMaybe a
SNothing

leverageCap :: NonNegativeInterval -> MaxPledgeLeverage
leverageCap :: NonNegativeInterval -> MaxPledgeLeverage
leverageCap = StrictMaybe NonNegativeInterval -> MaxPledgeLeverage
MaxPledgeLeverage (StrictMaybe NonNegativeInterval -> MaxPledgeLeverage)
-> (NonNegativeInterval -> StrictMaybe NonNegativeInterval)
-> NonNegativeInterval
-> MaxPledgeLeverage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonNegativeInterval -> StrictMaybe NonNegativeInterval
forall a. a -> StrictMaybe a
SJust

spec :: Spec
spec :: Spec
spec = String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"maxPool'" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
  String -> Gen Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"without a leverage cap the pre-Dijkstra reward pot is reproduced exactly" (Gen Property -> Spec) -> Gen Property -> Spec
forall a b. (a -> b) -> a -> b
$ do
    a0 <- Gen NonNegativeInterval
forall a. Arbitrary a => Gen a
arbitrary
    nOpt <- genNOpt
    r <- arbitrary
    (sigma, pR) <- genSigmaAndRelativePledge nOpt
    pure $ maxPool' a0 nOpt r sigma pR noLeverageCap === preDijkstraMaxPool a0 nOpt r sigma pR

  String -> Gen Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"a leverage cap of L is the same as capping the relative stake at L times the pledge" (Gen Property -> Spec) -> Gen Property -> Spec
forall a b. (a -> b) -> a -> b
$ do
    a0 <- Gen NonNegativeInterval
forall a. Arbitrary a => Gen a
arbitrary
    nOpt <- genNOpt
    r <- arbitrary
    (sigma, pR) <- genSigmaAndRelativePledge nOpt
    l <- genMaxPledgeLeverage
    pure $
      maxPool' a0 nOpt r sigma pR (leverageCap l)
        === maxPool' a0 nOpt r (min sigma (unboundRational l * pR)) pR noLeverageCap

  String -> Gen Bool -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"a leverage cap never increases the reward pot" (Gen Bool -> Spec) -> Gen Bool -> Spec
forall a b. (a -> b) -> a -> b
$ do
    a0 <- Gen NonNegativeInterval
forall a. Arbitrary a => Gen a
arbitrary
    nOpt <- genNOpt
    r <- arbitrary
    (sigma, pR) <- genSigmaAndRelativePledge nOpt
    l <- genMaxPledgeLeverage
    pure $ maxPool' a0 nOpt r sigma pR (leverageCap l) <= maxPool' a0 nOpt r sigma pR noLeverageCap

  String -> Gen Bool -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"the reward pot is monotonic in the leverage cap" (Gen Bool -> Spec) -> Gen Bool -> Spec
forall a b. (a -> b) -> a -> b
$ do
    a0 <- Gen NonNegativeInterval
forall a. Arbitrary a => Gen a
arbitrary
    nOpt <- genNOpt
    r <- arbitrary
    (sigma, pR) <- genSigmaAndRelativePledge nOpt
    l1 <- genMaxPledgeLeverage
    l2 <- genMaxPledgeLeverage
    pure $
      maxPool' a0 nOpt r sigma pR (leverageCap (min l1 l2))
        <= maxPool' a0 nOpt r sigma pR (leverageCap (max l1 l2))

  String -> Gen Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"a cap that does not bind gives the same reward pot as no cap at all" (Gen Property -> Spec) -> Gen Property -> Spec
forall a b. (a -> b) -> a -> b
$ do
    a0 <- Gen NonNegativeInterval
forall a. Arbitrary a => Gen a
arbitrary
    nOpt <- genNOpt
    r <- arbitrary
    (sigma, pR) <- genSigmaAndRelativePledge nOpt
    l <- genMaxPledgeLeverage
    let nonBinding = NonNegativeInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational NonNegativeInterval
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
pR Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= Rational -> Rational -> Rational
forall a. Ord a => a -> a -> a
min Rational
sigma (NonZero Word16 -> Rational
z0Of NonZero Word16
nOpt)
        capped = NonNegativeInterval
-> NonZero Word16
-> Coin
-> Rational
-> Rational
-> MaxPledgeLeverage
-> Coin
maxPool' NonNegativeInterval
a0 NonZero Word16
nOpt Coin
r Rational
sigma Rational
pR (NonNegativeInterval -> MaxPledgeLeverage
leverageCap NonNegativeInterval
l)
        uncapped = NonNegativeInterval
-> NonZero Word16
-> Coin
-> Rational
-> Rational
-> MaxPledgeLeverage
-> Coin
maxPool' NonNegativeInterval
a0 NonZero Word16
nOpt Coin
r Rational
sigma Rational
pR MaxPledgeLeverage
noLeverageCap
    pure $
      checkCoverage $
        cover 20 nonBinding "non-binding cap" $
          cover 20 (not nonBinding) "binding cap" $
            if nonBinding then capped === uncapped else property True

  String -> Gen Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"a pool with no pledge gets no rewards whenever a cap is in place" (Gen Property -> Spec) -> Gen Property -> Spec
forall a b. (a -> b) -> a -> b
$ do
    a0 <- Gen NonNegativeInterval
forall a. Arbitrary a => Gen a
arbitrary
    nOpt <- genNOpt
    r <- arbitrary
    (sigma, _) <- genSigmaAndRelativePledge nOpt
    l <- genMaxPledgeLeverage
    pure $ maxPool' a0 nOpt r sigma 0 (leverageCap l) === Coin 0

  String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"the cap binds at exactly L times the relative pledge" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
    -- With a0 = 0 the whole pot collapses to floor(r * σ'), so the effect of the
    -- cap can be read straight off:
    --   k = 10          => z0 = 1/10
    --   σ = z0          => saturated, so without a cap σ' = 1/10
    --   relativePledge  = 1/1000
    --   L = 50          => cap = L·relativePledge = 50/1000 = 1/20, which binds below z0
    let a0 :: NonNegativeInterval
a0 = Integer
0 Integer -> Integer -> NonNegativeInterval
forall r. (IsRatio r, HasCallStack) => Integer -> Integer -> r
%! Integer
1
        nOpt :: NonZero Word16
nOpt = Word16
10 Word16 -> NonZero Word16 -> NonZero Word16
forall a. HasZero a => a -> NonZero a -> NonZero a
`nonZeroOr` forall (n :: Natural) a.
(KnownNat n, 1 <= n, WithinBounds n a, Num a) =>
NonZero a
knownNonZeroBounded @1
        r :: Coin
r = Integer -> Coin
Coin Integer
1000
        sigma :: Rational
sigma = Integer
1 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
10
        pR :: Rational
pR = Integer
1 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1000
        l :: NonNegativeInterval
l = Integer
50 Integer -> Integer -> NonNegativeInterval
forall r. (IsRatio r, HasCallStack) => Integer -> Integer -> r
%! Integer
1
    -- uncapped: floor(1000 * 1/10) = 100
    NonNegativeInterval
-> NonZero Word16
-> Coin
-> Rational
-> Rational
-> MaxPledgeLeverage
-> Coin
maxPool' NonNegativeInterval
a0 NonZero Word16
nOpt Coin
r Rational
sigma Rational
pR MaxPledgeLeverage
noLeverageCap Coin -> Coin -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Integer -> Coin
Coin Integer
100
    -- capped:   floor(1000 * 1/20) = 50
    NonNegativeInterval
-> NonZero Word16
-> Coin
-> Rational
-> Rational
-> MaxPledgeLeverage
-> Coin
maxPool' NonNegativeInterval
a0 NonZero Word16
nOpt Coin
r Rational
sigma Rational
pR (NonNegativeInterval -> MaxPledgeLeverage
leverageCap NonNegativeInterval
l) Coin -> Coin -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Integer -> Coin
Coin Integer
50