{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

-- | Specs necessary to generate, environment, state, and signal
-- for the UTXO rule
module Test.Cardano.Ledger.Constrained.Conway.Utxo where

import Cardano.Ledger.Babbage.TxOut
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Decode (..), Encode (..), decode, encode, (!>), (<!))
import Cardano.Ledger.Compactible (fromCompact)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (
  Era (..),
  EraPParams (..),
  EraTx (..),
  EraTxAuxData (..),
  EraTxWits (..),
 )
import Cardano.Ledger.Conway.Governance (GovActionId, Proposals, gasDeposit, pPropsL)
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Shelley.API.Types
import Cardano.Ledger.Shelley.Rules (Identity, epochFromSlot, utxoEnvCertStateL)
import Constrained.API
import Control.DeepSeq (NFData)
import Control.Monad.Reader (runReader)
import Data.Bifunctor (Bifunctor (..))
import qualified Data.Map.Strict as Map
import qualified Data.OMap.Strict as OMap
import Data.Word
import GHC.Generics (Generic)
import Lens.Micro ((^.))
import Test.Cardano.Ledger.Babbage.Arbitrary ()
import Test.Cardano.Ledger.Common (Arbitrary (..), ToExpr, oneof)
import Test.Cardano.Ledger.Constrained.Conway.Gov (proposalsSpec)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Conway.TreeDiff ()
import Test.Cardano.Ledger.Core.Utils (testGlobals)

instance HasSimpleRep DepositPurpose

instance HasSpec DepositPurpose

witnessDepositPurpose ::
  forall era.
  Era era =>
  WitUniv era -> Specification DepositPurpose
witnessDepositPurpose :: forall era. Era era => WitUniv era -> Specification DepositPurpose
witnessDepositPurpose WitUniv era
univ = (Term DepositPurpose -> Pred) -> Specification DepositPurpose
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term DepositPurpose -> Pred) -> Specification DepositPurpose)
-> (Term DepositPurpose -> Pred) -> Specification DepositPurpose
forall a b. (a -> b) -> a -> b
$ \ Term DepositPurpose
[var|depPurpose|] ->
  (Term DepositPurpose
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep DepositPurpose)))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term DepositPurpose
depPurpose)
    -- CredentialDeposit !(Credential 'Staking c)
    (FunTy (MapList Term (Args (Credential 'Staking))) Pred
-> Weighted (BinderD Deps) (Credential 'Staking)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (Credential 'Staking))) Pred
 -> Weighted (BinderD Deps) (Credential 'Staking))
-> FunTy (MapList Term (Args (Credential 'Staking))) Pred
-> Weighted (BinderD Deps) (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
cred -> WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
cred)
    -- PoolDeposit !(KeyHash 'StakePool c)
    (FunTy (MapList Term (Args (KeyHash 'StakePool))) Pred
-> Weighted (BinderD Deps) (KeyHash 'StakePool)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (KeyHash 'StakePool))) Pred
 -> Weighted (BinderD Deps) (KeyHash 'StakePool))
-> FunTy (MapList Term (Args (KeyHash 'StakePool))) Pred
-> Weighted (BinderD Deps) (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'StakePool)
keyhash -> WitUniv era -> Term (KeyHash 'StakePool) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (KeyHash 'StakePool)
keyhash)
    -- DRepDeposit !(Credential 'DRepRole c)
    (FunTy (MapList Term (Args (Credential 'DRepRole))) Pred
-> Weighted (BinderD Deps) (Credential 'DRepRole)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (Credential 'DRepRole))) Pred
 -> Weighted (BinderD Deps) (Credential 'DRepRole))
-> FunTy (MapList Term (Args (Credential 'DRepRole))) Pred
-> Weighted (BinderD Deps) (Credential 'DRepRole)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
drep -> WitUniv era -> Term (Credential 'DRepRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'DRepRole)
drep)
    -- GovActionDeposit
    (FunTy (MapList Term (Args GovActionId)) Bool
-> Weighted (BinderD Deps) GovActionId
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args GovActionId)) Bool
 -> Weighted (BinderD Deps) GovActionId)
-> FunTy (MapList Term (Args GovActionId)) Bool
-> Weighted (BinderD Deps) GovActionId
forall a b. (a -> b) -> a -> b
$ \TermD Deps GovActionId
_ -> Bool
True)

data DepositPurpose
  = CredentialDeposit !(Credential 'Staking)
  | PoolDeposit !(KeyHash 'StakePool)
  | DRepDeposit !(Credential 'DRepRole)
  | GovActionDeposit !GovActionId
  deriving ((forall x. DepositPurpose -> Rep DepositPurpose x)
-> (forall x. Rep DepositPurpose x -> DepositPurpose)
-> Generic DepositPurpose
forall x. Rep DepositPurpose x -> DepositPurpose
forall x. DepositPurpose -> Rep DepositPurpose x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DepositPurpose -> Rep DepositPurpose x
from :: forall x. DepositPurpose -> Rep DepositPurpose x
$cto :: forall x. Rep DepositPurpose x -> DepositPurpose
to :: forall x. Rep DepositPurpose x -> DepositPurpose
Generic, DepositPurpose -> DepositPurpose -> Bool
(DepositPurpose -> DepositPurpose -> Bool)
-> (DepositPurpose -> DepositPurpose -> Bool) -> Eq DepositPurpose
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DepositPurpose -> DepositPurpose -> Bool
== :: DepositPurpose -> DepositPurpose -> Bool
$c/= :: DepositPurpose -> DepositPurpose -> Bool
/= :: DepositPurpose -> DepositPurpose -> Bool
Eq, Int -> DepositPurpose -> ShowS
[DepositPurpose] -> ShowS
DepositPurpose -> String
(Int -> DepositPurpose -> ShowS)
-> (DepositPurpose -> String)
-> ([DepositPurpose] -> ShowS)
-> Show DepositPurpose
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DepositPurpose -> ShowS
showsPrec :: Int -> DepositPurpose -> ShowS
$cshow :: DepositPurpose -> String
show :: DepositPurpose -> String
$cshowList :: [DepositPurpose] -> ShowS
showList :: [DepositPurpose] -> ShowS
Show, Eq DepositPurpose
Eq DepositPurpose =>
(DepositPurpose -> DepositPurpose -> Ordering)
-> (DepositPurpose -> DepositPurpose -> Bool)
-> (DepositPurpose -> DepositPurpose -> Bool)
-> (DepositPurpose -> DepositPurpose -> Bool)
-> (DepositPurpose -> DepositPurpose -> Bool)
-> (DepositPurpose -> DepositPurpose -> DepositPurpose)
-> (DepositPurpose -> DepositPurpose -> DepositPurpose)
-> Ord DepositPurpose
DepositPurpose -> DepositPurpose -> Bool
DepositPurpose -> DepositPurpose -> Ordering
DepositPurpose -> DepositPurpose -> DepositPurpose
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DepositPurpose -> DepositPurpose -> Ordering
compare :: DepositPurpose -> DepositPurpose -> Ordering
$c< :: DepositPurpose -> DepositPurpose -> Bool
< :: DepositPurpose -> DepositPurpose -> Bool
$c<= :: DepositPurpose -> DepositPurpose -> Bool
<= :: DepositPurpose -> DepositPurpose -> Bool
$c> :: DepositPurpose -> DepositPurpose -> Bool
> :: DepositPurpose -> DepositPurpose -> Bool
$c>= :: DepositPurpose -> DepositPurpose -> Bool
>= :: DepositPurpose -> DepositPurpose -> Bool
$cmax :: DepositPurpose -> DepositPurpose -> DepositPurpose
max :: DepositPurpose -> DepositPurpose -> DepositPurpose
$cmin :: DepositPurpose -> DepositPurpose -> DepositPurpose
min :: DepositPurpose -> DepositPurpose -> DepositPurpose
Ord)

instance Arbitrary DepositPurpose where
  arbitrary :: Gen DepositPurpose
arbitrary =
    [Gen DepositPurpose] -> Gen DepositPurpose
forall a. HasCallStack => [Gen a] -> Gen a
oneof
      [ Credential 'Staking -> DepositPurpose
CredentialDeposit (Credential 'Staking -> DepositPurpose)
-> Gen (Credential 'Staking) -> Gen DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Credential 'Staking)
forall a. Arbitrary a => Gen a
arbitrary
      , KeyHash 'StakePool -> DepositPurpose
PoolDeposit (KeyHash 'StakePool -> DepositPurpose)
-> Gen (KeyHash 'StakePool) -> Gen DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (KeyHash 'StakePool)
forall a. Arbitrary a => Gen a
arbitrary
      , Credential 'DRepRole -> DepositPurpose
DRepDeposit (Credential 'DRepRole -> DepositPurpose)
-> Gen (Credential 'DRepRole) -> Gen DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Credential 'DRepRole)
forall a. Arbitrary a => Gen a
arbitrary
      , GovActionId -> DepositPurpose
GovActionDeposit (GovActionId -> DepositPurpose)
-> Gen GovActionId -> Gen DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen GovActionId
forall a. Arbitrary a => Gen a
arbitrary
      ]

instance DecCBOR DepositPurpose where
  decCBOR :: forall s. Decoder s DepositPurpose
decCBOR =
    Decode ('Closed 'Dense) DepositPurpose -> Decoder s DepositPurpose
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode ('Closed 'Dense) DepositPurpose
 -> Decoder s DepositPurpose)
-> ((Word -> Decode 'Open DepositPurpose)
    -> Decode ('Closed 'Dense) DepositPurpose)
-> (Word -> Decode 'Open DepositPurpose)
-> Decoder s DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> (Word -> Decode 'Open DepositPurpose)
-> Decode ('Closed 'Dense) DepositPurpose
forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"DepositPurpose" ((Word -> Decode 'Open DepositPurpose) -> Decoder s DepositPurpose)
-> (Word -> Decode 'Open DepositPurpose)
-> Decoder s DepositPurpose
forall a b. (a -> b) -> a -> b
$
      \case
        Word
0 -> (Credential 'Staking -> DepositPurpose)
-> Decode 'Open (Credential 'Staking -> DepositPurpose)
forall t. t -> Decode 'Open t
SumD Credential 'Staking -> DepositPurpose
CredentialDeposit Decode 'Open (Credential 'Staking -> DepositPurpose)
-> Decode ('Closed Any) (Credential 'Staking)
-> Decode 'Open DepositPurpose
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Credential 'Staking)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Word
1 -> (KeyHash 'StakePool -> DepositPurpose)
-> Decode 'Open (KeyHash 'StakePool -> DepositPurpose)
forall t. t -> Decode 'Open t
SumD KeyHash 'StakePool -> DepositPurpose
PoolDeposit Decode 'Open (KeyHash 'StakePool -> DepositPurpose)
-> Decode ('Closed Any) (KeyHash 'StakePool)
-> Decode 'Open DepositPurpose
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (KeyHash 'StakePool)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Word
2 -> (Credential 'DRepRole -> DepositPurpose)
-> Decode 'Open (Credential 'DRepRole -> DepositPurpose)
forall t. t -> Decode 'Open t
SumD Credential 'DRepRole -> DepositPurpose
DRepDeposit Decode 'Open (Credential 'DRepRole -> DepositPurpose)
-> Decode ('Closed Any) (Credential 'DRepRole)
-> Decode 'Open DepositPurpose
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Credential 'DRepRole)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Word
3 -> (GovActionId -> DepositPurpose)
-> Decode 'Open (GovActionId -> DepositPurpose)
forall t. t -> Decode 'Open t
SumD GovActionId -> DepositPurpose
GovActionDeposit Decode 'Open (GovActionId -> DepositPurpose)
-> Decode ('Closed Any) GovActionId -> Decode 'Open DepositPurpose
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) GovActionId
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Word
k -> Word -> Decode 'Open DepositPurpose
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
k

instance EncCBOR DepositPurpose where
  encCBOR :: DepositPurpose -> Encoding
encCBOR =
    Encode 'Open DepositPurpose -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode 'Open DepositPurpose -> Encoding)
-> (DepositPurpose -> Encode 'Open DepositPurpose)
-> DepositPurpose
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      CredentialDeposit Credential 'Staking
c -> (Credential 'Staking -> DepositPurpose)
-> Word -> Encode 'Open (Credential 'Staking -> DepositPurpose)
forall t. t -> Word -> Encode 'Open t
Sum Credential 'Staking -> DepositPurpose
CredentialDeposit Word
0 Encode 'Open (Credential 'Staking -> DepositPurpose)
-> Encode ('Closed 'Dense) (Credential 'Staking)
-> Encode 'Open DepositPurpose
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Credential 'Staking
-> Encode ('Closed 'Dense) (Credential 'Staking)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Credential 'Staking
c
      PoolDeposit KeyHash 'StakePool
kh -> (KeyHash 'StakePool -> DepositPurpose)
-> Word -> Encode 'Open (KeyHash 'StakePool -> DepositPurpose)
forall t. t -> Word -> Encode 'Open t
Sum KeyHash 'StakePool -> DepositPurpose
PoolDeposit Word
1 Encode 'Open (KeyHash 'StakePool -> DepositPurpose)
-> Encode ('Closed 'Dense) (KeyHash 'StakePool)
-> Encode 'Open DepositPurpose
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> KeyHash 'StakePool -> Encode ('Closed 'Dense) (KeyHash 'StakePool)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To KeyHash 'StakePool
kh
      DRepDeposit Credential 'DRepRole
c -> (Credential 'DRepRole -> DepositPurpose)
-> Word -> Encode 'Open (Credential 'DRepRole -> DepositPurpose)
forall t. t -> Word -> Encode 'Open t
Sum Credential 'DRepRole -> DepositPurpose
DRepDeposit Word
2 Encode 'Open (Credential 'DRepRole -> DepositPurpose)
-> Encode ('Closed 'Dense) (Credential 'DRepRole)
-> Encode 'Open DepositPurpose
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Credential 'DRepRole
-> Encode ('Closed 'Dense) (Credential 'DRepRole)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Credential 'DRepRole
c
      GovActionDeposit GovActionId
gaid -> (GovActionId -> DepositPurpose)
-> Word -> Encode 'Open (GovActionId -> DepositPurpose)
forall t. t -> Word -> Encode 'Open t
Sum GovActionId -> DepositPurpose
GovActionDeposit Word
3 Encode 'Open (GovActionId -> DepositPurpose)
-> Encode ('Closed 'Dense) GovActionId
-> Encode 'Open DepositPurpose
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> GovActionId -> Encode ('Closed 'Dense) GovActionId
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To GovActionId
gaid

instance NFData DepositPurpose

instance ToExpr DepositPurpose

utxoEnvSpec ::
  UtxoExecContext ConwayEra ->
  Specification (UtxoEnv ConwayEra)
utxoEnvSpec :: UtxoExecContext ConwayEra -> Specification (UtxoEnv ConwayEra)
utxoEnvSpec UtxoExecContext {Tx ConwayEra
UTxO ConwayEra
UtxoEnv ConwayEra
uecTx :: Tx ConwayEra
uecUTxO :: UTxO ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
uecTx :: forall era. UtxoExecContext era -> Tx era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
..} =
  (Term (UtxoEnv ConwayEra) -> Term Bool)
-> Specification (UtxoEnv ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (UtxoEnv ConwayEra) -> Term Bool)
 -> Specification (UtxoEnv ConwayEra))
-> (Term (UtxoEnv ConwayEra) -> Term Bool)
-> Specification (UtxoEnv ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (UtxoEnv ConwayEra)
utxoEnv ->
    Term (UtxoEnv ConwayEra)
utxoEnv Term (UtxoEnv ConwayEra) -> Term (UtxoEnv ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. UtxoEnv ConwayEra -> Term (UtxoEnv ConwayEra)
forall a. HasSpec a => a -> Term a
lit UtxoEnv ConwayEra
uecUtxoEnv

utxoStateSpec ::
  UtxoExecContext ConwayEra ->
  UtxoEnv ConwayEra ->
  Specification (UTxOState ConwayEra)
utxoStateSpec :: UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification (UTxOState ConwayEra)
utxoStateSpec UtxoExecContext {UTxO ConwayEra
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUTxO :: UTxO ConwayEra
uecUTxO} UtxoEnv {SlotNo
ueSlot :: SlotNo
ueSlot :: forall era. UtxoEnv era -> SlotNo
ueSlot, CertState ConwayEra
ueCertState :: CertState ConwayEra
ueCertState :: forall era. UtxoEnv era -> CertState era
ueCertState} =
  (Term (UTxOState ConwayEra) -> Pred)
-> Specification (UTxOState ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (UTxOState ConwayEra) -> Pred)
 -> Specification (UTxOState ConwayEra))
-> (Term (UTxOState ConwayEra) -> Pred)
-> Specification (UTxOState ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (UTxOState ConwayEra)
utxoState ->
    Term (UTxOState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (UTxOState ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (UTxOState ConwayEra)
utxoState (FunTy (MapList Term (ProductAsList (UTxOState ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (UTxOState ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$
      \Term (UTxO ConwayEra)
utxosUtxo
       Term Coin
_utxosDeposited
       Term Coin
_utxosFees
       Term (ConwayGovState ConwayEra)
utxosGovState
       TermD Deps (ConwayInstantStake ConwayEra)
_utxosStakeDistr
       Term Coin
_utxosDonation ->
          [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (UTxO ConwayEra)
utxosUtxo Term (UTxO ConwayEra) -> Term (UTxO ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. UTxO ConwayEra -> Term (UTxO ConwayEra)
forall a. HasSpec a => a -> Term a
lit UTxO ConwayEra
uecUTxO
          , Term (ConwayGovState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ConwayGovState ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayGovState ConwayEra)
utxosGovState (FunTy
   (MapList Term (ProductAsList (ConwayGovState ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayGovState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Proposals ConwayEra)
props TermD Deps (StrictMaybe (Committee ConwayEra))
_ Term (Constitution ConwayEra)
constitution TermD Deps (PParams ConwayEra)
_ TermD Deps (PParams ConwayEra)
_ TermD Deps (FuturePParams ConwayEra)
_ TermD Deps (DRepPulsingState ConwayEra)
_ ->
              Term (Constitution ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (Constitution ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Constitution ConwayEra)
constitution (FunTy (MapList Term (ProductAsList (Constitution ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Constitution ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps Anchor
_ Term (StrictMaybe ScriptHash)
policy ->
                Term (Proposals ConwayEra)
-> Specification (Proposals ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Proposals ConwayEra)
props (Specification (Proposals ConwayEra) -> Pred)
-> Specification (Proposals ConwayEra) -> Pred
forall a b. (a -> b) -> a -> b
$ Term EpochNo
-> Term (StrictMaybe ScriptHash)
-> Term (CertState ConwayEra)
-> Specification (Proposals ConwayEra)
proposalsSpec (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
curEpoch) Term (StrictMaybe ScriptHash)
policy (ConwayCertState ConwayEra -> Term (ConwayCertState ConwayEra)
forall a. HasSpec a => a -> Term a
lit CertState ConwayEra
ConwayCertState ConwayEra
ueCertState)
          ]
  where
    curEpoch :: EpochNo
curEpoch = Reader Globals EpochNo -> Globals -> EpochNo
forall r a. Reader r a -> r -> a
runReader (SlotNo -> Reader Globals EpochNo
epochFromSlot SlotNo
ueSlot) Globals
testGlobals

data UtxoExecContext era = UtxoExecContext
  { forall era. UtxoExecContext era -> Tx era
uecTx :: !(Tx era)
  , forall era. UtxoExecContext era -> UTxO era
uecUTxO :: !(UTxO era)
  , forall era. UtxoExecContext era -> UtxoEnv era
uecUtxoEnv :: !(UtxoEnv era)
  }
  deriving ((forall x. UtxoExecContext era -> Rep (UtxoExecContext era) x)
-> (forall x. Rep (UtxoExecContext era) x -> UtxoExecContext era)
-> Generic (UtxoExecContext era)
forall x. Rep (UtxoExecContext era) x -> UtxoExecContext era
forall x. UtxoExecContext era -> Rep (UtxoExecContext era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (UtxoExecContext era) x -> UtxoExecContext era
forall era x. UtxoExecContext era -> Rep (UtxoExecContext era) x
$cfrom :: forall era x. UtxoExecContext era -> Rep (UtxoExecContext era) x
from :: forall x. UtxoExecContext era -> Rep (UtxoExecContext era) x
$cto :: forall era x. Rep (UtxoExecContext era) x -> UtxoExecContext era
to :: forall x. Rep (UtxoExecContext era) x -> UtxoExecContext era
Generic)

instance
  ( EraTx era
  , NFData (TxWits era)
  , NFData (TxAuxData era)
  , EraCertState era
  ) =>
  NFData (UtxoExecContext era)

instance
  ( EraTx era
  , ToExpr (TxOut era)
  , ToExpr (TxBody era)
  , ToExpr (TxWits era)
  , ToExpr (TxAuxData era)
  , ToExpr (PParamsHKD Identity era)
  , EraCertState era
  , ToExpr (CertState era)
  , ToExpr (Tx era)
  ) =>
  ToExpr (UtxoExecContext era)

instance
  ( EraPParams era
  , EncCBOR (TxOut era)
  , EncCBOR (TxBody era)
  , EncCBOR (TxAuxData era)
  , EncCBOR (TxWits era)
  , EncCBOR (Tx era)
  , EraCertState era
  ) =>
  EncCBOR (UtxoExecContext era)
  where
  encCBOR :: UtxoExecContext era -> Encoding
encCBOR x :: UtxoExecContext era
x@(UtxoExecContext Tx era
_ UTxO era
_ UtxoEnv era
_) =
    let UtxoExecContext {Tx era
UTxO era
UtxoEnv era
uecTx :: forall era. UtxoExecContext era -> Tx era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecTx :: Tx era
uecUTxO :: UTxO era
uecUtxoEnv :: UtxoEnv era
..} = UtxoExecContext era
x
     in Encode ('Closed 'Dense) (UtxoExecContext era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode ('Closed 'Dense) (UtxoExecContext era) -> Encoding)
-> Encode ('Closed 'Dense) (UtxoExecContext era) -> Encoding
forall a b. (a -> b) -> a -> b
$
          (Tx era -> UTxO era -> UtxoEnv era -> UtxoExecContext era)
-> Encode
     ('Closed 'Dense)
     (Tx era -> UTxO era -> UtxoEnv era -> UtxoExecContext era)
forall t. t -> Encode ('Closed 'Dense) t
Rec Tx era -> UTxO era -> UtxoEnv era -> UtxoExecContext era
forall era.
Tx era -> UTxO era -> UtxoEnv era -> UtxoExecContext era
UtxoExecContext
            Encode
  ('Closed 'Dense)
  (Tx era -> UTxO era -> UtxoEnv era -> UtxoExecContext era)
-> Encode ('Closed 'Dense) (Tx era)
-> Encode
     ('Closed 'Dense) (UTxO era -> UtxoEnv era -> UtxoExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Tx era -> Encode ('Closed 'Dense) (Tx era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Tx era
uecTx
            Encode
  ('Closed 'Dense) (UTxO era -> UtxoEnv era -> UtxoExecContext era)
-> Encode ('Closed 'Dense) (UTxO era)
-> Encode ('Closed 'Dense) (UtxoEnv era -> UtxoExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> UTxO era -> Encode ('Closed 'Dense) (UTxO era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To UTxO era
uecUTxO
            Encode ('Closed 'Dense) (UtxoEnv era -> UtxoExecContext era)
-> Encode ('Closed 'Dense) (UtxoEnv era)
-> Encode ('Closed 'Dense) (UtxoExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> UtxoEnv era -> Encode ('Closed 'Dense) (UtxoEnv era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To UtxoEnv era
uecUtxoEnv

instance CertState era ~ ConwayCertState era => Inject (UtxoExecContext era) (ConwayCertState era) where
  inject :: UtxoExecContext era -> ConwayCertState era
inject UtxoExecContext era
ctx = (UtxoExecContext era -> UtxoEnv era
forall era. UtxoExecContext era -> UtxoEnv era
uecUtxoEnv UtxoExecContext era
ctx) UtxoEnv era
-> Getting
     (ConwayCertState era) (UtxoEnv era) (ConwayCertState era)
-> ConwayCertState era
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const (ConwayCertState era) (CertState era))
-> UtxoEnv era -> Const (ConwayCertState era) (UtxoEnv era)
Getting (ConwayCertState era) (UtxoEnv era) (ConwayCertState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> UtxoEnv era -> f (UtxoEnv era)
utxoEnvCertStateL

utxoTxSpec ::
  HasSpec (Tx era) =>
  UtxoExecContext era ->
  Specification (Tx era)
utxoTxSpec :: forall era.
HasSpec (Tx era) =>
UtxoExecContext era -> Specification (Tx era)
utxoTxSpec UtxoExecContext {Tx era
uecTx :: forall era. UtxoExecContext era -> Tx era
uecTx :: Tx era
uecTx} =
  (Term (Tx era) -> Term Bool) -> Specification (Tx era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tx era) -> Term Bool) -> Specification (Tx era))
-> (Term (Tx era) -> Term Bool) -> Specification (Tx era)
forall a b. (a -> b) -> a -> b
$ \Term (Tx era)
tx -> Term (Tx era)
tx Term (Tx era) -> Term (Tx era) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Tx era -> Term (Tx era)
forall a. HasSpec a => a -> Term a
lit Tx era
uecTx

correctAddrAndWFCoin ::
  Term (TxOut ConwayEra) ->
  Pred
correctAddrAndWFCoin :: Term (TxOut ConwayEra) -> Pred
correctAddrAndWFCoin Term (TxOut ConwayEra)
txOut =
  Term (BabbageTxOut ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (BabbageTxOut ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (TxOut ConwayEra)
Term (BabbageTxOut ConwayEra)
txOut (FunTy
   (MapList Term (ProductAsList (BabbageTxOut ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (BabbageTxOut ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Addr
addr Term MaryValue
v TermD Deps (Datum ConwayEra)
_ TermD Deps (StrictMaybe (AlonzoScript ConwayEra))
_ ->
    [ Term MaryValue
-> FunTy (MapList Term (ProductAsList MaryValue)) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term MaryValue
v (FunTy (MapList Term (ProductAsList MaryValue)) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (ProductAsList MaryValue)) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Coin
c -> [Term Coin
0 Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Coin
c, Term Coin
c Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Word64 -> Term Coin
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64
forall a. Bounded a => a
maxBound :: Word64)]
    , (Term Addr
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Addr))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term Addr
addr)
        (FunTy
  (MapList
     Term
     (Args (Prod Network (Prod (Credential 'Payment) StakeReference))))
  (Term Bool)
-> Weighted
     (BinderD Deps)
     (Prod Network (Prod (Credential 'Payment) StakeReference))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args (Prod Network (Prod (Credential 'Payment) StakeReference))))
   (Term Bool)
 -> Weighted
      (BinderD Deps)
      (Prod Network (Prod (Credential 'Payment) StakeReference)))
-> FunTy
     (MapList
        Term
        (Args (Prod Network (Prod (Credential 'Payment) StakeReference))))
     (Term Bool)
-> Weighted
     (BinderD Deps)
     (Prod Network (Prod (Credential 'Payment) StakeReference))
forall a b. (a -> b) -> a -> b
$ \Term Network
n TermD Deps (Credential 'Payment)
_ TermD Deps StakeReference
_ -> Term Network
n Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet)
        ( FunTy (MapList Term (Args BootstrapAddress)) Pred
-> Weighted (BinderD Deps) BootstrapAddress
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args BootstrapAddress)) Pred
 -> Weighted (BinderD Deps) BootstrapAddress)
-> FunTy (MapList Term (Args BootstrapAddress)) Pred
-> Weighted (BinderD Deps) BootstrapAddress
forall a b. (a -> b) -> a -> b
$ \Term BootstrapAddress
bootstrapAddr ->
            Term BootstrapAddress
-> FunTy (MapList Term (ProductAsList BootstrapAddress)) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term BootstrapAddress
bootstrapAddr (FunTy (MapList Term (ProductAsList BootstrapAddress)) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList BootstrapAddress)) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps (AbstractHash Blake2b_224 Address')
_ Term NetworkMagic
nm TermD Deps AddrType
_ ->
              (Term NetworkMagic
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep NetworkMagic)))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term NetworkMagic
nm)
                (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
False)
                (FunTy (MapList Term (Args Word32)) Bool
-> Weighted (BinderD Deps) Word32
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Word32)) Bool
 -> Weighted (BinderD Deps) Word32)
-> FunTy (MapList Term (Args Word32)) Bool
-> Weighted (BinderD Deps) Word32
forall a b. (a -> b) -> a -> b
$ \TermD Deps Word32
_ -> Bool
True)
        )
    ]

depositsMap ::
  ConwayEraCertState era => CertState era -> Proposals era -> Map.Map DepositPurpose Coin
depositsMap :: forall era.
ConwayEraCertState era =>
CertState era -> Proposals era -> Map DepositPurpose Coin
depositsMap CertState era
certState Proposals era
props =
  [Map DepositPurpose Coin] -> Map DepositPurpose Coin
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions
    [ (Credential 'Staking -> DepositPurpose)
-> Map (Credential 'Staking) Coin -> Map DepositPurpose Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Credential 'Staking -> DepositPurpose
CredentialDeposit (Map (Credential 'Staking) Coin -> Map DepositPurpose Coin)
-> Map (Credential 'Staking) Coin -> Map DepositPurpose Coin
forall a b. (a -> b) -> a -> b
$
        (AccountState era -> Coin)
-> Map (Credential 'Staking) (AccountState era)
-> Map (Credential 'Staking) Coin
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
          (CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (AccountState era -> CompactForm Coin)
-> AccountState era
-> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AccountState era
-> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
-> CompactForm Coin
forall s a. s -> Getting a s a -> a
^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState era) (CompactForm Coin)
depositAccountStateL))
          (CertState era
certState CertState era
-> Getting
     (Map (Credential 'Staking) (AccountState era))
     (CertState era)
     (Map (Credential 'Staking) (AccountState era))
-> Map (Credential 'Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (DState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (DState era))
-> CertState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era
  -> Const
       (Map (Credential 'Staking) (AccountState era)) (DState era))
 -> CertState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (CertState era))
-> ((Map (Credential 'Staking) (AccountState era)
     -> Const
          (Map (Credential 'Staking) (AccountState era))
          (Map (Credential 'Staking) (AccountState era)))
    -> DState era
    -> Const
         (Map (Credential 'Staking) (AccountState era)) (DState era))
-> Getting
     (Map (Credential 'Staking) (AccountState era))
     (CertState era)
     (Map (Credential 'Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential 'Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (DState era))
-> ((Map (Credential 'Staking) (AccountState era)
     -> Const
          (Map (Credential 'Staking) (AccountState era))
          (Map (Credential 'Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential 'Staking) (AccountState era)) (Accounts era))
-> (Map (Credential 'Staking) (AccountState era)
    -> Const
         (Map (Credential 'Staking) (AccountState era))
         (Map (Credential 'Staking) (AccountState era)))
-> DState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) (AccountState era)
 -> Const
      (Map (Credential 'Staking) (AccountState era))
      (Map (Credential 'Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
accountsMapL)
    , (KeyHash 'StakePool -> DepositPurpose)
-> Map (KeyHash 'StakePool) Coin -> Map DepositPurpose Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys KeyHash 'StakePool -> DepositPurpose
PoolDeposit (Map (KeyHash 'StakePool) Coin -> Map DepositPurpose Coin)
-> Map (KeyHash 'StakePool) Coin -> Map DepositPurpose Coin
forall a b. (a -> b) -> a -> b
$ CertState era
certState CertState era
-> Getting
     (Map (KeyHash 'StakePool) Coin)
     (CertState era)
     (Map (KeyHash 'StakePool) Coin)
-> Map (KeyHash 'StakePool) Coin
forall s a. s -> Getting a s a -> a
^. (PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) Coin) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Const
          (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
-> Getting
     (Map (KeyHash 'StakePool) Coin)
     (CertState era)
     (Map (KeyHash 'StakePool) Coin)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) Coin
 -> Const
      (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
-> PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) Coin
 -> f (Map (KeyHash 'StakePool) Coin))
-> PState era -> f (PState era)
psDepositsL
    , (DRepState -> Coin)
-> Map DepositPurpose DRepState -> Map DepositPurpose Coin
forall a b.
(a -> b) -> Map DepositPurpose a -> Map DepositPurpose b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (DRepState -> CompactForm Coin) -> DRepState -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DRepState -> CompactForm Coin
drepDeposit) (Map DepositPurpose DRepState -> Map DepositPurpose Coin)
-> (Map (Credential 'DRepRole) DRepState
    -> Map DepositPurpose DRepState)
-> Map (Credential 'DRepRole) DRepState
-> Map DepositPurpose Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Credential 'DRepRole -> DepositPurpose)
-> Map (Credential 'DRepRole) DRepState
-> Map DepositPurpose DRepState
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Credential 'DRepRole -> DepositPurpose
DRepDeposit (Map (Credential 'DRepRole) DRepState -> Map DepositPurpose Coin)
-> Map (Credential 'DRepRole) DRepState -> Map DepositPurpose Coin
forall a b. (a -> b) -> a -> b
$ CertState era
certState CertState era
-> Getting
     (Map (Credential 'DRepRole) DRepState)
     (CertState era)
     (Map (Credential 'DRepRole) DRepState)
-> Map (Credential 'DRepRole) DRepState
forall s a. s -> Getting a s a -> a
^. (VState era
 -> Const (Map (Credential 'DRepRole) DRepState) (VState era))
-> CertState era
-> Const (Map (Credential 'DRepRole) DRepState) (CertState era)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState era) (VState era)
certVStateL ((VState era
  -> Const (Map (Credential 'DRepRole) DRepState) (VState era))
 -> CertState era
 -> Const (Map (Credential 'DRepRole) DRepState) (CertState era))
-> ((Map (Credential 'DRepRole) DRepState
     -> Const
          (Map (Credential 'DRepRole) DRepState)
          (Map (Credential 'DRepRole) DRepState))
    -> VState era
    -> Const (Map (Credential 'DRepRole) DRepState) (VState era))
-> Getting
     (Map (Credential 'DRepRole) DRepState)
     (CertState era)
     (Map (Credential 'DRepRole) DRepState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'DRepRole) DRepState
 -> Const
      (Map (Credential 'DRepRole) DRepState)
      (Map (Credential 'DRepRole) DRepState))
-> VState era
-> Const (Map (Credential 'DRepRole) DRepState) (VState era)
forall era (f :: * -> *).
Functor f =>
(Map (Credential 'DRepRole) DRepState
 -> f (Map (Credential 'DRepRole) DRepState))
-> VState era -> f (VState era)
vsDRepsL
    , [(DepositPurpose, Coin)] -> Map DepositPurpose Coin
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(DepositPurpose, Coin)] -> Map DepositPurpose Coin)
-> ([(GovActionId, GovActionState era)]
    -> [(DepositPurpose, Coin)])
-> [(GovActionId, GovActionState era)]
-> Map DepositPurpose Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((GovActionId, GovActionState era) -> (DepositPurpose, Coin))
-> [(GovActionId, GovActionState era)] -> [(DepositPurpose, Coin)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((GovActionId -> DepositPurpose)
-> (GovActionState era -> Coin)
-> (GovActionId, GovActionState era)
-> (DepositPurpose, Coin)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap GovActionId -> DepositPurpose
GovActionDeposit GovActionState era -> Coin
forall era. GovActionState era -> Coin
gasDeposit) ([(GovActionId, GovActionState era)] -> Map DepositPurpose Coin)
-> [(GovActionId, GovActionState era)] -> Map DepositPurpose Coin
forall a b. (a -> b) -> a -> b
$ OMap GovActionId (GovActionState era)
-> [(GovActionId, GovActionState era)]
forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList (Proposals era
props Proposals era
-> Getting
     (OMap GovActionId (GovActionState era))
     (Proposals era)
     (OMap GovActionId (GovActionState era))
-> OMap GovActionId (GovActionState era)
forall s a. s -> Getting a s a -> a
^. Getting
  (OMap GovActionId (GovActionState era))
  (Proposals era)
  (OMap GovActionId (GovActionState era))
forall era (f :: * -> *).
Functor f =>
(OMap GovActionId (GovActionState era)
 -> f (OMap GovActionId (GovActionState era)))
-> Proposals era -> f (Proposals era)
pPropsL)
    ]