{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Shelley.Spec.Ledger.STS.Ledgers
( LEDGERS,
LedgersEnv (..),
LedgersPredicateFailure (..),
PredicateFailure,
)
where
import Cardano.Binary (FromCBOR (..), ToCBOR (..))
import Cardano.Ledger.Era
import Cardano.Ledger.Shelley.Constraints (ShelleyBased)
import Control.Monad (foldM)
import Control.State.Transition
( Embed (..),
STS (..),
TRC (..),
TransitionRule,
judgmentContext,
trans,
)
import Data.Foldable (toList)
import Data.Sequence (Seq)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (ShelleyBase)
import Shelley.Spec.Ledger.Keys (DSignable, Hash)
import Shelley.Spec.Ledger.LedgerState
( AccountState,
LedgerState (..),
UTxOState,
emptyLedgerState,
_delegationState,
_utxoState,
)
import Shelley.Spec.Ledger.PParams (PParams)
import Shelley.Spec.Ledger.STS.Ledger (LEDGER, LedgerEnv (..))
import Shelley.Spec.Ledger.STS.Utxo
import Shelley.Spec.Ledger.Slot (SlotNo)
import Shelley.Spec.Ledger.Tx (Tx)
import Shelley.Spec.Ledger.TxBody (EraIndependentTxBody)
data LEDGERS era
data LedgersEnv era = LedgersEnv
{ :: SlotNo,
LedgersEnv era -> PParams era
ledgersPp :: PParams era,
LedgersEnv era -> AccountState
ledgersAccount :: AccountState
}
data LedgersPredicateFailure era
= LedgerFailure (PredicateFailure (LEDGER era))
deriving ((forall x.
LedgersPredicateFailure era -> Rep (LedgersPredicateFailure era) x)
-> (forall x.
Rep (LedgersPredicateFailure era) x -> LedgersPredicateFailure era)
-> Generic (LedgersPredicateFailure era)
forall x.
Rep (LedgersPredicateFailure era) x -> LedgersPredicateFailure era
forall x.
LedgersPredicateFailure era -> Rep (LedgersPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (LedgersPredicateFailure era) x -> LedgersPredicateFailure era
forall era x.
LedgersPredicateFailure era -> Rep (LedgersPredicateFailure era) x
$cto :: forall era x.
Rep (LedgersPredicateFailure era) x -> LedgersPredicateFailure era
$cfrom :: forall era x.
LedgersPredicateFailure era -> Rep (LedgersPredicateFailure era) x
Generic)
deriving stock instance
( ShelleyBased era,
Show (PredicateFailure (LEDGER era))
) =>
Show (LedgersPredicateFailure era)
deriving stock instance
( ShelleyBased era,
Eq (PredicateFailure (LEDGER era))
) =>
Eq (LedgersPredicateFailure era)
instance
( ShelleyBased era,
NoThunks (PredicateFailure (LEDGER era))
) =>
NoThunks (LedgersPredicateFailure era)
instance
( ShelleyBased era,
ToCBOR (PredicateFailure (LEDGER era))
) =>
ToCBOR (LedgersPredicateFailure era)
where
toCBOR :: LedgersPredicateFailure era -> Encoding
toCBOR (LedgerFailure PredicateFailure (LEDGER era)
e) = LedgerPredicateFailure era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (LEDGER era)
LedgerPredicateFailure era
e
instance
( ShelleyBased era,
FromCBOR (PredicateFailure (LEDGER era))
) =>
FromCBOR (LedgersPredicateFailure era)
where
fromCBOR :: Decoder s (LedgersPredicateFailure era)
fromCBOR = LedgerPredicateFailure era -> LedgersPredicateFailure era
forall era.
PredicateFailure (LEDGER era) -> LedgersPredicateFailure era
LedgerFailure (LedgerPredicateFailure era -> LedgersPredicateFailure era)
-> Decoder s (LedgerPredicateFailure era)
-> Decoder s (LedgersPredicateFailure era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (LedgerPredicateFailure era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
instance
( Era era,
ShelleyBased era,
Embed (LEDGER era) (LEDGERS era),
DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody)
) =>
STS (LEDGERS era)
where
type State (LEDGERS era) = LedgerState era
type Signal (LEDGERS era) = Seq (Tx era)
type Environment (LEDGERS era) = LedgersEnv era
type BaseM (LEDGERS era) = ShelleyBase
type PredicateFailure (LEDGERS era) = LedgersPredicateFailure era
initialRules :: [InitialRule (LEDGERS era)]
initialRules = [LedgerState era
-> F (Clause (LEDGERS era) 'Initial) (LedgerState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure LedgerState era
forall era. LedgerState era
emptyLedgerState]
transitionRules :: [TransitionRule (LEDGERS era)]
transitionRules = [TransitionRule (LEDGERS era)
forall era.
Embed (LEDGER era) (LEDGERS era) =>
TransitionRule (LEDGERS era)
ledgersTransition]
ledgersTransition ::
forall era.
( Embed (LEDGER era) (LEDGERS era)
) =>
TransitionRule (LEDGERS era)
ledgersTransition :: TransitionRule (LEDGERS era)
ledgersTransition = do
TRC (LedgersEnv slot pp account, State (LEDGERS era)
ls, Signal (LEDGERS era)
txwits) <- F (Clause (LEDGERS era) 'Transition) (TRC (LEDGERS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
let (UTxOState era
u, DPState (Crypto era)
dp) = (LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
_utxoState State (LEDGERS era)
LedgerState era
ls, LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
_delegationState State (LEDGERS era)
LedgerState era
ls)
(UTxOState era
u'', DPState (Crypto era)
dp'') <-
((UTxOState era, DPState (Crypto era))
-> (Ix, Tx era)
-> F (Clause (LEDGERS era) 'Transition)
(UTxOState era, DPState (Crypto era)))
-> (UTxOState era, DPState (Crypto era))
-> [(Ix, Tx era)]
-> F (Clause (LEDGERS era) 'Transition)
(UTxOState era, DPState (Crypto era))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
( \(UTxOState era
u', DPState (Crypto era)
dp') (Ix
ix, Tx era
tx) ->
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (LEDGER era) super =>
RuleContext rtype (LEDGER era)
-> Rule super rtype (State (LEDGER era))
trans @(LEDGER era) (RuleContext 'Transition (LEDGER era)
-> Rule (LEDGERS era) 'Transition (State (LEDGER era)))
-> RuleContext 'Transition (LEDGER era)
-> Rule (LEDGERS era) 'Transition (State (LEDGER era))
forall a b. (a -> b) -> a -> b
$
(Environment (LEDGER era), State (LEDGER era), Signal (LEDGER era))
-> TRC (LEDGER era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> Ix -> PParams era -> AccountState -> LedgerEnv era
forall era.
SlotNo -> Ix -> PParams era -> AccountState -> LedgerEnv era
LedgerEnv SlotNo
slot Ix
ix PParams era
pp AccountState
account, (UTxOState era
u', DPState (Crypto era)
dp'), Signal (LEDGER era)
Tx era
tx)
)
(UTxOState era
u, DPState (Crypto era)
dp)
([(Ix, Tx era)]
-> F (Clause (LEDGERS era) 'Transition)
(UTxOState era, DPState (Crypto era)))
-> [(Ix, Tx era)]
-> F (Clause (LEDGERS era) 'Transition)
(UTxOState era, DPState (Crypto era))
forall a b. (a -> b) -> a -> b
$ [Ix] -> [Tx era] -> [(Ix, Tx era)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ix
0 ..] ([Tx era] -> [(Ix, Tx era)]) -> [Tx era] -> [(Ix, Tx era)]
forall a b. (a -> b) -> a -> b
$
Seq (Tx era) -> [Tx era]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (Tx era)
Signal (LEDGERS era)
txwits
LedgerState era
-> F (Clause (LEDGERS era) 'Transition) (LedgerState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LedgerState era
-> F (Clause (LEDGERS era) 'Transition) (LedgerState era))
-> LedgerState era
-> F (Clause (LEDGERS era) 'Transition) (LedgerState era)
forall a b. (a -> b) -> a -> b
$ UTxOState era -> DPState (Crypto era) -> LedgerState era
forall era.
UTxOState era -> DPState (Crypto era) -> LedgerState era
LedgerState UTxOState era
u'' DPState (Crypto era)
dp''
instance
( Era era,
STS (LEDGER era),
ShelleyBased era,
DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
Environment (UTXO era) ~ UtxoEnv era,
State (UTXO era) ~ UTxOState era
) =>
Embed (LEDGER era) (LEDGERS era)
where
wrapFailed :: PredicateFailure (LEDGER era) -> PredicateFailure (LEDGERS era)
wrapFailed = PredicateFailure (LEDGER era) -> PredicateFailure (LEDGERS era)
forall era.
PredicateFailure (LEDGER era) -> LedgersPredicateFailure era
LedgerFailure