{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger (ConwayLedgerExecContext (..)) where

import Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe)
import Cardano.Ledger.Binary (EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (
  EraPParams (..),
  EraTx (..),
  EraTxAuxData (..),
  EraTxBody (..),
  EraTxOut (..),
  EraTxWits (..),
  ScriptHash,
 )
import Cardano.Ledger.Conway.Rules (EnactState)
import Cardano.Ledger.Shelley.LedgerState (LedgerState (..))
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..), UtxoEnv (..))
import Cardano.Ledger.State (EraCertState (..))
import Control.State.Transition.Extended (TRC (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Functor.Identity (Identity)
import qualified Data.Text as T
import GHC.Generics (Generic)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Common (NFData, ToExpr)
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  runFromAgdaFunction,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Constrained.Conway (UtxoExecContext (..))
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Shelley.Utils (runSTS)

data ConwayLedgerExecContext era
  = ConwayLedgerExecContext
  { forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecPolicyHash :: StrictMaybe ScriptHash
  , forall era. ConwayLedgerExecContext era -> EnactState era
clecEnactState :: EnactState era
  , forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecUtxoExecContext :: UtxoExecContext era
  }
  deriving ((forall x.
 ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x)
-> (forall x.
    Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era)
-> Generic (ConwayLedgerExecContext era)
forall x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
forall x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
forall era x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
$cfrom :: forall era x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
from :: forall x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
$cto :: forall era x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
to :: forall x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
Generic)

instance Inject (ConwayLedgerExecContext era) (StrictMaybe ScriptHash) where
  inject :: ConwayLedgerExecContext era -> StrictMaybe ScriptHash
inject = ConwayLedgerExecContext era -> StrictMaybe ScriptHash
forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecPolicyHash

instance Inject (ConwayLedgerExecContext ConwayEra) (EnactState ConwayEra) where
  inject :: ConwayLedgerExecContext ConwayEra -> EnactState ConwayEra
inject = ConwayLedgerExecContext ConwayEra -> EnactState ConwayEra
forall era. ConwayLedgerExecContext era -> EnactState era
clecEnactState

instance
  ( EraPParams era
  , EraTx era
  , NFData (TxWits era)
  , NFData (TxAuxData era)
  , EraCertState era
  ) =>
  NFData (ConwayLedgerExecContext era)

instance
  ( EraTx era
  , ToExpr (Tx era)
  , ToExpr (TxOut era)
  , ToExpr (TxBody era)
  , ToExpr (TxWits era)
  , ToExpr (TxAuxData era)
  , ToExpr (PParamsHKD Identity era)
  , EraCertState era
  , ToExpr (CertState era)
  ) =>
  ToExpr (ConwayLedgerExecContext era)

instance EraPParams era => EncCBOR (ConwayLedgerExecContext era) where
  encCBOR :: ConwayLedgerExecContext era -> Encoding
encCBOR ConwayLedgerExecContext {StrictMaybe ScriptHash
EnactState era
UtxoExecContext era
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecPolicyHash :: StrictMaybe ScriptHash
clecEnactState :: EnactState era
clecUtxoExecContext :: UtxoExecContext era
..} =
    Encode
  ('Closed 'Dense)
  (UtxoExecContext era -> ConwayLedgerExecContext era)
-> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode
   ('Closed 'Dense)
   (UtxoExecContext era -> ConwayLedgerExecContext era)
 -> Encoding)
-> Encode
     ('Closed 'Dense)
     (UtxoExecContext era -> ConwayLedgerExecContext era)
-> Encoding
forall a b. (a -> b) -> a -> b
$
      (StrictMaybe ScriptHash
 -> EnactState era
 -> UtxoExecContext era
 -> ConwayLedgerExecContext era)
-> Encode
     ('Closed 'Dense)
     (StrictMaybe ScriptHash
      -> EnactState era
      -> UtxoExecContext era
      -> ConwayLedgerExecContext era)
forall t. t -> Encode ('Closed 'Dense) t
Rec StrictMaybe ScriptHash
-> EnactState era
-> UtxoExecContext era
-> ConwayLedgerExecContext era
forall era.
StrictMaybe ScriptHash
-> EnactState era
-> UtxoExecContext era
-> ConwayLedgerExecContext era
ConwayLedgerExecContext
        Encode
  ('Closed 'Dense)
  (StrictMaybe ScriptHash
   -> EnactState era
   -> UtxoExecContext era
   -> ConwayLedgerExecContext era)
-> Encode ('Closed 'Dense) (StrictMaybe ScriptHash)
-> Encode
     ('Closed 'Dense)
     (EnactState era
      -> UtxoExecContext era -> ConwayLedgerExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> StrictMaybe ScriptHash
-> Encode ('Closed 'Dense) (StrictMaybe ScriptHash)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To StrictMaybe ScriptHash
clecPolicyHash
        Encode
  ('Closed 'Dense)
  (EnactState era
   -> UtxoExecContext era -> ConwayLedgerExecContext era)
-> Encode ('Closed 'Dense) (EnactState era)
-> Encode
     ('Closed 'Dense)
     (UtxoExecContext era -> ConwayLedgerExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> EnactState era -> Encode ('Closed 'Dense) (EnactState era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EnactState era
clecEnactState

instance ExecSpecRule "LEDGER" ConwayEra where
  type ExecContext "LEDGER" ConwayEra = ConwayLedgerExecContext ConwayEra

  runAgdaRule :: HasCallStack =>
SpecTRC "LEDGER" ConwayEra
-> Either Text (SpecState "LEDGER" ConwayEra)
runAgdaRule = (SpecEnvironment "LEDGER" ConwayEra
 -> SpecState "LEDGER" ConwayEra
 -> SpecSignal "LEDGER" ConwayEra
 -> ComputationResult Text (SpecState "LEDGER" ConwayEra))
-> SpecTRC "LEDGER" ConwayEra
-> Either Text (SpecState "LEDGER" ConwayEra)
forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction LEnv -> LState -> Tx -> T_ComputationResult_44 Text LState
SpecEnvironment "LEDGER" ConwayEra
-> SpecState "LEDGER" ConwayEra
-> SpecSignal "LEDGER" ConwayEra
-> ComputationResult Text (SpecState "LEDGER" ConwayEra)
Agda.ledgerStep

  extraInfo :: HasCallStack =>
Globals
-> ExecContext "LEDGER" ConwayEra
-> TRC (EraRule "LEDGER" ConwayEra)
-> Either
     Text
     (State (EraRule "LEDGER" ConwayEra),
      [Event (EraRule "LEDGER" ConwayEra)])
-> Doc AnsiStyle
extraInfo Globals
globals ConwayLedgerExecContext {StrictMaybe ScriptHash
EnactState ConwayEra
UtxoExecContext ConwayEra
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecPolicyHash :: StrictMaybe ScriptHash
clecEnactState :: EnactState ConwayEra
clecUtxoExecContext :: UtxoExecContext ConwayEra
..} (TRC (LedgerEnv {Maybe EpochNo
PParams ConwayEra
ChainAccountState
TxIx
SlotNo
ledgerSlotNo :: SlotNo
ledgerEpochNo :: Maybe EpochNo
ledgerIx :: TxIx
ledgerPp :: PParams ConwayEra
ledgerAccount :: ChainAccountState
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerAccount :: forall era. LedgerEnv era -> ChainAccountState
..}, LedgerState {CertState ConwayEra
UTxOState ConwayEra
lsUTxOState :: UTxOState ConwayEra
lsCertState :: CertState ConwayEra
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsCertState :: forall era. LedgerState era -> CertState era
..}, Signal (EraRule "LEDGER" ConwayEra)
sig)) Either
  Text
  (State (EraRule "LEDGER" ConwayEra),
   [Event (EraRule "LEDGER" ConwayEra)])
_ =
    forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Globals
-> ExecContext rule era
-> TRC (EraRule rule era)
-> Either
     Text (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @"UTXOW" @ConwayEra
      Globals
globals
      UtxoExecContext ConwayEra
ExecContext "UTXOW" ConwayEra
clecUtxoExecContext
      ((Environment (ConwayUTXOW ConwayEra),
 State (ConwayUTXOW ConwayEra), Signal (ConwayUTXOW ConwayEra))
-> TRC (ConwayUTXOW ConwayEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv ConwayEra
Environment (ConwayUTXOW ConwayEra)
utxoEnv, State (ConwayUTXOW ConwayEra)
UTxOState ConwayEra
lsUTxOState, Signal (EraRule "LEDGER" ConwayEra)
Signal (ConwayUTXOW ConwayEra)
sig))
      Either
  Text
  (State (EraRule "UTXOW" ConwayEra),
   [Event (EraRule "UTXOW" ConwayEra)])
stFinal
    where
      utxoEnv :: UtxoEnv ConwayEra
utxoEnv = SlotNo
-> PParams ConwayEra -> CertState ConwayEra -> UtxoEnv ConwayEra
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
ledgerSlotNo PParams ConwayEra
ledgerPp CertState ConwayEra
lsCertState
      stFinal :: Either
  Text
  (State (EraRule "UTXOW" ConwayEra),
   [Event (EraRule "UTXOW" ConwayEra)])
stFinal =
        (NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra)) -> Text)
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra)))
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
-> Either
     Text
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> Text
T.pack (String -> Text)
-> (NonEmpty (ConwayUtxowPredFailure ConwayEra) -> String)
-> NonEmpty (ConwayUtxowPredFailure ConwayEra)
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (ConwayUtxowPredFailure ConwayEra) -> String
forall a. Show a => a -> String
show) (Either
   (NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra)))
   (State (EraRule "UTXOW" ConwayEra),
    [Event (EraRule "UTXOW" ConwayEra)])
 -> Either
      Text
      (State (EraRule "UTXOW" ConwayEra),
       [Event (EraRule "UTXOW" ConwayEra)]))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra)))
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
-> Either
     Text
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
forall a b. (a -> b) -> a -> b
$
          forall (rule :: Symbol) era.
(BaseM (EraRule rule era) ~ ShelleyBase, STS (EraRule rule era)) =>
Globals
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
runSTS @"UTXOW" @ConwayEra Globals
globals UtxoEnv ConwayEra
Environment (EraRule "UTXOW" ConwayEra)
utxoEnv State (EraRule "UTXOW" ConwayEra)
UTxOState ConwayEra
lsUTxOState Signal (EraRule "UTXOW" ConwayEra)
Signal (EraRule "LEDGER" ConwayEra)
sig