{-# 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.Alonzo.Tx (AlonzoTx)
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 Lib 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)

-- TODO remove this once we get rid of the CPP directives
{- FOURMOLU_DISABLE -}
testImpConformance ::
  forall era.
  ( ConwayEraImp era
  , ExecSpecRule ConwayFn "LEDGER" era
  , ExecContext ConwayFn "LEDGER" era ~ ConwayLedgerExecContext era
  , ExecSignal ConwayFn "LEDGER" era ~ AlonzoTx era
  , ExecState ConwayFn "LEDGER" era ~ LedgerState era
  , SpecTranslate (ExecContext ConwayFn "LEDGER" era) (ExecState ConwayFn "LEDGER" era)
  , SpecTranslate (ExecContext ConwayFn "LEDGER" era) (ExecEnvironment ConwayFn "LEDGER" era)
  , SpecTranslate (ExecContext ConwayFn "LEDGER" era) (TxWits era)
  , HasCallStack
  , SpecRep (TxWits era) ~ Agda.TxWitnesses
  , SpecRep (TxBody era) ~ Agda.TxBody
  , ExecEnvironment ConwayFn "LEDGER" era ~ LedgerEnv era
  , Tx era ~ AlonzoTx era
  , SpecTranslate ConwayTxBodyTransContext (TxBody era)
  , ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" era)))
  ) =>
  Globals ->
  Either
    (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
    (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
  ExecEnvironment ConwayFn "LEDGER" era ->
  ExecState ConwayFn "LEDGER" era ->
  ExecSignal ConwayFn "LEDGER" era ->
  BaseImpM ()
testImpConformance :: forall era.
(ConwayEraImp era, ExecSpecRule ConwayFn "LEDGER" era,
 ExecContext ConwayFn "LEDGER" era ~ ConwayLedgerExecContext era,
 ExecSignal ConwayFn "LEDGER" era ~ AlonzoTx era,
 ExecState ConwayFn "LEDGER" era ~ LedgerState era,
 SpecTranslate
   (ExecContext ConwayFn "LEDGER" era)
   (ExecState ConwayFn "LEDGER" era),
 SpecTranslate
   (ExecContext ConwayFn "LEDGER" era)
   (ExecEnvironment ConwayFn "LEDGER" era),
 SpecTranslate (ExecContext ConwayFn "LEDGER" era) (TxWits era),
 HasCallStack, SpecRep (TxWits era) ~ TxWitnesses,
 SpecRep (TxBody era) ~ TxBody,
 ExecEnvironment ConwayFn "LEDGER" era ~ LedgerEnv era,
 Tx era ~ AlonzoTx era,
 SpecTranslate ConwayTxBodyTransContext (TxBody era),
 ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" era)))) =>
Globals
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ExecEnvironment ConwayFn "LEDGER" era
-> ExecState ConwayFn "LEDGER" era
-> ExecSignal ConwayFn "LEDGER" era
-> BaseImpM ()
testImpConformance Globals
_globals Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
impRuleResult ExecEnvironment ConwayFn "LEDGER" era
env ExecState ConwayFn "LEDGER" era
state ExecSignal ConwayFn "LEDGER" era
signal = do
  let ctx :: ConwayLedgerExecContext era
ctx =
        ConwayLedgerExecContext
          { clecPolicyHash :: StrictMaybe ScriptHash
clecPolicyHash =
              ExecState ConwayFn "LEDGER" era
state forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerState era) (UTxOState era)
lsUTxOStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (UTxOState era) (GovState era)
utxosGovStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
ConwayEraGov era =>
Lens' (GovState era) (Constitution era)
constitutionGovStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (Constitution era) (StrictMaybe ScriptHash)
constitutionScriptL
          , clecEnactState :: EnactState era
clecEnactState = forall era. ConwayEraGov era => GovState era -> EnactState era
mkEnactState forall a b. (a -> b) -> a -> b
$ ExecState ConwayFn "LEDGER" era
state forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerState era) (UTxOState era)
lsUTxOStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (UTxOState era) (GovState era)
utxosGovStateL
          , clecUtxoExecContext :: UtxoExecContext era
clecUtxoExecContext =
              UtxoExecContext
                { uecTx :: AlonzoTx era
uecTx = ExecSignal ConwayFn "LEDGER" era
signal
                , uecUTxO :: UTxO era
uecUTxO = ExecState ConwayFn "LEDGER" era
state forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerState era) (UTxOState era)
lsUTxOStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (UTxOState era) (UTxO era)
utxosUtxoL
                , uecUtxoEnv :: UtxoEnv era
uecUtxoEnv =
                    UtxoEnv
                      { ueSlot :: SlotNo
ueSlot = ExecEnvironment ConwayFn "LEDGER" era
env forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerEnv era) SlotNo
ledgerSlotNoL
                      , uePParams :: PParams era
uePParams = ExecState ConwayFn "LEDGER" era
state forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerState era) (UTxOState era)
lsUTxOStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (UTxOState era) (GovState era)
utxosGovStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraGov era => Lens' (GovState era) (PParams era)
curPParamsGovStateL
                      , ueCertState :: CertState era
ueCertState = ExecState ConwayFn "LEDGER" era
state forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerState era) (CertState era)
lsCertStateL
                      }
                }
          }
  -- translate inputs
  (SpecRep (LedgerEnv era)
specEnv, SpecRep (LedgerState era)
specState, SpecRep (AlonzoTx era)
specSignal) <-
    (,,)
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ConwayLedgerExecContext era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecEnvironment ConwayFn "LEDGER" era
env)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ConwayLedgerExecContext era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecState ConwayFn "LEDGER" era
state)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ConwayLedgerExecContext era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecSignal ConwayFn "LEDGER" era
signal)
  -- get agda response
  Either OpaqueErrorString LState
agdaResponse <-
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. FixupSpecRep a => a -> a
fixup) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep forall a b. (a -> b) -> a -> b
$
        forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
SpecRep (ExecEnvironment fn rule era)
-> SpecRep (ExecState fn rule era)
-> SpecRep (ExecSignal fn rule era)
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
runAgdaRule @ConwayFn @"LEDGER" @era SpecRep (LedgerEnv era)
specEnv SpecRep (LedgerState era)
specState SpecRep (AlonzoTx era)
specSignal
  -- translate imp response
  Either OpaqueErrorString LState
impResponse <-
    forall a (m :: * -> *) b.
(HasCallStack, ToExpr a, MonadIO m) =>
Either a b -> m b
expectRightExpr forall a b. (a -> b) -> a -> b
$
      forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ConwayLedgerExecContext era
ctx forall a b. (a -> b) -> a -> b
$
        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
          (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString)
          (forall ctx a.
(SpecTranslate ctx a, FixupSpecRep (SpecRep a)) =>
a -> SpecTransM ctx (SpecRep a)
toTestRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s. Inject t s => t -> s
inject @_ @(ExecState ConwayFn "LEDGER" era) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
          Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
impRuleResult

#if __GLASGOW_HASKELL__ >= 906
  logString "implEnv"
  logToExpr env
  logString "implState"
  logToExpr state
  logString "implSignal"
  logToExpr signal
  logString "specEnv"
  logToExpr specEnv
  logString "specState"
  logToExpr specState
  logString "specSignal"
  logToExpr specSignal
  logString "Extra info:"
  logDoc $
    extraInfo @ConwayFn @"LEDGER" @era
      _globals
      ctx
      env
      state
      signal
      (first showOpaqueErrorString impRuleResult)
  logDoc $ diffConformance impResponse agdaResponse
#endif
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Either OpaqueErrorString LState
impResponse forall a. Eq a => a -> a -> Bool
/= Either OpaqueErrorString LState
agdaResponse) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a. (HasCallStack, MonadIO m) => String -> m a
assertFailure String
"Conformance failure"
{- FOURMOLU_ENABLE -}

spec :: Spec
spec :: Spec
spec =
  forall t. ImpSpec t => SpecWith (ImpInit t) -> Spec
withImpInit @(LedgerSpec ConwayEra) 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) forall a b. (a -> b) -> a -> b
$
      forall era.
(Globals
 -> Either
      (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
      (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
 -> LedgerEnv era
 -> LedgerState era
 -> Tx era
 -> BaseImpM ())
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
modifyImpInitExpectLedgerRuleConformance forall era.
(ConwayEraImp era, ExecSpecRule ConwayFn "LEDGER" era,
 ExecContext ConwayFn "LEDGER" era ~ ConwayLedgerExecContext era,
 ExecSignal ConwayFn "LEDGER" era ~ AlonzoTx era,
 ExecState ConwayFn "LEDGER" era ~ LedgerState era,
 SpecTranslate
   (ExecContext ConwayFn "LEDGER" era)
   (ExecState ConwayFn "LEDGER" era),
 SpecTranslate
   (ExecContext ConwayFn "LEDGER" era)
   (ExecEnvironment ConwayFn "LEDGER" era),
 SpecTranslate (ExecContext ConwayFn "LEDGER" era) (TxWits era),
 HasCallStack, SpecRep (TxWits era) ~ TxWitnesses,
 SpecRep (TxBody era) ~ TxBody,
 ExecEnvironment ConwayFn "LEDGER" era ~ LedgerEnv era,
 Tx era ~ AlonzoTx era,
 SpecTranslate ConwayTxBodyTransContext (TxBody era),
 ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" era)))) =>
Globals
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ExecEnvironment ConwayFn "LEDGER" era
-> ExecState ConwayFn "LEDGER" era
-> ExecSignal ConwayFn "LEDGER" era
-> BaseImpM ()
testImpConformance forall a b. (a -> b) -> a -> b
$ do
        forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Basic imp conformance" forall a b. (a -> b) -> a -> b
$ do
          forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"Submit constitution" forall a b. (a -> b) -> a -> b
$ do
            GovActionId
_ <- forall era.
ConwayEraImp era =>
StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
-> ImpTestM era GovActionId
submitConstitution @ConwayEra forall a. StrictMaybe a
SNothing
            forall era. ShelleyEraImp era => Natural -> ImpTestM era ()
passNEpochs Natural
2
        forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Conway Imp conformance" forall a b. (a -> b) -> a -> b
$ do
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"BBODY" forall era.
(AlonzoEraImp era, BabbageEraTxBody era, EraSegWits era,
 InjectRuleFailure "BBODY" ConwayBbodyPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Bbody.spec
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"CERTS" forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayCertsPredFailure era,
 InjectRuleFailure "LEDGER" ConwayLedgerPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Certs.spec
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"DELEG" forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayDelegPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Deleg.spec
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"ENACT" 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
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"EPOCH" 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
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"GOV" forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayGovPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Gov.spec
          -- GOVCERT tests enabling pending on these two issues in spec:
          -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/634
          -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/633
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"GOVCERT" forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayGovCertPredFailure era,
 InjectRuleFailure "LEDGER" ConwayGovPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
GovCert.spec
          -- LEDGER tests enabling pending (at least) on the implementation of scriptSize in the spec:
          -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/620
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"LEDGER" forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayLedgerPredFailure era,
 Event (EraRule "MEMPOOL" era) ~ ConwayMempoolEvent era,
 BaseM (EraRule "LEDGERS" era) ~ ShelleyBase,
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era),
 Event (EraRule "LEDGERS" era) ~ ShelleyLedgersEvent era,
 Event (EraRule "LEDGER" era) ~ ConwayLedgerEvent era,
 STS (EraRule "LEDGERS" era), ApplyTx era) =>
SpecWith (ImpInit (LedgerSpec era))
Ledger.spec
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"RATIFY" forall era. ConwayEraImp era => SpecWith (ImpInit (LedgerSpec era))
Ratify.spec
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"UTXO" forall era. ConwayEraImp era => SpecWith (ImpInit (LedgerSpec era))
Utxo.spec
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"UTXOS" 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