{-# 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
    forall a b. (a -> b) -> a -> b
$ HasCallStack => PropertyT IO () -> Property
property
    forall a b. (a -> b) -> a -> b
$ do
      Trace UTXOW
tr <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @UTXOW () Word64
500
      forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace UTXOW
tr Word64
200 Word64
50
      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 = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ 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 =
      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
        forall a b. (a -> b) -> a -> b
$ forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UTXOW
tr

    abstractEnv :: UTxOEnv
abstractEnv = Trace UTXOW
tr forall s a. s -> Getting a s a -> a
^. forall s. Lens' (Trace s) (Environment 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 =
  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, forall a. Monoid a => a
mempty)
    (forall k a. Map k a -> [(k, a)]
M.toList 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 forall (m :: * -> *).
MonadError UTxOError m =>
UTxO -> UTxO -> m UTxO
`Concrete.UTxO.union` UTxO
singletonUtxo
       in (UTxO
utxo', 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')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT
      ( 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 = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. [a] -> [a]
reverse forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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) = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a. a -> [a] -> [a]
: [ATxAux ByteString]
acc) 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 = forall t. Decoded t => t -> Hash (BaseType t)
hashDecoded forall a b. (a -> b) -> a -> b
$ forall a. ATxAux a -> Annotated Tx a
Concrete.aTaTx ATxAux ByteString
concreteTxWitness

    txIdMap' :: Map TxId TxId
txIdMap' =
      forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert
        (TxBody -> TxId
Abstract.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 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 -> coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. EncCBOR a => a -> Hash a
serializeCborHash (forall a b. (Show a, ConvertText String b) => a -> b
show TxId
txId :: Text)