{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Chain.Delegation.Model (
  tests,
)
where

import Byron.Spec.Ledger.Delegation (DELEG, SDELEG)
import qualified Byron.Spec.Ledger.Delegation as Abstract
import qualified Cardano.Chain.Delegation.Validation.Scheduling as Scheduling
import Cardano.Prelude
import Control.Arrow (left)
import qualified Control.State.Transition as STS
import Data.Coerce
import Data.IORef
import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import qualified Test.Cardano.Chain.Elaboration.Delegation as E
import qualified Test.Cardano.Crypto.Dummy as Dummy
import qualified Test.Control.State.Transition.Generator as STS
import Prelude (id)

--------------------------------------------------------------------------------
-- SDELEG Property
--------------------------------------------------------------------------------

prop_commandSDELEG :: Property
prop_commandSDELEG :: Property
prop_commandSDELEG = TestLimit -> Property -> Property
withTests TestLimit
25 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  IORef State
concreteRef <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef State
initialConcreteState

  let traceLength :: Word64
traceLength = Word64
20 :: Word64

  DIEnv
abstractEnv <- 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 => Word64 -> Gen (Environment s)
STS.envGen @DELEG Word64
traceLength

  Sequential (PropertyT IO) StateSDELEG
actions <-
    forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll
      forall a b. (a -> b) -> a -> b
$ forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> (forall (v :: * -> *). state v)
-> [Command gen m state]
-> gen (Sequential m state)
Gen.sequential
        (forall a. Integral a => a -> a -> Range a
Range.linear Int
1 (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
traceLength))
        forall (v :: * -> *). StateSDELEG v
initialState
        [forall (m :: * -> *).
MonadIO m =>
IORef State
-> Environment SDELEG -> Command (GenT Identity) m StateSDELEG
commandSDELEG IORef State
concreteRef DIEnv
abstractEnv]

  IORef State -> PropertyT IO ()
cleanup IORef State
concreteRef forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, MonadCatch m, HasCallStack) =>
(forall (v :: * -> *). state v) -> Sequential m state -> m ()
executeSequential forall (v :: * -> *). StateSDELEG v
initialState Sequential (PropertyT IO) StateSDELEG
actions
  where
    initialConcreteState :: State
initialConcreteState = Seq ScheduledDelegation -> Set (EpochNumber, KeyHash) -> State
Scheduling.State forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty

    cleanup :: IORef Scheduling.State -> PropertyT IO ()
    cleanup :: IORef State -> PropertyT IO ()
cleanup = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. IORef a -> a -> IO ()
writeIORef State
initialConcreteState

--------------------------------------------------------------------------------
-- SDELEG State
--------------------------------------------------------------------------------

data StateSDELEG (v :: Type -> Type) = StateSDELEG
  { forall (v :: * -> *). StateSDELEG v -> DSState
abstractState :: Abstract.DSState
  , forall (v :: * -> *).
StateSDELEG v
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult :: Either (NonEmpty (STS.PredicateFailure SDELEG)) (STS.State SDELEG)
  }

initialState :: StateSDELEG v
initialState :: forall (v :: * -> *). StateSDELEG v
initialState = forall (v :: * -> *).
DSState
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
-> StateSDELEG v
StateSDELEG DSState
initialAbstractState (forall a b. b -> Either a b
Right DSState
initialAbstractState)
  where
    initialAbstractState :: DSState
initialAbstractState = [(Slot, (VKeyGenesis, VKey))]
-> Set (Epoch, VKeyGenesis) -> DSState
Abstract.DSState [] forall a. Monoid a => a
mempty

--------------------------------------------------------------------------------
-- SDELEG Signal
--------------------------------------------------------------------------------

newtype SignalSDELEG (v :: Type -> Type)
  = SignalSDELEG (STS.Signal SDELEG)
  deriving (Int -> SignalSDELEG v -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (v :: * -> *). Int -> SignalSDELEG v -> ShowS
forall (v :: * -> *). [SignalSDELEG v] -> ShowS
forall (v :: * -> *). SignalSDELEG v -> String
showList :: [SignalSDELEG v] -> ShowS
$cshowList :: forall (v :: * -> *). [SignalSDELEG v] -> ShowS
show :: SignalSDELEG v -> String
$cshow :: forall (v :: * -> *). SignalSDELEG v -> String
showsPrec :: Int -> SignalSDELEG v -> ShowS
$cshowsPrec :: forall (v :: * -> *). Int -> SignalSDELEG v -> ShowS
Show)

instance FunctorB SignalSDELEG where
  bmap :: forall (f :: * -> *) (g :: * -> *).
(forall a. f a -> g a) -> SignalSDELEG f -> SignalSDELEG g
bmap forall a. f a -> g a
_ = coerce :: forall a b. Coercible a b => a -> b
coerce

instance TraversableB SignalSDELEG where
  btraverse :: forall (e :: * -> *) (f :: * -> *) (g :: * -> *).
Applicative e =>
(forall a. f a -> e (g a)) -> SignalSDELEG f -> e (SignalSDELEG g)
btraverse forall a. f a -> e (g a)
_ SignalSDELEG f
s = forall (f :: * -> *) a. Applicative f => a -> f a
pure (coerce :: forall a b. Coercible a b => a -> b
coerce SignalSDELEG f
s)

--------------------------------------------------------------------------------
-- SDELEG Command
--------------------------------------------------------------------------------

-- TODO: Change dcertGen to use 'MonadGen'
commandSDELEG ::
  forall m.
  MonadIO m =>
  IORef Scheduling.State ->
  STS.Environment SDELEG ->
  Command Gen m StateSDELEG
commandSDELEG :: forall (m :: * -> *).
MonadIO m =>
IORef State
-> Environment SDELEG -> Command (GenT Identity) m StateSDELEG
commandSDELEG IORef State
concreteRef Environment SDELEG
abstractEnv = forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *)
       (input :: (* -> *) -> *) output.
(TraversableB input, Show (input Symbolic), Show output,
 Typeable output) =>
(state Symbolic -> Maybe (gen (input Symbolic)))
-> (input Concrete -> m output)
-> [Callback input output state]
-> Command gen m state
Command forall (v :: * -> *). StateSDELEG v -> Maybe (Gen (SignalSDELEG v))
gen forall (v :: * -> *). SignalSDELEG v -> m (Either Error State)
execute [Callback SignalSDELEG (Either Error State) StateSDELEG]
callbacks
  where
    gen :: StateSDELEG v -> Maybe (Gen (SignalSDELEG v))
    gen :: forall (v :: * -> *). StateSDELEG v -> Maybe (Gen (SignalSDELEG v))
gen StateSDELEG v
st =
      forall a. a -> Maybe a
Just
        forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *). Signal SDELEG -> SignalSDELEG v
SignalSDELEG
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          Maybe DCert
mDCert <- DIEnv -> Set (Epoch, VKeyGenesis) -> Gen (Maybe DCert)
Abstract.dcertGen Environment SDELEG
abstractEnv Set (Epoch, VKeyGenesis)
keyEpochDelegations
          case Maybe DCert
mDCert of
            Maybe DCert
Nothing -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
            Just DCert
dCert -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! DCert
dCert
      where
        keyEpochDelegations :: Set (Epoch, VKeyGenesis)
keyEpochDelegations = DSState -> Set (Epoch, VKeyGenesis)
Abstract._dSStateKeyEpochDelegations forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *). StateSDELEG v -> DSState
abstractState forall a b. (a -> b) -> a -> b
$ StateSDELEG v
st

    execute ::
      SignalSDELEG v ->
      m (Either Scheduling.Error Scheduling.State)
    execute :: forall (v :: * -> *). SignalSDELEG v -> m (Either Error State)
execute (SignalSDELEG Signal SDELEG
cert) = do
      State
concreteState <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef State
concreteRef

      let result :: Either Scheduling.Error Scheduling.State
          result :: Either Error State
result =
            forall (m :: * -> *).
MonadError Error m =>
Environment -> State -> ACertificate ByteString -> m State
Scheduling.scheduleCertificate
              (DIEnv -> Environment
E.elaborateDSEnv Environment SDELEG
abstractEnv)
              State
concreteState
              (ProtocolMagicId -> DCert -> ACertificate ByteString
E.elaborateDCertAnnotated ProtocolMagicId
Dummy.protocolMagicId Signal SDELEG
cert)

      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. IORef a -> a -> IO ()
writeIORef IORef State
concreteRef forall a b. (a -> b) -> a -> b
$ forall b a. b -> Either a b -> b
fromRight State
concreteState Either Error State
result

      forall (f :: * -> *) a. Applicative f => a -> f a
pure Either Error State
result

    callbacks ::
      [ Callback
          SignalSDELEG
          (Either Scheduling.Error Scheduling.State)
          StateSDELEG
      ]
    callbacks :: [Callback SignalSDELEG (Either Error State) StateSDELEG]
callbacks =
      [ forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
(forall (v :: * -> *).
 Ord1 v =>
 state v -> input v -> Var output v -> state v)
-> Callback input output state
Update forall a b. (a -> b) -> a -> b
$ \StateSDELEG {DSState
abstractState :: DSState
abstractState :: forall (v :: * -> *). StateSDELEG v -> DSState
abstractState} (SignalSDELEG Signal SDELEG
cert) Var (Either Error State) v
_ ->
          let result :: Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
result =
                forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, BaseM s ~ Identity) =>
RuleContext rtype s
-> Either (NonEmpty (PredicateFailure s)) (State s)
STS.applySTS @SDELEG (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
STS.TRC (Environment SDELEG
abstractEnv, DSState
abstractState, Signal SDELEG
cert))
           in forall (v :: * -> *).
DSState
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
-> StateSDELEG v
StateSDELEG (forall b a. b -> Either a b -> b
fromRight DSState
abstractState Either (NonEmpty SdelegPredicateFailure) DSState
result) (forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left forall a. a -> a
Prelude.id Either (NonEmpty SdelegPredicateFailure) DSState
result)
      , forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
(state Concrete
 -> state Concrete -> input Concrete -> output -> Test ())
-> Callback input output state
Ensure forall a b. (a -> b) -> a -> b
$ \StateSDELEG Concrete
_ StateSDELEG {Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult :: Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult :: forall (v :: * -> *).
StateSDELEG v
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult} SignalSDELEG Concrete
_ Either Error State
result -> do
          forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult
          forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow Either Error State
result
          forall a b. Either a b -> Bool
isRight Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall a b. Either a b -> Bool
isRight Either Error State
result
      ]

--------------------------------------------------------------------------------
-- Main Test Export
--------------------------------------------------------------------------------

tests :: Group
tests :: Group
tests = $$String
[(PropertyName, Property)]
Property
String -> PropertyName
String -> GroupName
GroupName -> [(PropertyName, Property)] -> Group
discover