{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.PoolReap
  ( POOLREAP,
    PoolreapEvent (..),
    PoolreapState (..),
    PredicateFailure,
    PoolreapPredicateFailure,
  )
where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Coin (Coin)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Era (Crypto)
import Cardano.Ledger.Keys (KeyHash, KeyRole (StakePool, Staking))
import Cardano.Ledger.Shelley.EpochBoundary (obligation)
import Cardano.Ledger.Shelley.LedgerState
  ( AccountState (..),
    DState (..),
    PState (..),
    UTxOState (..),
    rewards,
  )
import Cardano.Ledger.Shelley.TxBody (RewardAcnt, getRwdCred, _poolRAcnt)
import Cardano.Ledger.Slot (EpochNo (..))
import Cardano.Ledger.UnifiedMap (View (..))
import Cardano.Ledger.Val ((<+>), (<->))
import Control.SetAlgebra (dom, eval, setSingleton, (∈), (⋪), (▷), (◁))
import Control.State.Transition
  ( Assertion (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    tellEvent,
  )
import Data.Default.Class (Default, def)
import Data.Foldable (fold)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Typeable (Typeable)
import qualified Data.UMap as UM
import GHC.Generics (Generic)
import GHC.Records
import NoThunks.Class (NoThunks (..))

data POOLREAP era

data PoolreapState era = PoolreapState
  { PoolreapState era -> UTxOState era
prUTxOSt :: UTxOState era,
    PoolreapState era -> AccountState
prAcnt :: AccountState,
    PoolreapState era -> DState (Crypto era)
prDState :: DState (Crypto era),
    PoolreapState era -> PState (Crypto era)
prPState :: PState (Crypto era)
  }

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

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

data PoolreapEvent era = RetiredPools
  { PoolreapEvent era
-> Map
     (Credential 'Staking (Crypto era))
     (Map (KeyHash 'StakePool (Crypto era)) Coin)
refundPools :: Map.Map (Credential 'Staking (Crypto era)) (Map.Map (KeyHash 'StakePool (Crypto era)) Coin),
    PoolreapEvent era
-> Map
     (Credential 'Staking (Crypto era))
     (Map (KeyHash 'StakePool (Crypto era)) Coin)
unclaimedPools :: Map.Map (Credential 'Staking (Crypto era)) (Map.Map (KeyHash 'StakePool (Crypto era)) Coin),
    PoolreapEvent era -> EpochNo
epochNo :: EpochNo
  }

instance NoThunks (PoolreapPredicateFailure era)

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

instance
  forall era.
  ( Typeable era,
    Default (PoolreapState era),
    HasField "_poolDeposit" (Core.PParams era) Coin,
    HasField "_keyDeposit" (Core.PParams era) Coin
  ) =>
  STS (POOLREAP era)
  where
  type State (POOLREAP era) = PoolreapState era
  type Signal (POOLREAP era) = EpochNo
  type Environment (POOLREAP era) = Core.PParams era
  type BaseM (POOLREAP era) = ShelleyBase
  type PredicateFailure (POOLREAP era) = PoolreapPredicateFailure era
  type Event (POOLREAP era) = PoolreapEvent era
  transitionRules :: [TransitionRule (POOLREAP era)]
transitionRules = [TransitionRule (POOLREAP era)
forall era.
HasField "_poolDeposit" (PParams era) Coin =>
TransitionRule (POOLREAP era)
poolReapTransition]
  assertions :: [Assertion (POOLREAP era)]
assertions =
    [ String
-> (TRC (POOLREAP era) -> State (POOLREAP era) -> Bool)
-> Assertion (POOLREAP era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must equal obligation"
        ( \(TRC (Environment (POOLREAP era)
pp, State (POOLREAP era)
_, Signal (POOLREAP era)
_)) State (POOLREAP era)
st ->
            PParams era
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Coin
forall crypto pp (anymap :: * -> * -> *).
(HasField "_keyDeposit" pp Coin, HasField "_poolDeposit" pp Coin,
 Foldable (anymap (Credential 'Staking crypto))) =>
pp
-> anymap (Credential 'Staking crypto) Coin
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
-> Coin
obligation PParams era
Environment (POOLREAP era)
pp (DState (Crypto era)
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards (DState (Crypto era)
 -> View
      Coin
      (Credential 'Staking (Crypto era))
      (KeyHash 'StakePool (Crypto era))
      Ptr
      (Credential 'Staking (Crypto era))
      Coin)
-> DState (Crypto era)
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall a b. (a -> b) -> a -> b
$ PoolreapState era -> DState (Crypto era)
forall era. PoolreapState era -> DState (Crypto era)
prDState State (POOLREAP era)
PoolreapState era
st) (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams (PState (Crypto era)
 -> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall a b. (a -> b) -> a -> b
$ PoolreapState era -> PState (Crypto era)
forall era. PoolreapState era -> PState (Crypto era)
prPState State (POOLREAP era)
PoolreapState era
st)
              Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited (PoolreapState era -> UTxOState era
forall era. PoolreapState era -> UTxOState era
prUTxOSt State (POOLREAP era)
PoolreapState era
st)
        ),
      String
-> (TRC (POOLREAP era) -> State (POOLREAP era) -> Bool)
-> Assertion (POOLREAP era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"PoolReap may not create or remove reward accounts"
        ( \(TRC (Environment (POOLREAP era)
_, State (POOLREAP era)
st, Signal (POOLREAP era)
_)) State (POOLREAP era)
st' ->
            let r :: PoolreapState era
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
r = DState (Crypto era)
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards (DState (Crypto era)
 -> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin)
-> (PoolreapState era -> DState (Crypto era))
-> PoolreapState era
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PoolreapState era -> DState (Crypto era)
forall era. PoolreapState era -> DState (Crypto era)
prDState
             in View
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
  (Credential 'Staking (Crypto era))
  Coin
-> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PoolreapState era
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall era.
PoolreapState era
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
r State (POOLREAP era)
PoolreapState era
st) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== View
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
  (Credential 'Staking (Crypto era))
  Coin
-> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PoolreapState era
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall era.
PoolreapState era
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
r State (POOLREAP era)
PoolreapState era
st')
        )
    ]

poolReapTransition ::
  forall era.
  HasField "_poolDeposit" (Core.PParams era) Coin =>
  TransitionRule (POOLREAP era)
poolReapTransition :: TransitionRule (POOLREAP era)
poolReapTransition = do
  TRC (Environment (POOLREAP era)
pp, PoolreapState us a ds ps, Signal (POOLREAP era)
e) <- F (Clause (POOLREAP era) 'Transition) (TRC (POOLREAP era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  let retired :: Set (KeyHash 'StakePool (Crypto era))
      retired :: Set (KeyHash 'StakePool (Crypto era))
retired = Exp (Sett (KeyHash 'StakePool (Crypto era)) ())
-> Set (KeyHash 'StakePool (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Exp (Map (KeyHash 'StakePool (Crypto era)) EpochNo)
-> Exp (Sett (KeyHash 'StakePool (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall crypto.
PState crypto -> Map (KeyHash 'StakePool crypto) EpochNo
_retiring PState (Crypto era)
ps Map (KeyHash 'StakePool (Crypto era)) EpochNo
-> Exp (Single EpochNo ())
-> Exp (Map (KeyHash 'StakePool (Crypto era)) 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 (POOLREAP era)
e))
      pr :: Map.Map (KeyHash 'StakePool (Crypto era)) Coin
      pr :: Map (KeyHash 'StakePool (Crypto era)) Coin
pr = (KeyHash 'StakePool (Crypto era) -> Coin)
-> Set (KeyHash 'StakePool (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) Coin
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (Coin -> KeyHash 'StakePool (Crypto era) -> Coin
forall a b. a -> b -> a
const (PParams era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_poolDeposit" PParams era
Environment (POOLREAP era)
pp)) Set (KeyHash 'StakePool (Crypto era))
retired
      rewardAcnts :: Map.Map (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era))
      rewardAcnts :: Map (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era))
rewardAcnts = (PoolParams (Crypto era) -> RewardAcnt (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map PoolParams (Crypto era) -> RewardAcnt (Crypto era)
forall crypto. PoolParams crypto -> RewardAcnt crypto
_poolRAcnt (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
 -> Map (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era))
forall a b. (a -> b) -> a -> b
$ Exp
  (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (Crypto era))
retired Set (KeyHash 'StakePool (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp
     (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
◁ PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams PState (Crypto era)
ps)
      rewardAcnts_ :: Map.Map (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
      rewardAcnts_ :: Map
  (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
rewardAcnts_ = (RewardAcnt (Crypto era)
 -> Coin -> (RewardAcnt (Crypto era), Coin))
-> Map (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) Coin
-> Map
     (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), 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 (Crypto era)) (RewardAcnt (Crypto era))
rewardAcnts Map (KeyHash 'StakePool (Crypto era)) Coin
pr
      rewardAcnts' :: Map.Map (RewardAcnt (Crypto era)) Coin
      rewardAcnts' :: Map (RewardAcnt (Crypto era)) Coin
rewardAcnts' =
        (Coin -> Coin -> Coin)
-> [(RewardAcnt (Crypto era), Coin)]
-> Map (RewardAcnt (Crypto era)) 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
(<+>)
          ([(RewardAcnt (Crypto era), Coin)]
 -> Map (RewardAcnt (Crypto era)) Coin)
-> (Map
      (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
    -> [(RewardAcnt (Crypto era), Coin)])
-> Map
     (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
-> Map (RewardAcnt (Crypto era)) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map
  (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
-> [(RewardAcnt (Crypto era), Coin)]
forall k a. Map k a -> [a]
Map.elems
          (Map
   (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
 -> Map (RewardAcnt (Crypto era)) Coin)
-> Map
     (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
-> Map (RewardAcnt (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ Map
  (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
rewardAcnts_
      refunds :: Map.Map (Credential 'Staking (Crypto era)) Coin
      mRefunds :: Map.Map (Credential 'Staking (Crypto era)) Coin
      (Map (Credential 'Staking (Crypto era)) Coin
refunds, Map (Credential 'Staking (Crypto era)) Coin
mRefunds) =
        (Credential 'Staking (Crypto era) -> Coin -> Bool)
-> Map (Credential 'Staking (Crypto era)) Coin
-> (Map (Credential 'Staking (Crypto era)) Coin,
    Map (Credential 'Staking (Crypto era)) Coin)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
          (\Credential 'Staking (Crypto era)
k Coin
_ -> Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (Credential 'Staking (Crypto era)
k Credential 'Staking (Crypto era)
-> Exp (Sett (Credential 'Staking (Crypto era)) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> Exp (Sett (Credential 'Staking (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (DState (Crypto era)
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards DState (Crypto era)
ds)))
          ((RewardAcnt (Crypto era) -> Credential 'Staking (Crypto era))
-> Map (RewardAcnt (Crypto era)) Coin
-> Map (Credential 'Staking (Crypto era)) Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAcnt (Crypto era) -> Credential 'Staking (Crypto era)
forall crypto. RewardAcnt crypto -> Credential 'Staking crypto
getRwdCred Map (RewardAcnt (Crypto era)) Coin
rewardAcnts')
      refunded :: Coin
refunded = [Coin] -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([Coin] -> Coin) -> [Coin] -> Coin
forall a b. (a -> b) -> a -> b
$ Map (Credential 'Staking (Crypto era)) Coin -> [Coin]
forall k a. Map k a -> [a]
Map.elems Map (Credential 'Staking (Crypto era)) Coin
refunds
      unclaimed :: Coin
unclaimed = [Coin] -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([Coin] -> Coin) -> [Coin] -> Coin
forall a b. (a -> b) -> a -> b
$ Map (Credential 'Staking (Crypto era)) Coin -> [Coin]
forall k a. Map k a -> [a]
Map.elems Map (Credential 'Staking (Crypto era)) Coin
mRefunds

  Event (POOLREAP era) -> Rule (POOLREAP era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (POOLREAP era) -> Rule (POOLREAP era) 'Transition ())
-> Event (POOLREAP era) -> Rule (POOLREAP era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    let rewardAcntsWithPool :: Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
rewardAcntsWithPool =
          (Map
   (Credential 'Staking (Crypto era))
   (Map (KeyHash 'StakePool (Crypto era)) Coin)
 -> KeyHash 'StakePool (Crypto era)
 -> (RewardAcnt (Crypto era), Coin)
 -> Map
      (Credential 'Staking (Crypto era))
      (Map (KeyHash 'StakePool (Crypto era)) Coin))
-> Map
     (Credential 'Staking (Crypto era))
     (Map (KeyHash 'StakePool (Crypto era)) Coin)
-> Map
     (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
-> Map
     (Credential 'Staking (Crypto era))
     (Map (KeyHash 'StakePool (Crypto era)) Coin)
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey'
            ( \Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
acc KeyHash 'StakePool (Crypto era)
sp (RewardAcnt (Crypto era)
ra, Coin
coin) ->
                (Map (KeyHash 'StakePool (Crypto era)) Coin
 -> Map (KeyHash 'StakePool (Crypto era)) Coin
 -> Map (KeyHash 'StakePool (Crypto era)) Coin)
-> Credential 'Staking (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) Coin
-> Map
     (Credential 'Staking (Crypto era))
     (Map (KeyHash 'StakePool (Crypto era)) Coin)
-> Map
     (Credential 'Staking (Crypto era))
     (Map (KeyHash 'StakePool (Crypto era)) 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 (Crypto era)) Coin
-> Map (KeyHash 'StakePool (Crypto era)) Coin
-> Map (KeyHash 'StakePool (Crypto era)) 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
(<>)) (RewardAcnt (Crypto era) -> Credential 'Staking (Crypto era)
forall crypto. RewardAcnt crypto -> Credential 'Staking crypto
getRwdCred RewardAcnt (Crypto era)
ra) (KeyHash 'StakePool (Crypto era)
-> Coin -> Map (KeyHash 'StakePool (Crypto era)) Coin
forall k a. k -> a -> Map k a
Map.singleton KeyHash 'StakePool (Crypto era)
sp Coin
coin) Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
acc
            )
            Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
forall k a. Map k a
Map.empty
            Map
  (KeyHash 'StakePool (Crypto era)) (RewardAcnt (Crypto era), Coin)
rewardAcnts_
        (Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
refundPools', Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
unclaimedPools') =
          (Credential 'Staking (Crypto era)
 -> Map (KeyHash 'StakePool (Crypto era)) Coin -> Bool)
-> Map
     (Credential 'Staking (Crypto era))
     (Map (KeyHash 'StakePool (Crypto era)) Coin)
-> (Map
      (Credential 'Staking (Crypto era))
      (Map (KeyHash 'StakePool (Crypto era)) Coin),
    Map
      (Credential 'Staking (Crypto era))
      (Map (KeyHash 'StakePool (Crypto era)) Coin))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
            (\Credential 'Staking (Crypto era)
k Map (KeyHash 'StakePool (Crypto era)) Coin
_ -> Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (Credential 'Staking (Crypto era)
k Credential 'Staking (Crypto era)
-> Exp (Sett (Credential 'Staking (Crypto era)) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> Exp (Sett (Credential 'Staking (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (DState (Crypto era)
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards DState (Crypto era)
ds)))
            Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
rewardAcntsWithPool
     in RetiredPools :: forall era.
Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
-> Map
     (Credential 'Staking (Crypto era))
     (Map (KeyHash 'StakePool (Crypto era)) Coin)
-> EpochNo
-> PoolreapEvent era
RetiredPools
          { refundPools :: Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
refundPools = Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
refundPools',
            unclaimedPools :: Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
unclaimedPools = Map
  (Credential 'Staking (Crypto era))
  (Map (KeyHash 'StakePool (Crypto era)) Coin)
unclaimedPools',
            epochNo :: EpochNo
epochNo = EpochNo
Signal (POOLREAP era)
e
          }

  PoolreapState era
-> F (Clause (POOLREAP era) 'Transition) (PoolreapState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PoolreapState era
 -> F (Clause (POOLREAP era) 'Transition) (PoolreapState era))
-> PoolreapState era
-> F (Clause (POOLREAP era) 'Transition) (PoolreapState era)
forall a b. (a -> b) -> a -> b
$
    UTxOState era
-> AccountState
-> DState (Crypto era)
-> PState (Crypto era)
-> PoolreapState era
forall era.
UTxOState era
-> AccountState
-> DState (Crypto era)
-> PState (Crypto era)
-> PoolreapState era
PoolreapState
      UTxOState era
us {_deposited :: Coin
_deposited = UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited UTxOState era
us Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> (Coin
unclaimed Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
refunded)}
      AccountState
a {_treasury :: Coin
_treasury = AccountState -> Coin
_treasury AccountState
a Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
unclaimed}
      ( let u0 :: UnifiedMap (Crypto era)
u0 = DState (Crypto era) -> UnifiedMap (Crypto era)
forall crypto. DState crypto -> UnifiedMap crypto
_unified DState (Crypto era)
ds
            u1 :: UnifiedMap (Crypto era)
u1 = (UnifiedMap (Crypto era)
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall coin cr pl ptr.
UMap coin cr pl ptr -> View coin cr pl ptr cr coin
Rewards UnifiedMap (Crypto era)
u0 ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> Map (Credential 'Staking (Crypto era)) Coin
-> UnifiedMap (Crypto era)
forall cred coin pool ptr k.
(Ord cred, Monoid coin) =>
View coin cred pool ptr k coin
-> Map k coin -> UMap coin cred pool ptr
UM.∪+ Map (Credential 'Staking (Crypto era)) Coin
refunds)
            u2 :: UnifiedMap (Crypto era)
u2 = (UnifiedMap (Crypto era)
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
forall coin cr pl ptr.
UMap coin cr pl ptr -> View coin cr pl ptr cr pl
Delegations UnifiedMap (Crypto era)
u1 View
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
-> Set (KeyHash 'StakePool (Crypto era)) -> UnifiedMap (Crypto era)
forall cred ptr coin pool k v.
(Ord cred, Ord ptr, Ord coin, Ord pool) =>
View coin cred pool ptr k v -> Set v -> UMap coin cred pool ptr
UM.⋫ Set (KeyHash 'StakePool (Crypto era))
retired)
         in DState (Crypto era)
ds {_unified :: UnifiedMap (Crypto era)
_unified = UnifiedMap (Crypto era)
u2}
      )
      PState (Crypto era)
ps
        { _pParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
_pParams = Exp
  (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (Crypto era))
retired Set (KeyHash 'StakePool (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp
     (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
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)
⋪ PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams PState (Crypto era)
ps),
          _fPParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
_fPParams = Exp
  (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (Crypto era))
retired Set (KeyHash 'StakePool (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp
     (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
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)
⋪ PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_fPParams PState (Crypto era)
ps),
          _retiring :: Map (KeyHash 'StakePool (Crypto era)) EpochNo
_retiring = Exp (Map (KeyHash 'StakePool (Crypto era)) EpochNo)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (Crypto era))
retired Set (KeyHash 'StakePool (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
-> Exp (Map (KeyHash 'StakePool (Crypto era)) 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)
⋪ PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall crypto.
PState crypto -> Map (KeyHash 'StakePool crypto) EpochNo
_retiring PState (Crypto era)
ps)
        }