{-# 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 (IsValid (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core
import qualified Cardano.Ledger.Shelley as S (ShelleyEra)
import Cardano.Ledger.Shelley.LedgerState (LedgerState (..))
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..), UtxoEnv (..))
import Cardano.Ledger.State
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 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.Binary.Arbitrary ()
import Test.Cardano.Ledger.Binary.Twiddle (Twiddle, twiddleInvariantProp)
import Test.Cardano.Ledger.Common (ToExpr (..))
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Generic.Fields (
  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.Proof hiding (lift)
import Test.Cardano.Ledger.Generic.Trace (
  Gen1,
  forEachEpochTrace,
  testPropMax,
  testTraces,
  traceProp,
 )
import Test.Cardano.Ledger.Generic.TxGen (
  Box (..),
  applySTSByProof,
  assembleWits,
  coreTxBody,
  coreTxOut,
  genAlonzoTx,
  genUTxO,
 )
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, defaultMain, testGroup)

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

genTxAndUTXOState ::
  Reflect era => Proof era -> GenSize -> Gen (TRC (EraRule "UTXOW" era), GenState era)
genTxAndUTXOState :: forall era.
Reflect era =>
Proof era
-> GenSize -> Gen (TRC (EraRule "UTXOW" era), GenState era)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Conway GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams ConwayEra
pp ChainAccountState
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    Proof era -> GenSize -> Gen (Box era)
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
  (TRC (ConwayUTXOW ConwayEra), GenState era)
-> Gen (TRC (ConwayUTXOW ConwayEra), GenState era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Environment (ConwayUTXOW ConwayEra),
 State (ConwayUTXOW ConwayEra), Signal (ConwayUTXOW ConwayEra))
-> TRC (ConwayUTXOW ConwayEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> PParams ConwayEra -> CertState ConwayEra -> UtxoEnv ConwayEra
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams ConwayEra
pp CertState ConwayEra
ConwayCertState ConwayEra
forall a. Default a => a
def, LedgerState ConwayEra -> UTxOState ConwayEra
forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
LedgerState ConwayEra
ledgerState, Signal (EraRule "LEDGER" era)
Signal (ConwayUTXOW ConwayEra)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Babbage GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams BabbageEra
pp ChainAccountState
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    Proof era -> GenSize -> Gen (Box era)
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
  (TRC (BabbageUTXOW BabbageEra), GenState era)
-> Gen (TRC (BabbageUTXOW BabbageEra), GenState era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Environment (BabbageUTXOW BabbageEra),
 State (BabbageUTXOW BabbageEra), Signal (BabbageUTXOW BabbageEra))
-> TRC (BabbageUTXOW BabbageEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> PParams BabbageEra -> CertState BabbageEra -> UtxoEnv BabbageEra
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams BabbageEra
pp CertState BabbageEra
ShelleyCertState BabbageEra
forall a. Default a => a
def, LedgerState BabbageEra -> UTxOState BabbageEra
forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
LedgerState BabbageEra
ledgerState, Signal (EraRule "LEDGER" era)
Signal (BabbageUTXOW BabbageEra)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Alonzo GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams AlonzoEra
pp ChainAccountState
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    Proof era -> GenSize -> Gen (Box era)
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
  (TRC (AlonzoUTXOW AlonzoEra), GenState era)
-> Gen (TRC (AlonzoUTXOW AlonzoEra), GenState era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Environment (AlonzoUTXOW AlonzoEra),
 State (AlonzoUTXOW AlonzoEra), Signal (AlonzoUTXOW AlonzoEra))
-> TRC (AlonzoUTXOW AlonzoEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> PParams AlonzoEra -> CertState AlonzoEra -> UtxoEnv AlonzoEra
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams AlonzoEra
pp CertState AlonzoEra
ShelleyCertState AlonzoEra
forall a. Default a => a
def, LedgerState AlonzoEra -> UTxOState AlonzoEra
forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
LedgerState AlonzoEra
ledgerState, Signal (EraRule "LEDGER" era)
Signal (AlonzoUTXOW AlonzoEra)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Mary GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams MaryEra
pp ChainAccountState
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    Proof era -> GenSize -> Gen (Box era)
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
  (TRC (AllegraUTXOW MaryEra), GenState era)
-> Gen (TRC (AllegraUTXOW MaryEra), GenState era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Environment (AllegraUTXOW MaryEra), State (AllegraUTXOW MaryEra),
 Signal (AllegraUTXOW MaryEra))
-> TRC (AllegraUTXOW MaryEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> PParams MaryEra -> CertState MaryEra -> UtxoEnv MaryEra
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams MaryEra
pp CertState MaryEra
ShelleyCertState MaryEra
forall a. Default a => a
def, LedgerState MaryEra -> UTxOState MaryEra
forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
LedgerState MaryEra
ledgerState, Signal (AllegraUTXOW MaryEra)
Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Allegra GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams AllegraEra
pp ChainAccountState
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    Proof era -> GenSize -> Gen (Box era)
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
  (TRC (AllegraUTXOW AllegraEra), GenState era)
-> Gen (TRC (AllegraUTXOW AllegraEra), GenState era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Environment (AllegraUTXOW AllegraEra),
 State (AllegraUTXOW AllegraEra), Signal (AllegraUTXOW AllegraEra))
-> TRC (AllegraUTXOW AllegraEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> PParams AllegraEra -> CertState AllegraEra -> UtxoEnv AllegraEra
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams AllegraEra
pp CertState AllegraEra
ShelleyCertState AllegraEra
forall a. Default a => a
def, LedgerState AllegraEra -> UTxOState AllegraEra
forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
LedgerState AllegraEra
ledgerState, Signal (AllegraUTXOW AllegraEra)
Signal (EraRule "LEDGER" era)
vtx), GenState era
genState)
genTxAndUTXOState proof :: Proof era
proof@Proof era
Shelley GenSize
gsize = do
  (Box Proof era
_ (TRC (LedgerEnv SlotNo
slotNo Maybe EpochNo
_ TxIx
_ PParams ShelleyEra
pp ChainAccountState
_, State (EraRule "LEDGER" era)
ledgerState, Signal (EraRule "LEDGER" era)
vtx)) GenState era
genState) <-
    Proof era -> GenSize -> Gen (Box era)
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
  (TRC (ShelleyUTXOW ShelleyEra), GenState era)
-> Gen (TRC (ShelleyUTXOW ShelleyEra), GenState era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Environment (ShelleyUTXOW ShelleyEra),
 State (ShelleyUTXOW ShelleyEra), Signal (ShelleyUTXOW ShelleyEra))
-> TRC (ShelleyUTXOW ShelleyEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> PParams ShelleyEra -> CertState ShelleyEra -> UtxoEnv ShelleyEra
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slotNo PParams ShelleyEra
pp CertState ShelleyEra
ShelleyCertState ShelleyEra
forall a. Default a => a
def, LedgerState ShelleyEra -> UTxOState ShelleyEra
forall era. LedgerState era -> UTxOState era
lsUTxOState State (EraRule "LEDGER" era)
LedgerState ShelleyEra
ledgerState, Signal (EraRule "LEDGER" era)
Signal (ShelleyUTXOW ShelleyEra)
vtx), GenState era
genState)

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

testTxValidForLEDGERShelley ::
  (TRC (EraRule "LEDGER" S.ShelleyEra), GenState S.ShelleyEra) -> Property
testTxValidForLEDGERShelley :: (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
-> Property
testTxValidForLEDGERShelley (TRC (EraRule "LEDGER" ShelleyEra)
trc, GenState ShelleyEra
genState) =
  Proof ShelleyEra -> Box 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) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof ShelleyEra
Shelley (Proof ShelleyEra
-> TRC (EraRule "LEDGER" ShelleyEra)
-> GenState ShelleyEra
-> Box ShelleyEra
forall era.
Proof era -> TRC (EraRule "LEDGER" era) -> GenState era -> Box era
Box Proof ShelleyEra
Shelley TRC (EraRule "LEDGER" ShelleyEra)
trc GenState ShelleyEra
genState)

genTxAndLEDGERState ::
  forall era.
  ( Reflect era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  ) =>
  Proof era ->
  GenSize ->
  Gen (Box era)
genTxAndLEDGERState :: forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era) =>
Proof era -> GenSize -> Gen (Box era)
genTxAndLEDGERState Proof era
proof GenSize
sizes = do
  let slotNo :: SlotNo
slotNo = Word64 -> SlotNo
SlotNo (GenSize -> Word64
startSlot GenSize
sizes)
  TxIx
txIx <- 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.
Reflect 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) <- Proof era
-> SlotNo
-> RWST (GenEnv era) () (GenState era) Gen (UTxO era, Tx era)
forall era.
Reflect era =>
Proof era -> SlotNo -> GenRS era (UTxO era, Tx era)
genAlonzoTx Proof era
proof 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) <- Proof era
-> GenSize
-> RWST
     (GenEnv era) () (GenState era) Gen (TRC (EraRule "LEDGER" era))
-> Gen (TRC (EraRule "LEDGER" era), GenState era)
forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof era
proof 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)
  Box era -> Gen (Box era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof era -> TRC (EraRule "LEDGER" era) -> GenState era -> Box era
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
  , ToExpr (PredicateFailure (EraRule "LEDGER" era))
  , EraTest era
  ) =>
  Proof era ->
  Box 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) =>
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 Proof era
-> RuleContext 'Transition (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era))
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 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' Proof era
proof 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
        ( Expr -> [Char]
forall a. Show a => a -> [Char]
show (LedgerState era -> Expr
forall a. ToExpr a => a -> Expr
toExpr 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]
++ Expr -> [Char]
forall a. Show a => a -> [Char]
show (Tx era -> Expr
forall a. ToExpr a => a -> Expr
toExpr 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]
++ Expr -> [Char]
forall a. Show a => a -> [Char]
show (NonEmpty (PredicateFailure (EraRule "LEDGER" era)) -> Expr
forall a. ToExpr a => a -> Expr
toExpr 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

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 = Proof era -> [TxOutField era] -> TxOut era
forall era. Proof era -> [TxOutField era] -> TxOut era
coreTxOut Proof era
proof (Proof era -> TxOut era -> [TxOutField era]
forall era. Era era => Proof era -> TxOut era -> [TxOutField era]
abstractTxOut Proof era
proof TxOut era
x) TxOut era -> TxOut era -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TxOut 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 = Proof era -> [TxBodyField era] -> TxBody era
forall era.
EraTxBody era =>
Proof era -> [TxBodyField era] -> TxBody era
coreTxBody Proof era
proof (Proof era -> TxBody era -> [TxBodyField era]
forall era. Proof era -> TxBody era -> [TxBodyField era]
abstractTxBody Proof era
proof TxBody era
x) TxBody era -> TxBody era -> Property
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 = Proof era -> [WitnessesField era] -> TxWits era
forall era. Proof era -> [WitnessesField era] -> TxWits era
assembleWits Proof era
proof (Proof era -> TxWits era -> [WitnessesField era]
forall era. Proof era -> TxWits era -> [WitnessesField era]
abstractWitnesses Proof era
proof TxWits era
x) TxWits era -> TxWits era -> Property
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"
        [ Int -> [Char] -> (AlonzoTxWits BabbageEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage era" ((AlonzoTxWits BabbageEra -> Property) -> TestTree)
-> (AlonzoTxWits BabbageEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof BabbageEra -> TxWits BabbageEra -> Property
forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof BabbageEra
Babbage
        , Int -> [Char] -> (AlonzoTxWits AlonzoEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo era" ((AlonzoTxWits AlonzoEra -> Property) -> TestTree)
-> (AlonzoTxWits AlonzoEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof AlonzoEra -> TxWits AlonzoEra -> Property
forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof AlonzoEra
Alonzo
        , Int -> [Char] -> (ShelleyTxWits MaryEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary era" ((ShelleyTxWits MaryEra -> Property) -> TestTree)
-> (ShelleyTxWits MaryEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof MaryEra -> TxWits MaryEra -> Property
forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof MaryEra
Mary
        , Int -> [Char] -> (ShelleyTxWits AllegraEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra era" ((ShelleyTxWits AllegraEra -> Property) -> TestTree)
-> (ShelleyTxWits AllegraEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof AllegraEra -> TxWits AllegraEra -> Property
forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof AllegraEra
Allegra
        , Int -> [Char] -> (ShelleyTxWits ShelleyEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley era" ((ShelleyTxWits ShelleyEra -> Property) -> TestTree)
-> (ShelleyTxWits ShelleyEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof ShelleyEra -> TxWits ShelleyEra -> Property
forall era. EraTxWits era => Proof era -> TxWits era -> Property
txWitRoundTrip Proof ShelleyEra
Shelley
        ]
    , [Char] -> [TestTree] -> TestTree
testGroup
        [Char]
"TxBody roundtrips"
        [ Int -> [Char] -> (TxBody BabbageEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage era" ((TxBody BabbageEra -> Property) -> TestTree)
-> (TxBody BabbageEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof BabbageEra -> TxBody BabbageEra -> Property
forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof BabbageEra
Babbage
        , Int -> [Char] -> (TxBody AlonzoEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo era" ((TxBody AlonzoEra -> Property) -> TestTree)
-> (TxBody AlonzoEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof AlonzoEra -> TxBody AlonzoEra -> Property
forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof AlonzoEra
Alonzo
        , Int -> [Char] -> (TxBody MaryEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary era" ((TxBody MaryEra -> Property) -> TestTree)
-> (TxBody MaryEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof MaryEra -> TxBody MaryEra -> Property
forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof MaryEra
Mary
        , Int -> [Char] -> (TxBody AllegraEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra era" ((TxBody AllegraEra -> Property) -> TestTree)
-> (TxBody AllegraEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof AllegraEra -> TxBody AllegraEra -> Property
forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof AllegraEra
Allegra
        , Int -> [Char] -> (TxBody ShelleyEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley era" ((TxBody ShelleyEra -> Property) -> TestTree)
-> (TxBody ShelleyEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof ShelleyEra -> TxBody ShelleyEra -> Property
forall era. EraTxBody era => Proof era -> TxBody era -> Property
txBodyRoundTrip Proof ShelleyEra
Shelley
        ]
    , [Char] -> [TestTree] -> TestTree
testGroup
        [Char]
"TxOut roundtrips"
        [ Int -> [Char] -> (BabbageTxOut BabbageEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Babbage era" ((BabbageTxOut BabbageEra -> Property) -> TestTree)
-> (BabbageTxOut BabbageEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof BabbageEra -> TxOut BabbageEra -> Property
forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof BabbageEra
Babbage
        , Int -> [Char] -> (AlonzoTxOut AlonzoEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Alonzo era" ((AlonzoTxOut AlonzoEra -> Property) -> TestTree)
-> (AlonzoTxOut AlonzoEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof AlonzoEra -> TxOut AlonzoEra -> Property
forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof AlonzoEra
Alonzo
        , Int -> [Char] -> (ShelleyTxOut MaryEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Mary era" ((ShelleyTxOut MaryEra -> Property) -> TestTree)
-> (ShelleyTxOut MaryEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof MaryEra -> TxOut MaryEra -> Property
forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof MaryEra
Mary
        , Int -> [Char] -> (ShelleyTxOut AllegraEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Allegra era" ((ShelleyTxOut AllegraEra -> Property) -> TestTree)
-> (ShelleyTxOut AllegraEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof AllegraEra -> TxOut AllegraEra -> Property
forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof AllegraEra
Allegra
        , Int -> [Char] -> (ShelleyTxOut ShelleyEra -> Property) -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley era" ((ShelleyTxOut ShelleyEra -> Property) -> TestTree)
-> (ShelleyTxOut ShelleyEra -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Proof ShelleyEra -> TxOut ShelleyEra -> Property
forall era. EraTxOut era => Proof era -> TxOut era -> Property
txOutRoundTrip Proof ShelleyEra
Shelley
        ]
    ]

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

-- | Ada is preserved over a trace of length 100
adaIsPreserved ::
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  TestTree
adaIsPreserved :: forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof era
proof Int
numTx GenSize
gensize =
  Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (Proof era -> [Char]
forall a. Show a => a -> [Char]
show Proof era
proof [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
$
    Proof era
-> Int
-> GenSize
-> (MockChainState era -> MockChainState era -> Property)
-> Gen Property
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 -> 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)
    [ Int -> GenSize -> TestTree
adaIsPreservedBabbage Int
numTx GenSize
gensize
    , Proof AlonzoEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof AlonzoEra
Alonzo Int
numTx GenSize
gensize
    , Proof MaryEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof MaryEra
Mary Int
numTx GenSize
gensize
    , Proof AllegraEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof AllegraEra
Allegra Int
numTx GenSize
gensize
    , Proof ShelleyEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
adaIsPreserved Proof ShelleyEra
Shelley Int
numTx GenSize
gensize
    ]

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

-- | 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 ::
  ( 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 =
  Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (Proof era -> [Char]
forall a. Show a => a -> [Char]
show Proof era
proof [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
$
    Proof era
-> Int
-> GenSize
-> (MockChainState era -> MockChainState era -> Property)
-> Gen Property
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 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,
      Proof BabbageEra -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof BabbageEra
Babbage GenSize
genSize
    , Proof AlonzoEra -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof AlonzoEra
Alonzo GenSize
genSize
    , Proof MaryEra -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof MaryEra
Mary GenSize
genSize
    , Proof AllegraEra -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof AllegraEra
Allegra GenSize
genSize
    , Proof ShelleyEra -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> GenSize -> TestTree
incrementStakeInvariant Proof ShelleyEra
Shelley GenSize
genSize
    ]

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

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

adaIsPreservedInEachEpoch ::
  forall era.
  Reflect era =>
  Proof era ->
  GenSize ->
  TestTree
adaIsPreservedInEachEpoch :: forall era. Reflect era => Proof era -> GenSize -> TestTree
adaIsPreservedInEachEpoch Proof era
proof GenSize
genSize =
  Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 (Proof era -> [Char]
forall a. Show a => a -> [Char]
show Proof era
proof) (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    Proof era
-> Int
-> GenSize
-> (Trace (MOCKCHAIN era) -> Property)
-> Gen Property
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 = 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"
    ]

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

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

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

test :: Int -> Proof era -> IO ()
test :: forall era. Int -> Proof era -> IO ()
test Int
n Proof era
proof = TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
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 ->
      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
$
        Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (Gen (Box era) -> (Box era -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof era -> GenSize -> Gen (Box era)
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
forall a. Default a => a
def) (Proof era -> Box era -> Property
forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 ToExpr (PredicateFailure (EraRule "LEDGER" era)), EraTest era) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof era
proof))
    Proof era
Alonzo ->
      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
$
        Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (Gen (Box era) -> (Box era -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof era -> GenSize -> Gen (Box era)
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
forall a. Default a => a
def) (Proof era -> Box era -> Property
forall era.
(Reflect era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 ToExpr (PredicateFailure (EraRule "LEDGER" era)), EraTest era) =>
Proof era -> Box era -> Property
testTxValidForLEDGER Proof era
proof))
    Proof era
Shelley ->
      Int -> [Char] -> Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Shelley ValidTx preserves ADA" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (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 (GenSize
-> Gen (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
genTxAndLEDGERStateShelley GenSize
forall a. Default a => a
def) (TRC (EraRule "LEDGER" ShelleyEra), GenState ShelleyEra)
-> Property
(TRC (ShelleyLEDGER ShelleyEra), GenState ShelleyEra) -> Property
testTxValidForLEDGERShelley)
    Proof era
other -> [Char] -> TestTree
forall a. HasCallStack => [Char] -> a
error ([Char]
"NO Test in era " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Char]
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 = (b, GenState era) -> b
forall a b. (a, b) -> a
fst ((b, GenState era) -> b) -> Gen (b, GenState era) -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proof era -> GenSize -> GenRS era b -> Gen (b, GenState era)
forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof era
proof GenSize
forall a. Default a => a
def (Proof era -> GenRS era b
computeWith Proof era
proof)

runTest ::
  (Reflect era, ToExpr a) =>
  (Proof era -> GenRS era a) ->
  (a -> IO ()) ->
  Proof era ->
  IO ()
runTest :: forall era a.
(Reflect era, ToExpr 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 <- Gen a -> IO a
forall a. Gen a -> IO a
generate (Proof era -> (Proof era -> GenRS era a) -> Gen a
forall era b.
Reflect era =>
Proof era -> (Proof era -> GenRS era b) -> Gen b
makeGen Proof era
proof Proof era -> GenRS era a
computeWith)
  Expr -> IO ()
forall a. Show a => a -> IO ()
print (a -> Expr
forall a. ToExpr a => a -> Expr
toExpr a
ans)
  a -> IO ()
action a
ans

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

main3 :: IO ()
main3 :: IO ()
main3 = (Proof AlonzoEra -> GenRS AlonzoEra (UTxO AlonzoEra))
-> (UTxO AlonzoEra -> IO ()) -> Proof AlonzoEra -> IO ()
forall era a.
(Reflect era, ToExpr a) =>
(Proof era -> GenRS era a) -> (a -> IO ()) -> Proof era -> IO ()
runTest (\Proof AlonzoEra
_x -> Map TxIn (TxOut AlonzoEra) -> UTxO AlonzoEra
forall era. Map TxIn (TxOut era) -> UTxO era
UTxO (Map TxIn (TxOut AlonzoEra) -> UTxO AlonzoEra)
-> ((Map TxIn (TxOut AlonzoEra),
     Maybe (TxIn, AlonzoTxOut AlonzoEra))
    -> Map TxIn (TxOut AlonzoEra))
-> (Map TxIn (TxOut AlonzoEra),
    Maybe (TxIn, AlonzoTxOut AlonzoEra))
-> UTxO AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map TxIn (TxOut AlonzoEra), Maybe (TxIn, AlonzoTxOut AlonzoEra))
-> Map TxIn (TxOut AlonzoEra)
forall a b. (a, b) -> a
fst ((Map TxIn (TxOut AlonzoEra), Maybe (TxIn, AlonzoTxOut AlonzoEra))
 -> UTxO AlonzoEra)
-> RWST
     (GenEnv AlonzoEra)
     ()
     (GenState AlonzoEra)
     Gen
     (Map TxIn (TxOut AlonzoEra), Maybe (TxIn, AlonzoTxOut AlonzoEra))
-> GenRS AlonzoEra (UTxO AlonzoEra)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenRS
  AlonzoEra (Map TxIn (TxOut AlonzoEra), Maybe (UtxoEntry AlonzoEra))
RWST
  (GenEnv AlonzoEra)
  ()
  (GenState AlonzoEra)
  Gen
  (Map TxIn (TxOut AlonzoEra), Maybe (TxIn, AlonzoTxOut AlonzoEra))
forall era.
Reflect era =>
GenRS era (MUtxo era, Maybe (UtxoEntry era))
genUTxO) UTxO AlonzoEra -> IO ()
forall {era}. UTxO era -> IO ()
action Proof AlonzoEra
Alonzo
  where
    action :: UTxO era -> IO ()
action (UTxO Map TxIn (TxOut era)
x) = [Char] -> IO ()
putStrLn ([Char]
"Size = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Map TxIn (TxOut era) -> Int
forall k a. Map k a -> Int
Map.size Map TxIn (TxOut era)
x))