{-# 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 Cardano.Ledger.Coin
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  UTxOState (..),
 )
import Cardano.Ledger.Shelley.Rules.Reports (synopsisCoinMap)
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.UMap (depositMap)
import qualified Cardano.Ledger.UMap as UM
import Cardano.Ledger.Val ((<+>))
import qualified Data.Map.Strict as Map
import Lens.Micro ((^.))
import qualified Prettyprinter as Pretty
import Test.Cardano.Ledger.Binary.TreeDiff (ansiDocToString, diffExpr)
import Test.Cardano.Ledger.Shelley.ConcreteCryptoTypes (MockCrypto)
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.Cardano.Ledger.Shelley.Rules.TestChain (shortChainTrace)
import Test.Control.State.Transition.Trace (SourceSignalTarget (..))
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
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
  , EraStake era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  ) =>
  TestTree
tests :: forall era.
(EraGen era, EraGov era, EraStake era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Deposit Invariants"
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Non negative deposits" (Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
forall era.
(EraGen era, EraGov era, EraStake era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
shortChainTrace Constants
defaultConstants (forall era. SourceSignalTarget (CHAIN era) -> Property
nonNegativeDeposits @era))
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
        TestName
"Deposits = KeyDeposits + PoolDeposits"
        (Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
forall era.
(EraGen era, EraGov era, EraStake era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
shortChainTrace Constants
defaultConstants (forall era.
EraCertState era =>
SourceSignalTarget (CHAIN era) -> Property
depositInvariant @era))
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
        TestName
"Reward domain = Deposit domain"
        (Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
forall era.
(EraGen era, EraGov era, EraStake era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
shortChainTrace Constants
defaultConstants (forall era.
EraCertState 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 = (NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes) State (CHAIN era)
ChainState era
chainSt
      UTxOState {utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d} = (LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState (LedgerState era -> UTxOState era)
-> (EpochState era -> LedgerState era)
-> EpochState era
-> UTxOState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState) EpochState era
es
   in TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"nonNegativeDeposits: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Coin -> TestName
forall a. Show a => a -> TestName
show Coin
d) (Coin
d Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
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 ::
  EraCertState era =>
  SourceSignalTarget (CHAIN era) ->
  Property
depositInvariant :: forall era.
EraCertState 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 era
certState} = (EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (ChainState era -> EpochState era)
-> ChainState era
-> LedgerState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes) State (CHAIN era)
ChainState era
chainSt
      dstate :: DState era
dstate = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
      pstate :: PState era
pstate = CertState era
certState CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL
      allDeposits :: Coin
allDeposits = UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosDeposited UTxOState era
utxost
      sumCoin :: Map k Coin -> Coin
sumCoin = (Coin -> Coin -> Coin) -> Coin -> Map k Coin -> Coin
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
(<+>) (Integer -> Coin
Coin Integer
0)
      keyDeposits :: Coin
keyDeposits = (CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
UM.fromCompact (CompactForm Coin -> Coin)
-> (DState era -> CompactForm Coin) -> DState era -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UView (Credential 'Staking) RDPair -> CompactForm Coin
forall k. UView k RDPair -> CompactForm Coin
UM.sumDepositUView (UView (Credential 'Staking) RDPair -> CompactForm Coin)
-> (DState era -> UView (Credential 'Staking) RDPair)
-> DState era
-> CompactForm Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UMap -> UView (Credential 'Staking) RDPair
UM.RewDepUView (UMap -> UView (Credential 'Staking) RDPair)
-> (DState era -> UMap)
-> DState era
-> UView (Credential 'Staking) RDPair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DState era -> UMap
forall era. DState era -> UMap
dsUnified) DState era
dstate
      poolDeposits :: Coin
poolDeposits = Map (KeyHash 'StakePool) Coin -> Coin
forall {k}. Map k Coin -> Coin
sumCoin (PState era -> Map (KeyHash 'StakePool) Coin
forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits PState era
pstate)
   in TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
        ( Doc AnsiStyle -> TestName
ansiDocToString (Doc AnsiStyle -> TestName)
-> ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle]
-> TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
Pretty.vsep ([Doc AnsiStyle] -> TestName) -> [Doc AnsiStyle] -> TestName
forall a b. (a -> b) -> a -> b
$
            [ Doc AnsiStyle
"Deposit invariant fails:"
            , Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
Pretty.indent Int
2 (Doc AnsiStyle -> Doc AnsiStyle)
-> ([TestName] -> Doc AnsiStyle) -> [TestName] -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
Pretty.vsep ([Doc AnsiStyle] -> Doc AnsiStyle)
-> ([TestName] -> [Doc AnsiStyle]) -> [TestName] -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TestName -> Doc AnsiStyle) -> [TestName] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
map TestName -> Doc AnsiStyle
forall ann. TestName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
Pretty.pretty ([TestName] -> Doc AnsiStyle) -> [TestName] -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$
                [ TestName
"All deposits = " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Coin -> TestName
forall a. Show a => a -> TestName
show Coin
allDeposits
                , TestName
"Key deposits = " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Maybe (Map (Credential 'Staking) Coin) -> TestName
forall k. Maybe (Map k Coin) -> TestName
synopsisCoinMap (Map (Credential 'Staking) Coin
-> Maybe (Map (Credential 'Staking) Coin)
forall a. a -> Maybe a
Just (UMap -> Map (Credential 'Staking) Coin
depositMap (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dstate)))
                , TestName
"Pool deposits = " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Maybe (Map (KeyHash 'StakePool) Coin) -> TestName
forall k. Maybe (Map k Coin) -> TestName
synopsisCoinMap (Map (KeyHash 'StakePool) Coin
-> Maybe (Map (KeyHash 'StakePool) Coin)
forall a. a -> Maybe a
Just (PState era -> Map (KeyHash 'StakePool) Coin
forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits PState era
pstate))
                ]
            ]
        )
        (Coin
allDeposits Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Coin
keyDeposits Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
poolDeposits)

rewardDepositDomainInvariant ::
  EraCertState era =>
  SourceSignalTarget (CHAIN era) ->
  Property
rewardDepositDomainInvariant :: forall era.
EraCertState 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 era
certState} = (EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (ChainState era -> EpochState era)
-> ChainState era
-> LedgerState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes) State (CHAIN era)
ChainState era
chainSt
      dstate :: DState era
dstate = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
      rewardDomain :: Set (Credential 'Staking)
rewardDomain = UView (Credential 'Staking) RDPair -> Set (Credential 'Staking)
forall k v. UView k v -> Set k
UM.domain (UMap -> UView (Credential 'Staking) RDPair
UM.RewDepUView (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dstate))
      depositDomain :: Set (Credential 'Staking)
depositDomain = Map (Credential 'Staking) Coin -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet (UMap -> Map (Credential 'Staking) Coin
depositMap (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dstate))
   in TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
        ( Doc AnsiStyle -> TestName
ansiDocToString (Doc AnsiStyle -> TestName)
-> ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle]
-> TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
Pretty.vsep ([Doc AnsiStyle] -> TestName) -> [Doc AnsiStyle] -> TestName
forall a b. (a -> b) -> a -> b
$
            [ Doc AnsiStyle
"Reward-Deposit domain invariant fails:"
            , Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
Pretty.indent Int
2 (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ Set (Credential 'Staking)
-> Set (Credential 'Staking) -> Doc AnsiStyle
forall a. ToExpr a => a -> a -> Doc AnsiStyle
diffExpr Set (Credential 'Staking)
rewardDomain Set (Credential 'Staking)
depositDomain
            ]
        )
        (Set (Credential 'Staking)
rewardDomain Set (Credential 'Staking) -> Set (Credential 'Staking) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Set (Credential 'Staking)
depositDomain)