{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

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

import Cardano.Ledger.Coin
import Cardano.Ledger.Shelley (hardforkAlonzoAllowMIRTransfer)
import Cardano.Ledger.Shelley.API (ShelleyDELEG)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Rules (DelegEnv (..))
import Cardano.Ledger.Shelley.State
import Data.Foldable (fold)
import Data.Foldable as F (foldl')
import qualified Data.Map.Strict as Map
import Data.Maybe (isNothing)
import qualified Data.Set as Set
import Lens.Micro
import Lens.Micro.Extras (view)
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)
import Test.Cardano.Ledger.Shelley.Rules.TestChain (
  delegTraceFromBlock,
  forAllChainTrace,
  traceLen,
 )
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
 )
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  sourceSignalTargets,
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (
  Property,
  Testable (..),
  conjoin,
  counterexample,
  (===),
 )
import Test.Tasty (TestTree)
import Test.Tasty.QuickCheck (testProperty)

-- | Various properties of the DELEG STS Rule, tested on longer traces
-- (double the default length)
tests ::
  forall era.
  ( EraGen era
  , EraStake era
  , ShelleyEraAccounts era
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  ) =>
  TestTree
tests :: forall era.
(EraGen era, EraStake era, ShelleyEraAccounts era,
 ChainProperty era, HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
TestTree
tests =
  String -> Property -> TestTree
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> TestTree
testProperty String
"properties of the DELEG STS" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(EraGen era, EraGov era, EraStake era, Testable prop,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
traceLen Constants
defaultConstants ((Trace (CHAIN era) -> Property) -> Property)
-> (Trace (CHAIN era) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr -> do
      [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
        (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
chainProp (Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr)
  where
    delegProp :: DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
    delegProp :: DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
delegProp DelegEnv era
denv SourceSignalTarget (ShelleyDELEG era)
delegSst =
      [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
        [ SourceSignalTarget (ShelleyDELEG era) -> Property
forall era.
(EraCertState era, ShelleyEraTxCert era) =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyRegistration SourceSignalTarget (ShelleyDELEG era)
delegSst
        , SourceSignalTarget (ShelleyDELEG era) -> Property
forall era.
(EraCertState era, ShelleyEraTxCert era) =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDeRegistration SourceSignalTarget (ShelleyDELEG era)
delegSst
        , SourceSignalTarget (ShelleyDELEG era) -> Property
forall era.
(EraCertState era, ShelleyEraTxCert era) =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDelegation SourceSignalTarget (ShelleyDELEG era)
delegSst
        , SourceSignalTarget (ShelleyDELEG era) -> Property
forall era.
EraCertState era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
balancesSumInvariant SourceSignalTarget (ShelleyDELEG era)
delegSst
        , DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
forall era.
(EraPParams era, EraCertState era, ShelleyEraTxCert era,
 AtMostEra "Babbage" era) =>
DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
checkInstantaneousRewards DelegEnv era
denv SourceSignalTarget (ShelleyDELEG era)
delegSst
        ]
    chainProp :: SourceSignalTarget (CHAIN era) -> Property
    chainProp :: SourceSignalTarget (CHAIN era) -> Property
chainProp (SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block}) =
      let delegInfo :: (DelegEnv era, Trace (ShelleyDELEG era))
delegInfo = ChainState era
-> Block (BHeader MockCrypto) era
-> (DelegEnv era, Trace (ShelleyDELEG era))
forall era.
(ChainProperty era, ShelleyEraTxBody era,
 ShelleyEraAccounts era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (DelegEnv era, Trace (ShelleyDELEG era))
delegTraceFromBlock State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
          delegEnv :: DelegEnv era
delegEnv = (DelegEnv era, Trace (ShelleyDELEG era)) -> DelegEnv era
forall a b. (a, b) -> a
fst (DelegEnv era, Trace (ShelleyDELEG era))
delegInfo
          delegTr :: Trace (ShelleyDELEG era)
delegTr = (DelegEnv era, Trace (ShelleyDELEG era))
-> Trace (ShelleyDELEG era)
forall a b. (a, b) -> b
snd (DelegEnv era, Trace (ShelleyDELEG era))
delegInfo
          delegSsts :: [SourceSignalTarget (ShelleyDELEG era)]
delegSsts = Trace (ShelleyDELEG era) -> [SourceSignalTarget (ShelleyDELEG era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (ShelleyDELEG era)
delegTr
       in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ((SourceSignalTarget (ShelleyDELEG era) -> Property)
-> [SourceSignalTarget (ShelleyDELEG era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
delegProp DelegEnv era
delegEnv) [SourceSignalTarget (ShelleyDELEG era)]
delegSsts)

-- | Check stake key registration
keyRegistration ::
  (EraCertState era, ShelleyEraTxCert era) =>
  SourceSignalTarget (ShelleyDELEG era) ->
  Property
keyRegistration :: forall era.
(EraCertState era, ShelleyEraTxCert era) =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyRegistration
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = RegTxCert Credential Staking
cred
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
      [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"a newly registered key should have a reward account"
          (Credential Staking -> Accounts era -> Bool
forall era.
EraAccounts era =>
Credential Staking -> Accounts era -> Bool
isAccountRegistered Credential Staking
cred (CertState era
State (ShelleyDELEG era)
targetSt CertState era
-> Getting (Accounts era) (CertState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> Getting (Accounts era) (CertState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL))
      , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"a newly registered key should have a reward account with 0 balance"
          ( ((AccountState era
-> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
-> CompactForm Coin
forall s a. s -> Getting a s a -> a
^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState era) (CompactForm Coin)
balanceAccountStateL) (AccountState era -> CompactForm Coin)
-> Maybe (AccountState era) -> Maybe (CompactForm Coin)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential Staking -> Accounts era -> Maybe (AccountState era)
forall era.
EraAccounts era =>
Credential Staking -> Accounts era -> Maybe (AccountState era)
lookupAccountState Credential Staking
cred (CertState era
State (ShelleyDELEG era)
targetSt CertState era
-> Getting (Accounts era) (CertState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> Getting (Accounts era) (CertState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL))
              Maybe (CompactForm Coin) -> Maybe (CompactForm Coin) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CompactForm Coin -> Maybe (CompactForm Coin)
forall a. a -> Maybe a
Just CompactForm Coin
forall a. Monoid a => a
mempty
          )
      ]
keyRegistration SourceSignalTarget (ShelleyDELEG era)
_ = () -> Property
forall prop. Testable prop => prop -> Property
property ()

-- | Check stake key de-registration
keyDeRegistration ::
  (EraCertState era, ShelleyEraTxCert era) =>
  SourceSignalTarget (ShelleyDELEG era) ->
  Property
keyDeRegistration :: forall era.
(EraCertState era, ShelleyEraTxCert era) =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDeRegistration
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = UnRegTxCert Credential Staking
cred
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
      [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"a deregistered stake key should no longer be in the rewards mapping"
          (Bool -> Bool
not (Credential Staking -> Accounts era -> Bool
forall era.
EraAccounts era =>
Credential Staking -> Accounts era -> Bool
isAccountRegistered Credential Staking
cred (CertState era
State (ShelleyDELEG era)
targetSt CertState era
-> Getting (Accounts era) (CertState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> Getting (Accounts era) (CertState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL)))
      , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"a deregistered stake key should no longer be in the delegations mapping"
          (Maybe (KeyHash StakePool) -> Bool
forall a. Maybe a -> Bool
isNothing (Credential Staking -> Accounts era -> Maybe (KeyHash StakePool)
forall era.
EraAccounts era =>
Credential Staking -> Accounts era -> Maybe (KeyHash StakePool)
lookupStakePoolDelegation Credential Staking
cred (CertState era
State (ShelleyDELEG era)
targetSt CertState era
-> Getting (Accounts era) (CertState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> Getting (Accounts era) (CertState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL)))
      ]
keyDeRegistration SourceSignalTarget (ShelleyDELEG era)
_ = () -> Property
forall prop. Testable prop => prop -> Property
property ()

-- | Check stake key delegation
keyDelegation ::
  (EraCertState era, ShelleyEraTxCert era) =>
  SourceSignalTarget (ShelleyDELEG era) ->
  Property
keyDelegation :: forall era.
(EraCertState era, ShelleyEraTxCert era) =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDelegation
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = DelegStakeTxCert Credential Staking
stakeCred KeyHash StakePool
poolId
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
      [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"a delegated key should have a reward account"
          (Credential Staking -> Accounts era -> Bool
forall era.
EraAccounts era =>
Credential Staking -> Accounts era -> Bool
isAccountRegistered Credential Staking
stakeCred (CertState era
State (ShelleyDELEG era)
targetSt CertState era
-> Getting (Accounts era) (CertState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> Getting (Accounts era) (CertState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL))
      , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"a registered stake credential should be delegated"
          (Credential Staking -> Accounts era -> Maybe (KeyHash StakePool)
forall era.
EraAccounts era =>
Credential Staking -> Accounts era -> Maybe (KeyHash StakePool)
lookupStakePoolDelegation Credential Staking
stakeCred (CertState era
State (ShelleyDELEG era)
targetSt CertState era
-> Getting (Accounts era) (CertState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> Getting (Accounts era) (CertState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL) Maybe (KeyHash StakePool) -> Maybe (KeyHash StakePool) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== KeyHash StakePool -> Maybe (KeyHash StakePool)
forall a. a -> Maybe a
Just KeyHash StakePool
poolId)
      ]
keyDelegation SourceSignalTarget (ShelleyDELEG era)
_ = () -> Property
forall prop. Testable prop => prop -> Property
property ()

-- | Check that the sum of balances does not change and that each element
-- that is either removed or added has a zero balance.
balancesSumInvariant :: EraCertState era => SourceSignalTarget (ShelleyDELEG era) -> Property
balancesSumInvariant :: forall era.
EraCertState era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
balancesSumInvariant
  SourceSignalTarget {State (ShelleyDELEG era)
source :: forall a. SourceSignalTarget a -> State a
source :: State (ShelleyDELEG era)
source, State (ShelleyDELEG era)
target :: forall a. SourceSignalTarget a -> State a
target :: State (ShelleyDELEG era)
target} =
    let accountsBalances :: t era -> Map (Credential Staking) (CompactForm Coin)
accountsBalances t era
ds = (AccountState era -> CompactForm Coin)
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) (CompactForm Coin)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (AccountState era
-> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
-> CompactForm Coin
forall s a. s -> Getting a s a -> a
^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState era) (CompactForm Coin)
balanceAccountStateL) (t era
ds t era
-> Getting
     (Map (Credential Staking) (AccountState era))
     (t era)
     (Map (Credential Staking) (AccountState era))
-> Map (Credential Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (Accounts era
 -> Const
      (Map (Credential Staking) (AccountState era)) (Accounts era))
-> t era
-> Const (Map (Credential Staking) (AccountState era)) (t era)
forall era. Lens' (t era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential Staking) (AccountState era)) (Accounts era))
 -> t era
 -> Const (Map (Credential Staking) (AccountState era)) (t era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential Staking) (AccountState era)) (Accounts era))
-> Getting
     (Map (Credential Staking) (AccountState era))
     (t era)
     (Map (Credential Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState era)
 -> Const
      (Map (Credential Staking) (AccountState era))
      (Map (Credential Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
accountsMapL)
        sourceBalances :: Map (Credential Staking) (CompactForm Coin)
sourceBalances = DState era -> Map (Credential Staking) (CompactForm Coin)
forall {era} {t :: * -> *}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraAccounts era, CanSetAccounts t) =>
t era -> Map (Credential Staking) (CompactForm Coin)
accountsBalances (CertState era
State (ShelleyDELEG era)
source 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)
        targetBalances :: Map (Credential Staking) (CompactForm Coin)
targetBalances = DState era -> Map (Credential Staking) (CompactForm Coin)
forall {era} {t :: * -> *}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraAccounts era, CanSetAccounts t) =>
t era -> Map (Credential Staking) (CompactForm Coin)
accountsBalances (CertState era
State (ShelleyDELEG era)
target 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)
        balancesSum :: Map (Credential Staking) (CompactForm Coin) -> CompactForm Coin
balancesSum = (CompactForm Coin -> CompactForm Coin -> CompactForm Coin)
-> CompactForm Coin
-> Map (Credential Staking) (CompactForm Coin)
-> CompactForm Coin
forall b a. (b -> a -> b) -> b -> Map (Credential Staking) a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' CompactForm Coin -> CompactForm Coin -> CompactForm Coin
forall a. Semigroup a => a -> a -> a
(<>) CompactForm Coin
forall a. Monoid a => a
mempty
     in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"sum of balances should not change"
              (Map (Credential Staking) (CompactForm Coin) -> CompactForm Coin
balancesSum Map (Credential Staking) (CompactForm Coin)
sourceBalances CompactForm Coin -> CompactForm Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Map (Credential Staking) (CompactForm Coin) -> CompactForm Coin
balancesSum Map (Credential Staking) (CompactForm Coin)
targetBalances)
          , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"dropped elements have a zero reward balance"
              (Map (Credential Staking) (CompactForm Coin) -> Bool
forall a. Map (Credential Staking) a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((CompactForm Coin -> Bool)
-> Map (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (CompactForm Coin -> CompactForm Coin -> Bool
forall a. Eq a => a -> a -> Bool
/= CompactForm Coin
forall a. Monoid a => a
mempty) (Map (Credential Staking) (CompactForm Coin)
 -> Map (Credential Staking) (CompactForm Coin))
-> Map (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$ Map (Credential Staking) (CompactForm Coin)
sourceBalances Map (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map (Credential Staking) (CompactForm Coin)
targetBalances))
          , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"added elements have a zero reward balance"
              (Map (Credential Staking) (CompactForm Coin) -> Bool
forall a. Map (Credential Staking) a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((CompactForm Coin -> Bool)
-> Map (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (CompactForm Coin -> CompactForm Coin -> Bool
forall a. Eq a => a -> a -> Bool
/= CompactForm Coin
forall a. Monoid a => a
mempty) (Map (Credential Staking) (CompactForm Coin)
 -> Map (Credential Staking) (CompactForm Coin))
-> Map (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$ Map (Credential Staking) (CompactForm Coin)
targetBalances Map (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map (Credential Staking) (CompactForm Coin)
sourceBalances))
          ]

checkInstantaneousRewards ::
  (EraPParams era, EraCertState era, ShelleyEraTxCert era, AtMostEra "Babbage" era) =>
  DelegEnv era ->
  SourceSignalTarget (ShelleyDELEG era) ->
  Property
checkInstantaneousRewards :: forall era.
(EraPParams era, EraCertState era, ShelleyEraTxCert era,
 AtMostEra "Babbage" era) =>
DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
checkInstantaneousRewards
  DelegEnv era
denv
  SourceSignalTarget {State (ShelleyDELEG era)
source :: forall a. SourceSignalTarget a -> State a
source :: State (ShelleyDELEG era)
source, Signal (ShelleyDELEG era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal :: Signal (ShelleyDELEG era)
signal, State (ShelleyDELEG era)
target :: forall a. SourceSignalTarget a -> State a
target :: State (ShelleyDELEG era)
target} =
    case Signal (ShelleyDELEG era)
signal of
      MirTxCert (MIRCert MIRPot
ReservesMIR (StakeAddressesMIR Map (Credential Staking) DeltaCoin
irwd)) ->
        [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"a ReservesMIR certificate should add all entries to the `irwd` mapping"
              (Map (Credential Staking) DeltaCoin -> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential Staking) DeltaCoin
irwd Set (Credential Staking) -> Set (Credential Staking) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Map (Credential Staking) Coin -> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet (InstantaneousRewards -> Map (Credential Staking) Coin
iRReserves (InstantaneousRewards -> Map (Credential Staking) Coin)
-> InstantaneousRewards -> Map (Credential Staking) Coin
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
target 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)))
          , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"a ReservesMIR certificate should add the total value to the `irwd` map, overwriting any existing entries"
              ( if ProtVer -> Bool
hardforkAlonzoAllowMIRTransfer (ProtVer -> Bool)
-> (PParams era -> ProtVer) -> PParams era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting ProtVer (PParams era) ProtVer -> PParams era -> ProtVer
forall a s. Getting a s a -> s -> a
view Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL (PParams era -> Bool) -> PParams era -> Bool
forall a b. (a -> b) -> a -> b
$ DelegEnv era -> PParams era
forall era. DelegEnv era -> PParams era
ppDE DelegEnv era
denv
                  then -- In the Alonzo era, repeated fields are added
                    Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map (Credential Staking) Coin
iRReserves (InstantaneousRewards -> Map (Credential Staking) Coin)
-> InstantaneousRewards -> Map (Credential Staking) Coin
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
source 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))
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` Map (Credential Staking) DeltaCoin -> DeltaCoin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential Staking) DeltaCoin
irwd
                      Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map (Credential Staking) Coin
iRReserves (InstantaneousRewards -> Map (Credential Staking) Coin)
-> InstantaneousRewards -> Map (Credential Staking) Coin
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
target 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))
                  else -- Prior to the Alonzo era, repeated fields overridden
                    Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map (Credential Staking) Coin
iRReserves (DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
source 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)) Map (Credential Staking) Coin
-> Map (Credential Staking) DeltaCoin
-> Map (Credential Staking) Coin
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map (Credential Staking) DeltaCoin
irwd)
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` Map (Credential Staking) DeltaCoin -> DeltaCoin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential Staking) DeltaCoin
irwd
                      Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map (Credential Staking) Coin
iRReserves (InstantaneousRewards -> Map (Credential Staking) Coin)
-> InstantaneousRewards -> Map (Credential Staking) Coin
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
target 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))
              )
          ]
      MirTxCert (MIRCert MIRPot
TreasuryMIR (StakeAddressesMIR Map (Credential Staking) DeltaCoin
irwd)) ->
        [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"a TreasuryMIR certificate should add all entries to the `irwd` mapping"
              (Map (Credential Staking) DeltaCoin -> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential Staking) DeltaCoin
irwd Set (Credential Staking) -> Set (Credential Staking) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Map (Credential Staking) Coin -> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet (InstantaneousRewards -> Map (Credential Staking) Coin
iRTreasury (InstantaneousRewards -> Map (Credential Staking) Coin)
-> InstantaneousRewards -> Map (Credential Staking) Coin
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
target 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)))
          , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"a TreasuryMIR certificate should add* the total value to the `irwd` map"
              ( if ProtVer -> Bool
hardforkAlonzoAllowMIRTransfer (ProtVer -> Bool)
-> (DelegEnv era -> ProtVer) -> DelegEnv era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting ProtVer (PParams era) ProtVer -> PParams era -> ProtVer
forall a s. Getting a s a -> s -> a
view Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL (PParams era -> ProtVer)
-> (DelegEnv era -> PParams era) -> DelegEnv era -> ProtVer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DelegEnv era -> PParams era
forall era. DelegEnv era -> PParams era
ppDE (DelegEnv era -> Bool) -> DelegEnv era -> Bool
forall a b. (a -> b) -> a -> b
$ DelegEnv era
denv
                  then -- In the Alonzo era, repeated fields are added
                    Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map (Credential Staking) Coin
iRTreasury (InstantaneousRewards -> Map (Credential Staking) Coin)
-> InstantaneousRewards -> Map (Credential Staking) Coin
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
source 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))
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` Map (Credential Staking) DeltaCoin -> DeltaCoin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential Staking) DeltaCoin
irwd
                      Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map (Credential Staking) Coin
iRTreasury (InstantaneousRewards -> Map (Credential Staking) Coin)
-> InstantaneousRewards -> Map (Credential Staking) Coin
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
target 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))
                  else -- Prior to the Alonzo era, repeated fields overridden
                    Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map (Credential Staking) Coin
iRTreasury (DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
source 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)) Map (Credential Staking) Coin
-> Map (Credential Staking) DeltaCoin
-> Map (Credential Staking) Coin
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map (Credential Staking) DeltaCoin
irwd)
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` Map (Credential Staking) DeltaCoin -> DeltaCoin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential Staking) DeltaCoin
irwd
                      Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map (Credential Staking) Coin
iRTreasury (InstantaneousRewards -> Map (Credential Staking) Coin)
-> InstantaneousRewards -> Map (Credential Staking) Coin
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards (CertState era
State (ShelleyDELEG era)
target 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))
              )
          ]
      Signal (ShelleyDELEG era)
_ -> () -> Property
forall prop. Testable prop => prop -> Property
property ()