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

module Test.Cardano.Ledger.Generic.Properties where

import Cardano.Ledger.Alonzo.Tx (IsValid (..))
import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Shelley.LedgerState (
  LedgerState (..),
  NewEpochState,
  PulsingRewUpdate,
  UTxOState,
 )
import Cardano.Ledger.Shelley.Rules (
  LedgerEnv (..),
  RupdEnv,
  ShelleyLedgersEnv,
  ShelleyTICK,
  UtxoEnv (..),
 )
import Cardano.Ledger.State
import Cardano.Slotting.Slot (EpochNo, 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 Data.Maybe.Strict (StrictMaybe)
import Data.Sequence (Seq)
import Lens.Micro
import Test.Cardano.Ledger.Alonzo.Era
import Test.Cardano.Ledger.Alonzo.Serialisation.Generators ()
import Test.Cardano.Ledger.Babbage.Arbitrary ()
import Test.Cardano.Ledger.Babbage.ImpTest ()
import Test.Cardano.Ledger.Binary.Arbitrary ()
import Test.Cardano.Ledger.Binary.Twiddle (Twiddle, twiddleInvariantProp)
import Test.Cardano.Ledger.Common (ToExpr (..), showExpr)
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Generic.Functions (TotalAda (totalAda), isValid')
import Test.Cardano.Ledger.Generic.GenState (
  EraGenericGen,
  GenEnv (..),
  GenSize (..),
  GenState (..),
  initStableFields,
  modifyModel,
  runGenRS,
 )
import Test.Cardano.Ledger.Generic.MockChain (MOCKCHAIN, MockChainState (..))
import Test.Cardano.Ledger.Generic.ModelState
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 (
  genAlonzoTx,
  genUTxO,
  runSTSWithContext,
 )
import Test.Cardano.Ledger.Shelley.ImpTest (ShelleyEraImp)
import Test.Cardano.Ledger.Shelley.Serialisation.EraIndepGenerators ()
import Test.Cardano.Ledger.Shelley.TreeDiff ()
import Test.Control.State.Transition.Trace (Trace (..), lastState)
import Test.Control.State.Transition.Trace.Generator.QuickCheck (HasTrace (..))
import Test.QuickCheck
import Test.Tasty (TestTree, testGroup)

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

genTxAndUTXOState ::
  ( Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Tx era ~ Signal (EraRule "UTXOW" era)
  , EraGenericGen era
  ) =>
  GenSize -> Gen (TRC (EraRule "UTXOW" era), GenState era)
genTxAndUTXOState :: forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Tx era ~ Signal (EraRule "UTXOW" era), EraGenericGen era) =>
GenSize -> Gen (TRC (EraRule "UTXOW" era), GenState era)
genTxAndUTXOState GenSize
gsize = do
  (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams era
pp ChainAccountState
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx), GenState era
genState) <- GenSize -> Gen (TRC (EraRule "LEDGER" era), GenState era)
forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 EraGenericGen era) =>
GenSize -> Gen (TRC (EraRule "LEDGER" era), GenState era)
genTxAndLEDGERState GenSize
gsize
  (TRC (EraRule "UTXOW" era), GenState era)
-> Gen (TRC (EraRule "UTXOW" era), GenState era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Environment (EraRule "UTXOW" era), State (EraRule "UTXOW" era),
 Signal (EraRule "UTXOW" era))
-> TRC (EraRule "UTXOW" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> PParams era -> CertState era -> UtxoEnv era
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams era
pp CertState era
forall a. Default a => a
def, LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
LedgerState era
ledgerState, Signal (EraRule "UTXOW" era)
Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)

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

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

testTxValidForLEDGER ::
  forall era.
  ( Reflect era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , ToExpr (PredicateFailure (EraRule "LEDGER" era))
  , EraTest era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , STS (EraRule "LEDGER" era)
  , ToExpr (Environment (EraRule "LEDGER" era))
  ) =>
  (TRC (EraRule "LEDGER" era), GenState era) ->
  Property
testTxValidForLEDGER :: forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 ToExpr (PredicateFailure (EraRule "LEDGER" era)), EraTest era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era),
 ToExpr (Environment (EraRule "LEDGER" era))) =>
(TRC (EraRule "LEDGER" era), GenState era) -> Property
testTxValidForLEDGER (trc :: TRC (EraRule "LEDGER" era)
trc@(TRC (Environment (EraRule "LEDGER" era)
env, 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.
(BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era)) =>
RuleContext 'Transition (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era))
runSTSWithContext @era RuleContext 'Transition (EraRule "LEDGER" era)
TRC (EraRule "LEDGER" era)
trc of
    Right State (EraRule "LEDGER" era)
ledgerState' ->
      -- UTxOState and CertState after applying the transaction $$$
      Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
classify (IsValid -> Bool
forall a b. Coercible a b => a -> b
coerce (Proof era -> Tx era -> IsValid
forall era. Proof era -> Tx era -> IsValid
isValid' (forall era. Reflect era => Proof era
reify @era) Tx era
Signal (EraRule "LEDGER" era)
vtx)) [Char]
"TxValid" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        LedgerState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda State (EraRule "LEDGER" era)
LedgerState era
ledgerState' Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LedgerState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda State (EraRule "LEDGER" era)
LedgerState era
ledgerState
    Left NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs ->
      [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample
        ( Environment (EraRule "LEDGER" era) -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr Environment (EraRule "LEDGER" era)
env
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LedgerState era -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr State (EraRule "LEDGER" era)
LedgerState era
ledgerState
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Tx era -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr Tx era
Signal (EraRule "LEDGER" era)
vtx
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ NonEmpty (PredicateFailure (EraRule "LEDGER" era)) -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs
        )
        (Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False)

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

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

-- | A single Tx preserves Ada
txPreserveAda :: GenSize -> TestTree
txPreserveAda :: GenSize -> TestTree
txPreserveAda GenSize
genSize =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Individual Tx's preserve Ada"
    [ Int -> [Char] -> Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley Tx preserves Ada" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Gen (TRC (ShelleyLEDGER ShelleyEra), GenState ShelleyEra)
-> ((TRC (ShelleyLEDGER ShelleyEra), GenState ShelleyEra)
    -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 EraGenericGen era) =>
GenSize -> Gen (TRC (EraRule "LEDGER" era), GenState era)
genTxAndLEDGERState @ShelleyEra GenSize
genSize) (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
-> Property
(TRC (ShelleyLEDGER ShelleyEra), GenState ShelleyEra) -> Property
forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 ToExpr (PredicateFailure (EraRule "LEDGER" era)), EraTest era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era),
 ToExpr (Environment (EraRule "LEDGER" era))) =>
(TRC (EraRule "LEDGER" era), GenState era) -> Property
testTxValidForLEDGER
    , Int -> [Char] -> Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra Tx preserves ADA" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Gen (TRC (ShelleyLEDGER AllegraEra), GenState AllegraEra)
-> ((TRC (ShelleyLEDGER AllegraEra), GenState AllegraEra)
    -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 EraGenericGen era) =>
GenSize -> Gen (TRC (EraRule "LEDGER" era), GenState era)
genTxAndLEDGERState @AllegraEra GenSize
genSize) (TRC (EraRule "LEDGER" AllegraEra), GenState AllegraEra)
-> Property
(TRC (ShelleyLEDGER AllegraEra), GenState AllegraEra) -> Property
forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 ToExpr (PredicateFailure (EraRule "LEDGER" era)), EraTest era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era),
 ToExpr (Environment (EraRule "LEDGER" era))) =>
(TRC (EraRule "LEDGER" era), GenState era) -> Property
testTxValidForLEDGER
    , Int -> [Char] -> Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary Tx preserves ADA" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Gen (TRC (ShelleyLEDGER MaryEra), GenState MaryEra)
-> ((TRC (ShelleyLEDGER MaryEra), GenState MaryEra) -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 EraGenericGen era) =>
GenSize -> Gen (TRC (EraRule "LEDGER" era), GenState era)
genTxAndLEDGERState @MaryEra GenSize
genSize) (TRC (EraRule "LEDGER" MaryEra), GenState MaryEra) -> Property
(TRC (ShelleyLEDGER MaryEra), GenState MaryEra) -> Property
forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 ToExpr (PredicateFailure (EraRule "LEDGER" era)), EraTest era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era),
 ToExpr (Environment (EraRule "LEDGER" era))) =>
(TRC (EraRule "LEDGER" era), GenState era) -> Property
testTxValidForLEDGER
    , Int -> [Char] -> Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo ValidTx preserves ADA" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Gen (TRC (AlonzoLEDGER AlonzoEra), GenState AlonzoEra)
-> ((TRC (AlonzoLEDGER AlonzoEra), GenState AlonzoEra) -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 EraGenericGen era) =>
GenSize -> Gen (TRC (EraRule "LEDGER" era), GenState era)
genTxAndLEDGERState @AlonzoEra GenSize
genSize) (TRC (EraRule "LEDGER" AlonzoEra), GenState AlonzoEra) -> Property
(TRC (AlonzoLEDGER AlonzoEra), GenState AlonzoEra) -> Property
forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 ToExpr (PredicateFailure (EraRule "LEDGER" era)), EraTest era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era),
 ToExpr (Environment (EraRule "LEDGER" era))) =>
(TRC (EraRule "LEDGER" era), GenState era) -> Property
testTxValidForLEDGER
    , Int -> [Char] -> Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage ValidTx preserves ADA" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Gen (TRC (BabbageLEDGER BabbageEra), GenState BabbageEra)
-> ((TRC (BabbageLEDGER BabbageEra), GenState BabbageEra)
    -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 EraGenericGen era) =>
GenSize -> Gen (TRC (EraRule "LEDGER" era), GenState era)
genTxAndLEDGERState @BabbageEra GenSize
genSize) (TRC (EraRule "LEDGER" BabbageEra), GenState BabbageEra)
-> Property
(TRC (BabbageLEDGER BabbageEra), GenState BabbageEra) -> Property
forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 ToExpr (PredicateFailure (EraRule "LEDGER" era)), EraTest era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era),
 ToExpr (Environment (EraRule "LEDGER" era))) =>
(TRC (EraRule "LEDGER" era), GenState era) -> Property
testTxValidForLEDGER
    ]

-- | Ada is preserved over a trace of length 100
adaIsPreserved ::
  forall era.
  ( HasTrace (MOCKCHAIN era) (Gen1 era)
  , EraGenericGen era
  ) =>
  Int ->
  GenSize ->
  TestTree
adaIsPreserved :: forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
Int -> GenSize -> TestTree
adaIsPreserved Int
numTx GenSize
gensize =
  Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (forall era. Era era => [Char]
eraName @era [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" era. Trace length = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
numTx) (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
Int
-> GenSize
-> (MockChainState era -> MockChainState era -> prop)
-> Gen prop
traceProp @era
      Int
numTx
      GenSize
gensize
      (\MockChainState era
firstSt MockChainState era
lastSt -> NewEpochState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda (MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
firstSt) Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== NewEpochState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda (MockChainState era -> NewEpochState era
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
numTx)
    [ forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
Int -> GenSize -> TestTree
adaIsPreserved @BabbageEra Int
numTx GenSize
gensize
    , forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
Int -> GenSize -> TestTree
adaIsPreserved @AlonzoEra Int
numTx GenSize
gensize
    , forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
Int -> GenSize -> TestTree
adaIsPreserved @MaryEra Int
numTx GenSize
gensize
    , forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
Int -> GenSize -> TestTree
adaIsPreserved @AllegraEra Int
numTx GenSize
gensize
    , forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
Int -> GenSize -> TestTree
adaIsPreserved @ShelleyEra Int
numTx GenSize
gensize
    ]

-- | The incremental Stake invaraint is preserved over a trace of length 100=
stakeInvariant :: EraStake era => MockChainState era -> MockChainState era -> Property
stakeInvariant :: forall era.
EraStake era =>
MockChainState era -> MockChainState era -> Property
stakeInvariant (MockChainState {}) (MockChainState NewEpochState era
nes NewEpochState era
_ SlotNo
_ Int
_) =
  let utxo :: UTxO era
utxo = NewEpochState era
nes NewEpochState era
-> Getting (UTxO era) (NewEpochState era) (UTxO era) -> UTxO era
forall s a. s -> Getting a s a -> a
^. Getting (UTxO era) (NewEpochState era) (UTxO era)
forall era. Lens' (NewEpochState era) (UTxO era)
forall (t :: * -> *) era. CanSetUTxO t => Lens' (t era) (UTxO era)
utxoL
   in NewEpochState era
nes NewEpochState era
-> Getting
     (InstantStake era) (NewEpochState era) (InstantStake era)
-> InstantStake era
forall s a. s -> Getting a s a -> a
^. Getting (InstantStake era) (NewEpochState era) (InstantStake era)
forall era. Lens' (NewEpochState era) (InstantStake era)
forall (t :: * -> *) era.
CanSetInstantStake t =>
Lens' (t era) (InstantStake era)
instantStakeL InstantStake era -> InstantStake era -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== UTxO era -> InstantStake era -> InstantStake era
forall era.
EraStake era =>
UTxO era -> InstantStake era -> InstantStake era
addInstantStake UTxO era
utxo InstantStake era
forall a. Monoid a => a
mempty

incrementStakeInvariant ::
  forall era.
  ( HasTrace (MOCKCHAIN era) (Gen1 era)
  , EraGenericGen era
  ) =>
  GenSize ->
  TestTree
incrementStakeInvariant :: forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
GenSize -> TestTree
incrementStakeInvariant GenSize
gensize =
  Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (forall era. Era era => [Char]
eraName @era [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" era. Trace length = 100") (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
Int
-> GenSize
-> (MockChainState era -> MockChainState era -> prop)
-> Gen prop
traceProp @era Int
100 GenSize
gensize MockChainState era -> MockChainState era -> Property
forall era.
EraStake 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.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
GenSize -> TestTree
incrementStakeInvariant @BabbageEra GenSize
genSize
    , forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
GenSize -> TestTree
incrementStakeInvariant @AlonzoEra GenSize
genSize
    , forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
GenSize -> TestTree
incrementStakeInvariant @MaryEra GenSize
genSize
    , forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
GenSize -> TestTree
incrementStakeInvariant @AllegraEra GenSize
genSize
    , forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era) =>
GenSize -> TestTree
incrementStakeInvariant @ShelleyEra GenSize
genSize
    ]

genericProperties :: GenSize -> TestTree
genericProperties :: GenSize -> TestTree
genericProperties GenSize
genSize =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Generic Property tests"
    [ 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.
(ShelleyEraImp era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era),
 BaseM (EraRule "NEWEPOCH" era) ~ ShelleyBase,
 Embed (EraRule "TICK" era) (MOCKCHAIN era),
 Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 Embed (EraRule "LEDGERS" era) (MOCKCHAIN era), EraGenericGen era,
 ToExpr (PredicateFailure (EraRule "NEWEPOCH" era)),
 ToExpr (PredicateFailure (EraRule "RUPD" era))) =>
GenSize -> TestTree
adaIsPreservedInEachEpoch @BabbageEra GenSize
genSize
    , forall era.
(ShelleyEraImp era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era),
 BaseM (EraRule "NEWEPOCH" era) ~ ShelleyBase,
 Embed (EraRule "TICK" era) (MOCKCHAIN era),
 Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 Embed (EraRule "LEDGERS" era) (MOCKCHAIN era), EraGenericGen era,
 ToExpr (PredicateFailure (EraRule "NEWEPOCH" era)),
 ToExpr (PredicateFailure (EraRule "RUPD" era))) =>
GenSize -> TestTree
adaIsPreservedInEachEpoch @AlonzoEra GenSize
genSize
    , forall era.
(ShelleyEraImp era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era),
 BaseM (EraRule "NEWEPOCH" era) ~ ShelleyBase,
 Embed (EraRule "TICK" era) (MOCKCHAIN era),
 Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 Embed (EraRule "LEDGERS" era) (MOCKCHAIN era), EraGenericGen era,
 ToExpr (PredicateFailure (EraRule "NEWEPOCH" era)),
 ToExpr (PredicateFailure (EraRule "RUPD" era))) =>
GenSize -> TestTree
adaIsPreservedInEachEpoch @MaryEra GenSize
genSize
    , forall era.
(ShelleyEraImp era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era),
 BaseM (EraRule "NEWEPOCH" era) ~ ShelleyBase,
 Embed (EraRule "TICK" era) (MOCKCHAIN era),
 Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 Embed (EraRule "LEDGERS" era) (MOCKCHAIN era), EraGenericGen era,
 ToExpr (PredicateFailure (EraRule "NEWEPOCH" era)),
 ToExpr (PredicateFailure (EraRule "RUPD" era))) =>
GenSize -> TestTree
adaIsPreservedInEachEpoch @AllegraEra GenSize
genSize
    , forall era.
(ShelleyEraImp era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era),
 BaseM (EraRule "NEWEPOCH" era) ~ ShelleyBase,
 Embed (EraRule "TICK" era) (MOCKCHAIN era),
 Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 Embed (EraRule "LEDGERS" era) (MOCKCHAIN era), EraGenericGen era,
 ToExpr (PredicateFailure (EraRule "NEWEPOCH" era)),
 ToExpr (PredicateFailure (EraRule "RUPD" era))) =>
GenSize -> TestTree
adaIsPreservedInEachEpoch @ShelleyEra GenSize
genSize
    ]

adaIsPreservedInEachEpoch ::
  forall era.
  ( ShelleyEraImp era
  , State (EraRule "NEWEPOCH" era) ~ NewEpochState era
  , State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate
  , Environment (EraRule "NEWEPOCH" era) ~ ()
  , Environment (EraRule "RUPD" era) ~ RupdEnv era
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , Signal (EraRule "NEWEPOCH" era) ~ EpochNo
  , Signal (EraRule "RUPD" era) ~ SlotNo
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx era)
  , BaseM (EraRule "NEWEPOCH" era) ~ ShelleyBase
  , Embed (EraRule "TICK" era) (MOCKCHAIN era)
  , Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era)
  , Embed (EraRule "RUPD" era) (ShelleyTICK era)
  , Embed (EraRule "LEDGERS" era) (MOCKCHAIN era)
  , EraGenericGen era
  , ToExpr (PredicateFailure (EraRule "NEWEPOCH" era))
  , ToExpr (PredicateFailure (EraRule "RUPD" era))
  ) =>
  GenSize ->
  TestTree
adaIsPreservedInEachEpoch :: forall era.
(ShelleyEraImp era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era),
 BaseM (EraRule "NEWEPOCH" era) ~ ShelleyBase,
 Embed (EraRule "TICK" era) (MOCKCHAIN era),
 Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 Embed (EraRule "LEDGERS" era) (MOCKCHAIN era), EraGenericGen era,
 ToExpr (PredicateFailure (EraRule "NEWEPOCH" era)),
 ToExpr (PredicateFailure (EraRule "RUPD" era))) =>
GenSize -> TestTree
adaIsPreservedInEachEpoch GenSize
genSize =
  Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (forall era. Era era => [Char]
eraName @era) (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(Testable prop, HasTrace (MOCKCHAIN era) (Gen1 era),
 EraGenericGen era) =>
Int -> GenSize -> (Trace (MOCKCHAIN era) -> prop) -> Gen Property
forEachEpochTrace @era 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 = NewEpochState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda (MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes State (MOCKCHAIN era)
MockChainState era
trcInit) Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== NewEpochState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda (MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes State (MOCKCHAIN era)
MockChainState era
trcLast)
      where
        trcInit :: State (MOCKCHAIN era)
trcInit = Trace (MOCKCHAIN era) -> State (MOCKCHAIN era)
forall s. Trace s -> State s
_traceInitState Trace (MOCKCHAIN era)
trc
        trcLast :: State (MOCKCHAIN era)
trcLast = Trace (MOCKCHAIN era) -> State (MOCKCHAIN era)
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 =
  Int -> [Char] -> (Version -> a -> Gen Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
name ((Version -> a -> Gen Property) -> TestTree)
-> (Version -> a -> Gen Property) -> TestTree
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 @(TxBody AlonzoEra) [Char]
"Alonzo"
    , forall a. (Arbitrary a, Show a, Twiddle a) => [Char] -> TestTree
twiddleInvariantHolds @(TxBody BabbageEra) [Char]
"Babbage"
    ]