{-# 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.Shelley.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.Binary.Twiddle ()
import Test.Cardano.Ledger.Babbage.Arbitrary ()
import Test.Cardano.Ledger.Babbage.Binary.Twiddle ()
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
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Era (EraTest)
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.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 (..))

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

genTxAndUTXOState ::
  ( Signal (EraRule "LEDGER" era) ~ Tx TopTx 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 TopTx era ~ Signal (EraRule "UTXOW" era)
  , EraGenericGen era
  ) =>
  GenSize -> Gen (TRC (EraRule "UTXOW" era), GenState era)
genTxAndUTXOState :: forall era.
(Signal (EraRule "LEDGER" era) ~ Tx TopTx 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 TopTx era ~ Signal (EraRule "UTXOW" era), EraGenericGen era) =>
GenSize -> Gen (TRC (EraRule "UTXOW" era), GenState era)
genTxAndUTXOState GenSize
gsize = do
  (TRC (LedgerEnv slotNo _ _ pp _, ledgerState, vtx), genState) <- GenSize -> Gen (TRC (EraRule "LEDGER" era), GenState era)
forall era.
(Signal (EraRule "LEDGER" era) ~ Tx TopTx 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
  pure (TRC (UtxoEnv slotNo pp def, lsUTxOState ledgerState, vtx), genState)

genTxAndLEDGERState ::
  forall era.
  ( Signal (EraRule "LEDGER" era) ~ Tx TopTx 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 TopTx 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 <- Gen TxIx
forall a. Arbitrary a => Gen a
arbitrary
  let genT = do
        (initial, _) <- 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
        modifyModel (\ModelNewEpochState era
m -> ModelNewEpochState era
m {mUTxO = initial})
        (_utxo, tx) <- genAlonzoTx slotNo
        model <- gets gsModel
        pp <- gets (gePParams . gsGenEnv)
        let ledgerState = forall t era. Extract t era => ModelNewEpochState era -> t
extract @(LedgerState era) ModelNewEpochState era
model
            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))
        pure $ TRC (ledgerEnv, ledgerState, tx)
  (trc, genstate) <- runGenRS sizes (initStableFields >> genT)
  pure (trc, genstate)

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

testTxValidForLEDGER ::
  forall era.
  ( Reflect era
  , Signal (EraRule "LEDGER" era) ~ Tx TopTx 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 TopTx 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 TopTx era -> IsValid
forall era. Proof era -> Tx TopTx era -> IsValid
isValid' (forall era. Reflect era => Proof era
reify @era) Tx TopTx 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 TopTx era -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr Tx TopTx 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 -> Spec
txPreserveAda :: GenSize -> Spec
txPreserveAda GenSize
genSize =
  [Char] -> Spec -> Spec
forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
describe [Char]
"Individual Tx's preserve Ada" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Int -> [Char] -> Property -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
testPropMax Int
30 [Char]
"Shelley Tx preserves Ada" (Property -> Spec) -> Property -> Spec
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 TopTx 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 TopTx 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 -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
testPropMax Int
30 [Char]
"Allegra Tx preserves ADA" (Property -> Spec) -> Property -> Spec
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 TopTx 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 TopTx 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 -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
testPropMax Int
30 [Char]
"Mary Tx preserves ADA" (Property -> Spec) -> Property -> Spec
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 TopTx 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 TopTx 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 -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
testPropMax Int
30 [Char]
"Alonzo ValidTx preserves ADA" (Property -> Spec) -> Property -> Spec
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 TopTx 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 TopTx 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 -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
testPropMax Int
30 [Char]
"Babbage ValidTx preserves ADA" (Property -> Spec) -> Property -> Spec
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 TopTx 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 TopTx 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
  , ShelleyEraAccounts era
  ) =>
  Int ->
  GenSize ->
  Spec
adaIsPreserved :: forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
adaIsPreserved Int
numTx GenSize
gensize =
  Int -> [Char] -> Gen Property -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
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 -> Spec) -> Gen Property -> Spec
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts 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 -> Spec
tracePreserveAda :: Int -> GenSize -> Spec
tracePreserveAda Int
numTx GenSize
gensize =
  [Char] -> Spec -> Spec
forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
describe ([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) (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
adaIsPreserved @BabbageEra Int
numTx GenSize
gensize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
adaIsPreserved @AlonzoEra Int
numTx GenSize
gensize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
adaIsPreserved @MaryEra Int
numTx GenSize
gensize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
adaIsPreserved @AllegraEra Int
numTx GenSize
gensize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
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
  , ShelleyEraAccounts era
  ) =>
  GenSize ->
  Spec
incrementStakeInvariant :: forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
GenSize -> Spec
incrementStakeInvariant GenSize
gensize =
  Int -> [Char] -> Gen Property -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
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 -> Spec) -> Gen Property -> Spec
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts 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 -> Spec
incrementalStake :: GenSize -> Spec
incrementalStake GenSize
genSize =
  [Char] -> Spec -> Spec
forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
describe [Char]
"Incremental Stake invariant holds" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    -- 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,
 ShelleyEraAccounts era) =>
GenSize -> Spec
incrementStakeInvariant @BabbageEra GenSize
genSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
GenSize -> Spec
incrementStakeInvariant @AlonzoEra GenSize
genSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
GenSize -> Spec
incrementStakeInvariant @MaryEra GenSize
genSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
GenSize -> Spec
incrementStakeInvariant @AllegraEra GenSize
genSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
GenSize -> Spec
incrementStakeInvariant @ShelleyEra GenSize
genSize

genericProperties :: GenSize -> Spec
genericProperties :: GenSize -> Spec
genericProperties GenSize
genSize =
  [Char] -> Spec -> Spec
forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
describe [Char]
"Generic Property tests" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    GenSize -> Spec
txPreserveAda GenSize
genSize
    Int -> GenSize -> Spec
tracePreserveAda Int
45 GenSize
genSize
    GenSize -> Spec
incrementalStake GenSize
genSize
    Int -> Spec
testTraces Int
45
    GenSize -> Spec
epochPreserveAda GenSize
genSize
    Spec
twiddleInvariantHoldsEras

epochPreserveAda :: GenSize -> Spec
epochPreserveAda :: GenSize -> Spec
epochPreserveAda GenSize
genSize =
  [Char] -> Spec -> Spec
forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
describe [Char]
"Ada is preserved in each epoch" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    forall era.
(ShelleyEraAccounts era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 State (EraRule "TICK" era) ~ NewEpochState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Environment (EraRule "TICK" era) ~ (),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 Signal (EraRule "TICK" era) ~ SlotNo,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx 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)),
 ToExpr (PredicateFailure (EraRule "LEDGER" era)),
 Eq (PredicateFailure (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
GenSize -> Spec
adaIsPreservedInEachEpoch @BabbageEra GenSize
genSize
    forall era.
(ShelleyEraAccounts era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 State (EraRule "TICK" era) ~ NewEpochState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Environment (EraRule "TICK" era) ~ (),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 Signal (EraRule "TICK" era) ~ SlotNo,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx 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)),
 ToExpr (PredicateFailure (EraRule "LEDGER" era)),
 Eq (PredicateFailure (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
GenSize -> Spec
adaIsPreservedInEachEpoch @AlonzoEra GenSize
genSize
    forall era.
(ShelleyEraAccounts era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 State (EraRule "TICK" era) ~ NewEpochState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Environment (EraRule "TICK" era) ~ (),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 Signal (EraRule "TICK" era) ~ SlotNo,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx 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)),
 ToExpr (PredicateFailure (EraRule "LEDGER" era)),
 Eq (PredicateFailure (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
GenSize -> Spec
adaIsPreservedInEachEpoch @MaryEra GenSize
genSize
    forall era.
(ShelleyEraAccounts era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 State (EraRule "TICK" era) ~ NewEpochState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Environment (EraRule "TICK" era) ~ (),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 Signal (EraRule "TICK" era) ~ SlotNo,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx 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)),
 ToExpr (PredicateFailure (EraRule "LEDGER" era)),
 Eq (PredicateFailure (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
GenSize -> Spec
adaIsPreservedInEachEpoch @AllegraEra GenSize
genSize
    forall era.
(ShelleyEraAccounts era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 State (EraRule "TICK" era) ~ NewEpochState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Environment (EraRule "TICK" era) ~ (),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 Signal (EraRule "TICK" era) ~ SlotNo,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx 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)),
 ToExpr (PredicateFailure (EraRule "LEDGER" era)),
 Eq (PredicateFailure (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
GenSize -> Spec
adaIsPreservedInEachEpoch @ShelleyEra GenSize
genSize

adaIsPreservedInEachEpoch ::
  forall era.
  ( ShelleyEraAccounts era
  , State (EraRule "NEWEPOCH" era) ~ NewEpochState era
  , State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate
  , State (EraRule "TICK" era) ~ NewEpochState era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , State (EraRule "LEDGERS" era) ~ LedgerState era
  , Environment (EraRule "NEWEPOCH" era) ~ ()
  , Environment (EraRule "RUPD" era) ~ RupdEnv era
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , Environment (EraRule "TICK" era) ~ ()
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , Signal (EraRule "NEWEPOCH" era) ~ EpochNo
  , Signal (EraRule "RUPD" era) ~ SlotNo
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era)
  , Signal (EraRule "TICK" era) ~ SlotNo
  , Signal (EraRule "LEDGER" era) ~ Tx TopTx 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))
  , ToExpr (PredicateFailure (EraRule "LEDGER" era))
  , Eq (PredicateFailure (EraRule "LEDGER" era))
  , Show (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  GenSize ->
  Spec
adaIsPreservedInEachEpoch :: forall era.
(ShelleyEraAccounts era,
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 State (EraRule "TICK" era) ~ NewEpochState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Environment (EraRule "TICK" era) ~ (),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 Signal (EraRule "TICK" era) ~ SlotNo,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx 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)),
 ToExpr (PredicateFailure (EraRule "LEDGER" era)),
 Eq (PredicateFailure (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
GenSize -> Spec
adaIsPreservedInEachEpoch GenSize
genSize =
  Int -> [Char] -> Gen Property -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
testPropMax Int
30 (forall era. Era era => [Char]
eraName @era) (Gen Property -> Spec) -> Gen Property -> Spec
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(Testable prop, HasTrace (MOCKCHAIN era) (Gen1 era),
 EraGenericGen era, ShelleyEraAccounts 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 ->
  Spec
twiddleInvariantHolds :: forall a. (Arbitrary a, Show a, Twiddle a) => [Char] -> Spec
twiddleInvariantHolds [Char]
name =
  Int -> [Char] -> (Version -> a -> Gen Property) -> Spec
forall prop. Testable prop => Int -> [Char] -> prop -> Spec
testPropMax Int
30 [Char]
name ((Version -> a -> Gen Property) -> Spec)
-> (Version -> a -> Gen Property) -> Spec
forall a b. (a -> b) -> a -> b
$ forall a. Twiddle a => Version -> a -> Gen Property
twiddleInvariantProp @a

twiddleInvariantHoldsEras :: Spec
twiddleInvariantHoldsEras :: Spec
twiddleInvariantHoldsEras =
  [Char] -> Spec -> Spec
forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
describe [Char]
"Twiddle invariant holds for TxBody" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    forall a. (Arbitrary a, Show a, Twiddle a) => [Char] -> Spec
twiddleInvariantHolds @(TxBody TopTx AlonzoEra) [Char]
"Alonzo"
    forall a. (Arbitrary a, Show a, Twiddle a) => [Char] -> Spec
twiddleInvariantHolds @(TxBody TopTx BabbageEra) [Char]
"Babbage"