{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Cardano.Ledger.Shelley.Generator.Trace.TxCert (
  CERTS,
  genTxCerts,
)
where

import Cardano.Ledger.BaseTypes (CertIx, Globals, ShelleyBase, TxIx)
import Cardano.Ledger.CertState (
  CertState (..),
  lookupDepositDState,
  lookupDepositVState,
  psStakePoolParams,
 )
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Keys (HasKeyRole (coerceKeyRole), asWitness)
import Cardano.Ledger.Shelley.API (
  AccountState,
  DelplEnv (..),
  Ptr (..),
  ShelleyDELPL,
 )
import Cardano.Ledger.Shelley.Rules (ShelleyDelplEvent, ShelleyDelplPredFailure)
import Cardano.Ledger.Slot (SlotNo (..))
import Control.Monad.Trans.Reader (runReaderT)
import Control.State.Transition (
  BaseM,
  Embed,
  Environment,
  Event,
  PredicateFailure,
  STS (..),
  Signal,
  State,
  TRC (..),
  TransitionRule,
  initialRules,
  judgmentContext,
  trans,
  transitionRules,
  wrapEvent,
  wrapFailed,
 )
import Data.Functor.Identity (runIdentity)
import Data.List (partition)
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes, mapMaybe)
import Data.Proxy (Proxy (..))
import GHC.Generics (Generic)
import GHC.Stack (HasCallStack)
import Test.Cardano.Ledger.Core.KeyPair (KeyPair)
import Test.Cardano.Ledger.Shelley.Constants (Constants (..))
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv (..), KeySpace (..))
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ScriptClass (scriptKeyCombination)
import Test.Cardano.Ledger.Shelley.Generator.TxCert (CertCred (..), genTxCert)
import Test.Cardano.Ledger.Shelley.Utils (epochFromSlotNo, testGlobals)
import Test.Control.State.Transition.Trace (TraceOrder (OldestFirst), lastState, traceSignals)
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (Gen)

-- | This is a non-spec STS used to generate a sequence of certificates with
-- witnesses.
data CERTS era

newtype CertsPredicateFailure era
  = CertsFailure (PredicateFailure (Core.EraRule "DELPL" era))
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (CertsPredicateFailure era) x -> CertsPredicateFailure era
forall era x.
CertsPredicateFailure era -> Rep (CertsPredicateFailure era) x
$cto :: forall era x.
Rep (CertsPredicateFailure era) x -> CertsPredicateFailure era
$cfrom :: forall era x.
CertsPredicateFailure era -> Rep (CertsPredicateFailure era) x
Generic)

newtype CertsEvent era
  = CertsEvent (Event (Core.EraRule "DELPL" era))

deriving stock instance
  Eq (PredicateFailure (Core.EraRule "DELPL" era)) =>
  Eq (CertsPredicateFailure era)

deriving stock instance
  Show (PredicateFailure (Core.EraRule "DELPL" era)) =>
  Show (CertsPredicateFailure era)

instance
  ( Era era
  , Embed (Core.EraRule "DELPL" era) (CERTS era)
  , Environment (Core.EraRule "DELPL" era) ~ DelplEnv era
  , State (Core.EraRule "DELPL" era) ~ CertState era
  , Signal (Core.EraRule "DELPL" era) ~ TxCert era
  ) =>
  STS (CERTS era)
  where
  type Environment (CERTS era) = (SlotNo, TxIx, Core.PParams era, AccountState)
  type State (CERTS era) = (CertState era, CertIx)
  type Signal (CERTS era) = Maybe (TxCert era, CertCred era)
  type PredicateFailure (CERTS era) = CertsPredicateFailure era
  type Event (CERTS era) = CertsEvent era

  type BaseM (CERTS era) = ShelleyBase

  initialRules :: [InitialRule (CERTS era)]
initialRules = []
  transitionRules :: [TransitionRule (CERTS era)]
transitionRules = [forall era.
(Embed (EraRule "DELPL" era) (CERTS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era) =>
TransitionRule (CERTS era)
certsTransition]

certsTransition ::
  forall era.
  ( Embed (Core.EraRule "DELPL" era) (CERTS era)
  , Environment (Core.EraRule "DELPL" era) ~ DelplEnv era
  , State (Core.EraRule "DELPL" era) ~ CertState era
  , Signal (Core.EraRule "DELPL" era) ~ TxCert era
  ) =>
  TransitionRule (CERTS era)
certsTransition :: forall era.
(Embed (EraRule "DELPL" era) (CERTS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era) =>
TransitionRule (CERTS era)
certsTransition = do
  TRC
    ( (SlotNo
slot, TxIx
txIx, PParams era
pp, AccountState
acnt)
      , (CertState era
dpState, CertIx
nextCertIx)
      , Signal (CERTS era)
c
      ) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  case Signal (CERTS era)
c of
    Just (TxCert era
cert, CertCred era
_wits) -> do
      let ptr :: Ptr
ptr = SlotNo -> TxIx -> CertIx -> Ptr
Ptr SlotNo
slot TxIx
txIx CertIx
nextCertIx
      let epoch :: EpochNo
epoch = SlotNo -> EpochNo
epochFromSlotNo SlotNo
slot
      CertState era
dpState' <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(Core.EraRule "DELPL" era) forall a b. (a -> b) -> a -> b
$
          forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo
-> EpochNo -> Ptr -> PParams era -> AccountState -> DelplEnv era
DelplEnv SlotNo
slot EpochNo
epoch Ptr
ptr PParams era
pp AccountState
acnt, CertState era
dpState, TxCert era
cert)

      forall (f :: * -> *) a. Applicative f => a -> f a
pure (CertState era
dpState', forall a. Enum a => a -> a
succ CertIx
nextCertIx)
    Maybe (TxCert era, CertCred era)
Signal (CERTS era)
Nothing ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (CertState era
dpState, CertIx
nextCertIx)

instance
  ( Era era
  , STS (ShelleyDELPL era)
  , PredicateFailure (Core.EraRule "DELPL" era) ~ ShelleyDelplPredFailure era
  , Event (Core.EraRule "DELPL" era) ~ ShelleyDelplEvent era
  ) =>
  Embed (ShelleyDELPL era) (CERTS era)
  where
  wrapFailed :: PredicateFailure (ShelleyDELPL era) -> PredicateFailure (CERTS era)
wrapFailed = forall era.
PredicateFailure (EraRule "DELPL" era) -> CertsPredicateFailure era
CertsFailure
  wrapEvent :: Event (ShelleyDELPL era) -> Event (CERTS era)
wrapEvent = forall era. Event (EraRule "DELPL" era) -> CertsEvent era
CertsEvent

instance
  ( EraGen era
  , Embed (Core.EraRule "DELPL" era) (CERTS era)
  , Environment (Core.EraRule "DELPL" era) ~ DelplEnv era
  , State (Core.EraRule "DELPL" era) ~ CertState era
  , Signal (Core.EraRule "DELPL" era) ~ TxCert era
  , ProtVerAtMost era 8
  ) =>
  QC.HasTrace (CERTS era) (GenEnv era)
  where
  envGen :: HasCallStack => GenEnv era -> Gen (Environment (CERTS era))
envGen GenEnv era
_ = forall a. HasCallStack => String -> a
error String
"HasTrace CERTS - envGen not required"

  sigGen :: HasCallStack =>
GenEnv era
-> Environment (CERTS era)
-> State (CERTS era)
-> Gen (Signal (CERTS era))
sigGen
    ( GenEnv
        KeySpace era
ks
        ScriptSpace era
_scriptspace
        Constants
constants
      )
    (SlotNo
slot, TxIx
_txIx, PParams era
pparams, AccountState
accountState)
    (CertState era
dpState, CertIx
_certIx) =
      forall era.
(EraGen era, ProtVerAtMost era 8) =>
Constants
-> KeySpace era
-> PParams era
-> AccountState
-> CertState era
-> SlotNo
-> Gen (Maybe (TxCert era, CertCred era))
genTxCert
        Constants
constants
        KeySpace era
ks
        PParams era
pparams
        AccountState
accountState
        CertState era
dpState
        SlotNo
slot

  shrinkSignal :: HasCallStack => Signal (CERTS era) -> [Signal (CERTS era)]
shrinkSignal = forall a b. a -> b -> a
const []

  type BaseEnv (CERTS era) = Globals
  interpretSTS :: forall a.
HasCallStack =>
BaseEnv (CERTS era) -> BaseM (CERTS era) a -> a
interpretSTS BaseEnv (CERTS era)
globals BaseM (CERTS era) a
act = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT BaseM (CERTS era) a
act BaseEnv (CERTS era)
globals

-- | Generate certificates and also return the associated witnesses and
-- deposits and refunds required.
genTxCerts ::
  forall era.
  ( EraGen era
  , Embed (Core.EraRule "DELPL" era) (CERTS era)
  , Environment (Core.EraRule "DELPL" era) ~ DelplEnv era
  , State (Core.EraRule "DELPL" era) ~ CertState era
  , Signal (Core.EraRule "DELPL" era) ~ TxCert era
  ) =>
  GenEnv era ->
  Core.PParams era ->
  CertState era ->
  SlotNo ->
  TxIx ->
  AccountState ->
  Gen
    ( [TxCert era]
    , Coin
    , Coin
    , CertState era
    , [KeyPair 'Witness]
    , [(Core.Script era, Core.Script era)]
    )
genTxCerts :: forall era.
(EraGen era, Embed (EraRule "DELPL" era) (CERTS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era) =>
GenEnv era
-> PParams era
-> CertState era
-> SlotNo
-> TxIx
-> AccountState
-> Gen
     ([TxCert era], Coin, Coin, CertState era, [KeyPair 'Witness],
      [(Script era, Script era)])
genTxCerts
  ge :: GenEnv era
ge@( GenEnv
        KeySpace_ {Map (KeyHash 'Staking) (KeyPair 'Staking)
ksIndexedStakingKeys :: forall era.
KeySpace era -> Map (KeyHash 'Staking) (KeyPair 'Staking)
ksIndexedStakingKeys :: Map (KeyHash 'Staking) (KeyPair 'Staking)
ksIndexedStakingKeys}
        ScriptSpace era
_scriptspace
        Constants {Word64
maxCertsPerTx :: Constants -> Word64
maxCertsPerTx :: Word64
maxCertsPerTx}
      )
  PParams era
pp
  certState :: CertState era
certState@CertState {DState era
certDState :: forall era. CertState era -> DState era
certDState :: DState era
certDState, VState era
certVState :: forall era. CertState era -> VState era
certVState :: VState era
certVState, PState era
certPState :: forall era. CertState era -> PState era
certPState :: PState era
certPState}
  SlotNo
slot
  TxIx
txIx
  AccountState
acnt = do
    let env :: (SlotNo, TxIx, PParams era, AccountState)
env = (SlotNo
slot, TxIx
txIx, PParams era
pp, AccountState
acnt)
        st0 :: (CertState era, CertIx)
st0 = (CertState era
certState, forall a. Bounded a => a
minBound)

    Trace (CERTS era)
certsTrace <-
      forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
QC.traceFrom @(CERTS era) Globals
testGlobals Word64
maxCertsPerTx GenEnv era
ge (SlotNo, TxIx, PParams era, AccountState)
env (CertState era, CertIx)
st0

    let certsCreds :: [(TxCert era, CertCred era)]
certsCreds = forall a. [Maybe a] -> [a]
catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst forall a b. (a -> b) -> a -> b
$ Trace (CERTS era)
certsTrace
        (CertState era
lastState_, CertIx
_) = forall s. Trace s -> State s
lastState Trace (CERTS era)
certsTrace
        ([TxCert era]
certs, [CertCred era]
creds) = forall a b. [(a, b)] -> ([a], [b])
unzip [(TxCert era, CertCred era)]
certsCreds
        ([CertCred era]
scriptCreds, [CertCred era]
keyCreds) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition forall {era}. CertCred era -> Bool
isScript [CertCred era]
creds
        keyCreds' :: [CertCred era]
keyCreds' = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([CertCred era]
keyCreds forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map CertCred era -> [CertCred era]
scriptWitnesses [CertCred era]
scriptCreds)

        refunds :: Coin
refunds =
          forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> f (TxCert era)
-> Coin
getTotalRefundsTxCerts
            PParams era
pp
            (forall era. DState era -> Credential 'Staking -> Maybe Coin
lookupDepositDState DState era
certDState)
            (forall era. VState era -> Credential 'DRepRole -> Maybe Coin
lookupDepositVState VState era
certVState)
            [TxCert era]
certs

        deposits :: Coin
deposits = forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (KeyHash 'StakePool -> Bool) -> f (TxCert era) -> Coin
getTotalDepositsTxCerts PParams era
pp (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
certPState) [TxCert era]
certs

        certWits :: [KeyPair 'Witness]
certWits = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall era.
(HasCallStack, Era era, Show (Script era)) =>
CertCred era -> [KeyPair 'Witness]
keyCredAsWitness forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CertCred era]
keyCreds')
        certScripts :: [(Script era, Script era)]
certScripts = forall era.
(HasCallStack, Era era, Show (Script era)) =>
CertCred era -> (Script era, Script era)
extractScriptCred forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CertCred era]
scriptCreds
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( [TxCert era]
certs
      , Coin
deposits
      , Coin
refunds
      , CertState era
lastState_
      , [KeyPair 'Witness]
certWits
      , [(Script era, Script era)]
certScripts
      )
    where
      isScript :: CertCred era -> Bool
isScript (ScriptCred (Script era, Script era)
_) = Bool
True
      isScript CertCred era
_ = Bool
False

      scriptWitnesses :: CertCred era -> [CertCred era]
      scriptWitnesses :: CertCred era -> [CertCred era]
scriptWitnesses (ScriptCred (Script era
_, Script era
stakeScript)) =
        forall era. KeyPair 'Staking -> CertCred era
StakeCred forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KeyPair 'Staking]
witnessHashes''
        where
          witnessHashes :: [KeyHash 'Staking]
witnessHashes = forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era.
ScriptClass era =>
Proxy era -> Script era -> [KeyHash 'Witness]
scriptKeyCombination (forall {k} (t :: k). Proxy t
Proxy @era) Script era
stakeScript
          witnessHashes'' :: [KeyPair 'Staking]
witnessHashes'' = forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe KeyHash 'Staking -> Maybe (KeyPair 'Staking)
lookupWit [KeyHash 'Staking]
witnessHashes
      scriptWitnesses CertCred era
_ = []

      lookupWit :: KeyHash 'Staking -> Maybe (KeyPair 'Staking)
lookupWit = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Map (KeyHash 'Staking) (KeyPair 'Staking)
ksIndexedStakingKeys

extractScriptCred ::
  (HasCallStack, Era era, Show (Core.Script era)) =>
  CertCred era ->
  (Core.Script era, Core.Script era)
extractScriptCred :: forall era.
(HasCallStack, Era era, Show (Script era)) =>
CertCred era -> (Script era, Script era)
extractScriptCred (ScriptCred (Script era, Script era)
c) = (Script era, Script era)
c
extractScriptCred CertCred era
x =
  forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
    String
"extractScriptCred: use only for Script Credentials - "
      forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show CertCred era
x

keyCredAsWitness ::
  (HasCallStack, Era era, Show (Core.Script era)) =>
  CertCred era ->
  [KeyPair 'Witness]
keyCredAsWitness :: forall era.
(HasCallStack, Era era, Show (Script era)) =>
CertCred era -> [KeyPair 'Witness]
keyCredAsWitness (DelegateCred [KeyPair 'GenesisDelegate]
c) = forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a 'Witness
asWitness forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KeyPair 'GenesisDelegate]
c
keyCredAsWitness (CoreKeyCred [GenesisKeyPair MockCrypto]
c) = forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a 'Witness
asWitness forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GenesisKeyPair MockCrypto]
c
keyCredAsWitness (StakeCred KeyPair 'Staking
c) = [forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a 'Witness
asWitness KeyPair 'Staking
c]
keyCredAsWitness (PoolCred KeyPair 'StakePool
c) = [forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a 'Witness
asWitness KeyPair 'StakePool
c]
keyCredAsWitness CertCred era
NoCred = []
keyCredAsWitness CertCred era
x =
  forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
    String
"keyCredAsWitness: use only for Script Credentials - "
      forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show CertCred era
x