{-# 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, CompactForm)
import Cardano.Ledger.Compactible (fromCompact)
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.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) (CompactForm Coin))
refundPools ::
      Map.Map (Credential 'Staking) (Map.Map (KeyHash 'StakePool) (CompactForm Coin))
  , forall era.
ShelleyPoolreapEvent era
-> Map
     (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
unclaimedPools ::
      Map.Map (Credential 'Staking) (Map.Map (KeyHash 'StakePool) (CompactForm 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 accountsCount :: ShelleyPoolreapState era -> Int
accountsCount ShelleyPoolreapState era
prState =
                  Map (Credential 'Staking) (AccountState era) -> Int
forall k a. Map k a -> Int
Map.size (ShelleyPoolreapState era -> CertState era
forall era. ShelleyPoolreapState era -> CertState era
prCertState ShelleyPoolreapState era
prState CertState era
-> Getting
     (Map (Credential 'Staking) (AccountState era))
     (CertState era)
     (Map (Credential 'Staking) (AccountState era))
-> Map (Credential 'Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (DState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (DState era))
-> CertState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era
  -> Const
       (Map (Credential 'Staking) (AccountState era)) (DState era))
 -> CertState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (CertState era))
-> ((Map (Credential 'Staking) (AccountState era)
     -> Const
          (Map (Credential 'Staking) (AccountState era))
          (Map (Credential 'Staking) (AccountState era)))
    -> DState era
    -> Const
         (Map (Credential 'Staking) (AccountState era)) (DState era))
-> Getting
     (Map (Credential 'Staking) (AccountState era))
     (CertState era)
     (Map (Credential 'Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential 'Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (DState era))
-> ((Map (Credential 'Staking) (AccountState era)
     -> Const
          (Map (Credential 'Staking) (AccountState era))
          (Map (Credential 'Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential 'Staking) (AccountState era)) (Accounts era))
-> (Map (Credential 'Staking) (AccountState era)
    -> Const
         (Map (Credential 'Staking) (AccountState era))
         (Map (Credential 'Staking) (AccountState era)))
-> DState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) (AccountState era)
 -> Const
      (Map (Credential 'Staking) (AccountState era))
      (Map (Credential 'Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
accountsMapL)
             in ShelleyPoolreapState era -> Int
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 -> Int
accountsCount State (ShelleyPOOLREAP era)
ShelleyPoolreapState era
st Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== ShelleyPoolreapState era -> Int
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 -> Int
accountsCount 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) (CompactForm Coin)
    (Map (KeyHash 'StakePool) (CompactForm Coin)
retiringDeposits, Map (KeyHash 'StakePool) (CompactForm Coin)
remainingDeposits) =
      (KeyHash 'StakePool -> CompactForm Coin -> Bool)
-> Map (KeyHash 'StakePool) (CompactForm Coin)
-> (Map (KeyHash 'StakePool) (CompactForm Coin),
    Map (KeyHash 'StakePool) (CompactForm Coin))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\KeyHash 'StakePool
k CompactForm 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) (CompactForm Coin)
forall era.
PState era -> Map (KeyHash 'StakePool) (CompactForm Coin)
psDeposits PState era
ps)
    -- collect all accounts for stake pools that will retire
    retiredStakePoolAccounts :: Map.Map (KeyHash 'StakePool) RewardAccount
    retiredStakePoolAccounts :: Map (KeyHash 'StakePool) RewardAccount
retiredStakePoolAccounts = (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)
    retiredStakePoolAccountsWithRefund :: Map.Map (KeyHash 'StakePool) (RewardAccount, CompactForm Coin)
    retiredStakePoolAccountsWithRefund :: Map (KeyHash 'StakePool) (RewardAccount, CompactForm Coin)
retiredStakePoolAccountsWithRefund = (RewardAccount
 -> CompactForm Coin -> (RewardAccount, CompactForm Coin))
-> Map (KeyHash 'StakePool) RewardAccount
-> Map (KeyHash 'StakePool) (CompactForm Coin)
-> Map (KeyHash 'StakePool) (RewardAccount, CompactForm 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
retiredStakePoolAccounts Map (KeyHash 'StakePool) (CompactForm Coin)
retiringDeposits
    -- collect all of the potential refunds
    accountRefunds :: Map.Map (Credential 'Staking) (CompactForm Coin)
    accountRefunds :: Map (Credential 'Staking) (CompactForm Coin)
accountRefunds =
      (CompactForm Coin -> CompactForm Coin -> CompactForm Coin)
-> [(Credential 'Staking, CompactForm Coin)]
-> Map (Credential 'Staking) (CompactForm Coin)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith CompactForm Coin -> CompactForm Coin -> CompactForm Coin
forall a. Semigroup a => a -> a -> a
(<>) ([(Credential 'Staking, CompactForm Coin)]
 -> Map (Credential 'Staking) (CompactForm Coin))
-> [(Credential 'Staking, CompactForm Coin)]
-> Map (Credential 'Staking) (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$
        [(RewardAccount -> Credential 'Staking
raCredential RewardAccount
k, CompactForm Coin
v) | (RewardAccount
k, CompactForm Coin
v) <- Map (KeyHash 'StakePool) (RewardAccount, CompactForm Coin)
-> [(RewardAccount, CompactForm Coin)]
forall k a. Map k a -> [a]
Map.elems Map (KeyHash 'StakePool) (RewardAccount, CompactForm Coin)
retiredStakePoolAccountsWithRefund]
    accounts :: Accounts era
accounts = DState era
ds DState era
-> Getting (Accounts era) (DState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. Getting (Accounts era) (DState era) (Accounts era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL
    -- figure out whcich deposits can be refunded and which ones will be deposited into the treasury
    -- as unclaimed
    refunds, unclaimedDeposits :: Map.Map (Credential 'Staking) (CompactForm Coin)
    (Map (Credential 'Staking) (CompactForm Coin)
refunds, Map (Credential 'Staking) (CompactForm Coin)
unclaimedDeposits) =
      (Credential 'Staking -> CompactForm Coin -> Bool)
-> Map (Credential 'Staking) (CompactForm Coin)
-> (Map (Credential 'Staking) (CompactForm Coin),
    Map (Credential 'Staking) (CompactForm Coin))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
        (\Credential 'Staking
stakeCred CompactForm Coin
_ -> Credential 'Staking -> Accounts era -> Bool
forall era.
EraAccounts era =>
Credential 'Staking -> Accounts era -> Bool
isAccountRegistered Credential 'Staking
stakeCred Accounts era
accounts) -- (k ∈ dom (rewards ds))
        Map (Credential 'Staking) (CompactForm Coin)
accountRefunds
    refunded :: CompactForm Coin
refunded = Map (Credential 'Staking) (CompactForm Coin) -> CompactForm Coin
forall m. Monoid m => Map (Credential 'Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) (CompactForm Coin)
refunds
    unclaimed :: CompactForm Coin
unclaimed = Map (Credential 'Staking) (CompactForm Coin) -> CompactForm Coin
forall m. Monoid m => Map (Credential 'Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) (CompactForm Coin)
unclaimedDeposits

  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) (CompactForm Coin))
rewardAccountsWithPool =
          (Map
   (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
 -> KeyHash 'StakePool
 -> (RewardAccount, CompactForm Coin)
 -> Map
      (Credential 'Staking)
      (Map (KeyHash 'StakePool) (CompactForm Coin)))
-> Map
     (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
-> Map (KeyHash 'StakePool) (RewardAccount, CompactForm Coin)
-> Map
     (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey'
            ( \Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
acc KeyHash 'StakePool
sp (RewardAccount
ra, CompactForm Coin
coin) ->
                (Map (KeyHash 'StakePool) (CompactForm Coin)
 -> Map (KeyHash 'StakePool) (CompactForm Coin)
 -> Map (KeyHash 'StakePool) (CompactForm Coin))
-> Credential 'Staking
-> Map (KeyHash 'StakePool) (CompactForm Coin)
-> Map
     (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
-> Map
     (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ((CompactForm Coin -> CompactForm Coin -> CompactForm Coin)
-> Map (KeyHash 'StakePool) (CompactForm Coin)
-> Map (KeyHash 'StakePool) (CompactForm Coin)
-> Map (KeyHash 'StakePool) (CompactForm Coin)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith CompactForm Coin -> CompactForm Coin -> CompactForm Coin
forall a. Semigroup a => a -> a -> a
(<>)) (RewardAccount -> Credential 'Staking
raCredential RewardAccount
ra) (KeyHash 'StakePool
-> CompactForm Coin -> Map (KeyHash 'StakePool) (CompactForm Coin)
forall k a. k -> a -> Map k a
Map.singleton KeyHash 'StakePool
sp CompactForm Coin
coin) Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
acc
            )
            Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
forall k a. Map k a
Map.empty
            Map (KeyHash 'StakePool) (RewardAccount, CompactForm Coin)
retiredStakePoolAccountsWithRefund
        (Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
refundPools', Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
unclaimedPools') =
          (Credential 'Staking
 -> Map (KeyHash 'StakePool) (CompactForm Coin) -> Bool)
-> Map
     (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
-> (Map
      (Credential 'Staking)
      (Map (KeyHash 'StakePool) (CompactForm Coin)),
    Map
      (Credential 'Staking)
      (Map (KeyHash 'StakePool) (CompactForm Coin)))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
            (\Credential 'Staking
cred Map (KeyHash 'StakePool) (CompactForm Coin)
_ -> Credential 'Staking -> Accounts era -> Bool
forall era.
EraAccounts era =>
Credential 'Staking -> Accounts era -> Bool
isAccountRegistered Credential 'Staking
cred Accounts era
accounts) -- (k ∈ dom (rewards ds))
            Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
rewardAccountsWithPool
     in RetiredPools
          { refundPools :: Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
refundPools = Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
refundPools'
          , unclaimedPools :: Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm Coin))
unclaimedPools = Map
  (Credential 'Staking) (Map (KeyHash 'StakePool) (CompactForm 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 <-> fromCompact (unclaimed <> refunded)}
      ChainAccountState
a {casTreasury = casTreasury a <+> fromCompact 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))
-> ((Accounts era -> Identity (Accounts era))
    -> DState era -> Identity (DState era))
-> (Accounts era -> Identity (Accounts era))
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Identity (Accounts era))
-> DState era -> Identity (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL
            ((Accounts era -> Identity (Accounts era))
 -> CertState era -> Identity (CertState era))
-> (Accounts era -> Accounts era) -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Set (KeyHash 'StakePool) -> Accounts era -> Accounts era
forall era.
EraAccounts era =>
Set (KeyHash 'StakePool) -> Accounts era -> Accounts era
removeStakePoolDelegations Set (KeyHash 'StakePool)
retired (Accounts era -> Accounts era)
-> (Accounts era -> Accounts era) -> Accounts era -> Accounts era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Credential 'Staking) (CompactForm Coin)
-> Accounts era -> Accounts era
forall era.
EraAccounts era =>
Map (Credential 'Staking) (CompactForm Coin)
-> Accounts era -> Accounts era
addToBalanceAccounts Map (Credential 'Staking) (CompactForm Coin)
refunds
          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) (CompactForm Coin)
     -> Identity (Map (KeyHash 'StakePool) (CompactForm Coin)))
    -> PState era -> Identity (PState era))
-> (Map (KeyHash 'StakePool) (CompactForm Coin)
    -> Identity (Map (KeyHash 'StakePool) (CompactForm Coin)))
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) (CompactForm Coin)
 -> Identity (Map (KeyHash 'StakePool) (CompactForm Coin)))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) (CompactForm Coin)
 -> f (Map (KeyHash 'StakePool) (CompactForm Coin)))
-> PState era -> f (PState era)
psDepositsCompactL ((Map (KeyHash 'StakePool) (CompactForm Coin)
  -> Identity (Map (KeyHash 'StakePool) (CompactForm Coin)))
 -> CertState era -> Identity (CertState era))
-> Map (KeyHash 'StakePool) (CompactForm Coin)
-> CertState era
-> CertState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map (KeyHash 'StakePool) (CompactForm 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