{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Shelley.Spec.Ledger.STS.Delpl
( DELPL,
DelplEnv (..),
DelplPredicateFailure (..),
PredicateFailure,
)
where
import Cardano.Binary
( FromCBOR (..),
ToCBOR (..),
encodeListLen,
)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Era)
import Control.State.Transition
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (ShelleyBase, invalidKey)
import Shelley.Spec.Ledger.LedgerState
( AccountState,
DPState,
emptyDelegation,
_dstate,
_pstate,
)
import Shelley.Spec.Ledger.PParams (PParams)
import Shelley.Spec.Ledger.STS.Deleg (DELEG, DelegEnv (..))
import Shelley.Spec.Ledger.STS.Pool (POOL, PoolEnv (..))
import Shelley.Spec.Ledger.Serialization (decodeRecordSum)
import Shelley.Spec.Ledger.Slot (SlotNo)
import Shelley.Spec.Ledger.TxBody
( DCert (..),
DelegCert (..),
GenesisDelegCert (..),
PoolCert (..),
Ptr,
)
data DELPL era
data DelplEnv era = DelplEnv
{ DelplEnv era -> SlotNo
delplSlotNo :: SlotNo,
DelplEnv era -> Ptr
delPlPtr :: Ptr,
DelplEnv era -> PParams era
delPlPp :: PParams era,
DelplEnv era -> AccountState
delPlAcnt :: AccountState
}
data DelplPredicateFailure era
= PoolFailure (PredicateFailure (POOL era))
| DelegFailure (PredicateFailure (DELEG era))
deriving (Int -> DelplPredicateFailure era -> ShowS
[DelplPredicateFailure era] -> ShowS
DelplPredicateFailure era -> String
(Int -> DelplPredicateFailure era -> ShowS)
-> (DelplPredicateFailure era -> String)
-> ([DelplPredicateFailure era] -> ShowS)
-> Show (DelplPredicateFailure era)
forall era. Int -> DelplPredicateFailure era -> ShowS
forall era. [DelplPredicateFailure era] -> ShowS
forall era. DelplPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DelplPredicateFailure era] -> ShowS
$cshowList :: forall era. [DelplPredicateFailure era] -> ShowS
show :: DelplPredicateFailure era -> String
$cshow :: forall era. DelplPredicateFailure era -> String
showsPrec :: Int -> DelplPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> DelplPredicateFailure era -> ShowS
Show, DelplPredicateFailure era -> DelplPredicateFailure era -> Bool
(DelplPredicateFailure era -> DelplPredicateFailure era -> Bool)
-> (DelplPredicateFailure era -> DelplPredicateFailure era -> Bool)
-> Eq (DelplPredicateFailure era)
forall era.
DelplPredicateFailure era -> DelplPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DelplPredicateFailure era -> DelplPredicateFailure era -> Bool
$c/= :: forall era.
DelplPredicateFailure era -> DelplPredicateFailure era -> Bool
== :: DelplPredicateFailure era -> DelplPredicateFailure era -> Bool
$c== :: forall era.
DelplPredicateFailure era -> DelplPredicateFailure era -> Bool
Eq, (forall x.
DelplPredicateFailure era -> Rep (DelplPredicateFailure era) x)
-> (forall x.
Rep (DelplPredicateFailure era) x -> DelplPredicateFailure era)
-> Generic (DelplPredicateFailure era)
forall x.
Rep (DelplPredicateFailure era) x -> DelplPredicateFailure era
forall x.
DelplPredicateFailure era -> Rep (DelplPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DelplPredicateFailure era) x -> DelplPredicateFailure era
forall era x.
DelplPredicateFailure era -> Rep (DelplPredicateFailure era) x
$cto :: forall era x.
Rep (DelplPredicateFailure era) x -> DelplPredicateFailure era
$cfrom :: forall era x.
DelplPredicateFailure era -> Rep (DelplPredicateFailure era) x
Generic)
instance
Era era =>
STS (DELPL era)
where
type State (DELPL era) = DPState era
type Signal (DELPL era) = DCert era
type Environment (DELPL era) = DelplEnv era
type BaseM (DELPL era) = ShelleyBase
type PredicateFailure (DELPL era) = DelplPredicateFailure era
initialRules :: [InitialRule (DELPL era)]
initialRules = [DPState era -> F (Clause (DELPL era) 'Initial) (DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure DPState era
forall era. DPState era
emptyDelegation]
transitionRules :: [TransitionRule (DELPL era)]
transitionRules = [TransitionRule (DELPL era)
forall era. Era era => TransitionRule (DELPL era)
delplTransition]
instance NoThunks (DelplPredicateFailure era)
instance
(Typeable era, Era era, Typeable (Core.Script era)) =>
ToCBOR (DelplPredicateFailure era)
where
toCBOR :: DelplPredicateFailure era -> Encoding
toCBOR = \case
(PoolFailure PredicateFailure (POOL era)
a) ->
Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
0 :: Word8)
Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PoolPredicateFailure era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (POOL era)
PoolPredicateFailure era
a
(DelegFailure PredicateFailure (DELEG era)
a) ->
Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
1 :: Word8)
Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> DelegPredicateFailure era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (DELEG era)
DelegPredicateFailure era
a
instance
(Era era, Typeable (Core.Script era)) =>
FromCBOR (DelplPredicateFailure era)
where
fromCBOR :: Decoder s (DelplPredicateFailure era)
fromCBOR =
String
-> (Word -> Decoder s (Int, DelplPredicateFailure era))
-> Decoder s (DelplPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum
String
"PredicateFailure (DELPL era)"
( \case
Word
0 -> do
PoolPredicateFailure era
a <- Decoder s (PoolPredicateFailure era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
(Int, DelplPredicateFailure era)
-> Decoder s (Int, DelplPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (POOL era) -> DelplPredicateFailure era
forall era.
PredicateFailure (POOL era) -> DelplPredicateFailure era
PoolFailure PredicateFailure (POOL era)
PoolPredicateFailure era
a)
Word
1 -> do
DelegPredicateFailure era
a <- Decoder s (DelegPredicateFailure era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
(Int, DelplPredicateFailure era)
-> Decoder s (Int, DelplPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (DELEG era) -> DelplPredicateFailure era
forall era.
PredicateFailure (DELEG era) -> DelplPredicateFailure era
DelegFailure PredicateFailure (DELEG era)
DelegPredicateFailure era
a)
Word
k -> Word -> Decoder s (Int, DelplPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k
)
delplTransition ::
forall era.
Era era =>
TransitionRule (DELPL era)
delplTransition :: TransitionRule (DELPL era)
delplTransition = do
TRC (DelplEnv slot ptr pp acnt, State (DELPL era)
d, Signal (DELPL era)
c) <- F (Clause (DELPL era) 'Transition) (TRC (DELPL era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
case Signal (DELPL era)
c of
DCertPool (RegPool _) -> do
PState era
ps <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (POOL era) super =>
RuleContext rtype (POOL era) -> Rule super rtype (State (POOL era))
trans @(POOL era) (RuleContext 'Transition (POOL era)
-> Rule (DELPL era) 'Transition (State (POOL era)))
-> RuleContext 'Transition (POOL era)
-> Rule (DELPL era) 'Transition (State (POOL era))
forall a b. (a -> b) -> a -> b
$ (Environment (POOL era), State (POOL era), Signal (POOL era))
-> TRC (POOL era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> PParams era -> PoolEnv era
forall era. SlotNo -> PParams era -> PoolEnv era
PoolEnv SlotNo
slot PParams era
pp, DPState era -> PState era
forall era. DPState era -> PState era
_pstate State (DELPL era)
DPState era
d, Signal (POOL era)
Signal (DELPL era)
c)
DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPState era -> F (Clause (DELPL era) 'Transition) (DPState era))
-> DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall a b. (a -> b) -> a -> b
$ State (DELPL era)
DPState era
d {_pstate :: PState era
_pstate = PState era
ps}
DCertPool (RetirePool _ _) -> do
PState era
ps <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (POOL era) super =>
RuleContext rtype (POOL era) -> Rule super rtype (State (POOL era))
trans @(POOL era) (RuleContext 'Transition (POOL era)
-> Rule (DELPL era) 'Transition (State (POOL era)))
-> RuleContext 'Transition (POOL era)
-> Rule (DELPL era) 'Transition (State (POOL era))
forall a b. (a -> b) -> a -> b
$ (Environment (POOL era), State (POOL era), Signal (POOL era))
-> TRC (POOL era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> PParams era -> PoolEnv era
forall era. SlotNo -> PParams era -> PoolEnv era
PoolEnv SlotNo
slot PParams era
pp, DPState era -> PState era
forall era. DPState era -> PState era
_pstate State (DELPL era)
DPState era
d, Signal (POOL era)
Signal (DELPL era)
c)
DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPState era -> F (Clause (DELPL era) 'Transition) (DPState era))
-> DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall a b. (a -> b) -> a -> b
$ State (DELPL era)
DPState era
d {_pstate :: PState era
_pstate = PState era
ps}
DCertGenesis (GenesisDelegCert {}) -> do
DState era
ds <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (DELEG era) super =>
RuleContext rtype (DELEG era)
-> Rule super rtype (State (DELEG era))
trans @(DELEG era) (RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era)))
-> RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era))
forall a b. (a -> b) -> a -> b
$ (Environment (DELEG era), State (DELEG era), Signal (DELEG era))
-> TRC (DELEG era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> Ptr -> AccountState -> DelegEnv
DelegEnv SlotNo
slot Ptr
ptr AccountState
acnt, DPState era -> DState era
forall era. DPState era -> DState era
_dstate State (DELPL era)
DPState era
d, Signal (DELEG era)
Signal (DELPL era)
c)
DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPState era -> F (Clause (DELPL era) 'Transition) (DPState era))
-> DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall a b. (a -> b) -> a -> b
$ State (DELPL era)
DPState era
d {_dstate :: DState era
_dstate = DState era
ds}
DCertDeleg (RegKey _) -> do
DState era
ds <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (DELEG era) super =>
RuleContext rtype (DELEG era)
-> Rule super rtype (State (DELEG era))
trans @(DELEG era) (RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era)))
-> RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era))
forall a b. (a -> b) -> a -> b
$ (Environment (DELEG era), State (DELEG era), Signal (DELEG era))
-> TRC (DELEG era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> Ptr -> AccountState -> DelegEnv
DelegEnv SlotNo
slot Ptr
ptr AccountState
acnt, DPState era -> DState era
forall era. DPState era -> DState era
_dstate State (DELPL era)
DPState era
d, Signal (DELEG era)
Signal (DELPL era)
c)
DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPState era -> F (Clause (DELPL era) 'Transition) (DPState era))
-> DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall a b. (a -> b) -> a -> b
$ State (DELPL era)
DPState era
d {_dstate :: DState era
_dstate = DState era
ds}
DCertDeleg (DeRegKey _) -> do
DState era
ds <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (DELEG era) super =>
RuleContext rtype (DELEG era)
-> Rule super rtype (State (DELEG era))
trans @(DELEG era) (RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era)))
-> RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era))
forall a b. (a -> b) -> a -> b
$ (Environment (DELEG era), State (DELEG era), Signal (DELEG era))
-> TRC (DELEG era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> Ptr -> AccountState -> DelegEnv
DelegEnv SlotNo
slot Ptr
ptr AccountState
acnt, DPState era -> DState era
forall era. DPState era -> DState era
_dstate State (DELPL era)
DPState era
d, Signal (DELEG era)
Signal (DELPL era)
c)
DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPState era -> F (Clause (DELPL era) 'Transition) (DPState era))
-> DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall a b. (a -> b) -> a -> b
$ State (DELPL era)
DPState era
d {_dstate :: DState era
_dstate = DState era
ds}
DCertDeleg (Delegate _) -> do
DState era
ds <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (DELEG era) super =>
RuleContext rtype (DELEG era)
-> Rule super rtype (State (DELEG era))
trans @(DELEG era) (RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era)))
-> RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era))
forall a b. (a -> b) -> a -> b
$ (Environment (DELEG era), State (DELEG era), Signal (DELEG era))
-> TRC (DELEG era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> Ptr -> AccountState -> DelegEnv
DelegEnv SlotNo
slot Ptr
ptr AccountState
acnt, DPState era -> DState era
forall era. DPState era -> DState era
_dstate State (DELPL era)
DPState era
d, Signal (DELEG era)
Signal (DELPL era)
c)
DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPState era -> F (Clause (DELPL era) 'Transition) (DPState era))
-> DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall a b. (a -> b) -> a -> b
$ State (DELPL era)
DPState era
d {_dstate :: DState era
_dstate = DState era
ds}
DCertMir _ -> do
DState era
ds <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (DELEG era) super =>
RuleContext rtype (DELEG era)
-> Rule super rtype (State (DELEG era))
trans @(DELEG era) (RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era)))
-> RuleContext 'Transition (DELEG era)
-> Rule (DELPL era) 'Transition (State (DELEG era))
forall a b. (a -> b) -> a -> b
$ (Environment (DELEG era), State (DELEG era), Signal (DELEG era))
-> TRC (DELEG era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> Ptr -> AccountState -> DelegEnv
DelegEnv SlotNo
slot Ptr
ptr AccountState
acnt, DPState era -> DState era
forall era. DPState era -> DState era
_dstate State (DELPL era)
DPState era
d, Signal (DELEG era)
Signal (DELPL era)
c)
DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPState era -> F (Clause (DELPL era) 'Transition) (DPState era))
-> DPState era -> F (Clause (DELPL era) 'Transition) (DPState era)
forall a b. (a -> b) -> a -> b
$ State (DELPL era)
DPState era
d {_dstate :: DState era
_dstate = DState era
ds}
instance
Era era =>
Embed (POOL era) (DELPL era)
where
wrapFailed :: PredicateFailure (POOL era) -> PredicateFailure (DELPL era)
wrapFailed = PredicateFailure (POOL era) -> PredicateFailure (DELPL era)
forall era.
PredicateFailure (POOL era) -> DelplPredicateFailure era
PoolFailure
instance
Era era =>
Embed (DELEG era) (DELPL era)
where
wrapFailed :: PredicateFailure (DELEG era) -> PredicateFailure (DELPL era)
wrapFailed = PredicateFailure (DELEG era) -> PredicateFailure (DELPL era)
forall era.
PredicateFailure (DELEG era) -> DelplPredicateFailure era
DelegFailure