{-# 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 Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  FixupSpecRep (..),
  checkConformance,
  runSpecTransM,
  showOpaqueErrorString,
  toTestRep,
  unComputationResult,
 )
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 (ConwayEra)
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.LedgerState (LedgerState (..))
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..), UtxoEnv (..))
import Data.Bitraversable (bimapM)
import GHC.Generics (Generic)
import Lens.Micro.Mtl (use)
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.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)
  ) =>
  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
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
  forall fn.
  IsConwayUniv fn =>
  ExecSpecRule fn "LEDGER" ConwayEra
  where
  type ExecContext fn "LEDGER" ConwayEra = ConwayLedgerExecContext ConwayEra

  genExecContext :: HasCallStack => Gen (ExecContext fn "LEDGER" ConwayEra)
genExecContext = do
    ConwayEnactExecContext ConwayEra
ctx <- forall a. Arbitrary a => Gen a
arbitrary
    ConwayExecEnactEnv ConwayEra
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
-> 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 ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> Specification fn (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 fn "LEDGER" ConwayEra
-> Specification fn (ExecEnvironment fn "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 {AlonzoTx ConwayEra
UTxO 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 (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 (Maybe EpochNo)
_ Term fn TxIx
_txIx Term fn (PParams ConwayEra)
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 ConwayEra)
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 ConwayEra
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 ConwayEra
uecUtxoEnv)
          ]

  stateSpec :: HasCallStack =>
ExecContext fn "LEDGER" ConwayEra
-> ExecEnvironment fn "LEDGER" ConwayEra
-> Specification fn (ExecState fn "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 fn "LEDGER" ConwayEra
_ =
    let UtxoExecContext {AlonzoTx ConwayEra
UTxO 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 (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 ConwayEra)
utxos Term fn (CertState ConwayEra)
certState ->
          [ Term fn (UTxOState ConwayEra)
utxos forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification fn (UTxOState ConwayEra)
utxoStateSpec UtxoExecContext ConwayEra
clecUtxoExecContext UtxoEnv ConwayEra
uecUtxoEnv
          , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (CertState ConwayEra)
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 ConwayEra
uecUtxoEnv)
          ]

  signalSpec :: HasCallStack =>
ExecContext fn "LEDGER" ConwayEra
-> ExecEnvironment fn "LEDGER" ConwayEra
-> ExecState fn "LEDGER" ConwayEra
-> Specification fn (ExecSignal fn "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 fn "LEDGER" ConwayEra
_ ExecState fn "LEDGER" ConwayEra
_ =
    let UtxoExecContext {AlonzoTx ConwayEra
UTxO 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 (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 ConwayEra
uecTx)

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "LEDGER" ConwayEra)
-> SpecRep (ExecState fn "LEDGER" ConwayEra)
-> SpecRep (ExecSignal fn "LEDGER" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "LEDGER" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "LEDGER" ConwayEra)
env SpecRep (ExecState fn "LEDGER" ConwayEra)
st SpecRep (ExecSignal fn "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 fn "LEDGER" ConwayEra)
env SpecRep (ExecState fn "LEDGER" ConwayEra)
st SpecRep (ExecSignal fn "LEDGER" ConwayEra)
sig

  extraInfo :: HasCallStack =>
Globals
-> ExecContext fn "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 {Bool
Maybe EpochNo
PParams ConwayEra
TxIx
SlotNo
AccountState
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 -> AccountState
ledgerMempool :: forall era. LedgerEnv era -> Bool
ledgerMempool :: Bool
ledgerAccount :: AccountState
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 (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Globals
-> ExecContext fn 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 @fn @"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 fn "LEDGER" ConwayEra)
   (State (EraRule "LEDGER" ConwayEra)),
 ForAllExecSpecRep NFData fn "LEDGER" ConwayEra,
 ForAllExecSpecRep ToExpr fn "LEDGER" ConwayEra,
 NFData (SpecRep (PredicateFailure (EraRule "LEDGER" ConwayEra))),
 ToExpr (SpecRep (PredicateFailure (EraRule "LEDGER" ConwayEra))),
 Eq (SpecRep (PredicateFailure (EraRule "LEDGER" ConwayEra))),
 Eq (SpecRep (ExecState fn "LEDGER" ConwayEra)),
 Inject
   (State (EraRule "LEDGER" ConwayEra))
   (ExecState fn "LEDGER" ConwayEra),
 SpecTranslate
   (ExecContext fn "LEDGER" ConwayEra)
   (ExecState fn "LEDGER" ConwayEra),
 FixupSpecRep
   (SpecRep (PredicateFailure (EraRule "LEDGER" ConwayEra))),
 FixupSpecRep (SpecRep (ExecState fn "LEDGER" ConwayEra)),
 Inject
   (ExecEnvironment fn "LEDGER" ConwayEra)
   (Environment (EraRule "LEDGER" ConwayEra)),
 Inject
   (ExecState fn "LEDGER" ConwayEra)
   (State (EraRule "LEDGER" ConwayEra)),
 Inject
   (ExecSignal fn "LEDGER" ConwayEra)
   (Signal (EraRule "LEDGER" ConwayEra)),
 EncCBOR (ExecContext fn "LEDGER" ConwayEra),
 EncCBOR (Environment (EraRule "LEDGER" ConwayEra)),
 EncCBOR (State (EraRule "LEDGER" ConwayEra)),
 EncCBOR (Signal (EraRule "LEDGER" ConwayEra)),
 ToExpr (ExecContext fn "LEDGER" ConwayEra),
 ToExpr (PredicateFailure (EraRule "LEDGER" ConwayEra)),
 NFData (PredicateFailure (EraRule "LEDGER" ConwayEra)),
 HasCallStack) =>
ExecContext fn "LEDGER" ConwayEra
-> ExecEnvironment fn "LEDGER" ConwayEra
-> ExecState fn "LEDGER" ConwayEra
-> ExecSignal fn "LEDGER" ConwayEra
-> Property
testConformance ExecContext fn "LEDGER" ConwayEra
ctx ExecEnvironment fn "LEDGER" ConwayEra
env ExecState fn "LEDGER" ConwayEra
st ExecSignal fn "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 (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" @ConwayEra ExecEnvironment fn "LEDGER" ConwayEra
env ExecState fn "LEDGER" ConwayEra
st ExecSignal fn "LEDGER" ConwayEra
sig ExecContext fn "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 fn "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 fn "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 fn "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 fn "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 (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 OpaqueErrorString (SpecRep (ExecState fn rule era))
runAgdaRule @fn @"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 fn "LEDGER" ConwayEra
env) (forall t s. Inject t s => t -> s
inject ExecState fn "LEDGER" ConwayEra
st) (forall t s. Inject t s => t -> s
inject ExecSignal fn "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 fn "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 fn "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 (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Globals
-> ExecContext fn 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 @fn @"LEDGER" @ConwayEra
            Globals
globals
            ExecContext fn "LEDGER" ConwayEra
ctx
            (forall t s. Inject t s => t -> s
inject ExecEnvironment fn "LEDGER" ConwayEra
env)
            (forall t s. Inject t s => t -> s
inject ExecState fn "LEDGER" ConwayEra
st)
            (forall t s. Inject t s => t -> s
inject ExecSignal fn "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 (fn :: [*] -> * -> *).
(Era era, ToExpr (SpecRep (ExecState fn 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 OpaqueErrorString (SpecRep (ExecState fn rule era))
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> ImpTestM era ()
checkConformance @"LEDGER" @ConwayEra @fn
      ExecContext fn "LEDGER" ConwayEra
ctx
      (forall t s. Inject t s => t -> s
inject ExecEnvironment fn "LEDGER" ConwayEra
env)
      (forall t s. Inject t s => t -> s
inject ExecState fn "LEDGER" ConwayEra
st)
      (forall t s. Inject t s => t -> s
inject ExecSignal fn "LEDGER" ConwayEra
sig)
      Either OpaqueErrorString (SpecRep (LedgerState ConwayEra))
implResTest
      Either OpaqueErrorString LState
agdaResTest