{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Constrained.Preds.Universes
where

import qualified Cardano.Chain.Common as Byron
import qualified Cardano.Crypto.Signing as Byron
import Cardano.Ledger.Address (Addr (..), BootstrapAddress (..), bootstrapKeyHash)
import Cardano.Ledger.Allegra.Scripts (ValidityInterval (..))
import Cardano.Ledger.Alonzo.TxOut (AlonzoTxOut (..))
import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
import Cardano.Ledger.BaseTypes (
  Network (..),
  SlotNo (..),
  StrictMaybe (..),
  TxIx (..),
  inject,
  mkCertIxPartial,
 )
import qualified Cardano.Ledger.BaseTypes as Utils (Globals (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential (..), Ptr (..), StakeReference (..))
import Cardano.Ledger.DRep (DRep (..))
import Cardano.Ledger.Keys (coerceKeyRole)
import Cardano.Ledger.Keys.Bootstrap (BootstrapWitness, makeBootstrapWitness)
import Cardano.Ledger.Mary.Value (
  AssetName (..),
  MaryValue (..),
  MultiAsset (..),
  PolicyID (..),
  multiAssetFromList,
 )
import Cardano.Ledger.Plutus.Data (Data (..), Datum (..), dataToBinaryData, hashData)
import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..))
import Data.Default (Default (def))
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (IsString (..))
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes hiding (genTxOut)
import Test.Cardano.Ledger.Constrained.Combinators (genFromMap, itemFromSet, setSized)
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Rewrite (standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Scripts (allPlutusScripts, genCoreScript, spendPlutusScripts)
import Test.Cardano.Ledger.Constrained.Solver
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Core.KeyPair (KeyPair (..))
import Test.Cardano.Ledger.Generic.Functions (protocolVersion)
import Test.Cardano.Ledger.Generic.GenState (PlutusPurposeTag (..))
import Test.Cardano.Ledger.Generic.Proof
import Test.Cardano.Ledger.Shelley.Utils (epochFromSlotNo)
import qualified Test.Cardano.Ledger.Shelley.Utils as Utils
import Test.Tasty (TestTree, defaultMain)
import Test.Tasty.QuickCheck

import Cardano.Ledger.Conway.Governance (GovActionId (..), GovActionIx (..))
import Cardano.Ledger.TxIn (TxIn (..))

-- ==========================================================

data UnivSize = UnivSize
  { UnivSize -> Int
usNumTxOuts :: Int
  , UnivSize -> Int
usMaxAssets :: Int -- per Policy Id
  , UnivSize -> Int
usMaxPolicyID :: Int -- per MultiAsset
  , UnivSize -> Int
usNumMultiAsset :: Int
  , UnivSize -> Int
usNumPtr :: Int
  , UnivSize -> Int
usNumAddr :: Int
  , UnivSize -> Int
usNumKeys :: Int
  , UnivSize -> Int
usNumPools :: Int
  , UnivSize -> Int
usNumStakeKeys :: Int -- should be less than numKeys
  , UnivSize -> Int
usNumGenesisKeys :: Int -- should be less than numKeys
  , UnivSize -> Int
usNumVoteKeys :: Int -- should be less than numKeys
  , UnivSize -> Int
usNumCredentials :: Int
  , UnivSize -> Int
usNumDatums :: Int
  , UnivSize -> Int
usNumTxIn :: Int
  , UnivSize -> Int
usNumPreUtxo :: Int -- must be smaller than numTxIn
  , UnivSize -> Int
usNumColUtxo :: Int -- max size of the UTxo = numPreUtxo + numColUtxo
  , UnivSize -> Int
usNumDReps :: Int -- Should be less than the number of numCredentials
  , UnivSize -> Int
usMinCerts :: Int
  , UnivSize -> Int
usMaxCerts :: Int
  , UnivSize -> Int
usDatumFreq :: Int
  , UnivSize -> Bool
usGenerateWithdrawals :: Bool
  , UnivSize -> Int
usMinInputs :: Int
  , UnivSize -> Int
usMaxInputs :: Int
  , UnivSize -> Int
usMinCollaterals :: Int
  , UnivSize -> Int
usMaxCollaterals :: Int
  , UnivSize -> Int
usRegKeyFreq :: Int
  , UnivSize -> Int
usUnRegKeyFreq :: Int
  , UnivSize -> Bool
usAllowReRegisterPool :: Bool
  , UnivSize -> Int
usSpendScriptFreq :: Int
  , UnivSize -> Int
usCredScriptFreq :: Int
  }

instance Default UnivSize where
  def :: UnivSize
def =
    UnivSize
      { usNumTxOuts :: Int
usNumTxOuts = Int
100
      , usMaxAssets :: Int
usMaxAssets = Int
9 -- per Policy Id
      , usMaxPolicyID :: Int
usMaxPolicyID = Int
2 -- per MultiAsset
      , usNumMultiAsset :: Int
usNumMultiAsset = Int
10
      , usNumPtr :: Int
usNumPtr = Int
30
      , usNumAddr :: Int
usNumAddr = Int
200
      , usNumKeys :: Int
usNumKeys = Int
50
      , usNumPools :: Int
usNumPools = Int
40
      , usNumStakeKeys :: Int
usNumStakeKeys = Int
10 -- less than numKeys
      , usNumGenesisKeys :: Int
usNumGenesisKeys = Int
20 -- less than numKeys
      , usNumVoteKeys :: Int
usNumVoteKeys = Int
40 -- less than numKeys
      , usNumCredentials :: Int
usNumCredentials = Int
40
      , usNumDatums :: Int
usNumDatums = Int
30
      , usNumTxIn :: Int
usNumTxIn = Int
120
      , usNumPreUtxo :: Int
usNumPreUtxo = Int
100 -- must be smaller than numTxIn
      , usNumColUtxo :: Int
usNumColUtxo = Int
20 -- max size of the UTxo = numPreUtxo + numColUtxo
      , usNumDReps :: Int
usNumDReps = Int
20 -- -- Should be less than the number of numCredentials
      , usMaxCerts :: Int
usMaxCerts = Int
6
      , usMinCerts :: Int
usMinCerts = Int
4
      , usDatumFreq :: Int
usDatumFreq = Int
1
      , usGenerateWithdrawals :: Bool
usGenerateWithdrawals = Bool
True
      , usMinInputs :: Int
usMinInputs = Int
2
      , usMaxInputs :: Int
usMaxInputs = Int
10
      , usMinCollaterals :: Int
usMinCollaterals = Int
2
      , usMaxCollaterals :: Int
usMaxCollaterals = Int
2
      , usAllowReRegisterPool :: Bool
usAllowReRegisterPool = Bool
True
      , usRegKeyFreq :: Int
usRegKeyFreq = Int
1
      , usUnRegKeyFreq :: Int
usUnRegKeyFreq = Int
1
      , usSpendScriptFreq :: Int
usSpendScriptFreq = Int
3
      , usCredScriptFreq :: Int
usCredScriptFreq = Int
1
      }

-- ============================================================
-- Coins

variedCoin :: Gen Coin
variedCoin :: Gen Coin
variedCoin =
  Integer -> Coin
Coin
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
2, forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0)
      , (Int
2, forall a. Random a => (a, a) -> Gen a
choose (Integer
1, Integer
10))
      , (Int
2, forall a. Random a => (a, a) -> Gen a
choose (Integer
11, Integer
100))
      , (Int
2, forall a. Random a => (a, a) -> Gen a
choose (Integer
101, Integer
1000))
      , (Int
2, forall a. Random a => (a, a) -> Gen a
choose (Integer
1001, Integer
10000))
      , (Int
8, forall a. Random a => (a, a) -> Gen a
choose (Integer
10001, Integer
100000))
      , (Int
12, forall a. Random a => (a, a) -> Gen a
choose (Integer
100001, Integer
1000000))
      ]

noZeroCoin :: Gen Coin
noZeroCoin :: Gen Coin
noZeroCoin =
  Integer -> Coin
Coin
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
1, forall a. Random a => (a, a) -> Gen a
choose (Integer
1, Integer
10))
      , (Int
1, forall a. Random a => (a, a) -> Gen a
choose (Integer
11, Integer
1000))
      , (Int
1, forall a. Random a => (a, a) -> Gen a
choose (Integer
1001, Integer
100000))
      , (Int
6, forall a. Random a => (a, a) -> Gen a
choose (Integer
100001, Integer
600000))
      , (Int
6, forall a. Random a => (a, a) -> Gen a
choose (Integer
600001, Integer
2000000))
      , (Int
6, forall a. Random a => (a, a) -> Gen a
choose (Integer
2000001, Integer
4000000))
      ]

-- ===============================================
-- Generating Byron address and their universe

-- | Generate a pair, A Byron address, and the key that can sign it.
genAddrPair :: Network -> Gen (BootstrapAddress, Byron.SigningKey)
genAddrPair :: Network -> Gen (BootstrapAddress, SigningKey)
genAddrPair Network
netwrk = do
  SigningKey
signkey <- Gen SigningKey
genSigningKey
  let verificationKey :: VerificationKey
verificationKey = SigningKey -> VerificationKey
Byron.toVerification SigningKey
signkey
      asd :: AddrSpendingData
asd = VerificationKey -> AddrSpendingData
Byron.VerKeyASD VerificationKey
verificationKey
      byronNetwork :: NetworkMagic
byronNetwork = case Network
netwrk of
        Network
Mainnet -> NetworkMagic
Byron.NetworkMainOrStage
        Network
Testnet -> Word32 -> NetworkMagic
Byron.NetworkTestnet Word32
0
      attrs :: AddrAttributes
attrs =
        Maybe HDAddressPayload -> NetworkMagic -> AddrAttributes
Byron.AddrAttributes
          (forall a. a -> Maybe a
Just (ByteString -> HDAddressPayload
Byron.HDAddressPayload ByteString
"a compressed lenna.png"))
          NetworkMagic
byronNetwork
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Address -> BootstrapAddress
BootstrapAddress (AddrSpendingData -> AddrAttributes -> Address
Byron.makeAddress AddrSpendingData
asd AddrAttributes
attrs), SigningKey
signkey)

-- | Generate a Map, that maps the Hash of a Byron address to a pair of
--   the actual Byron address and the key that can sign it.
genByronUniv :: Network -> Gen (Map (KeyHash 'Payment) (Addr, Byron.SigningKey))
genByronUniv :: Network -> Gen (Map (KeyHash 'Payment) (Addr, SigningKey))
genByronUniv Network
netwrk = do
  [(BootstrapAddress, SigningKey)]
list <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (Network -> Gen (BootstrapAddress, SigningKey)
genAddrPair Network
netwrk)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      (forall a b. (a -> b) -> [a] -> [b]
List.map (\(BootstrapAddress
addr, SigningKey
signkey) -> (BootstrapAddress -> KeyHash 'Payment
bootstrapKeyHash BootstrapAddress
addr, (BootstrapAddress -> Addr
AddrBootstrap BootstrapAddress
addr, SigningKey
signkey))) [(BootstrapAddress, SigningKey)]
list)

-- | Given a list of Byron addresses, compute BootStrap witnesses of all of those addresses
--   Can only be used with StandardCrypto
bootWitness ::
  Hash HASH EraIndependentTxBody ->
  [BootstrapAddress] ->
  Map (KeyHash 'Payment) (Addr, Byron.SigningKey) ->
  Set BootstrapWitness
bootWitness :: Hash HASH EraIndependentTxBody
-> [BootstrapAddress]
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitness Hash HASH EraIndependentTxBody
hash [BootstrapAddress]
bootaddrs Map (KeyHash 'Payment) (Addr, SigningKey)
byronuniv = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set BootstrapWitness -> BootstrapAddress -> Set BootstrapWitness
accum forall a. Set a
Set.empty [BootstrapAddress]
bootaddrs
  where
    accum :: Set BootstrapWitness -> BootstrapAddress -> Set BootstrapWitness
accum Set BootstrapWitness
ans bootaddr :: BootstrapAddress
bootaddr@(BootstrapAddress Address
a) = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (BootstrapAddress -> KeyHash 'Payment
bootstrapKeyHash BootstrapAddress
bootaddr) Map (KeyHash 'Payment) (Addr, SigningKey)
byronuniv of
      Just (AddrBootstrap BootstrapAddress
_, SigningKey
signkey) ->
        forall a. Ord a => a -> Set a -> Set a
Set.insert (Hash HASH EraIndependentTxBody
-> SigningKey -> Attributes AddrAttributes -> BootstrapWitness
makeBootstrapWitness Hash HASH EraIndependentTxBody
hash SigningKey
signkey (Address -> Attributes AddrAttributes
Byron.addrAttributes Address
a)) Set BootstrapWitness
ans
      Maybe (Addr, SigningKey)
_ -> Set BootstrapWitness
ans

-- ==================
-- Datums

-- | The universe of non-empty Datums. i.e. There are no NoDatum Datums in this list
genDatums ::
  Era era => UnivSize -> Int -> Map DataHash (Data era) -> Gen [Datum era]
genDatums :: forall era.
Era era =>
UnivSize -> Int -> Map DataHash (Data era) -> Gen [Datum era]
genDatums UnivSize
sizes Int
n Map DataHash (Data era)
datauniv = forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era.
Era era =>
UnivSize -> Map DataHash (Data era) -> Gen (Datum era)
genDatum UnivSize
sizes Map DataHash (Data era)
datauniv)

-- | Only generate non-empty Datums. I.e. There are no NoDatum Datums generated.
genDatum :: Era era => UnivSize -> Map DataHash (Data era) -> Gen (Datum era)
genDatum :: forall era.
Era era =>
UnivSize -> Map DataHash (Data era) -> Gen (Datum era)
genDatum UnivSize {Int
usDatumFreq :: Int
usDatumFreq :: UnivSize -> Int
usDatumFreq} Map DataHash (Data era)
datauniv =
  forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
1, forall era. DataHash -> Datum era
DatumHash forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"from genDatums DatumHash case"] Map DataHash (Data era)
datauniv)
    ,
      ( Int
usDatumFreq
      , forall era. BinaryData era -> Datum era
Datum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Era era => Data era -> BinaryData era
dataToBinaryData forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"from genDatums Datum case"] Map DataHash (Data era)
datauniv
      )
    ]

-- ==============
-- TxOuts
-- ==============

genTxOut ::
  Reflect era =>
  UnivSize ->
  (Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)) ->
  Proof era ->
  Coin ->
  Set Addr ->
  Map ScriptHash (ScriptF era) ->
  Map ScriptHash (ScriptF era) ->
  Map DataHash (Data era) ->
  Gen (TxOut era)
genTxOut :: forall era.
Reflect era =>
UnivSize
-> (Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era))
-> Proof era
-> Coin
-> Set Addr
-> Map ScriptHash (ScriptF era)
-> Map ScriptHash (ScriptF era)
-> Map DataHash (Data era)
-> Gen (TxOut era)
genTxOut UnivSize
sizes Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)
genvalue Proof era
p Coin
c Set Addr
addruniv Map ScriptHash (ScriptF era)
scriptuniv Map ScriptHash (ScriptF era)
spendscriptuniv Map DataHash (Data era)
datauniv =
  case forall era. Proof era -> TxOutWit era
whichTxOut Proof era
p of
    TxOutWit era
TxOutShelleyToMary ->
      forall era.
(HasCallStack, Era era, Val (Value era)) =>
Addr -> Value era -> ShelleyTxOut era
ShelleyTxOut forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. [String] -> Set t -> Gen t
pick1 [String
"genTxOut ShelleyToMary Addr"] Set Addr
addruniv forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)
genvalue Coin
c Map ScriptHash (ScriptF era)
scriptuniv
    TxOutWit era
TxOutAlonzoToAlonzo -> do
      Addr
addr <- forall t. [String] -> Set t -> Gen t
pick1 [String
"genTxOut AlonzoToAlonzo Addr"] Set Addr
addruniv
      Value era
v <- Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)
genvalue Coin
c Map ScriptHash (ScriptF era)
scriptuniv
      case Addr
addr of
        AddrBootstrap BootstrapAddress
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr -> Value era -> StrictMaybe DataHash -> AlonzoTxOut era
AlonzoTxOut Addr
addr Value era
v forall a. StrictMaybe a
SNothing)
        Addr Network
_ PaymentCredential
paycred StakeReference
_ ->
          if forall era.
EraScript era =>
PaymentCredential -> Map ScriptHash (ScriptF era) -> Bool
needsDatum PaymentCredential
paycred Map ScriptHash (ScriptF era)
spendscriptuniv
            then
              forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr -> Value era -> StrictMaybe DataHash -> AlonzoTxOut era
AlonzoTxOut Addr
addr Value era
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> StrictMaybe a
SJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"from genTxOut, AlonzoToAlonzo, needsDatum case"] Map DataHash (Data era)
datauniv
            else forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr -> Value era -> StrictMaybe DataHash -> AlonzoTxOut era
AlonzoTxOut Addr
addr Value era
v forall a. StrictMaybe a
SNothing)
    TxOutWit era
TxOutBabbageToConway -> do
      Addr
addr <- forall t. [String] -> Set t -> Gen t
pick1 [String
"genTxOut BabbageToConway Addr"] Set Addr
addruniv
      Value era
v <- Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)
genvalue Coin
c Map ScriptHash (ScriptF era)
scriptuniv
      (ScriptF Proof era
_ Script era
refscript) <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"genTxOut, BabbageToConway, refscript case"] Map ScriptHash (ScriptF era)
scriptuniv
      StrictMaybe (Script era)
maybescript <- forall a. HasCallStack => [a] -> Gen a
elements [forall a. StrictMaybe a
SNothing, forall a. a -> StrictMaybe a
SJust Script era
refscript]
      case Addr
addr of
        AddrBootstrap BootstrapAddress
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr
-> Value era
-> Datum era
-> StrictMaybe (Script era)
-> BabbageTxOut era
BabbageTxOut Addr
addr Value era
v forall era. Datum era
NoDatum StrictMaybe (Script era)
maybescript
        Addr Network
_ PaymentCredential
paycred StakeReference
_ ->
          if forall era.
EraScript era =>
PaymentCredential -> Map ScriptHash (ScriptF era) -> Bool
needsDatum PaymentCredential
paycred Map ScriptHash (ScriptF era)
spendscriptuniv
            then forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr
-> Value era
-> Datum era
-> StrictMaybe (Script era)
-> BabbageTxOut era
BabbageTxOut Addr
addr Value era
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era.
Era era =>
UnivSize -> Map DataHash (Data era) -> Gen (Datum era)
genDatum UnivSize
sizes Map DataHash (Data era)
datauniv forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure StrictMaybe (Script era)
maybescript
            else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr
-> Value era
-> Datum era
-> StrictMaybe (Script era)
-> BabbageTxOut era
BabbageTxOut Addr
addr Value era
v forall era. Datum era
NoDatum StrictMaybe (Script era)
maybescript

needsDatum ::
  EraScript era =>
  Credential 'Payment ->
  Map ScriptHash (ScriptF era) ->
  Bool
needsDatum :: forall era.
EraScript era =>
PaymentCredential -> Map ScriptHash (ScriptF era) -> Bool
needsDatum (ScriptHashObj ScriptHash
hash) Map ScriptHash (ScriptF era)
spendScriptUniv = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScriptHash
hash Map ScriptHash (ScriptF era)
spendScriptUniv of
  Maybe (ScriptF era)
Nothing -> Bool
False
  Just (ScriptF Proof era
_ Script era
script) -> Bool -> Bool
not (forall era. EraScript era => Script era -> Bool
isNativeScript Script era
script)
needsDatum PaymentCredential
_ Map ScriptHash (ScriptF era)
_ = Bool
False

genTxOuts ::
  Reflect era =>
  UnivSize ->
  (Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)) ->
  Proof era ->
  Int ->
  Set Addr ->
  Map ScriptHash (ScriptF era) ->
  Map ScriptHash (ScriptF era) ->
  Map DataHash (Data era) ->
  Gen [TxOutF era]
genTxOuts :: forall era.
Reflect era =>
UnivSize
-> (Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era))
-> Proof era
-> Int
-> Set Addr
-> Map ScriptHash (ScriptF era)
-> Map ScriptHash (ScriptF era)
-> Map DataHash (Data era)
-> Gen [TxOutF era]
genTxOuts UnivSize
sizes Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)
genvalue Proof era
p Int
ntxouts Set Addr
addruniv Map ScriptHash (ScriptF era)
scriptuniv Map ScriptHash (ScriptF era)
spendscriptuniv Map DataHash (Data era)
datauniv = do
  let genOne :: Gen (TxOut era)
genOne = do
        Coin
c <- Gen Coin
noZeroCoin
        forall era.
Reflect era =>
UnivSize
-> (Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era))
-> Proof era
-> Coin
-> Set Addr
-> Map ScriptHash (ScriptF era)
-> Map ScriptHash (ScriptF era)
-> Map DataHash (Data era)
-> Gen (TxOut era)
genTxOut UnivSize
sizes Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)
genvalue Proof era
p Coin
c Set Addr
addruniv Map ScriptHash (ScriptF era)
scriptuniv Map ScriptHash (ScriptF era)
spendscriptuniv Map DataHash (Data era)
datauniv
  forall a. Int -> Gen a -> Gen [a]
vectorOf Int
ntxouts (forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (TxOut era)
genOne)

-- ==================================================================
-- MultiAssets

genMultiAssetTriple ::
  Map.Map ScriptHash (ScriptF era) ->
  Set AssetName ->
  Gen Integer ->
  Gen (PolicyID, AssetName, Integer)
genMultiAssetTriple :: forall era.
Map ScriptHash (ScriptF era)
-> Set AssetName
-> Gen Integer
-> Gen (PolicyID, AssetName, Integer)
genMultiAssetTriple Map ScriptHash (ScriptF era)
scriptMap Set AssetName
assetSet Gen Integer
genAmount =
  (,,)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ScriptHash -> PolicyID
PolicyID forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [] Map ScriptHash (ScriptF era)
scriptMap))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [] Set AssetName
assetSet))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Integer
genAmount

-- ===================================================================
-- Helper functions in the Gen monad.

pick1 :: [String] -> Set t -> Gen t
pick1 :: forall t. [String] -> Set t -> Gen t
pick1 [String]
msgs Set t
s = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet (String
"from pick1" forall a. a -> [a] -> [a]
: [String]
msgs) Set t
s

makeHashScriptMap ::
  Reflect era =>
  Proof era ->
  Int ->
  PlutusPurposeTag ->
  Map (KeyHash 'Witness) (KeyPair 'Witness) ->
  ValidityInterval ->
  Gen (Map ScriptHash (ScriptF era))
makeHashScriptMap :: forall era.
Reflect era =>
Proof era
-> Int
-> PlutusPurposeTag
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> ValidityInterval
-> Gen (Map ScriptHash (ScriptF era))
makeHashScriptMap Proof era
p Int
size PlutusPurposeTag
tag Map (KeyHash 'Witness) (KeyPair 'Witness)
m ValidityInterval
vi = do
  let genOne :: PlutusPurposeTag -> Gen (Script era)
genOne PlutusPurposeTag
Spending =
        -- Make an effort to get as many plutus scripts as possible (in Eras that support plutus)
        case forall era. Proof era -> ScriptWit era
whichScript Proof era
p of
          ScriptWit era
ScriptShelleyToShelley -> forall era.
Proof era
-> PlutusPurposeTag
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> ValidityInterval
-> Gen (Script era)
genCoreScript Proof era
p PlutusPurposeTag
Spending Map (KeyHash 'Witness) (KeyPair 'Witness)
m ValidityInterval
vi
          ScriptWit era
ScriptAllegraToMary -> forall era.
Proof era
-> PlutusPurposeTag
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> ValidityInterval
-> Gen (Script era)
genCoreScript Proof era
p PlutusPurposeTag
Spending Map (KeyHash 'Witness) (KeyPair 'Witness)
m ValidityInterval
vi
          ScriptWit era
ScriptAlonzoToConway ->
            forall a. HasCallStack => [Gen a] -> Gen a
oneof
              [ forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [] (forall era.
Reflect era =>
Proof era -> Map ScriptHash (IsValid, Script era)
spendPlutusScripts Proof era
p)
              , forall era.
Proof era
-> PlutusPurposeTag
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> ValidityInterval
-> Gen (Script era)
genCoreScript Proof era
p PlutusPurposeTag
Spending Map (KeyHash 'Witness) (KeyPair 'Witness)
m ValidityInterval
vi
              ]
      genOne PlutusPurposeTag
t = forall era.
Proof era
-> PlutusPurposeTag
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> ValidityInterval
-> Gen (Script era)
genCoreScript Proof era
p PlutusPurposeTag
t Map (KeyHash 'Witness) (KeyPair 'Witness)
m ValidityInterval
vi
  [Script era]
scs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
size (PlutusPurposeTag -> Gen (Script era)
genOne PlutusPurposeTag
tag)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Script era
x -> (forall era. EraScript era => Script era -> ScriptHash
hashScript Script era
x, forall era. Proof era -> Script era -> ScriptF era
ScriptF Proof era
p Script era
x)) [Script era]
scs

genDataWits ::
  Era era =>
  Proof era ->
  Int ->
  Gen (Map DataHash (Data era))
genDataWits :: forall era.
Era era =>
Proof era -> Int -> Gen (Map DataHash (Data era))
genDataWits Proof era
_p Int
size = do
  [Data era]
scs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
size forall a. Arbitrary a => Gen a
arbitrary
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Data era
x -> (forall era. Data era -> DataHash
hashData Data era
x, Data era
x)) [Data era]
scs

--  This universe must not use Byron Addresses in Babbage and Conway, as Byron Addresses
--  do not play well with plutusScripts in those eras.
genAddrWith ::
  Proof era ->
  Network ->
  Set (Credential 'Payment) ->
  Set Ptr ->
  Set (Credential 'Staking) ->
  Map (KeyHash 'Payment) (Addr, Byron.SigningKey) -> -- The Byron Addresss Universe
  Gen Addr
genAddrWith :: forall era.
Proof era
-> Network
-> Set PaymentCredential
-> Set Ptr
-> Set (Credential 'Staking)
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Gen Addr
genAddrWith Proof era
proof Network
net Set PaymentCredential
ps Set Ptr
ptrss Set (Credential 'Staking)
cs Map (KeyHash 'Payment) (Addr, SigningKey)
byronMap =
  case forall era. Proof era -> TxOutWit era
whichTxOut Proof era
proof of
    TxOutWit era
TxOutBabbageToConway -> Network -> PaymentCredential -> StakeReference -> Addr
Addr Network
net forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. [String] -> Set t -> Gen t
pick1 [String
"from genPayCred ScriptHashObj"] Set PaymentCredential
ps forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
Proof era
-> Set Ptr -> Set (Credential 'Staking) -> Gen StakeReference
genStakeRefWith Proof era
proof Set Ptr
ptrss Set (Credential 'Staking)
cs
    TxOutWit era
_ ->
      forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ (Int
8, Network -> PaymentCredential -> StakeReference -> Addr
Addr Network
net forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. [String] -> Set t -> Gen t
pick1 [String
"from genPayCred ScriptHashObj"] Set PaymentCredential
ps forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
Proof era
-> Set Ptr -> Set (Credential 'Staking) -> Gen StakeReference
genStakeRefWith Proof era
proof Set Ptr
ptrss Set (Credential 'Staking)
cs)
        , (Int
2, forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"from byronAddrUniv"] Map (KeyHash 'Payment) (Addr, SigningKey)
byronMap) -- This generates a known Byron Address
        ]

genPtr :: SlotNo -> Gen Ptr
genPtr :: SlotNo -> Gen Ptr
genPtr (SlotNo Word64
n) =
  SlotNo -> TxIx -> CertIx -> Ptr
Ptr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64 -> SlotNo
SlotNo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
n))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Word64 -> TxIx
TxIx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
10))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (HasCallStack => Integer -> CertIx
mkCertIxPartial forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
1, Integer
20))

genStakeRefWith ::
  forall era.
  Proof era ->
  Set Ptr ->
  Set (Credential 'Staking) ->
  Gen StakeReference
genStakeRefWith :: forall era.
Proof era
-> Set Ptr -> Set (Credential 'Staking) -> Gen StakeReference
genStakeRefWith Proof era
proof Set Ptr
ps Set (Credential 'Staking)
cs =
  forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
80, Credential 'Staking -> StakeReference
StakeRefBase forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. [String] -> Set t -> Gen t
pick1 [String
"from genStakeRefWith StakeRefBase"] Set (Credential 'Staking)
cs)
    ,
      ( if forall era. Proof era -> ProtVer
protocolVersion Proof era
proof forall a. Ord a => a -> a -> Bool
>= forall era. Proof era -> ProtVer
protocolVersion Proof ConwayEra
Conway then Int
0 else Int
5
      , Ptr -> StakeReference
StakeRefPtr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. [String] -> Set t -> Gen t
pick1 [String
"from genStakeRefWith StakeRefPtr"] Set Ptr
ps
      )
    , (Int
15, forall (f :: * -> *) a. Applicative f => a -> f a
pure StakeReference
StakeRefNull)
    ]

noScripts :: Proof era -> Addr -> Bool
noScripts :: forall era. Proof era -> Addr -> Bool
noScripts Proof era
_ (Addr Network
_ (ScriptHashObj ScriptHash
_) StakeReference
_) = Bool
False
noScripts Proof era
_ (Addr Network
_ PaymentCredential
_ (StakeRefBase (ScriptHashObj ScriptHash
_))) = Bool
False
noScripts Proof era
_ (AddrBootstrap BootstrapAddress
_) = Bool
False
noScripts Proof era
_ Addr
_ = Bool
True

-- | Make some candidate DReps. The 'Always...' and one from each Credential.
genDReps :: Set (Credential 'Staking) -> Gen [DRep]
genDReps :: Set (Credential 'Staking) -> Gen [DRep]
genDReps Set (Credential 'Staking)
creds =
  forall a. [a] -> Gen [a]
shuffle
    ( forall a b. (a -> b) -> [a] -> [b]
map (Credential 'DRepRole -> DRep
DRepCredential forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole) (forall a. Set a -> [a]
Set.toList Set (Credential 'Staking)
creds)
        forall a. [a] -> [a] -> [a]
++ [DRep
DRepAlwaysAbstain, DRep
DRepAlwaysNoConfidence]
    )

genDRepsT ::
  UnivSize ->
  Term era (Set (Credential 'Staking)) ->
  Target era (Gen (Set DRep))
genDRepsT :: forall era.
UnivSize
-> Term era (Set (Credential 'Staking))
-> Target era (Gen (Set DRep))
genDRepsT UnivSize
sizes Term era (Set (Credential 'Staking))
creds = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"listToSet" (\Set (Credential 'Staking)
cs -> (forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take (UnivSize -> Int
usNumDReps UnivSize
sizes)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Credential 'Staking) -> Gen [DRep]
genDReps Set (Credential 'Staking)
cs) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (Credential 'Staking))
creds

-- ======================================================================
-- Reusable Targets. First order representations of functions for use in
-- building 'Target's. We will apply these to Term variables,
-- (using  (:$) and (^$)) to indicate how to construct a random values assigned
-- to those variables. By convention we name these "functional" targets by
-- post-fixing their names with a captial "T". These may be a bit more
-- prescriptive rather than descriptive, but you do what you have to do.

txOutT :: Reflect era => Proof era -> Addr -> Coin -> TxOutF era
txOutT :: forall era. Reflect era => Proof era -> Addr -> Coin -> TxOutF era
txOutT Proof era
p Addr
x Coin
c = forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
p (forall era.
(EraTxOut era, HasCallStack) =>
Addr -> Value era -> TxOut era
mkBasicTxOut Addr
x (forall t s. Inject t s => t -> s
inject Coin
c))

-- | The collateral consists only of VKey addresses
--   and the collateral outputs in the UTxO do not contain any non-ADA part
colTxOutT :: EraTxOut era => Proof era -> Set Addr -> Gen (TxOutF era)
colTxOutT :: forall era.
EraTxOut era =>
Proof era -> Set Addr -> Gen (TxOutF era)
colTxOutT Proof era
p Set Addr
noScriptAddr =
  forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
p
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall era.
(EraTxOut era, HasCallStack) =>
Addr -> Value era -> TxOut era
mkBasicTxOut forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. [String] -> Set t -> Gen t
pick1 [String
"from colTxOutT noScriptAddr"] Set Addr
noScriptAddr forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall t s. Inject t s => t -> s
inject forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Coin
noZeroCoin))

-- | The collateral consists only of VKey addresses
--   and the collateral outputs in the UTxO do not contain any non-ADA part
colTxOutSetT :: EraTxOut era => Proof era -> Set Addr -> Gen (Set (TxOutF era))
colTxOutSetT :: forall era.
EraTxOut era =>
Proof era -> Set Addr -> Gen (Set (TxOutF era))
colTxOutSetT Proof era
p Set Addr
noScriptAddr = forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' Gen (Set (TxOutF era)) -> Addr -> Gen (Set (TxOutF era))
accum (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty) Set Addr
noScriptAddr
  where
    accum :: Gen (Set (TxOutF era)) -> Addr -> Gen (Set (TxOutF era))
accum Gen (Set (TxOutF era))
ansM Addr
addr = do
      Coin
c <- Gen Coin
noZeroCoin
      forall a. Ord a => a -> Set a -> Set a
Set.insert (forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
p (forall era.
(EraTxOut era, HasCallStack) =>
Addr -> Value era -> TxOut era
mkBasicTxOut Addr
addr (forall t s. Inject t s => t -> s
inject Coin
c))) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Set (TxOutF era))
ansM

scriptHashObjT :: Term era ScriptHash -> Target era (Credential k)
scriptHashObjT :: forall era (k :: KeyRole).
Term era ScriptHash -> Target era (Credential k)
scriptHashObjT Term era ScriptHash
x = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"ScriptHashObj" forall (kr :: KeyRole). ScriptHash -> Credential kr
ScriptHashObj forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era ScriptHash
x

keyHashObjT ::
  Term era (KeyHash 'Witness) -> Target era (Credential k)
keyHashObjT :: forall era (k :: KeyRole).
Term era (KeyHash 'Witness) -> Target era (Credential k)
keyHashObjT Term era (KeyHash 'Witness)
x = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"KeyHashObj" (forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (KeyHash 'Witness)
x

makeValidityT ::
  Term era SlotNo -> Term era SlotNo -> Term era SlotNo -> Target era ValidityInterval
makeValidityT :: forall era.
Term era SlotNo
-> Term era SlotNo
-> Term era SlotNo
-> Target era ValidityInterval
makeValidityT Term era SlotNo
begin Term era SlotNo
current Term era SlotNo
end =
  forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr
    String
"(-i)x(+j)"
    (\SlotNo
beginD SlotNo
x SlotNo
endD -> StrictMaybe SlotNo -> StrictMaybe SlotNo -> ValidityInterval
ValidityInterval (forall a. a -> StrictMaybe a
SJust (SlotNo
x forall a. Num a => a -> a -> a
- SlotNo
beginD)) (forall a. a -> StrictMaybe a
SJust (SlotNo
x forall a. Num a => a -> a -> a
+ SlotNo
endD)))
    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era SlotNo
begin
    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era SlotNo
current
    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era SlotNo
end

ptrUnivT :: Int -> Term era SlotNo -> Target era (Gen (Set Ptr))
ptrUnivT :: forall era. Int -> Term era SlotNo -> Target era (Gen (Set Ptr))
ptrUnivT Int
nptrs Term era SlotNo
x = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"" (forall a. Ord a => [String] -> Int -> Gen a -> Gen (Set a)
setSized [String
"From init ptruniv"] Int
nptrs) forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"" SlotNo -> Gen Ptr
genPtr forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era SlotNo
x)

addrUnivT ::
  Proof era ->
  Int ->
  Term era Network ->
  Term era (Set (Credential 'Payment)) ->
  Term era (Set Ptr) ->
  Term era (Set (Credential 'Staking)) ->
  Term era (Map (KeyHash 'Payment) (Addr, Byron.SigningKey)) ->
  Target era (Gen (Set Addr))
addrUnivT :: forall era.
Proof era
-> Int
-> Term era Network
-> Term era (Set PaymentCredential)
-> Term era (Set Ptr)
-> Term era (Set (Credential 'Staking))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Gen (Set Addr))
addrUnivT Proof era
p Int
naddr Term era Network
net Term era (Set PaymentCredential)
ps Term era (Set Ptr)
pts Term era (Set (Credential 'Staking))
cs Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUnivT =
  forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"" (forall a. Ord a => [String] -> Int -> Gen a -> Gen (Set a)
setSized [String
"From addrUnivT"] Int
naddr)
    forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"genAddrWith" (forall era.
Proof era
-> Network
-> Set PaymentCredential
-> Set Ptr
-> Set (Credential 'Staking)
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Gen Addr
genAddrWith Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Network
net forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set PaymentCredential)
ps forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set Ptr)
pts forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (Credential 'Staking))
cs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUnivT)

makeHashScriptMapT ::
  Proof era ->
  Int ->
  PlutusPurposeTag ->
  Term era (Map (KeyHash 'Witness) (KeyPair 'Witness)) ->
  Term era ValidityInterval ->
  Target era (Gen (Map ScriptHash (ScriptF era)))
makeHashScriptMapT :: forall era.
Proof era
-> Int
-> PlutusPurposeTag
-> Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
-> Term era ValidityInterval
-> Target era (Gen (Map ScriptHash (ScriptF era)))
makeHashScriptMapT Proof era
p Int
size PlutusPurposeTag
tag Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
m Term era ValidityInterval
vi =
  forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr
    String
"makeHashScriptMap"
    (forall era a. (Reflect era => Proof era -> a) -> Proof era -> a
unReflect forall era.
Reflect era =>
Proof era
-> Int
-> PlutusPurposeTag
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> ValidityInterval
-> Gen (Map ScriptHash (ScriptF era))
makeHashScriptMap Proof era
p Int
size PlutusPurposeTag
tag)
    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
m
    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era ValidityInterval
vi

cast :: forall k. Set (KeyHash 'Witness) -> Set (KeyHash k)
cast :: forall (k :: KeyRole). Set (KeyHash 'Witness) -> Set (KeyHash k)
cast Set (KeyHash 'Witness)
x = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\KeyHash 'Witness
kh -> forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole @KeyHash @'Witness KeyHash 'Witness
kh) Set (KeyHash 'Witness)
x

-- TODO make some Script Credentials in addition to Key credentials
castCredCold :: Set (KeyHash 'Witness) -> Set (Credential 'ColdCommitteeRole)
castCredCold :: Set (KeyHash 'Witness) -> Set (Credential 'ColdCommitteeRole)
castCredCold = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj)

castCredHot :: Set (KeyHash 'Witness) -> Set (Credential 'HotCommitteeRole)
castCredHot :: Set (KeyHash 'Witness) -> Set (Credential 'HotCommitteeRole)
castCredHot = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj)

txinToGovactionId :: TxIn -> GovActionId
txinToGovactionId :: TxIn -> GovActionId
txinToGovactionId (TxIn TxId
idx (TxIx Word64
n)) = TxId -> GovActionIx -> GovActionId
GovActionId TxId
idx (Word16 -> GovActionIx
GovActionIx (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n))

-- =================================================================
-- Using constraints to generate the Universes

universePreds :: Reflect era => UnivSize -> Proof era -> [Pred era]
universePreds :: forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
universePreds UnivSize
size Proof era
p =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
100 Int
500) forall era. Era era => Term era SlotNo
currentSlot
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
30) forall era. Era era => Term era SlotNo
beginSlotDelta -- Note that (currentSlot - beginSlotDelta) is aways positive
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
900 Int
1000) forall era. Era era => Term era SlotNo
endSlotDelta -- Note each block may have spacing of 2-4 blocks,
  -- So for a Trace of length at most 300, we need at least 900 slots on average
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumKeys UnivSize
size)) Term era [KeyPair 'Witness]
keypairs
  , forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"xx" (\[KeyPair 'Witness]
s -> forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. (a -> b) -> [a] -> [b]
map (\KeyPair 'Witness
x -> (forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey (forall (kd :: KeyRole). KeyPair kd -> VKey kd
vKey KeyPair 'Witness
x), KeyPair 'Witness
x)) [KeyPair 'Witness]
s)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [KeyPair 'Witness]
keypairs)
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumPools UnivSize
size)) Term era (Set (KeyHash 'Witness))
prePoolUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness))
prePoolUniv (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)
  , forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"WitnessToStakePool" forall (k :: KeyRole). Set (KeyHash 'Witness) -> Set (KeyHash k)
cast forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
prePoolUniv)
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumStakeKeys UnivSize
size)) Term era (Set (KeyHash 'Witness))
preStakeUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness))
preStakeUniv (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)
  , forall era. Era era => Term era (Set (KeyHash 'Staking))
stakeHashUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"WitnessToStaking" forall (k :: KeyRole). Set (KeyHash 'Witness) -> Set (KeyHash k)
cast forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
preStakeUniv)
  , forall era. Era era => Term era (Set (KeyHash 'DRepRole))
drepHashUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"WitnessToDRepRole" forall (k :: KeyRole). Set (KeyHash 'Witness) -> Set (KeyHash k)
cast forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
preStakeUniv)
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumGenesisKeys UnivSize
size)) Term era (Set (KeyHash 'Witness))
preGenesisUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness))
preGenesisUniv (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)
  , Term era (Set (KeyHash 'Genesis))
preGenesisDom forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"WitnessToGenesis" forall (k :: KeyRole). Set (KeyHash 'Witness) -> Set (KeyHash k)
cast forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
preGenesisUniv)
  , Term era (Set (KeyHash 'Genesis))
preGenesisDom forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv)
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumVoteKeys UnivSize
size)) Term era (Set (KeyHash 'Witness))
preVoteUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness))
preVoteUniv (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)
  , forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole))
voteCredUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"WitnessToStakePool" Set (KeyHash 'Witness) -> Set (Credential 'ColdCommitteeRole)
castCredCold forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
preVoteUniv)
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumTxIn UnivSize
size)) forall era. Era era => Term era (Set TxIn)
txinUniv
  , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. b -> Either a b
Right forall era. Era era => Term era TxIn
feeTxIn) forall era. Era era => Term era (Set TxIn)
txinUniv
  , forall era. Era era => Term era (Set GovActionId)
govActionIdUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"TxIn-to-GovActionId" (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map TxIn -> GovActionId
txinToGovactionId) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set TxIn)
txinUniv)
  , forall era. Era era => Term era ValidityInterval
validityInterval forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Term era SlotNo
-> Term era SlotNo
-> Term era SlotNo
-> Target era ValidityInterval
makeValidityT forall era. Era era => Term era SlotNo
beginSlotDelta forall era. Era era => Term era SlotNo
currentSlot forall era. Era era => Term era SlotNo
endSlotDelta
  , forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
      (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumCredentials UnivSize
size))
      Term era [Credential 'Staking]
credList
      [
        ( UnivSize -> Int
usCredScriptFreq UnivSize
size
        , forall era (k :: KeyRole).
Term era ScriptHash -> Target era (Credential k)
scriptHashObjT Term era ScriptHash
scripthash
        , [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era ScriptHash
scripthash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))]
        )
      , (Int
1, forall era (k :: KeyRole).
Term era (KeyHash 'Witness) -> Target era (Credential k)
keyHashObjT Term era (KeyHash 'Witness)
keyhash, [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'Witness)
keyhash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)])
      ]
  , forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall x era. Ord x => Term era [x] -> Target era (Set x)
listToSetTarget Term era [Credential 'Staking]
credList
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
spendscriptUniv Proof era
p) (forall era.
Proof era
-> Int
-> PlutusPurposeTag
-> Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
-> Term era ValidityInterval
-> Target era (Gen (Map ScriptHash (ScriptF era)))
makeHashScriptMapT Proof era
p Int
25 PlutusPurposeTag
Spending forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv forall era. Era era => Term era ValidityInterval
validityInterval)
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p) (forall era.
Proof era
-> Int
-> PlutusPurposeTag
-> Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
-> Term era ValidityInterval
-> Target era (Gen (Map ScriptHash (ScriptF era)))
makeHashScriptMapT Proof era
p Int
25 PlutusPurposeTag
Certifying forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv forall era. Era era => Term era ValidityInterval
validityInterval)
  , forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"union" forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
spendscriptUniv Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))
  , forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
      (forall era. Era era => Int -> Term era Size
ExactSize Int
70)
      Term era [PaymentCredential]
spendcredList
      [
        ( UnivSize -> Int
usSpendScriptFreq UnivSize
size
        , forall era (k :: KeyRole).
Term era ScriptHash -> Target era (Credential k)
scriptHashObjT Term era ScriptHash
scripthash
        , [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era ScriptHash
scripthash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
spendscriptUniv Proof era
p))]
        )
      , (Int
2, forall era (k :: KeyRole).
Term era (KeyHash 'Witness) -> Target era (Credential k)
keyHashObjT Term era (KeyHash 'Witness)
keyhash, [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'Witness)
keyhash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)])
      ]
  , forall era. Era era => Term era (Set PaymentCredential)
spendCredsUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall x era. Ord x => Term era [x] -> Target era (Set x)
listToSetTarget Term era [PaymentCredential]
spendcredList
  , forall era. Era era => Term era EpochNo
currentEpoch forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"epochFromSlotNo" SlotNo -> EpochNo
epochFromSlotNo forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era SlotNo
currentSlot)
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Era era => Term era (Map DataHash (Data era))
dataUniv (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"dataWits" (forall era.
Era era =>
Proof era -> Int -> Gen (Map DataHash (Data era))
genDataWits Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Int
IntR Int
30))
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Era era => Term era [Datum era]
datumsUniv (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"genDatums" (forall era.
Era era =>
UnivSize -> Int -> Map DataHash (Data era) -> Gen [Datum era]
genDatums UnivSize
size (UnivSize -> Int
usNumDatums UnivSize
size)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Map DataHash (Data era))
dataUniv)
  , -- 'network' is set by testGlobals which contains 'Testnet'
    forall era. Era era => Term era Network
network forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall t era. t -> Target era t
constTarget (Globals -> Network
Utils.networkId Globals
Utils.testGlobals)
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Era era => Term era (Set Ptr)
ptrUniv (forall era. Int -> Term era SlotNo -> Target era (Gen (Set Ptr))
ptrUnivT (UnivSize -> Int
usNumPtr UnivSize
size) forall era. Era era => Term era SlotNo
currentSlot)
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"byronUniv" Network -> Gen (Map (KeyHash 'Payment) (Addr, SigningKey))
genByronUniv forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Network
network)
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom
      forall era. Era era => Term era (Set Addr)
addrUniv
      (forall era.
Proof era
-> Int
-> Term era Network
-> Term era (Set PaymentCredential)
-> Term era (Set Ptr)
-> Term era (Set (Credential 'Staking))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Gen (Set Addr))
addrUnivT Proof era
p (UnivSize -> Int
usNumAddr UnivSize
size) forall era. Era era => Term era Network
network forall era. Era era => Term era (Set PaymentCredential)
spendCredsUniv forall era. Era era => Term era (Set Ptr)
ptrUniv forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv)
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom
      forall era. Era era => Term era [MultiAsset]
multiAssetUniv
      (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"multiAsset" (forall a. Int -> Gen a -> Gen [a]
vectorOf (UnivSize -> Int
usNumMultiAsset UnivSize
size) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom
      Term era [TxOutF era]
preTxoutUniv
      ( forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"genTxOuts" (forall era.
Reflect era =>
UnivSize
-> (Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era))
-> Proof era
-> Int
-> Set Addr
-> Map ScriptHash (ScriptF era)
-> Map ScriptHash (ScriptF era)
-> Map DataHash (Data era)
-> Gen [TxOutF era]
genTxOuts UnivSize
size (forall era.
UnivSize
-> Proof era
-> Coin
-> Map ScriptHash (ScriptF era)
-> Gen (Value era)
genValueF UnivSize
size Proof era
p) Proof era
p (UnivSize -> Int
usNumTxOuts UnivSize
size))
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set Addr)
addrUniv
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p)
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
spendscriptUniv Proof era
p)
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Map DataHash (Data era))
dataUniv
      )
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom
      (forall era. Era era => Proof era -> Term era (Set (TxOutF era))
colTxoutUniv Proof era
p)
      ( forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr
          String
"colTxOutUniv"
          (\Set Addr
x -> forall era.
EraTxOut era =>
Proof era -> Set Addr -> Gen (Set (TxOutF era))
colTxOutSetT Proof era
p (forall a. (a -> Bool) -> Set a -> Set a
Set.filter (forall era. Proof era -> Addr -> Bool
noScripts Proof era
p) Set Addr
x))
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set Addr)
addrUniv
      )
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Era era => Term era (Set DRep)
drepUniv (forall era.
UnivSize
-> Term era (Set (Credential 'Staking))
-> Target era (Gen (Set DRep))
genDRepsT UnivSize
size forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv)
  , forall era. Era era => Term era (Set PaymentCredential)
payUniv forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era (Set PaymentCredential)
spendCredsUniv
  , forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"coerce" (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'Staking -> Credential 'DRepRole
stakeToDRepRole) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv)
  , forall era.
Era era =>
Term era (Set (Credential 'HotCommitteeRole))
hotCommitteeCredsUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"coerce" (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'Staking -> Credential 'HotCommitteeRole
stakeToHotCommittee) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv)
  , forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole))
coldCommitteeCredsUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"coerce" (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'Staking -> Credential 'ColdCommitteeRole
stakeToColdCommittee) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv)
  , forall era. Era era => Term era Coin
bigCoin forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall t era. t -> Target era t
constTarget (Integer -> Coin
Coin Integer
2000000)
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom
      forall era. Reflect era => Term era (TxOutF era)
feeTxOut
      ( forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr
          String
"txout"
          ( \Set Addr
a Coin
c ->
              forall era. Reflect era => Proof era -> Addr -> Coin -> TxOutF era
txOutT Proof era
p
                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. [String] -> Set t -> Gen t
pick1 [String
"from feeTxOut on (filter nocripts addrUniv)"] (forall a. (a -> Bool) -> Set a -> Set a
Set.filter (forall era. Proof era -> Addr -> Bool
noScripts Proof era
p) Set Addr
a)
                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Coin
c
          )
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set Addr)
addrUniv
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Coin
bigCoin
      )
  , forall era. Era era => Proof era -> Term era (Set (TxOutF era))
txoutUniv Proof era
p
      forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr
              String
"insert"
              (\TxOutF era
x [TxOutF era]
y Set (TxOutF era)
_z -> forall a. Ord a => a -> Set a -> Set a
Set.insert TxOutF era
x {- (Set.union z -} (forall a. Ord a => [a] -> Set a
Set.fromList [TxOutF era]
y)) -- )
              forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Reflect era => Term era (TxOutF era)
feeTxOut
              forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [TxOutF era]
preTxoutUniv
              forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. Era era => Proof era -> Term era (Set (TxOutF era))
colTxoutUniv Proof era
p)
           )
  , forall era.
Reflect era =>
Term era (Map ScriptHash (IsValid, ScriptF era))
plutusUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall t era. t -> Target era t
constTarget (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\(IsValid
x, Script era
y) -> (IsValid
x, forall era. Proof era -> Script era -> ScriptF era
ScriptF Proof era
p Script era
y)) (forall era.
Reflect era =>
Proof era -> Map ScriptHash (IsValid, Script era)
allPlutusScripts Proof era
p))
  , forall era.
Reflect era =>
Term era (Map ScriptHash (IsValid, ScriptF era))
spendPlutusUniv forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall t era. t -> Target era t
constTarget (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\(IsValid
x, Script era
y) -> (IsValid
x, forall era. Proof era -> Script era -> ScriptF era
ScriptF Proof era
p Script era
y)) (forall era.
Reflect era =>
Proof era -> Map ScriptHash (IsValid, Script era)
spendPlutusScripts Proof era
p))
  ]
  where
    credList :: Term era [Credential 'Staking]
credList = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"credList" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era (Credential 'Staking)
CredR) forall era s t. Access era s t
No)
    spendcredList :: Term era [PaymentCredential]
spendcredList = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"spendcred.list" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era PaymentCredential
PCredR) forall era s t. Access era s t
No)
    keyhash :: Term era (KeyHash 'Witness)
keyhash = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"keyhash" forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR forall era s t. Access era s t
No)
    scripthash :: Term era ScriptHash
scripthash = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"scripthash" forall era. Era era => Rep era ScriptHash
ScriptHashR forall era s t. Access era s t
No)
    preTxoutUniv :: Term era [TxOutF era]
preTxoutUniv = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"preTxoutUniv" (forall era a. Rep era a -> Rep era [a]
ListR (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) forall era s t. Access era s t
No)
    keypairs :: Term era [KeyPair 'Witness]
keypairs = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"keypairs" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era (KeyPair 'Witness)
KeyPairR) forall era s t. Access era s t
No)
    prePoolUniv :: Term era (Set (KeyHash 'Witness))
prePoolUniv = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"prePoolUniv" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) forall era s t. Access era s t
No)
    preStakeUniv :: Term era (Set (KeyHash 'Witness))
preStakeUniv = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"preStakeUniv" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) forall era s t. Access era s t
No)
    preGenesisUniv :: Term era (Set (KeyHash 'Witness))
preGenesisUniv = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"preGenesisUniv" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) forall era s t. Access era s t
No)
    preGenesisDom :: Term era (Set (KeyHash 'Genesis))
preGenesisDom = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"preGenesisDom" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR) forall era s t. Access era s t
No)
    preVoteUniv :: Term era (Set (KeyHash 'Witness))
preVoteUniv = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"preVoteUniv" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) forall era s t. Access era s t
No)

multiAsset :: UnivSize -> Map.Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset :: forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size Map ScriptHash (ScriptF era)
scripts = do
  let assets :: Set AssetName
assets =
        forall a. Ord a => [a] -> Set a
Set.fromList [ShortByteString -> AssetName
AssetName (forall a. IsString a => String -> a
fromString (forall a. Show a => a -> String
show (Int
n :: Int) forall a. [a] -> [a] -> [a]
++ String
"Asset")) | Int
n <- [Int
0 .. (UnivSize -> Int
usMaxAssets UnivSize
size)]]
  Int
n <- forall a. HasCallStack => [a] -> Gen a
elements [Int
0 .. (UnivSize -> Int
usMaxPolicyID UnivSize
size)]
  if Int
n forall a. Eq a => a -> a -> Bool
== Int
0
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty -- About 1/3 of the list will be the empty MA
    else do
      -- So lots of duplicates, but we want to choose the empty MA, 1/3 of the time.
      [(PolicyID, AssetName, Integer)]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era.
Map ScriptHash (ScriptF era)
-> Set AssetName
-> Gen Integer
-> Gen (PolicyID, AssetName, Integer)
genMultiAssetTriple Map ScriptHash (ScriptF era)
scripts Set AssetName
assets (forall a. Random a => (a, a) -> Gen a
choose (Integer
1, Integer
100)))
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [(PolicyID, AssetName, Integer)] -> MultiAsset
multiAssetFromList [(PolicyID, AssetName, Integer)]
xs

genValueF :: UnivSize -> Proof era -> Coin -> Map ScriptHash (ScriptF era) -> Gen (Value era)
genValueF :: forall era.
UnivSize
-> Proof era
-> Coin
-> Map ScriptHash (ScriptF era)
-> Gen (Value era)
genValueF UnivSize
size Proof era
proof Coin
c Map ScriptHash (ScriptF era)
scripts = case forall era. Proof era -> ValueWit era
whichValue Proof era
proof of
  ValueWit era
ValueShelleyToAllegra -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Coin
c
  ValueWit era
ValueMaryToConway -> Coin -> MultiAsset -> MaryValue
MaryValue Coin
c forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size Map ScriptHash (ScriptF era)
scripts

stakeToDRepRole :: Credential 'Staking -> Credential 'DRepRole
stakeToDRepRole :: Credential 'Staking -> Credential 'DRepRole
stakeToDRepRole = forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole

stakeToHotCommittee :: Credential 'Staking -> Credential 'HotCommitteeRole
stakeToHotCommittee :: Credential 'Staking -> Credential 'HotCommitteeRole
stakeToHotCommittee = forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole

stakeToColdCommittee :: Credential 'Staking -> Credential 'ColdCommitteeRole
stakeToColdCommittee :: Credential 'Staking -> Credential 'ColdCommitteeRole
stakeToColdCommittee = forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole

solveUniv :: Reflect era => UnivSize -> Proof era -> Gen (Subst era)
solveUniv :: forall era. Reflect era => UnivSize -> Proof era -> Gen (Subst era)
solveUniv UnivSize
size Proof era
proof = do
  forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
universePreds UnivSize
size Proof era
proof) forall era. Subst era
emptySubst

universeStage ::
  Reflect era =>
  UnivSize ->
  Proof era ->
  Subst era ->
  Gen (Subst era)
universeStage :: forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
size Proof era
proof = forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
universePreds UnivSize
size Proof era
proof)

demo :: ReplMode -> IO ()
demo :: ReplMode -> IO ()
demo ReplMode
mode = do
  let proof :: Proof ShelleyEra
proof = Proof ShelleyEra
Shelley
  Subst ShelleyEra
subst <- forall a. Gen a -> IO a
generate (forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof ShelleyEra
proof forall era. Subst era
emptySubst)
  if ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive
    then String -> IO ()
putStrLn String
"\n" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStrLn (forall a. Show a => a -> String
show Subst ShelleyEra
subst)
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Env ShelleyEra
env <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ShelleyEra
subst forall era. Env era
emptyEnv)
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ShelleyEra
proof Env ShelleyEra
env String
""

demoTest :: TestTree
demoTest :: TestTree
demoTest = forall a. String -> IO a -> TestTree
testIO String
"Testing Universe Stage" (ReplMode -> IO ()
demo ReplMode
CI)

main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall a. String -> IO a -> TestTree
testIO String
"Testing Universe Stage" (ReplMode -> IO ()
demo ReplMode
Interactive)