{-# 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 "LEDGER" era
  , ExecContext "LEDGER" era ~ ConwayLedgerExecContext era
  , ExecSignal "LEDGER" era ~ AlonzoTx 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
  , 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 "LEDGER" era ->
  ExecState "LEDGER" era ->
  ExecSignal "LEDGER" era ->
  BaseImpM ()
testImpConformance :: forall era.
(ConwayEraImp era, ExecSpecRule "LEDGER" era,
 ExecContext "LEDGER" era ~ ConwayLedgerExecContext era,
 ExecSignal "LEDGER" era ~ AlonzoTx 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,
 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 "LEDGER" era
-> ExecState "LEDGER" era
-> ExecSignal "LEDGER" era
-> BaseImpM ()
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
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 "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 "LEDGER" era
signal
                , uecUTxO :: UTxO era
uecUTxO = ExecState "LEDGER" era
state forall s a. s -> Getting a s a -> a
^. forall (t :: * -> *) era. CanSetUTxO t => Lens' (t era) (UTxO era)
utxoL
                , uecUtxoEnv :: UtxoEnv era
uecUtxoEnv =
                    UtxoEnv
                      { ueSlot :: SlotNo
ueSlot = ExecEnvironment "LEDGER" era
env forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerEnv era) SlotNo
ledgerSlotNoL
                      , uePParams :: PParams era
uePParams = ExecState "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 "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 "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 "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 "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 (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 (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 "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 @"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 "LEDGER" era,
 ExecContext "LEDGER" era ~ ConwayLedgerExecContext era,
 ExecSignal "LEDGER" era ~ AlonzoTx 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,
 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 "LEDGER" era
-> ExecState "LEDGER" era
-> ExecSignal "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
describe String
"DELEG" forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayDelegPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Deleg.spec
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe 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
describe String
"GOV" forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayGovPredFailure era) =>
SpecWith (ImpInit (LedgerSpec era))
Gov.spec
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"GOVCERT" 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
          forall a. HasCallStack => String -> SpecWith a -> SpecWith a
xdescribe String
"LEDGER" forall era.
(ConwayEraImp era,
 InjectRuleFailure "LEDGER" ConwayLedgerPredFailure 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