{-# 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 Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe)
import Cardano.Ledger.Binary (EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (
  EraPParams (..),
  EraTx (..),
  EraTxAuxData (..),
  EraTxBody (..),
  EraTxOut (..),
  EraTxWits (..),
  ScriptHash,
 )
import Cardano.Ledger.Conway.Rules (EnactState)
import Cardano.Ledger.Shelley.LedgerState (LedgerState (..))
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..), UtxoEnv (..))
import Cardano.Ledger.State (EraCertState (..))
import Constrained.API (
  assert,
  constrained,
  constrained',
  genFromSpec,
  lit,
  satisfies,
  (==.),
 )
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (bimapM)
import Data.Functor.Identity (Identity)
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 (..),
  FixupSpecRep (..),
  checkConformance,
  runSpecTransM,
  showOpaqueErrorString,
  toTestRep,
  unComputationResult,
 )
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.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Constrained.Conway (UtxoExecContext (..), utxoStateSpec)
import Test.Cardano.Ledger.Conway.Arbitrary ()
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 x.
 ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x)
-> (forall x.
    Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era)
-> Generic (ConwayLedgerExecContext era)
forall x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
forall x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
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
$cfrom :: forall era x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
from :: forall x.
ConwayLedgerExecContext era -> Rep (ConwayLedgerExecContext era) x
$cto :: forall era x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
to :: forall x.
Rep (ConwayLedgerExecContext era) x -> ConwayLedgerExecContext era
Generic)

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

instance Inject (ConwayLedgerExecContext ConwayEra) (EnactState ConwayEra) where
  inject :: ConwayLedgerExecContext ConwayEra -> EnactState ConwayEra
inject = ConwayLedgerExecContext ConwayEra -> EnactState ConwayEra
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 (Tx 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
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecPolicyHash :: StrictMaybe ScriptHash
clecEnactState :: EnactState era
clecUtxoExecContext :: UtxoExecContext era
..} =
    Encode
  ('Closed 'Dense)
  (UtxoExecContext era -> ConwayLedgerExecContext era)
-> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode
   ('Closed 'Dense)
   (UtxoExecContext era -> ConwayLedgerExecContext era)
 -> Encoding)
-> Encode
     ('Closed 'Dense)
     (UtxoExecContext era -> ConwayLedgerExecContext era)
-> Encoding
forall a b. (a -> b) -> a -> b
$
      (StrictMaybe ScriptHash
 -> EnactState era
 -> UtxoExecContext era
 -> ConwayLedgerExecContext era)
-> Encode
     ('Closed 'Dense)
     (StrictMaybe ScriptHash
      -> EnactState era
      -> UtxoExecContext era
      -> ConwayLedgerExecContext era)
forall t. t -> Encode ('Closed 'Dense) t
Rec StrictMaybe ScriptHash
-> EnactState era
-> UtxoExecContext era
-> ConwayLedgerExecContext era
forall era.
StrictMaybe ScriptHash
-> EnactState era
-> UtxoExecContext era
-> ConwayLedgerExecContext era
ConwayLedgerExecContext
        Encode
  ('Closed 'Dense)
  (StrictMaybe ScriptHash
   -> EnactState era
   -> UtxoExecContext era
   -> ConwayLedgerExecContext era)
-> Encode ('Closed 'Dense) (StrictMaybe ScriptHash)
-> Encode
     ('Closed 'Dense)
     (EnactState era
      -> UtxoExecContext era -> ConwayLedgerExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> StrictMaybe ScriptHash
-> Encode ('Closed 'Dense) (StrictMaybe ScriptHash)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To StrictMaybe ScriptHash
clecPolicyHash
        Encode
  ('Closed 'Dense)
  (EnactState era
   -> UtxoExecContext era -> ConwayLedgerExecContext era)
-> Encode ('Closed 'Dense) (EnactState era)
-> Encode
     ('Closed 'Dense)
     (UtxoExecContext era -> ConwayLedgerExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> EnactState era -> Encode ('Closed 'Dense) (EnactState era)
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 <- Gen (ConwayEnactExecContext ConwayEra)
forall a. Arbitrary a => Gen a
arbitrary
    ConwayExecEnactEnv ConwayEra
env <- Specification (ConwayExecEnactEnv ConwayEra)
-> Gen (ConwayExecEnactEnv ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification (ConwayExecEnactEnv ConwayEra)
forall a. Monoid a => a
mempty
    StrictMaybe ScriptHash
-> EnactState ConwayEra
-> UtxoExecContext ConwayEra
-> ConwayLedgerExecContext ConwayEra
forall era.
StrictMaybe ScriptHash
-> EnactState era
-> UtxoExecContext era
-> ConwayLedgerExecContext era
ConwayLedgerExecContext
      (StrictMaybe ScriptHash
 -> EnactState ConwayEra
 -> UtxoExecContext ConwayEra
 -> ConwayLedgerExecContext ConwayEra)
-> Gen (StrictMaybe ScriptHash)
-> Gen
     (EnactState ConwayEra
      -> UtxoExecContext ConwayEra -> ConwayLedgerExecContext ConwayEra)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (StrictMaybe ScriptHash)
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  (EnactState ConwayEra
   -> UtxoExecContext ConwayEra -> ConwayLedgerExecContext ConwayEra)
-> Gen (EnactState ConwayEra)
-> Gen
     (UtxoExecContext ConwayEra -> ConwayLedgerExecContext ConwayEra)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Specification (EnactState ConwayEra) -> Gen (EnactState ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> Specification (EnactState ConwayEra)
enactStateSpec ConwayEnactExecContext ConwayEra
ctx ConwayExecEnactEnv ConwayEra
env)
      Gen
  (UtxoExecContext ConwayEra -> ConwayLedgerExecContext ConwayEra)
-> Gen (UtxoExecContext ConwayEra)
-> Gen (ConwayLedgerExecContext ConwayEra)
forall a b. Gen (a -> b) -> Gen a -> Gen b
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
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecPolicyHash :: StrictMaybe ScriptHash
clecEnactState :: EnactState ConwayEra
clecUtxoExecContext :: UtxoExecContext ConwayEra
..} =
    let UtxoExecContext {Tx ConwayEra
UTxO ConwayEra
UtxoEnv ConwayEra
uecTx :: Tx ConwayEra
uecUTxO :: UTxO ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
uecTx :: forall era. UtxoExecContext era -> Tx era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
..} = UtxoExecContext ConwayEra
clecUtxoExecContext
     in FunTy
  (MapList
     Term (Args (SimpleRep (ExecEnvironment "LEDGER" ConwayEra))))
  [Pred]
-> Specification (ExecEnvironment "LEDGER" ConwayEra)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList
      Term (Args (SimpleRep (ExecEnvironment "LEDGER" ConwayEra))))
   [Pred]
 -> Specification (ExecEnvironment "LEDGER" ConwayEra))
-> FunTy
     (MapList
        Term (Args (SimpleRep (ExecEnvironment "LEDGER" ConwayEra))))
     [Pred]
-> Specification (ExecEnvironment "LEDGER" ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term SlotNo
slotNo TermD Deps (Maybe EpochNo)
_ TermD Deps TxIx
_txIx Term (PParams ConwayEra)
pp TermD Deps ChainAccountState
_acntSt ->
          [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (PParams ConwayEra)
pp Term (PParams ConwayEra) -> Term (PParams ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. PParams ConwayEra -> Term (PParams ConwayEra)
forall a. HasSpec a => a -> Term a
lit (UtxoEnv ConwayEra -> PParams ConwayEra
forall era. UtxoEnv era -> PParams era
uePParams UtxoEnv ConwayEra
uecUtxoEnv)
          , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term SlotNo
slotNo Term SlotNo -> Term SlotNo -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. SlotNo -> Term SlotNo
forall a. HasSpec a => a -> Term a
lit (UtxoEnv ConwayEra -> SlotNo
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
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecPolicyHash :: StrictMaybe ScriptHash
clecEnactState :: EnactState ConwayEra
clecUtxoExecContext :: UtxoExecContext ConwayEra
..} ExecEnvironment "LEDGER" ConwayEra
_ =
    let UtxoExecContext {Tx ConwayEra
UTxO ConwayEra
UtxoEnv ConwayEra
uecTx :: forall era. UtxoExecContext era -> Tx era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecTx :: Tx ConwayEra
uecUTxO :: UTxO ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
..} = UtxoExecContext ConwayEra
clecUtxoExecContext
     in FunTy
  (MapList Term (Args (SimpleRep (ExecState "LEDGER" ConwayEra))))
  [Pred]
-> Specification (ExecState "LEDGER" ConwayEra)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (ExecState "LEDGER" ConwayEra))))
   [Pred]
 -> Specification (ExecState "LEDGER" ConwayEra))
-> FunTy
     (MapList Term (Args (SimpleRep (ExecState "LEDGER" ConwayEra))))
     [Pred]
-> Specification (ExecState "LEDGER" ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (UTxOState ConwayEra)
utxos Term (ConwayCertState ConwayEra)
certState ->
          [ Term (UTxOState ConwayEra)
utxos Term (UTxOState ConwayEra)
-> Specification (UTxOState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification (UTxOState ConwayEra)
utxoStateSpec UtxoExecContext ConwayEra
clecUtxoExecContext UtxoEnv ConwayEra
uecUtxoEnv
          , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (ConwayCertState ConwayEra)
certState Term (ConwayCertState ConwayEra)
-> Term (ConwayCertState ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. ConwayCertState ConwayEra -> Term (ConwayCertState ConwayEra)
forall a. HasSpec a => a -> Term a
lit (UtxoEnv ConwayEra -> CertState ConwayEra
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
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecPolicyHash :: StrictMaybe ScriptHash
clecEnactState :: EnactState ConwayEra
clecUtxoExecContext :: UtxoExecContext ConwayEra
..} ExecEnvironment "LEDGER" ConwayEra
_ ExecState "LEDGER" ConwayEra
_ =
    let UtxoExecContext {Tx ConwayEra
UTxO ConwayEra
UtxoEnv ConwayEra
uecTx :: forall era. UtxoExecContext era -> Tx era
uecUTxO :: forall era. UtxoExecContext era -> UTxO era
uecUtxoEnv :: forall era. UtxoExecContext era -> UtxoEnv era
uecTx :: Tx ConwayEra
uecUTxO :: UTxO ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
..} = UtxoExecContext ConwayEra
clecUtxoExecContext
     in (Term (Tx ConwayEra) -> Term Bool) -> Specification (Tx ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (Term (Tx ConwayEra) -> Term (Tx ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Tx ConwayEra -> Term (Tx ConwayEra)
forall a. HasSpec a => a -> Term a
lit Tx 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 = ComputationResult Text LState -> Either OpaqueErrorString LState
forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult (ComputationResult Text LState -> Either OpaqueErrorString LState)
-> ComputationResult Text LState -> Either OpaqueErrorString LState
forall a b. (a -> b) -> a -> b
$ LEnv -> LState -> Tx -> ComputationResult Text LState
Agda.ledgerStep LEnv
SpecRep (ExecEnvironment "LEDGER" ConwayEra)
env LState
SpecRep (ExecState "LEDGER" ConwayEra)
st Tx
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
clecPolicyHash :: forall era. ConwayLedgerExecContext era -> StrictMaybe ScriptHash
clecEnactState :: forall era. ConwayLedgerExecContext era -> EnactState era
clecUtxoExecContext :: forall era. ConwayLedgerExecContext era -> UtxoExecContext era
clecPolicyHash :: StrictMaybe ScriptHash
clecEnactState :: EnactState ConwayEra
clecUtxoExecContext :: UtxoExecContext ConwayEra
..}
    LedgerEnv {Maybe EpochNo
PParams ConwayEra
ChainAccountState
TxIx
SlotNo
ledgerSlotNo :: SlotNo
ledgerEpochNo :: Maybe EpochNo
ledgerIx :: TxIx
ledgerPp :: PParams ConwayEra
ledgerAccount :: ChainAccountState
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
..}
    LedgerState {CertState ConwayEra
UTxOState ConwayEra
lsUTxOState :: UTxOState ConwayEra
lsCertState :: CertState ConwayEra
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsCertState :: forall era. LedgerState era -> CertState era
..}
    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
ExecContext "UTXOW" ConwayEra
clecUtxoExecContext
        UtxoEnv ConwayEra
Environment (EraRule "UTXOW" ConwayEra)
utxoEnv
        State (EraRule "UTXOW" ConwayEra)
UTxOState ConwayEra
lsUTxOState
        Signal (EraRule "UTXOW" ConwayEra)
Signal (EraRule "LEDGER" ConwayEra)
sig
        Either
  OpaqueErrorString
  (State (EraRule "UTXOW" ConwayEra),
   [Event (EraRule "UTXOW" ConwayEra)])
stFinal
      where
        utxoEnv :: UtxoEnv ConwayEra
utxoEnv = SlotNo
-> PParams ConwayEra -> CertState ConwayEra -> UtxoEnv ConwayEra
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 =
          (NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra))
 -> OpaqueErrorString)
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra)))
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
-> Either
     OpaqueErrorString
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
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 NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra))
-> OpaqueErrorString
NonEmpty (ConwayUtxowPredFailure ConwayEra) -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString (Either
   (NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra)))
   (State (EraRule "UTXOW" ConwayEra),
    [Event (EraRule "UTXOW" ConwayEra)])
 -> Either
      OpaqueErrorString
      (State (EraRule "UTXOW" ConwayEra),
       [Event (EraRule "UTXOW" ConwayEra)]))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" ConwayEra)))
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
-> Either
     OpaqueErrorString
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
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
Environment (EraRule "UTXOW" ConwayEra)
utxoEnv State (EraRule "UTXOW" ConwayEra)
UTxOState ConwayEra
lsUTxOState Signal (EraRule "UTXOW" ConwayEra)
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 = ImpM (LedgerSpec ConwayEra) () -> Property
forall prop. Testable prop => prop -> Property
property (ImpM (LedgerSpec ConwayEra) () -> Property)
-> ImpM (LedgerSpec ConwayEra) () -> Property
forall a b. (a -> b) -> a -> b
$ do
    (LEnv
specEnv, LState
specSt, Tx
specSig) <-
      String
-> ImpTestM
     ConwayEra
     (SpecRep (ExecEnvironment "LEDGER" ConwayEra),
      SpecRep (ExecState "LEDGER" ConwayEra),
      SpecRep (ExecSignal "LEDGER" ConwayEra))
-> ImpTestM
     ConwayEra
     (SpecRep (ExecEnvironment "LEDGER" ConwayEra),
      SpecRep (ExecState "LEDGER" ConwayEra),
      SpecRep (ExecSignal "LEDGER" ConwayEra))
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating the inputs" (ImpTestM
   ConwayEra
   (SpecRep (ExecEnvironment "LEDGER" ConwayEra),
    SpecRep (ExecState "LEDGER" ConwayEra),
    SpecRep (ExecSignal "LEDGER" ConwayEra))
 -> ImpTestM
      ConwayEra
      (SpecRep (ExecEnvironment "LEDGER" ConwayEra),
       SpecRep (ExecState "LEDGER" ConwayEra),
       SpecRep (ExecSignal "LEDGER" ConwayEra)))
-> ImpTestM
     ConwayEra
     (SpecRep (ExecEnvironment "LEDGER" ConwayEra),
      SpecRep (ExecState "LEDGER" ConwayEra),
      SpecRep (ExecSignal "LEDGER" ConwayEra))
-> ImpTestM
     ConwayEra
     (SpecRep (ExecEnvironment "LEDGER" ConwayEra),
      SpecRep (ExecState "LEDGER" ConwayEra),
      SpecRep (ExecSignal "LEDGER" ConwayEra))
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
    Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"ctx:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> ConwayLedgerExecContext ConwayEra -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecContext "LEDGER" ConwayEra
ConwayLedgerExecContext ConwayEra
ctx
    Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implEnv:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> LedgerEnv ConwayEra -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr LedgerEnv ConwayEra
ExecEnvironment "LEDGER" ConwayEra
env
    Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implSt:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> LedgerState ConwayEra -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr LedgerState ConwayEra
ExecState "LEDGER" ConwayEra
st
    Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implSig:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Tx ConwayEra -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr Tx ConwayEra
ExecSignal "LEDGER" ConwayEra
sig
    Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specEnv:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> LEnv -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr LEnv
specEnv
    Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specSt:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> LState -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr LState
specSt
    Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specSig:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Tx -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr Tx
specSig
    Either OpaqueErrorString LState
agdaResTest <-
      (Either OpaqueErrorString LState
 -> Either OpaqueErrorString LState)
-> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
-> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
forall a b.
(a -> b)
-> ImpM (LedgerSpec ConwayEra) a -> ImpM (LedgerSpec ConwayEra) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LState -> LState)
-> Either OpaqueErrorString LState
-> Either OpaqueErrorString LState
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second LState -> LState
forall a. FixupSpecRep a => a -> a
fixup) (ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
 -> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState))
-> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
-> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
forall a b. (a -> b) -> a -> b
$
        String
-> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
-> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Deep evaluating Agda output" (ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
 -> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState))
-> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
-> ImpM (LedgerSpec ConwayEra) (Either OpaqueErrorString LState)
forall a b. (a -> b) -> a -> b
$
          Either OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra))
-> ImpM
     (LedgerSpec ConwayEra)
     (Either OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra)))
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep (Either OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra))
 -> ImpM
      (LedgerSpec ConwayEra)
      (Either
         OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra))))
-> Either
     OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra))
-> ImpM
     (LedgerSpec ConwayEra)
     (Either OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra)))
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
SpecRep (ExecEnvironment "LEDGER" ConwayEra)
specEnv LState
SpecRep (ExecState "LEDGER" ConwayEra)
specSt Tx
SpecRep (ExecSignal "LEDGER" ConwayEra)
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 (LedgerEnv ConwayEra -> LedgerEnv ConwayEra
forall t s. Inject t s => t -> s
inject LedgerEnv ConwayEra
ExecEnvironment "LEDGER" ConwayEra
env) (LedgerState ConwayEra -> LedgerState ConwayEra
forall t s. Inject t s => t -> s
inject LedgerState ConwayEra
ExecState "LEDGER" ConwayEra
st) (Tx ConwayEra -> Tx ConwayEra
forall t s. Inject t s => t -> s
inject Tx ConwayEra
ExecSignal "LEDGER" ConwayEra
sig)
    Either OpaqueErrorString (SpecRep (LedgerState ConwayEra))
implResTest <-
      String
-> ImpM
     (LedgerSpec ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
-> ImpM
     (LedgerSpec ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating implementation values to SpecRep" (ImpM
   (LedgerSpec ConwayEra)
   (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
 -> ImpM
      (LedgerSpec ConwayEra)
      (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra))))
-> ImpM
     (LedgerSpec ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
-> ImpM
     (LedgerSpec ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
forall a b. (a -> b) -> a -> b
$
        Either
  Text (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
-> ImpM
     (LedgerSpec ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
forall a (m :: * -> *) b.
(HasCallStack, ToExpr a, MonadIO m) =>
Either a b -> m b
expectRightExpr (Either
   Text (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
 -> ImpM
      (LedgerSpec ConwayEra)
      (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra))))
-> Either
     Text (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
-> ImpM
     (LedgerSpec ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
forall a b. (a -> b) -> a -> b
$
          ConwayLedgerExecContext ConwayEra
-> SpecTransM
     (ConwayLedgerExecContext ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
-> Either
     Text (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext "LEDGER" ConwayEra
ConwayLedgerExecContext ConwayEra
ctx (SpecTransM
   (ConwayLedgerExecContext ConwayEra)
   (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
 -> Either
      Text (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra))))
-> SpecTransM
     (ConwayLedgerExecContext ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
-> Either
     Text (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
forall a b. (a -> b) -> a -> b
$
            (NonEmpty (ConwayLedgerPredFailure ConwayEra)
 -> SpecTransM
      (ConwayLedgerExecContext ConwayEra) OpaqueErrorString)
-> ((LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
    -> SpecTransM
         (ConwayLedgerExecContext ConwayEra)
         (SpecRep (LedgerState ConwayEra)))
-> Either
     (NonEmpty (ConwayLedgerPredFailure ConwayEra))
     (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
-> SpecTransM
     (ConwayLedgerExecContext ConwayEra)
     (Either OpaqueErrorString (SpecRep (LedgerState ConwayEra)))
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
              ((NonEmpty OpaqueErrorString -> OpaqueErrorString)
-> SpecTransM
     (ConwayLedgerExecContext ConwayEra) (NonEmpty OpaqueErrorString)
-> SpecTransM (ConwayLedgerExecContext ConwayEra) OpaqueErrorString
forall a b.
(a -> b)
-> SpecTransM (ConwayLedgerExecContext ConwayEra) a
-> SpecTransM (ConwayLedgerExecContext ConwayEra) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty OpaqueErrorString -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString (SpecTransM
   (ConwayLedgerExecContext ConwayEra) (NonEmpty OpaqueErrorString)
 -> SpecTransM
      (ConwayLedgerExecContext ConwayEra) OpaqueErrorString)
-> (NonEmpty (ConwayLedgerPredFailure ConwayEra)
    -> SpecTransM
         (ConwayLedgerExecContext ConwayEra) (NonEmpty OpaqueErrorString))
-> NonEmpty (ConwayLedgerPredFailure ConwayEra)
-> SpecTransM (ConwayLedgerExecContext ConwayEra) OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConwayLedgerPredFailure ConwayEra
 -> SpecTransM
      (ConwayLedgerExecContext ConwayEra) OpaqueErrorString)
-> NonEmpty (ConwayLedgerPredFailure ConwayEra)
-> SpecTransM
     (ConwayLedgerExecContext ConwayEra) (NonEmpty OpaqueErrorString)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse ConwayLedgerPredFailure ConwayEra
-> SpecTransM (ConwayLedgerExecContext ConwayEra) OpaqueErrorString
ConwayLedgerPredFailure ConwayEra
-> SpecTransM
     (ConwayLedgerExecContext ConwayEra)
     (SpecRep (ConwayLedgerPredFailure ConwayEra))
forall ctx a.
(SpecTranslate ctx a, FixupSpecRep (SpecRep a)) =>
a -> SpecTransM ctx (SpecRep a)
toTestRep)
              (LedgerState ConwayEra
-> SpecTransM
     (ConwayLedgerExecContext ConwayEra)
     (SpecRep (LedgerState ConwayEra))
forall ctx a.
(SpecTranslate ctx a, FixupSpecRep (SpecRep a)) =>
a -> SpecTransM ctx (SpecRep a)
toTestRep (LedgerState ConwayEra
 -> SpecTransM
      (ConwayLedgerExecContext ConwayEra)
      (SpecRep (LedgerState ConwayEra)))
-> ((LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
    -> LedgerState ConwayEra)
-> (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
-> SpecTransM
     (ConwayLedgerExecContext ConwayEra)
     (SpecRep (LedgerState ConwayEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s. Inject t s => t -> s
inject @_ @(ExecState "LEDGER" ConwayEra) (LedgerState ConwayEra -> LedgerState ConwayEra)
-> ((LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
    -> LedgerState ConwayEra)
-> (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
-> LedgerState ConwayEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
-> LedgerState ConwayEra
forall a b. (a, b) -> a
fst)
              Either
  (NonEmpty (ConwayLedgerPredFailure ConwayEra))
  (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
implRes
    Globals
globals <- Getting Globals (ImpTestState ConwayEra) Globals
-> ImpM (LedgerSpec ConwayEra) Globals
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting Globals (ImpTestState ConwayEra) Globals
forall era (f :: * -> *).
Functor f =>
(Globals -> f Globals) -> ImpTestState era -> f (ImpTestState era)
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
            (LedgerEnv ConwayEra -> LedgerEnv ConwayEra
forall t s. Inject t s => t -> s
inject LedgerEnv ConwayEra
ExecEnvironment "LEDGER" ConwayEra
env)
            (LedgerState ConwayEra -> LedgerState ConwayEra
forall t s. Inject t s => t -> s
inject LedgerState ConwayEra
ExecState "LEDGER" ConwayEra
st)
            (Tx ConwayEra -> Tx ConwayEra
forall t s. Inject t s => t -> s
inject Tx ConwayEra
ExecSignal "LEDGER" ConwayEra
sig)
            ((NonEmpty (ConwayLedgerPredFailure ConwayEra) -> OpaqueErrorString)
-> Either
     (NonEmpty (ConwayLedgerPredFailure ConwayEra))
     (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
-> Either
     OpaqueErrorString
     (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
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 NonEmpty (ConwayLedgerPredFailure ConwayEra) -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either
  (NonEmpty (ConwayLedgerPredFailure ConwayEra))
  (LedgerState ConwayEra, [ConwayLedgerEvent ConwayEra])
implRes)
    Doc AnsiStyle -> ImpM (LedgerSpec ConwayEra) ()
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
      (LedgerEnv ConwayEra -> LedgerEnv ConwayEra
forall t s. Inject t s => t -> s
inject LedgerEnv ConwayEra
ExecEnvironment "LEDGER" ConwayEra
env)
      (LedgerState ConwayEra -> LedgerState ConwayEra
forall t s. Inject t s => t -> s
inject LedgerState ConwayEra
ExecState "LEDGER" ConwayEra
st)
      (Tx ConwayEra -> Tx ConwayEra
forall t s. Inject t s => t -> s
inject Tx ConwayEra
ExecSignal "LEDGER" ConwayEra
sig)
      Either OpaqueErrorString (SpecRep (LedgerState ConwayEra))
Either OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra))
implResTest
      Either OpaqueErrorString LState
Either OpaqueErrorString (SpecRep (ExecState "LEDGER" ConwayEra))
agdaResTest