{-# 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 TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
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 (..),
EraTxWits (..),
ppMaxTxSizeL,
)
import Cardano.Ledger.Conway.Governance (GovActionId)
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.Word
import GHC.Generics (Generic)
import Lens.Micro ((&), (.~), (^.))
import Test.Cardano.Ledger.Babbage.Arbitrary ()
import Test.Cardano.Ledger.Common (Arbitrary (..), Gen, 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)
import Test.Cardano.Ledger.Generic.GenState (
GenEnv (..),
GenSize (..),
GenState (..),
initialLedgerState,
runGenRS,
)
import qualified Test.Cardano.Ledger.Generic.GenState as GenSize
import Test.Cardano.Ledger.Generic.Instances ()
import Test.Cardano.Ledger.Generic.TxGen (genAlonzoTx)
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)
(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)
(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)
(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)
(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)
)
]
genUtxoExecContext :: Gen (UtxoExecContext ConwayEra)
genUtxoExecContext :: Gen (UtxoExecContext ConwayEra)
genUtxoExecContext = do
SlotNo
ueSlot <- Gen SlotNo
forall a. Arbitrary a => Gen a
arbitrary
let
genSize :: GenSize
genSize =
GenSize
GenSize.small
{ invalidScriptFreq = 0
, regCertFreq = 0
, delegCertFreq = 0
}
((UTxO ConwayEra
uecUTxO, Tx ConwayEra
uecTx), GenState ConwayEra
gs) <- GenSize
-> GenRS ConwayEra (UTxO ConwayEra, Tx ConwayEra)
-> Gen ((UTxO ConwayEra, Tx ConwayEra), GenState ConwayEra)
forall era a.
EraGenericGen era =>
GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS GenSize
genSize (GenRS ConwayEra (UTxO ConwayEra, Tx ConwayEra)
-> Gen ((UTxO ConwayEra, Tx ConwayEra), GenState ConwayEra))
-> GenRS ConwayEra (UTxO ConwayEra, Tx ConwayEra)
-> Gen ((UTxO ConwayEra, Tx ConwayEra), GenState ConwayEra)
forall a b. (a -> b) -> a -> b
$ SlotNo -> GenRS ConwayEra (UTxO ConwayEra, Tx ConwayEra)
forall era.
EraGenericGen era =>
SlotNo -> GenRS era (UTxO era, Tx era)
genAlonzoTx SlotNo
ueSlot
let
txSize :: Integer
txSize = Tx ConwayEra
uecTx Tx ConwayEra -> Getting Integer (Tx ConwayEra) Integer -> Integer
forall s a. s -> Getting a s a -> a
^. Getting Integer (Tx ConwayEra) Integer
forall era. EraTx era => SimpleGetter (Tx era) Integer
SimpleGetter (Tx ConwayEra) Integer
sizeTxF
lState :: LedgerState ConwayEra
lState = GenState ConwayEra -> LedgerState ConwayEra
forall era. Reflect era => GenState era -> LedgerState era
initialLedgerState GenState ConwayEra
gs
ueCertState :: CertState ConwayEra
ueCertState = LedgerState ConwayEra -> CertState ConwayEra
forall era. LedgerState era -> CertState era
lsCertState LedgerState ConwayEra
lState
uePParams :: PParams ConwayEra
uePParams =
GenEnv ConwayEra -> PParams ConwayEra
forall era. GenEnv era -> PParams era
gePParams (GenState ConwayEra -> GenEnv ConwayEra
forall era. GenState era -> GenEnv era
gsGenEnv GenState ConwayEra
gs)
PParams ConwayEra
-> (PParams ConwayEra -> PParams ConwayEra) -> PParams ConwayEra
forall a b. a -> (a -> b) -> b
& (Word32 -> Identity Word32)
-> PParams ConwayEra -> Identity (PParams ConwayEra)
forall era. EraPParams era => Lens' (PParams era) Word32
Lens' (PParams ConwayEra) Word32
ppMaxTxSizeL ((Word32 -> Identity Word32)
-> PParams ConwayEra -> Identity (PParams ConwayEra))
-> Word32 -> PParams ConwayEra -> PParams ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Integer -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
txSize
PParams ConwayEra
-> (PParams ConwayEra -> PParams ConwayEra) -> PParams ConwayEra
forall a b. a -> (a -> b) -> b
& (ProtVer -> Identity ProtVer)
-> PParams ConwayEra -> Identity (PParams ConwayEra)
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL ((ProtVer -> Identity ProtVer)
-> PParams ConwayEra -> Identity (PParams ConwayEra))
-> ProtVer -> PParams ConwayEra -> PParams ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Version -> Natural -> ProtVer
ProtVer (forall (v :: Natural).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @10) Natural
0
uecUtxoEnv :: UtxoEnv ConwayEra
uecUtxoEnv = UtxoEnv {PParams ConwayEra
CertState ConwayEra
SlotNo
ueSlot :: SlotNo
ueCertState :: CertState ConwayEra
ueSlot :: SlotNo
ueCertState :: CertState ConwayEra
uePParams :: PParams ConwayEra
uePParams :: PParams ConwayEra
..}
UtxoExecContext ConwayEra -> Gen (UtxoExecContext ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UtxoExecContext {Tx ConwayEra
UTxO ConwayEra
UtxoEnv ConwayEra
uecTx :: Tx ConwayEra
uecUTxO :: UTxO ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
uecUTxO :: UTxO ConwayEra
uecTx :: Tx ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
..}