{-# 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)
genAndRunSimpleTx :: TraceM (ConwayEra StandardCrypto) Property
genAndRunSimpleTx :: TraceM (ConwayEra StandardCrypto) Property
genAndRunSimpleTx = do
let proof :: Proof (ConwayEra StandardCrypto)
proof = Proof (ConwayEra StandardCrypto)
Conway
Env (ConwayEra StandardCrypto)
_ <- forall era. Reflect era => Proof era -> TraceM era (Env era)
genLedgerStateEnv Proof (ConwayEra StandardCrypto)
proof
TxIx
txIx <- forall a era. Gen a -> TraceM era a
liftGen forall a. Arbitrary a => Gen a
arbitrary
Env (ConwayEra StandardCrypto)
env0 <- forall era. TraceM era (Env era)
getEnv
(LedgerEnv (ConwayEra StandardCrypto)
lenv, LedgerState (ConwayEra StandardCrypto)
ledgerstate) <- forall a era. Typed a -> TraceM era a
liftTyped forall a b. (a -> b) -> a -> b
$ forall era.
Reflect era =>
Proof era
-> TxIx -> Env era -> Typed (LedgerEnv era, LedgerState era)
getSTSLedgerEnv Proof (ConwayEra StandardCrypto)
proof TxIx
txIx Env (ConwayEra StandardCrypto)
env0
AlonzoTx (ConwayEra StandardCrypto)
tx <- forall era. Reflect era => Proof era -> Coin -> TraceM era (Tx era)
simpleTx Proof (ConwayEra StandardCrypto)
proof (Integer -> Coin
Coin Integer
70000)
forall era t. Term era t -> t -> TraceM era ()
setVar forall era. Reflect era => Term era (TxF era)
txterm (forall era. Proof era -> Tx era -> TxF era
TxF Proof (ConwayEra StandardCrypto)
proof AlonzoTx (ConwayEra StandardCrypto)
tx)
let txb :: TxBody (ConwayEra StandardCrypto)
txb = AlonzoTx (ConwayEra StandardCrypto)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
feeCoin :: Coin
feeCoin = TxBody (ConwayEra StandardCrypto)
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL
forall era.
Era era =>
Proof era -> Set (TxIn (EraCrypto era)) -> TraceM era ()
inputsAction Proof (ConwayEra StandardCrypto)
proof (TxBody (ConwayEra StandardCrypto)
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
inputsTxBodyL)
forall era.
Reflect era =>
Proof era -> TxBody era -> [TxOutF era] -> TraceM era ()
outputsAction Proof (ConwayEra StandardCrypto)
proof TxBody (ConwayEra StandardCrypto)
txb (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof (ConwayEra StandardCrypto)
proof) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (TxBody (ConwayEra StandardCrypto)
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL)))
forall era. Era era => Coin -> TraceM era ()
feesAction Coin
feeCoin
LedgerState (ConwayEra StandardCrypto)
expectedLedgerState <- forall era r a. RootTarget era r a -> TraceM era a
getTarget (forall era.
EraGov era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof (ConwayEra StandardCrypto)
proof)
Env (ConwayEra StandardCrypto)
env1 <- forall era. TraceM era (Env era)
getEnv
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 StandardCrypto)
proof Env (ConwayEra StandardCrypto)
env1 LedgerState (ConwayEra StandardCrypto)
expectedLedgerState LedgerEnv (ConwayEra StandardCrypto)
lenv LedgerState (ConwayEra StandardCrypto)
ledgerstate AlonzoTx (ConwayEra StandardCrypto)
tx
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 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 (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' forall a. (Eq a, Show a) => a -> a -> Property
=== State (EraRule "LEDGER" era)
expectedLedgerState
Left NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs ->
let errsLines :: [String]
errsLines = String
"" forall a. a -> [a] -> [a]
: String
"applySTS 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]
toList NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs)
in forall prop. Testable prop => String -> prop -> Property
counterexample
([String] -> String
unlines ([String]
errsLines forall a. [a] -> [a] -> [a]
++ [String
"Tx =", forall a. Show a => a -> String
show (forall era. Proof era -> Tx era -> PDoc
pcTx Proof era
proof Signal (EraRule "LEDGER" era)
tx)]))
( forall prop. Testable prop => IO () -> prop -> Property
whenFail
(String -> IO ()
putStrLn ([String] -> String
unlines [String]
errsLines) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 forall a b. (a -> b) -> a -> b
$ forall a. Testable a => String -> a -> TestTree
testProperty String
"TraceMain" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall era a. TraceM era a -> Gen a
toGen TraceM (ConwayEra StandardCrypto) Property
genAndRunSimpleTx))
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) <- 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 <- forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
afterEnv (forall era.
EraGov era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
proof)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 LedgerState era
expectedLedgerState LedgerEnv era
lenv 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 <- forall era. Reflect era => Proof era -> Coin -> TraceM era (Tx era)
simpleTx Proof era
proof (Integer -> Coin
Coin Integer
70000)
forall era t. Term era t -> t -> TraceM era ()
setVar forall era. Reflect era => Term era (TxF era)
txterm (forall era. Proof era -> Tx era -> TxF era
TxF Proof era
proof Tx era
tx)
let !txb :: TxBody era
txb = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
!feeCoin :: Coin
feeCoin = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL
forall era.
Era era =>
Proof era -> Set (TxIn (EraCrypto era)) -> TraceM era ()
inputsAction Proof era
proof (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
inputsTxBodyL)
forall era.
Reflect era =>
Proof era -> TxBody era -> [TxOutF era] -> TraceM era ()
outputsAction Proof era
proof TxBody era
txb (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
proof) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL)))
forall era. Era era => Coin -> TraceM era ()
feesAction Coin
feeCoin
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
_ <- forall era. Reflect era => Proof era -> TraceM era (Env era)
genLedgerStateEnv Proof era
proof
!TxIx
txIx <- forall a era. Gen a -> TraceM era a
liftGen forall a. Arbitrary a => Gen a
arbitrary
![TraceStep era (Tx era)]
pairs <- forall era a.
Int -> (Int -> TraceM era a) -> TraceM era [TraceStep era a]
beforeAfterTrace Int
tracelen (forall era. Reflect era => Proof era -> Int -> TraceM era (Tx era)
oneTx Proof era
proof)
forall prop. Testable prop => [prop] -> Property
conjoin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ !TraceStep era (Tx era)
x -> forall a era. Typed a -> TraceM era a
liftTyped (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)
x)) [TraceStep era (Tx era)]
pairs
conwayTrace :: TestTree
conwayTrace :: TestTree
conwayTrace =
forall a. Testable a => String -> a -> TestTree
testProperty
(String
"Testing each Tx in a Conway trace of length=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
tracelen forall a. [a] -> [a] -> [a]
++ String
" passes applySTS.")
(forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (forall a b c. (a, b, c) -> a
fstTriple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall era a.
Int -> Env era -> TraceM era a -> Gen (a, Int, Env era)
runTraceM Int
0 forall era. Env era
emptyEnv (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 StandardCrypto)
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