{-# 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.DSIGN as DSIGN
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 (
  Era (EraCrypto),
  EraScript,
  EraTxOut (..),
  TxOut,
  Value,
  hashScript,
  isNativeScript,
 )
import Cardano.Ledger.Credential (Credential (..), Ptr (..), StakeReference (..))
import Cardano.Ledger.Crypto (Crypto, DSIGN)
import Cardano.Ledger.DRep (DRep (..))
import Cardano.Ledger.Hashes (DataHash, EraIndependentTxBody, ScriptHash)
import Cardano.Ledger.Keys (Hash, KeyHash, KeyRole (..), coerceKeyRole, hashKey)
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 c, Byron.SigningKey)
genAddrPair :: forall c. Network -> Gen (BootstrapAddress c, 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 (forall c. Address -> BootstrapAddress c
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 :: Crypto c => Network -> Gen (Map (KeyHash 'Payment c) (Addr c, Byron.SigningKey))
genByronUniv :: forall c.
Crypto c =>
Network -> Gen (Map (KeyHash 'Payment c) (Addr c, SigningKey))
genByronUniv Network
netwrk = do
  [(BootstrapAddress c, SigningKey)]
list <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall c. Network -> Gen (BootstrapAddress c, 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 c
addr, SigningKey
signkey) -> (forall c. Crypto c => BootstrapAddress c -> KeyHash 'Payment c
bootstrapKeyHash BootstrapAddress c
addr, (forall c. BootstrapAddress c -> Addr c
AddrBootstrap BootstrapAddress c
addr, SigningKey
signkey))) [(BootstrapAddress c, SigningKey)]
list)

-- | Given a list of Byron addresses, compute BootStrap witnesses of all of those addresses
--   Can only be used with StandardCrypto
bootWitness ::
  (Crypto c, DSIGN c ~ DSIGN.Ed25519DSIGN) =>
  Hash c EraIndependentTxBody ->
  [BootstrapAddress c] ->
  Map (KeyHash 'Payment c) (Addr c, Byron.SigningKey) ->
  Set (BootstrapWitness c)
bootWitness :: forall c.
(Crypto c, DSIGN c ~ Ed25519DSIGN) =>
Hash c EraIndependentTxBody
-> [BootstrapAddress c]
-> Map (KeyHash 'Payment c) (Addr c, SigningKey)
-> Set (BootstrapWitness c)
bootWitness Hash c EraIndependentTxBody
hash [BootstrapAddress c]
bootaddrs Map (KeyHash 'Payment c) (Addr c, SigningKey)
byronuniv = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (BootstrapWitness c)
-> BootstrapAddress c -> Set (BootstrapWitness c)
accum forall a. Set a
Set.empty [BootstrapAddress c]
bootaddrs
  where
    accum :: Set (BootstrapWitness c)
-> BootstrapAddress c -> Set (BootstrapWitness c)
accum Set (BootstrapWitness c)
ans bootaddr :: BootstrapAddress c
bootaddr@(BootstrapAddress Address
a) = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall c. Crypto c => BootstrapAddress c -> KeyHash 'Payment c
bootstrapKeyHash BootstrapAddress c
bootaddr) Map (KeyHash 'Payment c) (Addr c, SigningKey)
byronuniv of
      Just (AddrBootstrap BootstrapAddress c
_, SigningKey
signkey) ->
        forall a. Ord a => a -> Set a -> Set a
Set.insert (forall c.
(DSIGN c ~ Ed25519DSIGN, Crypto c) =>
Hash c EraIndependentTxBody
-> SigningKey -> Attributes AddrAttributes -> BootstrapWitness c
makeBootstrapWitness Hash c EraIndependentTxBody
hash SigningKey
signkey (Address -> Attributes AddrAttributes
Byron.addrAttributes Address
a)) Set (BootstrapWitness c)
ans
      Maybe (Addr c, SigningKey)
_ -> Set (BootstrapWitness c)
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 (EraCrypto era)) (Data era) -> Gen [Datum era]
genDatums :: forall era.
Era era =>
UnivSize
-> Int
-> Map (DataHash (EraCrypto era)) (Data era)
-> Gen [Datum era]
genDatums UnivSize
sizes Int
n Map (DataHash (EraCrypto era)) (Data era)
datauniv = forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era.
Era era =>
UnivSize
-> Map (DataHash (EraCrypto era)) (Data era) -> Gen (Datum era)
genDatum UnivSize
sizes Map (DataHash (EraCrypto era)) (Data era)
datauniv)

-- | Only generate non-empty Datums. I.e. There are no NoDatum Datums generated.
genDatum :: Era era => UnivSize -> Map (DataHash (EraCrypto era)) (Data era) -> Gen (Datum era)
genDatum :: forall era.
Era era =>
UnivSize
-> Map (DataHash (EraCrypto era)) (Data era) -> Gen (Datum era)
genDatum UnivSize {Int
usDatumFreq :: Int
usDatumFreq :: UnivSize -> Int
usDatumFreq} Map (DataHash (EraCrypto era)) (Data era)
datauniv =
  forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
1, forall era. DataHash (EraCrypto era) -> 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 (EraCrypto era)) (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 (EraCrypto era)) (Data era)
datauniv
      )
    ]

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

genTxOut ::
  Reflect era =>
  UnivSize ->
  (Coin -> Map (ScriptHash (EraCrypto era)) (ScriptF era) -> Gen (Value era)) ->
  Proof era ->
  Coin ->
  Set (Addr (EraCrypto era)) ->
  Map (ScriptHash (EraCrypto era)) (ScriptF era) ->
  Map (ScriptHash (EraCrypto era)) (ScriptF era) ->
  Map (DataHash (EraCrypto era)) (Data era) ->
  Gen (TxOut era)
genTxOut :: forall era.
Reflect era =>
UnivSize
-> (Coin
    -> Map (ScriptHash (EraCrypto era)) (ScriptF era)
    -> Gen (Value era))
-> Proof era
-> Coin
-> Set (Addr (EraCrypto era))
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map (DataHash (EraCrypto era)) (Data era)
-> Gen (TxOut era)
genTxOut UnivSize
sizes Coin
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (Value era)
genvalue Proof era
p Coin
c Set (Addr (EraCrypto era))
addruniv Map (ScriptHash (EraCrypto era)) (ScriptF era)
scriptuniv Map (ScriptHash (EraCrypto era)) (ScriptF era)
spendscriptuniv Map (DataHash (EraCrypto era)) (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 (EraCrypto era) -> 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 (EraCrypto era))
addruniv forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (Value era)
genvalue Coin
c Map (ScriptHash (EraCrypto era)) (ScriptF era)
scriptuniv
    TxOutWit era
TxOutAlonzoToAlonzo -> do
      Addr StandardCrypto
addr <- forall t. [String] -> Set t -> Gen t
pick1 [String
"genTxOut AlonzoToAlonzo Addr"] Set (Addr (EraCrypto era))
addruniv
      Value era
v <- Coin
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (Value era)
genvalue Coin
c Map (ScriptHash (EraCrypto era)) (ScriptF era)
scriptuniv
      case Addr StandardCrypto
addr of
        AddrBootstrap BootstrapAddress StandardCrypto
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr (EraCrypto era)
-> Value era
-> StrictMaybe (DataHash (EraCrypto era))
-> AlonzoTxOut era
AlonzoTxOut Addr StandardCrypto
addr Value era
v forall a. StrictMaybe a
SNothing)
        Addr Network
_ PaymentCredential StandardCrypto
paycred StakeReference StandardCrypto
_ ->
          if forall era.
EraScript era =>
Credential 'Payment (EraCrypto era)
-> Map (ScriptHash (EraCrypto era)) (ScriptF era) -> Bool
needsDatum PaymentCredential StandardCrypto
paycred Map (ScriptHash (EraCrypto era)) (ScriptF era)
spendscriptuniv
            then
              forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr (EraCrypto era)
-> Value era
-> StrictMaybe (DataHash (EraCrypto era))
-> AlonzoTxOut era
AlonzoTxOut Addr StandardCrypto
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 (EraCrypto era)) (Data era)
datauniv
            else forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr (EraCrypto era)
-> Value era
-> StrictMaybe (DataHash (EraCrypto era))
-> AlonzoTxOut era
AlonzoTxOut Addr StandardCrypto
addr Value era
v forall a. StrictMaybe a
SNothing)
    TxOutWit era
TxOutBabbageToConway -> do
      Addr StandardCrypto
addr <- forall t. [String] -> Set t -> Gen t
pick1 [String
"genTxOut BabbageToConway Addr"] Set (Addr (EraCrypto era))
addruniv
      Value era
v <- Coin
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (Value era)
genvalue Coin
c Map (ScriptHash (EraCrypto era)) (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 (EraCrypto era)) (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 StandardCrypto
addr of
        AddrBootstrap BootstrapAddress StandardCrypto
_ -> 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 (EraCrypto era)
-> Value era
-> Datum era
-> StrictMaybe (Script era)
-> BabbageTxOut era
BabbageTxOut Addr StandardCrypto
addr Value era
v forall era. Datum era
NoDatum StrictMaybe (Script era)
maybescript
        Addr Network
_ PaymentCredential StandardCrypto
paycred StakeReference StandardCrypto
_ ->
          if forall era.
EraScript era =>
Credential 'Payment (EraCrypto era)
-> Map (ScriptHash (EraCrypto era)) (ScriptF era) -> Bool
needsDatum PaymentCredential StandardCrypto
paycred Map (ScriptHash (EraCrypto era)) (ScriptF era)
spendscriptuniv
            then forall era.
(Era era, Val (Value era), HasCallStack) =>
Addr (EraCrypto era)
-> Value era
-> Datum era
-> StrictMaybe (Script era)
-> BabbageTxOut era
BabbageTxOut Addr StandardCrypto
addr Value era
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era.
Era era =>
UnivSize
-> Map (DataHash (EraCrypto era)) (Data era) -> Gen (Datum era)
genDatum UnivSize
sizes Map (DataHash (EraCrypto era)) (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 (EraCrypto era)
-> Value era
-> Datum era
-> StrictMaybe (Script era)
-> BabbageTxOut era
BabbageTxOut Addr StandardCrypto
addr Value era
v forall era. Datum era
NoDatum StrictMaybe (Script era)
maybescript

needsDatum ::
  EraScript era =>
  Credential 'Payment (EraCrypto era) ->
  Map (ScriptHash (EraCrypto era)) (ScriptF era) ->
  Bool
needsDatum :: forall era.
EraScript era =>
Credential 'Payment (EraCrypto era)
-> Map (ScriptHash (EraCrypto era)) (ScriptF era) -> Bool
needsDatum (ScriptHashObj ScriptHash (EraCrypto era)
hash) Map (ScriptHash (EraCrypto era)) (ScriptF era)
spendScriptUniv = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScriptHash (EraCrypto era)
hash Map (ScriptHash (EraCrypto era)) (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 Credential 'Payment (EraCrypto era)
_ Map (ScriptHash (EraCrypto era)) (ScriptF era)
_ = Bool
False

genTxOuts ::
  Reflect era =>
  UnivSize ->
  (Coin -> Map (ScriptHash (EraCrypto era)) (ScriptF era) -> Gen (Value era)) ->
  Proof era ->
  Int ->
  Set (Addr (EraCrypto era)) ->
  Map (ScriptHash (EraCrypto era)) (ScriptF era) ->
  Map (ScriptHash (EraCrypto era)) (ScriptF era) ->
  Map (DataHash (EraCrypto era)) (Data era) ->
  Gen [TxOutF era]
genTxOuts :: forall era.
Reflect era =>
UnivSize
-> (Coin
    -> Map (ScriptHash (EraCrypto era)) (ScriptF era)
    -> Gen (Value era))
-> Proof era
-> Int
-> Set (Addr (EraCrypto era))
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map (DataHash (EraCrypto era)) (Data era)
-> Gen [TxOutF era]
genTxOuts UnivSize
sizes Coin
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (Value era)
genvalue Proof era
p Int
ntxouts Set (Addr (EraCrypto era))
addruniv Map (ScriptHash (EraCrypto era)) (ScriptF era)
scriptuniv Map (ScriptHash (EraCrypto era)) (ScriptF era)
spendscriptuniv Map (DataHash (EraCrypto era)) (Data era)
datauniv = do
  let genOne :: Gen (TxOut era)
genOne = do
        Coin
c <- Gen Coin
noZeroCoin
        forall era.
Reflect era =>
UnivSize
-> (Coin
    -> Map (ScriptHash (EraCrypto era)) (ScriptF era)
    -> Gen (Value era))
-> Proof era
-> Coin
-> Set (Addr (EraCrypto era))
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map (DataHash (EraCrypto era)) (Data era)
-> Gen (TxOut era)
genTxOut UnivSize
sizes Coin
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (Value era)
genvalue Proof era
p Coin
c Set (Addr (EraCrypto era))
addruniv Map (ScriptHash (EraCrypto era)) (ScriptF era)
scriptuniv Map (ScriptHash (EraCrypto era)) (ScriptF era)
spendscriptuniv Map (DataHash (EraCrypto era)) (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 (EraCrypto era)) (ScriptF era) ->
  Set AssetName ->
  Gen Integer ->
  Gen (PolicyID (EraCrypto era), AssetName, Integer)
genMultiAssetTriple :: forall era.
Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Set AssetName
-> Gen Integer
-> Gen (PolicyID (EraCrypto era), AssetName, Integer)
genMultiAssetTriple Map (ScriptHash (EraCrypto era)) (ScriptF era)
scriptMap Set AssetName
assetSet Gen Integer
genAmount =
  (,,)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall c. ScriptHash c -> PolicyID c
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 (EraCrypto era)) (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 (EraCrypto era)) (KeyPair 'Witness (EraCrypto era)) ->
  ValidityInterval ->
  Gen (Map (ScriptHash (EraCrypto era)) (ScriptF era))
makeHashScriptMap :: forall era.
Reflect era =>
Proof era
-> Int
-> PlutusPurposeTag
-> Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era))
-> ValidityInterval
-> Gen (Map (ScriptHash (EraCrypto era)) (ScriptF era))
makeHashScriptMap Proof era
p Int
size PlutusPurposeTag
tag Map
  (KeyHash 'Witness (EraCrypto era))
  (KeyPair 'Witness (EraCrypto era))
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
-> KeyMap era
-> ValidityInterval
-> Gen (Script era)
genCoreScript Proof era
p PlutusPurposeTag
Spending Map
  (KeyHash 'Witness (EraCrypto era))
  (KeyPair 'Witness (EraCrypto era))
m ValidityInterval
vi
          ScriptWit era
ScriptAllegraToMary -> forall era.
Proof era
-> PlutusPurposeTag
-> KeyMap era
-> ValidityInterval
-> Gen (Script era)
genCoreScript Proof era
p PlutusPurposeTag
Spending Map
  (KeyHash 'Witness (EraCrypto era))
  (KeyPair 'Witness (EraCrypto era))
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 (EraCrypto era)) (IsValid, Script era)
spendPlutusScripts Proof era
p)
              , forall era.
Proof era
-> PlutusPurposeTag
-> KeyMap era
-> ValidityInterval
-> Gen (Script era)
genCoreScript Proof era
p PlutusPurposeTag
Spending Map
  (KeyHash 'Witness (EraCrypto era))
  (KeyPair 'Witness (EraCrypto era))
m ValidityInterval
vi
              ]
      genOne PlutusPurposeTag
t = forall era.
Proof era
-> PlutusPurposeTag
-> KeyMap era
-> ValidityInterval
-> Gen (Script era)
genCoreScript Proof era
p PlutusPurposeTag
t Map
  (KeyHash 'Witness (EraCrypto era))
  (KeyPair 'Witness (EraCrypto era))
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 (EraCrypto era)
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 (EraCrypto era)) (Data era))
genDataWits :: forall era.
Era era =>
Proof era -> Int -> Gen (Map (DataHash (EraCrypto era)) (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. Era era => Data era -> DataHash (EraCrypto era)
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 (EraCrypto era)) ->
  Set Ptr ->
  Set (Credential 'Staking (EraCrypto era)) ->
  Map (KeyHash 'Payment (EraCrypto era)) (Addr (EraCrypto era), Byron.SigningKey) -> -- The Byron Addresss Universe
  Gen (Addr (EraCrypto era))
genAddrWith :: forall era.
Proof era
-> Network
-> Set (Credential 'Payment (EraCrypto era))
-> Set Ptr
-> Set (Credential 'Staking (EraCrypto era))
-> Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey)
-> Gen (Addr (EraCrypto era))
genAddrWith Proof era
proof Network
net Set (Credential 'Payment (EraCrypto era))
ps Set Ptr
ptrss Set (Credential 'Staking (EraCrypto era))
cs Map
  (KeyHash 'Payment (EraCrypto era))
  (Addr (EraCrypto era), SigningKey)
byronMap =
  case forall era. Proof era -> TxOutWit era
whichTxOut Proof era
proof of
    TxOutWit era
TxOutBabbageToConway -> forall c.
Network -> PaymentCredential c -> StakeReference c -> Addr c
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 (Credential 'Payment (EraCrypto era))
ps forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
Proof era
-> Set Ptr
-> Set (Credential 'Staking (EraCrypto era))
-> Gen (StakeReference (EraCrypto era))
genStakeRefWith Proof era
proof Set Ptr
ptrss Set (Credential 'Staking (EraCrypto era))
cs
    TxOutWit era
_ ->
      forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ (Int
8, forall c.
Network -> PaymentCredential c -> StakeReference c -> Addr c
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 (Credential 'Payment (EraCrypto era))
ps forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
Proof era
-> Set Ptr
-> Set (Credential 'Staking (EraCrypto era))
-> Gen (StakeReference (EraCrypto era))
genStakeRefWith Proof era
proof Set Ptr
ptrss Set (Credential 'Staking (EraCrypto era))
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 (EraCrypto era))
  (Addr (EraCrypto era), 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 (EraCrypto era)) ->
  Gen (StakeReference (EraCrypto era))
genStakeRefWith :: forall era.
Proof era
-> Set Ptr
-> Set (Credential 'Staking (EraCrypto era))
-> Gen (StakeReference (EraCrypto era))
genStakeRefWith Proof era
proof Set Ptr
ps Set (Credential 'Staking (EraCrypto era))
cs =
  forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
80, forall c. StakeCredential c -> StakeReference c
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 (EraCrypto era))
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 StandardCrypto)
Conway then Int
0 else Int
5
      , forall c. Ptr -> StakeReference c
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 forall c. StakeReference c
StakeRefNull)
    ]

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

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

genDRepsT ::
  UnivSize ->
  Term era (Set (Credential 'Staking (EraCrypto era))) ->
  Target era (Gen (Set (DRep (EraCrypto era))))
genDRepsT :: forall era.
UnivSize
-> Term era (Set (Credential 'Staking (EraCrypto era)))
-> Target era (Gen (Set (DRep (EraCrypto era))))
genDRepsT UnivSize
sizes Term era (Set (Credential 'Staking (EraCrypto era)))
creds = forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"listToSet" (\Set (Credential 'Staking (EraCrypto era))
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
<$> forall c. Set (Credential 'Staking c) -> Gen [DRep c]
genDReps Set (Credential 'Staking (EraCrypto era))
cs) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (Credential 'Staking (EraCrypto era)))
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 (EraCrypto era) -> Coin -> TxOutF era
txOutT :: forall era.
Reflect era =>
Proof era -> Addr (EraCrypto era) -> Coin -> TxOutF era
txOutT Proof era
p Addr (EraCrypto era)
x Coin
c = forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
p (forall era.
(EraTxOut era, HasCallStack) =>
Addr (EraCrypto era) -> Value era -> TxOut era
mkBasicTxOut Addr (EraCrypto era)
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 (EraCrypto era)) -> Gen (TxOutF era)
colTxOutT :: forall era.
EraTxOut era =>
Proof era -> Set (Addr (EraCrypto era)) -> Gen (TxOutF era)
colTxOutT Proof era
p Set (Addr (EraCrypto era))
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 (EraCrypto era) -> 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 (EraCrypto era))
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 (EraCrypto era)) -> Gen (Set (TxOutF era))
colTxOutSetT :: forall era.
EraTxOut era =>
Proof era -> Set (Addr (EraCrypto era)) -> Gen (Set (TxOutF era))
colTxOutSetT Proof era
p Set (Addr (EraCrypto era))
noScriptAddr = forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' Gen (Set (TxOutF era))
-> Addr (EraCrypto era) -> Gen (Set (TxOutF era))
accum (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty) Set (Addr (EraCrypto era))
noScriptAddr
  where
    accum :: Gen (Set (TxOutF era))
-> Addr (EraCrypto era) -> Gen (Set (TxOutF era))
accum Gen (Set (TxOutF era))
ansM Addr (EraCrypto era)
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 (EraCrypto era) -> Value era -> TxOut era
mkBasicTxOut Addr (EraCrypto era)
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 (EraCrypto era)) -> Target era (Credential k (EraCrypto era))
scriptHashObjT :: forall era (k :: KeyRole).
Term era (ScriptHash (EraCrypto era))
-> Target era (Credential k (EraCrypto era))
scriptHashObjT Term era (ScriptHash (EraCrypto era))
x = forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"ScriptHashObj" forall (kr :: KeyRole) c. ScriptHash c -> Credential kr c
ScriptHashObj forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (ScriptHash (EraCrypto era))
x

keyHashObjT ::
  Term era (KeyHash 'Witness (EraCrypto era)) -> Target era (Credential k (EraCrypto era))
keyHashObjT :: forall era (k :: KeyRole).
Term era (KeyHash 'Witness (EraCrypto era))
-> Target era (Credential k (EraCrypto era))
keyHashObjT Term era (KeyHash 'Witness (EraCrypto era))
x = forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"KeyHashObj" (forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (KeyHash 'Witness (EraCrypto era))
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 r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"" (forall a. Ord a => [String] -> Int -> Gen a -> Gen (Set a)
setSized [String
"From init ptruniv"] Int
nptrs) forall era r a b.
RootTarget era r (a -> b)
-> RootTarget era r a -> RootTarget era r b
:$ (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 (EraCrypto era))) ->
  Term era (Set Ptr) ->
  Term era (Set (Credential 'Staking (EraCrypto era))) ->
  Term era (Map (KeyHash 'Payment (EraCrypto era)) (Addr (EraCrypto era), Byron.SigningKey)) ->
  Target era (Gen (Set (Addr (EraCrypto era))))
addrUnivT :: forall era.
Proof era
-> Int
-> Term era Network
-> Term era (Set (Credential 'Payment (EraCrypto era)))
-> Term era (Set Ptr)
-> Term era (Set (Credential 'Staking (EraCrypto era)))
-> Term
     era
     (Map
        (KeyHash 'Payment (EraCrypto era))
        (Addr (EraCrypto era), SigningKey))
-> Target era (Gen (Set (Addr (EraCrypto era))))
addrUnivT Proof era
p Int
naddr Term era Network
net Term era (Set (Credential 'Payment (EraCrypto era)))
ps Term era (Set Ptr)
pts Term era (Set (Credential 'Staking (EraCrypto era)))
cs Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUnivT =
  forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"" (forall a. Ord a => [String] -> Int -> Gen a -> Gen (Set a)
setSized [String
"From addrUnivT"] Int
naddr)
    forall era r a b.
RootTarget era r (a -> b)
-> RootTarget era r a -> RootTarget era r b
:$ (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"genAddrWith" (forall era.
Proof era
-> Network
-> Set (Credential 'Payment (EraCrypto era))
-> Set Ptr
-> Set (Credential 'Staking (EraCrypto era))
-> Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey)
-> Gen (Addr (EraCrypto era))
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 (Credential 'Payment (EraCrypto era)))
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 (EraCrypto era)))
cs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUnivT)

makeHashScriptMapT ::
  Proof era ->
  Int ->
  PlutusPurposeTag ->
  Term era (Map (KeyHash 'Witness (EraCrypto era)) (KeyPair 'Witness (EraCrypto era))) ->
  Term era ValidityInterval ->
  Target era (Gen (Map (ScriptHash (EraCrypto era)) (ScriptF era)))
makeHashScriptMapT :: forall era.
Proof era
-> Int
-> PlutusPurposeTag
-> Term
     era
     (Map
        (KeyHash 'Witness (EraCrypto era))
        (KeyPair 'Witness (EraCrypto era)))
-> Term era ValidityInterval
-> Target
     era (Gen (Map (ScriptHash (EraCrypto era)) (ScriptF era)))
makeHashScriptMapT Proof era
p Int
size PlutusPurposeTag
tag Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
m Term era ValidityInterval
vi =
  forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era))
-> ValidityInterval
-> Gen (Map (ScriptHash (EraCrypto era)) (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 (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
m
    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era ValidityInterval
vi

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

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

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

txinToGovactionId :: TxIn c -> GovActionId c
txinToGovactionId :: forall c. TxIn c -> GovActionId c
txinToGovactionId (TxIn TxId c
idx (TxIx Word64
n)) = forall c. TxId c -> GovActionIx -> GovActionId c
GovActionId TxId c
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 a era. Sizeable a => Term era Size -> Term era a -> 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 a era. Sizeable a => Term era Size -> Term era a -> 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 a era. Sizeable a => Term era Size -> Term era a -> 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 a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumKeys UnivSize
size)) Term era [KeyPair 'Witness (EraCrypto era)]
keypairs
  , forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"xx" (\[KeyPair 'Witness StandardCrypto]
s -> forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. (a -> b) -> [a] -> [b]
map (\KeyPair 'Witness StandardCrypto
x -> (forall c (kd :: KeyRole). Crypto c => VKey kd c -> KeyHash kd c
hashKey (forall (kd :: KeyRole) c. KeyPair kd c -> VKey kd c
vKey KeyPair 'Witness StandardCrypto
x), KeyPair 'Witness StandardCrypto
x)) [KeyPair 'Witness StandardCrypto]
s)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [KeyPair 'Witness (EraCrypto era)]
keypairs)
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumPools UnivSize
size)) Term era (Set (KeyHash 'Witness (EraCrypto era)))
prePoolUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness (EraCrypto era)))
prePoolUniv (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv)
  , forall era.
Era era =>
Term era (Set (KeyHash 'StakePool (EraCrypto era)))
poolHashUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"WitnessToStakePool" forall c (k :: KeyRole).
Set (KeyHash 'Witness c) -> Set (KeyHash k c)
cast forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness (EraCrypto era)))
prePoolUniv)
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumStakeKeys UnivSize
size)) Term era (Set (KeyHash 'Witness (EraCrypto era)))
preStakeUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness (EraCrypto era)))
preStakeUniv (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv)
  , forall era.
Era era =>
Term era (Set (KeyHash 'Staking (EraCrypto era)))
stakeHashUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"WitnessToStaking" forall c (k :: KeyRole).
Set (KeyHash 'Witness c) -> Set (KeyHash k c)
cast forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness (EraCrypto era)))
preStakeUniv)
  , forall era.
Era era =>
Term era (Set (KeyHash 'DRepRole (EraCrypto era)))
drepHashUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"WitnessToDRepRole" forall c (k :: KeyRole).
Set (KeyHash 'Witness c) -> Set (KeyHash k c)
cast forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness (EraCrypto era)))
preStakeUniv)
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumGenesisKeys UnivSize
size)) Term era (Set (KeyHash 'Witness (EraCrypto era)))
preGenesisUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness (EraCrypto era)))
preGenesisUniv (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv)
  , Term era (Set (KeyHash 'Genesis (EraCrypto era)))
preGenesisDom forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"WitnessToGenesis" forall c (k :: KeyRole).
Set (KeyHash 'Witness c) -> Set (KeyHash k c)
cast forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness (EraCrypto era)))
preGenesisUniv)
  , Term era (Set (KeyHash 'Genesis (EraCrypto era)))
preGenesisDom forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
genesisHashUniv)
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumVoteKeys UnivSize
size)) Term era (Set (KeyHash 'Witness (EraCrypto era)))
preVoteUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness (EraCrypto era)))
preVoteUniv (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv)
  , forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
voteCredUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"WitnessToStakePool" forall c.
Set (KeyHash 'Witness c) -> Set (Credential 'ColdCommitteeRole c)
castCredCold forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness (EraCrypto era)))
preVoteUniv)
  , forall a era. Sizeable a => Term era Size -> Term era a -> 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 (EraCrypto era)))
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 (EraCrypto era))
feeTxIn) forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
txinUniv
  , forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
govActionIdUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"TxIn-to-GovActionId" (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. TxIn c -> GovActionId c
txinToGovactionId) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
txinUniv)
  , forall era. Era era => Term era ValidityInterval
validityInterval forall era a r. Term era a -> RootTarget era r a -> 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 a.
(Era era, Eq a) =>
Term era Size
-> Term era [a] -> [(Int, Target era a, [Pred era])] -> Pred era
Choose
      (forall era. Era era => Int -> Term era Size
ExactSize (UnivSize -> Int
usNumCredentials UnivSize
size))
      Term era [Credential 'Staking (EraCrypto era)]
credList
      [
        ( UnivSize -> Int
usCredScriptFreq UnivSize
size
        , forall era (k :: KeyRole).
Term era (ScriptHash (EraCrypto era))
-> Target era (Credential k (EraCrypto era))
scriptHashObjT Term era (ScriptHash (EraCrypto era))
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 (EraCrypto era))
scripthash) (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
nonSpendScriptUniv Proof era
p))]
        )
      , (Int
1, forall era (k :: KeyRole).
Term era (KeyHash 'Witness (EraCrypto era))
-> Target era (Credential k (EraCrypto era))
keyHashObjT Term era (KeyHash 'Witness (EraCrypto era))
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 (EraCrypto era))
keyhash) (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv)])
      ]
  , forall era.
Era era =>
Term era (Set (Credential 'Staking (EraCrypto era)))
credsUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: forall x era. Ord x => Term era [x] -> Target era (Set x)
listToSetTarget Term era [Credential 'Staking (EraCrypto era)]
credList
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
spendscriptUniv Proof era
p) (forall era.
Proof era
-> Int
-> PlutusPurposeTag
-> Term
     era
     (Map
        (KeyHash 'Witness (EraCrypto era))
        (KeyPair 'Witness (EraCrypto era)))
-> Term era ValidityInterval
-> Target
     era (Gen (Map (ScriptHash (EraCrypto era)) (ScriptF era)))
makeHashScriptMapT Proof era
p Int
25 PlutusPurposeTag
Spending forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv forall era. Era era => Term era ValidityInterval
validityInterval)
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
nonSpendScriptUniv Proof era
p) (forall era.
Proof era
-> Int
-> PlutusPurposeTag
-> Term
     era
     (Map
        (KeyHash 'Witness (EraCrypto era))
        (KeyPair 'Witness (EraCrypto era)))
-> Term era ValidityInterval
-> Target
     era (Gen (Map (ScriptHash (EraCrypto era)) (ScriptF era)))
makeHashScriptMapT Proof era
p Int
25 PlutusPurposeTag
Certifying forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv forall era. Era era => Term era ValidityInterval
validityInterval)
  , forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
allScriptUniv Proof era
p forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 (EraCrypto era)) (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 (EraCrypto era)) (ScriptF era))
nonSpendScriptUniv Proof era
p))
  , forall era a.
(Era era, Eq a) =>
Term era Size
-> Term era [a] -> [(Int, Target era a, [Pred era])] -> Pred era
Choose
      (forall era. Era era => Int -> Term era Size
ExactSize Int
70)
      Term era [Credential 'Payment (EraCrypto era)]
spendcredList
      [
        ( UnivSize -> Int
usSpendScriptFreq UnivSize
size
        , forall era (k :: KeyRole).
Term era (ScriptHash (EraCrypto era))
-> Target era (Credential k (EraCrypto era))
scriptHashObjT Term era (ScriptHash (EraCrypto era))
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 (EraCrypto era))
scripthash) (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
spendscriptUniv Proof era
p))]
        )
      , (Int
2, forall era (k :: KeyRole).
Term era (KeyHash 'Witness (EraCrypto era))
-> Target era (Credential k (EraCrypto era))
keyHashObjT Term era (KeyHash 'Witness (EraCrypto era))
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 (EraCrypto era))
keyhash) (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv)])
      ]
  , forall era.
Era era =>
Term era (Set (Credential 'Payment (EraCrypto era)))
spendCredsUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: forall x era. Ord x => Term era [x] -> Target era (Set x)
listToSetTarget Term era [Credential 'Payment (EraCrypto era)]
spendcredList
  , forall era. Era era => Term era EpochNo
currentEpoch forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom forall era.
Era era =>
Term era (Map (DataHash (EraCrypto era)) (Data era))
dataUniv (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"dataWits" (forall era.
Era era =>
Proof era -> Int -> Gen (Map (DataHash (EraCrypto era)) (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 a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom forall era. Era era => Term era [Datum era]
datumsUniv (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"genDatums" (forall era.
Era era =>
UnivSize
-> Int
-> Map (DataHash (EraCrypto era)) (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 (EraCrypto era)) (Data era))
dataUniv)
  , -- 'network' is set by testGlobals which contains 'Testnet'
    forall era. Era era => Term era Network
network forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: forall t era. t -> Target era t
constTarget (Globals -> Network
Utils.networkId Globals
Utils.testGlobals)
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> 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 a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"byronUniv" forall c.
Crypto c =>
Network -> Gen (Map (KeyHash 'Payment c) (Addr c, 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 a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom
      forall era. Era era => Term era (Set (Addr (EraCrypto era)))
addrUniv
      (forall era.
Proof era
-> Int
-> Term era Network
-> Term era (Set (Credential 'Payment (EraCrypto era)))
-> Term era (Set Ptr)
-> Term era (Set (Credential 'Staking (EraCrypto era)))
-> Term
     era
     (Map
        (KeyHash 'Payment (EraCrypto era))
        (Addr (EraCrypto era), SigningKey))
-> Target era (Gen (Set (Addr (EraCrypto era))))
addrUnivT Proof era
p (UnivSize -> Int
usNumAddr UnivSize
size) forall era. Era era => Term era Network
network forall era.
Era era =>
Term era (Set (Credential 'Payment (EraCrypto era)))
spendCredsUniv forall era. Era era => Term era (Set Ptr)
ptrUniv forall era.
Era era =>
Term era (Set (Credential 'Staking (EraCrypto era)))
credsUniv forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv)
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom
      forall era. Era era => Term era [MultiAsset (EraCrypto era)]
multiAssetUniv
      (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 (EraCrypto era)) (ScriptF era)
-> Gen (MultiAsset (EraCrypto era))
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 (EraCrypto era)) (ScriptF era))
nonSpendScriptUniv Proof era
p))
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom
      Term era [TxOutF era]
preTxoutUniv
      ( forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"genTxOuts" (forall era.
Reflect era =>
UnivSize
-> (Coin
    -> Map (ScriptHash (EraCrypto era)) (ScriptF era)
    -> Gen (Value era))
-> Proof era
-> Int
-> Set (Addr (EraCrypto era))
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map (DataHash (EraCrypto era)) (Data era)
-> Gen [TxOutF era]
genTxOuts UnivSize
size (forall era.
UnivSize
-> Proof era
-> Coin
-> Map (ScriptHash (EraCrypto era)) (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 (EraCrypto era)))
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 (EraCrypto era)) (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 (EraCrypto era)) (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 (EraCrypto era)) (Data era))
dataUniv
      )
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom
      (forall era. Era era => Proof era -> Term era (Set (TxOutF era))
colTxoutUniv Proof era
p)
      ( forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr
          String
"colTxOutUniv"
          (\Set (Addr StandardCrypto)
x -> forall era.
EraTxOut era =>
Proof era -> Set (Addr (EraCrypto era)) -> Gen (Set (TxOutF era))
colTxOutSetT Proof era
p (forall a. (a -> Bool) -> Set a -> Set a
Set.filter (forall era. Proof era -> Addr (EraCrypto era) -> Bool
noScripts Proof era
p) Set (Addr StandardCrypto)
x))
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set (Addr (EraCrypto era)))
addrUniv
      )
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom forall era. Era era => Term era (Set (DRep (EraCrypto era)))
drepUniv (forall era.
UnivSize
-> Term era (Set (Credential 'Staking (EraCrypto era)))
-> Target era (Gen (Set (DRep (EraCrypto era))))
genDRepsT UnivSize
size forall era.
Era era =>
Term era (Set (Credential 'Staking (EraCrypto era)))
credsUniv)
  , forall era.
Era era =>
Term era (Set (Credential 'Payment (EraCrypto era)))
payUniv forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era.
Era era =>
Term era (Set (Credential 'Payment (EraCrypto era)))
spendCredsUniv
  , forall era.
Era era =>
Term era (Set (Credential 'DRepRole (EraCrypto era)))
voteUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"coerce" (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. Credential 'Staking c -> Credential 'DRepRole c
stakeToDRepRole) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Set (Credential 'Staking (EraCrypto era)))
credsUniv)
  , forall era.
Era era =>
Term era (Set (Credential 'HotCommitteeRole (EraCrypto era)))
hotCommitteeCredsUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"coerce" (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. Credential 'Staking c -> Credential 'HotCommitteeRole c
stakeToHotCommittee) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Set (Credential 'Staking (EraCrypto era)))
credsUniv)
  , forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
coldCommitteeCredsUniv forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"coerce" (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. Credential 'Staking c -> Credential 'ColdCommitteeRole c
stakeToColdCommittee) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Set (Credential 'Staking (EraCrypto era)))
credsUniv)
  , forall era. Era era => Term era Coin
bigCoin forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: forall t era. t -> Target era t
constTarget (Integer -> Coin
Coin Integer
2000000)
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom
      forall era. Reflect era => Term era (TxOutF era)
feeTxOut
      ( forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr
          String
"txout"
          ( \Set (Addr StandardCrypto)
a Coin
c ->
              forall era.
Reflect era =>
Proof era -> Addr (EraCrypto era) -> 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 (EraCrypto era) -> Bool
noScripts Proof era
p) Set (Addr StandardCrypto)
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 (EraCrypto era)))
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 a r. Term era a -> RootTarget era r a -> Pred era
:<-: ( forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 (EraCrypto era)) (IsValid, ScriptF era))
plutusUniv forall era a r. Term era a -> RootTarget era r a -> 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 (EraCrypto era)) (IsValid, Script era)
allPlutusScripts Proof era
p))
  , forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (IsValid, ScriptF era))
spendPlutusUniv forall era a r. Term era a -> RootTarget era r a -> 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 (EraCrypto era)) (IsValid, Script era)
spendPlutusScripts Proof era
p))
  ]
  where
    credList :: Term era [Credential 'Staking (EraCrypto era)]
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 (EraCrypto era))
CredR) forall era s t. Access era s t
No)
    spendcredList :: Term era [Credential 'Payment (EraCrypto era)]
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 (Credential 'Payment (EraCrypto era))
PCredR) forall era s t. Access era s t
No)
    keyhash :: Term era (KeyHash 'Witness (EraCrypto era))
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 (EraCrypto era))
WitHashR forall era s t. Access era s t
No)
    scripthash :: Term era (ScriptHash (EraCrypto era))
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 (EraCrypto era))
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 (EraCrypto era)]
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 (EraCrypto era))
KeyPairR) forall era s t. Access era s t
No)
    prePoolUniv :: Term era (Set (KeyHash 'Witness (EraCrypto era)))
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 (EraCrypto era))
WitHashR) forall era s t. Access era s t
No)
    preStakeUniv :: Term era (Set (KeyHash 'Witness (EraCrypto era)))
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 (EraCrypto era))
WitHashR) forall era s t. Access era s t
No)
    preGenesisUniv :: Term era (Set (KeyHash 'Witness (EraCrypto era)))
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 (EraCrypto era))
WitHashR) forall era s t. Access era s t
No)
    preGenesisDom :: Term era (Set (KeyHash 'Genesis (EraCrypto era)))
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 (EraCrypto era))
GenHashR) forall era s t. Access era s t
No)
    preVoteUniv :: Term era (Set (KeyHash 'Witness (EraCrypto era)))
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 (EraCrypto era))
WitHashR) forall era s t. Access era s t
No)

multiAsset ::
  UnivSize -> Map.Map (ScriptHash (EraCrypto era)) (ScriptF era) -> Gen (MultiAsset (EraCrypto era))
multiAsset :: forall era.
UnivSize
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (MultiAsset (EraCrypto era))
multiAsset UnivSize
size Map (ScriptHash (EraCrypto era)) (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 (EraCrypto era), AssetName, Integer)]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era.
Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Set AssetName
-> Gen Integer
-> Gen (PolicyID (EraCrypto era), AssetName, Integer)
genMultiAssetTriple Map (ScriptHash (EraCrypto era)) (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
$ forall era. [(PolicyID era, AssetName, Integer)] -> MultiAsset era
multiAssetFromList [(PolicyID (EraCrypto era), AssetName, Integer)]
xs

genValueF ::
  UnivSize -> Proof era -> Coin -> Map (ScriptHash (EraCrypto era)) (ScriptF era) -> Gen (Value era)
genValueF :: forall era.
UnivSize
-> Proof era
-> Coin
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (Value era)
genValueF UnivSize
size Proof era
proof Coin
c Map (ScriptHash (EraCrypto era)) (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 -> forall c. Coin -> MultiAsset c -> MaryValue c
MaryValue Coin
c forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era.
UnivSize
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (MultiAsset (EraCrypto era))
multiAsset UnivSize
size Map (ScriptHash (EraCrypto era)) (ScriptF era)
scripts

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

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

stakeToColdCommittee :: Credential 'Staking c -> Credential 'ColdCommitteeRole c
stakeToColdCommittee :: forall c. Credential 'Staking c -> Credential 'ColdCommitteeRole c
stakeToColdCommittee = forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
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 StandardCrypto)
proof = Proof (ShelleyEra StandardCrypto)
Shelley
  Subst (ShelleyEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
subst)
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Env (ShelleyEra StandardCrypto)
env <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst (ShelleyEra StandardCrypto)
subst forall era. Env era
emptyEnv)
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof (ShelleyEra StandardCrypto)
proof Env (ShelleyEra StandardCrypto)
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)