{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Generic.Trace where

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

import Cardano.Ledger.Address (Addr (..))
import Cardano.Ledger.Alonzo.Rules (AlonzoUtxowPredFailure (..))
import Cardano.Ledger.Alonzo.Tx (AlonzoTx (body))
import Cardano.Ledger.Babbage.Rules (BabbageUtxowPredFailure (..))
import Cardano.Ledger.Babbage.TxBody (certs')
import Cardano.Ledger.BaseTypes (BlocksMade (..), Globals)
import Cardano.Ledger.Coin (CompactForm (CompactCoin))
import Cardano.Ledger.EpochBoundary (SnapShots (..), calculatePoolDistr)
import Cardano.Ledger.PoolDistr (IndividualPoolStake (..), PoolDistr (..))
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  CertState (..),
  DState (dsUnified),
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  PState (..),
  StashedAVVMAddresses,
  UTxOState (..),
  curPParamsEpochStateL,
  prevPParamsEpochStateL,
 )
import Cardano.Ledger.Shelley.Rules (
  ShelleyLedgerPredFailure (..),
  ShelleyLedgersPredFailure (..),
  ShelleyUtxowPredFailure (ScriptWitnessNotValidatingUTXOW),
 )
import qualified Cardano.Ledger.UMap as UM
import Cardano.Ledger.UTxO (UTxO (..))
import Cardano.Slotting.Slot (EpochNo (..), SlotNo (..))
import Control.Monad (forM)
import Control.Monad.Trans.Class (MonadTrans (lift))
import Control.Monad.Trans.RWS.Strict (get, gets)
import Control.Monad.Trans.Reader (ReaderT (..))
import qualified Control.State.Transition as STS
import Control.State.Transition.Extended (IRC (), STS (..), TRC (..))
import Data.Default (Default (def))
import qualified Data.Foldable as Fold
import Data.Functor.Identity (Identity (runIdentity))
import Data.IORef (IORef, newIORef, readIORef, writeIORef)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import Data.Sequence.Strict (StrictSeq (..))
import qualified Data.Sequence.Strict as SS
import qualified Data.Set as Set
import Data.Vector (Vector, (!))
import qualified Data.Vector as Vector
import qualified Debug.Trace as Debug
import GHC.Word (Word64)
import Lens.Micro ((&), (.~), (^.))
import Prettyprinter (hsep, parens, vsep)
import System.IO.Unsafe (unsafePerformIO)
import Test.Cardano.Ledger.Generic.ApplyTx (applyTx)
import Test.Cardano.Ledger.Generic.Fields (TxBodyField (..), abstractTxBody)
import Test.Cardano.Ledger.Generic.Functions (
  adaPots,
  allInputs,
  getBody,
  getScriptWits,
  getWitnesses,
  isValid',
  totalAda,
  txoutFields,
 )
import Test.Cardano.Ledger.Generic.GenState (
  GenEnv (..),
  GenRS,
  GenSize (..),
  GenState (..),
  getBlocksizeMax,
  getReserves,
  getSlot,
  getSlotDelta,
  getTreasury,
  gsModel,
  initStableFields,
  initialLedgerState,
  modifyModel,
  runGenRS,
 )
import Test.Cardano.Ledger.Generic.MockChain
import Test.Cardano.Ledger.Generic.ModelState (MUtxo, stashedAVVMAddressesZero)
import Test.Cardano.Ledger.Generic.PrettyCore (
  PDoc,
  PrettyA (..),
  pcCoin,
  pcCredential,
  pcKeyHash,
  pcPoolParams,
  pcScript,
  pcScriptHash,
  pcSlotNo,
  pcTxBodyField,
  pcTxIn,
  ppInt,
  ppList,
  ppMap,
  ppRecord,
  ppSafeHash,
  ppSet,
  ppString,
  ppWord64,
  scriptSummary,
 )
import Test.Cardano.Ledger.Generic.Proof hiding (lift)
import Test.Cardano.Ledger.Generic.TxGen (genAlonzoTx)
import Test.Cardano.Ledger.Shelley.Rules.IncrementalStake (stakeDistr)
import Test.Cardano.Ledger.Shelley.Utils (applySTSTest, runShelleyBase, testGlobals)
import Test.Control.State.Transition.Trace (Trace (..), lastState, splitTrace)
import Test.Control.State.Transition.Trace.Generator.QuickCheck (HasTrace (..), traceFromInitState)
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain, testGroup)
import Test.Tasty.QuickCheck (testProperty)

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

-- | Generate a Tx and an internal Model of the state after the tx
--   has been applied. That model can be used to generate the next Tx
genRsTxAndModel :: forall era. Reflect era => Proof era -> Int -> SlotNo -> GenRS era (Tx era)
genRsTxAndModel :: forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> GenRS era (Tx era)
genRsTxAndModel Proof era
proof Int
n SlotNo
slot = do
  (UTxO era
_, Tx era
tx) <- forall era.
Reflect era =>
Proof era -> SlotNo -> GenRS era (UTxO era, Tx era)
genAlonzoTx Proof era
proof SlotNo
slot
  forall era.
(ModelNewEpochState era -> ModelNewEpochState era) -> GenRS era ()
modifyModel (\ModelNewEpochState era
model -> forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> Model era -> Tx era -> Model era
applyTx Proof era
proof Int
n SlotNo
slot ModelNewEpochState era
model Tx era
tx)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Tx era
tx

-- | Generate a Vector of (StrictSeq (Tx era))  representing a (Vector Block)
genRsTxSeq ::
  forall era.
  Reflect era =>
  Proof era ->
  Int ->
  Int ->
  [(StrictSeq (Tx era), SlotNo)] ->
  SlotNo ->
  GenRS era (Vector (StrictSeq (Tx era), SlotNo))
genRsTxSeq :: forall era.
Reflect era =>
Proof era
-> Int
-> Int
-> [(StrictSeq (Tx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
genRsTxSeq Proof era
proof Int
this Int
lastN [(StrictSeq (Tx era), SlotNo)]
ans SlotNo
_slot | Int
this forall a. Ord a => a -> a -> Bool
>= Int
lastN = do
  seq :: forall a b. a -> b -> b
seq
    (forall a. IO a -> a
unsafePerformIO (forall a. IORef a -> a -> IO ()
writeIORef IORef TT
theVector (forall era. Proof era -> [(StrictSeq (Tx era), SlotNo)] -> TT
TT Proof era
proof (forall a. [a] -> [a]
reverse [(StrictSeq (Tx era), SlotNo)]
ans))))
    (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [a] -> Vector a
Vector.fromList (forall a. [a] -> [a]
reverse [(StrictSeq (Tx era), SlotNo)]
ans)))
genRsTxSeq Proof era
proof Int
this Int
lastN [(StrictSeq (Tx era), SlotNo)]
ans SlotNo
slot = do
  Integer
maxBlockSize <- forall era. GenState era -> Integer
getBlocksizeMax forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall w (m :: * -> *) r s. (Monoid w, Monad m) => RWST r w s m s
get
  Int
n <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Random a => (a, a) -> Gen a
choose (Int
2 :: Int, forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
maxBlockSize)
  [Tx era]
txs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
0 .. Int
n forall a. Num a => a -> a -> a
- Int
1] (\Int
i -> forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> GenRS era (Tx era)
genRsTxAndModel Proof era
proof (Int
this forall a. Num a => a -> a -> a
+ Int
i) SlotNo
slot)
  (Word64, Word64)
newSlotRange <- forall w (m :: * -> *) s a r.
(Monoid w, Monad m) =>
(s -> a) -> RWST r w s m a
gets forall era. GenState era -> (Word64, Word64)
getSlotDelta
  SlotNo
nextSlotNo <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Word64 -> SlotNo
SlotNo forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Num a => a -> a -> a
+ (SlotNo -> Word64
unSlotNo SlotNo
slot)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Word64, Word64)
newSlotRange
  forall era.
Reflect era =>
Proof era
-> Int
-> Int
-> [(StrictSeq (Tx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
genRsTxSeq Proof era
proof (Int
this forall a. Num a => a -> a -> a
+ Int
n) Int
lastN ((forall a. [a] -> StrictSeq a
SS.fromList [Tx era]
txs, SlotNo
slot) forall a. a -> [a] -> [a]
: [(StrictSeq (Tx era), SlotNo)]
ans) SlotNo
nextSlotNo

-- | Generate a Vector of Blocks, and an initial LedgerState
genTxSeq ::
  forall era.
  Reflect era =>
  Proof era -> -- Proof of the Era we want to generate the sequence in
  GenSize -> -- Size of things the generated code should adhere to
  Int -> -- The number of Tx in the sequence
  GenRS era () -> -- An arbitrary 'initialization action', to run before we generate the sequence
  -- use (pure ()) if you don't want or need initialization
  Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq :: forall era.
Reflect era =>
Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq Proof era
proof GenSize
gensize Int
numTx GenRS era ()
initialize = do
  forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof era
proof GenSize
gensize (GenRS era ()
initialize forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall era.
Reflect era =>
Proof era
-> Int
-> Int
-> [(StrictSeq (Tx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
genRsTxSeq Proof era
proof Int
0 Int
numTx [] (Word64 -> SlotNo
SlotNo forall a b. (a -> b) -> a -> b
$ Word64
1))

runTest :: IO ()
runTest :: IO ()
runTest = do
  (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo)
v, GenState BabbageEra
_) <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
Reflect era =>
Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq Proof BabbageEra
Babbage forall a. Default a => a
def Int
20 (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  forall a. Show a => a -> IO ()
print (forall a. Vector a -> Int
Vector.length Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo)
v)

-- ==================================================================
-- Constructing the "real", initial NewEpochState, from the GenState

initialMockChainState ::
  Reflect era =>
  Proof era ->
  GenState era ->
  MockChainState era
initialMockChainState :: forall era.
Reflect era =>
Proof era -> GenState era -> MockChainState era
initialMockChainState Proof era
proof GenState era
gstate =
  forall era.
NewEpochState era
-> NewEpochState era -> SlotNo -> Int -> MockChainState era
MockChainState NewEpochState era
newepochstate NewEpochState era
newepochstate (forall era. GenState era -> SlotNo
getSlot GenState era
gstate) Int
0
  where
    ledgerstate :: LedgerState era
ledgerstate = forall era. Reflect era => GenState era -> LedgerState era
initialLedgerState GenState era
gstate
    newepochstate :: NewEpochState era
newepochstate =
      NewEpochState
        { nesEL :: EpochNo
nesEL = Word64 -> EpochNo
EpochNo Word64
0
        , nesBprev :: BlocksMade
nesBprev = Map (KeyHash 'StakePool) Natural -> BlocksMade
BlocksMade forall k a. Map k a
Map.empty
        , nesBcur :: BlocksMade
nesBcur = Map (KeyHash 'StakePool) Natural -> BlocksMade
BlocksMade forall k a. Map k a
Map.empty
        , nesEs :: EpochState era
nesEs = forall era.
Reflect era =>
GenState era -> LedgerState era -> EpochState era
makeEpochState GenState era
gstate LedgerState era
ledgerstate
        , nesRu :: StrictMaybe PulsingRewUpdate
nesRu = forall a. StrictMaybe a
SNothing
        , nesPd :: PoolDistr
nesPd = Map (KeyHash 'StakePool) IndividualPoolStake
-> CompactForm Coin -> PoolDistr
PoolDistr (forall era.
GenState era -> Map (KeyHash 'StakePool) IndividualPoolStake
gsInitialPoolDistr GenState era
gstate) (Word64 -> CompactForm Coin
CompactCoin Word64
1)
        , stashedAVVMAddresses :: StashedAVVMAddresses era
stashedAVVMAddresses = forall era. Proof era -> StashedAVVMAddresses era
stashedAVVMAddressesZero Proof era
proof
        }

makeEpochState :: Reflect era => GenState era -> LedgerState era -> EpochState era
makeEpochState :: forall era.
Reflect era =>
GenState era -> LedgerState era -> EpochState era
makeEpochState GenState era
gstate LedgerState era
ledgerstate =
  EpochState
    { esAccountState :: AccountState
esAccountState = Coin -> Coin -> AccountState
AccountState (forall era. GenState era -> Coin
getTreasury GenState era
gstate) (forall era. GenState era -> Coin
getReserves GenState era
gstate)
    , esSnapshots :: SnapShots
esSnapshots = forall era. EraTxOut era => LedgerState era -> SnapShots
snaps LedgerState era
ledgerstate
    , esLState :: LedgerState era
esLState = LedgerState era
ledgerstate
    , esNonMyopic :: NonMyopic
esNonMyopic = forall a. Default a => a
def
    }
    forall a b. a -> (a -> b) -> b
& forall era. EraGov era => Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall era. GenEnv era -> PParams era
gePParams (forall era. GenState era -> GenEnv era
gsGenEnv GenState era
gstate)
    forall a b. a -> (a -> b) -> b
& forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall era. GenEnv era -> PParams era
gePParams (forall era. GenState era -> GenEnv era
gsGenEnv GenState era
gstate)

snaps :: EraTxOut era => LedgerState era -> SnapShots
snaps :: forall era. EraTxOut era => LedgerState era -> SnapShots
snaps (LedgerState UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u, utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
f} (CertState VState era
_ PState era
pstate DState era
dstate)) =
  SnapShot -> PoolDistr -> SnapShot -> SnapShot -> Coin -> SnapShots
SnapShots SnapShot
snap (SnapShot -> PoolDistr
calculatePoolDistr SnapShot
snap) SnapShot
snap SnapShot
snap Coin
f
  where
    snap :: SnapShot
snap = forall era.
EraTxOut era =>
UTxO era -> DState era -> PState era -> SnapShot
stakeDistr UTxO era
u DState era
dstate PState era
pstate

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

-- | Turn a UTxO into a smaller UTxO, with only entries mentioned in
--   the inputs of 'txs' ,  then pretty print it.
pcSmallUTxO :: EraTx era => Proof era -> MUtxo era -> [Tx era] -> PDoc
pcSmallUTxO :: forall era. EraTx era => Proof era -> MUtxo era -> [Tx era] -> PDoc
pcSmallUTxO Proof era
proof MUtxo era
u [Tx era]
txs = forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap TxIn -> PDoc
pcTxIn (forall era. EraTxOut era => Proof era -> TxOut era -> PDoc
shortTxOut Proof era
proof) MUtxo era
m
  where
    keys :: Set TxIn
keys = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map Tx era -> Set TxIn
f [Tx era]
txs)
    f :: Tx era -> Set TxIn
f Tx era
tx = forall era. EraTxBody era => Proof era -> TxBody era -> Set TxIn
allInputs Proof era
proof (forall era. EraTx era => Proof era -> Tx era -> TxBody era
getBody Proof era
proof Tx era
tx)
    m :: MUtxo era
m = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys MUtxo era
u Set TxIn
keys

raiseMockError ::
  forall era.
  Reflect era =>
  Word64 ->
  SlotNo ->
  EpochState era ->
  NonEmpty (MockChainFailure era) ->
  [Tx era] ->
  GenState era ->
  String
raiseMockError :: forall era.
Reflect era =>
Word64
-> SlotNo
-> EpochState era
-> NonEmpty (MockChainFailure era)
-> [Tx era]
-> GenState era
-> String
raiseMockError Word64
slot (SlotNo Word64
next) EpochState era
epochstate NonEmpty (MockChainFailure era)
pdfs [Tx era]
txs GenState {Int
Set (KeyHash 'StakePool)
Set (Credential 'Staking)
Map (ScriptHash, PlutusPurposeTag) (IsValid, Script era)
Map DataHash (Data era)
Map ScriptHash (Script era)
Map (KeyHash 'Witness) (KeyPair 'Witness)
Map (KeyHash 'StakePool) PoolParams
Map (KeyHash 'StakePool) IndividualPoolStake
Map ValidityInterval (Set ScriptHash)
Map TxIn (TxOut era)
Map (Credential 'Staking) (KeyHash 'StakePool)
Map (Credential 'Staking) Coin
ValidityInterval
Proof era
ModelNewEpochState era
GenEnv era
gsSeedIdx :: forall era. GenState era -> Int
gsProof :: forall era. GenState era -> Proof era
gsAvoidKey :: forall era. GenState era -> Set (KeyHash 'StakePool)
gsAvoidCred :: forall era. GenState era -> Set (Credential 'Staking)
gsStableDelegators :: forall era. GenState era -> Set (Credential 'Staking)
gsStablePools :: forall era. GenState era -> Set (KeyHash 'StakePool)
gsInitialPoolParams :: forall era. GenState era -> Map (KeyHash 'StakePool) PoolParams
gsInitialDelegations :: forall era.
GenState era -> Map (Credential 'Staking) (KeyHash 'StakePool)
gsInitialRewards :: forall era. GenState era -> Map (Credential 'Staking) Coin
gsInitialUtxo :: forall era. GenState era -> Map TxIn (TxOut era)
gsVI :: forall era. GenState era -> Map ValidityInterval (Set ScriptHash)
gsDatums :: forall era. GenState era -> Map DataHash (Data era)
gsPlutusScripts :: forall era.
GenState era
-> Map (ScriptHash, PlutusPurposeTag) (IsValid, Script era)
gsScripts :: forall era. GenState era -> Map ScriptHash (Script era)
gsKeys :: forall era.
GenState era -> Map (KeyHash 'Witness) (KeyPair 'Witness)
gsValidityInterval :: forall era. GenState era -> ValidityInterval
gsSeedIdx :: Int
gsGenEnv :: GenEnv era
gsProof :: Proof era
gsAvoidKey :: Set (KeyHash 'StakePool)
gsAvoidCred :: Set (Credential 'Staking)
gsStableDelegators :: Set (Credential 'Staking)
gsStablePools :: Set (KeyHash 'StakePool)
gsInitialPoolDistr :: Map (KeyHash 'StakePool) IndividualPoolStake
gsInitialPoolParams :: Map (KeyHash 'StakePool) PoolParams
gsInitialDelegations :: Map (Credential 'Staking) (KeyHash 'StakePool)
gsInitialRewards :: Map (Credential 'Staking) Coin
gsInitialUtxo :: Map TxIn (TxOut era)
gsModel :: ModelNewEpochState era
gsVI :: Map ValidityInterval (Set ScriptHash)
gsDatums :: Map DataHash (Data era)
gsPlutusScripts :: Map (ScriptHash, PlutusPurposeTag) (IsValid, Script era)
gsScripts :: Map ScriptHash (Script era)
gsKeys :: Map (KeyHash 'Witness) (KeyPair 'Witness)
gsValidityInterval :: ValidityInterval
gsGenEnv :: forall era. GenState era -> GenEnv era
gsInitialPoolDistr :: forall era.
GenState era -> Map (KeyHash 'StakePool) IndividualPoolStake
gsModel :: forall era. GenState era -> ModelNewEpochState era
..} =
  let utxo :: Map TxIn (TxOut era)
utxo = forall era. UTxO era -> Map TxIn (TxOut era)
unUTxO forall a b. (a -> b) -> a -> b
$ (forall era. UTxOState era -> UTxO era
utxosUtxo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> UTxOState era
lsUTxOState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState) EpochState era
epochstate
      _ssPoolParams :: Map (KeyHash 'StakePool) PoolParams
_ssPoolParams = (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> PState era
certPState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState) EpochState era
epochstate
      _pooldeposits :: Map (KeyHash 'StakePool) Coin
_pooldeposits = (forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> PState era
certPState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState) EpochState era
epochstate
      _keydeposits :: Map (Credential 'Staking) Coin
_keydeposits = (UMap -> Map (Credential 'Staking) Coin
UM.depositMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. DState era -> UMap
dsUnified forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState) EpochState era
epochstate
   in forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$
        forall ann. [Doc ann] -> Doc ann
vsep
          [ forall a. String -> Doc a
ppString String
"==================================="
          , forall a. String -> Doc a
ppString String
"UTxO\n" forall a. Semigroup a => a -> a -> a
<> forall era. EraTx era => Proof era -> MUtxo era -> [Tx era] -> PDoc
pcSmallUTxO forall era. Reflect era => Proof era
reify Map TxIn (TxOut era)
utxo [Tx era]
txs
          , forall a. String -> Doc a
ppString String
"==================================="
          , forall a. String -> Doc a
ppString String
"Stable Pools\n" forall a. Semigroup a => a -> a -> a
<> forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet forall (discriminator :: KeyRole). KeyHash discriminator -> PDoc
pcKeyHash Set (KeyHash 'StakePool)
gsStablePools
          , forall a. String -> Doc a
ppString String
"==================================="
          , forall a. String -> Doc a
ppString String
"Stable Delegators\n" forall a. Semigroup a => a -> a -> a
<> forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet forall (keyrole :: KeyRole). Credential keyrole -> PDoc
pcCredential Set (Credential 'Staking)
gsStableDelegators
          , -- You never know what is NEEDED to debug a failure, and what is a DISTRACTION
            -- These things certainly fall in that category. I leave them commented out so if
            -- they are not a distraction in the current error, they are easy to turn back on.
            -- ppString "===================================",
            -- ppString "PoolDeposits\n" <> ppMap pcKeyHash pcCoin _pooldeposits,
            -- ppString "===================================",
            -- ppString "KeyDeposits\n" <> ppMap pcCredential pcCoin _keydeposits,
            -- ppString "Model KeyDeposits\n" <> ppMap pcCredential pcCoin (mKeyDeposits gsModel),
            -- ppString "Initial Pool Distr\n" <> ppMap pcKeyHash pcIndividualPoolStake gsInitialPoolDistr,
            -- ppString "===================================",
            -- ppString "Initial Pool Params\n" <> ppMap pcKeyHash pcPoolParams gsInitialPoolParams,
            -- ppString "===================================",
            -- ppString "Initial Rewards\n" <> ppMap pcCredential pcCoin gsInitialRewards,
            forall a. String -> Doc a
ppString String
"==================================="
          , forall era. Reflect era => MUtxo era -> [Tx era] -> PDoc
showBlock Map TxIn (TxOut era)
utxo [Tx era]
txs
          , forall a. String -> Doc a
ppString String
"==================================="
          , forall a. String -> Doc a
ppString (forall a. Show a => a -> String
show (forall era. Proof era -> EpochState era -> AdaPots
adaPots forall era. Reflect era => Proof era
reify EpochState era
epochstate))
          , forall a. String -> Doc a
ppString String
"==================================="
          , forall x ann. (x -> Doc ann) -> [x] -> Doc ann
ppList (forall era.
Reflect era =>
Proof era -> MockChainFailure era -> PDoc
ppMockChainFailure forall era. Reflect era => Proof era
reify) (forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList NonEmpty (MockChainFailure era)
pdfs)
          , forall a. String -> Doc a
ppString String
"==================================="
          , forall a. String -> Doc a
ppString String
"Last Slot " forall a. Semigroup a => a -> a -> a
<> forall a. Word64 -> Doc a
ppWord64 Word64
slot
          , forall a. String -> Doc a
ppString String
"Current Slot " forall a. Semigroup a => a -> a -> a
<> forall a. Word64 -> Doc a
ppWord64 Word64
next
          , forall a. String -> Doc a
ppString String
"==================================="
          , forall a. String -> Doc a
ppString String
"Script TxWits\n"
              forall a. Semigroup a => a -> a -> a
<> forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap
                ScriptHash -> PDoc
pcScriptHash
                (forall era. Proof era -> Script era -> PDoc
scriptSummary @era forall era. Reflect era => Proof era
reify)
                (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map ScriptHash (Script era)
gsScripts forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Proof era -> [MockChainFailure era] -> Set ScriptHash
badScripts forall era. Reflect era => Proof era
reify forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList NonEmpty (MockChainFailure era)
pdfs)
          , -- ppString "===================================",
            -- ppString "Real Pool Params\n" <> ppMap pcKeyHash pcPoolParams poolParams,
            forall a. String -> Doc a
ppString String
"====================================="
          , forall a. String -> Doc a
ppString (String
"Protocol Parameters\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (EpochState era
epochstate forall s a. s -> Getting a s a -> a
^. forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL))
          ]

badScripts :: Proof era -> [MockChainFailure era] -> Set.Set ScriptHash
badScripts :: forall era. Proof era -> [MockChainFailure era] -> Set ScriptHash
badScripts Proof era
proof [MockChainFailure era]
xs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' (\Set ScriptHash
s MockChainFailure era
mcf -> forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ScriptHash
s (forall era. Proof era -> MockChainFailure era -> Set ScriptHash
getw Proof era
proof MockChainFailure era
mcf)) forall a. Set a
Set.empty [MockChainFailure era]
xs
  where
    getw :: Proof era -> MockChainFailure era -> Set.Set ScriptHash
    getw :: forall era. Proof era -> MockChainFailure era -> Set ScriptHash
getw
      Proof era
Babbage
      ( MockChainFromLedgersFailure
          ( LedgerFailure
              ( UtxowFailure
                  ( AlonzoInBabbageUtxowPredFailure
                      ( ShelleyInAlonzoUtxowPredFailure
                          (ScriptWitnessNotValidatingUTXOW Set ScriptHash
set)
                        )
                    )
                )
            )
        ) = Set ScriptHash
set
    getw
      Proof era
Alonzo
      ( MockChainFromLedgersFailure
          ( LedgerFailure
              ( UtxowFailure
                  ( ShelleyInAlonzoUtxowPredFailure
                      (ScriptWitnessNotValidatingUTXOW Set ScriptHash
set)
                    )
                )
            )
        ) = Set ScriptHash
set
    getw
      Proof era
Mary
      ( MockChainFromLedgersFailure
          ( LedgerFailure
              ( UtxowFailure
                  (ScriptWitnessNotValidatingUTXOW Set ScriptHash
set)
                )
            )
        ) = Set ScriptHash
set
    getw
      Proof era
Allegra
      ( MockChainFromLedgersFailure
          ( LedgerFailure
              ( UtxowFailure
                  (ScriptWitnessNotValidatingUTXOW Set ScriptHash
set)
                )
            )
        ) = Set ScriptHash
set
    getw Proof era
_ MockChainFailure era
_ = forall a. Set a
Set.empty

showBlock :: forall era. Reflect era => MUtxo era -> [Tx era] -> PDoc
showBlock :: forall era. Reflect era => MUtxo era -> [Tx era] -> PDoc
showBlock MUtxo era
u [Tx era]
txs = forall x ann. (x -> Doc ann) -> [x] -> Doc ann
ppList (Tx era, Int) -> PDoc
pppair (forall a b. [a] -> [b] -> [(a, b)]
zip [Tx era]
txs [Int
0 ..])
  where
    pppair :: (Tx era, Int) -> PDoc
pppair (Tx era
tx, Int
n) =
      let body :: TxBody era
body = forall era. EraTx era => Proof era -> Tx era -> TxBody era
getBody forall era. Reflect era => Proof era
reify Tx era
tx
       in forall ann. [Doc ann] -> Doc ann
vsep
            [ forall a. String -> Doc a
ppString String
"\n###########"
            , forall a. Int -> Doc a
ppInt Int
n
            , forall index. SafeHash index -> PDoc
ppSafeHash (forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
body)
            , forall era.
Reflect era =>
Proof era -> MUtxo era -> TxBody era -> PDoc
smartTxBody forall era. Reflect era => Proof era
reify MUtxo era
u TxBody era
body
            , forall a. String -> Doc a
ppString (forall a. Show a => a -> String
show (forall era. Proof era -> Tx era -> IsValid
isValid' forall era. Reflect era => Proof era
reify Tx era
tx))
            , forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap ScriptHash -> PDoc
pcScriptHash (forall era. Reflect era => Proof era -> Script era -> PDoc
pcScript @era forall era. Reflect era => Proof era
reify) (forall era.
EraTxWits era =>
Proof era -> TxWits era -> Map ScriptHash (Script era)
getScriptWits forall era. Reflect era => Proof era
reify (forall era. EraTx era => Proof era -> Tx era -> TxWits era
getWitnesses forall era. Reflect era => Proof era
reify Tx era
tx))
            , forall a. String -> Doc a
ppString String
"\n"
            ]

shortTxOut :: EraTxOut era => Proof era -> TxOut era -> PDoc
shortTxOut :: forall era. EraTxOut era => Proof era -> TxOut era -> PDoc
shortTxOut Proof era
proof TxOut era
out = case forall era.
Proof era -> TxOut era -> (Addr, Value era, [TxOutField era])
txoutFields Proof era
proof TxOut era
out of
  (Addr Network
_ PaymentCredential
pay StakeReference
_, Value era
_, [TxOutField era]
_) ->
    forall ann. [Doc ann] -> Doc ann
hsep [PDoc
"Out", forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall ann. [Doc ann] -> Doc ann
hsep [PDoc
"Addr", forall (keyrole :: KeyRole). Credential keyrole -> PDoc
pcCredential PaymentCredential
pay], Coin -> PDoc
pcCoin (TxOut era
out forall s a. s -> Getting a s a -> a
^. forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
coinTxOutL)]
  (Addr, Value era, [TxOutField era])
_ -> forall a. HasCallStack => String -> a
error String
"Bootstrap Address in shortTxOut"

smartTxBody :: Reflect era => Proof era -> MUtxo era -> TxBody era -> PDoc
smartTxBody :: forall era.
Reflect era =>
Proof era -> MUtxo era -> TxBody era -> PDoc
smartTxBody Proof era
proof MUtxo era
u TxBody era
txbody = Text -> [(Text, PDoc)] -> PDoc
ppRecord Text
"TxBody" [(Text, PDoc)]
pairs
  where
    fields :: [TxBodyField era]
fields = forall era. Proof era -> TxBody era -> [TxBodyField era]
abstractTxBody Proof era
proof TxBody era
txbody
    pairs :: [(Text, PDoc)]
pairs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a b. (a -> b) -> [a] -> [b]
map TxBodyField era -> [(Text, PDoc)]
help [TxBodyField era]
fields)
    help :: TxBodyField era -> [(Text, PDoc)]
help (Inputs Set TxIn
s) = [(Text
"spend inputs", forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet TxIn -> PDoc
pcIn Set TxIn
s)]
    help (Collateral Set TxIn
s) = [(Text
"coll inputs", forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet TxIn -> PDoc
pcIn Set TxIn
s)]
    help TxBodyField era
x = forall era. Proof era -> TxBodyField era -> [(Text, PDoc)]
pcTxBodyField Proof era
proof TxBodyField era
x
    pcIn :: TxIn -> PDoc
pcIn TxIn
x =
      forall ann. [Doc ann] -> Doc ann
hsep
        [ TxIn -> PDoc
pcTxIn TxIn
x
        , PDoc
" -> "
        , case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TxIn
x MUtxo era
u of Just TxOut era
out -> forall era. EraTxOut era => Proof era -> TxOut era -> PDoc
shortTxOut Proof era
proof TxOut era
out; Maybe (TxOut era)
Nothing -> PDoc
"?"
        ]

-- =====================================================================
-- HasTrace instance of MOCKCHAIN depends on STS(MOCKCHAIN era) instance
-- We show the type family instances here for reference.
{-
instance STS (MOCKCHAIN era)
  where
  type State (MOCKCHAIN era) = MockChainState era
  type Signal (MOCKCHAIN era) = (MockBlock era)
  type Environment (MOCKCHAIN era) = ()
-}
-- ==============================================================

data Gen1 era = Gen1 (Vector (StrictSeq (Tx era), SlotNo)) (GenState era)

instance
  ( STS (MOCKCHAIN era)
  , Reflect era
  ) =>
  HasTrace (MOCKCHAIN era) (Gen1 era)
  where
  type BaseEnv (MOCKCHAIN era) = Globals

  interpretSTS :: forall a.
HasCallStack =>
BaseEnv (MOCKCHAIN era) -> BaseM (MOCKCHAIN era) a -> a
interpretSTS BaseEnv (MOCKCHAIN era)
globals BaseM (MOCKCHAIN era) a
act = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT BaseM (MOCKCHAIN era) a
act BaseEnv (MOCKCHAIN era)
globals

  envGen :: HasCallStack => Gen1 era -> Gen (Environment (MOCKCHAIN era))
envGen Gen1 era
_gstate = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  sigGen :: HasCallStack =>
Gen1 era
-> Environment (MOCKCHAIN era)
-> State (MOCKCHAIN era)
-> Gen (Signal (MOCKCHAIN era))
sigGen (Gen1 Vector (StrictSeq (Tx era), SlotNo)
txss GenState era
gs) () mcs :: State (MOCKCHAIN era)
mcs@(MockChainState NewEpochState era
newepoch NewEpochState era
_ (SlotNo Word64
lastSlot) Int
count) = do
    let NewEpochState EpochNo
epochnum BlocksMade
_ BlocksMade
_ EpochState era
epochstate StrictMaybe PulsingRewUpdate
_ PoolDistr
pooldistr StashedAVVMAddresses era
_ = NewEpochState era
newepoch
    KeyHash 'StakePool
issuerkey <- EpochNo -> Word64 -> Int -> PoolDistr -> Gen (KeyHash 'StakePool)
chooseIssuer EpochNo
epochnum Word64
lastSlot Int
count PoolDistr
pooldistr
    let (StrictSeq (Tx era)
txs, SlotNo
nextSlotNo) = Vector (StrictSeq (Tx era), SlotNo)
txss forall a. Vector a -> Int -> a
! Int
count
    -- Assmble it into a MockBlock
    let mockblock :: MockBlock era
mockblock = forall era.
KeyHash 'StakePool -> SlotNo -> StrictSeq (Tx era) -> MockBlock era
MockBlock KeyHash 'StakePool
issuerkey SlotNo
nextSlotNo StrictSeq (Tx era)
txs
    -- Run the STS Rules for MOCKCHAIN with generated signal

    case forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(MOCKCHAIN era) ((), State (MOCKCHAIN era)
mcs, MockBlock era
mockblock))) of
      Left NonEmpty (MockChainFailure era)
pdfs ->
        let txsl :: [Tx era]
txsl = forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList StrictSeq (Tx era)
txs
         in forall a. String -> a -> a
Debug.trace
              (forall era.
Reflect era =>
Word64
-> SlotNo
-> EpochState era
-> NonEmpty (MockChainFailure era)
-> [Tx era]
-> GenState era
-> String
raiseMockError Word64
lastSlot SlotNo
nextSlotNo EpochState era
epochstate NonEmpty (MockChainFailure era)
pdfs [Tx era]
txsl GenState era
gs)
              ( forall a. HasCallStack => String -> a
error forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines forall a b. (a -> b) -> a -> b
$
                  String
"sigGen in (HasTrace (MOCKCHAIN era) (Gen1 era)) FAILS" forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList NonEmpty (MockChainFailure era)
pdfs)
              )
      Right State (MOCKCHAIN era)
mcs2 -> seq :: forall a b. a -> b -> b
seq State (MOCKCHAIN era)
mcs2 (forall (f :: * -> *) a. Applicative f => a -> f a
pure MockBlock era
mockblock)

  shrinkSignal :: HasCallStack => Signal (MOCKCHAIN era) -> [Signal (MOCKCHAIN era)]
shrinkSignal Signal (MOCKCHAIN era)
_ = []

-- TODO, perhaps we might add shrinking like this. Just a thought. Failure is usually caused by just one Tx
-- in the Block. If the first or last Tx, is independent of the failing Tx, we can probably throw them away.
--  shrinkSignal (MockBlock _ _ xs) | SS.null xs = []
--  shrinkSignal (MockBlock i s xs) = [MockBlock i s (SS.drop 1 xs), MockBlock i s (SS.take (SS.length xs - 1) xs)]

mapProportion :: EpochNo -> Word64 -> Int -> Map.Map k Int -> Gen k
mapProportion :: forall k. EpochNo -> Word64 -> Int -> Map k Int -> Gen k
mapProportion EpochNo
epochnum Word64
lastSlot Int
count Map k Int
m =
  case [(Int, Gen k)]
pairs of
    [] ->
      -- TODO, we need to figure out why this occurs. It always occurs near SlotNo 300, So I am assuming that
      -- sometimes as we move into the 3rd epoch, however stakeDistr is computed becomes empty. This is probably
      -- because there is no action in Test.Cardano.Ledger.Constrained.Trace.Actions for the epoch boundary.
      -- This temporary fix is good enough for now. But the annoying trace message reminds us to fix this.
      forall a. String -> a -> a
Debug.trace
        ( String
"There are no stakepools to choose an issuer from"
            forall a. [a] -> [a] -> [a]
++ String
", epoch="
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show EpochNo
epochnum
            forall a. [a] -> [a] -> [a]
++ String
", last slot="
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Word64
lastSlot
            forall a. [a] -> [a] -> [a]
++ String
", index of Tx="
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
count
        )
        forall a. a
discard
    ((Int, Gen k)
w : [(Int, Gen k)]
_) ->
      if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Int
n, Gen k
_k) -> Int
n forall a. Eq a => a -> a -> Bool
== Int
0) [(Int, Gen k)]
pairs
        then forall a b. (a, b) -> b
snd (Int, Gen k)
w -- All stakepools have zero Stake, choose issuer arbitrarily. possible, but rare.
        else forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int, Gen k)]
pairs
  where
    pairs :: [(Int, Gen k)]
pairs = [(Int
n, forall (f :: * -> *) a. Applicative f => a -> f a
pure k
k) | (k
k, Int
n) <- forall k a. Map k a -> [(k, a)]
Map.toList Map k Int
m]

chooseIssuer :: EpochNo -> Word64 -> Int -> PoolDistr -> Gen (KeyHash 'StakePool)
chooseIssuer :: EpochNo -> Word64 -> Int -> PoolDistr -> Gen (KeyHash 'StakePool)
chooseIssuer EpochNo
epochnum Word64
lastSlot Int
count (PoolDistr Map (KeyHash 'StakePool) IndividualPoolStake
m CompactForm Coin
_) = forall k. EpochNo -> Word64 -> Int -> Map k Int -> Gen k
mapProportion EpochNo
epochnum Word64
lastSlot Int
count (forall {b}. Integral b => IndividualPoolStake -> b
getInt forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (KeyHash 'StakePool) IndividualPoolStake
m)
  where
    getInt :: IndividualPoolStake -> b
getInt IndividualPoolStake
x = forall a b. (RealFrac a, Integral b) => a -> b
floor (IndividualPoolStake -> Rational
individualPoolStake IndividualPoolStake
x forall a. Num a => a -> a -> a
* Rational
1000)

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

-- Generating Traces, and making properties out of a Trace
-- =========================================================================

genTrace ::
  forall era.
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  GenRS era () -> -- An arbitrary 'initialization action', to run before we generate the sequence
  -- use (pure ()) if you don't want or need initialization
  Gen (Trace (MOCKCHAIN era))
genTrace :: forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
numTxInTrace GenSize
gsize GenRS era ()
initialize = do
  (Vector (StrictSeq (Tx era), SlotNo)
vs, GenState era
genstate) <- forall era.
Reflect era =>
Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq Proof era
proof GenSize
gsize Int
numTxInTrace GenRS era ()
initialize
  let initState :: MockChainState era
initState = forall era.
Reflect era =>
Proof era -> GenState era -> MockChainState era
initialMockChainState Proof era
proof GenState era
genstate
  forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState @(MOCKCHAIN era)
    Globals
testGlobals
    (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (t :: * -> *) a. Foldable t => t a -> Int
length Vector (StrictSeq (Tx era), SlotNo)
vs))
    (forall era.
Vector (StrictSeq (Tx era), SlotNo) -> GenState era -> Gen1 era
Gen1 Vector (StrictSeq (Tx era), SlotNo)
vs GenState era
genstate)
    (forall a. a -> Maybe a
Just (\IRC (MOCKCHAIN era)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right MockChainState era
initState))

traceProp ::
  forall era prop.
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  (MockChainState era -> MockChainState era -> prop) ->
  Gen prop
traceProp :: 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
numTxInTrace GenSize
gsize MockChainState era -> MockChainState era -> prop
f = do
  Trace (MOCKCHAIN era)
trace1 <- forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
numTxInTrace GenSize
gsize forall era. Reflect era => GenRS era ()
initStableFields
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (MockChainState era -> MockChainState era -> prop
f (forall s. Trace s -> State s
_traceInitState Trace (MOCKCHAIN era)
trace1) (forall s. Trace s -> State s
lastState Trace (MOCKCHAIN era)
trace1))

forEachEpochTrace ::
  forall era prop.
  ( Testable prop
  , Reflect era
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  (Trace (MOCKCHAIN era) -> prop) ->
  Gen Property
forEachEpochTrace :: forall era prop.
(Testable prop, Reflect era) =>
Proof era
-> Int
-> GenSize
-> (Trace (MOCKCHAIN era) -> prop)
-> Gen Property
forEachEpochTrace Proof era
proof Int
tracelen GenSize
genSize Trace (MOCKCHAIN era) -> prop
f = do
  let newEpoch :: MockChainState era -> MockChainState era -> Bool
newEpoch MockChainState era
tr1 MockChainState era
tr2 = forall era. NewEpochState era -> EpochNo
nesEL (forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
tr1) forall a. Eq a => a -> a -> Bool
/= forall era. NewEpochState era -> EpochNo
nesEL (forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
tr2)
  Trace (MOCKCHAIN era)
trc <- case Proof era
proof of
    Proof era
Conway -> forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Babbage -> forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Alonzo -> forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Allegra -> forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Mary -> forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Shelley -> forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize forall era. Reflect era => GenRS era ()
initStableFields
  let propf :: (Trace (MOCKCHAIN era), Int) -> Property
propf (Trace (MOCKCHAIN era)
subtrace, Int
index) = forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Subtrace of EpochNo " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
index forall a. [a] -> [a] -> [a]
++ String
" fails.") (Trace (MOCKCHAIN era) -> prop
f Trace (MOCKCHAIN era)
subtrace)
  -- The very last sub-trace may not be a full epoch, so we throw it away.
  case forall a. [a] -> [a]
reverse (forall s. (State s -> State s -> Bool) -> Trace s -> [Trace s]
splitTrace forall {era} {era}.
MockChainState era -> MockChainState era -> Bool
newEpoch Trace (MOCKCHAIN era)
trc) of
    [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => prop -> Property
property Bool
True)
    Trace (MOCKCHAIN era)
_ : [Trace (MOCKCHAIN era)]
revSplits -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => [prop] -> Property
conjoin ((Trace (MOCKCHAIN era), Int) -> Property
propf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. [a] -> [a]
reverse [Trace (MOCKCHAIN era)]
revSplits) [Int
0 :: Int ..]))

-- | Check a property on the 'sts' traces.
--
-- Takes an optional generator for initial state of the STS.
forAllTraceFromInitState ::
  forall sts traceGenEnv prop.
  ( HasTrace sts traceGenEnv
  , Testable prop
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  -- | Optional generator of STS initial state
  Maybe (IRC sts -> Gen (Either (NonEmpty (STS.PredicateFailure sts)) (State sts))) ->
  (Trace sts -> prop) ->
  Property
forAllTraceFromInitState :: 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 BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 =
  forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind
    (forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState @sts @traceGenEnv BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0)
    (forall a b. a -> b -> a
const [])

-- =========================================================================
-- Test for just making a trace

-- | We are making 'smoke' tests, testing for smoke rather than fire.
--   Under the assumption that shorter tests have advantages
--   like not getting turned off because the tests take too long. A glaring failure is
--   likely to be caught in 'n' tests, rather than the standard '100'
testPropMax :: Testable prop => Int -> String -> prop -> TestTree
testPropMax :: forall prop. Testable prop => Int -> String -> prop -> TestTree
testPropMax Int
n String
name prop
x = forall a. Testable a => String -> a -> TestTree
testProperty String
name (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n prop
x)

chainTest ::
  forall era.
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  , Eq (StashedAVVMAddresses era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  TestTree
chainTest :: forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof era
proof Int
n GenSize
gsize = forall prop. Testable prop => Int -> String -> prop -> TestTree
testPropMax Int
30 String
message Gen Property
action
  where
    message :: String
message = forall a. Show a => a -> String
show Proof era
proof forall a. [a] -> [a] -> [a]
++ String
" era."
    action :: Gen Property
action = do
      (Vector (StrictSeq (Tx era), SlotNo)
vs, GenState era
genstate) <- forall era.
Reflect era =>
Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq Proof era
proof GenSize
gsize Int
n forall era. Reflect era => GenRS era ()
initStableFields
      let initState :: MockChainState era
initState = forall era.
Reflect era =>
Proof era -> GenState era -> MockChainState era
initialMockChainState Proof era
proof GenState era
genstate
      Trace (MOCKCHAIN era)
trace1 <-
        forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState @(MOCKCHAIN era)
          Globals
testGlobals
          (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (t :: * -> *) a. Foldable t => t a -> Int
length Vector (StrictSeq (Tx era), SlotNo)
vs))
          (forall era.
Vector (StrictSeq (Tx era), SlotNo) -> GenState era -> Gen1 era
Gen1 Vector (StrictSeq (Tx era), SlotNo)
vs GenState era
genstate)
          (forall a. a -> Maybe a
Just (\IRC (MOCKCHAIN era)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right MockChainState era
initState))
      -- Here is where we can add some properties for traces:
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s. Trace s -> State s
_traceInitState Trace (MOCKCHAIN era)
trace1 forall a. (Eq a, Show a) => a -> a -> Property
=== MockChainState era
initState)

testTraces :: Int -> TestTree
testTraces :: Int -> TestTree
testTraces Int
n =
  String -> [TestTree] -> TestTree
testGroup
    String
"MockChainTrace"
    [ forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof BabbageEra
Babbage Int
n forall a. Default a => a
def
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof AlonzoEra
Alonzo Int
n forall a. Default a => a
def
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof MaryEra
Mary Int
n forall a. Default a => a
def
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof AllegraEra
Allegra Int
n forall a. Default a => a
def
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
multiEpochTest Proof BabbageEra
Babbage Int
225 forall a. Default a => a
def
    , forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
multiEpochTest Proof ShelleyEra
Shelley Int
225 forall a. Default a => a
def
    ]

-- | Show that Ada is preserved across multiple Epochs
multiEpochTest ::
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  TestTree
multiEpochTest :: forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
multiEpochTest Proof era
proof Int
numTx GenSize
gsize =
  let gensize :: GenSize
gensize = GenSize
gsize {blocksizeMax :: Integer
blocksizeMax = Integer
4, slotDelta :: (Word64, Word64)
slotDelta = (Word64
6, Word64
12)}
      getEpoch :: MockChainState era -> EpochNo
getEpoch MockChainState era
mockchainstate = forall era. NewEpochState era -> EpochNo
nesEL (forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
mockchainstate)
      propf :: t -> MockChainState era -> Property
propf t
firstSt MockChainState era
lastSt =
        forall a prop. (Show a, Testable prop) => a -> prop -> Property
collect (forall {era}. MockChainState era -> EpochNo
getEpoch MockChainState era
lastSt) (forall t. TotalAda t => t -> Coin
totalAda t
firstSt forall a. (Eq a, Show a) => a -> a -> Property
=== forall t. TotalAda t => t -> Coin
totalAda MockChainState era
lastSt)
   in forall prop. Testable prop => Int -> String -> prop -> TestTree
testPropMax
        Int
30
        (String
"Multi epoch. Ada is preserved. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Proof era
proof forall a. [a] -> [a] -> [a]
++ String
" era. Trace length = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
numTx)
        (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 forall {t} {era}.
(TotalAda t, Reflect era) =>
t -> MockChainState era -> Property
propf)

-- ===========================================================
-- Debugging tools for replaying failures. We store the trace in
-- the IORef TT, and then we can use 'main3' to display what we
-- need to see from the trace.

main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
multiEpochTest Proof ShelleyEra
Shelley Int
200 forall a. Default a => a
def

data TT where
  TT :: Proof era -> [(StrictSeq (Tx era), SlotNo)] -> TT

theVector :: IORef TT
theVector :: IORef TT
theVector = forall a. IO a -> a
unsafePerformIO (forall a. a -> IO (IORef a)
newIORef (forall era. Proof era -> [(StrictSeq (Tx era), SlotNo)] -> TT
TT Proof BabbageEra
Babbage []))

showVector :: (forall era. Proof era -> [Tx era] -> SlotNo -> PDoc) -> IO ()
showVector :: (forall era. Proof era -> [Tx era] -> SlotNo -> PDoc) -> IO ()
showVector forall era. Proof era -> [Tx era] -> SlotNo -> PDoc
pretty = do
  TT
xs <- forall a. IORef a -> IO a
readIORef IORef TT
theVector
  case TT
xs of
    TT Proof era
_ [] -> forall a. Show a => a -> IO ()
print (String
"NONE" :: String)
    TT Proof era
proof [(StrictSeq (Tx era), SlotNo)]
ys -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(StrictSeq (Tx era)
ss, SlotNo
slot) -> forall a. Show a => a -> IO ()
print (forall era. Proof era -> [Tx era] -> SlotNo -> PDoc
pretty Proof era
proof (forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList StrictSeq (Tx era)
ss) SlotNo
slot)) [(StrictSeq (Tx era), SlotNo)]
ys

main3 :: IO ()
main3 :: IO ()
main3 = (forall era. Proof era -> [Tx era] -> SlotNo -> PDoc) -> IO ()
showVector forall era. Proof era -> [Tx era] -> SlotNo -> PDoc
pretty
  where
    pretty :: Proof era -> [Tx era] -> SlotNo -> PDoc
    pretty :: forall era. Proof era -> [Tx era] -> SlotNo -> PDoc
pretty Proof era
Babbage [Tx era]
xs SlotNo
slot =
      forall ann. [Doc ann] -> Doc ann
vsep
        [ SlotNo -> PDoc
pcSlotNo SlotNo
slot
        , forall ann. [Doc ann] -> Doc ann
vsep (forall a b. (a -> b) -> [a] -> [b]
map (forall x ann. (x -> Doc ann) -> [x] -> Doc ann
ppList forall t. PrettyA t => t -> PDoc
prettyA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. BabbageTxBody era -> StrictSeq (TxCert era)
certs' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. AlonzoTx era -> TxBody era
body) [Tx era]
xs)
        ]
    pretty Proof era
p [Tx era]
_ SlotNo
_ = forall a. String -> Doc a
ppString (String
"main3 does not work in era " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Proof era
p)

main2 :: IO ()
main2 :: IO ()
main2 = TestTree -> IO ()
defaultMain (forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof BabbageEra
Babbage Int
100 forall a. Default a => a
def)

-- | display information about stable fields if the only action is to 'initStableFields'
displayStableInfo :: IO ()
displayStableInfo :: IO ()
displayStableInfo = do
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
  ((), GenState BabbageEra
gstate) <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof BabbageEra
proof forall a. Default a => a
def forall era. Reflect era => GenRS era ()
initStableFields
  let mcst :: MockChainState BabbageEra
mcst = forall era.
Reflect era =>
Proof era -> GenState era -> MockChainState era
initialMockChainState Proof BabbageEra
proof GenState BabbageEra
gstate
  let del :: Map (KeyHash 'StakePool) PoolParams
del = forall era. GenState era -> Map (KeyHash 'StakePool) PoolParams
gsInitialPoolParams GenState BabbageEra
gstate
  forall a. Show a => a -> IO ()
print (forall era. Reflect era => MockChainState era -> PDoc
ppMockChainState MockChainState BabbageEra
mcst)
  forall a. Show a => a -> IO ()
print (forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap forall (discriminator :: KeyRole). KeyHash discriminator -> PDoc
pcKeyHash PoolParams -> PDoc
pcPoolParams Map (KeyHash 'StakePool) PoolParams
del)