{-# 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 (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
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
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  IORef State
concreteRef <- IO (IORef State) -> PropertyT IO (IORef State)
forall a. IO a -> PropertyT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef State) -> PropertyT IO (IORef State))
-> IO (IORef State) -> PropertyT IO (IORef State)
forall a b. (a -> b) -> a -> b
$ State -> IO (IORef State)
forall a. a -> IO (IORef a)
newIORef State
initialConcreteState

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

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

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

    cleanup :: IORef Scheduling.State -> PropertyT IO ()
    cleanup :: IORef State -> PropertyT IO ()
cleanup = IO () -> PropertyT IO ()
forall a. IO a -> PropertyT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> PropertyT IO ())
-> (IORef State -> IO ()) -> IORef State -> PropertyT IO ()
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
. (IORef State -> State -> IO ()) -> State -> IORef State -> IO ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip IORef State -> State -> IO ()
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 = DSState
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
-> StateSDELEG v
forall (v :: * -> *).
DSState
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
-> StateSDELEG v
StateSDELEG DSState
initialAbstractState (DSState -> Either (NonEmpty SdelegPredicateFailure) DSState
forall a b. b -> Either a b
Right DSState
initialAbstractState)
  where
    initialAbstractState :: DSState
initialAbstractState = [(Slot, (VKeyGenesis, VKey))]
-> Set (Epoch, VKeyGenesis) -> DSState
Abstract.DSState [] Set (Epoch, VKeyGenesis)
forall a. Monoid a => a
mempty

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

newtype SignalSDELEG (v :: Type -> Type)
  = SignalSDELEG (STS.Signal SDELEG)
  deriving (Int -> SignalSDELEG v -> ShowS
[SignalSDELEG v] -> ShowS
SignalSDELEG v -> String
(Int -> SignalSDELEG v -> ShowS)
-> (SignalSDELEG v -> String)
-> ([SignalSDELEG v] -> ShowS)
-> Show (SignalSDELEG v)
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
$cshowsPrec :: forall (v :: * -> *). Int -> SignalSDELEG v -> ShowS
showsPrec :: Int -> SignalSDELEG v -> ShowS
$cshow :: forall (v :: * -> *). SignalSDELEG v -> String
show :: SignalSDELEG v -> String
$cshowList :: forall (v :: * -> *). [SignalSDELEG v] -> ShowS
showList :: [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
_ = SignalSDELEG f -> SignalSDELEG g
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 = SignalSDELEG g -> e (SignalSDELEG g)
forall a. a -> e a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SignalSDELEG f -> SignalSDELEG g
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 = (StateSDELEG Symbolic -> Maybe (Gen (SignalSDELEG Symbolic)))
-> (SignalSDELEG Concrete -> m (Either Error State))
-> [Callback SignalSDELEG (Either Error State) StateSDELEG]
-> Command (GenT Identity) m StateSDELEG
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 StateSDELEG Symbolic -> Maybe (Gen (SignalSDELEG Symbolic))
forall (v :: * -> *). StateSDELEG v -> Maybe (Gen (SignalSDELEG v))
gen SignalSDELEG Concrete -> m (Either Error State)
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 =
      Gen (SignalSDELEG v) -> Maybe (Gen (SignalSDELEG v))
forall a. a -> Maybe a
Just
        (Gen (SignalSDELEG v) -> Maybe (Gen (SignalSDELEG v)))
-> Gen (SignalSDELEG v) -> Maybe (Gen (SignalSDELEG v))
forall a b. (a -> b) -> a -> b
$ DCert -> SignalSDELEG v
Signal SDELEG -> SignalSDELEG v
forall (v :: * -> *). Signal SDELEG -> SignalSDELEG v
SignalSDELEG
        (DCert -> SignalSDELEG v)
-> GenT Identity DCert -> Gen (SignalSDELEG v)
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 DIEnv
Environment SDELEG
abstractEnv Set (Epoch, VKeyGenesis)
keyEpochDelegations
          case Maybe DCert
mDCert of
            Maybe DCert
Nothing -> GenT Identity DCert
forall a. GenT Identity a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            Just DCert
dCert -> DCert -> GenT Identity DCert
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DCert -> GenT Identity DCert) -> DCert -> GenT Identity DCert
forall a b. (a -> b) -> a -> b
$! DCert
dCert
      where
        keyEpochDelegations :: Set (Epoch, VKeyGenesis)
keyEpochDelegations = DSState -> Set (Epoch, VKeyGenesis)
Abstract._dSStateKeyEpochDelegations (DSState -> Set (Epoch, VKeyGenesis))
-> DSState -> Set (Epoch, VKeyGenesis)
forall a b. (a -> b) -> a -> b
$ StateSDELEG v -> DSState
forall (v :: * -> *). StateSDELEG v -> DSState
abstractState (StateSDELEG v -> DSState) -> StateSDELEG v -> DSState
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 <- IO State -> m State
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO State -> m State) -> IO State -> m State
forall a b. (a -> b) -> a -> b
$ IORef State -> IO State
forall a. IORef a -> IO a
readIORef IORef State
concreteRef

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

      IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> (State -> IO ()) -> State -> m ()
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
. IORef State -> State -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef State
concreteRef (State -> m ()) -> State -> m ()
forall a b. (a -> b) -> a -> b
$ State -> Either Error State -> State
forall b a. b -> Either a b -> b
fromRight State
concreteState Either Error State
result

      Either Error State -> m (Either Error State)
forall a. a -> m a
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 (v :: * -> *).
 Ord1 v =>
 StateSDELEG v
 -> SignalSDELEG v -> Var (Either Error State) v -> StateSDELEG v)
-> Callback SignalSDELEG (Either Error State) StateSDELEG
forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
(forall (v :: * -> *).
 Ord1 v =>
 state v -> input v -> Var output v -> state v)
-> Callback input output state
Update ((forall (v :: * -> *).
  Ord1 v =>
  StateSDELEG v
  -> SignalSDELEG v -> Var (Either Error State) v -> StateSDELEG v)
 -> Callback SignalSDELEG (Either Error State) StateSDELEG)
-> (forall (v :: * -> *).
    Ord1 v =>
    StateSDELEG v
    -> SignalSDELEG v -> Var (Either Error State) v -> StateSDELEG v)
-> Callback SignalSDELEG (Either Error State) StateSDELEG
forall a b. (a -> b) -> a -> b
$ \StateSDELEG {DSState
abstractState :: forall (v :: * -> *). StateSDELEG v -> DSState
abstractState :: 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 ((Environment SDELEG, State SDELEG, Signal SDELEG) -> TRC SDELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
STS.TRC (Environment SDELEG
abstractEnv, DSState
State SDELEG
abstractState, Signal SDELEG
cert))
           in DSState
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
-> StateSDELEG v
forall (v :: * -> *).
DSState
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
-> StateSDELEG v
StateSDELEG (DSState
-> Either (NonEmpty SdelegPredicateFailure) DSState -> DSState
forall b a. b -> Either a b -> b
fromRight DSState
abstractState Either (NonEmpty SdelegPredicateFailure) DSState
result) ((NonEmpty SdelegPredicateFailure
 -> NonEmpty SdelegPredicateFailure)
-> Either (NonEmpty SdelegPredicateFailure) DSState
-> Either (NonEmpty SdelegPredicateFailure) DSState
forall b c d. (b -> c) -> Either b d -> Either c d
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left NonEmpty SdelegPredicateFailure -> NonEmpty SdelegPredicateFailure
forall a. a -> a
Prelude.id Either (NonEmpty SdelegPredicateFailure) DSState
result)
      , (StateSDELEG Concrete
 -> StateSDELEG Concrete
 -> SignalSDELEG Concrete
 -> Either Error State
 -> Test ())
-> Callback SignalSDELEG (Either Error State) StateSDELEG
forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
(state Concrete
 -> state Concrete -> input Concrete -> output -> Test ())
-> Callback input output state
Ensure ((StateSDELEG Concrete
  -> StateSDELEG Concrete
  -> SignalSDELEG Concrete
  -> Either Error State
  -> Test ())
 -> Callback SignalSDELEG (Either Error State) StateSDELEG)
-> (StateSDELEG Concrete
    -> StateSDELEG Concrete
    -> SignalSDELEG Concrete
    -> Either Error State
    -> Test ())
-> Callback SignalSDELEG (Either Error State) StateSDELEG
forall a b. (a -> b) -> a -> b
$ \StateSDELEG Concrete
_ StateSDELEG {Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult :: forall (v :: * -> *).
StateSDELEG v
-> Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult :: Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
lastAbstractResult} SignalSDELEG Concrete
_ Either Error State
result -> do
          Either (NonEmpty SdelegPredicateFailure) DSState -> Test ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
Either (NonEmpty SdelegPredicateFailure) DSState
lastAbstractResult
          Either Error State -> Test ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow Either Error State
result
          Either (NonEmpty SdelegPredicateFailure) DSState -> Bool
forall a b. Either a b -> Bool
isRight Either (NonEmpty (PredicateFailure SDELEG)) (State SDELEG)
Either (NonEmpty SdelegPredicateFailure) DSState
lastAbstractResult Bool -> Bool -> Test ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== Either Error State -> Bool
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 -> GroupName
String -> PropertyName
GroupName -> [(PropertyName, Property)] -> Group
discover