{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Cardano.Ledger.Shelley.Rules.Deposits (
  tests,
)
where

import Test.Cardano.Ledger.Shelley.Rules.TestChain (
  shortChainTrace,
 )

import Cardano.Ledger.Coin
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  CertState (..),
  DState (..),
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  PState (..),
  UTxOState (..),
 )
import Cardano.Ledger.Shelley.Rules.Reports (
  synopsisCoinMap,
 )
import Cardano.Ledger.UMap (depositMap)
import qualified Cardano.Ledger.UMap as UM
import Cardano.Ledger.Val ((<+>))
import qualified Data.Map.Strict as Map
import qualified Prettyprinter as Pretty
import Test.Cardano.Ledger.Shelley.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
import Test.Cardano.Ledger.Shelley.Rules.Chain (CHAIN, ChainState (..))
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC

import Test.Cardano.Ledger.Binary.TreeDiff (ansiDocToString, diffExpr)
import Test.QuickCheck (
  Property,
  counterexample,
  (===),
 )
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)

-- | Tests that redundant Deposit information is consistent
tests ::
  forall era.
  ( EraGen era
  , EraGov era
  , QC.HasTrace (CHAIN era) (GenEnv era)
  ) =>
  TestTree
tests :: forall era.
(EraGen era, EraGov era, HasTrace (CHAIN era) (GenEnv era)) =>
TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Deposit Invariants"
    [ forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Non negative deposits" (forall era.
(EraGen era, HasTrace (CHAIN era) (GenEnv era), EraGov era) =>
Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
shortChainTrace Constants
defaultConstants (forall era. SourceSignalTarget (CHAIN era) -> Property
nonNegativeDeposits @era))
    , forall a. Testable a => TestName -> a -> TestTree
testProperty
        TestName
"Deposits = KeyDeposits + PoolDeposits"
        (forall era.
(EraGen era, HasTrace (CHAIN era) (GenEnv era), EraGov era) =>
Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
shortChainTrace Constants
defaultConstants (forall era. SourceSignalTarget (CHAIN era) -> Property
depositInvariant @era))
    , forall a. Testable a => TestName -> a -> TestTree
testProperty
        TestName
"Reward domain = Deposit domain"
        (forall era.
(EraGen era, HasTrace (CHAIN era) (GenEnv era), EraGov era) =>
Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
shortChainTrace Constants
defaultConstants (forall era. SourceSignalTarget (CHAIN era) -> Property
rewardDepositDomainInvariant @era))
    ]

-- | Check that deposits are always non-negative
nonNegativeDeposits ::
  SourceSignalTarget (CHAIN era) ->
  Property
nonNegativeDeposits :: forall era. SourceSignalTarget (CHAIN era) -> Property
nonNegativeDeposits SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt} =
  let es :: EpochState era
es = (forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) State (CHAIN era)
chainSt
      UTxOState {utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d} = (forall era. LedgerState era -> UTxOState era
lsUTxOState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState) EpochState era
es
   in forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"nonNegativeDeposits: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Coin
d) (Coin
d forall a. Ord a => a -> a -> Bool
>= forall a. Monoid a => a
mempty)

-- | Check that the sum of key Deposits (in the UMap) and the pool Depoits (in psDeposits) are equal to the utsosDeposits
depositInvariant ::
  SourceSignalTarget (CHAIN era) ->
  Property
depositInvariant :: forall era. SourceSignalTarget (CHAIN era) -> Property
depositInvariant SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt} =
  let LedgerState {lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsUTxOState = UTxOState era
utxost, lsCertState :: forall era. LedgerState era -> CertState era
lsCertState = CertState VState era
_vstate PState era
pstate DState era
dstate} = (forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) State (CHAIN era)
chainSt
      allDeposits :: Coin
allDeposits = forall era. UTxOState era -> Coin
utxosDeposited UTxOState era
utxost
      sumCoin :: Map k Coin -> Coin
sumCoin = forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' forall t. Val t => t -> t -> t
(<+>) (Integer -> Coin
Coin Integer
0)
      keyDeposits :: Coin
keyDeposits = (forall a. Compactible a => CompactForm a -> a
UM.fromCompact forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c k. UView c k RDPair -> CompactForm Coin
UM.sumDepositUView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. UMap c -> UView c (Credential 'Staking c) RDPair
UM.RewDepUView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. DState era -> UMap (EraCrypto era)
dsUnified) DState era
dstate
      poolDeposits :: Coin
poolDeposits = forall {k}. Map k Coin -> Coin
sumCoin (forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) Coin
psDeposits PState era
pstate)
   in forall prop. Testable prop => TestName -> prop -> Property
counterexample
        ( Doc AnsiStyle -> TestName
ansiDocToString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. [Doc ann] -> Doc ann
Pretty.vsep forall a b. (a -> b) -> a -> b
$
            [ Doc AnsiStyle
"Deposit invariant fails:"
            , forall ann. Int -> Doc ann -> Doc ann
Pretty.indent Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. [Doc ann] -> Doc ann
Pretty.vsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
Pretty.pretty forall a b. (a -> b) -> a -> b
$
                [ TestName
"All deposits = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Coin
allDeposits
                , TestName
"Key deposits = " forall a. [a] -> [a] -> [a]
++ forall k. Maybe (Map k Coin) -> TestName
synopsisCoinMap (forall a. a -> Maybe a
Just (forall c. UMap c -> Map (Credential 'Staking c) Coin
depositMap (forall era. DState era -> UMap (EraCrypto era)
dsUnified DState era
dstate)))
                , TestName
"Pool deposits = " forall a. [a] -> [a] -> [a]
++ forall k. Maybe (Map k Coin) -> TestName
synopsisCoinMap (forall a. a -> Maybe a
Just (forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) Coin
psDeposits PState era
pstate))
                ]
            ]
        )
        (Coin
allDeposits forall a. (Eq a, Show a) => a -> a -> Property
=== Coin
keyDeposits forall t. Val t => t -> t -> t
<+> Coin
poolDeposits)

rewardDepositDomainInvariant ::
  SourceSignalTarget (CHAIN era) ->
  Property
rewardDepositDomainInvariant :: forall era. SourceSignalTarget (CHAIN era) -> Property
rewardDepositDomainInvariant SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt} =
  let LedgerState {lsCertState :: forall era. LedgerState era -> CertState era
lsCertState = CertState {certDState :: forall era. CertState era -> DState era
certDState = DState era
dstate}} = (forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) State (CHAIN era)
chainSt
      rewardDomain :: Set (Credential 'Staking (EraCrypto era))
rewardDomain = forall c k v. UView c k v -> Set k
UM.domain (forall c. UMap c -> UView c (Credential 'Staking c) RDPair
UM.RewDepUView (forall era. DState era -> UMap (EraCrypto era)
dsUnified DState era
dstate))
      depositDomain :: Set (Credential 'Staking (EraCrypto era))
depositDomain = forall k a. Map k a -> Set k
Map.keysSet (forall c. UMap c -> Map (Credential 'Staking c) Coin
depositMap (forall era. DState era -> UMap (EraCrypto era)
dsUnified DState era
dstate))
   in forall prop. Testable prop => TestName -> prop -> Property
counterexample
        ( Doc AnsiStyle -> TestName
ansiDocToString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. [Doc ann] -> Doc ann
Pretty.vsep forall a b. (a -> b) -> a -> b
$
            [ Doc AnsiStyle
"Reward-Deposit domain invariant fails:"
            , forall ann. Int -> Doc ann -> Doc ann
Pretty.indent Int
2 forall a b. (a -> b) -> a -> b
$ forall a. ToExpr a => a -> a -> Doc AnsiStyle
diffExpr Set (Credential 'Staking (EraCrypto era))
rewardDomain Set (Credential 'Staking (EraCrypto era))
depositDomain
            ]
        )
        (Set (Credential 'Staking (EraCrypto era))
rewardDomain forall a. (Eq a, Show a) => a -> a -> Property
=== Set (Credential 'Staking (EraCrypto era))
depositDomain)