{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger () where

import Data.Bifunctor (Bifunctor (..))
import Data.Functor.Identity (Identity)
import qualified Data.List.NonEmpty as NE

import Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe)
import Cardano.Ledger.Conway.Core (
  Era (..),
  EraPParams (..),
  EraTx,
  EraTxAuxData (..),
  EraTxBody (..),
  EraTxOut (..),
  EraTxWits (..),
  ScriptHash,
 )
import Cardano.Ledger.Conway.Rules (EnactState)

import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  FixupSpecRep (..),
  OpaqueErrorString (..),
  checkConformance,
  computationResultToEither,
  runSpecTransM,
  toTestRep,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Constrained.Conway (IsConwayUniv, UtxoExecContext (..), utxoStateSpec)
import Test.Cardano.Ledger.Conway.Arbitrary ()

import Cardano.Ledger.Conway (Conway)
import Constrained (
  Specification (..),
  assert,
  constrained,
  constrained',
  genFromSpec,
  lit,
  satisfies,
  (==.),
 )

import Cardano.Ledger.Binary (EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Shelley.Rules (UtxoEnv (..))
import Data.Bitraversable (bimapM)
import qualified Data.Text as T
import GHC.Generics (Generic)
import qualified Lib as Agda
import Test.Cardano.Ledger.Common (Arbitrary (..), NFData, Testable (..), ToExpr, ansiExpr)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (enactStateSpec)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext)
import Test.Cardano.Ledger.Conway.ImpTest (impAnn, logDoc, tryRunImpRuleNoAssertions)
import Test.Cardano.Ledger.Imp.Common (expectRightExpr)
import UnliftIO (evaluateDeep)

data ConwayLedgerExecContext era
  = ConwayLedgerExecContext
  { forall era.
ConwayLedgerExecContext era
-> StrictMaybe (ScriptHash (EraCrypto era))
clecPolicyHash :: StrictMaybe (ScriptHash (EraCrypto era))
  , forall era. ConwayLedgerExecContext era -> EnactState era
clecEnactState :: EnactState era
  , forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecUtxoExecContext :: UtxoExecContext era
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
forall era x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
$cto :: forall era x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
$cfrom :: forall era x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
Generic)

instance
  c ~ EraCrypto era =>
  Inject (ConwayLedgerExecContext era) (StrictMaybe (ScriptHash c))
  where
  inject :: ConwayLedgerExecContext era -> StrictMaybe (ScriptHash c)
inject = forall era.
ConwayLedgerExecContext era
-> StrictMaybe (ScriptHash (EraCrypto era))
clecPolicyHash

instance Inject (ConwayLedgerExecContext Conway) (EnactState Conway) where
  inject :: ConwayLedgerExecContext Conway -> EnactState Conway
inject = forall era. ConwayLedgerExecContext era -> EnactState era
clecEnactState

instance
  ( EraPParams era
  , EraTx era
  , NFData (TxWits era)
  , NFData (TxAuxData era)
  ) =>
  NFData (ConwayLedgerExecContext era)

instance
  ( EraTx era
  , ToExpr (TxOut era)
  , ToExpr (TxBody era)
  , ToExpr (TxWits era)
  , ToExpr (TxAuxData era)
  , ToExpr (PParamsHKD Identity era)
  ) =>
  ToExpr (ConwayLedgerExecContext era)

instance EraPParams era => EncCBOR (ConwayLedgerExecContext era) where
  encCBOR :: ConwayLedgerExecContext era -> Encoding
encCBOR ConwayLedgerExecContext {StrictMaybe (ScriptHash (EraCrypto era))
EnactState era
UtxoExecContext era
clecUtxoExecContext :: UtxoExecContext era
clecEnactState :: EnactState era
clecPolicyHash :: StrictMaybe (ScriptHash (EraCrypto era))
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecPolicyHash :: forall era.
ConwayLedgerExecContext era
-> StrictMaybe (ScriptHash (EraCrypto era))
..} =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$
      forall t. t -> Encode ('Closed 'Dense) t
Rec forall era.
StrictMaybe (ScriptHash (EraCrypto era))
-> EnactState era
-> UtxoExecContext era
-> ConwayLedgerExecContext era
ConwayLedgerExecContext
        forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To StrictMaybe (ScriptHash (EraCrypto era))
clecPolicyHash
        forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EnactState era
clecEnactState

instance
  forall fn.
  IsConwayUniv fn =>
  ExecSpecRule fn "LEDGER" Conway
  where
  type ExecContext fn "LEDGER" Conway = ConwayLedgerExecContext Conway

  genExecContext :: HasCallStack => Gen (ExecContext fn "LEDGER" Conway)
genExecContext = do
    ConwayEnactExecContext Conway
ctx <- forall a. Arbitrary a => Gen a
arbitrary
    ConwayExecEnactEnv Conway
env <- forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
    forall era.
StrictMaybe (ScriptHash (EraCrypto era))
-> EnactState era
-> UtxoExecContext era
-> ConwayLedgerExecContext era
ConwayLedgerExecContext
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayEnactExecContext Conway
-> ConwayExecEnactEnv Conway
-> Specification fn (EnactState Conway)
enactStateSpec ConwayEnactExecContext Conway
ctx ConwayExecEnactEnv Conway
env)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (UtxoExecContext Conway)
genUtxoExecContext

  environmentSpec :: HasCallStack =>
ExecContext fn "LEDGER" Conway
-> Specification fn (ExecEnvironment fn "LEDGER" Conway)
environmentSpec ConwayLedgerExecContext {StrictMaybe (ScriptHash (EraCrypto Conway))
EnactState Conway
UtxoExecContext Conway
clecUtxoExecContext :: UtxoExecContext Conway
clecEnactState :: EnactState Conway
clecPolicyHash :: StrictMaybe (ScriptHash (EraCrypto Conway))
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecPolicyHash :: forall era.
ConwayLedgerExecContext era
-> StrictMaybe (ScriptHash (EraCrypto era))
..} =
    let UtxoExecContext {AlonzoTx Conway
UTxO Conway
UtxoEnv Conway
uecTx :: forall era. UtxoExecContext era -> AlonzoTx era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecUtxoEnv :: UtxoEnv Conway
uecUTxO :: UTxO Conway
uecTx :: AlonzoTx Conway
..} = UtxoExecContext Conway
clecUtxoExecContext
     in forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term fn SlotNo
slotNo Term fn TxIx
_txIx Term fn (PParams Conway)
pp Term fn AccountState
_acntSt Term fn Bool
_mempool ->
          [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (PParams Conway)
pp forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall era. UtxoEnv era -> PParams era
uePParams UtxoEnv Conway
uecUtxoEnv)
          , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn SlotNo
slotNo forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall era. UtxoEnv era -> SlotNo
ueSlot UtxoEnv Conway
uecUtxoEnv)
          ]

  stateSpec :: HasCallStack =>
ExecContext fn "LEDGER" Conway
-> ExecEnvironment fn "LEDGER" Conway
-> Specification fn (ExecState fn "LEDGER" Conway)
stateSpec ConwayLedgerExecContext {StrictMaybe (ScriptHash (EraCrypto Conway))
EnactState Conway
UtxoExecContext Conway
clecUtxoExecContext :: UtxoExecContext Conway
clecEnactState :: EnactState Conway
clecPolicyHash :: StrictMaybe (ScriptHash (EraCrypto Conway))
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecPolicyHash :: forall era.
ConwayLedgerExecContext era
-> StrictMaybe (ScriptHash (EraCrypto era))
..} ExecEnvironment fn "LEDGER" Conway
_ =
    let UtxoExecContext {AlonzoTx Conway
UTxO Conway
UtxoEnv Conway
uecUtxoEnv :: UtxoEnv Conway
uecUTxO :: UTxO Conway
uecTx :: AlonzoTx Conway
uecTx :: forall era. UtxoExecContext era -> AlonzoTx era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
..} = UtxoExecContext Conway
clecUtxoExecContext
     in forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term fn (UTxOState Conway)
utxos Term fn (CertState Conway)
certState ->
          [ Term fn (UTxOState Conway)
utxos forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext Conway
-> UtxoEnv Conway -> Specification fn (UTxOState Conway)
utxoStateSpec UtxoExecContext Conway
clecUtxoExecContext UtxoEnv Conway
uecUtxoEnv
          , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (CertState Conway)
certState forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall era. UtxoEnv era -> CertState era
ueCertState UtxoEnv Conway
uecUtxoEnv)
          ]

  signalSpec :: HasCallStack =>
ExecContext fn "LEDGER" Conway
-> ExecEnvironment fn "LEDGER" Conway
-> ExecState fn "LEDGER" Conway
-> Specification fn (ExecSignal fn "LEDGER" Conway)
signalSpec ConwayLedgerExecContext {StrictMaybe (ScriptHash (EraCrypto Conway))
EnactState Conway
UtxoExecContext Conway
clecUtxoExecContext :: UtxoExecContext Conway
clecEnactState :: EnactState Conway
clecPolicyHash :: StrictMaybe (ScriptHash (EraCrypto Conway))
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecPolicyHash :: forall era.
ConwayLedgerExecContext era
-> StrictMaybe (ScriptHash (EraCrypto era))
..} ExecEnvironment fn "LEDGER" Conway
_ ExecState fn "LEDGER" Conway
_ =
    let UtxoExecContext {AlonzoTx Conway
UTxO Conway
UtxoEnv Conway
uecUtxoEnv :: UtxoEnv Conway
uecUTxO :: UTxO Conway
uecTx :: AlonzoTx Conway
uecTx :: forall era. UtxoExecContext era -> AlonzoTx era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
..} = UtxoExecContext Conway
clecUtxoExecContext
     in forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit AlonzoTx Conway
uecTx)

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "LEDGER" Conway)
-> SpecRep (ExecState fn "LEDGER" Conway)
-> SpecRep (ExecSignal fn "LEDGER" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "LEDGER" Conway))))
     (SpecRep (ExecState fn "LEDGER" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "LEDGER" Conway)
env SpecRep (ExecState fn "LEDGER" Conway)
st SpecRep (ExecSignal fn "LEDGER" Conway)
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\T_String_6
e -> String -> OpaqueErrorString
OpaqueErrorString (T_String_6 -> String
T.unpack T_String_6
e) forall a. a -> [a] -> NonEmpty a
NE.:| [])
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ LEnv -> LState -> Tx -> T_ComputationResult_48 T_String_6 LState
Agda.ledgerStep SpecRep (ExecEnvironment fn "LEDGER" Conway)
env SpecRep (ExecState fn "LEDGER" Conway)
st SpecRep (ExecSignal fn "LEDGER" Conway)
sig

  testConformance :: (ShelleyEraImp Conway,
 SpecTranslate
   (ExecContext fn "LEDGER" Conway) (State (EraRule "LEDGER" Conway)),
 ForAllExecSpecRep NFData fn "LEDGER" Conway,
 ForAllExecSpecRep ToExpr fn "LEDGER" Conway,
 NFData (SpecRep (PredicateFailure (EraRule "LEDGER" Conway))),
 ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" Conway))),
 Eq (SpecRep (PredicateFailure (EraRule "LEDGER" Conway))),
 Eq (SpecRep (ExecState fn "LEDGER" Conway)),
 Inject
   (State (EraRule "LEDGER" Conway)) (ExecState fn "LEDGER" Conway),
 SpecTranslate
   (ExecContext fn "LEDGER" Conway) (ExecState fn "LEDGER" Conway),
 FixupSpecRep
   (SpecRep (PredicateFailure (EraRule "LEDGER" Conway))),
 FixupSpecRep (SpecRep (ExecState fn "LEDGER" Conway)),
 Inject
   (ExecEnvironment fn "LEDGER" Conway)
   (Environment (EraRule "LEDGER" Conway)),
 Inject
   (ExecState fn "LEDGER" Conway) (State (EraRule "LEDGER" Conway)),
 Inject
   (ExecSignal fn "LEDGER" Conway) (Signal (EraRule "LEDGER" Conway)),
 EncCBOR (ExecContext fn "LEDGER" Conway),
 EncCBOR (Environment (EraRule "LEDGER" Conway)),
 EncCBOR (State (EraRule "LEDGER" Conway)),
 EncCBOR (Signal (EraRule "LEDGER" Conway)),
 ToExpr (ExecContext fn "LEDGER" Conway), HasCallStack) =>
ExecContext fn "LEDGER" Conway
-> ExecEnvironment fn "LEDGER" Conway
-> ExecState fn "LEDGER" Conway
-> ExecSignal fn "LEDGER" Conway
-> Property
testConformance ExecContext fn "LEDGER" Conway
ctx ExecEnvironment fn "LEDGER" Conway
env ExecState fn "LEDGER" Conway
st ExecSignal fn "LEDGER" Conway
sig = forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ do
    (LEnv
specEnv, LState
specSt, Tx
specSig) <-
      forall a era.
NFData a =>
String -> ImpTestM era a -> ImpTestM era a
impAnn String
"Translating the inputs" forall a b. (a -> b) -> a -> b
$
        forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> ExecContext fn rule era
-> ImpTestM
     era
     (SpecRep (ExecEnvironment fn rule era),
      SpecRep (ExecState fn rule era), SpecRep (ExecSignal fn rule era))
translateInputs @fn @"LEDGER" @Conway ExecEnvironment fn "LEDGER" Conway
env ExecState fn "LEDGER" Conway
st ExecSignal fn "LEDGER" Conway
sig ExecContext fn "LEDGER" Conway
ctx
    forall era.
HasCallStack =>
Doc AnsiStyle -> ImpTestM era AuxiliaryData
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"ctx:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecContext fn "LEDGER" Conway
ctx
    forall era.
HasCallStack =>
Doc AnsiStyle -> ImpTestM era AuxiliaryData
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implEnv:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecEnvironment fn "LEDGER" Conway
env
    forall era.
HasCallStack =>
Doc AnsiStyle -> ImpTestM era AuxiliaryData
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implSt:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecState fn "LEDGER" Conway
st
    forall era.
HasCallStack =>
Doc AnsiStyle -> ImpTestM era AuxiliaryData
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implSig:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecSignal fn "LEDGER" Conway
sig
    forall era.
HasCallStack =>
Doc AnsiStyle -> ImpTestM era AuxiliaryData
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specEnv:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr LEnv
specEnv
    forall era.
HasCallStack =>
Doc AnsiStyle -> ImpTestM era AuxiliaryData
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specSt:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr LState
specSt
    forall era.
HasCallStack =>
Doc AnsiStyle -> ImpTestM era AuxiliaryData
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specSig:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr Tx
specSig
    Either (NonEmpty OpaqueErrorString) LState
agdaResTest <-
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a. FixupSpecRep a => a -> a
fixup forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a. FixupSpecRep a => a -> a
fixup) forall a b. (a -> b) -> a -> b
$
        forall a era.
NFData a =>
String -> ImpTestM era a -> ImpTestM era a
impAnn String
"Deep evaluating Agda output" 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 :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
SpecRep (ExecEnvironment fn rule era)
-> SpecRep (ExecState fn rule era)
-> SpecRep (ExecSignal fn rule era)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
     (SpecRep (ExecState fn rule era))
runAgdaRule @fn @"LEDGER" @Conway LEnv
specEnv LState
specSt Tx
specSig
    -- TODO figure out why assertions are failing and then we can remove this
    -- whole method
    Either
  (NonEmpty (ConwayLedgerPredFailure Conway))
  (LedgerState Conway, [ConwayLedgerEvent Conway])
implRes <- forall (rule :: Symbol) era.
(STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase) =>
Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> ImpTestM
     era
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (State (EraRule rule era), [Event (EraRule rule era)]))
tryRunImpRuleNoAssertions @"LEDGER" @Conway (forall t s. Inject t s => t -> s
inject ExecEnvironment fn "LEDGER" Conway
env) (forall t s. Inject t s => t -> s
inject ExecState fn "LEDGER" Conway
st) (forall t s. Inject t s => t -> s
inject ExecSignal fn "LEDGER" Conway
sig)
    Either (NonEmpty OpaqueErrorString) (SpecRep (LedgerState Conway))
implResTest <-
      forall a era.
NFData a =>
String -> ImpTestM era a -> ImpTestM era a
impAnn String
"Translating implementation values to SpecRep" forall a b. (a -> b) -> a -> b
$
        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 T_String_6 a
runSpecTransM ExecContext fn "LEDGER" Conway
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 (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
(SpecTranslate ctx a, FixupSpecRep (SpecRep a)) =>
a -> SpecTransM ctx (SpecRep a)
toTestRep) (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 fn "LEDGER" Conway) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) Either
  (NonEmpty (ConwayLedgerPredFailure Conway))
  (LedgerState Conway, [ConwayLedgerEvent Conway])
implRes
    let extra :: Doc AnsiStyle
extra = forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Doc AnsiStyle
extraInfo @fn @"LEDGER" @Conway ExecContext fn "LEDGER" Conway
ctx (forall t s. Inject t s => t -> s
inject ExecEnvironment fn "LEDGER" Conway
env) (forall t s. Inject t s => t -> s
inject ExecState fn "LEDGER" Conway
st) (forall t s. Inject t s => t -> s
inject ExecSignal fn "LEDGER" Conway
sig)
    forall era.
HasCallStack =>
Doc AnsiStyle -> ImpTestM era AuxiliaryData
logDoc Doc AnsiStyle
extra
    forall (rule :: Symbol) era (fn :: [*] -> * -> *).
(Era era, ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (SpecRep (ExecState fn rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Eq (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
     (SpecRep (ExecState fn rule era))
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
     (SpecRep (ExecState fn rule era))
-> ImpTestM era AuxiliaryData
checkConformance @"LEDGER" @Conway @fn
      ExecContext fn "LEDGER" Conway
ctx
      (forall t s. Inject t s => t -> s
inject ExecEnvironment fn "LEDGER" Conway
env)
      (forall t s. Inject t s => t -> s
inject ExecState fn "LEDGER" Conway
st)
      (forall t s. Inject t s => t -> s
inject ExecSignal fn "LEDGER" Conway
sig)
      Either (NonEmpty OpaqueErrorString) (SpecRep (LedgerState Conway))
implResTest
      Either (NonEmpty OpaqueErrorString) LState
agdaResTest