{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Shelley.Spec.Ledger.STS.Mir
  ( MIR,
    PredicateFailure,
    MirPredicateFailure,
  )
where

import Cardano.Ledger.Era (Crypto)
import Cardano.Ledger.Val ((<->))
import Control.SetAlgebra (dom, eval, (∪+), (◁))
import Control.State.Transition
  ( Assertion (..),
    InitialRule,
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
  )
import Data.Foldable (fold)
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (ShelleyBase)
import Shelley.Spec.Ledger.EpochBoundary (emptySnapShots)
import Shelley.Spec.Ledger.LedgerState
  ( AccountState (..),
    EpochState,
    InstantaneousRewards (..),
    RewardAccounts,
    emptyAccount,
    emptyInstantaneousRewards,
    emptyLedgerState,
    esAccountState,
    esLState,
    esNonMyopic,
    esPp,
    esPrevPp,
    esSnapshots,
    _delegationState,
    _dstate,
    _irwd,
    _rewards,
    pattern EpochState,
  )
import Shelley.Spec.Ledger.PParams (emptyPParams)
import Shelley.Spec.Ledger.Rewards (emptyNonMyopic)

data MIR era

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

instance NoThunks (MirPredicateFailure era)

instance Typeable era => STS (MIR era) where
  type State (MIR era) = EpochState era
  type Signal (MIR era) = ()
  type Environment (MIR era) = ()
  type BaseM (MIR era) = ShelleyBase
  type PredicateFailure (MIR era) = MirPredicateFailure era

  initialRules :: [InitialRule (MIR era)]
initialRules = [InitialRule (MIR era)
forall era. InitialRule (MIR era)
initialMir]
  transitionRules :: [TransitionRule (MIR era)]
transitionRules = [TransitionRule (MIR era)
forall era. TransitionRule (MIR era)
mirTransition]

  assertions :: [Assertion (MIR era)]
assertions =
    [ String
-> (TRC (MIR era) -> State (MIR era) -> Bool)
-> Assertion (MIR era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"MIR may not create or remove reward accounts"
        ( \(TRC (Environment (MIR era)
_, State (MIR era)
st, Signal (MIR era)
_)) State (MIR era)
st' ->
            let r :: EpochState era -> RewardAccounts (Crypto era)
r = DState (Crypto era) -> RewardAccounts (Crypto era)
forall crypto. DState crypto -> RewardAccounts crypto
_rewards (DState (Crypto era) -> RewardAccounts (Crypto era))
-> (EpochState era -> DState (Crypto era))
-> EpochState era
-> RewardAccounts (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DPState (Crypto era) -> DState (Crypto era)
forall crypto. DPState crypto -> DState crypto
_dstate (DPState (Crypto era) -> DState (Crypto era))
-> (EpochState era -> DPState (Crypto era))
-> EpochState era
-> DState (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
_delegationState (LedgerState era -> DPState (Crypto era))
-> (EpochState era -> LedgerState era)
-> EpochState era
-> DPState (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState
             in Map (Credential 'Staking (Crypto era)) Coin -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EpochState era -> Map (Credential 'Staking (Crypto era)) Coin
forall era. EpochState era -> RewardAccounts (Crypto era)
r State (MIR era)
EpochState era
st) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Credential 'Staking (Crypto era)) Coin -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EpochState era -> Map (Credential 'Staking (Crypto era)) Coin
forall era. EpochState era -> RewardAccounts (Crypto era)
r State (MIR era)
EpochState era
st')
        )
    ]

initialMir :: InitialRule (MIR era)
initialMir :: InitialRule (MIR era)
initialMir =
  EpochState era -> F (Clause (MIR era) 'Initial) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EpochState era -> F (Clause (MIR era) 'Initial) (EpochState era))
-> EpochState era -> F (Clause (MIR era) 'Initial) (EpochState era)
forall a b. (a -> b) -> a -> b
$
    AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
forall era.
AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
EpochState
      AccountState
emptyAccount
      SnapShots (Crypto era)
forall crypto. SnapShots crypto
emptySnapShots
      LedgerState era
forall era. LedgerState era
emptyLedgerState
      PParams era
forall era. PParams era
emptyPParams
      PParams era
forall era. PParams era
emptyPParams
      NonMyopic (Crypto era)
forall crypto. NonMyopic crypto
emptyNonMyopic

mirTransition :: forall era. TransitionRule (MIR era)
mirTransition :: TransitionRule (MIR era)
mirTransition = do
  TRC
    ( Environment (MIR era)
_,
      EpochState
        { esAccountState = acnt,
          esSnapshots = ss,
          esLState = ls,
          esPrevPp = pr,
          esPp = pp,
          esNonMyopic = nm
        },
      ()
      ) <-
    F (Clause (MIR era) 'Transition) (TRC (MIR era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let dpState :: DPState (Crypto era)
dpState = LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
_delegationState LedgerState era
ls
      ds :: DState (Crypto era)
ds = DPState (Crypto era) -> DState (Crypto era)
forall crypto. DPState crypto -> DState crypto
_dstate DPState (Crypto era)
dpState
      rewards :: RewardAccounts (Crypto era)
rewards = DState (Crypto era) -> RewardAccounts (Crypto era)
forall crypto. DState crypto -> RewardAccounts crypto
_rewards DState (Crypto era)
ds
      reserves :: Coin
reserves = AccountState -> Coin
_reserves AccountState
acnt
      treasury :: Coin
treasury = AccountState -> Coin
_treasury AccountState
acnt
      irwdR :: RewardAccounts (Crypto era)
irwdR = Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall s t. Embed s t => Exp t -> s
eval (Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era))
-> Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall a b. (a -> b) -> a -> b
$ (RewardAccounts (Crypto era)
-> Exp (Sett (Credential 'Staking (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom RewardAccounts (Crypto era)
rewards) Exp (Sett (Credential 'Staking (Crypto era)) ())
-> RewardAccounts (Crypto era) -> Exp (RewardAccounts (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)
 (InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era)
forall crypto.
InstantaneousRewards crypto
-> Map (Credential 'Staking crypto) Coin
iRReserves (InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era))
-> InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era)
forall a b. (a -> b) -> a -> b
$ DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd DState (Crypto era)
ds) :: RewardAccounts (Crypto era)
      irwdT :: RewardAccounts (Crypto era)
irwdT = Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall s t. Embed s t => Exp t -> s
eval (Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era))
-> Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall a b. (a -> b) -> a -> b
$ (RewardAccounts (Crypto era)
-> Exp (Sett (Credential 'Staking (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom RewardAccounts (Crypto era)
rewards) Exp (Sett (Credential 'Staking (Crypto era)) ())
-> RewardAccounts (Crypto era) -> Exp (RewardAccounts (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)
 (InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era)
forall crypto.
InstantaneousRewards crypto
-> Map (Credential 'Staking crypto) Coin
iRTreasury (InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era))
-> InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era)
forall a b. (a -> b) -> a -> b
$ DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd DState (Crypto era)
ds) :: RewardAccounts (Crypto era)
      totR :: Coin
totR = RewardAccounts (Crypto era) -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts (Crypto era)
irwdR
      totT :: Coin
totT = RewardAccounts (Crypto era) -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts (Crypto era)
irwdT
      update :: RewardAccounts (Crypto era)
update = (Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall s t. Embed s t => Exp t -> s
eval (RewardAccounts (Crypto era)
irwdR RewardAccounts (Crypto era)
-> RewardAccounts (Crypto era) -> Exp (RewardAccounts (Crypto era))
forall k n s1 (f :: * -> * -> *) s2.
(Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (f k n)) =>
s1 -> s2 -> Exp (f k n)
∪+ RewardAccounts (Crypto era)
irwdT)) :: RewardAccounts (Crypto era)

  if Coin
totR Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
reserves Bool -> Bool -> Bool
&& Coin
totT Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
treasury
    then
      EpochState era -> F (Clause (MIR era) 'Transition) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EpochState era
 -> F (Clause (MIR era) 'Transition) (EpochState era))
-> EpochState era
-> F (Clause (MIR era) 'Transition) (EpochState era)
forall a b. (a -> b) -> a -> b
$
        AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
forall era.
AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
EpochState
          AccountState
acnt
            { _reserves :: Coin
_reserves = Coin
reserves Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Coin
totR,
              _treasury :: Coin
_treasury = Coin
treasury Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Coin
totT
            }
          SnapShots (Crypto era)
ss
          LedgerState era
ls
            { _delegationState :: DPState (Crypto era)
_delegationState =
                DPState (Crypto era)
dpState
                  { _dstate :: DState (Crypto era)
_dstate =
                      DState (Crypto era)
ds
                        { _rewards :: RewardAccounts (Crypto era)
_rewards = Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall s t. Embed s t => Exp t -> s
eval ((DState (Crypto era) -> RewardAccounts (Crypto era)
forall crypto. DState crypto -> RewardAccounts crypto
_rewards DState (Crypto era)
ds) RewardAccounts (Crypto era)
-> RewardAccounts (Crypto era) -> Exp (RewardAccounts (Crypto era))
forall k n s1 (f :: * -> * -> *) s2.
(Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (f k n)) =>
s1 -> s2 -> Exp (f k n)
∪+ RewardAccounts (Crypto era)
update),
                          _irwd :: InstantaneousRewards (Crypto era)
_irwd = InstantaneousRewards (Crypto era)
forall crypto. InstantaneousRewards crypto
emptyInstantaneousRewards
                        }
                  }
            }
          PParams era
pr
          PParams era
pp
          NonMyopic (Crypto era)
nm
    else
      EpochState era -> F (Clause (MIR era) 'Transition) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EpochState era
 -> F (Clause (MIR era) 'Transition) (EpochState era))
-> EpochState era
-> F (Clause (MIR era) 'Transition) (EpochState era)
forall a b. (a -> b) -> a -> b
$
        AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
forall era.
AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
EpochState
          AccountState
acnt
          SnapShots (Crypto era)
ss
          LedgerState era
ls
            { _delegationState :: DPState (Crypto era)
_delegationState =
                DPState (Crypto era)
dpState
                  { _dstate :: DState (Crypto era)
_dstate =
                      DState (Crypto era)
ds {_irwd :: InstantaneousRewards (Crypto era)
_irwd = InstantaneousRewards (Crypto era)
forall crypto. InstantaneousRewards crypto
emptyInstantaneousRewards}
                  }
            }
          PParams era
pr
          PParams era
pp
          NonMyopic (Crypto era)
nm