{-# 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 (Shelley)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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.Shelley), GenState S.Shelley)
genTxAndLEDGERStateShelley :: GenSize
-> Gen
     (TRC (EraRule "LEDGER" (ShelleyEra StandardCrypto)),
      GenState (ShelleyEra StandardCrypto))
genTxAndLEDGERStateShelley GenSize
genSize = do
  Box Proof (ShelleyEra StandardCrypto)
_ TRC (EraRule "LEDGER" (ShelleyEra StandardCrypto))
trc GenState (ShelleyEra StandardCrypto)
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 StandardCrypto)
Shelley GenSize
genSize
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TRC (EraRule "LEDGER" (ShelleyEra StandardCrypto))
trc, GenState (ShelleyEra StandardCrypto)
genState)

testTxValidForLEDGERShelley :: (TRC (EraRule "LEDGER" S.Shelley), GenState S.Shelley) -> Property
testTxValidForLEDGERShelley :: (TRC (EraRule "LEDGER" (ShelleyEra StandardCrypto)),
 GenState (ShelleyEra StandardCrypto))
-> Property
testTxValidForLEDGERShelley (TRC (EraRule "LEDGER" (ShelleyEra StandardCrypto))
trc, GenState (ShelleyEra StandardCrypto)
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 StandardCrypto)
Shelley (forall era.
Proof era -> TRC (EraRule "LEDGER" era) -> GenState era -> Box era
Box Proof (ShelleyEra StandardCrypto)
Shelley TRC (EraRule "LEDGER" (ShelleyEra StandardCrypto))
trc GenState (ShelleyEra StandardCrypto)
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 StandardCrypto) (TxOut era)
initial, Maybe (TxIn StandardCrypto, 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 (EraCrypto era)) (TxOut era)
mUTxO = Map (TxIn StandardCrypto) (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. Era 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.
Era 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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)),
      GenState (ShelleyEra StandardCrypto))
genTxAndLEDGERStateShelley GenSize
genSize) ((TRC (EraRule "LEDGER" (ShelleyEra StandardCrypto)),
 GenState (ShelleyEra StandardCrypto))
-> 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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
Alonzo Int
numTx GenSize
gensize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof (MaryEra StandardCrypto)
Mary Int
numTx GenSize
gensize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof (AllegraEra StandardCrypto)
Allegra Int
numTx GenSize
gensize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof (ShelleyEra StandardCrypto)
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 StandardCrypto)
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 (EraCrypto era)
istake Coin
_) -> IncrementalStake (EraCrypto era)
istake forall a. (Eq a, Show a) => a -> a -> Property
=== forall era.
EraTxOut era =>
PParams era
-> IncrementalStake (EraCrypto era)
-> UTxO era
-> UTxO era
-> IncrementalStake (EraCrypto era)
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 StandardCrypto)
Babbage GenSize
genSize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof (AlonzoEra StandardCrypto)
Alonzo GenSize
genSize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof (MaryEra StandardCrypto)
Mary GenSize
genSize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof (AllegraEra StandardCrypto)
Allegra GenSize
genSize
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof (ShelleyEra StandardCrypto)
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 StandardCrypto)
Babbage GenSize
genSize
    , forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof (AlonzoEra StandardCrypto)
Alonzo GenSize
genSize
    , forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof (MaryEra StandardCrypto)
Mary GenSize
genSize
    , forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof (AllegraEra StandardCrypto)
Allegra GenSize
genSize
    , forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof (ShelleyEra StandardCrypto)
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 StandardCrypto)) [Char]
"Alonzo"
    , forall a. (Arbitrary a, Show a, Twiddle a) => [Char] -> TestTree
twiddleInvariantHolds @(BabbageTxBody (BabbageEra StandardCrypto)) [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 StandardCrypto)
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 StandardCrypto)),
      GenState (ShelleyEra StandardCrypto))
genTxAndLEDGERStateShelley forall a. Default a => a
def) (TRC (EraRule "LEDGER" (ShelleyEra StandardCrypto)),
 GenState (ShelleyEra StandardCrypto))
-> 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 StandardCrypto)
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 StandardCrypto)
x (Word64 -> SlotNo
SlotNo Word64
0)) (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())) Proof (BabbageEra StandardCrypto)
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 StandardCrypto)
_x -> forall era. Map (TxIn (EraCrypto era)) (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 StandardCrypto)
Alonzo
  where
    action :: UTxO era -> IO ()
action (UTxO Map (TxIn (EraCrypto era)) (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 (EraCrypto era)) (TxOut era)
x))