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

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

import Data.Bifunctor (Bifunctor (..))
import Data.Functor.Identity (Identity)

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

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

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

import Cardano.Ledger.Binary (EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Shelley.LedgerState (LedgerState (..))
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..), UtxoEnv (..))
import Data.Bitraversable (bimapM)
import GHC.Generics (Generic)
import Lens.Micro.Mtl (use)
import qualified MAlonzo.Code.Ledger.Foreign.API 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.Conformance.ExecSpecRule.Conway.Utxow ()
import Test.Cardano.Ledger.Conway.ImpTest (impAnn, impGlobalsL, logDoc, tryRunImpRuleNoAssertions)
import Test.Cardano.Ledger.Imp.Common (expectRightExpr)
import Test.Cardano.Ledger.Shelley.Utils (runSTS)
import UnliftIO (evaluateDeep)

data ConwayLedgerExecContext era
  = ConwayLedgerExecContext
  { forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecPolicyHash :: StrictMaybe ScriptHash
  , 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 Inject (ConwayLedgerExecContext era) (StrictMaybe ScriptHash) where
  inject :: ConwayLedgerExecContext era -> StrictMaybe ScriptHash
inject = forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecPolicyHash

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

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

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

instance EraPParams era => EncCBOR (ConwayLedgerExecContext era) where
  encCBOR :: ConwayLedgerExecContext era -> Encoding
encCBOR ConwayLedgerExecContext {StrictMaybe ScriptHash
EnactState era
UtxoExecContext era
clecUtxoExecContext :: UtxoExecContext era
clecEnactState :: EnactState era
clecPolicyHash :: StrictMaybe ScriptHash
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
..} =
    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
-> 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
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 ExecSpecRule "LEDGER" ConwayEra where
  type ExecContext "LEDGER" ConwayEra = ConwayLedgerExecContext ConwayEra

  genExecContext :: HasCallStack => Gen (ExecContext "LEDGER" ConwayEra)
genExecContext = do
    ConwayEnactExecContext ConwayEra
ctx <- forall a. Arbitrary a => Gen a
arbitrary
    ConwayExecEnactEnv ConwayEra
env <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec forall a. Specification a
TrueSpec
    forall era.
StrictMaybe ScriptHash
-> 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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> Specification (EnactState ConwayEra)
enactStateSpec ConwayEnactExecContext ConwayEra
ctx ConwayExecEnactEnv ConwayEra
env)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (UtxoExecContext ConwayEra)
genUtxoExecContext

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

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

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "LEDGER" ConwayEra)
-> SpecRep (ExecState "LEDGER" ConwayEra)
-> SpecRep (ExecSignal "LEDGER" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "LEDGER" ConwayEra)
env SpecRep (ExecState "LEDGER" ConwayEra)
st SpecRep (ExecSignal "LEDGER" ConwayEra)
sig = forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$ LEnv -> LState -> Tx -> T_ComputationResult_46 Text LState
Agda.ledgerStep SpecRep (ExecEnvironment "LEDGER" ConwayEra)
env SpecRep (ExecState "LEDGER" ConwayEra)
st SpecRep (ExecSignal "LEDGER" ConwayEra)
sig

  extraInfo :: HasCallStack =>
Globals
-> ExecContext "LEDGER" ConwayEra
-> Environment (EraRule "LEDGER" ConwayEra)
-> State (EraRule "LEDGER" ConwayEra)
-> Signal (EraRule "LEDGER" ConwayEra)
-> Either
     OpaqueErrorString
     (State (EraRule "LEDGER" ConwayEra),
      [Event (EraRule "LEDGER" ConwayEra)])
-> Doc AnsiStyle
extraInfo
    Globals
globals
    ConwayLedgerExecContext {StrictMaybe ScriptHash
EnactState ConwayEra
UtxoExecContext ConwayEra
clecUtxoExecContext :: UtxoExecContext ConwayEra
clecEnactState :: EnactState ConwayEra
clecPolicyHash :: StrictMaybe ScriptHash
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
..}
    LedgerEnv {Maybe EpochNo
ChainAccountState
PParams ConwayEra
TxIx
SlotNo
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerAccount :: forall era. LedgerEnv era -> ChainAccountState
ledgerAccount :: ChainAccountState
ledgerPp :: PParams ConwayEra
ledgerIx :: TxIx
ledgerEpochNo :: Maybe EpochNo
ledgerSlotNo :: SlotNo
..}
    LedgerState {CertState ConwayEra
UTxOState ConwayEra
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsCertState :: forall era. LedgerState era -> CertState era
lsCertState :: CertState ConwayEra
lsUTxOState :: UTxOState ConwayEra
..}
    Signal (EraRule "LEDGER" ConwayEra)
sig
    Either
  OpaqueErrorString
  (State (EraRule "LEDGER" ConwayEra),
   [Event (EraRule "LEDGER" ConwayEra)])
_ =
      forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Globals
-> ExecContext rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     OpaqueErrorString
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @"UTXOW" @ConwayEra
        Globals
globals
        UtxoExecContext ConwayEra
clecUtxoExecContext
        UtxoEnv ConwayEra
utxoEnv
        UTxOState ConwayEra
lsUTxOState
        Signal (EraRule "LEDGER" ConwayEra)
sig
        Either
  OpaqueErrorString
  (State (EraRule "UTXOW" ConwayEra),
   [Event (EraRule "UTXOW" ConwayEra)])
stFinal
      where
        utxoEnv :: UtxoEnv ConwayEra
utxoEnv = forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
ledgerSlotNo PParams ConwayEra
ledgerPp CertState ConwayEra
lsCertState
        stFinal :: Either
  OpaqueErrorString
  (State (EraRule "UTXOW" ConwayEra),
   [Event (EraRule "UTXOW" ConwayEra)])
stFinal =
          forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString forall a b. (a -> b) -> a -> b
$
            forall (rule :: Symbol) era.
(BaseM (EraRule rule era) ~ ShelleyBase, STS (EraRule rule era)) =>
Globals
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
runSTS @"UTXOW" @ConwayEra Globals
globals UtxoEnv ConwayEra
utxoEnv UTxOState ConwayEra
lsUTxOState Signal (EraRule "LEDGER" ConwayEra)
sig

  testConformance :: (ShelleyEraImp ConwayEra,
 SpecTranslate
   (ExecContext "LEDGER" ConwayEra)
   (State (EraRule "LEDGER" ConwayEra)),
 ForAllExecSpecRep NFData "LEDGER" ConwayEra,
 ForAllExecSpecRep ToExpr "LEDGER" ConwayEra,
 NFData (SpecRep (PredicateFailure (EraRule "LEDGER" ConwayEra))),
 ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" ConwayEra))),
 Eq (SpecRep (PredicateFailure (EraRule "LEDGER" ConwayEra))),
 Eq (SpecRep (ExecState "LEDGER" ConwayEra)),
 Inject
   (State (EraRule "LEDGER" ConwayEra))
   (ExecState "LEDGER" ConwayEra),
 SpecTranslate
   (ExecContext "LEDGER" ConwayEra) (ExecState "LEDGER" ConwayEra),
 FixupSpecRep
   (SpecRep (PredicateFailure (EraRule "LEDGER" ConwayEra))),
 FixupSpecRep (SpecRep (ExecState "LEDGER" ConwayEra)),
 Inject
   (ExecEnvironment "LEDGER" ConwayEra)
   (Environment (EraRule "LEDGER" ConwayEra)),
 Inject
   (ExecState "LEDGER" ConwayEra)
   (State (EraRule "LEDGER" ConwayEra)),
 Inject
   (ExecSignal "LEDGER" ConwayEra)
   (Signal (EraRule "LEDGER" ConwayEra)),
 EncCBOR (ExecContext "LEDGER" ConwayEra),
 EncCBOR (Environment (EraRule "LEDGER" ConwayEra)),
 EncCBOR (State (EraRule "LEDGER" ConwayEra)),
 EncCBOR (Signal (EraRule "LEDGER" ConwayEra)),
 ToExpr (ExecContext "LEDGER" ConwayEra),
 ToExpr (PredicateFailure (EraRule "LEDGER" ConwayEra)),
 NFData (PredicateFailure (EraRule "LEDGER" ConwayEra)),
 HasCallStack) =>
ExecContext "LEDGER" ConwayEra
-> ExecEnvironment "LEDGER" ConwayEra
-> ExecState "LEDGER" ConwayEra
-> ExecSignal "LEDGER" ConwayEra
-> Property
testConformance ExecContext "LEDGER" ConwayEra
ctx ExecEnvironment "LEDGER" ConwayEra
env ExecState "LEDGER" ConwayEra
st ExecSignal "LEDGER" ConwayEra
sig = forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ do
    (LEnv
specEnv, LState
specSt, Tx
specSig) <-
      forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating the inputs" forall a b. (a -> b) -> a -> b
$
        forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecEnvironment rule era
-> ExecState rule era
-> ExecSignal rule era
-> ExecContext rule era
-> ImpTestM
     era
     (SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
      SpecRep (ExecSignal rule era))
translateInputs @"LEDGER" @ConwayEra ExecEnvironment "LEDGER" ConwayEra
env ExecState "LEDGER" ConwayEra
st ExecSignal "LEDGER" ConwayEra
sig ExecContext "LEDGER" ConwayEra
ctx
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
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 "LEDGER" ConwayEra
ctx
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
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 "LEDGER" ConwayEra
env
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
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 "LEDGER" ConwayEra
st
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
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 "LEDGER" ConwayEra
sig
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
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 t. HasCallStack => Doc AnsiStyle -> ImpM t ()
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 t. HasCallStack => Doc AnsiStyle -> ImpM t ()
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 OpaqueErrorString LState
agdaResTest <-
      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 a t. NFData a => String -> ImpM t a -> ImpM t 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 (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" @ConwayEra LEnv
specEnv LState
specSt Tx
specSig
    -- TODO figure out why assertions are failing and then we can remove this
    -- whole method
    Either
  (NonEmpty (ConwayLedgerPredFailure ConwayEra))
  (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
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" @ConwayEra (forall t s. Inject t s => t -> s
inject ExecEnvironment "LEDGER" ConwayEra
env) (forall t s. Inject t s => t -> s
inject ExecState "LEDGER" ConwayEra
st) (forall t s. Inject t s => t -> s
inject ExecSignal "LEDGER" ConwayEra
sig)
    Either OpaqueErrorString (SpecRep (LedgerState ConwayEra))
implResTest <-
      forall a t. NFData a => String -> ImpM t a -> ImpM t 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 Text a
runSpecTransM ExecContext "LEDGER" ConwayEra
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 b. Functor f => (a -> b) -> f a -> f b
fmap forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 "LEDGER" ConwayEra) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
              Either
  (NonEmpty (ConwayLedgerPredFailure ConwayEra))
  (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
implRes
    Globals
globals <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use forall era. Lens' (ImpTestState era) Globals
impGlobalsL
    let extra :: Doc AnsiStyle
extra =
          forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Globals
-> ExecContext rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     OpaqueErrorString
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @"LEDGER" @ConwayEra
            Globals
globals
            ExecContext "LEDGER" ConwayEra
ctx
            (forall t s. Inject t s => t -> s
inject ExecEnvironment "LEDGER" ConwayEra
env)
            (forall t s. Inject t s => t -> s
inject ExecState "LEDGER" ConwayEra
st)
            (forall t s. Inject t s => t -> s
inject ExecSignal "LEDGER" ConwayEra
sig)
            (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either
  (NonEmpty (ConwayLedgerPredFailure ConwayEra))
  (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
implRes)
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc Doc AnsiStyle
extra
    forall (rule :: Symbol) era.
(Era era, ToExpr (SpecRep (ExecState rule era)),
 Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> ImpTestM era ()
checkConformance @"LEDGER" @ConwayEra
      ExecContext "LEDGER" ConwayEra
ctx
      (forall t s. Inject t s => t -> s
inject ExecEnvironment "LEDGER" ConwayEra
env)
      (forall t s. Inject t s => t -> s
inject ExecState "LEDGER" ConwayEra
st)
      (forall t s. Inject t s => t -> s
inject ExecSignal "LEDGER" ConwayEra
sig)
      Either OpaqueErrorString (SpecRep (LedgerState ConwayEra))
implResTest
      Either OpaqueErrorString LState
agdaResTest