{-# 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.API (ShelleyDELEG)
import Cardano.Ledger.Shelley.Core
import qualified Cardano.Ledger.Shelley.HardForks as HardForks (allowMIRTransfer)
import Cardano.Ledger.Shelley.Rules (DelegEnv (..))
import Cardano.Ledger.Shelley.State
import qualified Cardano.Ledger.UMap as UM
import Control.SetAlgebra (eval, rng, (∈))
import Data.Foldable (fold)
import Data.Foldable as F (foldl')
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
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 POOL STS Rule, tested on longer traces
-- (double the default length)
tests ::
  forall era.
  ( EraGen era
  , EraStake era
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  ) =>
  TestTree
tests :: forall era.
(EraGen era, EraStake era, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
TestTree
tests =
  TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"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.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyRegistration SourceSignalTarget (ShelleyDELEG era)
delegSst
        , SourceSignalTarget (ShelleyDELEG era) -> Property
forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDeRegistration SourceSignalTarget (ShelleyDELEG era)
delegSst
        , SourceSignalTarget (ShelleyDELEG era) -> Property
forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDelegation SourceSignalTarget (ShelleyDELEG era)
delegSst
        , SourceSignalTarget (ShelleyDELEG era) -> Property
forall era. SourceSignalTarget (ShelleyDELEG era) -> Property
rewardsSumInvariant SourceSignalTarget (ShelleyDELEG era)
delegSst
        , DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
forall era.
(EraPParams era, ShelleyEraTxCert era, ProtVerAtMost era 8) =>
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) =>
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 :: ShelleyEraTxCert era => SourceSignalTarget (ShelleyDELEG era) -> Property
keyRegistration :: forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyRegistration
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = RegTxCert StakeCredential
hk
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
      [ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"a newly registered key should have a reward account"
          (StakeCredential -> UView StakeCredential RDPair -> Bool
forall k v. k -> UView k v -> Bool
UM.member StakeCredential
hk (DState era -> UView StakeCredential RDPair
forall era. DState era -> UView StakeCredential RDPair
rewards DState era
State (ShelleyDELEG era)
targetSt))
      , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"a newly registered key should have a reward account with 0 balance"
          ((RDPair -> CompactForm Coin
UM.rdReward (RDPair -> CompactForm Coin)
-> Maybe RDPair -> Maybe (CompactForm Coin)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakeCredential -> UView StakeCredential RDPair -> Maybe RDPair
forall k v. k -> UView k v -> Maybe v
UM.lookup StakeCredential
hk (DState era -> UView StakeCredential RDPair
forall era. DState era -> UView StakeCredential RDPair
rewards DState era
State (ShelleyDELEG era)
targetSt)) Maybe (CompactForm Coin) -> Maybe (CompactForm Coin) -> Bool
forall a. Eq a => a -> a -> Bool
== 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 :: ShelleyEraTxCert era => SourceSignalTarget (ShelleyDELEG era) -> Property
keyDeRegistration :: forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDeRegistration
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = UnRegTxCert StakeCredential
hk
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
      [ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"a deregistered stake key should no longer be in the rewards mapping"
          (StakeCredential -> UView StakeCredential RDPair -> Bool
forall k v. k -> UView k v -> Bool
UM.notMember StakeCredential
hk (DState era -> UView StakeCredential RDPair
forall era. DState era -> UView StakeCredential RDPair
rewards DState era
State (ShelleyDELEG era)
targetSt))
      , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"a deregistered stake key should no longer be in the delegations mapping"
          (StakeCredential
-> UView StakeCredential (KeyHash 'StakePool) -> Bool
forall k v. k -> UView k v -> Bool
UM.notMember StakeCredential
hk (DState era -> UView StakeCredential (KeyHash 'StakePool)
forall era.
DState era -> UView StakeCredential (KeyHash 'StakePool)
delegations DState era
State (ShelleyDELEG era)
targetSt))
      ]
keyDeRegistration SourceSignalTarget (ShelleyDELEG era)
_ = () -> Property
forall prop. Testable prop => prop -> Property
property ()

-- | Check stake key delegation
keyDelegation :: ShelleyEraTxCert era => SourceSignalTarget (ShelleyDELEG era) -> Property
keyDelegation :: forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDelegation
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = DelegStakeTxCert StakeCredential
from KeyHash 'StakePool
to
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    let fromImage :: Set (KeyHash 'StakePool)
fromImage = Exp (Sett (KeyHash 'StakePool) ()) -> Set (KeyHash 'StakePool)
forall s t. Embed s t => Exp t -> s
eval (Map StakeCredential (KeyHash 'StakePool)
-> Exp (Sett (KeyHash 'StakePool) ())
forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
rng (StakeCredential -> Set StakeCredential
forall a. a -> Set a
Set.singleton StakeCredential
from Set StakeCredential
-> UView StakeCredential (KeyHash 'StakePool)
-> Map StakeCredential (KeyHash 'StakePool)
forall k v. Set k -> UView k v -> Map k v
`UM.domRestrictedMap` DState era -> UView StakeCredential (KeyHash 'StakePool)
forall era.
DState era -> UView StakeCredential (KeyHash 'StakePool)
delegations DState era
State (ShelleyDELEG era)
targetSt))
     in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a delegated key should have a reward account"
              (StakeCredential -> UView StakeCredential RDPair -> Bool
forall k v. k -> UView k v -> Bool
UM.member StakeCredential
from (DState era -> UView StakeCredential RDPair
forall era. DState era -> UView StakeCredential RDPair
rewards DState era
State (ShelleyDELEG era)
targetSt))
          , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a registered stake credential should be delegated"
              (Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
to KeyHash 'StakePool -> Set (KeyHash 'StakePool) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ Set (KeyHash 'StakePool)
fromImage) :: Bool)
          , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a registered stake credential should be uniquely delegated"
              (Set (KeyHash 'StakePool) -> Int
forall a. Set a -> Int
Set.size Set (KeyHash 'StakePool)
fromImage Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1)
          ]
keyDelegation SourceSignalTarget (ShelleyDELEG era)
_ = () -> Property
forall prop. Testable prop => prop -> Property
property ()

-- | Check that the sum of rewards does not change and that each element
-- that is either removed or added has a zero balance.
rewardsSumInvariant :: SourceSignalTarget (ShelleyDELEG era) -> Property
rewardsSumInvariant :: forall era. SourceSignalTarget (ShelleyDELEG era) -> Property
rewardsSumInvariant
  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 sourceRewards :: Map StakeCredential (CompactForm Coin)
sourceRewards = UMap -> Map StakeCredential (CompactForm Coin)
UM.compactRewardMap (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
State (ShelleyDELEG era)
source)
        targetRewards :: Map StakeCredential (CompactForm Coin)
targetRewards = UMap -> Map StakeCredential (CompactForm Coin)
UM.compactRewardMap (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
State (ShelleyDELEG era)
target)
        rewardsSum :: Map StakeCredential (CompactForm Coin) -> CompactForm Coin
rewardsSum = (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
          [ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"sum of rewards should not change"
              (Map StakeCredential (CompactForm Coin) -> CompactForm Coin
rewardsSum Map StakeCredential (CompactForm Coin)
sourceRewards CompactForm Coin -> CompactForm Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Map StakeCredential (CompactForm Coin) -> CompactForm Coin
rewardsSum Map StakeCredential (CompactForm Coin)
targetRewards)
          , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"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
/= Word64 -> CompactForm Coin
UM.CompactCoin Word64
0) (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)
sourceRewards 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)
targetRewards))
          , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"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
/= Word64 -> CompactForm Coin
UM.CompactCoin Word64
0) (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)
targetRewards 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)
sourceRewards))
          ]

checkInstantaneousRewards ::
  (EraPParams era, ShelleyEraTxCert era, ProtVerAtMost era 8) =>
  DelegEnv era ->
  SourceSignalTarget (ShelleyDELEG era) ->
  Property
checkInstantaneousRewards :: forall era.
(EraPParams era, ShelleyEraTxCert era, ProtVerAtMost era 8) =>
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
          [ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"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 DState era
State (ShelleyDELEG era)
target))
          , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a ReservesMIR certificate should add the total value to the `irwd` map, overwriting any existing entries"
              ( if ProtVer -> Bool
HardForks.allowMIRTransfer (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 DState era
State (ShelleyDELEG era)
source)
                      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 DState era
State (ShelleyDELEG era)
target)
                  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 DState era
State (ShelleyDELEG era)
source) 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 DState era
State (ShelleyDELEG era)
target)
              )
          ]
      MirTxCert (MIRCert MIRPot
TreasuryMIR (StakeAddressesMIR Map StakeCredential DeltaCoin
irwd)) ->
        [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"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 DState era
State (ShelleyDELEG era)
target))
          , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a TreasuryMIR certificate should add* the total value to the `irwd` map"
              ( if ProtVer -> Bool
HardForks.allowMIRTransfer (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 DState era
State (ShelleyDELEG era)
source)
                      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 DState era
State (ShelleyDELEG era)
target)
                  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 DState era
State (ShelleyDELEG era)
source) 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 DState era
State (ShelleyDELEG era)
target)
              )
          ]
      Signal (ShelleyDELEG era)
_ -> () -> Property
forall prop. Testable prop => prop -> Property
property ()