{-# 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