{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Shelley.Rules.TestChain (
  delegTraceFromBlock,
  forAllChainTrace,
  ledgerTraceFromBlock,
  ledgerTraceFromBlockWithRestrictedUTxO,
  chainSstWithTick,
  poolTraceFromBlock,
  TestingLedger,
  splitTrace,
  forEachEpochTrace,
  traceLen,
  longTraceLen,
  shortChainTrace,
) where

import Cardano.Ledger.BaseTypes (Globals, SlotNo (..))
import Cardano.Ledger.Block (
  Block (..),
  bheader,
  neededTxInsForBlock,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Ptr (..), SlotNo32 (..))
import Cardano.Ledger.Shelley.API (ApplyBlock, ShelleyDELEG)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  UTxOState (..),
  curPParamsEpochStateL,
  lsCertStateL,
 )
import Cardano.Ledger.Shelley.Rules (
  DelegEnv (..),
  LedgerEnv (..),
  PoolEnv (..),
  ShelleyPOOL,
 )
import Cardano.Ledger.Shelley.State
import Cardano.Protocol.TPraos.API (GetLedgerView)
import Cardano.Protocol.TPraos.BHeader (
  BHeader (..),
  bhbody,
  bheaderSlotNo,
 )
import Control.Monad.Trans.Reader (ReaderT)
import Control.State.Transition
import Data.Foldable (toList)
import Data.Functor.Identity (Identity)
import qualified Data.Map.Strict as Map
import Data.Maybe (mapMaybe)
import Data.Proxy
import qualified Data.Set as Set
import Data.Word (Word64)
import Lens.Micro ((^.))
import Lens.Micro.Extras (view)
import Test.Cardano.Ledger.Shelley.ConcreteCryptoTypes (MockCrypto)
import Test.Cardano.Ledger.Shelley.Constants (Constants)
import Test.Cardano.Ledger.Shelley.Generator.Block (tickChainState)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import qualified Test.Cardano.Ledger.Shelley.Generator.Presets as Preset (genEnv)
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
import Test.Cardano.Ledger.Shelley.Generator.Trace.Chain (mkGenesisChainState)
import Test.Cardano.Ledger.Shelley.Rules.Chain (CHAIN, ChainState (..))
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
  epochFromSlotNo,
  runShelleyBase,
  testGlobals,
 )
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  Trace (..),
  sourceSignalTargets,
  splitTrace,
 )
import qualified Test.Control.State.Transition.Trace as Trace
import Test.Control.State.Transition.Trace.Generator.QuickCheck (forAllTraceFromInitState)
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (
  Property,
  Testable (..),
  conjoin,
  withMaxSuccess,
 )

------------------------------
-- Constants for Properties --
------------------------------

numberOfTests :: Word64
numberOfTests :: Word64
numberOfTests = Word64
300

traceLen :: Word64
traceLen :: Word64
traceLen = Word64
100

longTraceLen :: Word64
longTraceLen :: Word64
longTraceLen = Word64
150

type TestingLedger era ledger =
  ( BaseM ledger ~ ReaderT Globals Identity
  , Environment ledger ~ LedgerEnv era
  , State ledger ~ LedgerState era
  , Signal ledger ~ Tx era
  , Embed (EraRule "DELEGS" era) ledger
  , Embed (EraRule "UTXOW" era) ledger
  , STS ledger
  )

-- ===================================================

-- | Properties on really short chains, with only 100 successes
shortChainTrace ::
  forall era.
  ( EraGen era
  , EraGov era
  , EraStake era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  ) =>
  Constants ->
  (SourceSignalTarget (CHAIN era) -> Property) ->
  Property
shortChainTrace :: forall era.
(EraGen era, EraGov era, EraStake era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
shortChainTrace Constants
constants SourceSignalTarget (CHAIN era) -> Property
f = Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
100 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ forall era prop.
(EraGen era, EraGov era, EraStake era, Testable prop,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
10 Constants
constants ((Trace (CHAIN era) -> Property) -> Property)
-> (Trace (CHAIN era) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr -> [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ((SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
f (Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr))

----------------------------------------------------------------------
-- Projections of CHAIN Trace
----------------------------------------------------------------------

-- | Reconstruct a LEDGER trace from the transactions in a Block and ChainState
ledgerTraceFromBlock ::
  forall era ledger.
  ( ChainProperty era
  , TestingLedger era ledger
  ) =>
  ChainState era ->
  Block (BHeader MockCrypto) era ->
  (ChainState era, Trace ledger)
ledgerTraceFromBlock :: forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock ChainState era
chainSt Block (BHeader MockCrypto) era
block =
  ( ChainState era
tickedChainSt
  , ShelleyBase (Trace ledger) -> Trace ledger
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase (Trace ledger) -> Trace ledger)
-> ShelleyBase (Trace ledger) -> Trace ledger
forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure @ledger LedgerEnv era
Environment ledger
ledgerEnv State ledger
LedgerState era
ledgerSt0 [Tx era]
[Signal ledger]
txs
  )
  where
    (ChainState era
tickedChainSt, LedgerEnv era
ledgerEnv, LedgerState era
ledgerSt0, [Tx era]
txs) = ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
forall era.
(GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) era
block

-- | This function is nearly the same as ledgerTraceFromBlock, but
-- it restricts the UTxO state to only those needed by the block.
-- It also returns the unused UTxO for comparison later.
ledgerTraceFromBlockWithRestrictedUTxO ::
  forall era ledger.
  ( ChainProperty era
  , TestingLedger era ledger
  ) =>
  ChainState era ->
  Block (BHeader MockCrypto) era ->
  (UTxO era, Trace ledger)
ledgerTraceFromBlockWithRestrictedUTxO :: forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (UTxO era, Trace ledger)
ledgerTraceFromBlockWithRestrictedUTxO ChainState era
chainSt Block (BHeader MockCrypto) era
block =
  ( Map TxIn (TxOut era) -> UTxO era
forall era. Map TxIn (TxOut era) -> UTxO era
UTxO Map TxIn (TxOut era)
irrelevantUTxO
  , ShelleyBase (Trace ledger) -> Trace ledger
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase (Trace ledger) -> Trace ledger)
-> ShelleyBase (Trace ledger) -> Trace ledger
forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure @ledger LedgerEnv era
Environment ledger
ledgerEnv State ledger
LedgerState era
ledgerSt0' [Tx era]
[Signal ledger]
txs
  )
  where
    (ChainState era
_tickedChainSt, LedgerEnv era
ledgerEnv, LedgerState era
ledgerSt0, [Tx era]
txs) = ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
forall era.
(GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) era
block
    txIns :: Set TxIn
txIns = Block (BHeader MockCrypto) era -> Set TxIn
forall h era. EraSegWits era => Block h era -> Set TxIn
neededTxInsForBlock Block (BHeader MockCrypto) era
block
    LedgerState UTxOState era
utxoSt CertState era
delegationSt = LedgerState era
ledgerSt0
    utxo :: Map TxIn (TxOut era)
utxo = UTxO era -> Map TxIn (TxOut era)
forall era. UTxO era -> Map TxIn (TxOut era)
unUTxO (UTxO era -> Map TxIn (TxOut era))
-> (UTxOState era -> UTxO era)
-> UTxOState era
-> Map TxIn (TxOut era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo (UTxOState era -> Map TxIn (TxOut era))
-> UTxOState era -> Map TxIn (TxOut era)
forall a b. (a -> b) -> a -> b
$ UTxOState era
utxoSt
    (Map TxIn (TxOut era)
relevantUTxO, Map TxIn (TxOut era)
irrelevantUTxO) = (TxIn -> TxOut era -> Bool)
-> Map TxIn (TxOut era)
-> (Map TxIn (TxOut era), Map TxIn (TxOut era))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (Bool -> TxOut era -> Bool
forall a b. a -> b -> a
const (Bool -> TxOut era -> Bool)
-> (TxIn -> Bool) -> TxIn -> TxOut era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TxIn -> Set TxIn -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TxIn
txIns)) Map TxIn (TxOut era)
utxo
    ledgerSt0' :: LedgerState era
ledgerSt0' = UTxOState era -> CertState era -> LedgerState era
forall era. UTxOState era -> CertState era -> LedgerState era
LedgerState (UTxOState era
utxoSt {utxosUtxo = UTxO relevantUTxO}) CertState era
delegationSt

-- | Reconstruct a POOL trace from the transactions in a Block and ChainState
poolTraceFromBlock ::
  forall era.
  ( ChainProperty era
  , ShelleyEraTxBody era
  ) =>
  ChainState era ->
  Block (BHeader MockCrypto) era ->
  (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock :: forall era.
(ChainProperty era, ShelleyEraTxBody era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock ChainState era
chainSt Block (BHeader MockCrypto) era
block =
  ( ChainState era
tickedChainSt
  , ShelleyBase (Trace (ShelleyPOOL era)) -> Trace (ShelleyPOOL era)
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase (Trace (ShelleyPOOL era)) -> Trace (ShelleyPOOL era))
-> ShelleyBase (Trace (ShelleyPOOL era)) -> Trace (ShelleyPOOL era)
forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure @(ShelleyPOOL era) PoolEnv era
Environment (ShelleyPOOL era)
poolEnv PState era
State (ShelleyPOOL era)
poolSt0 [PoolCert]
[Signal (ShelleyPOOL era)]
poolCerts
  )
  where
    (ChainState era
tickedChainSt, LedgerEnv era
ledgerEnv, LedgerState era
ledgerSt0, [Tx era]
txs) = ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
forall era.
(GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) era
block
    certs :: [Tx era] -> [TxCert era]
certs = (Tx era -> [TxCert era]) -> [Tx era] -> [TxCert era]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (StrictSeq (TxCert era) -> [TxCert era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (TxCert era) -> [TxCert era])
-> (Tx era -> StrictSeq (TxCert era)) -> Tx era -> [TxCert era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (StrictSeq (TxCert era)) (TxBody era) (StrictSeq (TxCert era))
-> TxBody era -> StrictSeq (TxCert era)
forall a s. Getting a s a -> s -> a
view Getting
  (StrictSeq (TxCert era)) (TxBody era) (StrictSeq (TxCert era))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL (TxBody era -> StrictSeq (TxCert era))
-> (Tx era -> TxBody era) -> Tx era -> StrictSeq (TxCert era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (TxBody era) (Tx era) (TxBody era) -> Tx era -> TxBody era
forall a s. Getting a s a -> s -> a
view Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL)
    poolCerts :: [PoolCert]
poolCerts = (TxCert era -> Maybe PoolCert) -> [TxCert era] -> [PoolCert]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TxCert era -> Maybe PoolCert
forall era. EraTxCert era => TxCert era -> Maybe PoolCert
getPoolCertTxCert ([Tx era] -> [TxCert era]
certs [Tx era]
txs)
    poolEnv :: PoolEnv era
poolEnv =
      let LedgerEnv SlotNo
sl Maybe EpochNo
_ TxIx
_ PParams era
pp ChainAccountState
_ = LedgerEnv era
ledgerEnv
       in EpochNo -> PParams era -> PoolEnv era
forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv (SlotNo -> EpochNo
epochFromSlotNo SlotNo
sl) PParams era
pp
    poolSt0 :: PState era
poolSt0 =
      LedgerState era
ledgerSt0 LedgerState era
-> Getting (PState era) (LedgerState era) (PState era)
-> PState era
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const (PState era) (CertState era))
-> LedgerState era -> Const (PState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (PState era) (CertState era))
 -> LedgerState era -> Const (PState era) (LedgerState era))
-> ((PState era -> Const (PState era) (PState era))
    -> CertState era -> Const (PState era) (CertState era))
-> Getting (PState era) (LedgerState era) (PState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era -> Const (PState era) (PState era))
-> CertState era -> Const (PState era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL

-- | Reconstruct a DELEG trace from all the transaction certificates in a Block
delegTraceFromBlock ::
  forall era.
  ( ChainProperty era
  , ShelleyEraTxBody era
  ) =>
  ChainState era ->
  Block (BHeader MockCrypto) era ->
  (DelegEnv era, Trace (ShelleyDELEG era))
delegTraceFromBlock :: forall era.
(ChainProperty era, ShelleyEraTxBody era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (DelegEnv era, Trace (ShelleyDELEG era))
delegTraceFromBlock ChainState era
chainSt Block (BHeader MockCrypto) era
block =
  ( DelegEnv era
delegEnv
  , ShelleyBase (Trace (ShelleyDELEG era)) -> Trace (ShelleyDELEG era)
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase (Trace (ShelleyDELEG era))
 -> Trace (ShelleyDELEG era))
-> ShelleyBase (Trace (ShelleyDELEG era))
-> Trace (ShelleyDELEG era)
forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure @(ShelleyDELEG era) DelegEnv era
Environment (ShelleyDELEG era)
delegEnv DState era
State (ShelleyDELEG era)
delegSt0 [TxCert era]
[Signal (ShelleyDELEG era)]
blockCerts
  )
  where
    (ChainState era
_tickedChainSt, LedgerEnv era
ledgerEnv, LedgerState era
ledgerSt0, [Tx era]
txs) = ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
forall era.
(GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) era
block
    certs :: [Tx era] -> [TxCert era]
certs = (Tx era -> [TxCert era]) -> [Tx era] -> [TxCert era]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([TxCert era] -> [TxCert era]
forall a. [a] -> [a]
reverse ([TxCert era] -> [TxCert era])
-> (Tx era -> [TxCert era]) -> Tx era -> [TxCert era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictSeq (TxCert era) -> [TxCert era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (TxCert era) -> [TxCert era])
-> (Tx era -> StrictSeq (TxCert era)) -> Tx era -> [TxCert era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (StrictSeq (TxCert era)) (TxBody era) (StrictSeq (TxCert era))
-> TxBody era -> StrictSeq (TxCert era)
forall a s. Getting a s a -> s -> a
view Getting
  (StrictSeq (TxCert era)) (TxBody era) (StrictSeq (TxCert era))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL (TxBody era -> StrictSeq (TxCert era))
-> (Tx era -> TxBody era) -> Tx era -> StrictSeq (TxCert era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (TxBody era) (Tx era) (TxBody era) -> Tx era -> TxBody era
forall a s. Getting a s a -> s -> a
view Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL)
    blockCerts :: [TxCert era]
blockCerts = (TxCert era -> Bool) -> [TxCert era] -> [TxCert era]
forall a. (a -> Bool) -> [a] -> [a]
filter TxCert era -> Bool
forall {era}.
(ProtVerIsInBounds
   "at most"
   era
   8
   (OrdCond (CmpNat (ProtVerLow era) 8) 'True 'True 'False),
 Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 ShelleyEraTxCert era) =>
TxCert era -> Bool
delegCert ([Tx era] -> [TxCert era]
certs [Tx era]
txs)
    delegEnv :: DelegEnv era
delegEnv =
      let LedgerEnv slot :: SlotNo
slot@(SlotNo Word64
slot64) Maybe EpochNo
_ TxIx
txIx PParams era
pp ChainAccountState
reserves = LedgerEnv era
ledgerEnv
          dummyCertIx :: CertIx
dummyCertIx = CertIx
forall a. Bounded a => a
minBound
          ptr :: Ptr
ptr = SlotNo32 -> TxIx -> CertIx -> Ptr
Ptr (Word32 -> SlotNo32
SlotNo32 (Word64 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
slot64)) TxIx
txIx CertIx
dummyCertIx
       in SlotNo
-> EpochNo
-> Ptr
-> ChainAccountState
-> PParams era
-> DelegEnv era
forall era.
SlotNo
-> EpochNo
-> Ptr
-> ChainAccountState
-> PParams era
-> DelegEnv era
DelegEnv SlotNo
slot (SlotNo -> EpochNo
epochFromSlotNo SlotNo
slot) Ptr
ptr ChainAccountState
reserves PParams era
pp
    delegSt0 :: DState era
delegSt0 =
      LedgerState era
ledgerSt0 LedgerState era
-> Getting (DState era) (LedgerState era) (DState era)
-> DState era
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const (DState era) (CertState era))
-> LedgerState era -> Const (DState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (DState era) (CertState era))
 -> LedgerState era -> Const (DState era) (LedgerState era))
-> ((DState era -> Const (DState era) (DState era))
    -> CertState era -> Const (DState era) (CertState era))
-> Getting (DState era) (LedgerState era) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const (DState era) (DState era))
-> CertState era -> Const (DState era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
    delegCert :: TxCert era -> Bool
delegCert (RegTxCert Credential 'Staking
_) = Bool
True
    delegCert (UnRegTxCert Credential 'Staking
_) = Bool
True
    delegCert (DelegStakeTxCert Credential 'Staking
_ KeyHash 'StakePool
_) = Bool
True
    delegCert (MirTxCert MIRCert
_) = Bool
True
    delegCert TxCert era
_ = Bool
False

-- | Reconstruct a POOL trace from the transactions in a Block and ChainState
--
-- NOTE: we need to tick the slot before processing transactions
-- (in the same way that the CHAIN rule TICKs the slot before processing
-- transactions with the LEDGERS rule)
ledgerTraceBase ::
  forall era.
  ( GetLedgerView era
  , ApplyBlock era
  ) =>
  ChainState era ->
  Block (BHeader MockCrypto) era ->
  (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase :: forall era.
(GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) era
block =
  ( ChainState era
tickedChainSt
  , SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
LedgerEnv SlotNo
slot Maybe EpochNo
forall a. Maybe a
Nothing TxIx
forall a. Bounded a => a
minBound PParams era
pp_ (EpochState era -> ChainAccountState
forall era. EpochState era -> ChainAccountState
esChainAccountState EpochState era
nes)
  , EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState EpochState era
nes
  , [Tx era]
txs
  )
  where
    (Block (BHeader BHBody MockCrypto
bhb SignedKES (KES MockCrypto) (BHBody MockCrypto)
_) TxSeq era
txSeq) = Block (BHeader MockCrypto) era
block
    slot :: SlotNo
slot = BHBody MockCrypto -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody MockCrypto
bhb
    tickedChainSt :: ChainState era
tickedChainSt = SlotNo -> ChainState era -> ChainState era
forall era.
(GetLedgerView era, ApplyBlock era) =>
SlotNo -> ChainState era -> ChainState era
tickChainState SlotNo
slot ChainState era
chainSt
    nes :: EpochState era
nes = (NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
tickedChainSt
    pp_ :: PParams era
pp_ = EpochState era
nes EpochState era
-> Getting (PParams era) (EpochState era) (PParams era)
-> PParams era
forall s a. s -> Getting a s a -> a
^. Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
    -- Oldest to Newest first
    txs :: [Tx era]
txs = ([Tx era] -> [Tx era]
forall a. [a] -> [a]
reverse ([Tx era] -> [Tx era])
-> (TxSeq era -> [Tx era]) -> TxSeq era -> [Tx era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictSeq (Tx era) -> [Tx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (Tx era) -> [Tx era])
-> (TxSeq era -> StrictSeq (Tx era)) -> TxSeq era -> [Tx era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxSeq era -> StrictSeq (Tx era)
forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq) TxSeq era
txSeq -- HERE WE USE SOME SegWit function

-- | Transform the [(source, signal, target)] of a CHAIN Trace
-- by manually applying the Chain TICK Rule to each source and producing
-- [(source, signal, target')].
--
-- This allows for testing properties on Chain traces while excluding the effects
-- of Transactions and Certificates. For example we can check that pools that are
-- due for retirement at an epoch transition, are indeed retired.
--
-- Had we not excluded the effects of Transactions/Certificates, we might have
-- a pool that was correctly retired, but is again registered by a certificate
-- in the block following the transition.
chainSstWithTick ::
  forall era.
  ChainProperty era =>
  Trace (CHAIN era) ->
  [SourceSignalTarget (CHAIN era)]
chainSstWithTick :: forall era.
ChainProperty era =>
Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
chainSstWithTick Trace (CHAIN era)
ledgerTr =
  (SourceSignalTarget (CHAIN era) -> SourceSignalTarget (CHAIN era))
-> [SourceSignalTarget (CHAIN era)]
-> [SourceSignalTarget (CHAIN era)]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> SourceSignalTarget (CHAIN era)
applyTick (Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
ledgerTr)
  where
    applyTick :: SourceSignalTarget (CHAIN era) -> SourceSignalTarget (CHAIN era)
applyTick sst :: SourceSignalTarget (CHAIN era)
sst@SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
      let bh :: BHeader MockCrypto
bh = Block (BHeader MockCrypto) era -> BHeader MockCrypto
forall h era. Block h era -> h
bheader Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
          slot :: SlotNo
slot = (BHBody MockCrypto -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo (BHBody MockCrypto -> SlotNo)
-> (BHeader MockCrypto -> BHBody MockCrypto)
-> BHeader MockCrypto
-> SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BHeader MockCrypto -> BHBody MockCrypto
forall c. Crypto c => BHeader c -> BHBody c
bhbody) BHeader MockCrypto
bh
       in SourceSignalTarget (CHAIN era)
sst {target = tickChainState @era slot chainSt}

---------------------------
-- Utils --
---------------------------

forAllChainTrace ::
  forall era prop.
  ( EraGen era
  , EraGov era
  , EraStake era
  , Testable prop
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  ) =>
  Word64 -> -- trace length
  Constants ->
  (Trace (CHAIN era) -> prop) ->
  Property
forAllChainTrace :: forall era prop.
(EraGen era, EraGov era, EraStake era, Testable prop,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace Word64
n Constants
constants Trace (CHAIN era) -> prop
prop =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
numberOfTests) (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Property -> Property
forall prop. Testable prop => prop -> Property
property (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    BaseEnv (CHAIN era)
-> Word64
-> GenEnv MockCrypto era
-> Maybe
     (IRC (CHAIN era)
      -> Gen
           (Either
              (NonEmpty (PredicateFailure (CHAIN era))) (State (CHAIN era))))
-> (Trace (CHAIN era) -> prop)
-> Property
forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState
      Globals
BaseEnv (CHAIN era)
testGlobals
      Word64
n
      (forall era c.
(EraGen era, Crypto c) =>
Proxy era -> Constants -> GenEnv c era
Preset.genEnv @era @MockCrypto Proxy era
p Constants
constants)
      ((IRC (CHAIN era)
 -> Gen
      (Either
         (NonEmpty (PredicateFailure (CHAIN era))) (State (CHAIN era))))
-> Maybe
     (IRC (CHAIN era)
      -> Gen
           (Either
              (NonEmpty (PredicateFailure (CHAIN era))) (State (CHAIN era))))
forall a. a -> Maybe a
Just ((IRC (CHAIN era)
  -> Gen
       (Either
          (NonEmpty (PredicateFailure (CHAIN era))) (State (CHAIN era))))
 -> Maybe
      (IRC (CHAIN era)
       -> Gen
            (Either
               (NonEmpty (PredicateFailure (CHAIN era))) (State (CHAIN era)))))
-> (IRC (CHAIN era)
    -> Gen
         (Either
            (NonEmpty (PredicateFailure (CHAIN era))) (State (CHAIN era))))
-> Maybe
     (IRC (CHAIN era)
      -> Gen
           (Either
              (NonEmpty (PredicateFailure (CHAIN era))) (State (CHAIN era))))
forall a b. (a -> b) -> a -> b
$ GenEnv MockCrypto era
-> IRC (CHAIN era)
-> Gen
     (Either
        (NonEmpty (TestChainPredicateFailure era)) (ChainState era))
forall era a c.
(EraGen era, EraGov era, EraStake era) =>
GenEnv c era -> IRC (CHAIN era) -> Gen (Either a (ChainState era))
mkGenesisChainState (forall era c.
(EraGen era, Crypto c) =>
Proxy era -> Constants -> GenEnv c era
Preset.genEnv @era @MockCrypto Proxy era
p Constants
constants))
      Trace (CHAIN era) -> prop
prop
  where
    p :: Proxy era
    p :: Proxy era
p = Proxy era
forall {k} (t :: k). Proxy t
Proxy

-- | Test a property on the first 'subtracecount' sub-Traces that end on an EpochBoundary
forEachEpochTrace ::
  forall era prop.
  ( EraGen era
  , EraGov era
  , EraStake era
  , Testable prop
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  ) =>
  Int ->
  Word64 ->
  Constants ->
  (Trace (CHAIN era) -> prop) ->
  Property
forEachEpochTrace :: forall era prop.
(EraGen era, EraGov era, EraStake era, Testable prop,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Int
-> Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forEachEpochTrace Int
subtracecount Word64
tracelen Constants
constants Trace (CHAIN era) -> prop
f = Word64 -> Constants -> (Trace (CHAIN era) -> Property) -> Property
forall era prop.
(EraGen era, EraGov era, EraStake era, Testable prop,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace Word64
tracelen Constants
constants Trace (CHAIN era) -> Property
action
  where
    -- split at contiguous elements with different Epoch numbers
    p :: ChainState era -> ChainState era -> Bool
p ChainState era
new ChainState era
old = (NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (NewEpochState era -> EpochNo)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
new EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
/= (NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (NewEpochState era -> EpochNo)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
old
    -- At a minimum throw away the last trace which is probably an incomplete epoch
    action :: Trace (CHAIN era) -> Property
action Trace (CHAIN era)
tr = [prop] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([prop] -> Property) -> [prop] -> Property
forall a b. (a -> b) -> a -> b
$ (Trace (CHAIN era) -> prop) -> [Trace (CHAIN era)] -> [prop]
forall a b. (a -> b) -> [a] -> [b]
map Trace (CHAIN era) -> prop
f (Int -> [Trace (CHAIN era)] -> [Trace (CHAIN era)]
forall a. Int -> [a] -> [a]
take (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
subtracecount (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) ([Trace (CHAIN era)] -> [Trace (CHAIN era)]
forall a. [a] -> [a]
reverse [Trace (CHAIN era)]
traces))
      where
        traces :: [Trace (CHAIN era)]
traces = (State (CHAIN era) -> State (CHAIN era) -> Bool)
-> Trace (CHAIN era) -> [Trace (CHAIN era)]
forall s. (State s -> State s -> Bool) -> Trace s -> [Trace s]
splitTrace State (CHAIN era) -> State (CHAIN era) -> Bool
ChainState era -> ChainState era -> Bool
forall {era} {era}. ChainState era -> ChainState era -> Bool
p Trace (CHAIN era)
tr
        m :: Int
m = [Trace (CHAIN era)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Trace (CHAIN era)]
traces

-- ================================
-- an example how one might debug one test, which can be replayed
-- import Test.Tasty (defaultMain)
-- main :: IO ()
-- main = defaultMain (minimal @(ShelleyEra TestCrypto))
-- Then in ghci, one can just type
-- :main --quickcheck-replay=443873
-- =================================