{-# 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
  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
20 :: Word64

  abstractEnv <- forAll $ STS.envGen @DELEG traceLength

  actions <-
    forAll
      $ Gen.sequential
        (Range.linear 1 (fromIntegral traceLength))
        initialState
        [commandSDELEG concreteRef abstractEnv]

  cleanup concreteRef >> executeSequential initialState 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
          mDCert <- DIEnv -> Set (Epoch, VKeyGenesis) -> Gen (Maybe DCert)
Abstract.dcertGen DIEnv
Environment SDELEG
abstractEnv Set (Epoch, VKeyGenesis)
keyEpochDelegations
          case 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
      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 =
            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)

      liftIO . writeIORef concreteRef $ fromRight concreteState result

      pure 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