{-# 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)) -- Subtransition Failures
  | DelegFailure (PredicateFailure (DELEG era)) -- Subtransition Failures
  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