{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Constrained.Trace.Tests where

import Cardano.Ledger.Babbage.TxOut ()
import Cardano.Ledger.BaseTypes (TxIx)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core (EraRule, EraTx (..), EraTxBody (..), Tx)
import Cardano.Ledger.Plutus.Data ()
import Cardano.Ledger.Shelley.LedgerState (LedgerState (..))
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..))
import Control.State.Transition.Extended (STS (..), TRC (..))
import Data.Foldable (toList)
import Lens.Micro ((^.))
import System.IO (hSetEncoding, stdout, utf8)
import Test.Cardano.Ledger.Constrained.Ast (runTarget)
import Test.Cardano.Ledger.Constrained.Classes (TxF (..), TxOutF (..))
import Test.Cardano.Ledger.Constrained.Env (Env (..), emptyEnv)
import Test.Cardano.Ledger.Constrained.Monad (Typed)
import Test.Cardano.Ledger.Constrained.Preds.Repl (goRepl)
import Test.Cardano.Ledger.Constrained.Trace.Actions (feesAction, inputsAction, outputsAction)
import Test.Cardano.Ledger.Constrained.Trace.DrepCertTx (drepTree)
import Test.Cardano.Ledger.Constrained.Trace.SimpleTx (getSTSLedgerEnv, simpleTx)
import Test.Cardano.Ledger.Constrained.Trace.TraceMonad (
  TraceM,
  TraceStep (..),
  beforeAfterTrace,
  fstTriple,
  genLedgerStateEnv,
  getEnv,
  getTarget,
  liftGen,
  liftTyped,
  runTraceM,
  setVar,
  toGen,
 )
import Test.Cardano.Ledger.Constrained.Vars hiding (drepDeposit)
import Test.Cardano.Ledger.Generic.PrettyCore (pcTx)
import Test.Cardano.Ledger.Generic.Proof hiding (LEDGER, lift)
import Test.Cardano.Ledger.Generic.TxGen (applySTSByProof)
import Test.QuickCheck (
  Arbitrary (..),
  Property,
  conjoin,
  counterexample,
  whenFail,
  withMaxSuccess,
  (===),
 )
import Test.Tasty
import Test.Tasty.QuickCheck (testProperty)

-- =======================================================================
-- Test that simpleTx and the 'actions' actually agree with the applySTS

-- | Construct and run one simpleTx, and run it through applySTS
--  Check that the computed LedgerState is the same as the expected LedgerState
--  Computed by using 'inputsAction' , 'outputsAction' , and 'feesAction'
genAndRunSimpleTx :: TraceM ConwayEra Property
genAndRunSimpleTx :: TraceM ConwayEra Property
genAndRunSimpleTx = do
  let proof :: Proof ConwayEra
proof = Proof ConwayEra
Conway
  Env ConwayEra
_ <- Proof ConwayEra -> TraceM ConwayEra (Env ConwayEra)
forall era. Reflect era => Proof era -> TraceM era (Env era)
genLedgerStateEnv Proof ConwayEra
proof

  -- Compute the TRC before we make the Tx, because that adds things to the Env
  TxIx
txIx <- Gen TxIx -> TraceM ConwayEra TxIx
forall a era. Gen a -> TraceM era a
liftGen Gen TxIx
forall a. Arbitrary a => Gen a
arbitrary
  Env ConwayEra
env0 <- TraceM ConwayEra (Env ConwayEra)
forall era. TraceM era (Env era)
getEnv
  (LedgerEnv ConwayEra
lenv, LedgerState ConwayEra
ledgerstate) <- Typed (LedgerEnv ConwayEra, LedgerState ConwayEra)
-> TraceM ConwayEra (LedgerEnv ConwayEra, LedgerState ConwayEra)
forall a era. Typed a -> TraceM era a
liftTyped (Typed (LedgerEnv ConwayEra, LedgerState ConwayEra)
 -> TraceM ConwayEra (LedgerEnv ConwayEra, LedgerState ConwayEra))
-> Typed (LedgerEnv ConwayEra, LedgerState ConwayEra)
-> TraceM ConwayEra (LedgerEnv ConwayEra, LedgerState ConwayEra)
forall a b. (a -> b) -> a -> b
$ Proof ConwayEra
-> TxIx
-> Env ConwayEra
-> Typed (LedgerEnv ConwayEra, LedgerState ConwayEra)
forall era.
Reflect era =>
Proof era
-> TxIx -> Env era -> Typed (LedgerEnv era, LedgerState era)
getSTSLedgerEnv Proof ConwayEra
proof TxIx
txIx Env ConwayEra
env0

  -- Now generate a simpleTx, and store it in the Env
  -- apply the changes we expect this Tx to make, and save the result.
  AlonzoTx ConwayEra
tx <- Proof ConwayEra -> Coin -> TraceM ConwayEra (Tx ConwayEra)
forall era. Reflect era => Proof era -> Coin -> TraceM era (Tx era)
simpleTx Proof ConwayEra
proof (Integer -> Coin
Coin Integer
70000)
  Term ConwayEra (TxF ConwayEra)
-> TxF ConwayEra -> TraceM ConwayEra ()
forall era t. Term era t -> t -> TraceM era ()
setVar Term ConwayEra (TxF ConwayEra)
forall era. Reflect era => Term era (TxF era)
txterm (Proof ConwayEra -> Tx ConwayEra -> TxF ConwayEra
forall era. Proof era -> Tx era -> TxF era
TxF Proof ConwayEra
proof Tx ConwayEra
AlonzoTx ConwayEra
tx)
  let txb :: TxBody ConwayEra
txb = AlonzoTx ConwayEra
tx AlonzoTx ConwayEra
-> Getting
     (TxBody ConwayEra) (AlonzoTx ConwayEra) (TxBody ConwayEra)
-> TxBody ConwayEra
forall s a. s -> Getting a s a -> a
^. (TxBody ConwayEra -> Const (TxBody ConwayEra) (TxBody ConwayEra))
-> Tx ConwayEra -> Const (TxBody ConwayEra) (Tx ConwayEra)
Getting (TxBody ConwayEra) (AlonzoTx ConwayEra) (TxBody ConwayEra)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx ConwayEra) (TxBody ConwayEra)
bodyTxL
      feeCoin :: Coin
feeCoin = TxBody ConwayEra
txb TxBody ConwayEra -> Getting Coin (TxBody ConwayEra) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody ConwayEra) Coin
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody ConwayEra) Coin
feeTxBodyL
  Proof ConwayEra -> Set TxIn -> TraceM ConwayEra ()
forall era. Era era => Proof era -> Set TxIn -> TraceM era ()
inputsAction Proof ConwayEra
proof (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody ConwayEra) (Set TxIn)
inputsTxBodyL)
  Proof ConwayEra
-> TxBody ConwayEra -> [TxOutF ConwayEra] -> TraceM ConwayEra ()
forall era.
Reflect era =>
Proof era -> TxBody era -> [TxOutF era] -> TraceM era ()
outputsAction Proof ConwayEra
proof TxBody ConwayEra
txb ((BabbageTxOut ConwayEra -> TxOutF ConwayEra)
-> [BabbageTxOut ConwayEra] -> [TxOutF ConwayEra]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proof ConwayEra -> TxOut ConwayEra -> TxOutF ConwayEra
forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof ConwayEra
proof) (StrictSeq (BabbageTxOut ConwayEra) -> [BabbageTxOut ConwayEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictSeq (BabbageTxOut ConwayEra))
     (TxBody ConwayEra)
     (StrictSeq (BabbageTxOut ConwayEra))
-> StrictSeq (BabbageTxOut ConwayEra)
forall s a. s -> Getting a s a -> a
^. (StrictSeq (TxOut ConwayEra)
 -> Const
      (StrictSeq (BabbageTxOut ConwayEra)) (StrictSeq (TxOut ConwayEra)))
-> TxBody ConwayEra
-> Const (StrictSeq (BabbageTxOut ConwayEra)) (TxBody ConwayEra)
Getting
  (StrictSeq (BabbageTxOut ConwayEra))
  (TxBody ConwayEra)
  (StrictSeq (BabbageTxOut ConwayEra))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
Lens' (TxBody ConwayEra) (StrictSeq (TxOut ConwayEra))
outputsTxBodyL)))
  Coin -> TraceM ConwayEra ()
forall era. Era era => Coin -> TraceM era ()
feesAction Coin
feeCoin
  LedgerState ConwayEra
expectedLedgerState <- RootTarget
  ConwayEra (LedgerState ConwayEra) (LedgerState ConwayEra)
-> TraceM ConwayEra (LedgerState ConwayEra)
forall era r a. RootTarget era r a -> TraceM era a
getTarget (Proof ConwayEra
-> RootTarget
     ConwayEra (LedgerState ConwayEra) (LedgerState ConwayEra)
forall era.
Reflect era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof ConwayEra
proof)
  Env ConwayEra
env1 <- TraceM ConwayEra (Env ConwayEra)
forall era. TraceM era (Env era)
getEnv
  -- Now compute the env we compute using the STS
  Property -> TraceM ConwayEra Property
forall a. a -> TraceM ConwayEra a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> TraceM ConwayEra Property)
-> Property -> TraceM ConwayEra Property
forall a b. (a -> b) -> a -> b
$ Proof ConwayEra
-> Env ConwayEra
-> State (EraRule "LEDGER" ConwayEra)
-> Environment (EraRule "LEDGER" ConwayEra)
-> State (EraRule "LEDGER" ConwayEra)
-> Signal (EraRule "LEDGER" ConwayEra)
-> Property
forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era, Reflect era,
 Show (State (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era)),
 Eq (State (EraRule "LEDGER" era))) =>
Proof era
-> Env era
-> State (EraRule "LEDGER" era)
-> Environment (EraRule "LEDGER" era)
-> State (EraRule "LEDGER" era)
-> Signal (EraRule "LEDGER" era)
-> Property
ledgerStateEqProp Proof ConwayEra
proof Env ConwayEra
env1 State (EraRule "LEDGER" ConwayEra)
LedgerState ConwayEra
expectedLedgerState LedgerEnv ConwayEra
Environment (EraRule "LEDGER" ConwayEra)
lenv State (EraRule "LEDGER" ConwayEra)
LedgerState ConwayEra
ledgerstate AlonzoTx ConwayEra
Signal (EraRule "LEDGER" ConwayEra)
tx

-- | Create a Property by testing that applying the STS "LEDGER" rule, succeeds and
--   returns the expected LedgerState. If it fails, print out the failures and
--   drop into the Repl, so that users can explore the inputs.
ledgerStateEqProp ::
  ( Signal (EraRule "LEDGER" era) ~ Tx era
  , Reflect era
  , Show (State (EraRule "LEDGER" era))
  , Show (PredicateFailure (EraRule "LEDGER" era))
  , Eq (State (EraRule "LEDGER" era))
  ) =>
  Proof era ->
  Env era ->
  State (EraRule "LEDGER" era) ->
  Environment (EraRule "LEDGER" era) ->
  State (EraRule "LEDGER" era) ->
  Signal (EraRule "LEDGER" era) ->
  Property
ledgerStateEqProp :: forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era, Reflect era,
 Show (State (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era)),
 Eq (State (EraRule "LEDGER" era))) =>
Proof era
-> Env era
-> State (EraRule "LEDGER" era)
-> Environment (EraRule "LEDGER" era)
-> State (EraRule "LEDGER" era)
-> Signal (EraRule "LEDGER" era)
-> Property
ledgerStateEqProp Proof era
proof Env era
env1 State (EraRule "LEDGER" era)
expectedLedgerState Environment (EraRule "LEDGER" era)
ledgerenv State (EraRule "LEDGER" era)
ledgerstate Signal (EraRule "LEDGER" era)
tx =
  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 ((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 (Environment (EraRule "LEDGER" era)
ledgerenv, State (EraRule "LEDGER" era)
ledgerstate, Signal (EraRule "LEDGER" era)
tx)) of
    Right State (EraRule "LEDGER" era)
ledgerState' ->
      State (EraRule "LEDGER" era)
ledgerState' State (EraRule "LEDGER" era)
-> State (EraRule "LEDGER" era) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== {- `ediffEq` -} State (EraRule "LEDGER" era)
expectedLedgerState
    Left NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs ->
      let errsLines :: [String]
errsLines = String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"applySTS fails" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (PredicateFailure (EraRule "LEDGER" era) -> String)
-> [PredicateFailure (EraRule "LEDGER" era)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PredicateFailure (EraRule "LEDGER" era) -> String
forall a. Show a => a -> String
show (NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> [PredicateFailure (EraRule "LEDGER" era)]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs)
       in String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
            ([String] -> String
unlines ([String]
errsLines [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"Tx =", PDoc -> String
forall a. Show a => a -> String
show (Proof era -> Tx era -> PDoc
forall era. Proof era -> Tx era -> PDoc
pcTx Proof era
proof Tx era
Signal (EraRule "LEDGER" era)
tx)]))
            ( IO () -> Bool -> Property
forall prop. Testable prop => IO () -> prop -> Property
whenFail
                (String -> IO ()
putStrLn ([String] -> String
unlines [String]
errsLines) IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Proof era -> Env era -> String -> IO ()
forall era. Proof era -> Env era -> String -> IO ()
goRepl Proof era
proof Env era
env1 String
"")
                Bool
False
            )

main1 :: IO ()
main1 :: IO ()
main1 = do
  Handle -> TextEncoding -> IO ()
hSetEncoding Handle
stdout TextEncoding
utf8
  TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"TraceMain" (Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (TraceM ConwayEra Property -> Gen Property
forall era a. TraceM era a -> Gen a
toGen TraceM ConwayEra Property
genAndRunSimpleTx))

-- =================================================================
-- Show that each step in a trace computes the right LedgerState

runOne ::
  ( Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , Show (PredicateFailure (EraRule "LEDGER" era))
  , Reflect era
  ) =>
  Proof era ->
  TxIx ->
  TraceStep era (Signal (EraRule "LEDGER" era)) ->
  Typed Property
runOne :: forall era.
(Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Show (PredicateFailure (EraRule "LEDGER" era)), Reflect era) =>
Proof era
-> TxIx
-> TraceStep era (Signal (EraRule "LEDGER" era))
-> Typed Property
runOne Proof era
proof TxIx
txIx (TraceStep Env era
beforeEnv Env era
afterEnv Signal (EraRule "LEDGER" era)
tx) = do
  (LedgerEnv era
lenv, LedgerState era
ledgerstate) <- Proof era
-> TxIx -> Env era -> Typed (LedgerEnv era, LedgerState era)
forall era.
Reflect era =>
Proof era
-> TxIx -> Env era -> Typed (LedgerEnv era, LedgerState era)
getSTSLedgerEnv Proof era
proof TxIx
txIx Env era
beforeEnv
  LedgerState era
expectedLedgerState <- Env era
-> RootTarget era (LedgerState era) (LedgerState era)
-> Typed (LedgerState era)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
afterEnv (Proof era -> RootTarget era (LedgerState era) (LedgerState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
proof)
  Property -> Typed Property
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Typed Property) -> Property -> Typed Property
forall a b. (a -> b) -> a -> b
$ Proof era
-> Env era
-> State (EraRule "LEDGER" era)
-> Environment (EraRule "LEDGER" era)
-> State (EraRule "LEDGER" era)
-> Signal (EraRule "LEDGER" era)
-> Property
forall era.
(Signal (EraRule "LEDGER" era) ~ Tx era, Reflect era,
 Show (State (EraRule "LEDGER" era)),
 Show (PredicateFailure (EraRule "LEDGER" era)),
 Eq (State (EraRule "LEDGER" era))) =>
Proof era
-> Env era
-> State (EraRule "LEDGER" era)
-> Environment (EraRule "LEDGER" era)
-> State (EraRule "LEDGER" era)
-> Signal (EraRule "LEDGER" era)
-> Property
ledgerStateEqProp Proof era
proof Env era
afterEnv State (EraRule "LEDGER" era)
LedgerState era
expectedLedgerState LedgerEnv era
Environment (EraRule "LEDGER" era)
lenv State (EraRule "LEDGER" era)
LedgerState era
ledgerstate Signal (EraRule "LEDGER" era)
tx

oneTx :: Reflect era => Proof era -> Int -> TraceM era (Tx era)
oneTx :: forall era. Reflect era => Proof era -> Int -> TraceM era (Tx era)
oneTx Proof era
proof Int
_n = do
  !Tx era
tx <- Proof era -> Coin -> TraceM era (Tx era)
forall era. Reflect era => Proof era -> Coin -> TraceM era (Tx era)
simpleTx Proof era
proof (Integer -> Coin
Coin Integer
70000)
  Term era (TxF era) -> TxF era -> TraceM era ()
forall era t. Term era t -> t -> TraceM era ()
setVar Term era (TxF era)
forall era. Reflect era => Term era (TxF era)
txterm (Proof era -> Tx era -> TxF era
forall era. Proof era -> Tx era -> TxF era
TxF Proof era
proof Tx era
tx)
  let !txb :: TxBody era
txb = Tx era
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL
      !feeCoin :: Coin
feeCoin = TxBody era
txb TxBody era -> Getting Coin (TxBody era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody era) Coin
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody era) Coin
feeTxBodyL
  Proof era -> Set TxIn -> TraceM era ()
forall era. Era era => Proof era -> Set TxIn -> TraceM era ()
inputsAction Proof era
proof (TxBody era
txb TxBody era
-> Getting (Set TxIn) (TxBody era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody era) (Set TxIn)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody era) (Set TxIn)
inputsTxBodyL)
  Proof era -> TxBody era -> [TxOutF era] -> TraceM era ()
forall era.
Reflect era =>
Proof era -> TxBody era -> [TxOutF era] -> TraceM era ()
outputsAction Proof era
proof TxBody era
txb ((TxOut era -> TxOutF era) -> [TxOut era] -> [TxOutF era]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proof era -> TxOut era -> TxOutF era
forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
proof) (StrictSeq (TxOut era) -> [TxOut era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (TxBody era
txb TxBody era
-> Getting
     (StrictSeq (TxOut era)) (TxBody era) (StrictSeq (TxOut era))
-> StrictSeq (TxOut era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (TxOut era)) (TxBody era) (StrictSeq (TxOut era))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL)))
  Coin -> TraceM era ()
forall era. Era era => Coin -> TraceM era ()
feesAction Coin
feeCoin
  Tx era -> TraceM era (Tx era)
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tx era
tx

testTrace ::
  ( Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , Reflect era
  , Show (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  Proof era ->
  Int ->
  TraceM era Property
testTrace :: forall era.
(Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era, Reflect era,
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Int -> TraceM era Property
testTrace Proof era
proof Int
tracelen = do
  !Env era
_ <- Proof era -> TraceM era (Env era)
forall era. Reflect era => Proof era -> TraceM era (Env era)
genLedgerStateEnv Proof era
proof
  !TxIx
txIx <- Gen TxIx -> TraceM era TxIx
forall a era. Gen a -> TraceM era a
liftGen Gen TxIx
forall a. Arbitrary a => Gen a
arbitrary
  ![TraceStep era (Tx era)]
pairs <- Int
-> (Int -> TraceM era (Tx era))
-> TraceM era [TraceStep era (Tx era)]
forall era a.
Int -> (Int -> TraceM era a) -> TraceM era [TraceStep era a]
beforeAfterTrace Int
tracelen (Proof era -> Int -> TraceM era (Tx era)
forall era. Reflect era => Proof era -> Int -> TraceM era (Tx era)
oneTx Proof era
proof)
  [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property)
-> TraceM era [Property] -> TraceM era Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TraceStep era (Tx era) -> TraceM era Property)
-> [TraceStep era (Tx era)] -> TraceM era [Property]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ !TraceStep era (Tx era)
x -> Typed Property -> TraceM era Property
forall a era. Typed a -> TraceM era a
liftTyped (Proof era
-> TxIx
-> TraceStep era (Signal (EraRule "LEDGER" era))
-> Typed Property
forall era.
(Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Show (PredicateFailure (EraRule "LEDGER" era)), Reflect era) =>
Proof era
-> TxIx
-> TraceStep era (Signal (EraRule "LEDGER" era))
-> Typed Property
runOne Proof era
proof TxIx
txIx TraceStep era (Tx era)
TraceStep era (Signal (EraRule "LEDGER" era))
x)) [TraceStep era (Tx era)]
pairs

conwayTrace :: TestTree
conwayTrace :: TestTree
conwayTrace =
  String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (String
"Testing each Tx in a Conway trace of length=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
tracelen String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" passes applySTS.")
    (Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n ((Property, Int, Env ConwayEra) -> Property
forall a b c. (a, b, c) -> a
fstTriple ((Property, Int, Env ConwayEra) -> Property)
-> Gen (Property, Int, Env ConwayEra) -> Gen Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int
-> Env ConwayEra
-> TraceM ConwayEra Property
-> Gen (Property, Int, Env ConwayEra)
forall era a.
Int -> Env era -> TraceM era a -> Gen (a, Int, Env era)
runTraceM Int
0 Env ConwayEra
forall era. Env era
emptyEnv (Proof ConwayEra -> Int -> TraceM ConwayEra Property
forall era.
(Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era, Reflect era,
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
Proof era -> Int -> TraceM era Property
testTrace Proof ConwayEra
Conway Int
tracelen))))
  where
    tracelen :: Int
tracelen = Int
100
    n :: Int
n = Int
10

conwayTxwithDRepCertsTraceTests :: TestTree
conwayTxwithDRepCertsTraceTests :: TestTree
conwayTxwithDRepCertsTraceTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"Tx with DRep Certs trace tests"
    [ TestTree
conwayTrace
    , TestTree
drepTree
    ]

main :: IO ()
main :: IO ()
main = do
  Handle -> TextEncoding -> IO ()
hSetEncoding Handle
stdout TextEncoding
utf8
  TestTree -> IO ()
defaultMain TestTree
conwayTxwithDRepCertsTraceTests