{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Test.Cardano.Chain.UTxO.Model (
  tests,
  elaborateAndUpdate,
  elaborateInitialUTxO,
  elaborateTxWitnesses,
  elaborateTxWitsBSWithMap,
) where

import qualified Byron.Spec.Ledger.STS.UTXO as Abstract
import Byron.Spec.Ledger.STS.UTXOW (UTXOW)
import qualified Byron.Spec.Ledger.UTxO as Abstract
import Cardano.Chain.Block (BlockValidationMode (BlockValidation))
import Cardano.Chain.UTxO (
  TxValidationMode (TxValidation),
  updateUTxOTxWitness,
 )
import qualified Cardano.Chain.UTxO as Concrete
import qualified Cardano.Chain.UTxO.UTxO as Concrete.UTxO
import Cardano.Chain.ValidationMode (ValidationMode (..))
import Cardano.Crypto (hashDecoded, serializeCborHash)
import Cardano.Prelude hiding (trace, traceM, traceShow)
import Data.Coerce (coerce)
import qualified Data.Map.Strict as M
import Hedgehog (MonadTest, evalEither, forAll, property)
import Lens.Micro ((^.))
import qualified Test.Cardano.Chain.Elaboration.UTxO as E
import Test.Cardano.Prelude
import Test.Control.State.Transition.Generator (classifyTraceLength, trace)
import Test.Control.State.Transition.Trace (
  Trace,
  TraceOrder (OldestFirst),
  traceEnv,
  traceSignals,
 )
import Test.Options (TSGroup, TSProperty, withTestsTS)

tests :: TSGroup
tests :: TSGroup
tests = $$discoverPropArg

-- | Every abstract trace of transaction that was generated according to the
--   inference rules, after being elaborated must be validated by the concrete
--   UTxO validator.
ts_prop_generatedUTxOChainsAreValidated :: TSProperty
ts_prop_generatedUTxOChainsAreValidated :: TSProperty
ts_prop_generatedUTxOChainsAreValidated =
  TestLimit -> Property -> TSProperty
withTestsTS TestLimit
300
    (Property -> TSProperty) -> Property -> TSProperty
forall a b. (a -> b) -> a -> b
$ HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property
    (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      Trace UTXOW
tr <- Gen (Trace UTXOW) -> PropertyT IO (Trace UTXOW)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (Trace UTXOW) -> PropertyT IO (Trace UTXOW))
-> Gen (Trace UTXOW) -> PropertyT IO (Trace UTXOW)
forall a b. (a -> b) -> a -> b
$ forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @UTXOW () Word64
500
      Trace UTXOW -> Word64 -> Word64 -> PropertyT IO ()
forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace UTXOW
tr Word64
200 Word64
50
      Trace UTXOW -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => Trace UTXOW -> m ()
passConcreteValidation Trace UTXOW
tr

passConcreteValidation :: MonadTest m => Trace UTXOW -> m ()
passConcreteValidation :: forall (m :: * -> *). MonadTest m => Trace UTXOW -> m ()
passConcreteValidation !Trace UTXOW
tr = m (UTxO, Map TxId TxId) -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m (UTxO, Map TxId TxId) -> m ())
-> m (UTxO, Map TxId TxId) -> m ()
forall a b. (a -> b) -> a -> b
$ Either UTxOValidationError (UTxO, Map TxId TxId)
-> m (UTxO, Map TxId TxId)
forall (m :: * -> *) x a.
(MonadTest m, Show x, HasCallStack) =>
Either x a -> m a
evalEither Either UTxOValidationError (UTxO, Map TxId TxId)
res
  where
    res :: Either UTxOValidationError (UTxO, Map TxId TxId)
res =
      ((UTxO, Map TxId TxId)
 -> Tx -> Either UTxOValidationError (UTxO, Map TxId TxId))
-> (UTxO, Map TxId TxId)
-> [Tx]
-> Either UTxOValidationError (UTxO, Map TxId TxId)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (UTxOEnv
-> (UTxO, Map TxId TxId)
-> Tx
-> Either UTxOValidationError (UTxO, Map TxId TxId)
elaborateAndUpdate UTxOEnv
abstractEnv) (UTxO, Map TxId TxId)
initSt
        ([Tx] -> Either UTxOValidationError (UTxO, Map TxId TxId))
-> [Tx] -> Either UTxOValidationError (UTxO, Map TxId TxId)
forall a b. (a -> b) -> a -> b
$ TraceOrder -> Trace UTXOW -> [Signal UTXOW]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UTXOW
tr

    abstractEnv :: UTxOEnv
abstractEnv = Trace UTXOW
tr Trace UTXOW -> Getting UTxOEnv (Trace UTXOW) UTxOEnv -> UTxOEnv
forall s a. s -> Getting a s a -> a
^. Getting UTxOEnv (Trace UTXOW) UTxOEnv
(Environment UTXOW -> Const UTxOEnv (Environment UTXOW))
-> Trace UTXOW -> Const UTxOEnv (Trace UTXOW)
forall s (f :: * -> *).
Functor f =>
(Environment s -> f (Environment s)) -> Trace s -> f (Trace s)
traceEnv

    initSt :: (UTxO, Map TxId TxId)
initSt = UTxO -> (UTxO, Map TxId TxId)
elaborateInitialUTxO (UTxOEnv -> UTxO
Abstract.utxo0 UTxOEnv
abstractEnv)

-- | Create the initial concrete UTxO by elaborating the outputs and updating
--   the map from abstract TxIds to concrete TxIds
elaborateInitialUTxO ::
  Abstract.UTxO ->
  (Concrete.UTxO, Map Abstract.TxId Concrete.TxId)
elaborateInitialUTxO :: UTxO -> (UTxO, Map TxId TxId)
elaborateInitialUTxO UTxO
abstractUtxo =
  ((TxIn, TxOut) -> (UTxO, Map TxId TxId) -> (UTxO, Map TxId TxId))
-> (UTxO, Map TxId TxId)
-> [(TxIn, TxOut)]
-> (UTxO, Map TxId TxId)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    (TxIn, TxOut) -> (UTxO, Map TxId TxId) -> (UTxO, Map TxId TxId)
txOutToUTxO
    (UTxO
Concrete.UTxO.empty, Map TxId TxId
forall a. Monoid a => a
mempty)
    (Map TxIn TxOut -> [(TxIn, TxOut)]
forall k a. Map k a -> [(k, a)]
M.toList (Map TxIn TxOut -> [(TxIn, TxOut)])
-> Map TxIn TxOut -> [(TxIn, TxOut)]
forall a b. (a -> b) -> a -> b
$ UTxO -> Map TxIn TxOut
Abstract.unUTxO UTxO
abstractUtxo)
  where
    txOutToUTxO ::
      (Abstract.TxIn, Abstract.TxOut) ->
      (Concrete.UTxO, Map Abstract.TxId Concrete.TxId) ->
      (Concrete.UTxO, Map Abstract.TxId Concrete.TxId)
    txOutToUTxO :: (TxIn, TxOut) -> (UTxO, Map TxId TxId) -> (UTxO, Map TxId TxId)
txOutToUTxO (Abstract.TxIn TxId
abstractTxId Natural
_, TxOut
abstractTxOut) (UTxO
utxo, Map TxId TxId
txIdMap) =
      let singletonUtxo :: UTxO
singletonUtxo =
            TxOut -> UTxO
Concrete.UTxO.fromTxOut (TxOut -> TxOut
E.elaborateTxOut TxOut
abstractTxOut)
          [(Concrete.TxInUtxo TxId
concreteTxId Word16
_, TxOut
_)] =
            UTxO -> [(TxIn, TxOut)]
Concrete.UTxO.toList UTxO
singletonUtxo
          Right UTxO
utxo' = UTxO
utxo UTxO -> UTxO -> Either UTxOError UTxO
forall (m :: * -> *).
MonadError UTxOError m =>
UTxO -> UTxO -> m UTxO
`Concrete.UTxO.union` UTxO
singletonUtxo
       in (UTxO
utxo', TxId -> TxId -> Map TxId TxId -> Map TxId TxId
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert TxId
abstractTxId TxId
concreteTxId Map TxId TxId
txIdMap)

-- | Elaborate a single transaction, apply it to the UTxO, and update the TxId
--   map with the new concrete TxId
elaborateAndUpdate ::
  Abstract.UTxOEnv ->
  (Concrete.UTxO, Map Abstract.TxId Concrete.TxId) ->
  Abstract.Tx ->
  Either
    Concrete.UTxOValidationError
    (Concrete.UTxO, Map Abstract.TxId Concrete.TxId)
elaborateAndUpdate :: UTxOEnv
-> (UTxO, Map TxId TxId)
-> Tx
-> Either UTxOValidationError (UTxO, Map TxId TxId)
elaborateAndUpdate UTxOEnv
abstractEnv (UTxO
utxo, Map TxId TxId
txIdMap) Tx
abstractTxWits =
  (,Map TxId TxId
txIdMap')
    (UTxO -> (UTxO, Map TxId TxId))
-> Either UTxOValidationError UTxO
-> Either UTxOValidationError (UTxO, Map TxId TxId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ValidationMode (Either UTxOValidationError) UTxO
-> ValidationMode -> Either UTxOValidationError UTxO
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT
      ( Environment
-> UTxO
-> ATxAux ByteString
-> ReaderT ValidationMode (Either UTxOValidationError) UTxO
forall (m :: * -> *).
(MonadError UTxOValidationError m, MonadReader ValidationMode m) =>
Environment -> UTxO -> ATxAux ByteString -> m UTxO
updateUTxOTxWitness
          (UTxOEnv -> Environment
E.elaborateUTxOEnv UTxOEnv
abstractEnv)
          UTxO
utxo
          ATxAux ByteString
concreteTxWitness
      )
      ValidationMode
vMode
  where
    (ATxAux ByteString
concreteTxWitness, Map TxId TxId
txIdMap') =
      Map TxId TxId -> Tx -> (ATxAux ByteString, Map TxId TxId)
elaborateTxWitsBSWithMap Map TxId TxId
txIdMap Tx
abstractTxWits

    vMode :: ValidationMode
vMode =
      ValidationMode
        { blockValidationMode :: BlockValidationMode
blockValidationMode = BlockValidationMode
BlockValidation
        , txValidationMode :: TxValidationMode
txValidationMode = TxValidationMode
TxValidation
        }

elaborateTxWitnesses ::
  Map Abstract.TxId Concrete.TxId ->
  [Abstract.Tx] ->
  ([Concrete.ATxAux ByteString], Map Abstract.TxId Concrete.TxId)
elaborateTxWitnesses :: Map TxId TxId -> [Tx] -> ([ATxAux ByteString], Map TxId TxId)
elaborateTxWitnesses Map TxId TxId
txIdMap = ([ATxAux ByteString] -> [ATxAux ByteString])
-> ([ATxAux ByteString], Map TxId TxId)
-> ([ATxAux ByteString], Map TxId TxId)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first [ATxAux ByteString] -> [ATxAux ByteString]
forall a. [a] -> [a]
reverse (([ATxAux ByteString], Map TxId TxId)
 -> ([ATxAux ByteString], Map TxId TxId))
-> ([Tx] -> ([ATxAux ByteString], Map TxId TxId))
-> [Tx]
-> ([ATxAux ByteString], Map TxId TxId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (([ATxAux ByteString], Map TxId TxId)
 -> Tx -> ([ATxAux ByteString], Map TxId TxId))
-> ([ATxAux ByteString], Map TxId TxId)
-> [Tx]
-> ([ATxAux ByteString], Map TxId TxId)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([ATxAux ByteString], Map TxId TxId)
-> Tx -> ([ATxAux ByteString], Map TxId TxId)
step ([], Map TxId TxId
txIdMap)
  where
    step :: ([ATxAux ByteString], Map TxId TxId)
-> Tx -> ([ATxAux ByteString], Map TxId TxId)
step ([ATxAux ByteString]
acc, Map TxId TxId
m) = (ATxAux ByteString -> [ATxAux ByteString])
-> (ATxAux ByteString, Map TxId TxId)
-> ([ATxAux ByteString], Map TxId TxId)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ATxAux ByteString -> [ATxAux ByteString] -> [ATxAux ByteString]
forall a. a -> [a] -> [a]
: [ATxAux ByteString]
acc) ((ATxAux ByteString, Map TxId TxId)
 -> ([ATxAux ByteString], Map TxId TxId))
-> (Tx -> (ATxAux ByteString, Map TxId TxId))
-> Tx
-> ([ATxAux ByteString], Map TxId TxId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Map TxId TxId -> Tx -> (ATxAux ByteString, Map TxId TxId)
elaborateTxWitsBSWithMap Map TxId TxId
m

elaborateTxWitsBSWithMap ::
  Map Abstract.TxId Concrete.TxId ->
  Abstract.Tx ->
  (Concrete.ATxAux ByteString, Map Abstract.TxId Concrete.TxId)
elaborateTxWitsBSWithMap :: Map TxId TxId -> Tx -> (ATxAux ByteString, Map TxId TxId)
elaborateTxWitsBSWithMap Map TxId TxId
txIdMap Tx
abstractTxWits = (ATxAux ByteString
concreteTxWitness, Map TxId TxId
txIdMap')
  where
    concreteTxWitness :: ATxAux ByteString
concreteTxWitness =
      (TxId -> TxId) -> Tx -> ATxAux ByteString
E.elaborateTxBS
        (Map TxId TxId -> TxId -> TxId
elaborateTxId Map TxId TxId
txIdMap)
        Tx
abstractTxWits

    concreteTxId :: Hash (BaseType (Annotated Tx ByteString))
concreteTxId = Annotated Tx ByteString
-> Hash (BaseType (Annotated Tx ByteString))
forall t. Decoded t => t -> Hash (BaseType t)
hashDecoded (Annotated Tx ByteString
 -> Hash (BaseType (Annotated Tx ByteString)))
-> Annotated Tx ByteString
-> Hash (BaseType (Annotated Tx ByteString))
forall a b. (a -> b) -> a -> b
$ ATxAux ByteString -> Annotated Tx ByteString
forall a. ATxAux a -> Annotated Tx a
Concrete.aTaTx ATxAux ByteString
concreteTxWitness

    txIdMap' :: Map TxId TxId
txIdMap' =
      TxId -> TxId -> Map TxId TxId -> Map TxId TxId
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert
        (TxBody -> TxId
Abstract.txid (TxBody -> TxId) -> TxBody -> TxId
forall a b. (a -> b) -> a -> b
$ Tx -> TxBody
Abstract.body Tx
abstractTxWits)
        TxId
concreteTxId
        Map TxId TxId
txIdMap

-- | This function uses the supplied txIdMap to look up the concrete
-- counterpart to an abstract TxId. If the key is not present in the map,
-- though, it hashes the `show` Text of the TxId, which essentially creates
-- a new TxId outside of the UTxO (but which is unlikely to collide with
-- another TxId.
elaborateTxId ::
  Map Abstract.TxId Concrete.TxId ->
  (Abstract.TxId -> Concrete.TxId)
elaborateTxId :: Map TxId TxId -> TxId -> TxId
elaborateTxId Map TxId TxId
txIdMap TxId
txId =
  case TxId -> Map TxId TxId -> Maybe TxId
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup TxId
txId Map TxId TxId
txIdMap of
    Just TxId
concreteTxId -> TxId
concreteTxId
    Maybe TxId
Nothing -> Hash Text -> TxId
forall a b. Coercible a b => a -> b
coerce (Hash Text -> TxId) -> Hash Text -> TxId
forall a b. (a -> b) -> a -> b
$ Text -> Hash Text
forall a. EncCBOR a => a -> Hash a
serializeCborHash (TxId -> Text
forall a b. (Show a, ConvertText String b) => a -> b
show TxId
txId :: Text)