{-# 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 (LedgerEnv, UtxoEnv (..), ledgerSlotNoL)
import Control.State.Transition
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (bimapM)
import Data.List.NonEmpty
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.Conway (ConwayTxBodyTransContext)
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)

testImpConformance ::
  forall era t.
  ( ConwayEraImp era
  , ExecSpecRule "LEDGER" era
  , ExecContext "LEDGER" era ~ ConwayLedgerExecContext era
  , ExecSignal "LEDGER" era ~ Tx era
  , ExecState "LEDGER" era ~ LedgerState era
  , SpecTranslate (ExecContext "LEDGER" era) (ExecState "LEDGER" era)
  , SpecTranslate (ExecContext "LEDGER" era) (ExecEnvironment "LEDGER" era)
  , SpecTranslate (ExecContext "LEDGER" era) (TxWits era)
  , HasCallStack
  , SpecRep (TxWits era) ~ Agda.TxWitnesses
  , SpecRep (TxBody era) ~ Agda.TxBody
  , ExecEnvironment "LEDGER" era ~ LedgerEnv era
  , SpecTranslate ConwayTxBodyTransContext (TxBody era)
  , ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" era)))
  , SpecTranslate (ConwayLedgerExecContext era) (Tx era)
  , ToExpr (SpecRep (Tx era))
  ) =>
  Globals ->
  Either
    (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
    (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
  ExecEnvironment "LEDGER" era ->
  ExecState "LEDGER" era ->
  ExecSignal "LEDGER" era ->
  ImpM t ()
testImpConformance :: forall era t.
(ConwayEraImp era, ExecSpecRule "LEDGER" era,
 ExecContext "LEDGER" era ~ ConwayLedgerExecContext era,
 ExecSignal "LEDGER" era ~ Tx era,
 ExecState "LEDGER" era ~ LedgerState era,
 SpecTranslate (ExecContext "LEDGER" era) (ExecState "LEDGER" era),
 SpecTranslate
   (ExecContext "LEDGER" era) (ExecEnvironment "LEDGER" era),
 SpecTranslate (ExecContext "LEDGER" era) (TxWits era),
 HasCallStack, SpecRep (TxWits era) ~ TxWitnesses,
 SpecRep (TxBody era) ~ TxBody,
 ExecEnvironment "LEDGER" era ~ LedgerEnv era,
 SpecTranslate ConwayTxBodyTransContext (TxBody era),
 ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" era))),
 SpecTranslate (ConwayLedgerExecContext era) (Tx era),
 ToExpr (SpecRep (Tx era))) =>
Globals
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ExecEnvironment "LEDGER" era
-> ExecState "LEDGER" era
-> ExecSignal "LEDGER" era
-> ImpM t ()
testImpConformance Globals
_globals Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
impRuleResult ExecEnvironment "LEDGER" era
env ExecState "LEDGER" era
state ExecSignal "LEDGER" era
signal = do
  let ctx :: ConwayLedgerExecContext era
ctx =
        ConwayLedgerExecContext
          { clecPolicyHash :: StrictMaybe ScriptHash
clecPolicyHash =
              ExecState "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
$ ExecState "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
ExecSignal "LEDGER" era
signal
                , uecUTxO :: UTxO era
uecUTxO = ExecState "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 = ExecEnvironment "LEDGER" era
LedgerEnv 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 = ExecState "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 = ExecState "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
  (SpecRep (LedgerEnv era)
specEnv, SpecRep (LedgerState era)
specState, SpecRep (Tx era)
specSignal) <-
    (,,)
      (SpecRep (LedgerEnv era)
 -> SpecRep (LedgerState era)
 -> SpecRep (Tx era)
 -> (SpecRep (LedgerEnv era), SpecRep (LedgerState era),
     SpecRep (Tx era)))
-> ImpM t (SpecRep (LedgerEnv era))
-> ImpM
     t
     (SpecRep (LedgerState era)
      -> SpecRep (Tx era)
      -> (SpecRep (LedgerEnv era), SpecRep (LedgerState era),
          SpecRep (Tx era)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either SpecTranslationError (SpecRep (LedgerEnv era))
-> ImpM t (SpecRep (LedgerEnv era))
forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (ConwayLedgerExecContext era
-> SpecTransM
     (ConwayLedgerExecContext era) (SpecRep (LedgerEnv era))
-> Either SpecTranslationError (SpecRep (LedgerEnv era))
forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ConwayLedgerExecContext era
ctx (SpecTransM (ConwayLedgerExecContext era) (SpecRep (LedgerEnv era))
 -> Either SpecTranslationError (SpecRep (LedgerEnv era)))
-> SpecTransM
     (ConwayLedgerExecContext era) (SpecRep (LedgerEnv era))
-> Either SpecTranslationError (SpecRep (LedgerEnv era))
forall a b. (a -> b) -> a -> b
$ LedgerEnv era
-> SpecTransM
     (ConwayLedgerExecContext era) (SpecRep (LedgerEnv era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecEnvironment "LEDGER" era
LedgerEnv era
env)
      ImpM
  t
  (SpecRep (LedgerState era)
   -> SpecRep (Tx era)
   -> (SpecRep (LedgerEnv era), SpecRep (LedgerState era),
       SpecRep (Tx era)))
-> ImpM t (SpecRep (LedgerState era))
-> ImpM
     t
     (SpecRep (Tx era)
      -> (SpecRep (LedgerEnv era), SpecRep (LedgerState era),
          SpecRep (Tx era)))
forall a b. ImpM t (a -> b) -> ImpM t a -> ImpM t b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either SpecTranslationError (SpecRep (LedgerState era))
-> ImpM t (SpecRep (LedgerState era))
forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (ConwayLedgerExecContext era
-> SpecTransM
     (ConwayLedgerExecContext era) (SpecRep (LedgerState era))
-> Either SpecTranslationError (SpecRep (LedgerState era))
forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ConwayLedgerExecContext era
ctx (SpecTransM
   (ConwayLedgerExecContext era) (SpecRep (LedgerState era))
 -> Either SpecTranslationError (SpecRep (LedgerState era)))
-> SpecTransM
     (ConwayLedgerExecContext era) (SpecRep (LedgerState era))
-> Either SpecTranslationError (SpecRep (LedgerState era))
forall a b. (a -> b) -> a -> b
$ LedgerState era
-> SpecTransM
     (ConwayLedgerExecContext era) (SpecRep (LedgerState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecState "LEDGER" era
LedgerState era
state)
      ImpM
  t
  (SpecRep (Tx era)
   -> (SpecRep (LedgerEnv era), SpecRep (LedgerState era),
       SpecRep (Tx era)))
-> ImpM t (SpecRep (Tx era))
-> ImpM
     t
     (SpecRep (LedgerEnv era), SpecRep (LedgerState era),
      SpecRep (Tx era))
forall a b. ImpM t (a -> b) -> ImpM t a -> ImpM t b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either SpecTranslationError (SpecRep (Tx era))
-> ImpM t (SpecRep (Tx era))
forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (ConwayLedgerExecContext era
-> SpecTransM (ConwayLedgerExecContext era) (SpecRep (Tx era))
-> Either SpecTranslationError (SpecRep (Tx era))
forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ConwayLedgerExecContext era
ctx (SpecTransM (ConwayLedgerExecContext era) (SpecRep (Tx era))
 -> Either SpecTranslationError (SpecRep (Tx era)))
-> SpecTransM (ConwayLedgerExecContext era) (SpecRep (Tx era))
-> Either SpecTranslationError (SpecRep (Tx era))
forall a b. (a -> b) -> a -> b
$ Tx era
-> SpecTransM (ConwayLedgerExecContext era) (SpecRep (Tx era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Tx era
ExecSignal "LEDGER" era
signal)
  -- get agda response
  Either OpaqueErrorString LState
agdaResponse <-
    (Either OpaqueErrorString LState
 -> Either OpaqueErrorString LState)
-> ImpM t (Either OpaqueErrorString LState)
-> ImpM t (Either OpaqueErrorString LState)
forall a b. (a -> b) -> ImpM t a -> ImpM t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LState -> LState)
-> Either OpaqueErrorString LState
-> Either OpaqueErrorString LState
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 LState -> LState
forall a. FixupSpecRep a => a -> a
fixup) (ImpM t (Either OpaqueErrorString LState)
 -> ImpM t (Either OpaqueErrorString LState))
-> ImpM t (Either OpaqueErrorString LState)
-> ImpM t (Either OpaqueErrorString LState)
forall a b. (a -> b) -> a -> b
$
      Either OpaqueErrorString (SpecRep (ExecState "LEDGER" era))
-> ImpM
     t (Either OpaqueErrorString (SpecRep (ExecState "LEDGER" era)))
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep (Either OpaqueErrorString (SpecRep (ExecState "LEDGER" era))
 -> ImpM
      t (Either OpaqueErrorString (SpecRep (ExecState "LEDGER" era))))
-> Either OpaqueErrorString (SpecRep (ExecState "LEDGER" era))
-> ImpM
     t (Either OpaqueErrorString (SpecRep (ExecState "LEDGER" era)))
forall a b. (a -> b) -> a -> b
$
        forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
SpecRep (ExecEnvironment rule era)
-> SpecRep (ExecState rule era)
-> SpecRep (ExecSignal rule era)
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
runAgdaRule @"LEDGER" @era SpecRep (ExecEnvironment "LEDGER" era)
SpecRep (LedgerEnv era)
specEnv SpecRep (ExecState "LEDGER" era)
SpecRep (LedgerState era)
specState SpecRep (Tx era)
SpecRep (ExecSignal "LEDGER" era)
specSignal
  -- translate imp response
  Either OpaqueErrorString LState
impResponse <-
    Either SpecTranslationError (Either OpaqueErrorString LState)
-> ImpM t (Either OpaqueErrorString LState)
forall a (m :: * -> *) b.
(HasCallStack, ToExpr a, MonadIO m) =>
Either a b -> m b
expectRightExpr (Either SpecTranslationError (Either OpaqueErrorString LState)
 -> ImpM t (Either OpaqueErrorString LState))
-> Either SpecTranslationError (Either OpaqueErrorString LState)
-> ImpM t (Either OpaqueErrorString LState)
forall a b. (a -> b) -> a -> b
$
      ConwayLedgerExecContext era
-> SpecTransM
     (ConwayLedgerExecContext era) (Either OpaqueErrorString LState)
-> Either SpecTranslationError (Either OpaqueErrorString LState)
forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ConwayLedgerExecContext era
ctx (SpecTransM
   (ConwayLedgerExecContext era) (Either OpaqueErrorString LState)
 -> Either SpecTranslationError (Either OpaqueErrorString LState))
-> SpecTransM
     (ConwayLedgerExecContext era) (Either OpaqueErrorString LState)
-> Either SpecTranslationError (Either OpaqueErrorString LState)
forall a b. (a -> b) -> a -> b
$
        (NonEmpty (PredicateFailure (EraRule "LEDGER" era))
 -> SpecTransM (ConwayLedgerExecContext era) OpaqueErrorString)
-> ((LedgerState era, [Event (EraRule "LEDGER" era)])
    -> SpecTransM (ConwayLedgerExecContext era) LState)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (LedgerState era, [Event (EraRule "LEDGER" era)])
-> SpecTransM
     (ConwayLedgerExecContext era) (Either OpaqueErrorString LState)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM
          (OpaqueErrorString
-> SpecTransM (ConwayLedgerExecContext era) OpaqueErrorString
forall a. a -> SpecTransM (ConwayLedgerExecContext era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString
 -> SpecTransM (ConwayLedgerExecContext era) OpaqueErrorString)
-> (NonEmpty (PredicateFailure (EraRule "LEDGER" era))
    -> OpaqueErrorString)
-> NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> SpecTransM (ConwayLedgerExecContext era) OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString)
          (LedgerState era
-> SpecTransM
     (ConwayLedgerExecContext era) (SpecRep (LedgerState era))
LedgerState era -> SpecTransM (ConwayLedgerExecContext era) LState
forall ctx a.
(SpecTranslate ctx a, FixupSpecRep (SpecRep a)) =>
a -> SpecTransM ctx (SpecRep a)
toTestRep (LedgerState era
 -> SpecTransM (ConwayLedgerExecContext era) LState)
-> ((LedgerState era, [Event (EraRule "LEDGER" era)])
    -> LedgerState era)
-> (LedgerState era, [Event (EraRule "LEDGER" era)])
-> SpecTransM (ConwayLedgerExecContext era) LState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s. Inject t s => t -> s
inject @_ @(ExecState "LEDGER" era) (LedgerState era -> LedgerState era)
-> ((LedgerState era, [Event (EraRule "LEDGER" era)])
    -> LedgerState era)
-> (LedgerState era, [Event (EraRule "LEDGER" era)])
-> LedgerState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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

  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 ExecEnvironment "LEDGER" era
LedgerEnv 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 ExecState "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
ExecSignal "LEDGER" era
signal
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"specEnv"
  SpecRep (LedgerEnv era) -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr SpecRep (LedgerEnv era)
specEnv
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"specState"
  SpecRep (LedgerState era) -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr SpecRep (LedgerState era)
specState
  String -> ImpM t ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"specSignal"
  SpecRep (Tx era) -> ImpM t ()
forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr SpecRep (Tx 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
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     OpaqueErrorString
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @"LEDGER" @era
      Globals
_globals
      ExecContext "LEDGER" era
ConwayLedgerExecContext era
ctx
      ExecEnvironment "LEDGER" era
Environment (EraRule "LEDGER" era)
env
      ExecState "LEDGER" era
State (EraRule "LEDGER" era)
state
      ExecSignal "LEDGER" era
Signal (EraRule "LEDGER" era)
signal
      ((NonEmpty (PredicateFailure (EraRule "LEDGER" era))
 -> OpaqueErrorString)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (LedgerState era, [Event (EraRule "LEDGER" era)])
-> Either
     OpaqueErrorString (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 NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString 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 OpaqueErrorString LState
-> Either OpaqueErrorString LState -> Doc AnsiStyle
forall a. ToExpr a => a -> a -> Doc AnsiStyle
diffConformance Either OpaqueErrorString LState
impResponse Either OpaqueErrorString LState
agdaResponse
  Bool -> ImpM t () -> ImpM t ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Either OpaqueErrorString LState
impResponse Either OpaqueErrorString LState
-> Either OpaqueErrorString LState -> Bool
forall a. Eq a => a -> a -> Bool
/= Either OpaqueErrorString LState
agdaResponse) (ImpM t () -> ImpM t ()) -> ImpM t () -> ImpM t ()
forall a b. (a -> b) -> a -> b
$
    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
 -> Either
      (NonEmpty (PredicateFailure (EraRule "LEDGER" ConwayEra)))
      (State (EraRule "LEDGER" ConwayEra),
       [Event (EraRule "LEDGER" ConwayEra)])
 -> LedgerEnv ConwayEra
 -> LedgerState ConwayEra
 -> Tx ConwayEra
 -> ImpM t ())
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
-> SpecWith (ImpInit (LedgerSpec ConwayEra))
forall era.
(forall t.
 Globals
 -> Either
      (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
      (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
 -> LedgerEnv era
 -> LedgerState era
 -> Tx era
 -> ImpM t ())
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
modifyImpInitExpectLedgerRuleConformance Globals
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" ConwayEra)))
     (State (EraRule "LEDGER" ConwayEra),
      [Event (EraRule "LEDGER" ConwayEra)])
-> ExecEnvironment "LEDGER" ConwayEra
-> ExecState "LEDGER" ConwayEra
-> ExecSignal "LEDGER" ConwayEra
-> ImpM t ()
Globals
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" ConwayEra)))
     (State (EraRule "LEDGER" ConwayEra),
      [Event (EraRule "LEDGER" ConwayEra)])
-> LedgerEnv ConwayEra
-> LedgerState ConwayEra
-> Tx ConwayEra
-> ImpM t ()
forall t.
Globals
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" ConwayEra)))
     (State (EraRule "LEDGER" ConwayEra),
      [Event (EraRule "LEDGER" ConwayEra)])
-> LedgerEnv ConwayEra
-> LedgerState ConwayEra
-> Tx ConwayEra
-> ImpM t ()
forall era t.
(ConwayEraImp era, ExecSpecRule "LEDGER" era,
 ExecContext "LEDGER" era ~ ConwayLedgerExecContext era,
 ExecSignal "LEDGER" era ~ Tx era,
 ExecState "LEDGER" era ~ LedgerState era,
 SpecTranslate (ExecContext "LEDGER" era) (ExecState "LEDGER" era),
 SpecTranslate
   (ExecContext "LEDGER" era) (ExecEnvironment "LEDGER" era),
 SpecTranslate (ExecContext "LEDGER" era) (TxWits era),
 HasCallStack, SpecRep (TxWits era) ~ TxWitnesses,
 SpecRep (TxBody era) ~ TxBody,
 ExecEnvironment "LEDGER" era ~ LedgerEnv era,
 SpecTranslate ConwayTxBodyTransContext (TxBody era),
 ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" era))),
 SpecTranslate (ConwayLedgerExecContext era) (Tx era),
 ToExpr (SpecRep (Tx era))) =>
Globals
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ExecEnvironment "LEDGER" era
-> ExecState "LEDGER" era
-> ExecSignal "LEDGER" era
-> ImpM t ()
testImpConformance (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