{-# 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)
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.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 -> 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
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 (CertState era)) => Default (ShelleyPoolreapState era) where
  def :: ShelleyPoolreapState era
def = forall era.
UTxOState era
-> ChainAccountState -> CertState era -> ShelleyPoolreapState era
PoolreapState 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
  , 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 = [forall era.
EraCertState era =>
TransitionRule (ShelleyPOOLREAP era)
poolReapTransition]

  renderAssertionViolation :: AssertionViolation (ShelleyPOOLREAP era) -> String
renderAssertionViolation = forall era t.
(EraGov era, State t ~ ShelleyPoolreapState era,
 EraCertState 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 (ShelleyPOOLREAP era)
_trc State (ShelleyPOOLREAP era)
st ->
            forall era.
(EraGov era, EraCertState era) =>
CertState era -> UTxOState era -> Bool
potEqualsObligation
              (forall era. ShelleyPoolreapState era -> CertState era
prCertState 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 ShelleyPoolreapState era
prState = forall era. DState era -> UView (Credential 'Staking) RDPair
rewards (forall era. ShelleyPoolreapState era -> CertState era
prCertState ShelleyPoolreapState era
prState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL)
             in forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {era}.
EraCertState 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}.
EraCertState era =>
ShelleyPoolreapState era -> UView (Credential 'Staking) RDPair
r State (ShelleyPOOLREAP 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) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  let
    ps :: PState era
ps = CertState era
cs forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL
    ds :: DState era
ds = CertState era
cs forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL
    -- 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
-> ChainAccountState -> CertState 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)}
      ChainAccountState
a {casTreasury :: Coin
casTreasury = ChainAccountState -> Coin
casTreasury ChainAccountState
a forall t. Val t => t -> t -> t
<+> Coin
unclaimed}
      ( CertState era
cs
          forall a b. a -> (a -> b) -> b
& forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) UMap
dsUnifiedL
            forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ( \UMap
uni ->
                  UMap -> UView (Credential 'Staking) (KeyHash 'StakePool)
SPoolUView (UMap -> UView (Credential 'Staking) RDPair
RewDepUView UMap
uni 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) forall k v. UView k v -> Set v -> UMap
UM.⋫ Set (KeyHash 'StakePool)
retired
               )
          forall a b. a -> (a -> b) -> b
& forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
Lens' (PState era) (Map (KeyHash 'StakePool) PoolParams)
psStakePoolParamsL forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall s t. Embed s t => Exp t -> s
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 a b. a -> (a -> b) -> b
& forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
Lens' (PState era) (Map (KeyHash 'StakePool) PoolParams)
psFutureStakePoolParamsL forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall s t. Embed s t => Exp t -> s
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 a b. a -> (a -> b) -> b
& forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (PState era) (Map (KeyHash 'StakePool) EpochNo)
psRetiringL forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall s t. Embed s t => Exp t -> s
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 a b. a -> (a -> b) -> b
& forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (PState era) (Map (KeyHash 'StakePool) Coin)
psDepositsL forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map (KeyHash 'StakePool) 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 :: 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 (Environment t
_, State t
poolreapst, Signal t
_)} =
    let obligations :: Obligations
obligations =
          forall era.
(EraGov era, EraCertState era) =>
CertState era -> GovState era -> Obligations
allObligations (forall era. ShelleyPoolreapState era -> CertState era
prCertState State t
poolreapst) (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