{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Cardano.Ledger.Generic.Properties where

import Cardano.Ledger.Alonzo.Tx (AlonzoTxBody (..), IsValid (..))
import Cardano.Ledger.Babbage.TxBody (BabbageTxBody (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core
import qualified Cardano.Ledger.Shelley as S (ShelleyEra)
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  UTxOState (..),
  updateStakeDistribution,
 )
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..), UtxoEnv (..))
import Cardano.Ledger.UTxO (UTxO (..))
import Cardano.Slotting.Slot (SlotNo (..))
import Control.Monad.Trans.RWS.Strict (gets)
import Control.State.Transition.Extended hiding (Assertion)
import Data.Coerce (coerce)
import Data.Default (Default (def))
import qualified Data.Map.Strict as Map
import Test.Cardano.Ledger.Alonzo.Serialisation.Generators ()
import Test.Cardano.Ledger.Babbage.Arbitrary ()
import Test.Cardano.Ledger.Binary.Arbitrary ()
import Test.Cardano.Ledger.Binary.Twiddle (Twiddle, twiddleInvariantProp)
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Generic.Fields (
  abstractTx,
  abstractTxBody,
  abstractTxOut,
  abstractWitnesses,
 )
import Test.Cardano.Ledger.Generic.Functions (TotalAda (totalAda), isValid')
import Test.Cardano.Ledger.Generic.GenState (
  GenEnv (..),
  GenRS,
  GenSize (..),
  GenState (..),
  blocksizeMax,
  initStableFields,
  modifyModel,
  runGenRS,
 )
import Test.Cardano.Ledger.Generic.MockChain (MOCKCHAIN, MockChainState (..))
import Test.Cardano.Ledger.Generic.ModelState
import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (..), pcLedgerState, pcTx)
import Test.Cardano.Ledger.Generic.Proof hiding (lift)
import Test.Cardano.Ledger.Generic.Trace (
  Gen1,
  forEachEpochTrace,
  testPropMax,
  testTraces,
  traceProp,
 )
import Test.Cardano.Ledger.Generic.TxGen (
  Box (..),
  applySTSByProof,
  assembleWits,
  coreTx,
  coreTxBody,
  coreTxOut,
  genAlonzoTx,
  genUTxO,
 )
import Test.Cardano.Ledger.Shelley.Serialisation.EraIndepGenerators ()
import Test.Control.State.Transition.Trace (Trace (..), lastState)
import Test.Control.State.Transition.Trace.Generator.QuickCheck (HasTrace (..))
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain, testGroup)

-- =====================================
-- Top level generators of TRC

genTxAndUTXOState ::
  Reflect era => Proof era -> GenSize -> Gen (TRC (EraRule "UTXOW" era), GenState era)
genTxAndUTXOState :: forall era.
Reflect era =>
Proof era
-> GenSize -> Gen (TRC (EraRule "UTXOW" era), GenState era)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Conway GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams ConwayEra
pp AccountState
_ Bool
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof GenSize
gsize
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams ConwayEra
pp forall a. Default a => a
def, forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Babbage GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams BabbageEra
pp AccountState
_ Bool
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof GenSize
gsize
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams BabbageEra
pp forall a. Default a => a
def, forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Alonzo GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams AlonzoEra
pp AccountState
_ Bool
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof GenSize
gsize
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams AlonzoEra
pp forall a. Default a => a
def, forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Mary GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams MaryEra
pp AccountState
_ Bool
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof GenSize
gsize
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams MaryEra
pp forall a. Default a => a
def, forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Allegra GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams AllegraEra
pp AccountState
_ Bool
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof GenSize
gsize
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams AllegraEra
pp forall a. Default a => a
def, forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Shelley GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams ShelleyEra
pp AccountState
_ Bool
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof GenSize
gsize
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams ShelleyEra
pp forall a. Default a => a
def, forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)

genTxAndLEDGERStateShelley ::
  GenSize -> Gen (TRC (EraRule "LEDGER" S.ShelleyEra), GenState S.ShelleyEra)
genTxAndLEDGERStateShelley :: GenSize
-> Gen (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
genTxAndLEDGERStateShelley GenSize
genSize = do
  Box Proof ShelleyEra
_ TRC (EraRule "LEDGER" ShelleyEra)
trc GenState ShelleyEra
genState <- forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof ShelleyEra
Shelley GenSize
genSize
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TRC (EraRule "LEDGER" ShelleyEra)
trc, GenState ShelleyEra
genState)

testTxValidForLEDGERShelley ::
  (TRC (EraRule "LEDGER" S.ShelleyEra), GenState S.ShelleyEra) -> Property
testTxValidForLEDGERShelley :: (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
-> Property
testTxValidForLEDGERShelley (TRC (EraRule "LEDGER" ShelleyEra)
trc, GenState ShelleyEra
genState) =
  forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 PrettyA (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof ShelleyEra
Shelley (forall era.
Proof era -> TRC (EraRule "LEDGER" era) -> GenState era -> Box era
Box Proof ShelleyEra
Shelley TRC (EraRule "LEDGER" ShelleyEra)
trc GenState ShelleyEra
genState)

genTxAndLEDGERState ::
  forall era.
  ( Reflect era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  ) =>
  Proof era ->
  GenSize ->
  Gen (Box era)
genTxAndLEDGERState :: forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof GenSize
sizes = do
  let slotNo :: SlotNo
slotNo = Word64 -> SlotNo
SlotNo (GenSize -> Word64
startSlot GenSize
sizes)
  TxIx
txIx <- forall a. Arbitrary a => Gen a
arbitrary
  let genT :: RWST
  (GenEnv era) () (GenState era) Gen (TRC (EraRule "LEDGER" era))
genT = do
        (Map TxIn (TxOut era)
initial, Maybe (TxIn, TxOut era)
_) <- forall era.
Reflect era =>
GenRS era (MUtxo era, Maybe (UtxoEntry era))
genUTxO -- Generate a random UTxO, so mUTxO is not empty
        forall era.
(ModelNewEpochState era -> ModelNewEpochState era) -> GenRS era ()
modifyModel (\ModelNewEpochState era
m -> ModelNewEpochState era
m {mUTxO :: Map TxIn (TxOut era)
mUTxO = Map TxIn (TxOut era)
initial})
        (UTxO era
_utxo, Tx era
tx) <- forall era.
Reflect era =>
Proof era -> SlotNo -> GenRS era (UTxO era, Tx era)
genAlonzoTx Proof era
proof SlotNo
slotNo
        ModelNewEpochState era
model <- forall w (m :: * -> *) s a r.
(Monoid w, Monad m) =>
(s -> a) -> RWST r w s m a
gets forall era. GenState era -> ModelNewEpochState era
gsModel
        PParams era
pp <- forall w (m :: * -> *) s a r.
(Monoid w, Monad m) =>
(s -> a) -> RWST r w s m a
gets (forall era. GenEnv era -> PParams era
gePParams forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. GenState era -> GenEnv era
gsGenEnv)
        let ledgerState :: LedgerState era
ledgerState = forall t era. Extract t era => ModelNewEpochState era -> t
extract @(LedgerState era) ModelNewEpochState era
model
            ledgerEnv :: LedgerEnv era
ledgerEnv = forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> AccountState
-> Bool
-> LedgerEnv era
LedgerEnv SlotNo
slotNo forall a. Maybe a
Nothing TxIx
txIx PParams era
pp (Coin -> Coin -> AccountState
AccountState (Integer -> Coin
Coin Integer
0) (Integer -> Coin
Coin Integer
0)) Bool
False
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
ledgerEnv, LedgerState era
ledgerState, Tx era
tx)
  (TRC (EraRule "LEDGER" era)
trc, GenState era
genstate) <- forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof era
proof GenSize
sizes (forall era. Reflect era => GenRS era ()
initStableFields forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RWST
  (GenEnv era) () (GenState era) Gen (TRC (EraRule "LEDGER" era))
genT)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
Proof era -> TRC (EraRule "LEDGER" era) -> GenState era -> Box era
Box Proof era
proof TRC (EraRule "LEDGER" era)
trc GenState era
genstate)

-- =============================================
-- Now a test

testTxValidForLEDGER ::
  ( Reflect era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , PrettyA (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  Proof era ->
  Box era ->
  Property
testTxValidForLEDGER :: forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 PrettyA (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof era
proof (Box Proof era
_ trc :: TRC (EraRule "LEDGER" era)
trc@(TRC (Environment (EraRule "LEDGER" era)
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
_genstate) =
  -- trc encodes the initial (generated) state, vtx is the transaction
  case forall era.
Era era =>
Proof era
-> RuleContext 'Transition (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era))
applySTSByProof Proof era
proof TRC (EraRule "LEDGER" era)
trc of
    Right State (EraRule "LEDGER" era)
ledgerState' ->
      -- UTxOState and CertState after applying the transaction $$$
      forall prop. Testable prop => Bool -> [Char] -> prop -> Property
classify (coerce :: forall a b. Coercible a b => a -> b
coerce (forall era. Proof era -> Tx era -> IsValid
isValid' Proof era
proof Signal (EraRule "LEDGER" era)
vtx)) [Char]
"TxValid" forall a b. (a -> b) -> a -> b
$
        forall t. TotalAda t => t -> Coin
totalAda State (EraRule "LEDGER" era)
ledgerState' forall a. (Eq a, Show a) => a -> a -> Property
=== forall t. TotalAda t => t -> Coin
totalAda State (EraRule "LEDGER" era)
ledgerState
    Left NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs ->
      forall prop. Testable prop => [Char] -> prop -> Property
counterexample
        ( forall a. Show a => a -> [Char]
show (forall era. Proof era -> LedgerState era -> PDoc
pcLedgerState Proof era
proof State (EraRule "LEDGER" era)
ledgerState)
            forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall era. Proof era -> Tx era -> PDoc
pcTx Proof era
proof Signal (EraRule "LEDGER" era)
vtx)
            forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs)
        )
        (forall prop. Testable prop => prop -> Property
property Bool
False)

-- =============================================
-- Make some property tests

-- =========================================================================
-- The generic types make a roundtrip without adding or losing information

txOutRoundTrip ::
  EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip :: forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof era
proof TxOut era
x = forall era. Proof era -> [TxOutField era] -> TxOut era
coreTxOut Proof era
proof (forall era. Era era => Proof era -> TxOut era -> [TxOutField era]
abstractTxOut Proof era
proof TxOut era
x) forall a. (Eq a, Show a) => a -> a -> Property
=== TxOut era
x

txRoundTrip ::
  EraTx era => Proof era -> Tx era -> Property
txRoundTrip :: forall era. EraTx era => Proof era -> Tx era -> Property
txRoundTrip Proof era
proof Tx era
x = forall era. Proof era -> [TxField era] -> Tx era
coreTx Proof era
proof (forall era. Proof era -> Tx era -> [TxField era]
abstractTx Proof era
proof Tx era
x) forall a. (Eq a, Show a) => a -> a -> Property
=== Tx era
x

txBodyRoundTrip ::
  EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip :: forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof era
proof TxBody era
x = forall era.
EraTxBody era =>
Proof era -> [TxBodyField era] -> TxBody era
coreTxBody Proof era
proof (forall era. Proof era -> TxBody era -> [TxBodyField era]
abstractTxBody Proof era
proof TxBody era
x) forall a. (Eq a, Show a) => a -> a -> Property
=== TxBody era
x

txWitRoundTrip ::
  EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip :: forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof era
proof TxWits era
x = forall era. Proof era -> [WitnessesField era] -> TxWits era
assembleWits Proof era
proof (forall era. Proof era -> TxWits era -> [WitnessesField era]
abstractWitnesses Proof era
proof TxWits era
x) forall a. (Eq a, Show a) => a -> a -> Property
=== TxWits era
x

coreTypesRoundTrip :: TestTree
coreTypesRoundTrip :: TestTree
coreTypesRoundTrip =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Core types make generic roundtrips"
    [ [Char] -> [TestTree] -> TestTree
testGroup
        [Char]
"TxWits roundtrip"
        [ forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof BabbageEra
Babbage
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof AlonzoEra
Alonzo
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof MaryEra
Mary
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof AllegraEra
Allegra
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof ShelleyEra
Shelley
        ]
    , [Char] -> [TestTree] -> TestTree
testGroup
        [Char]
"TxBody roundtrips"
        [ forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof BabbageEra
Babbage
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof AlonzoEra
Alonzo
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof MaryEra
Mary
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof AllegraEra
Allegra
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof ShelleyEra
Shelley
        ]
    , [Char] -> [TestTree] -> TestTree
testGroup
        [Char]
"TxOut roundtrips"
        [ forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof BabbageEra
Babbage
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof AlonzoEra
Alonzo
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof MaryEra
Mary
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof AllegraEra
Allegra
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley era" forall a b. (a -> b) -> a -> b
$ forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof ShelleyEra
Shelley
        ]
    , [Char] -> [TestTree] -> TestTree
testGroup
        [Char]
"Tx roundtrips"
        [ forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage era" forall a b. (a -> b) -> a -> b
$ forall era. EraTx era => Proof era -> Tx era -> Property
txRoundTrip Proof BabbageEra
Babbage
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo era" forall a b. (a -> b) -> a -> b
$ forall era. EraTx era => Proof era -> Tx era -> Property
txRoundTrip Proof AlonzoEra
Alonzo
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary era" forall a b. (a -> b) -> a -> b
$ forall era. EraTx era => Proof era -> Tx era -> Property
txRoundTrip Proof MaryEra
Mary
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra era" forall a b. (a -> b) -> a -> b
$ forall era. EraTx era => Proof era -> Tx era -> Property
txRoundTrip Proof AllegraEra
Allegra
        , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley era" forall a b. (a -> b) -> a -> b
$ forall era. EraTx era => Proof era -> Tx era -> Property
txRoundTrip Proof ShelleyEra
Shelley
        ]
    ]

-- | A single Tx preserves Ada
txPreserveAda :: GenSize -> TestTree
txPreserveAda :: GenSize -> TestTree
txPreserveAda GenSize
genSize =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Individual Tx's preserve Ada"
    [ forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley Tx preservers Ada" forall a b. (a -> b) -> a -> b
$
        forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (GenSize
-> Gen (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
genTxAndLEDGERStateShelley GenSize
genSize) ((TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
-> Property
testTxValidForLEDGERShelley)
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra Tx preserves ADA" forall a b. (a -> b) -> a -> b
$
        forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof AllegraEra
Allegra GenSize
genSize) (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 PrettyA (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof AllegraEra
Allegra)
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary Tx preserves ADA" forall a b. (a -> b) -> a -> b
$
        forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof MaryEra
Mary GenSize
genSize) (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 PrettyA (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof MaryEra
Mary)
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo ValidTx preserves ADA" forall a b. (a -> b) -> a -> b
$
        forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof AlonzoEra
Alonzo GenSize
genSize) (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 PrettyA (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof AlonzoEra
Alonzo)
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage ValidTx preserves ADA" forall a b. (a -> b) -> a -> b
$
        forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof BabbageEra
Babbage GenSize
genSize) (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 PrettyA (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof BabbageEra
Babbage)
        -- TODO
        -- testPropMax 30 "Conway ValidTx preserves ADA" $
        --  forAll (genTxAndLEDGERState Conway genSize) (testTxValidForLEDGER Conway)
    ]

-- | Ada is preserved over a trace of length 100
adaIsPreserved ::
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  TestTree
adaIsPreserved :: forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof era
proof Int
numTx GenSize
gensize =
  forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (forall a. Show a => a -> [Char]
show Proof era
proof forall a. [a] -> [a] -> [a]
++ [Char]
" era. Trace length = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
numTx) forall a b. (a -> b) -> a -> b
$
    forall era prop.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int
-> GenSize
-> (MockChainState era -> MockChainState era -> prop)
-> Gen prop
traceProp
      Proof era
proof
      Int
numTx
      GenSize
gensize
      (\MockChainState era
firstSt MockChainState era
lastSt -> forall t. TotalAda t => t -> Coin
totalAda (forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
firstSt) forall a. (Eq a, Show a) => a -> a -> Property
=== forall t. TotalAda t => t -> Coin
totalAda (forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
lastSt))

tracePreserveAda :: Int -> GenSize -> TestTree
tracePreserveAda :: Int -> GenSize -> TestTree
tracePreserveAda Int
numTx GenSize
gensize =
  [Char] -> [TestTree] -> TestTree
testGroup
    ([Char]
"Total Ada is preserved over traces of length " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
numTx)
    [ Int -> GenSize -> TestTree
adaIsPreservedBabbage Int
numTx GenSize
gensize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof AlonzoEra
Alonzo Int
numTx GenSize
gensize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof MaryEra
Mary Int
numTx GenSize
gensize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof AllegraEra
Allegra Int
numTx GenSize
gensize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof ShelleyEra
Shelley Int
numTx GenSize
gensize
    ]

adaIsPreservedBabbage :: Int -> GenSize -> TestTree
adaIsPreservedBabbage :: Int -> GenSize -> TestTree
adaIsPreservedBabbage Int
numTx GenSize
gensize = forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof BabbageEra
Babbage Int
numTx GenSize
gensize

-- | The incremental Stake invaraint is preserved over a trace of length 100=
stakeInvariant :: EraTxOut era => MockChainState era -> MockChainState era -> Property
stakeInvariant :: forall era.
EraTxOut era =>
MockChainState era -> MockChainState era -> Property
stakeInvariant (MockChainState NewEpochState era
_ NewEpochState era
_ SlotNo
_ Int
_) (MockChainState NewEpochState era
nes NewEpochState era
_ SlotNo
_ Int
_) =
  case (forall era. LedgerState era -> UTxOState era
lsUTxOState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs) NewEpochState era
nes of
    (UTxOState UTxO era
utxo Coin
_ Coin
_ GovState era
_ IncrementalStake
istake Coin
_) -> IncrementalStake
istake forall a. (Eq a, Show a) => a -> a -> Property
=== forall era.
EraTxOut era =>
PParams era
-> IncrementalStake -> UTxO era -> UTxO era -> IncrementalStake
updateStakeDistribution forall a. Default a => a
def forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty UTxO era
utxo

incrementStakeInvariant ::
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof era ->
  GenSize ->
  TestTree
incrementStakeInvariant :: forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof era
proof GenSize
gensize =
  forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (forall a. Show a => a -> [Char]
show Proof era
proof forall a. [a] -> [a] -> [a]
++ [Char]
" era. Trace length = 100") forall a b. (a -> b) -> a -> b
$
    forall era prop.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int
-> GenSize
-> (MockChainState era -> MockChainState era -> prop)
-> Gen prop
traceProp Proof era
proof Int
100 GenSize
gensize forall era.
EraTxOut era =>
MockChainState era -> MockChainState era -> Property
stakeInvariant

incrementalStake :: GenSize -> TestTree
incrementalStake :: GenSize -> TestTree
incrementalStake GenSize
genSize =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Incremental Stake invariant holds"
    [ -- TODO re-enable this once we have added all the new rules to Conway
      -- incrementStakeInvariant Conway genSize,
      forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof BabbageEra
Babbage GenSize
genSize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof AlonzoEra
Alonzo GenSize
genSize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof MaryEra
Mary GenSize
genSize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof AllegraEra
Allegra GenSize
genSize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof ShelleyEra
Shelley GenSize
genSize
    ]

genericProperties :: GenSize -> TestTree
genericProperties :: GenSize -> TestTree
genericProperties GenSize
genSize =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Generic Property tests"
    [ TestTree
coreTypesRoundTrip
    , GenSize -> TestTree
txPreserveAda GenSize
genSize
    , Int -> GenSize -> TestTree
tracePreserveAda Int
45 GenSize
genSize
    , GenSize -> TestTree
incrementalStake GenSize
genSize
    , Int -> TestTree
testTraces Int
45
    , GenSize -> TestTree
epochPreserveAda GenSize
genSize
    , TestTree
twiddleInvariantHoldsEras
    ]

epochPreserveAda :: GenSize -> TestTree
epochPreserveAda :: GenSize -> TestTree
epochPreserveAda GenSize
genSize =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Ada is preserved in each epoch"
    [ forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof BabbageEra
Babbage GenSize
genSize
    , forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof AlonzoEra
Alonzo GenSize
genSize
    , forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof MaryEra
Mary GenSize
genSize
    , forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof AllegraEra
Allegra GenSize
genSize
    , forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof ShelleyEra
Shelley GenSize
genSize
    ]

adaIsPreservedInEachEpoch ::
  forall era.
  Reflect era =>
  Proof era ->
  GenSize ->
  TestTree
adaIsPreservedInEachEpoch :: forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof era
proof GenSize
genSize =
  forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (forall a. Show a => a -> [Char]
show Proof era
proof) forall a b. (a -> b) -> a -> b
$
    forall era prop.
(Testable prop, Reflect era) =>
Proof era
-> Int
-> GenSize
-> (Trace (MOCKCHAIN era) -> prop)
-> Gen Property
forEachEpochTrace Proof era
proof Int
200 GenSize
genSize Trace (MOCKCHAIN era) -> Property
withTrace
  where
    withTrace :: Trace (MOCKCHAIN era) -> Property
    withTrace :: Trace (MOCKCHAIN era) -> Property
withTrace Trace (MOCKCHAIN era)
trc = forall t. TotalAda t => t -> Coin
totalAda (forall era. MockChainState era -> NewEpochState era
mcsNes State (MOCKCHAIN era)
trcInit) forall a. (Eq a, Show a) => a -> a -> Property
=== forall t. TotalAda t => t -> Coin
totalAda (forall era. MockChainState era -> NewEpochState era
mcsNes State (MOCKCHAIN era)
trcLast)
      where
        trcInit :: State (MOCKCHAIN era)
trcInit = forall s. Trace s -> State s
_traceInitState Trace (MOCKCHAIN era)
trc
        trcLast :: State (MOCKCHAIN era)
trcLast = forall s. Trace s -> State s
lastState Trace (MOCKCHAIN era)
trc

twiddleInvariantHolds ::
  forall a.
  ( Arbitrary a
  , Show a
  , Twiddle a
  ) =>
  String ->
  TestTree
twiddleInvariantHolds :: forall a. (Arbitrary a, Show a, Twiddle a) => [Char] -> TestTree
twiddleInvariantHolds [Char]
name =
  forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
name forall a b. (a -> b) -> a -> b
$ forall a. Twiddle a => Version -> a -> Gen Property
twiddleInvariantProp @a

twiddleInvariantHoldsEras :: TestTree
twiddleInvariantHoldsEras :: TestTree
twiddleInvariantHoldsEras =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Twiddle invariant holds for TxBody"
    [ forall a. (Arbitrary a, Show a, Twiddle a) => [Char] -> TestTree
twiddleInvariantHolds @(AlonzoTxBody AlonzoEra) [Char]
"Alonzo"
    , forall a. (Arbitrary a, Show a, Twiddle a) => [Char] -> TestTree
twiddleInvariantHolds @(BabbageTxBody BabbageEra) [Char]
"Babbage"
    ]

-- ==============================================================
-- Infrastrucure for running individual tests, with easy replay.
-- In ghci just type
-- :main --quickcheck-replay=205148

main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ Int -> GenSize -> TestTree
adaIsPreservedBabbage Int
100 (forall a. Default a => a
def {blocksizeMax :: Integer
blocksizeMax = Integer
4})

main8 :: IO ()
main8 :: IO ()
main8 = forall era. Int -> Proof era -> IO ()
test Int
100 Proof BabbageEra
Babbage

test :: Int -> Proof era -> IO ()
test :: forall era. Int -> Proof era -> IO ()
test Int
n Proof era
proof = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$
  case Proof era
proof of
    -- TODO
    -- Conway ->
    --  testPropMax 30 "Conway ValidTx preserves ADA" $
    --    withMaxSuccess n (forAll (genTxAndLEDGERState proof def) (testTxValidForLEDGER proof))
    Proof era
Babbage ->
      forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage ValidTx preserves ADA" forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof forall a. Default a => a
def) (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 PrettyA (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof era
proof))
    Proof era
Alonzo ->
      forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo ValidTx preserves ADA" forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof forall a. Default a => a
def) (forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 PrettyA (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof era
proof))
    Proof era
Shelley ->
      forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley ValidTx preserves ADA" forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (GenSize
-> Gen (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
genTxAndLEDGERStateShelley forall a. Default a => a
def) (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
-> Property
testTxValidForLEDGERShelley)
    Proof era
other -> forall a. HasCallStack => [Char] -> a
error ([Char]
"NO Test in era " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Proof era
other)

-- ===============================================================
-- Tools for generating other things from a GenEnv. This way one can
-- test individual functions in this file. These are intended for use
-- when developng and debugging.

-- | Construct a random (Gen b)
makeGen :: Reflect era => Proof era -> (Proof era -> GenRS era b) -> Gen b
makeGen :: forall era b.
Reflect era =>
Proof era -> (Proof era -> GenRS era b) -> Gen b
makeGen Proof era
proof Proof era -> GenRS era b
computeWith = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof era
proof forall a. Default a => a
def (Proof era -> GenRS era b
computeWith Proof era
proof)

runTest ::
  (Reflect era, PrettyA a) =>
  (Proof era -> GenRS era a) ->
  (a -> IO ()) ->
  Proof era ->
  IO ()
runTest :: forall era a.
(Reflect era, PrettyA a) =>
(Proof era -> GenRS era a) -> (a -> IO ()) -> Proof era -> IO ()
runTest Proof era -> GenRS era a
computeWith a -> IO ()
action Proof era
proof = do
  a
ans <- forall a. Gen a -> IO a
generate (forall era b.
Reflect era =>
Proof era -> (Proof era -> GenRS era b) -> Gen b
makeGen Proof era
proof Proof era -> GenRS era a
computeWith)
  forall a. Show a => a -> IO ()
print (forall t. PrettyA t => t -> PDoc
prettyA a
ans)
  a -> IO ()
action a
ans

main2 :: IO ()
main2 :: IO ()
main2 = forall era a.
(Reflect era, PrettyA a) =>
(Proof era -> GenRS era a) -> (a -> IO ()) -> Proof era -> IO ()
runTest (\Proof BabbageEra
x -> forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era.
Reflect era =>
Proof era -> SlotNo -> GenRS era (UTxO era, Tx era)
genAlonzoTx Proof BabbageEra
x (Word64 -> SlotNo
SlotNo Word64
0)) (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())) Proof BabbageEra
Babbage

main3 :: IO ()
main3 :: IO ()
main3 = forall era a.
(Reflect era, PrettyA a) =>
(Proof era -> GenRS era a) -> (a -> IO ()) -> Proof era -> IO ()
runTest (\Proof AlonzoEra
_x -> forall era. Map TxIn (TxOut era) -> UTxO era
UTxO 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 era.
Reflect era =>
GenRS era (MUtxo era, Maybe (UtxoEntry era))
genUTxO) forall {era}. UTxO era -> IO ()
action Proof AlonzoEra
Alonzo
  where
    action :: UTxO era -> IO ()
action (UTxO Map TxIn (TxOut era)
x) = [Char] -> IO ()
putStrLn ([Char]
"Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall k a. Map k a -> Int
Map.size Map TxIn (TxOut era)
x))