{-# 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 #-}

-- | 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 (..),
  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)
    -- CredentialDeposit !(Credential 'Staking c)
    (FunTy (MapList Term (Args (Credential 'Staking))) Pred
-> Weighted (BinderD Deps) (Credential 'Staking)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (Credential 'Staking))) Pred
 -> Weighted (BinderD Deps) (Credential 'Staking))
-> FunTy (MapList Term (Args (Credential 'Staking))) Pred
-> Weighted (BinderD Deps) (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
cred -> WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
cred)
    -- PoolDeposit !(KeyHash 'StakePool c)
    (FunTy (MapList Term (Args (KeyHash 'StakePool))) Pred
-> Weighted (BinderD Deps) (KeyHash 'StakePool)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (KeyHash 'StakePool))) Pred
 -> Weighted (BinderD Deps) (KeyHash 'StakePool))
-> FunTy (MapList Term (Args (KeyHash 'StakePool))) Pred
-> Weighted (BinderD Deps) (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'StakePool)
keyhash -> WitUniv era -> Term (KeyHash 'StakePool) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (KeyHash 'StakePool)
keyhash)
    -- DRepDeposit !(Credential 'DRepRole c)
    (FunTy (MapList Term (Args (Credential 'DRepRole))) Pred
-> Weighted (BinderD Deps) (Credential 'DRepRole)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (Credential 'DRepRole))) Pred
 -> Weighted (BinderD Deps) (Credential 'DRepRole))
-> FunTy (MapList Term (Args (Credential 'DRepRole))) Pred
-> Weighted (BinderD Deps) (Credential 'DRepRole)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
drep -> WitUniv era -> Term (Credential 'DRepRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'DRepRole)
drep)
    -- GovActionDeposit
    (FunTy (MapList Term (Args GovActionId)) Bool
-> Weighted (BinderD Deps) GovActionId
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args GovActionId)) Bool
 -> Weighted (BinderD Deps) GovActionId)
-> FunTy (MapList Term (Args GovActionId)) Bool
-> Weighted (BinderD Deps) GovActionId
forall a b. (a -> b) -> a -> b
$ \TermD Deps GovActionId
_ -> Bool
True)

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

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

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

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

instance NFData DepositPurpose

instance ToExpr DepositPurpose

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

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

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

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

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

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

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

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

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

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 -- TODO make the test work with invalid scripts
        , 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
..}