{-# 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.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) (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 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 = ShelleyPoolreapEvent ShelleyEra

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 (Credential 'Staking) RDPair
r = forall era. DState era -> UView (Credential 'Staking) 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 (Credential 'Staking) 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 (Credential 'Staking) 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)
    retired :: Set (KeyHash 'StakePool)
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) 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) Coin
    (Map (KeyHash 'StakePool) Coin
retiringDeposits, Map (KeyHash 'StakePool) Coin
remainingDeposits) =
      forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\KeyHash 'StakePool
k Coin
_ -> forall a. Ord a => a -> Set a -> Bool
Set.member KeyHash 'StakePool
k Set (KeyHash 'StakePool)
retired) (forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits PState era
ps)
    rewardAccounts :: Map.Map (KeyHash 'StakePool) RewardAccount
    rewardAccounts :: Map (KeyHash 'StakePool) RewardAccount
rewardAccounts = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map PoolParams -> RewardAccount
ppRewardAccount forall a b. (a -> b) -> a -> b
$ forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool)
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) PoolParams
psStakePoolParams PState era
ps)
    rewardAccounts_ ::
      Map.Map (KeyHash 'StakePool) (RewardAccount, Coin)
    rewardAccounts_ :: Map (KeyHash 'StakePool) (RewardAccount, 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) RewardAccount
rewardAccounts Map (KeyHash 'StakePool) Coin
retiringDeposits
    rewardAccounts' :: Map.Map RewardAccount Coin
    rewardAccounts' :: Map RewardAccount 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) (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) =
      forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
        (\Credential 'Staking
k Coin
_ -> forall k v. k -> UView k v -> Bool
UM.member Credential 'Staking
k (forall era. DState era -> UView (Credential 'Staking) 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 RewardAccount -> Credential 'Staking
raCredential Map RewardAccount Coin
rewardAccounts')
    refunded :: Coin
refunded = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
refunds
    unclaimed :: Coin
unclaimed = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
mRefunds

  forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$
    let rewardAccountsWithPool :: Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
rewardAccountsWithPool =
          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) ->
                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
(<>)) (RewardAccount -> Credential 'Staking
raCredential RewardAccount
ra) (forall k a. k -> a -> Map k a
Map.singleton KeyHash 'StakePool
sp Coin
coin) Map (Credential 'Staking) (Map (KeyHash 'StakePool) Coin)
acc
            )
            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') =
          forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
            (\Credential 'Staking
k Map (KeyHash 'StakePool) Coin
_ -> forall k v. k -> UView k v -> Bool
UM.member Credential 'Staking
k (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 = 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
u0 = forall era. DState era -> UMap
dsUnified DState era
ds
            u1 :: UMap
u1 = UMap -> UView (Credential 'Staking) RDPair
RewDepUView UMap
u0 UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) (CompactForm Coin) -> UMap
UM.∪+ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
compactCoinOrError Map (Credential 'Staking) Coin
refunds
            u2 :: UMap
u2 = UMap -> UView (Credential 'Staking) (KeyHash 'StakePool)
SPoolUView UMap
u1 forall k v. UView k v -> Set v -> UMap
UM.⋫ Set (KeyHash 'StakePool)
retired
         in DState era
ds {dsUnified :: UMap
dsUnified = UMap
u2}
      )
      PState era
ps
        { psStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psStakePoolParams = forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool)
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) PoolParams
psStakePoolParams PState era
ps)
        , -- TODO: redundant
          psFutureStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams = forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool)
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) PoolParams
psFutureStakePoolParams PState era
ps)
        , psRetiring :: Map (KeyHash 'StakePool) EpochNo
psRetiring = forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool)
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) EpochNo
psRetiring PState era
ps)
        , psDeposits :: Map (KeyHash 'StakePool) Coin
psDeposits = Map (KeyHash 'StakePool) 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