{-# 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 (..),
  ShelleyPoolreapEnv (..),
  PredicateFailure,
  ShelleyPoolreapPredFailure,
)
where

import Cardano.Ledger.Address (RewardAccount, raCredential)
import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.CertState (VState)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyHash, KeyRole (StakePool, Staking))
import Cardano.Ledger.PoolParams (ppRewardAccount)
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyPOOLREAP)
import Cardano.Ledger.Shelley.Governance (EraGov)
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  CertState (..),
  DState (..),
  PState (..),
  UTxOState (..),
  allObligations,
  rewards,
  utxosGovStateL,
 )
import Cardano.Ledger.Shelley.LedgerState.Types (potEqualsObligation)
import Cardano.Ledger.Slot (EpochNo (..))
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 -> AccountState
prAccountState :: AccountState
  , forall era. ShelleyPoolreapState era -> DState era
prDState :: DState era
  , forall era. ShelleyPoolreapState era -> PState era
prPState :: PState era
  }

newtype ShelleyPoolreapEnv era = ShelleyPoolreapEnv
  { forall era. ShelleyPoolreapEnv era -> VState era
speVState :: VState era
  -- ^ This enviroment field is only needed for assertions.
  }

deriving stock instance Eq (PParams era) => Eq (ShelleyPoolreapEnv era)

deriving stock instance Show (PParams era) => Show (ShelleyPoolreapEnv era)

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

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

instance NFData (ShelleyPoolreapPredFailure era)

data ShelleyPoolreapEvent era = RetiredPools
  { forall era.
ShelleyPoolreapEvent era
-> Map
     (Credential 'Staking (EraCrypto era))
     (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
refundPools ::
      Map.Map (Credential 'Staking (EraCrypto era)) (Map.Map (KeyHash 'StakePool (EraCrypto era)) Coin)
  , forall era.
ShelleyPoolreapEvent era
-> Map
     (Credential 'Staking (EraCrypto era))
     (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
unclaimedPools ::
      Map.Map (Credential 'Staking (EraCrypto era)) (Map.Map (KeyHash 'StakePool (EraCrypto era)) Coin)
  , forall era. ShelleyPoolreapEvent era -> EpochNo
epochNo :: EpochNo
  }
  deriving (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
$cto :: forall era x.
Rep (ShelleyPoolreapEvent era) x -> ShelleyPoolreapEvent era
$cfrom :: forall era x.
ShelleyPoolreapEvent era -> Rep (ShelleyPoolreapEvent era) x
Generic)

deriving instance Eq (ShelleyPoolreapEvent era)

instance NFData (ShelleyPoolreapEvent era)

instance NoThunks (ShelleyPoolreapPredFailure era)

instance Default (UTxOState era) => Default (ShelleyPoolreapState era) where
  def :: ShelleyPoolreapState era
def = forall era.
UTxOState era
-> AccountState
-> DState era
-> PState era
-> ShelleyPoolreapState era
PoolreapState forall a. Default a => a
def forall a. Default a => a
def forall a. Default a => a
def forall a. Default a => a
def

type instance EraRuleEvent "POOLREAP" (ShelleyEra c) = ShelleyPoolreapEvent (ShelleyEra c)

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

  renderAssertionViolation :: AssertionViolation (ShelleyPOOLREAP era) -> String
renderAssertionViolation = forall era t.
(EraGov era, Environment t ~ ShelleyPoolreapEnv era,
 State t ~ ShelleyPoolreapState era) =>
AssertionViolation t -> String
renderPoolReapViolation
  assertions :: [Assertion (ShelleyPOOLREAP era)]
assertions =
    [ forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must equal obligation (PoolReap)"
        ( \(TRC (Environment (ShelleyPOOLREAP era)
env, State (ShelleyPOOLREAP era)
_, Signal (ShelleyPOOLREAP era)
_)) State (ShelleyPOOLREAP era)
st ->
            forall era. EraGov era => CertState era -> UTxOState era -> Bool
potEqualsObligation
              (forall era. VState era -> PState era -> DState era -> CertState era
CertState (forall era. ShelleyPoolreapEnv era -> VState era
speVState Environment (ShelleyPOOLREAP era)
env) (forall era. ShelleyPoolreapState era -> PState era
prPState State (ShelleyPOOLREAP era)
st) (forall era. ShelleyPoolreapState era -> DState era
prDState State (ShelleyPOOLREAP era)
st))
              (forall era. ShelleyPoolreapState era -> UTxOState era
prUTxOSt State (ShelleyPOOLREAP era)
st)
        )
    , 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
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
r = forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ShelleyPoolreapState era -> DState era
prDState
             in forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {era}.
ShelleyPoolreapState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
r State (ShelleyPOOLREAP era)
st) forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {era}.
ShelleyPoolreapState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
r State (ShelleyPOOLREAP era)
st')
        )
    ]

poolReapTransition :: forall era. TransitionRule (ShelleyPOOLREAP era)
poolReapTransition :: forall era. TransitionRule (ShelleyPOOLREAP era)
poolReapTransition = do
  TRC (Environment (ShelleyPOOLREAP era)
_, PoolreapState UTxOState era
us AccountState
a DState era
ds PState era
ps, Signal (ShelleyPOOLREAP era)
e) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

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

  forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$
    let rewardAccountsWithPool :: Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
rewardAccountsWithPool =
          forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey'
            ( \Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
acc KeyHash 'StakePool (EraCrypto era)
sp (RewardAccount (EraCrypto era)
ra, Coin
coin) ->
                forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>)) (forall c. RewardAccount c -> Credential 'Staking c
raCredential RewardAccount (EraCrypto era)
ra) (forall k a. k -> a -> Map k a
Map.singleton KeyHash 'StakePool (EraCrypto era)
sp Coin
coin) Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
acc
            )
            forall k a. Map k a
Map.empty
            Map
  (KeyHash 'StakePool (EraCrypto era))
  (RewardAccount (EraCrypto era), Coin)
rewardAccounts_
        (Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
refundPools', Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
unclaimedPools') =
          forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
            (\Credential 'Staking (EraCrypto era)
k Map (KeyHash 'StakePool (EraCrypto era)) Coin
_ -> forall k c v. k -> UView c k v -> Bool
UM.member Credential 'Staking (EraCrypto era)
k (forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards DState era
ds)) -- (k ∈ dom (rewards ds))
            Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
rewardAccountsWithPool
     in RetiredPools
          { refundPools :: Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
refundPools = Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
refundPools'
          , unclaimedPools :: Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
unclaimedPools = Map
  (Credential 'Staking (EraCrypto era))
  (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
unclaimedPools'
          , epochNo :: EpochNo
epochNo = Signal (ShelleyPOOLREAP era)
e
          }
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall era.
UTxOState era
-> AccountState
-> DState era
-> PState era
-> ShelleyPoolreapState era
PoolreapState
      UTxOState era
us {utxosDeposited :: Coin
utxosDeposited = forall era. UTxOState era -> Coin
utxosDeposited UTxOState era
us forall t. Val t => t -> t -> t
<-> (Coin
unclaimed forall t. Val t => t -> t -> t
<+> Coin
refunded)}
      AccountState
a {asTreasury :: Coin
asTreasury = AccountState -> Coin
asTreasury AccountState
a forall t. Val t => t -> t -> t
<+> Coin
unclaimed}
      ( let u0 :: UMap (EraCrypto era)
u0 = forall era. DState era -> UMap (EraCrypto era)
dsUnified DState era
ds
            u1 :: UMap (EraCrypto era)
u1 = forall c. UMap c -> UView c (Credential 'Staking c) RDPair
RewDepUView UMap (EraCrypto era)
u0 forall c.
UView c (Credential 'Staking c) RDPair
-> Map (Credential 'Staking c) (CompactForm Coin) -> UMap c
UM.∪+ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
compactCoinOrError Map (Credential 'Staking (EraCrypto era)) Coin
refunds
            u2 :: UMap (EraCrypto era)
u2 = forall c.
UMap c -> UView c (Credential 'Staking c) (KeyHash 'StakePool c)
SPoolUView UMap (EraCrypto era)
u1 forall c k v. UView c k v -> Set v -> UMap c
UM.⋫ Set (KeyHash 'StakePool (EraCrypto era))
retired
         in DState era
ds {dsUnified :: UMap (EraCrypto era)
dsUnified = UMap (EraCrypto era)
u2}
      )
      PState era
ps
        { psStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams = forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (EraCrypto era))
retired 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)
 forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams PState era
ps)
        , -- TODO: redundant
          psFutureStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psFutureStakePoolParams = forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (EraCrypto era))
retired 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)
 forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psFutureStakePoolParams PState era
ps)
        , psRetiring :: Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psRetiring = forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (EraCrypto era))
retired 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)
 forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psRetiring PState era
ps)
        , psDeposits :: Map (KeyHash 'StakePool (EraCrypto era)) Coin
psDeposits = Map (KeyHash 'StakePool (EraCrypto era)) Coin
remainingDeposits
        }

renderPoolReapViolation ::
  ( EraGov era
  , Environment t ~ ShelleyPoolreapEnv era
  , State t ~ ShelleyPoolreapState era
  ) =>
  AssertionViolation t ->
  String
renderPoolReapViolation :: forall era t.
(EraGov era, Environment t ~ ShelleyPoolreapEnv era,
 State t ~ ShelleyPoolreapState era) =>
AssertionViolation t -> String
renderPoolReapViolation
  AssertionViolation {String
avSTS :: forall sts. AssertionViolation sts -> String
avSTS :: String
avSTS, String
avMsg :: forall sts. AssertionViolation sts -> String
avMsg :: String
avMsg, avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx = TRC (ShelleyPoolreapEnv VState era
vs, State t
poolreapst, Signal t
_)} =
    let certst :: CertState era
certst = forall era. VState era -> PState era -> DState era -> CertState era
CertState VState era
vs (forall era. ShelleyPoolreapState era -> PState era
prPState State t
poolreapst) (forall era. ShelleyPoolreapState era -> DState era
prDState State t
poolreapst)
        obligations :: Obligations
obligations = forall era.
EraGov era =>
CertState era -> GovState era -> Obligations
allObligations CertState era
certst (forall era. ShelleyPoolreapState era -> UTxOState era
prUTxOSt State t
poolreapst forall s a. s -> Getting a s a -> a
^. forall era. Lens' (UTxOState era) (GovState era)
utxosGovStateL)
     in String
"\n\nAssertionViolation ("
          forall a. Semigroup a => a -> a -> a
<> String
avSTS
          forall a. Semigroup a => a -> a -> a
<> String
")\n   "
          forall a. Semigroup a => a -> a -> a
<> String
avMsg
          forall a. Semigroup a => a -> a -> a
<> String
"\npot (utxosDeposited) = "
          forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall era. UTxOState era -> Coin
utxosDeposited (forall era. ShelleyPoolreapState era -> UTxOState era
prUTxOSt State t
poolreapst))
          forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Obligations
obligations