{-# 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 (Globals)
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Core (EraRule)
import Control.State.Transition
import Data.Bifunctor (Bifunctor (..))
import Data.Data (Proxy (..))
import Data.List.NonEmpty as NE
import Data.Text qualified as T
import GHC.TypeLits (symbolVal)
import Lens.Micro.Mtl (view, (.=))
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  ExecSpecTopLevelRule (..),
  SpecTRC (..),
  diffConformance,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecNormalize (..),
  runSpecTransM,
 )
import Test.Cardano.Ledger.Conway.ImpTest
import Test.Cardano.Ledger.Imp.Common hiding (Args)
import UnliftIO (evaluateDeep)

conformanceHook ::
  forall rule era.
  ( ExecSpecRule rule era
  , ToExpr (Event (EraRule rule era))
  ) =>
  Globals ->
  TRC (EraRule rule era) ->
  ExecContext rule era ->
  Either
    (NonEmpty (PredicateFailure (EraRule rule era)))
    (State (EraRule rule era), [Event (EraRule rule era)]) ->
  ImpTestM era ()
conformanceHook :: forall (rule :: Symbol) era.
(ExecSpecRule rule era, ToExpr (Event (EraRule rule era))) =>
Globals
-> TRC (EraRule rule era)
-> ExecContext rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpTestM era ()
conformanceHook Globals
globals trc :: TRC (EraRule rule era)
trc@(TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
state, Signal (EraRule rule era)
signal)) ExecContext rule era
ctx Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
impRuleResult = do
  String -> ImpM (LedgerSpec era) () -> ImpM (LedgerSpec era) ()
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 (LedgerSpec era) () -> ImpM (LedgerSpec era) ())
-> ImpM (LedgerSpec era) () -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ do
    String -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => String -> ImpM t ()
logString String
"Translating inputs"
    case ExecContext rule era
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
-> Either Text (SpecTRC rule era)
forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM ExecContext rule era
ctx (TRC (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
TRC (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
translateInputs TRC (EraRule rule era)
trc) of
      Left Text
err -> do
        ecd <- Getting Bool (ImpTestEnv era) Bool -> ImpM (LedgerSpec era) Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool (ImpTestEnv era) Bool
forall era (f :: * -> *).
Functor f =>
(Bool -> f Bool) -> ImpTestEnv era -> f (ImpTestEnv era)
iteExpectedConformanceFailureL
        if ecd
          then impConformanceFailureL .= True
          else assertFailure $ "Failed translation with: " <> show err
      Right SpecTRC rule era
strc -> do
        specTRC@(SpecTRC specEnv specState specSignal) <- SpecTRC rule era -> ImpM (LedgerSpec era) (SpecTRC rule era)
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep SpecTRC rule era
strc

        logString "Evaluating Agda rule"
        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 era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM @era ExecContext rule era
ctx (SpecTransM era (ExecContext rule era) (SpecState rule era)
 -> Either Text (SpecState rule era))
-> (State (EraRule rule era)
    -> SpecTransM era (ExecContext rule era) (SpecState rule era))
-> State (EraRule rule era)
-> Either Text (SpecState rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TRC (EraRule rule era)
-> State (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecState rule era)
forall (rule :: Symbol) era.
ExecSpecRule rule era =>
TRC (EraRule rule era)
-> State (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecState rule era)
translateOutput 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 (LedgerSpec era) ()
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          (Left Text
_, Left Text
_) -> () -> ImpM (LedgerSpec era) ()
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          (Either Text (SpecState rule era),
 Either Text (SpecState rule era))
_ -> do
            ecd <- Getting Bool (ImpTestEnv era) Bool -> ImpM (LedgerSpec era) Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool (ImpTestEnv era) Bool
forall era (f :: * -> *).
Functor f =>
(Bool -> f Bool) -> ImpTestEnv era -> f (ImpTestEnv era)
iteExpectedConformanceFailureL
            if ecd
              then
                impConformanceFailureL .= True
              else
                assertFailure "Conformance failure"

submitTxConformanceHook ::
  forall era.
  (HasCallStack, ExecSpecTopLevelRule "LEDGER" era) =>
  Globals ->
  TRC (EraRule "LEDGER" era) ->
  Either
    (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
    (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
  ImpTestM era ()
submitTxConformanceHook :: forall era.
(HasCallStack, ExecSpecTopLevelRule "LEDGER" era) =>
Globals
-> TRC (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ImpTestM era ()
submitTxConformanceHook Globals
globals TRC (EraRule "LEDGER" era)
trc =
  Globals
-> TRC (EraRule "LEDGER" era)
-> ExecContext "LEDGER" era
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ImpM (LedgerSpec era) ()
forall (rule :: Symbol) era.
(ExecSpecRule rule era, ToExpr (Event (EraRule rule era))) =>
Globals
-> TRC (EraRule rule era)
-> ExecContext rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpTestM era ()
conformanceHook Globals
globals TRC (EraRule "LEDGER" era)
trc (Globals -> TRC (EraRule "LEDGER" era) -> ExecContext "LEDGER" era
forall (rule :: Symbol) era.
ExecSpecTopLevelRule rule era =>
Globals -> TRC (EraRule rule era) -> ExecContext rule era
mkRuleExecContext Globals
globals TRC (EraRule "LEDGER" era)
trc)

epochBoundaryConformanceHook ::
  forall era.
  ( ExecSpecTopLevelRule "NEWEPOCH" era
  , ToExpr (Event (EraRule "NEWEPOCH" era))
  ) =>
  Globals ->
  TRC (EraRule "NEWEPOCH" era) ->
  State (EraRule "NEWEPOCH" era) ->
  ImpTestM era ()
epochBoundaryConformanceHook :: forall era.
(ExecSpecTopLevelRule "NEWEPOCH" era,
 ToExpr (Event (EraRule "NEWEPOCH" era))) =>
Globals
-> TRC (EraRule "NEWEPOCH" era)
-> State (EraRule "NEWEPOCH" era)
-> ImpTestM era ()
epochBoundaryConformanceHook Globals
globals TRC (EraRule "NEWEPOCH" era)
trc State (EraRule "NEWEPOCH" era)
implRes =
  forall (rule :: Symbol) era.
(ExecSpecRule rule era, ToExpr (Event (EraRule rule era))) =>
Globals
-> TRC (EraRule rule era)
-> ExecContext rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpTestM era ()
conformanceHook @"NEWEPOCH" @era Globals
globals TRC (EraRule "NEWEPOCH" era)
trc (Globals
-> TRC (EraRule "NEWEPOCH" era) -> ExecContext "NEWEPOCH" era
forall (rule :: Symbol) era.
ExecSpecTopLevelRule rule era =>
Globals -> TRC (EraRule rule era) -> ExecContext rule era
mkRuleExecContext Globals
globals TRC (EraRule "NEWEPOCH" era)
trc) (Either
   (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" era)))
   (State (EraRule "NEWEPOCH" era), [Event (EraRule "NEWEPOCH" era)])
 -> ImpTestM era ())
-> Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" era)))
     (State (EraRule "NEWEPOCH" era), [Event (EraRule "NEWEPOCH" era)])
-> ImpTestM era ()
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 (NewEpochState era
State (EraRule "NEWEPOCH" era)
implRes, [])