{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.PoolReap (
  ShelleyPOOLREAP,
  ShelleyPoolreapEvent (..),
  ShelleyPoolreapState (..),
  PredicateFailure,
  ShelleyPoolreapPredFailure,
) where

import Cardano.Ledger.Address (RewardAccount, raCredential)
import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.PoolParams (ppRewardAccount)
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyPOOLREAP)
import Cardano.Ledger.Shelley.LedgerState (
  UTxOState (..),
  allObligations,
  utxosGovStateL,
 )
import Cardano.Ledger.Shelley.LedgerState.Types (potEqualsObligation)
import Cardano.Ledger.Slot (EpochNo (..))
import Cardano.Ledger.State
import Cardano.Ledger.UMap (UView (RewDepUView, SPoolUView), compactCoinOrError)
import qualified Cardano.Ledger.UMap as UM
import Cardano.Ledger.Val ((<+>), (<->))
import Control.DeepSeq (NFData)
import Control.SetAlgebra (dom, eval, setSingleton, (⋪), (▷), (◁))
import Control.State.Transition (
  Assertion (..),
  AssertionViolation (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  tellEvent,
 )
import Data.Default (Default, def)
import Data.Foldable (fold)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set (member)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks (..))

data ShelleyPoolreapState era = PoolreapState
  { forall era. ShelleyPoolreapState era -> UTxOState era
prUTxOSt :: UTxOState era
  , forall era. ShelleyPoolreapState era -> ChainAccountState
prChainAccountState :: ChainAccountState
  , forall era. ShelleyPoolreapState era -> CertState era
prCertState :: CertState era
  }

deriving stock instance
  (Show (UTxOState era), Show (CertState era)) => Show (ShelleyPoolreapState era)

data ShelleyPoolreapPredFailure era -- No predicate failures
  deriving (Int -> ShelleyPoolreapPredFailure era -> ShowS
[ShelleyPoolreapPredFailure era] -> ShowS
ShelleyPoolreapPredFailure era -> String
(Int -> ShelleyPoolreapPredFailure era -> ShowS)
-> (ShelleyPoolreapPredFailure era -> String)
-> ([ShelleyPoolreapPredFailure era] -> ShowS)
-> Show (ShelleyPoolreapPredFailure era)
forall era. Int -> ShelleyPoolreapPredFailure era -> ShowS
forall era. [ShelleyPoolreapPredFailure era] -> ShowS
forall era. ShelleyPoolreapPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall era. Int -> ShelleyPoolreapPredFailure era -> ShowS
showsPrec :: Int -> ShelleyPoolreapPredFailure era -> ShowS
$cshow :: forall era. ShelleyPoolreapPredFailure era -> String
show :: ShelleyPoolreapPredFailure era -> String
$cshowList :: forall era. [ShelleyPoolreapPredFailure era] -> ShowS
showList :: [ShelleyPoolreapPredFailure era] -> ShowS
Show, ShelleyPoolreapPredFailure era
-> ShelleyPoolreapPredFailure era -> Bool
(ShelleyPoolreapPredFailure era
 -> ShelleyPoolreapPredFailure era -> Bool)
-> (ShelleyPoolreapPredFailure era
    -> ShelleyPoolreapPredFailure era -> Bool)
-> Eq (ShelleyPoolreapPredFailure era)
forall era.
ShelleyPoolreapPredFailure era
-> ShelleyPoolreapPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ShelleyPoolreapPredFailure era
-> ShelleyPoolreapPredFailure era -> Bool
== :: ShelleyPoolreapPredFailure era
-> ShelleyPoolreapPredFailure era -> Bool
$c/= :: forall era.
ShelleyPoolreapPredFailure era
-> ShelleyPoolreapPredFailure era -> Bool
/= :: ShelleyPoolreapPredFailure era
-> ShelleyPoolreapPredFailure era -> Bool
Eq, (forall x.
 ShelleyPoolreapPredFailure era
 -> Rep (ShelleyPoolreapPredFailure era) x)
-> (forall x.
    Rep (ShelleyPoolreapPredFailure era) x
    -> ShelleyPoolreapPredFailure era)
-> Generic (ShelleyPoolreapPredFailure era)
forall x.
Rep (ShelleyPoolreapPredFailure era) x
-> ShelleyPoolreapPredFailure era
forall x.
ShelleyPoolreapPredFailure era
-> Rep (ShelleyPoolreapPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyPoolreapPredFailure era) x
-> ShelleyPoolreapPredFailure era
forall era x.
ShelleyPoolreapPredFailure era
-> Rep (ShelleyPoolreapPredFailure era) x
$cfrom :: forall era x.
ShelleyPoolreapPredFailure era
-> Rep (ShelleyPoolreapPredFailure era) x
from :: forall x.
ShelleyPoolreapPredFailure era
-> Rep (ShelleyPoolreapPredFailure era) x
$cto :: forall era x.
Rep (ShelleyPoolreapPredFailure era) x
-> ShelleyPoolreapPredFailure era
to :: forall x.
Rep (ShelleyPoolreapPredFailure era) x
-> ShelleyPoolreapPredFailure era
Generic)

instance NFData (ShelleyPoolreapPredFailure era)

data ShelleyPoolreapEvent era = RetiredPools
  { forall era.
ShelleyPoolreapEvent era
-> Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
refundPools ::
      Map.Map (Credential 'Staking) (Map.Map (KeyHash 'StakePool) Coin)
  , forall era.
ShelleyPoolreapEvent era
-> Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
unclaimedPools ::
      Map.Map (Credential 'Staking) (Map.Map (KeyHash 'StakePool) Coin)
  , forall era. ShelleyPoolreapEvent era -> EpochNo
epochNo :: EpochNo
  }
  deriving ((forall x.
 ShelleyPoolreapEvent era -> Rep (ShelleyPoolreapEvent era) x)
-> (forall x.
    Rep (ShelleyPoolreapEvent era) x -> ShelleyPoolreapEvent era)
-> Generic (ShelleyPoolreapEvent era)
forall x.
Rep (ShelleyPoolreapEvent era) x -> ShelleyPoolreapEvent era
forall x.
ShelleyPoolreapEvent era -> Rep (ShelleyPoolreapEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyPoolreapEvent era) x -> ShelleyPoolreapEvent era
forall era x.
ShelleyPoolreapEvent era -> Rep (ShelleyPoolreapEvent era) x
$cfrom :: forall era x.
ShelleyPoolreapEvent era -> Rep (ShelleyPoolreapEvent era) x
from :: forall x.
ShelleyPoolreapEvent era -> Rep (ShelleyPoolreapEvent era) x
$cto :: forall era x.
Rep (ShelleyPoolreapEvent era) x -> ShelleyPoolreapEvent era
to :: forall x.
Rep (ShelleyPoolreapEvent era) x -> ShelleyPoolreapEvent era
Generic)

deriving instance Eq (ShelleyPoolreapEvent era)

instance NFData (ShelleyPoolreapEvent era)

instance NoThunks (ShelleyPoolreapPredFailure era)

instance (Default (UTxOState era), Default (CertState era)) => Default (ShelleyPoolreapState era) where
  def :: ShelleyPoolreapState era
def = UTxOState era
-> ChainAccountState -> CertState era -> ShelleyPoolreapState era
forall era.
UTxOState era
-> ChainAccountState -> CertState era -> ShelleyPoolreapState era
PoolreapState UTxOState era
forall a. Default a => a
def ChainAccountState
forall a. Default a => a
def CertState era
forall a. Default a => a
def

type instance EraRuleEvent "POOLREAP" ShelleyEra = ShelleyPoolreapEvent ShelleyEra

instance
  ( Default (ShelleyPoolreapState era)
  , EraPParams era
  , EraGov era
  , EraCertState era
  ) =>
  STS (ShelleyPOOLREAP era)
  where
  type State (ShelleyPOOLREAP era) = ShelleyPoolreapState era
  type Signal (ShelleyPOOLREAP era) = EpochNo
  type Environment (ShelleyPOOLREAP era) = ()
  type BaseM (ShelleyPOOLREAP era) = ShelleyBase
  type PredicateFailure (ShelleyPOOLREAP era) = ShelleyPoolreapPredFailure era
  type Event (ShelleyPOOLREAP era) = ShelleyPoolreapEvent era
  transitionRules :: [TransitionRule (ShelleyPOOLREAP era)]
transitionRules = [TransitionRule (ShelleyPOOLREAP era)
forall era.
EraCertState era =>
TransitionRule (ShelleyPOOLREAP era)
poolReapTransition]

  renderAssertionViolation :: AssertionViolation (ShelleyPOOLREAP era) -> String
renderAssertionViolation = AssertionViolation (ShelleyPOOLREAP era) -> String
forall era t.
(EraGov era, State t ~ ShelleyPoolreapState era,
 EraCertState era) =>
AssertionViolation t -> String
renderPoolReapViolation
  assertions :: [Assertion (ShelleyPOOLREAP era)]
assertions =
    [ String
-> (TRC (ShelleyPOOLREAP era)
    -> State (ShelleyPOOLREAP era) -> Bool)
-> Assertion (ShelleyPOOLREAP era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must equal obligation (PoolReap)"
        ( \TRC (ShelleyPOOLREAP era)
_trc State (ShelleyPOOLREAP era)
st ->
            CertState era -> UTxOState era -> Bool
forall era.
(EraGov era, EraCertState era) =>
CertState era -> UTxOState era -> Bool
potEqualsObligation
              (ShelleyPoolreapState era -> CertState era
forall era. ShelleyPoolreapState era -> CertState era
prCertState State (ShelleyPOOLREAP era)
ShelleyPoolreapState era
st)
              (ShelleyPoolreapState era -> UTxOState era
forall era. ShelleyPoolreapState era -> UTxOState era
prUTxOSt State (ShelleyPOOLREAP era)
ShelleyPoolreapState era
st)
        )
    , String
-> (TRC (ShelleyPOOLREAP era)
    -> State (ShelleyPOOLREAP era) -> Bool)
-> Assertion (ShelleyPOOLREAP era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"PoolReap may not create or remove reward accounts"
        ( \(TRC (Environment (ShelleyPOOLREAP era)
_, State (ShelleyPOOLREAP era)
st, Signal (ShelleyPOOLREAP era)
_)) State (ShelleyPOOLREAP era)
st' ->
            let r :: ShelleyPoolreapState era -> UView (Credential 'Staking) RDPair
r ShelleyPoolreapState era
prState = DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards (ShelleyPoolreapState era -> CertState era
forall era. ShelleyPoolreapState era -> CertState era
prCertState ShelleyPoolreapState era
prState 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)
             in UView (Credential 'Staking) RDPair -> Int
forall a. UView (Credential 'Staking) a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (ShelleyPoolreapState era -> UView (Credential 'Staking) RDPair
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraCertState era) =>
ShelleyPoolreapState era -> UView (Credential 'Staking) RDPair
r State (ShelleyPOOLREAP era)
ShelleyPoolreapState era
st) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== UView (Credential 'Staking) RDPair -> Int
forall a. UView (Credential 'Staking) a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (ShelleyPoolreapState era -> UView (Credential 'Staking) RDPair
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraCertState era) =>
ShelleyPoolreapState era -> UView (Credential 'Staking) RDPair
r State (ShelleyPOOLREAP era)
ShelleyPoolreapState era
st')
        )
    ]

poolReapTransition :: forall era. EraCertState era => TransitionRule (ShelleyPOOLREAP era)
poolReapTransition :: forall era.
EraCertState era =>
TransitionRule (ShelleyPOOLREAP era)
poolReapTransition = do
  TRC (Environment (ShelleyPOOLREAP era)
_, PoolreapState UTxOState era
us ChainAccountState
a CertState era
cs, Signal (ShelleyPOOLREAP era)
e) <- Rule
  (ShelleyPOOLREAP era)
  'Transition
  (RuleContext 'Transition (ShelleyPOOLREAP era))
F (Clause (ShelleyPOOLREAP era) 'Transition)
  (TRC (ShelleyPOOLREAP era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  let
    ps :: PState era
ps = CertState era
cs CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL
    ds :: DState era
ds = CertState era
cs 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
    -- The set of pools retiring this epoch
    retired :: Set (KeyHash 'StakePool)
    retired :: Set (KeyHash 'StakePool)
retired = Exp (Sett (KeyHash 'StakePool) ()) -> Set (KeyHash 'StakePool)
forall s t. Embed s t => Exp t -> s
eval (Exp (Map (KeyHash 'StakePool) EpochNo)
-> Exp (Sett (KeyHash 'StakePool) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (PState era -> Map (KeyHash 'StakePool) EpochNo
forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
psRetiring PState era
ps Map (KeyHash 'StakePool) EpochNo
-> Exp (Single EpochNo ())
-> Exp (Map (KeyHash 'StakePool) EpochNo)
forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
▷ EpochNo -> Exp (Single EpochNo ())
forall k. Ord k => k -> Exp (Single k ())
setSingleton EpochNo
Signal (ShelleyPOOLREAP era)
e))
    -- The Map of pools (retiring this epoch) to their deposits
    retiringDeposits, remainingDeposits :: Map.Map (KeyHash 'StakePool) Coin
    (Map (KeyHash 'StakePool) Coin
retiringDeposits, Map (KeyHash 'StakePool) Coin
remainingDeposits) =
      (KeyHash 'StakePool -> Coin -> Bool)
-> Map (KeyHash 'StakePool) Coin
-> (Map (KeyHash 'StakePool) Coin, Map (KeyHash 'StakePool) Coin)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\KeyHash 'StakePool
k Coin
_ -> KeyHash 'StakePool -> Set (KeyHash 'StakePool) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member KeyHash 'StakePool
k Set (KeyHash 'StakePool)
retired) (PState era -> Map (KeyHash 'StakePool) Coin
forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits PState era
ps)
    rewardAccounts :: Map.Map (KeyHash 'StakePool) RewardAccount
    rewardAccounts :: Map (KeyHash 'StakePool) RewardAccount
rewardAccounts = (PoolParams -> RewardAccount)
-> Map (KeyHash 'StakePool) PoolParams
-> Map (KeyHash 'StakePool) RewardAccount
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map PoolParams -> RewardAccount
ppRewardAccount (Map (KeyHash 'StakePool) PoolParams
 -> Map (KeyHash 'StakePool) RewardAccount)
-> Map (KeyHash 'StakePool) PoolParams
-> Map (KeyHash 'StakePool) RewardAccount
forall a b. (a -> b) -> a -> b
$ Exp (Map (KeyHash 'StakePool) PoolParams)
-> Map (KeyHash 'StakePool) PoolParams
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool)
retired Set (KeyHash 'StakePool)
-> Map (KeyHash 'StakePool) PoolParams
-> Exp (Map (KeyHash 'StakePool) PoolParams)
forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
◁ PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
ps)
    rewardAccounts_ ::
      Map.Map (KeyHash 'StakePool) (RewardAccount, Coin)
    rewardAccounts_ :: Map (KeyHash 'StakePool) (RewardAccount, Coin)
rewardAccounts_ = (RewardAccount -> Coin -> (RewardAccount, Coin))
-> Map (KeyHash 'StakePool) RewardAccount
-> Map (KeyHash 'StakePool) Coin
-> Map (KeyHash 'StakePool) (RewardAccount, Coin)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (,) Map (KeyHash 'StakePool) RewardAccount
rewardAccounts Map (KeyHash 'StakePool) Coin
retiringDeposits
    rewardAccounts' :: Map.Map RewardAccount Coin
    rewardAccounts' :: Map RewardAccount Coin
rewardAccounts' =
      (Coin -> Coin -> Coin)
-> [(RewardAccount, Coin)] -> Map RewardAccount Coin
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
(<+>)
        ([(RewardAccount, Coin)] -> Map RewardAccount Coin)
-> (Map (KeyHash 'StakePool) (RewardAccount, Coin)
    -> [(RewardAccount, Coin)])
-> Map (KeyHash 'StakePool) (RewardAccount, Coin)
-> Map RewardAccount Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (KeyHash 'StakePool) (RewardAccount, Coin)
-> [(RewardAccount, Coin)]
forall k a. Map k a -> [a]
Map.elems
        (Map (KeyHash 'StakePool) (RewardAccount, Coin)
 -> Map RewardAccount Coin)
-> Map (KeyHash 'StakePool) (RewardAccount, Coin)
-> Map RewardAccount Coin
forall a b. (a -> b) -> a -> b
$ Map (KeyHash 'StakePool) (RewardAccount, Coin)
rewardAccounts_
    refunds :: Map.Map (Credential 'Staking) Coin
    mRefunds :: Map.Map (Credential 'Staking) Coin
    (Map (Credential 'Staking) Coin
refunds, Map (Credential 'Staking) Coin
mRefunds) =
      (Credential 'Staking -> Coin -> Bool)
-> Map (Credential 'Staking) Coin
-> (Map (Credential 'Staking) Coin, Map (Credential 'Staking) Coin)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
        (\Credential 'Staking
k Coin
_ -> Credential 'Staking -> UView (Credential 'Staking) RDPair -> Bool
forall k v. k -> UView k v -> Bool
UM.member Credential 'Staking
k (DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
ds)) -- (k ∈ dom (rewards ds))
        ((RewardAccount -> Credential 'Staking)
-> Map RewardAccount Coin -> Map (Credential 'Staking) Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAccount -> Credential 'Staking
raCredential Map RewardAccount Coin
rewardAccounts')
    refunded :: Coin
refunded = 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 Map (Credential 'Staking) Coin
refunds
    unclaimed :: Coin
unclaimed = 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 Map (Credential 'Staking) Coin
mRefunds

  Event (ShelleyPOOLREAP era)
-> Rule (ShelleyPOOLREAP era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (ShelleyPOOLREAP era)
 -> Rule (ShelleyPOOLREAP era) 'Transition ())
-> Event (ShelleyPOOLREAP era)
-> Rule (ShelleyPOOLREAP era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    let rewardAccountsWithPool :: Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
rewardAccountsWithPool =
          (Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
 -> KeyHash 'StakePool
 -> (RewardAccount, Coin)
 -> Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin))
-> Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
-> Map (KeyHash 'StakePool) (RewardAccount, Coin)
-> Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey'
            ( \Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
acc KeyHash 'StakePool
sp (RewardAccount
ra, Coin
coin) ->
                (Map (KeyHash 'StakePool) Coin
 -> Map (KeyHash 'StakePool) Coin -> Map (KeyHash 'StakePool) Coin)
-> Credential 'Staking
-> Map (KeyHash 'StakePool) Coin
-> Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
-> Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ((Coin -> Coin -> Coin)
-> Map (KeyHash 'StakePool) Coin
-> Map (KeyHash 'StakePool) Coin
-> Map (KeyHash 'StakePool) Coin
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
(<>)) (RewardAccount -> Credential 'Staking
raCredential RewardAccount
ra) (KeyHash 'StakePool -> Coin -> Map (KeyHash 'StakePool) Coin
forall k a. k -> a -> Map k a
Map.singleton KeyHash 'StakePool
sp Coin
coin) Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
acc
            )
            Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
forall k a. Map k a
Map.empty
            Map (KeyHash 'StakePool) (RewardAccount, Coin)
rewardAccounts_
        (Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
refundPools', Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
unclaimedPools') =
          (Credential 'Staking -> Map (KeyHash 'StakePool) Coin -> Bool)
-> Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
-> (Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin),
    Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
            (\Credential 'Staking
k Map (KeyHash 'StakePool) Coin
_ -> Credential 'Staking -> UView (Credential 'Staking) RDPair -> Bool
forall k v. k -> UView k v -> Bool
UM.member Credential 'Staking
k (DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
ds)) -- (k ∈ dom (rewards ds))
            Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
rewardAccountsWithPool
     in RetiredPools
          { refundPools :: Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
refundPools = Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
refundPools'
          , unclaimedPools :: Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
unclaimedPools = Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
unclaimedPools'
          , epochNo :: EpochNo
epochNo = EpochNo
Signal (ShelleyPOOLREAP era)
e
          }
  ShelleyPoolreapState era
-> F (Clause (ShelleyPOOLREAP era) 'Transition)
     (ShelleyPoolreapState era)
forall a. a -> F (Clause (ShelleyPOOLREAP era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShelleyPoolreapState era
 -> F (Clause (ShelleyPOOLREAP era) 'Transition)
      (ShelleyPoolreapState era))
-> ShelleyPoolreapState era
-> F (Clause (ShelleyPOOLREAP era) 'Transition)
     (ShelleyPoolreapState era)
forall a b. (a -> b) -> a -> b
$
    UTxOState era
-> ChainAccountState -> CertState era -> ShelleyPoolreapState era
forall era.
UTxOState era
-> ChainAccountState -> CertState era -> ShelleyPoolreapState era
PoolreapState
      UTxOState era
us {utxosDeposited = utxosDeposited us <-> (unclaimed <+> refunded)}
      ChainAccountState
a {casTreasury = casTreasury a <+> unclaimed}
      ( CertState era
cs
          CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (DState era -> Identity (DState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Identity (DState era))
 -> CertState era -> Identity (CertState era))
-> ((UMap -> Identity UMap) -> DState era -> Identity (DState era))
-> (UMap -> Identity UMap)
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Identity UMap) -> DState era -> Identity (DState era)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL
            ((UMap -> Identity UMap)
 -> CertState era -> Identity (CertState era))
-> (UMap -> UMap) -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ( \UMap
uni ->
                   UMap -> UView (Credential 'Staking) (KeyHash 'StakePool)
SPoolUView (UMap -> UView (Credential 'Staking) RDPair
RewDepUView UMap
uni UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) (CompactForm Coin) -> UMap
UM.∪+ (Coin -> CompactForm Coin)
-> Map (Credential 'Staking) Coin
-> Map (Credential 'Staking) (CompactForm Coin)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
Coin -> CompactForm Coin
compactCoinOrError Map (Credential 'Staking) Coin
refunds) UView (Credential 'Staking) (KeyHash 'StakePool)
-> Set (KeyHash 'StakePool) -> UMap
forall k v. UView k v -> Set v -> UMap
UM.⋫ Set (KeyHash 'StakePool)
retired
               )
          CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (PState era -> Identity (PState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era -> Identity (PState era))
 -> CertState era -> Identity (CertState era))
-> ((Map (KeyHash 'StakePool) PoolParams
     -> Identity (Map (KeyHash 'StakePool) PoolParams))
    -> PState era -> Identity (PState era))
-> (Map (KeyHash 'StakePool) PoolParams
    -> Identity (Map (KeyHash 'StakePool) PoolParams))
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) PoolParams
 -> Identity (Map (KeyHash 'StakePool) PoolParams))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) PoolParams
 -> f (Map (KeyHash 'StakePool) PoolParams))
-> PState era -> f (PState era)
psStakePoolParamsL ((Map (KeyHash 'StakePool) PoolParams
  -> Identity (Map (KeyHash 'StakePool) PoolParams))
 -> CertState era -> Identity (CertState era))
-> (Map (KeyHash 'StakePool) PoolParams
    -> Map (KeyHash 'StakePool) PoolParams)
-> CertState era
-> CertState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Exp (Map (KeyHash 'StakePool) PoolParams)
-> Map (KeyHash 'StakePool) PoolParams
forall s t. Embed s t => Exp t -> s
eval (Exp (Map (KeyHash 'StakePool) PoolParams)
 -> Map (KeyHash 'StakePool) PoolParams)
-> (Map (KeyHash 'StakePool) PoolParams
    -> Exp (Map (KeyHash 'StakePool) PoolParams))
-> Map (KeyHash 'StakePool) PoolParams
-> Map (KeyHash 'StakePool) PoolParams
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (KeyHash 'StakePool)
retired Set (KeyHash 'StakePool)
-> Map (KeyHash 'StakePool) PoolParams
-> Exp (Map (KeyHash 'StakePool) PoolParams)
forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
⋪))
          CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (PState era -> Identity (PState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era -> Identity (PState era))
 -> CertState era -> Identity (CertState era))
-> ((Map (KeyHash 'StakePool) PoolParams
     -> Identity (Map (KeyHash 'StakePool) PoolParams))
    -> PState era -> Identity (PState era))
-> (Map (KeyHash 'StakePool) PoolParams
    -> Identity (Map (KeyHash 'StakePool) PoolParams))
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) PoolParams
 -> Identity (Map (KeyHash 'StakePool) PoolParams))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) PoolParams
 -> f (Map (KeyHash 'StakePool) PoolParams))
-> PState era -> f (PState era)
psFutureStakePoolParamsL ((Map (KeyHash 'StakePool) PoolParams
  -> Identity (Map (KeyHash 'StakePool) PoolParams))
 -> CertState era -> Identity (CertState era))
-> (Map (KeyHash 'StakePool) PoolParams
    -> Map (KeyHash 'StakePool) PoolParams)
-> CertState era
-> CertState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Exp (Map (KeyHash 'StakePool) PoolParams)
-> Map (KeyHash 'StakePool) PoolParams
forall s t. Embed s t => Exp t -> s
eval (Exp (Map (KeyHash 'StakePool) PoolParams)
 -> Map (KeyHash 'StakePool) PoolParams)
-> (Map (KeyHash 'StakePool) PoolParams
    -> Exp (Map (KeyHash 'StakePool) PoolParams))
-> Map (KeyHash 'StakePool) PoolParams
-> Map (KeyHash 'StakePool) PoolParams
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (KeyHash 'StakePool)
retired Set (KeyHash 'StakePool)
-> Map (KeyHash 'StakePool) PoolParams
-> Exp (Map (KeyHash 'StakePool) PoolParams)
forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
⋪))
          CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (PState era -> Identity (PState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era -> Identity (PState era))
 -> CertState era -> Identity (CertState era))
-> ((Map (KeyHash 'StakePool) EpochNo
     -> Identity (Map (KeyHash 'StakePool) EpochNo))
    -> PState era -> Identity (PState era))
-> (Map (KeyHash 'StakePool) EpochNo
    -> Identity (Map (KeyHash 'StakePool) EpochNo))
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) EpochNo
 -> Identity (Map (KeyHash 'StakePool) EpochNo))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) EpochNo
 -> f (Map (KeyHash 'StakePool) EpochNo))
-> PState era -> f (PState era)
psRetiringL ((Map (KeyHash 'StakePool) EpochNo
  -> Identity (Map (KeyHash 'StakePool) EpochNo))
 -> CertState era -> Identity (CertState era))
-> (Map (KeyHash 'StakePool) EpochNo
    -> Map (KeyHash 'StakePool) EpochNo)
-> CertState era
-> CertState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Exp (Map (KeyHash 'StakePool) EpochNo)
-> Map (KeyHash 'StakePool) EpochNo
forall s t. Embed s t => Exp t -> s
eval (Exp (Map (KeyHash 'StakePool) EpochNo)
 -> Map (KeyHash 'StakePool) EpochNo)
-> (Map (KeyHash 'StakePool) EpochNo
    -> Exp (Map (KeyHash 'StakePool) EpochNo))
-> Map (KeyHash 'StakePool) EpochNo
-> Map (KeyHash 'StakePool) EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (KeyHash 'StakePool)
retired Set (KeyHash 'StakePool)
-> Map (KeyHash 'StakePool) EpochNo
-> Exp (Map (KeyHash 'StakePool) EpochNo)
forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
⋪))
          CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (PState era -> Identity (PState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era -> Identity (PState era))
 -> CertState era -> Identity (CertState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Identity (Map (KeyHash 'StakePool) Coin))
    -> PState era -> Identity (PState era))
-> (Map (KeyHash 'StakePool) Coin
    -> Identity (Map (KeyHash 'StakePool) Coin))
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) Coin
 -> Identity (Map (KeyHash 'StakePool) Coin))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) Coin
 -> f (Map (KeyHash 'StakePool) Coin))
-> PState era -> f (PState era)
psDepositsL ((Map (KeyHash 'StakePool) Coin
  -> Identity (Map (KeyHash 'StakePool) Coin))
 -> CertState era -> Identity (CertState era))
-> Map (KeyHash 'StakePool) Coin -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map (KeyHash 'StakePool) Coin
remainingDeposits
      )

renderPoolReapViolation ::
  ( EraGov era
  , State t ~ ShelleyPoolreapState era
  , EraCertState era
  ) =>
  AssertionViolation t ->
  String
renderPoolReapViolation :: forall era t.
(EraGov era, State t ~ ShelleyPoolreapState era,
 EraCertState era) =>
AssertionViolation t -> String
renderPoolReapViolation
  AssertionViolation {String
avSTS :: String
avSTS :: forall sts. AssertionViolation sts -> String
avSTS, String
avMsg :: String
avMsg :: forall sts. AssertionViolation sts -> String
avMsg, avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx = TRC (Environment t
_, State t
poolreapst, Signal t
_)} =
    let obligations :: Obligations
obligations =
          CertState era -> GovState era -> Obligations
forall era.
(EraGov era, EraCertState era) =>
CertState era -> GovState era -> Obligations
allObligations (ShelleyPoolreapState era -> CertState era
forall era. ShelleyPoolreapState era -> CertState era
prCertState State t
ShelleyPoolreapState era
poolreapst) (ShelleyPoolreapState era -> UTxOState era
forall era. ShelleyPoolreapState era -> UTxOState era
prUTxOSt State t
ShelleyPoolreapState era
poolreapst UTxOState era
-> Getting (GovState era) (UTxOState era) (GovState era)
-> GovState era
forall s a. s -> Getting a s a -> a
^. Getting (GovState era) (UTxOState era) (GovState era)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL)
     in String
"\n\nAssertionViolation ("
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avSTS
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")\n   "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avMsg
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\npot (utxosDeposited) = "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Coin -> String
forall a. Show a => a -> String
show (UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosDeposited (ShelleyPoolreapState era -> UTxOState era
forall era. ShelleyPoolreapState era -> UTxOState era
prUTxOSt State t
ShelleyPoolreapState era
poolreapst))
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Obligations -> String
forall a. Show a => a -> String
show Obligations
obligations