{-# 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 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

  -- Compute the TRC before we make the Tx, because that adds things to the Env
  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

  -- 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 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
  -- Now compute the env we compute using the STS
  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

-- | 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 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
=== {- `ediffEq` -} 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))

-- =================================================================
-- 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) <- 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