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

-- | 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.Shelley.API.Types
import Data.Word

import Constrained

import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Decode (..), Encode (..), decode, encode, (!>), (<!))
import Cardano.Ledger.CertState (
  DRepState (..),
  certDStateL,
  certPStateL,
  certVStateL,
  dsUnifiedL,
  psDepositsL,
  vsDRepsL,
 )
import Cardano.Ledger.Conway (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.Tx (AlonzoTx)
import Cardano.Ledger.Crypto (Crypto, StandardCrypto)
import Cardano.Ledger.Shelley.Rules (Identity, epochFromSlot)
import Cardano.Ledger.UMap (depositMap)
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 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.Instances
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Conway.TreeDiff ()
import Test.Cardano.Ledger.Core.Utils (testGlobals)

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

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

instance Crypto c => DecCBOR (DepositPurpose c) where
  decCBOR :: forall s. Decoder s (DepositPurpose c)
decCBOR =
    forall (w :: Wrapped) t s. 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 forall c. Credential 'Staking c -> DepositPurpose c
CredentialDeposit forall (w1 :: Wrapped) a t (w :: Density).
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 forall c. KeyHash 'StakePool c -> DepositPurpose c
PoolDeposit forall (w1 :: Wrapped) a t (w :: Density).
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 forall c. Credential 'DRepRole c -> DepositPurpose c
DRepDeposit forall (w1 :: Wrapped) a t (w :: Density).
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 forall c. GovActionId c -> DepositPurpose c
GovActionDeposit forall (w1 :: Wrapped) a t (w :: Density).
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 Crypto c => EncCBOR (DepositPurpose c) where
  encCBOR :: DepositPurpose c -> 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
c -> forall t. t -> Word -> Encode 'Open t
Sum forall c. Credential 'Staking c -> DepositPurpose c
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
c
      PoolDeposit KeyHash 'StakePool c
kh -> forall t. t -> Word -> Encode 'Open t
Sum forall c. KeyHash 'StakePool c -> DepositPurpose c
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 c
kh
      DRepDeposit Credential 'DRepRole c
c -> forall t. t -> Word -> Encode 'Open t
Sum forall c. Credential 'DRepRole c -> DepositPurpose c
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
c
      GovActionDeposit GovActionId c
gaid -> forall t. t -> Word -> Encode 'Open t
Sum forall c. GovActionId c -> DepositPurpose c
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 c
gaid

instance Crypto c => NFData (DepositPurpose c)

instance ToExpr (DepositPurpose c)

utxoEnvSpec ::
  IsConwayUniv fn =>
  UtxoExecContext Conway ->
  Specification fn (UtxoEnv (ConwayEra StandardCrypto))
utxoEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext Conway -> Specification fn (UtxoEnv Conway)
utxoEnvSpec UtxoExecContext {AlonzoTx Conway
UTxO Conway
UtxoEnv Conway
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecTx :: forall era. UtxoExecContext era -> AlonzoTx era
uecUtxoEnv :: UtxoEnv Conway
uecUTxO :: UTxO Conway
uecTx :: AlonzoTx Conway
..} =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (UtxoEnv Conway)
utxoEnv ->
    Term fn (UtxoEnv Conway)
utxoEnv forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit UtxoEnv Conway
uecUtxoEnv

utxoStateSpec ::
  IsConwayUniv fn =>
  UtxoExecContext (ConwayEra StandardCrypto) ->
  UtxoEnv (ConwayEra StandardCrypto) ->
  Specification fn (UTxOState (ConwayEra StandardCrypto))
utxoStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext Conway
-> UtxoEnv Conway -> Specification fn (UTxOState Conway)
utxoStateSpec UtxoExecContext {UTxO Conway
uecUTxO :: UTxO Conway
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUTxO} UtxoEnv {SlotNo
ueSlot :: forall era. UtxoEnv era -> SlotNo
ueSlot :: SlotNo
ueSlot, CertState Conway
ueCertState :: forall era. UtxoEnv era -> CertState era
ueCertState :: CertState Conway
ueCertState} =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (UTxOState Conway)
utxoState ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (UTxOState Conway)
utxoState forall a b. (a -> b) -> a -> b
$
      \Term fn (UTxO Conway)
utxosUtxo
       Term fn Coin
_utxosDeposited
       Term fn Coin
_utxosFees
       Term fn (ConwayGovState Conway)
utxosGovState
       Term fn (IncrementalStake StandardCrypto)
_utxosStakeDistr
       Term fn Coin
_utxosDonation ->
          [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (UTxO Conway)
utxosUtxo forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit UTxO Conway
uecUTxO
          , forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ConwayGovState Conway)
utxosGovState forall a b. (a -> b) -> a -> b
$ \Term fn (Proposals Conway)
props Term fn (StrictMaybe (Committee Conway))
_ Term fn (Constitution Conway)
constitution Term fn (PParams Conway)
_ Term fn (PParams Conway)
_ Term fn (FuturePParams Conway)
_ Term fn (DRepPulsingState Conway)
_ ->
              forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (Constitution Conway)
constitution forall a b. (a -> b) -> a -> b
$ \Term fn (Anchor StandardCrypto)
_ Term fn (StrictMaybe (ScriptHash StandardCrypto))
policy ->
                forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Proposals Conway)
props forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn EpochNo
-> Term fn (StrictMaybe (ScriptHash StandardCrypto))
-> CertState Conway
-> Specification fn (Proposals Conway)
proposalsSpec (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit EpochNo
curEpoch) Term fn (StrictMaybe (ScriptHash StandardCrypto))
policy CertState Conway
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)
  ) =>
  NFData (UtxoExecContext era)

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

instance
  ( EraPParams era
  , EncCBOR (TxOut era)
  , EncCBOR (TxBody era)
  , EncCBOR (TxAuxData era)
  , EncCBOR (TxWits era)
  ) =>
  EncCBOR (UtxoExecContext era)
  where
  encCBOR :: UtxoExecContext era -> Encoding
encCBOR x :: UtxoExecContext era
x@(UtxoExecContext AlonzoTx era
_ UTxO era
_ UtxoEnv era
_) =
    let UtxoExecContext {AlonzoTx era
UTxO 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 Inject (UtxoExecContext era) (CertState era) where
  inject :: UtxoExecContext era -> CertState era
inject = forall era. UtxoEnv era -> CertState era
ueCertState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. UtxoExecContext era -> UtxoEnv era
uecUtxoEnv

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

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

depositsMap :: CertState era -> Proposals era -> Map.Map (DepositPurpose (EraCrypto era)) Coin
depositsMap :: forall era.
CertState era
-> Proposals era -> Map (DepositPurpose (EraCrypto era)) 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 forall c. Credential 'Staking c -> DepositPurpose c
CredentialDeposit forall a b. (a -> b) -> a -> b
$ forall c. UMap c -> Map (Credential 'Staking c) Coin
depositMap (CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era. Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) (UMap (EraCrypto era))
dsUnifiedL)
    , forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys forall c. KeyHash 'StakePool c -> DepositPurpose c
PoolDeposit forall a b. (a -> b) -> a -> b
$ CertState era
certState forall s a. s -> Getting a s a -> a
^. forall 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 (EraCrypto era)) Coin)
psDepositsL
    , forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall c. DRepState c -> 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 forall c. Credential 'DRepRole c -> DepositPurpose c
DRepDeposit forall a b. (a -> b) -> a -> b
$ CertState era
certState forall s a. s -> Getting a s a -> a
^. forall 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 (EraCrypto era)) (DRepState (EraCrypto era)))
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 forall c. GovActionId c -> DepositPurpose c
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 (EraCrypto era)) (GovActionState era))
pPropsL)
    ]