{-# 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.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.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.Rules (Identity, epochFromSlot, utxoEnvCertStateL)
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.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 IsConwayUniv fn => HasSpec fn DepositPurpose

witnessDepositPurpose ::
  forall fn era.
  (Era era, IsConwayUniv fn) =>
  WitUniv era -> Specification fn DepositPurpose
witnessDepositPurpose :: forall (fn :: [*] -> * -> *) era.
(Era era, IsConwayUniv fn) =>
WitUniv era -> Specification fn DepositPurpose
witnessDepositPurpose WitUniv era
univ = 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 DepositPurpose
[var|depPurpose|] ->
  (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 DepositPurpose
depPurpose)
    -- CredentialDeposit !(Credential 'Staking c)
    (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 (Credential 'Staking)
cred -> forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'Staking)
cred)
    -- PoolDeposit !(KeyHash 'StakePool c)
    (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 (KeyHash 'StakePool)
keyhash -> forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (KeyHash 'StakePool)
keyhash)
    -- DRepDeposit !(Credential 'DRepRole c)
    (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 (Credential 'DRepRole)
drep -> forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'DRepRole)
drep)
    -- GovActionDeposit
    (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 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 ::
  IsConwayUniv fn =>
  UtxoExecContext ConwayEra ->
  Specification fn (UtxoEnv ConwayEra)
utxoEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext ConwayEra -> Specification fn (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 (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 ConwayEra)
utxoEnv ->
    Term fn (UtxoEnv ConwayEra)
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 ConwayEra
uecUtxoEnv

utxoStateSpec ::
  IsConwayUniv fn =>
  UtxoExecContext ConwayEra ->
  UtxoEnv ConwayEra ->
  Specification fn (UTxOState ConwayEra)
utxoStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification fn (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 (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 ConwayEra)
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 ConwayEra)
utxoState forall a b. (a -> b) -> a -> b
$
      \Term fn (UTxO ConwayEra)
utxosUtxo
       Term fn Coin
_utxosDeposited
       Term fn Coin
_utxosFees
       Term fn (ConwayGovState ConwayEra)
utxosGovState
       Term fn (ConwayInstantStake ConwayEra)
_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 ConwayEra)
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 ConwayEra
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 ConwayEra)
utxosGovState forall a b. (a -> b) -> a -> b
$ \Term fn (Proposals ConwayEra)
props Term fn (StrictMaybe (Committee ConwayEra))
_ Term fn (Constitution ConwayEra)
constitution Term fn (PParams ConwayEra)
_ Term fn (PParams ConwayEra)
_ Term fn (FuturePParams ConwayEra)
_ Term fn (DRepPulsingState ConwayEra)
_ ->
              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 ConwayEra)
constitution forall a b. (a -> b) -> a -> b
$ \Term fn Anchor
_ Term fn (StrictMaybe ScriptHash)
policy ->
                forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Proposals ConwayEra)
props forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn EpochNo
-> Term fn (StrictMaybe ScriptHash)
-> Term fn (CertState ConwayEra)
-> Specification fn (Proposals ConwayEra)
proposalsSpec (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit EpochNo
curEpoch) Term fn (StrictMaybe ScriptHash)
policy (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn 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 ::
  ( 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) ->
  Pred fn
correctAddrAndWFCoin :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (TxOut ConwayEra) -> Pred fn
correctAddrAndWFCoin Term fn (TxOut ConwayEra)
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 ConwayEra)
txOut forall a b. (a -> b) -> a -> b
$ \Term fn Addr
addr Term fn MaryValue
v Term fn (Datum ConwayEra)
_ Term fn (StrictMaybe (AlonzoScript ConwayEra))
_ ->
    [ 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
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
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)
_ Term fn StakeReference
_ -> 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
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
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 ::
  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)
    ]