{-# 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 StakeCredential
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"
          (StakeCredential -> Accounts era -> Bool
forall era.
EraAccounts era =>
StakeCredential -> Accounts era -> Bool
isAccountRegistered StakeCredential
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
<$> StakeCredential -> Accounts era -> Maybe (AccountState era)
forall era.
EraAccounts era =>
StakeCredential -> Accounts era -> Maybe (AccountState era)
lookupAccountState StakeCredential
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 StakeCredential
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 (StakeCredential -> Accounts era -> Bool
forall era.
EraAccounts era =>
StakeCredential -> Accounts era -> Bool
isAccountRegistered StakeCredential
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 (StakeCredential -> Accounts era -> Maybe (KeyHash StakePool)
forall era.
EraAccounts era =>
StakeCredential -> Accounts era -> Maybe (KeyHash StakePool)
lookupStakePoolDelegation StakeCredential
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 StakeCredential
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"
          (StakeCredential -> Accounts era -> Bool
forall era.
EraAccounts era =>
StakeCredential -> Accounts era -> Bool
isAccountRegistered StakeCredential
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"
          (StakeCredential -> Accounts era -> Maybe (KeyHash StakePool)
forall era.
EraAccounts era =>
StakeCredential -> Accounts era -> Maybe (KeyHash StakePool)
lookupStakePoolDelegation StakeCredential
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 StakeCredential (CompactForm Coin)
accountsBalances t era
ds = (AccountState era -> CompactForm Coin)
-> Map StakeCredential (AccountState era)
-> Map StakeCredential (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 StakeCredential (AccountState era))
     (t era)
     (Map StakeCredential (AccountState era))
-> Map StakeCredential (AccountState era)
forall s a. s -> Getting a s a -> a
^. (Accounts era
 -> Const (Map StakeCredential (AccountState era)) (Accounts era))
-> t era -> Const (Map StakeCredential (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 StakeCredential (AccountState era)) (Accounts era))
 -> t era -> Const (Map StakeCredential (AccountState era)) (t era))
-> ((Map StakeCredential (AccountState era)
     -> Const
          (Map StakeCredential (AccountState era))
          (Map StakeCredential (AccountState era)))
    -> Accounts era
    -> Const (Map StakeCredential (AccountState era)) (Accounts era))
-> Getting
     (Map StakeCredential (AccountState era))
     (t era)
     (Map StakeCredential (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map StakeCredential (AccountState era)
 -> Const
      (Map StakeCredential (AccountState era))
      (Map StakeCredential (AccountState era)))
-> Accounts era
-> Const (Map StakeCredential (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map StakeCredential (AccountState era))
Lens' (Accounts era) (Map StakeCredential (AccountState era))
accountsMapL)
        sourceBalances :: Map StakeCredential (CompactForm Coin)
sourceBalances = DState era -> Map StakeCredential (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 StakeCredential (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 StakeCredential (CompactForm Coin)
targetBalances = DState era -> Map StakeCredential (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 StakeCredential (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 StakeCredential (CompactForm Coin) -> CompactForm Coin
balancesSum = (CompactForm Coin -> CompactForm Coin -> CompactForm Coin)
-> CompactForm Coin
-> Map StakeCredential (CompactForm Coin)
-> CompactForm Coin
forall b a. (b -> a -> b) -> b -> Map StakeCredential 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 StakeCredential (CompactForm Coin) -> CompactForm Coin
balancesSum Map StakeCredential (CompactForm Coin)
sourceBalances CompactForm Coin -> CompactForm Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Map StakeCredential (CompactForm Coin) -> CompactForm Coin
balancesSum Map StakeCredential (CompactForm Coin)
targetBalances)
          , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"dropped elements have a zero reward balance"
              (Map StakeCredential (CompactForm Coin) -> Bool
forall a. Map StakeCredential a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((CompactForm Coin -> Bool)
-> Map StakeCredential (CompactForm Coin)
-> Map StakeCredential (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 StakeCredential (CompactForm Coin)
 -> Map StakeCredential (CompactForm Coin))
-> Map StakeCredential (CompactForm Coin)
-> Map StakeCredential (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$ Map StakeCredential (CompactForm Coin)
sourceBalances Map StakeCredential (CompactForm Coin)
-> Map StakeCredential (CompactForm Coin)
-> Map StakeCredential (CompactForm Coin)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map StakeCredential (CompactForm Coin)
targetBalances))
          , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              String
"added elements have a zero reward balance"
              (Map StakeCredential (CompactForm Coin) -> Bool
forall a. Map StakeCredential a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((CompactForm Coin -> Bool)
-> Map StakeCredential (CompactForm Coin)
-> Map StakeCredential (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 StakeCredential (CompactForm Coin)
 -> Map StakeCredential (CompactForm Coin))
-> Map StakeCredential (CompactForm Coin)
-> Map StakeCredential (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$ Map StakeCredential (CompactForm Coin)
targetBalances Map StakeCredential (CompactForm Coin)
-> Map StakeCredential (CompactForm Coin)
-> Map StakeCredential (CompactForm Coin)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map StakeCredential (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 StakeCredential 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 StakeCredential DeltaCoin -> Set StakeCredential
forall k a. Map k a -> Set k
Map.keysSet Map StakeCredential DeltaCoin
irwd Set StakeCredential -> Set StakeCredential -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Map StakeCredential Coin -> Set StakeCredential
forall k a. Map k a -> Set k
Map.keysSet (InstantaneousRewards -> Map StakeCredential Coin
iRReserves (InstantaneousRewards -> Map StakeCredential Coin)
-> InstantaneousRewards -> Map StakeCredential 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 StakeCredential Coin -> Coin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRReserves (InstantaneousRewards -> Map StakeCredential Coin)
-> InstantaneousRewards -> Map StakeCredential 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 StakeCredential DeltaCoin -> DeltaCoin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map StakeCredential DeltaCoin
irwd
                      Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map StakeCredential Coin -> Coin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRReserves (InstantaneousRewards -> Map StakeCredential Coin)
-> InstantaneousRewards -> Map StakeCredential 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 StakeCredential Coin -> Coin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential 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 StakeCredential Coin
-> Map StakeCredential DeltaCoin -> Map StakeCredential Coin
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map StakeCredential DeltaCoin
irwd)
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` Map StakeCredential DeltaCoin -> DeltaCoin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map StakeCredential DeltaCoin
irwd
                      Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map StakeCredential Coin -> Coin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRReserves (InstantaneousRewards -> Map StakeCredential Coin)
-> InstantaneousRewards -> Map StakeCredential 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 StakeCredential 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 StakeCredential DeltaCoin -> Set StakeCredential
forall k a. Map k a -> Set k
Map.keysSet Map StakeCredential DeltaCoin
irwd Set StakeCredential -> Set StakeCredential -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Map StakeCredential Coin -> Set StakeCredential
forall k a. Map k a -> Set k
Map.keysSet (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury (InstantaneousRewards -> Map StakeCredential Coin)
-> InstantaneousRewards -> Map StakeCredential 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 StakeCredential Coin -> Coin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury (InstantaneousRewards -> Map StakeCredential Coin)
-> InstantaneousRewards -> Map StakeCredential 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 StakeCredential DeltaCoin -> DeltaCoin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map StakeCredential DeltaCoin
irwd
                      Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map StakeCredential Coin -> Coin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury (InstantaneousRewards -> Map StakeCredential Coin)
-> InstantaneousRewards -> Map StakeCredential 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 StakeCredential Coin -> Coin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential 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 StakeCredential Coin
-> Map StakeCredential DeltaCoin -> Map StakeCredential Coin
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map StakeCredential DeltaCoin
irwd)
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` Map StakeCredential DeltaCoin -> DeltaCoin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map StakeCredential DeltaCoin
irwd
                      Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map StakeCredential Coin -> Coin
forall m. Monoid m => Map StakeCredential m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury (InstantaneousRewards -> Map StakeCredential Coin)
-> InstantaneousRewards -> Map StakeCredential 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 ()