{-# 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 (..),
  decodeRecordSum,
  encodeListLen,
  encodeWord,
 )
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (
  Era (..),
  EraPParams (..),
  EraTx (..),
  EraTxAuxData (..),
  EraTxWits (..),
  TxLevel (..),
  ppMaxTxSizeL,
 )
import Cardano.Ledger.Conway.Governance (GovActionId)
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Shelley.API.Types
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.Slot (epochFromSlot)
import Constrained.API
import Control.DeepSeq (NFData)
import Control.Monad.Reader (runReader)
import Data.Functor.Identity (Identity)
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, succVersionOrCurrent)
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 = Text
-> (Word -> Decoder s (Int, DepositPurpose))
-> Decoder s DepositPurpose
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"DepositPurpose" ((Word -> Decoder s (Int, DepositPurpose))
 -> Decoder s DepositPurpose)
-> (Word -> Decoder s (Int, DepositPurpose))
-> Decoder s DepositPurpose
forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> do
      c <- Decoder s (Credential Staking)
forall s. Decoder s (Credential Staking)
forall a s. DecCBOR a => Decoder s a
decCBOR
      pure (2, CredentialDeposit c)
    Word
1 -> do
      kh <- Decoder s (KeyHash StakePool)
forall s. Decoder s (KeyHash StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
      pure (2, PoolDeposit kh)
    Word
2 -> do
      c <- Decoder s (Credential DRepRole)
forall s. Decoder s (Credential DRepRole)
forall a s. DecCBOR a => Decoder s a
decCBOR
      pure (2, DRepDeposit c)
    Word
3 -> do
      gaid <- Decoder s GovActionId
forall s. Decoder s GovActionId
forall a s. DecCBOR a => Decoder s a
decCBOR
      pure (2, GovActionDeposit gaid)
    Word
k -> Word -> Decoder s (Int, DepositPurpose)
forall a (m :: * -> *). (Typeable a, MonadFail m) => Word -> m a
invalidKey Word
k

instance EncCBOR DepositPurpose where
  encCBOR :: DepositPurpose -> Encoding
encCBOR = \case
    CredentialDeposit Credential Staking
c -> Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
encodeWord Word
0 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Credential Staking -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Credential Staking
c
    PoolDeposit KeyHash StakePool
kh -> Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
encodeWord Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash StakePool
kh
    DRepDeposit Credential DRepRole
c -> Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
encodeWord Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Credential DRepRole -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Credential DRepRole
c
    GovActionDeposit GovActionId
gaid -> Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
encodeWord Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> GovActionId -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR GovActionId
gaid

instance NFData DepositPurpose

instance ToExpr DepositPurpose

utxoEnvSpec ::
  UtxoExecContext ConwayEra ->
  Specification (UtxoEnv ConwayEra)
utxoEnvSpec :: UtxoExecContext ConwayEra -> Specification (UtxoEnv ConwayEra)
utxoEnvSpec UtxoExecContext {Tx TopTx ConwayEra
UTxO ConwayEra
UtxoEnv ConwayEra
uecTx :: Tx TopTx ConwayEra
uecUTxO :: UTxO ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecTx :: forall era. UtxoExecContext era -> Tx TopTx 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, PParams ConwayEra
uePParams :: PParams ConwayEra
uePParams :: forall era. UtxoEnv era -> PParams era
uePParams, 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 Version
-> Term (StrictMaybe ScriptHash)
-> Term (CertState ConwayEra)
-> Specification (Proposals ConwayEra)
proposalsSpec
                    (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
curEpoch)
                    (Version -> Term Version
forall a. HasSpec a => a -> Term a
lit (ProtVer -> Version
succVersionOrCurrent (PParams ConwayEra
uePParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL)))
                    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 TopTx era
uecTx :: !(Tx TopTx 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 TopTx era)
  , ToExpr (TxWits era)
  , ToExpr (TxAuxData era)
  , ToExpr (PParamsHKD Identity era)
  , EraCertState era
  , ToExpr (CertState era)
  , ToExpr (Tx TopTx era)
  ) =>
  ToExpr (UtxoExecContext era)

instance
  ( EraPParams era
  , EncCBOR (TxOut era)
  , EncCBOR (Tx TopTx era)
  , EraCertState era
  ) =>
  EncCBOR (UtxoExecContext era)
  where
  encCBOR :: UtxoExecContext era -> Encoding
encCBOR x :: UtxoExecContext era
x@(UtxoExecContext Tx TopTx era
_ UTxO era
_ UtxoEnv era
_) =
    let UtxoExecContext {Tx TopTx era
UTxO era
UtxoEnv era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecTx :: forall era. UtxoExecContext era -> Tx TopTx era
uecTx :: Tx TopTx era
uecUTxO :: UTxO era
uecUtxoEnv :: UtxoEnv era
..} = UtxoExecContext era
x
     in Word -> Encoding
encodeListLen Word
3
          Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Tx TopTx era -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Tx TopTx era
uecTx
          Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> UTxO era -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR UTxO era
uecUTxO
          Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> UtxoEnv era -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR 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)
Shelley.utxoEnvCertStateL

utxoTxSpec ::
  HasSpec (Tx TopTx era) =>
  UtxoExecContext era ->
  Specification (Tx TopTx era)
utxoTxSpec :: forall era.
HasSpec (Tx TopTx era) =>
UtxoExecContext era -> Specification (Tx TopTx era)
utxoTxSpec UtxoExecContext {Tx TopTx era
uecTx :: forall era. UtxoExecContext era -> Tx TopTx era
uecTx :: Tx TopTx era
uecTx} =
  (Term (Tx TopTx era) -> Term Bool) -> Specification (Tx TopTx era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tx TopTx era) -> Term Bool)
 -> Specification (Tx TopTx era))
-> (Term (Tx TopTx era) -> Term Bool)
-> Specification (Tx TopTx era)
forall a b. (a -> b) -> a -> b
$ \Term (Tx TopTx era)
tx -> Term (Tx TopTx era)
tx Term (Tx TopTx era) -> Term (Tx TopTx era) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Tx TopTx era -> Term (Tx TopTx era)
forall a. HasSpec a => a -> Term a
lit Tx TopTx 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
  ueSlot <- Gen SlotNo
forall a. Arbitrary a => Gen a
arbitrary
  let
    genSize =
      GenSize
GenSize.small
        { invalidScriptFreq = 0 -- TODO make the test work with invalid scripts
        , regCertFreq = 0
        , delegCertFreq = 0
        }
  ((uecUTxO, uecTx), gs) <- runGenRS genSize $ genAlonzoTx ueSlot
  let
    txSize = Tx TopTx ConwayEra
uecTx Tx TopTx ConwayEra
-> Getting Word32 (Tx TopTx ConwayEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (Tx TopTx ConwayEra) Word32
forall era (l :: TxLevel).
(EraTx era, HasCallStack) =>
SimpleGetter (Tx l era) Word32
SimpleGetter (Tx TopTx ConwayEra) Word32
forall (l :: TxLevel).
HasCallStack =>
SimpleGetter (Tx l ConwayEra) Word32
sizeTxF
    lState = GenState ConwayEra -> LedgerState ConwayEra
forall era. Reflect era => GenState era -> LedgerState era
initialLedgerState GenState ConwayEra
gs
    ueCertState = LedgerState ConwayEra -> CertState ConwayEra
forall era. LedgerState era -> CertState era
lsCertState LedgerState ConwayEra
lState
    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
.~ Word32 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
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 {PParams ConwayEra
CertState ConwayEra
SlotNo
ueSlot :: SlotNo
uePParams :: PParams ConwayEra
ueCertState :: CertState ConwayEra
ueSlot :: SlotNo
ueCertState :: CertState ConwayEra
uePParams :: PParams ConwayEra
..}
  pure UtxoExecContext {..}