{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Test.Cardano.Ledger.Conformance.Imp (spec) where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Core
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rules (UtxoEnv (..), ledgerSlotNoL)
import Cardano.Ledger.TxIn (TxId)
import Control.State.Transition
import Data.Bifunctor (Bifunctor (..))
import Data.List.NonEmpty
import Data.Text qualified as T
import Lens.Micro
import MAlonzo.Code.Ledger.Foreign.API qualified as Agda
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (ConwayLedgerExecContext (..))
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core
import Test.Cardano.Ledger.Constrained.Conway
import Test.Cardano.Ledger.Conway.Imp.BbodySpec qualified as Bbody
import Test.Cardano.Ledger.Conway.Imp.CertsSpec qualified as Certs
import Test.Cardano.Ledger.Conway.Imp.DelegSpec qualified as Deleg
import Test.Cardano.Ledger.Conway.Imp.EnactSpec qualified as Enact
import Test.Cardano.Ledger.Conway.Imp.EpochSpec qualified as Epoch
import Test.Cardano.Ledger.Conway.Imp.GovCertSpec qualified as GovCert
import Test.Cardano.Ledger.Conway.Imp.GovSpec qualified as Gov
import Test.Cardano.Ledger.Conway.Imp.LedgerSpec qualified as Ledger
import Test.Cardano.Ledger.Conway.Imp.RatifySpec qualified as Ratify
import Test.Cardano.Ledger.Conway.Imp.UtxoSpec qualified as Utxo
import Test.Cardano.Ledger.Conway.Imp.UtxosSpec qualified as Utxos
import Test.Cardano.Ledger.Conway.ImpTest
import Test.Cardano.Ledger.Imp.Common hiding (Args)
import UnliftIO (evaluateDeep)

submitTxConformanceHook ::
  forall era t.
  ( ConwayEraImp era
  , ExecSpecRule "LEDGER" era
  , ExecContext "LEDGER" era ~ ConwayLedgerExecContext era
  , SpecTranslate (ExecContext "LEDGER" era) (TxWits era)
  , HasCallStack
  , SpecRep (TxWits era) ~ Agda.TxWitnesses
  , SpecRep (TxBody era) ~ Agda.TxBody
  , SpecTranslate TxId (TxBody era)
  , SpecTranslate (ConwayLedgerExecContext era) (Tx era)
  , ToExpr (SpecRep (Tx era))
  , SpecNormalize (SpecState "LEDGER" era)
  , Eq (SpecState "LEDGER" era)
  ) =>
  Globals ->
  TRC (EraRule "LEDGER" era) ->
  Either
    (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
    (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
  ImpM t ()
submitTxConformanceHook :: forall era t.
(ConwayEraImp era, ExecSpecRule "LEDGER" era,
 ExecContext "LEDGER" era ~ ConwayLedgerExecContext era,
 SpecTranslate (ExecContext "LEDGER" era) (TxWits era),
 HasCallStack, SpecRep (TxWits era) ~ TxWitnesses,
 SpecRep (TxBody era) ~ TxBody, SpecTranslate TxId (TxBody era),
 SpecTranslate (ConwayLedgerExecContext era) (Tx era),
 ToExpr (SpecRep (Tx era)), SpecNormalize (SpecState "LEDGER" era),
 Eq (SpecState "LEDGER" era)) =>
Globals
-> TRC (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ImpM t ()
submitTxConformanceHook Globals
globals trc :: TRC (EraRule "LEDGER" era)
trc@(TRC (Environment (EraRule "LEDGER" era)
env, State (EraRule "LEDGER" era)
state, Signal (EraRule "LEDGER" era)
signal)) Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
impRuleResult = do
  let ctx :: ConwayLedgerExecContext era
ctx =
        ConwayLedgerExecContext
          { clecPolicyHash :: StrictMaybe ScriptHash
clecPolicyHash =
              State (EraRule "LEDGER" era)
LedgerState era
state LedgerState era
-> Getting
     (StrictMaybe ScriptHash) (LedgerState era) (StrictMaybe ScriptHash)
-> StrictMaybe ScriptHash
forall s a. s -> Getting a s a -> a
^. (UTxOState era -> Const (StrictMaybe ScriptHash) (UTxOState era))
-> LedgerState era
-> Const (StrictMaybe ScriptHash) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(UTxOState era -> f (UTxOState era))
-> LedgerState era -> f (LedgerState era)
lsUTxOStateL ((UTxOState era -> Const (StrictMaybe ScriptHash) (UTxOState era))
 -> LedgerState era
 -> Const (StrictMaybe ScriptHash) (LedgerState era))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> UTxOState era -> Const (StrictMaybe ScriptHash) (UTxOState era))
-> Getting
     (StrictMaybe ScriptHash) (LedgerState era) (StrictMaybe ScriptHash)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovState era -> Const (StrictMaybe ScriptHash) (GovState era))
-> UTxOState era -> Const (StrictMaybe ScriptHash) (UTxOState era)
(ConwayGovState era
 -> Const (StrictMaybe ScriptHash) (ConwayGovState era))
-> UTxOState era -> Const (StrictMaybe ScriptHash) (UTxOState era)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL ((ConwayGovState era
  -> Const (StrictMaybe ScriptHash) (ConwayGovState era))
 -> UTxOState era -> Const (StrictMaybe ScriptHash) (UTxOState era))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> ConwayGovState era
    -> Const (StrictMaybe ScriptHash) (ConwayGovState era))
-> (StrictMaybe ScriptHash
    -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
-> UTxOState era
-> Const (StrictMaybe ScriptHash) (UTxOState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constitution era
 -> Const (StrictMaybe ScriptHash) (Constitution era))
-> GovState era -> Const (StrictMaybe ScriptHash) (GovState era)
(Constitution era
 -> Const (StrictMaybe ScriptHash) (Constitution era))
-> ConwayGovState era
-> Const (StrictMaybe ScriptHash) (ConwayGovState era)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Constitution era)
Lens' (GovState era) (Constitution era)
constitutionGovStateL ((Constitution era
  -> Const (StrictMaybe ScriptHash) (Constitution era))
 -> ConwayGovState era
 -> Const (StrictMaybe ScriptHash) (ConwayGovState era))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> Constitution era
    -> Const (StrictMaybe ScriptHash) (Constitution era))
-> (StrictMaybe ScriptHash
    -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
-> ConwayGovState era
-> Const (StrictMaybe ScriptHash) (ConwayGovState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictMaybe ScriptHash
 -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
-> Constitution era
-> Const (StrictMaybe ScriptHash) (Constitution era)
forall era (f :: * -> *).
Functor f =>
(StrictMaybe ScriptHash -> f (StrictMaybe ScriptHash))
-> Constitution era -> f (Constitution era)
constitutionScriptL
          , clecEnactState :: EnactState era
clecEnactState = GovState era -> EnactState era
forall era. ConwayEraGov era => GovState era -> EnactState era
mkEnactState (GovState era -> EnactState era) -> GovState era -> EnactState era
forall a b. (a -> b) -> a -> b
$ State (EraRule "LEDGER" era)
LedgerState era
state LedgerState era
-> Getting (GovState era) (LedgerState era) (GovState era)
-> GovState era
forall s a. s -> Getting a s a -> a
^. (UTxOState era -> Const (GovState era) (UTxOState era))
-> LedgerState era -> Const (GovState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(UTxOState era -> f (UTxOState era))
-> LedgerState era -> f (LedgerState era)
lsUTxOStateL ((UTxOState era -> Const (GovState era) (UTxOState era))
 -> LedgerState era -> Const (GovState era) (LedgerState era))
-> ((GovState era -> Const (GovState era) (GovState era))
    -> UTxOState era -> Const (GovState era) (UTxOState era))
-> Getting (GovState era) (LedgerState era) (GovState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovState era -> Const (GovState era) (GovState era))
-> UTxOState era -> Const (GovState era) (UTxOState era)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL
          , clecUtxoExecContext :: UtxoExecContext era
clecUtxoExecContext =
              UtxoExecContext
                { uecTx :: Tx era
uecTx = Tx era
Signal (EraRule "LEDGER" era)
signal
                , uecUTxO :: UTxO era
uecUTxO = State (EraRule "LEDGER" era)
LedgerState era
state LedgerState era
-> Getting (UTxO era) (LedgerState era) (UTxO era) -> UTxO era
forall s a. s -> Getting a s a -> a
^. Getting (UTxO era) (LedgerState era) (UTxO era)
forall era. Lens' (LedgerState era) (UTxO era)
forall (t :: * -> *) era. CanSetUTxO t => Lens' (t era) (UTxO era)
utxoL
                , uecUtxoEnv :: UtxoEnv era
uecUtxoEnv =
                    UtxoEnv
                      { ueSlot :: SlotNo
ueSlot = LedgerEnv era
Environment (EraRule "LEDGER" era)
env LedgerEnv era -> Getting SlotNo (LedgerEnv era) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (LedgerEnv era) SlotNo
forall era (f :: * -> *).
Functor f =>
(SlotNo -> f SlotNo) -> LedgerEnv era -> f (LedgerEnv era)
ledgerSlotNoL
                      , uePParams :: PParams era
uePParams = State (EraRule "LEDGER" era)
LedgerState era
state LedgerState era
-> Getting (PParams era) (LedgerState era) (PParams era)
-> PParams era
forall s a. s -> Getting a s a -> a
^. (UTxOState era -> Const (PParams era) (UTxOState era))
-> LedgerState era -> Const (PParams era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(UTxOState era -> f (UTxOState era))
-> LedgerState era -> f (LedgerState era)
lsUTxOStateL ((UTxOState era -> Const (PParams era) (UTxOState era))
 -> LedgerState era -> Const (PParams era) (LedgerState era))
-> ((PParams era -> Const (PParams era) (PParams era))
    -> UTxOState era -> Const (PParams era) (UTxOState era))
-> Getting (PParams era) (LedgerState era) (PParams era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovState era -> Const (PParams era) (GovState era))
-> UTxOState era -> Const (PParams era) (UTxOState era)
(ConwayGovState era -> Const (PParams era) (ConwayGovState era))
-> UTxOState era -> Const (PParams era) (UTxOState era)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL ((ConwayGovState era -> Const (PParams era) (ConwayGovState era))
 -> UTxOState era -> Const (PParams era) (UTxOState era))
-> ((PParams era -> Const (PParams era) (PParams era))
    -> ConwayGovState era -> Const (PParams era) (ConwayGovState era))
-> (PParams era -> Const (PParams era) (PParams era))
-> UTxOState era
-> Const (PParams era) (UTxOState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PParams era -> Const (PParams era) (PParams era))
-> GovState era -> Const (PParams era) (GovState era)
(PParams era -> Const (PParams era) (PParams era))
-> ConwayGovState era -> Const (PParams era) (ConwayGovState era)
forall era. EraGov era => Lens' (GovState era) (PParams era)
Lens' (GovState era) (PParams era)
curPParamsGovStateL
                      , ueCertState :: CertState era
ueCertState = State (EraRule "LEDGER" era)
LedgerState era
state LedgerState era
-> Getting (CertState era) (LedgerState era) (CertState era)
-> CertState era
forall s a. s -> Getting a s a -> a
^. Getting (CertState era) (LedgerState era) (CertState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL
                      }
                }
          }
  -- translate inputs
  specTRC :: SpecTRC "LEDGER" era
specTRC@(SpecTRC SpecEnvironment "LEDGER" era
specEnv SpecState "LEDGER" era
specState SpecSignal "LEDGER" era
specSignal) <-
    String
-> ImpM t (SpecTRC "LEDGER" era) -> ImpM t (SpecTRC "LEDGER" era)
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating inputs" (ImpM t (SpecTRC "LEDGER" era) -> ImpM t (SpecTRC "LEDGER" era))
-> (Either Text (SpecTRC "LEDGER" era)
    -> ImpM t (SpecTRC "LEDGER" era))
-> Either Text (SpecTRC "LEDGER" era)
-> ImpM t (SpecTRC "LEDGER" era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text (SpecTRC "LEDGER" era) -> ImpM t (SpecTRC "LEDGER" era)
forall a b (m :: * -> *).
(HasCallStack, ToExpr a, NFData b, MonadIO m) =>
Either a b -> m b
expectRightDeepExpr (Either Text (SpecTRC "LEDGER" era)
 -> ImpM t (SpecTRC "LEDGER" era))
-> Either Text (SpecTRC "LEDGER" era)
-> ImpM t (SpecTRC "LEDGER" era)
forall a b. (a -> b) -> a -> b
$ ExecContext "LEDGER" era
-> TRC (EraRule "LEDGER" era) -> Either Text (SpecTRC "LEDGER" era)
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> TRC (EraRule rule era) -> Either Text (SpecTRC rule era)
translateInputs ExecContext "LEDGER" era
ConwayLedgerExecContext era
ctx TRC (EraRule "LEDGER" era)
trc
  -- get agda response
  Either Text (SpecState "LEDGER" era)
agdaResponse <- (Either Text (SpecState "LEDGER" era)
 -> Either Text (SpecState "LEDGER" era))
-> ImpM t (Either Text (SpecState "LEDGER" era))
-> ImpM t (Either Text (SpecState "LEDGER" era))
forall a b. (a -> b) -> ImpM t a -> ImpM t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SpecState "LEDGER" era -> SpecState "LEDGER" era)
-> Either Text (SpecState "LEDGER" era)
-> Either Text (SpecState "LEDGER" era)
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SpecState "LEDGER" era -> SpecState "LEDGER" era
forall a. SpecNormalize a => a -> a
specNormalize) (ImpM t (Either Text (SpecState "LEDGER" era))
 -> ImpM t (Either Text (SpecState "LEDGER" era)))
-> (Either Text (SpecState "LEDGER" era)
    -> ImpM t (Either Text (SpecState "LEDGER" era)))
-> Either Text (SpecState "LEDGER" era)
-> ImpM t (Either Text (SpecState "LEDGER" era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text (SpecState "LEDGER" era)
-> ImpM t (Either Text (SpecState "LEDGER" era))
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep (Either Text (SpecState "LEDGER" era)
 -> ImpM t (Either Text (SpecState "LEDGER" era)))
-> Either Text (SpecState "LEDGER" era)
-> ImpM t (Either Text (SpecState "LEDGER" era))
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
SpecTRC rule era -> Either Text (SpecState rule era)
runAgdaRule @"LEDGER" @era SpecTRC "LEDGER" era
specTRC
  -- translate imp response
  let
    impRuleResult' :: Either Text (LedgerState era)
impRuleResult' = (NonEmpty (PredicateFailure (EraRule "LEDGER" era)) -> Text)
-> ((LedgerState era, [Event (EraRule "LEDGER" era)])
    -> LedgerState era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (LedgerState era, [Event (EraRule "LEDGER" era)])
-> Either Text (LedgerState era)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (String -> Text
T.pack (String -> Text)
-> (NonEmpty (PredicateFailure (EraRule "LEDGER" era)) -> String)
-> NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (PredicateFailure (EraRule "LEDGER" era)) -> String
forall a. Show a => a -> String
show) (LedgerState era, [Event (EraRule "LEDGER" era)])
-> LedgerState era
forall a b. (a, b) -> a
fst Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (LedgerState era, [Event (EraRule "LEDGER" era)])
impRuleResult
    impResponse :: Either Text (SpecState "LEDGER" era)
impResponse = (Text -> Text)
-> Either Text (SpecState "LEDGER" era)
-> Either Text (SpecState "LEDGER" era)
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) -> (Text -> String) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
forall a. Show a => a -> String
show) (Either Text (SpecState "LEDGER" era)
 -> Either Text (SpecState "LEDGER" era))
-> (LedgerState era -> Either Text (SpecState "LEDGER" era))
-> LedgerState era
-> Either Text (SpecState "LEDGER" era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecContext "LEDGER" era
-> TRC (EraRule "LEDGER" era)
-> State (EraRule "LEDGER" era)
-> Either Text (SpecState "LEDGER" era)
forall (rule :: Symbol) era.
ExecSpecRule rule era =>
ExecContext rule era
-> TRC (EraRule rule era)
-> State (EraRule rule era)
-> Either Text (SpecState rule era)
translateOutput ExecContext "LEDGER" era
ConwayLedgerExecContext era
ctx TRC (EraRule "LEDGER" era)
trc (LedgerState era -> Either Text (SpecState "LEDGER" era))
-> Either Text (LedgerState era)
-> Either Text (SpecState "LEDGER" era)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Either Text (LedgerState era)
impRuleResult'

  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"implEnv"
  LedgerEnv era -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr LedgerEnv era
Environment (EraRule "LEDGER" era)
env
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"implState"
  LedgerState era -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr State (EraRule "LEDGER" era)
LedgerState era
state
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"implSignal"
  Tx era -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr Tx era
Signal (EraRule "LEDGER" era)
signal
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"specEnv"
  SpecEnvironment "LEDGER" era -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr SpecEnvironment "LEDGER" era
specEnv
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"specState"
  SpecState "LEDGER" era -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr SpecState "LEDGER" era
specState
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"specSignal"
  SpecSignal "LEDGER" era -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr SpecSignal "LEDGER" era
specSignal
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"Extra info:"
  Doc AnsiStyle -> ImpM t ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM t ()) -> Doc AnsiStyle -> ImpM t ()
forall a b. (a -> b) -> a -> b
$
    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 @"LEDGER" @era
      Globals
globals
      ExecContext "LEDGER" era
ConwayLedgerExecContext era
ctx
      ((Environment (EraRule "LEDGER" era), State (EraRule "LEDGER" era),
 Signal (EraRule "LEDGER" era))
-> TRC (EraRule "LEDGER" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule "LEDGER" era)
env, State (EraRule "LEDGER" era)
state, Signal (EraRule "LEDGER" era)
signal))
      ((NonEmpty (PredicateFailure (EraRule "LEDGER" era)) -> Text)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (LedgerState era, [Event (EraRule "LEDGER" era)])
-> Either Text (LedgerState era, [Event (EraRule "LEDGER" era)])
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 (PredicateFailure (EraRule "LEDGER" era)) -> String)
-> NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (PredicateFailure (EraRule "LEDGER" era)) -> String
forall a. Show a => a -> String
show) Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (LedgerState era, [Event (EraRule "LEDGER" era)])
impRuleResult)
  Doc AnsiStyle -> ImpM t ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM t ()) -> Doc AnsiStyle -> ImpM t ()
forall a b. (a -> b) -> a -> b
$ Either Text (SpecState "LEDGER" era)
-> Either Text (SpecState "LEDGER" era) -> Doc AnsiStyle
forall a.
ToExpr a =>
Either Text a -> Either Text a -> Doc AnsiStyle
diffConformance Either Text (SpecState "LEDGER" era)
impResponse Either Text (SpecState "LEDGER" era)
agdaResponse
  case (Either Text (SpecState "LEDGER" era)
impResponse, Either Text (SpecState "LEDGER" era)
agdaResponse) of
    (Right SpecState "LEDGER" era
impRes, Right SpecState "LEDGER" era
agdaRes)
      | SpecState "LEDGER" era
impRes SpecState "LEDGER" era -> SpecState "LEDGER" era -> Bool
forall a. Eq a => a -> a -> Bool
== SpecState "LEDGER" era
agdaRes -> () -> ImpM t ()
forall a. a -> ImpM t a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    (Left Text
_, Left Text
_) -> () -> ImpM t ()
forall a. a -> ImpM t a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    (Either Text (SpecState "LEDGER" era),
 Either Text (SpecState "LEDGER" era))
_ -> String -> ImpM t ()
forall (m :: * -> *) a. (HasCallStack, MonadIO m) => String -> m a
assertFailure String
"Conformance failure"

spec :: Spec
spec :: Spec
spec =
  forall t. ImpSpec t => SpecWith (ImpInit t) -> Spec
withImpInit @(LedgerSpec ConwayEra) (SpecWith (ImpInit (LedgerSpec ConwayEra)) -> Spec)
-> SpecWith (ImpInit (LedgerSpec ConwayEra)) -> Spec
forall a b. (a -> b) -> a -> b
$
    forall era.
ShelleyEraImp era =>
Version
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
modifyImpInitProtVer @ConwayEra (forall (v :: Natural).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @10) (SpecWith (ImpInit (LedgerSpec ConwayEra))
 -> SpecWith (ImpInit (LedgerSpec ConwayEra)))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a b. (a -> b) -> a -> b
$
      (forall t.
 Globals
 -> TRC (EraRule "LEDGER" ConwayEra)
 -> Either
      (NonEmpty (PredicateFailure (EraRule "LEDGER" ConwayEra)))
      (State (EraRule "LEDGER" ConwayEra),
       [Event (EraRule "LEDGER" ConwayEra)])
 -> ImpM t ())
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(forall t.
 Globals
 -> TRC (EraRule "LEDGER" era)
 -> Either
      (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
      (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
 -> ImpM t ())
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
modifyImpInitPostSubmitTxHook Globals
-> TRC (EraRule "LEDGER" ConwayEra)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" ConwayEra)))
     (State (EraRule "LEDGER" ConwayEra),
      [Event (EraRule "LEDGER" ConwayEra)])
-> ImpM t ()
forall t.
Globals
-> TRC (EraRule "LEDGER" ConwayEra)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" ConwayEra)))
     (State (EraRule "LEDGER" ConwayEra),
      [Event (EraRule "LEDGER" ConwayEra)])
-> ImpM t ()
forall era t.
(ConwayEraImp era, ExecSpecRule "LEDGER" era,
 ExecContext "LEDGER" era ~ ConwayLedgerExecContext era,
 SpecTranslate (ExecContext "LEDGER" era) (TxWits era),
 HasCallStack, SpecRep (TxWits era) ~ TxWitnesses,
 SpecRep (TxBody era) ~ TxBody, SpecTranslate TxId (TxBody era),
 SpecTranslate (ConwayLedgerExecContext era) (Tx era),
 ToExpr (SpecRep (Tx era)), SpecNormalize (SpecState "LEDGER" era),
 Eq (SpecState "LEDGER" era)) =>
Globals
-> TRC (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ImpM t ()
submitTxConformanceHook (SpecWith (ImpInit (LedgerSpec ConwayEra))
 -> SpecWith (ImpInit (LedgerSpec ConwayEra)))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a b. (a -> b) -> a -> b
$ do
        String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Basic imp conformance" (SpecWith (ImpInit (LedgerSpec ConwayEra))
 -> SpecWith (ImpInit (LedgerSpec ConwayEra)))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a b. (a -> b) -> a -> b
$ do
          String
-> ImpM (LedgerSpec ConwayEra) ()
-> SpecWith (Arg (ImpM (LedgerSpec ConwayEra) ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"Submit constitution" (ImpM (LedgerSpec ConwayEra) ()
 -> SpecWith (Arg (ImpM (LedgerSpec ConwayEra) ())))
-> ImpM (LedgerSpec ConwayEra) ()
-> SpecWith (Arg (ImpM (LedgerSpec ConwayEra) ()))
forall a b. (a -> b) -> a -> b
$ do
            GovActionId
_ <- forall era.
ConwayEraImp era =>
StrictMaybe (GovPurposeId 'ConstitutionPurpose)
-> ImpTestM era GovActionId
submitConstitution @ConwayEra StrictMaybe (GovPurposeId 'ConstitutionPurpose)
forall a. StrictMaybe a
SNothing
            Natural -> ImpM (LedgerSpec ConwayEra) ()
forall era. ShelleyEraImp era => Natural -> ImpTestM era ()
passNEpochs Natural
2
        String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Conway Imp conformance" (SpecWith (ImpInit (LedgerSpec ConwayEra))
 -> SpecWith (ImpInit (LedgerSpec ConwayEra)))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a b. (a -> b) -> a -> b
$ do
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"BBODY" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(AlonzoEraImp era, BabbageEraTxBody era,
 InjectRuleFailure "BBODY" ConwayBbodyPredFailure era,
 InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure era,
 ToExpr (Event (EraRule "BBODY" era)), ConwayEraPParams era) =>
SpecWith (ImpInit (LedgerSpec era))
Bbody.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"CERTS" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayCertsPredFailure era,
 InjectRuleFailure "LEDGER" ConwayLedgerPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Certs.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"DELEG" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayDelegPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Deleg.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"ENACT" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era, NFData (Event (EraRule "ENACT" era)),
 ToExpr (Event (EraRule "ENACT" era)),
 Eq (Event (EraRule "ENACT" era)),
 Typeable (Event (EraRule "ENACT" era)),
 Event (EraRule "HARDFORK" era) ~ ConwayHardForkEvent era,
 Event (EraRule "NEWEPOCH" era) ~ ConwayNewEpochEvent era,
 Event (EraRule "EPOCH" era) ~ ConwayEpochEvent era,
 InjectRuleEvent "TICK" ConwayEpochEvent era,
 InjectRuleFailure "LEDGER" ConwayGovPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Enact.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"EPOCH" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era, InjectRuleEvent "TICK" ConwayEpochEvent era,
 Event (EraRule "EPOCH" era) ~ ConwayEpochEvent era,
 Event (EraRule "NEWEPOCH" era) ~ ConwayNewEpochEvent era) =>
SpecWith (ImpInit (LedgerSpec era))
Epoch.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"GOV" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayGovPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Gov.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"GOVCERT" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayGovCertPredFailure era,
 InjectRuleFailure "LEDGER" ConwayGovPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
GovCert.spec
          -- LEDGER tests pending on the dRep delegations cleanup in the spec:
          -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/635
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"LEDGER" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayLedgerPredFailure era,
 InjectRuleFailure "LEDGER" ConwayUtxoPredFailure era,
 InjectRuleFailure "LEDGER" ConwayGovPredFailure era,
 ApplyTx era) =>
SpecWith (ImpInit (LedgerSpec era))
Ledger.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"RATIFY" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(HasCallStack, ConwayEraImp era) =>
SpecWith (ImpInit (LedgerSpec era))
Ratify.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"UTXO" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" BabbageUtxoPredFailure era,
 InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure era,
 Inject (ConwayContextError era) (ContextError era)) =>
SpecWith (ImpInit (LedgerSpec era))
Utxo.spec
          String
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"UTXOS" SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(ConwayEraImp era,
 Inject (BabbageContextError era) (ContextError era),
 Inject (ConwayContextError era) (ContextError era),
 InjectRuleFailure "LEDGER" BabbageUtxoPredFailure era,
 InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure era,
 InjectRuleFailure "LEDGER" AlonzoUtxowPredFailure era,
 InjectRuleFailure "LEDGER" ShelleyUtxowPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Utxos.spec