{-# 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.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 era
r = DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards (DState era -> RewardAccounts era)
-> (EpochState era -> DState era)
-> EpochState era
-> RewardAccounts era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DPState era -> DState era
forall era. DPState era -> DState era
_dstate (DPState era -> DState era)
-> (EpochState era -> DPState era) -> EpochState era -> DState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState era -> DPState era
forall era. LedgerState era -> DPState era
_delegationState (LedgerState era -> DPState era)
-> (EpochState era -> LedgerState era)
-> EpochState era
-> DPState 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 era) Coin -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EpochState era -> Map (Credential 'Staking era) Coin
forall era. EpochState era -> RewardAccounts era
r State (MIR era)
EpochState era
st) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Credential 'Staking era) Coin -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EpochState era -> Map (Credential 'Staking era) Coin
forall era. EpochState era -> RewardAccounts 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 era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
forall era.
AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
EpochState
      AccountState
emptyAccount
      SnapShots era
forall era. SnapShots era
emptySnapShots
      LedgerState era
forall era. LedgerState era
emptyLedgerState
      PParams era
forall era. PParams era
emptyPParams
      PParams era
forall era. PParams era
emptyPParams
      NonMyopic era
forall era. NonMyopic era
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 era
dpState = LedgerState era -> DPState era
forall era. LedgerState era -> DPState era
_delegationState LedgerState era
ls
      ds :: DState era
ds = DPState era -> DState era
forall era. DPState era -> DState era
_dstate DPState era
dpState
      rewards :: RewardAccounts era
rewards = DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards DState era
ds
      reserves :: Coin
reserves = AccountState -> Coin
_reserves AccountState
acnt
      treasury :: Coin
treasury = AccountState -> Coin
_treasury AccountState
acnt
      irwdR :: RewardAccounts era
irwdR = Exp (RewardAccounts era) -> RewardAccounts era
forall s t. Embed s t => Exp t -> s
eval (Exp (RewardAccounts era) -> RewardAccounts era)
-> Exp (RewardAccounts era) -> RewardAccounts era
forall a b. (a -> b) -> a -> b
$ (RewardAccounts era -> Exp (Sett (Credential 'Staking era) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom RewardAccounts era
rewards) Exp (Sett (Credential 'Staking era) ())
-> RewardAccounts era -> Exp (RewardAccounts 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 era -> RewardAccounts era
forall era.
InstantaneousRewards era -> Map (Credential 'Staking era) Coin
iRReserves (InstantaneousRewards era -> RewardAccounts era)
-> InstantaneousRewards era -> RewardAccounts era
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards era
forall era. DState era -> InstantaneousRewards era
_irwd DState era
ds) :: RewardAccounts era
      irwdT :: RewardAccounts era
irwdT = Exp (RewardAccounts era) -> RewardAccounts era
forall s t. Embed s t => Exp t -> s
eval (Exp (RewardAccounts era) -> RewardAccounts era)
-> Exp (RewardAccounts era) -> RewardAccounts era
forall a b. (a -> b) -> a -> b
$ (RewardAccounts era -> Exp (Sett (Credential 'Staking era) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom RewardAccounts era
rewards) Exp (Sett (Credential 'Staking era) ())
-> RewardAccounts era -> Exp (RewardAccounts 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 era -> RewardAccounts era
forall era.
InstantaneousRewards era -> Map (Credential 'Staking era) Coin
iRTreasury (InstantaneousRewards era -> RewardAccounts era)
-> InstantaneousRewards era -> RewardAccounts era
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards era
forall era. DState era -> InstantaneousRewards era
_irwd DState era
ds) :: RewardAccounts era
      totR :: Coin
totR = RewardAccounts era -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts era
irwdR
      totT :: Coin
totT = RewardAccounts era -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts era
irwdT
      update :: RewardAccounts era
update = (Exp (RewardAccounts era) -> RewardAccounts era
forall s t. Embed s t => Exp t -> s
eval (RewardAccounts era
irwdR RewardAccounts era
-> RewardAccounts era -> Exp (RewardAccounts 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 era
irwdT)) :: RewardAccounts 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 era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
forall era.
AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic 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 era
ss
          LedgerState era
ls
            { _delegationState :: DPState era
_delegationState =
                DPState era
dpState
                  { _dstate :: DState era
_dstate =
                      DState era
ds
                        { _rewards :: RewardAccounts era
_rewards = Exp (RewardAccounts era) -> RewardAccounts era
forall s t. Embed s t => Exp t -> s
eval ((DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards DState era
ds) RewardAccounts era
-> RewardAccounts era -> Exp (RewardAccounts 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 era
update),
                          _irwd :: InstantaneousRewards era
_irwd = InstantaneousRewards era
forall era. InstantaneousRewards era
emptyInstantaneousRewards
                        }
                  }
            }
          PParams era
pr
          PParams era
pp
          NonMyopic 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 era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
forall era.
AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
EpochState
          AccountState
acnt
          SnapShots era
ss
          LedgerState era
ls
            { _delegationState :: DPState era
_delegationState =
                DPState era
dpState
                  { _dstate :: DState era
_dstate =
                      DState era
ds {_irwd :: InstantaneousRewards era
_irwd = InstantaneousRewards era
forall era. InstantaneousRewards era
emptyInstantaneousRewards}
                  }
            }
          PParams era
pr
          PParams era
pp
          NonMyopic era
nm