{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Byron.Spec.Chain.STS.Rule.BBody where

import Byron.Spec.Chain.STS.Block
import Byron.Spec.Chain.STS.Rule.Bupi
import Byron.Spec.Ledger.Core (BlockCount, Epoch, hash)
import Byron.Spec.Ledger.Delegation (
  DELEG,
  DIState,
  DSEnv (DSEnv),
  _dIStateDelegationMap,
  _dSEnvAllowedDelegators,
  _dSEnvEpoch,
  _dSEnvK,
  _dSEnvSlot,
 )
import Byron.Spec.Ledger.STS.UTXO (UTxOEnv (UTxOEnv, pps, utxo0), UTxOState)
import Byron.Spec.Ledger.STS.UTXOWS (UTXOWS)
import Byron.Spec.Ledger.UTxO (UTxO)
import Byron.Spec.Ledger.Update (PParams, UPIState, maxBkSz)
import Control.State.Transition (
  Embed,
  Environment,
  STS (..),
  Signal,
  State,
  TRC (TRC),
  initialRules,
  judgmentContext,
  trans,
  transitionRules,
  wrapFailed,
  (?!),
 )
import Data.Bimap (keys)
import Data.Data (Data)
import Data.Set (fromList)
import Data.Word (Word8)
import Lens.Micro ((^.))

data BBODY deriving (Typeable BBODY
Typeable BBODY =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BBODY -> c BBODY)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BBODY)
-> (BBODY -> Constr)
-> (BBODY -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BBODY))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BBODY))
-> ((forall b. Data b => b -> b) -> BBODY -> BBODY)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BBODY -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BBODY -> r)
-> (forall u. (forall d. Data d => d -> u) -> BBODY -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BBODY -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BBODY -> m BBODY)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BBODY -> m BBODY)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BBODY -> m BBODY)
-> Data BBODY
BBODY -> Constr
BBODY -> DataType
(forall b. Data b => b -> b) -> BBODY -> BBODY
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BBODY -> u
forall u. (forall d. Data d => d -> u) -> BBODY -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BBODY -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BBODY -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BBODY -> m BBODY
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BBODY -> m BBODY
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BBODY
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BBODY -> c BBODY
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BBODY)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BBODY)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BBODY -> c BBODY
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BBODY -> c BBODY
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BBODY
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BBODY
$ctoConstr :: BBODY -> Constr
toConstr :: BBODY -> Constr
$cdataTypeOf :: BBODY -> DataType
dataTypeOf :: BBODY -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BBODY)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BBODY)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BBODY)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BBODY)
$cgmapT :: (forall b. Data b => b -> b) -> BBODY -> BBODY
gmapT :: (forall b. Data b => b -> b) -> BBODY -> BBODY
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BBODY -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BBODY -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BBODY -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BBODY -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BBODY -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BBODY -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BBODY -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BBODY -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BBODY -> m BBODY
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BBODY -> m BBODY
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BBODY -> m BBODY
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BBODY -> m BBODY
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BBODY -> m BBODY
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BBODY -> m BBODY
Data)

-- | These `PredicateFailure`s are all throwable.
data BbodyPredicateFailure
  = InvalidBlockSize
  | InvalidUtxoHash
  | InvalidDelegationHash
  | InvalidUpdateProposalHash
  | BUPIFailure (PredicateFailure BUPI)
  | DelegationFailure (PredicateFailure DELEG)
  | UTXOWSFailure (PredicateFailure UTXOWS)
  deriving (BbodyPredicateFailure -> BbodyPredicateFailure -> Bool
(BbodyPredicateFailure -> BbodyPredicateFailure -> Bool)
-> (BbodyPredicateFailure -> BbodyPredicateFailure -> Bool)
-> Eq BbodyPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BbodyPredicateFailure -> BbodyPredicateFailure -> Bool
== :: BbodyPredicateFailure -> BbodyPredicateFailure -> Bool
$c/= :: BbodyPredicateFailure -> BbodyPredicateFailure -> Bool
/= :: BbodyPredicateFailure -> BbodyPredicateFailure -> Bool
Eq, Int -> BbodyPredicateFailure -> ShowS
[BbodyPredicateFailure] -> ShowS
BbodyPredicateFailure -> String
(Int -> BbodyPredicateFailure -> ShowS)
-> (BbodyPredicateFailure -> String)
-> ([BbodyPredicateFailure] -> ShowS)
-> Show BbodyPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BbodyPredicateFailure -> ShowS
showsPrec :: Int -> BbodyPredicateFailure -> ShowS
$cshow :: BbodyPredicateFailure -> String
show :: BbodyPredicateFailure -> String
$cshowList :: [BbodyPredicateFailure] -> ShowS
showList :: [BbodyPredicateFailure] -> ShowS
Show, Typeable BbodyPredicateFailure
Typeable BbodyPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> BbodyPredicateFailure
 -> c BbodyPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BbodyPredicateFailure)
-> (BbodyPredicateFailure -> Constr)
-> (BbodyPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BbodyPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c BbodyPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> BbodyPredicateFailure -> BbodyPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> BbodyPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> BbodyPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> BbodyPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BbodyPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> BbodyPredicateFailure -> m BbodyPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> BbodyPredicateFailure -> m BbodyPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> BbodyPredicateFailure -> m BbodyPredicateFailure)
-> Data BbodyPredicateFailure
BbodyPredicateFailure -> Constr
BbodyPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> BbodyPredicateFailure -> BbodyPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> BbodyPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> BbodyPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BbodyPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BbodyPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BbodyPredicateFailure -> m BbodyPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BbodyPredicateFailure -> m BbodyPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BbodyPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BbodyPredicateFailure
-> c BbodyPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BbodyPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BbodyPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BbodyPredicateFailure
-> c BbodyPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BbodyPredicateFailure
-> c BbodyPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BbodyPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BbodyPredicateFailure
$ctoConstr :: BbodyPredicateFailure -> Constr
toConstr :: BbodyPredicateFailure -> Constr
$cdataTypeOf :: BbodyPredicateFailure -> DataType
dataTypeOf :: BbodyPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BbodyPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BbodyPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BbodyPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BbodyPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> BbodyPredicateFailure -> BbodyPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> BbodyPredicateFailure -> BbodyPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BbodyPredicateFailure -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BbodyPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BbodyPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BbodyPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> BbodyPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> BbodyPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> BbodyPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> BbodyPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BbodyPredicateFailure -> m BbodyPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BbodyPredicateFailure -> m BbodyPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BbodyPredicateFailure -> m BbodyPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BbodyPredicateFailure -> m BbodyPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BbodyPredicateFailure -> m BbodyPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BbodyPredicateFailure -> m BbodyPredicateFailure
Data)

instance STS BBODY where
  type
    Environment BBODY =
      ( PParams
      , Epoch
      , UTxO
      , Word8
      , BlockCount -- Chain stability parameter
      )

  type
    State BBODY =
      ( UTxOState
      , DIState
      , UPIState
      )

  type Signal BBODY = Block

  type PredicateFailure BBODY = BbodyPredicateFailure

  initialRules :: [InitialRule BBODY]
initialRules = []

  transitionRules :: [TransitionRule BBODY]
transitionRules =
    [ do
        TRC ((PParams
ppsVal, Epoch
e_n, UTxO
utxoGenesis, Word8
ngk, BlockCount
k), (UTxOState
utxoSt, DIState
ds, UPIState
us), Signal BBODY
b) <- Rule BBODY 'Transition (RuleContext 'Transition BBODY)
F (Clause BBODY 'Transition) (TRC BBODY)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let bMax :: Natural
bMax = PParams
ppsVal PParams -> Getting Natural PParams Natural -> Natural
forall s a. s -> Getting a s a -> a
^. Getting Natural PParams Natural
Lens' PParams Natural
maxBkSz
        Block -> Natural
bSize Signal BBODY
Block
b Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
bMax Bool -> PredicateFailure BBODY -> Rule BBODY 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure BBODY
BbodyPredicateFailure
InvalidBlockSize
        let bh :: BlockHeader
bh = Signal BBODY
Block
b Block -> Getting BlockHeader Block BlockHeader -> BlockHeader
forall s a. s -> Getting a s a -> a
^. Getting BlockHeader Block BlockHeader
Lens' Block BlockHeader
bHeader
        [Tx] -> Hash
forall a. HasHash a => a -> Hash
hash (Signal BBODY
Block
b Block -> Getting BlockBody Block BlockBody -> BlockBody
forall s a. s -> Getting a s a -> a
^. Getting BlockBody Block BlockBody
Lens' Block BlockBody
bBody BlockBody -> Getting [Tx] BlockBody [Tx] -> [Tx]
forall s a. s -> Getting a s a -> a
^. Getting [Tx] BlockBody [Tx]
Lens' BlockBody [Tx]
bUtxo) Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== BlockHeader
bh BlockHeader -> Getting Hash BlockHeader Hash -> Hash
forall s a. s -> Getting a s a -> a
^. Getting Hash BlockHeader Hash
Lens' BlockHeader Hash
bhUtxoHash Bool -> PredicateFailure BBODY -> Rule BBODY 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure BBODY
BbodyPredicateFailure
InvalidUtxoHash
        [DCert] -> Hash
forall a. HasHash a => a -> Hash
hash (Signal BBODY
Block
b Block -> Getting BlockBody Block BlockBody -> BlockBody
forall s a. s -> Getting a s a -> a
^. Getting BlockBody Block BlockBody
Lens' Block BlockBody
bBody BlockBody -> Getting [DCert] BlockBody [DCert] -> [DCert]
forall s a. s -> Getting a s a -> a
^. Getting [DCert] BlockBody [DCert]
Lens' BlockBody [DCert]
bDCerts) Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== BlockHeader
bh BlockHeader -> Getting Hash BlockHeader Hash -> Hash
forall s a. s -> Getting a s a -> a
^. Getting Hash BlockHeader Hash
Lens' BlockHeader Hash
bhDlgHash Bool -> PredicateFailure BBODY -> Rule BBODY 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure BBODY
BbodyPredicateFailure
InvalidDelegationHash
        (Maybe UProp, [Vote]) -> Hash
forall a. HasHash a => a -> Hash
hash (Block -> (Maybe UProp, [Vote])
bUpdPayload Signal BBODY
Block
b) Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== BlockHeader
bh BlockHeader -> Getting Hash BlockHeader Hash -> Hash
forall s a. s -> Getting a s a -> a
^. Getting Hash BlockHeader Hash
Lens' BlockHeader Hash
bhUpdHash Bool -> PredicateFailure BBODY -> Rule BBODY 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure BBODY
BbodyPredicateFailure
InvalidUpdateProposalHash

        UPIState
us' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @BUPI (RuleContext 'Transition BUPI
 -> Rule BBODY 'Transition (State BUPI))
-> RuleContext 'Transition BUPI
-> Rule BBODY 'Transition (State BUPI)
forall a b. (a -> b) -> a -> b
$
            (Environment BUPI, State BUPI, Signal BUPI) -> TRC BUPI
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              ( (BlockHeader
bh BlockHeader -> Getting Slot BlockHeader Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot BlockHeader Slot
Lens' BlockHeader Slot
bhSlot, DIState -> Bimap VKeyGenesis VKey
_dIStateDelegationMap DIState
ds, BlockCount
k, Word8
ngk)
              , UPIState
State BUPI
us
              , (Signal BBODY
Block
b Block -> Getting BlockBody Block BlockBody -> BlockBody
forall s a. s -> Getting a s a -> a
^. Getting BlockBody Block BlockBody
Lens' Block BlockBody
bBody BlockBody
-> Getting (Maybe UProp) BlockBody (Maybe UProp) -> Maybe UProp
forall s a. s -> Getting a s a -> a
^. Getting (Maybe UProp) BlockBody (Maybe UProp)
Lens' BlockBody (Maybe UProp)
bUpdProp, Signal BBODY
Block
b Block -> Getting BlockBody Block BlockBody -> BlockBody
forall s a. s -> Getting a s a -> a
^. Getting BlockBody Block BlockBody
Lens' Block BlockBody
bBody BlockBody -> Getting [Vote] BlockBody [Vote] -> [Vote]
forall s a. s -> Getting a s a -> a
^. Getting [Vote] BlockBody [Vote]
Lens' BlockBody [Vote]
bUpdVotes, Block -> (ProtVer, VKey)
bEndorsment Signal BBODY
Block
b)
              )
        DIState
ds' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @DELEG (RuleContext 'Transition DELEG
 -> Rule BBODY 'Transition (State DELEG))
-> RuleContext 'Transition DELEG
-> Rule BBODY 'Transition (State DELEG)
forall a b. (a -> b) -> a -> b
$
            (Environment DELEG, State DELEG, Signal DELEG) -> TRC DELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              ( ( DSEnv
                    { _dSEnvAllowedDelegators :: Set VKeyGenesis
_dSEnvAllowedDelegators =
                        ([VKeyGenesis] -> Set VKeyGenesis
forall a. Ord a => [a] -> Set a
fromList ([VKeyGenesis] -> Set VKeyGenesis)
-> (DIState -> [VKeyGenesis]) -> DIState -> Set VKeyGenesis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bimap VKeyGenesis VKey -> [VKeyGenesis]
forall a b. Bimap a b -> [a]
keys (Bimap VKeyGenesis VKey -> [VKeyGenesis])
-> (DIState -> Bimap VKeyGenesis VKey) -> DIState -> [VKeyGenesis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DIState -> Bimap VKeyGenesis VKey
_dIStateDelegationMap) DIState
ds
                    , _dSEnvEpoch :: Epoch
_dSEnvEpoch = Epoch
e_n
                    , _dSEnvSlot :: Slot
_dSEnvSlot = BlockHeader
bh BlockHeader -> Getting Slot BlockHeader Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot BlockHeader Slot
Lens' BlockHeader Slot
bhSlot
                    , _dSEnvK :: BlockCount
_dSEnvK = BlockCount
k
                    }
                )
              , DIState
State DELEG
ds
              , Signal BBODY
Block
b Block -> Getting BlockBody Block BlockBody -> BlockBody
forall s a. s -> Getting a s a -> a
^. Getting BlockBody Block BlockBody
Lens' Block BlockBody
bBody BlockBody -> Getting [DCert] BlockBody [DCert] -> [DCert]
forall s a. s -> Getting a s a -> a
^. Getting [DCert] BlockBody [DCert]
Lens' BlockBody [DCert]
bDCerts
              )
        UTxOState
utxoSt' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UTXOWS (RuleContext 'Transition UTXOWS
 -> Rule BBODY 'Transition (State UTXOWS))
-> RuleContext 'Transition UTXOWS
-> Rule BBODY 'Transition (State UTXOWS)
forall a b. (a -> b) -> a -> b
$
            (Environment UTXOWS, State UTXOWS, Signal UTXOWS) -> TRC UTXOWS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              (UTxOEnv {utxo0 :: UTxO
utxo0 = UTxO
utxoGenesis, pps :: PParams
pps = PParams
ppsVal}, UTxOState
State UTXOWS
utxoSt, Signal BBODY
Block
b Block -> Getting BlockBody Block BlockBody -> BlockBody
forall s a. s -> Getting a s a -> a
^. Getting BlockBody Block BlockBody
Lens' Block BlockBody
bBody BlockBody -> Getting [Tx] BlockBody [Tx] -> [Tx]
forall s a. s -> Getting a s a -> a
^. Getting [Tx] BlockBody [Tx]
Lens' BlockBody [Tx]
bUtxo)

        (UTxOState, DIState, UPIState)
-> F (Clause BBODY 'Transition) (UTxOState, DIState, UPIState)
forall a. a -> F (Clause BBODY 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((UTxOState, DIState, UPIState)
 -> F (Clause BBODY 'Transition) (UTxOState, DIState, UPIState))
-> (UTxOState, DIState, UPIState)
-> F (Clause BBODY 'Transition) (UTxOState, DIState, UPIState)
forall a b. (a -> b) -> a -> b
$! (UTxOState
utxoSt', DIState
ds', UPIState
us')
    ]

instance Embed BUPI BBODY where
  wrapFailed :: PredicateFailure BUPI -> PredicateFailure BBODY
wrapFailed = PredicateFailure BUPI -> PredicateFailure BBODY
PredicateFailure BUPI -> BbodyPredicateFailure
BUPIFailure

instance Embed DELEG BBODY where
  wrapFailed :: PredicateFailure DELEG -> PredicateFailure BBODY
wrapFailed = PredicateFailure DELEG -> PredicateFailure BBODY
PredicateFailure DELEG -> BbodyPredicateFailure
DelegationFailure

instance Embed UTXOWS BBODY where
  wrapFailed :: PredicateFailure UTXOWS -> PredicateFailure BBODY
wrapFailed = PredicateFailure UTXOWS -> PredicateFailure BBODY
PredicateFailure UTXOWS -> BbodyPredicateFailure
UTXOWSFailure