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

module Test.Cardano.Ledger.Conformance.Imp.Core where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Core
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rules (ledgerSlotNoL)
import Cardano.Ledger.TxIn (TxId)
import Control.State.Transition
import Data.Bifunctor (Bifunctor (..))
import Data.Data (Proxy (..))
import Data.List.NonEmpty
import Data.Text qualified as T
import GHC.TypeLits (symbolVal)
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.Base
import Test.Cardano.Ledger.Constrained.Conway
import Test.Cardano.Ledger.Conway.ImpTest
import Test.Cardano.Ledger.Imp.Common hiding (Args)
import UnliftIO (evaluateDeep)

conformanceHook ::
  forall rule era t.
  ( ShelleyEraImp era
  , ExecSpecRule rule era
  , ToExpr (Event (EraRule rule era))
  ) =>
  Globals ->
  ExecContext rule era ->
  TRC (EraRule rule era) ->
  Either
    (NonEmpty (PredicateFailure (EraRule rule era)))
    (State (EraRule rule era), [Event (EraRule rule era)]) ->
  ImpM t ()
conformanceHook :: forall (rule :: Symbol) era t.
(ShelleyEraImp era, ExecSpecRule rule era,
 ToExpr (Event (EraRule rule era))) =>
Globals
-> ExecContext rule era
-> TRC (EraRule rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpM t ()
conformanceHook Globals
globals ExecContext rule era
ctx trc :: TRC (EraRule rule era)
trc@(TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
state, Signal (EraRule rule era)
signal)) Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
impRuleResult =
  String -> ImpM t () -> ImpM t ()
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn (String
"Conformance hook (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Proxy rule -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @rule) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")") (ImpM t () -> ImpM t ()) -> ImpM t () -> ImpM t ()
forall a b. (a -> b) -> a -> b
$ do
    -- translate inputs
    specTRC@(SpecTRC specEnv specState specSignal) <-
      String -> ImpM t (SpecTRC rule era) -> ImpM t (SpecTRC rule era)
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating inputs" (ImpM t (SpecTRC rule era) -> ImpM t (SpecTRC rule era))
-> (Either Text (SpecTRC rule era) -> ImpM t (SpecTRC rule era))
-> Either Text (SpecTRC rule era)
-> ImpM t (SpecTRC rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text (SpecTRC rule era) -> ImpM t (SpecTRC rule era)
forall a b (m :: * -> *).
(HasCallStack, ToExpr a, NFData b, MonadIO m) =>
Either a b -> m b
expectRightDeepExpr (Either Text (SpecTRC rule era) -> ImpM t (SpecTRC rule era))
-> Either Text (SpecTRC rule era) -> ImpM t (SpecTRC rule era)
forall a b. (a -> b) -> a -> b
$ ExecContext rule era
-> TRC (EraRule rule era) -> Either Text (SpecTRC rule era)
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> TRC (EraRule rule era) -> Either Text (SpecTRC rule era)
translateInputs ExecContext rule era
ctx TRC (EraRule rule era)
trc
    -- get agda response
    agdaResponse' <-
      fmap (second $ first specNormalize) . evaluateDeep $ runAgdaRuleWithDebug @rule @era specTRC
    -- translate imp response
    let
      agdaResponse = ((SpecState rule era, Text) -> SpecState rule era)
-> Either Text (SpecState rule era, Text)
-> Either Text (SpecState rule era)
forall a b. (a -> b) -> Either Text a -> Either Text b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SpecState rule era, Text) -> SpecState rule era
forall a b. (a, b) -> a
fst Either Text (SpecState rule era, Text)
agdaResponse'
      agdaDebug = (Text -> Text)
-> ((SpecState rule era, Text) -> Text)
-> Either Text (SpecState rule era, Text)
-> Text
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Text -> Text -> Text
forall a b. a -> b -> a
const Text
"") (SpecState rule era, Text) -> Text
forall a b. (a, b) -> b
snd Either Text (SpecState rule era, Text)
agdaResponse'
      impRuleResult' = (NonEmpty (PredicateFailure (EraRule rule era)) -> Text)
-> ((State (EraRule rule era), [Event (EraRule rule era)])
    -> State (EraRule rule era))
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Either Text (State (EraRule rule 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 rule era)) -> String)
-> NonEmpty (PredicateFailure (EraRule rule era))
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (PredicateFailure (EraRule rule era)) -> String
forall a. Show a => a -> String
show) (State (EraRule rule era), [Event (EraRule rule era)])
-> State (EraRule rule era)
forall a b. (a, b) -> a
fst Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
impRuleResult
      impResponse = (Text -> Text)
-> Either Text (SpecState rule era)
-> Either Text (SpecState rule 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 rule era)
 -> Either Text (SpecState rule era))
-> (State (EraRule rule era) -> Either Text (SpecState rule era))
-> State (EraRule rule era)
-> Either Text (SpecState rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) era.
ExecSpecRule rule era =>
ExecContext rule era
-> TRC (EraRule rule era)
-> State (EraRule rule era)
-> Either Text (SpecState rule era)
translateOutput @rule @era ExecContext rule era
ctx TRC (EraRule rule era)
trc (State (EraRule rule era) -> Either Text (SpecState rule era))
-> Either Text (State (EraRule rule era))
-> Either Text (SpecState rule era)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Either Text (State (EraRule rule era))
impRuleResult'

    logString "implEnv"
    logToExpr env
    logString "implState"
    logToExpr state
    logString "implSignal"
    logToExpr signal
    logString "implStateOut"
    logToExpr impRuleResult
    logString "specEnv"
    logToExpr specEnv
    logString "specState"
    logToExpr specState
    logString "specSignal"
    logToExpr specSignal
    logString "specDebug"
    logToExpr agdaDebug
    logString "Extra info:"
    logDoc $
      extraInfo @rule @era
        globals
        ctx
        (TRC (env, state, signal))
        (first (T.pack . show) impRuleResult)
    logString "diffConformance:"
    logDoc $ diffConformance impResponse agdaResponse
    case (impResponse, agdaResponse) of
      (Right SpecState rule era
impRes, Right SpecState rule era
agdaRes)
        | SpecState rule era
impRes SpecState rule era -> SpecState rule era -> Bool
forall a. Eq a => a -> a -> Bool
== SpecState rule 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 rule era),
 Either Text (SpecState rule era))
_ -> String -> ImpM t ()
forall (m :: * -> *) a. (HasCallStack, MonadIO m) => String -> m a
assertFailure String
"Conformance failure"

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 TopTx era) ~ Agda.TxBody
  , SpecTranslate TxId (TxBody TopTx era)
  , SpecTranslate (ConwayLedgerExecContext era) (Tx TopTx era)
  , ToExpr (SpecRep (Tx TopTx 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 TopTx era) ~ TxBody,
 SpecTranslate TxId (TxBody TopTx era),
 SpecTranslate (ConwayLedgerExecContext era) (Tx TopTx era),
 ToExpr (SpecRep (Tx TopTx 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)) =
  Globals
-> ExecContext "LEDGER" era
-> TRC (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ImpM t ()
forall (rule :: Symbol) era t.
(ShelleyEraImp era, ExecSpecRule rule era,
 ToExpr (Event (EraRule rule era))) =>
Globals
-> ExecContext rule era
-> TRC (EraRule rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpM t ()
conformanceHook Globals
globals ExecContext "LEDGER" era
ConwayLedgerExecContext era
ctx TRC (EraRule "LEDGER" era)
trc
  where
    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)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL ((GovState era -> Const (StrictMaybe ScriptHash) (GovState era))
 -> UTxOState era -> Const (StrictMaybe ScriptHash) (UTxOState era))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> GovState era -> Const (StrictMaybe ScriptHash) (GovState 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)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Constitution era)
Lens' (GovState era) (Constitution era)
constitutionGovStateL ((Constitution era
  -> Const (StrictMaybe ScriptHash) (Constitution era))
 -> GovState era -> Const (StrictMaybe ScriptHash) (GovState era))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> Constitution era
    -> Const (StrictMaybe ScriptHash) (Constitution era))
-> (StrictMaybe ScriptHash
    -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
-> GovState era
-> Const (StrictMaybe ScriptHash) (GovState 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 TopTx era
uecTx = Tx TopTx 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)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL ((GovState era -> Const (PParams era) (GovState era))
 -> UTxOState era -> Const (PParams era) (UTxOState era))
-> ((PParams era -> Const (PParams era) (PParams era))
    -> GovState era -> Const (PParams era) (GovState 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)
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
                    }
              }
        }

epochBoundaryConformanceHook ::
  forall era t.
  ( ShelleyEraImp era
  , ExecSpecRule "NEWEPOCH" era
  , ExecContext "NEWEPOCH" era ~ ()
  , ToExpr (Event (EraRule "NEWEPOCH" era))
  ) =>
  Globals ->
  TRC (EraRule "NEWEPOCH" era) ->
  State (EraRule "NEWEPOCH" era) ->
  ImpM t ()
epochBoundaryConformanceHook :: forall era t.
(ShelleyEraImp era, ExecSpecRule "NEWEPOCH" era,
 ExecContext "NEWEPOCH" era ~ (),
 ToExpr (Event (EraRule "NEWEPOCH" era))) =>
Globals
-> TRC (EraRule "NEWEPOCH" era)
-> State (EraRule "NEWEPOCH" era)
-> ImpM t ()
epochBoundaryConformanceHook Globals
globals TRC (EraRule "NEWEPOCH" era)
trc State (EraRule "NEWEPOCH" era)
res =
  forall (rule :: Symbol) era t.
(ShelleyEraImp era, ExecSpecRule rule era,
 ToExpr (Event (EraRule rule era))) =>
Globals
-> ExecContext rule era
-> TRC (EraRule rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpM t ()
conformanceHook @"NEWEPOCH" @era Globals
globals () TRC (EraRule "NEWEPOCH" era)
trc (Either
   (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" era)))
   (State (EraRule "NEWEPOCH" era), [Event (EraRule "NEWEPOCH" era)])
 -> ImpM t ())
-> Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" era)))
     (State (EraRule "NEWEPOCH" era), [Event (EraRule "NEWEPOCH" era)])
-> ImpM t ()
forall a b. (a -> b) -> a -> b
$ (NewEpochState era, [Event (EraRule "NEWEPOCH" era)])
-> Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" era)))
     (NewEpochState era, [Event (EraRule "NEWEPOCH" era)])
forall a b. b -> Either a b
Right (State (EraRule "NEWEPOCH" era)
NewEpochState era
res, [])