{-# 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.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (
  Era (..),
  EraPParams (..),
  EraTx,
  EraTxAuxData (..),
  EraTxBody (..),
  EraTxWits (..),
 )
import Cardano.Ledger.Conway.Governance (GovActionId, Proposals, gasDeposit, pPropsL)
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.Tx (AlonzoTx)
import Cardano.Ledger.Shelley.API.Types
import Cardano.Ledger.Shelley.Rules (Identity, epochFromSlot, utxoEnvCertStateL)
import Cardano.Ledger.UMap (depositMap)
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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term DepositPurpose
[var|depPurpose|] ->
  (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term DepositPurpose
depPurpose)
    -- CredentialDeposit !(Credential 'Staking c)
    (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
cred -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
cred)
    -- PoolDeposit !(KeyHash 'StakePool c)
    (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'StakePool)
keyhash -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (KeyHash 'StakePool)
keyhash)
    -- DRepDeposit !(Credential 'DRepRole c)
    (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
drep -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'DRepRole)
drep)
    -- GovActionDeposit
    (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term GovActionId
_ -> Bool
True)

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

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

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

instance EncCBOR DepositPurpose where
  encCBOR :: DepositPurpose -> Encoding
encCBOR =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      CredentialDeposit Credential 'Staking
c -> forall t. t -> Word -> Encode 'Open t
Sum Credential 'Staking -> DepositPurpose
CredentialDeposit Word
0 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Credential 'Staking
c
      PoolDeposit KeyHash 'StakePool
kh -> forall t. t -> Word -> Encode 'Open t
Sum KeyHash 'StakePool -> DepositPurpose
PoolDeposit Word
1 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To KeyHash 'StakePool
kh
      DRepDeposit Credential 'DRepRole
c -> forall t. t -> Word -> Encode 'Open t
Sum Credential 'DRepRole -> DepositPurpose
DRepDeposit Word
2 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Credential 'DRepRole
c
      GovActionDeposit GovActionId
gaid -> forall t. t -> Word -> Encode 'Open t
Sum GovActionId -> DepositPurpose
GovActionDeposit Word
3 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> 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 {UTxO ConwayEra
AlonzoTx ConwayEra
UtxoEnv ConwayEra
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecTx :: forall era. UtxoExecContext era -> AlonzoTx era
uecUtxoEnv :: UtxoEnv ConwayEra
uecUTxO :: UTxO ConwayEra
uecTx :: AlonzoTx ConwayEra
..} =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (UtxoEnv ConwayEra)
utxoEnv ->
    Term (UtxoEnv ConwayEra)
utxoEnv forall a. HasSpec a => Term a -> Term a -> Term Bool
==. 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 :: UTxO ConwayEra
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUTxO} UtxoEnv {SlotNo
ueSlot :: forall era. UtxoEnv era -> SlotNo
ueSlot :: SlotNo
ueSlot, CertState ConwayEra
ueCertState :: forall era. UtxoEnv era -> CertState era
ueCertState :: CertState ConwayEra
ueCertState} =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (UTxOState ConwayEra)
utxoState ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (UTxOState ConwayEra)
utxoState forall a b. (a -> b) -> a -> b
$
      \Term (UTxO ConwayEra)
utxosUtxo
       Term Coin
_utxosDeposited
       Term Coin
_utxosFees
       Term (ConwayGovState ConwayEra)
utxosGovState
       Term (ConwayInstantStake ConwayEra)
_utxosStakeDistr
       Term Coin
_utxosDonation ->
          [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (UTxO ConwayEra)
utxosUtxo forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit UTxO ConwayEra
uecUTxO
          , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayGovState ConwayEra)
utxosGovState forall a b. (a -> b) -> a -> b
$ \Term (Proposals ConwayEra)
props Term (StrictMaybe (Committee ConwayEra))
_ Term (Constitution ConwayEra)
constitution Term (PParams ConwayEra)
_ Term (PParams ConwayEra)
_ Term (FuturePParams ConwayEra)
_ Term (DRepPulsingState ConwayEra)
_ ->
              forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Constitution ConwayEra)
constitution forall a b. (a -> b) -> a -> b
$ \Term Anchor
_ Term (StrictMaybe ScriptHash)
policy ->
                forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Proposals ConwayEra)
props forall a b. (a -> b) -> a -> b
$ Term EpochNo
-> Term (StrictMaybe ScriptHash)
-> Term (CertState ConwayEra)
-> Specification (Proposals ConwayEra)
proposalsSpec (forall a. HasSpec a => a -> Term a
lit EpochNo
curEpoch) Term (StrictMaybe ScriptHash)
policy (forall a. HasSpec a => a -> Term a
lit CertState ConwayEra
ueCertState)
          ]
  where
    curEpoch :: EpochNo
curEpoch = 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 -> AlonzoTx era
uecTx :: !(AlonzoTx era)
  , forall era. UtxoExecContext era -> UTxO era
uecUTxO :: !(UTxO era)
  , forall era. UtxoExecContext era -> UtxoEnv era
uecUtxoEnv :: !(UtxoEnv era)
  }
  deriving (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
$cto :: forall era x. Rep (UtxoExecContext era) x -> UtxoExecContext era
$cfrom :: forall era x. UtxoExecContext era -> Rep (UtxoExecContext era) x
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 (UtxoExecContext era)

instance
  ( EraPParams era
  , EncCBOR (TxOut era)
  , EncCBOR (TxBody era)
  , EncCBOR (TxAuxData era)
  , EncCBOR (TxWits era)
  , EraCertState era
  ) =>
  EncCBOR (UtxoExecContext era)
  where
  encCBOR :: UtxoExecContext era -> Encoding
encCBOR x :: UtxoExecContext era
x@(UtxoExecContext AlonzoTx era
_ UTxO era
_ UtxoEnv era
_) =
    let UtxoExecContext {UTxO era
AlonzoTx era
UtxoEnv era
uecUtxoEnv :: UtxoEnv era
uecUTxO :: UTxO era
uecTx :: AlonzoTx era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecTx :: forall era. UtxoExecContext era -> AlonzoTx era
..} = UtxoExecContext era
x
     in forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$
          forall t. t -> Encode ('Closed 'Dense) t
Rec forall era.
AlonzoTx era -> UTxO era -> UtxoEnv era -> UtxoExecContext era
UtxoExecContext
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To AlonzoTx era
uecTx
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To UTxO era
uecUTxO
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> 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 = (forall era. UtxoExecContext era -> UtxoEnv era
uecUtxoEnv UtxoExecContext era
ctx) forall s a. s -> Getting a s a -> a
^. forall era. Lens' (UtxoEnv era) (CertState era)
utxoEnvCertStateL

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

correctAddrAndWFCoin ::
  Term (TxOut ConwayEra) ->
  Pred
correctAddrAndWFCoin :: Term (TxOut ConwayEra) -> Pred
correctAddrAndWFCoin Term (TxOut ConwayEra)
txOut =
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (TxOut ConwayEra)
txOut forall a b. (a -> b) -> a -> b
$ \Term Addr
addr Term MaryValue
v Term (Datum ConwayEra)
_ Term (StrictMaybe (AlonzoScript ConwayEra))
_ ->
    [ forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term MaryValue
v forall a b. (a -> b) -> a -> b
$ \Term Coin
c -> [Term Coin
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Coin
c, Term Coin
c forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word64)]
    , (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term Addr
addr)
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Network
n Term (Credential 'Payment)
_ Term StakeReference
_ -> Term Network
n forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Network
Testnet)
        ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term BootstrapAddress
bootstrapAddr ->
            forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term BootstrapAddress
bootstrapAddr forall a b. (a -> b) -> a -> b
$ \Term (AbstractHash Blake2b_224 Address')
_ Term NetworkMagic
nm Term AddrType
_ ->
              (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term NetworkMagic
nm)
                (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
False)
                (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term 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 =
  forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions
    [ forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Credential 'Staking -> DepositPurpose
CredentialDeposit forall a b. (a -> b) -> a -> b
$ UMap -> Map (Credential 'Staking) Coin
depositMap (CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) UMap
dsUnifiedL)
    , forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys KeyHash 'StakePool -> DepositPurpose
PoolDeposit forall a b. (a -> b) -> a -> b
$ CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (PState era) (Map (KeyHash 'StakePool) Coin)
psDepositsL
    , forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DRepState -> Coin
drepDeposit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Credential 'DRepRole -> DepositPurpose
DRepDeposit forall a b. (a -> b) -> a -> b
$ CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
certVStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
Lens' (VState era) (Map (Credential 'DRepRole) DRepState)
vsDRepsL
    , forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap GovActionId -> DepositPurpose
GovActionDeposit forall era. GovActionState era -> Coin
gasDeposit) forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList (Proposals era
props forall s a. s -> Getting a s a -> a
^. forall era.
Lens' (Proposals era) (OMap GovActionId (GovActionState era))
pPropsL)
    ]