cardano-ledger-conformance-0.1.0.0: Testing utilities for conformance testing
Safe HaskellSafe-Inferred
LanguageHaskell2010

Test.Cardano.Ledger.Conformance.ExecSpecRule.Core

Synopsis

Documentation

class (ForAllExecTypes (HasSpec fn) fn rule era, ForAllExecTypes ToExpr fn rule era, ForAllExecTypes NFData fn rule era, KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext fn rule era) (PredicateFailure (EraRule rule era)), Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era)), Inject (ExecState fn rule era) (State (EraRule rule era)), Inject (ExecSignal fn rule era) (Signal (EraRule rule era))) ⇒ ExecSpecRule fn (rule ∷ Symbol) era where Source #

Minimal complete definition

environmentSpec, stateSpec, signalSpec, runAgdaRule

Associated Types

type ExecContext fn rule era Source #

type ExecContext fn rule era = ()

type ExecEnvironment fn rule era Source #

type ExecEnvironment fn rule era = Environment (EraRule rule era)

type ExecState fn rule era Source #

type ExecState fn rule era = State (EraRule rule era)

type ExecSignal fn rule era Source #

type ExecSignal fn rule era = Signal (EraRule rule era)

Methods

environmentSpecHasCallStackExecContext fn rule era → Specification fn (ExecEnvironment fn rule era) Source #

stateSpecHasCallStackExecContext fn rule era → ExecEnvironment fn rule era → Specification fn (ExecState fn rule era) Source #

signalSpecHasCallStackExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → Specification fn (ExecSignal fn rule era) Source #

classOfExecSignal fn rule era → Maybe String Source #

genExecContextHasCallStackGen (ExecContext fn rule era) Source #

default genExecContextArbitrary (ExecContext fn rule era) ⇒ Gen (ExecContext fn rule era) Source #

runAgdaRuleHasCallStackSpecRep (ExecEnvironment fn rule era) → SpecRep (ExecState fn rule era) → SpecRep (ExecSignal fn rule era) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) Source #

translateInputsHasCallStackExecEnvironment 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)) Source #

default translateInputs ∷ (ForAllExecTypes (SpecTranslate (ExecContext fn rule era)) fn rule era, ForAllExecSpecRep ToExpr fn rule era) ⇒ 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)) Source #

testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era)), Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era)), Inject (ExecState fn rule era) (State (EraRule rule era)), Inject (ExecSignal fn rule era) (Signal (EraRule rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property Source #

extraInfoHasCallStackExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Doc AnsiStyle Source #

Instances

Instances details
(IsConwayUniv fn, Inject (ConwayCertExecContext Conway) (Map (RewardAccount StandardCrypto) Coin)) ⇒ ExecSpecRule fn "CERT" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert

Associated Types

type ExecContext fn "CERT" Conway Source #

type ExecEnvironment fn "CERT" Conway Source #

type ExecState fn "CERT" Conway Source #

type ExecSignal fn "CERT" Conway Source #

IsConwayUniv fn ⇒ ExecSpecRule fn "CERTS" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs

Associated Types

type ExecContext fn "CERTS" Conway Source #

type ExecEnvironment fn "CERTS" Conway Source #

type ExecState fn "CERTS" Conway Source #

type ExecSignal fn "CERTS" Conway Source #

Methods

environmentSpecExecContext fn "CERTS" ConwaySpecification fn (ExecEnvironment fn "CERTS" Conway) Source #

stateSpecExecContext fn "CERTS" ConwayExecEnvironment fn "CERTS" ConwaySpecification fn (ExecState fn "CERTS" Conway) Source #

signalSpecExecContext fn "CERTS" ConwayExecEnvironment fn "CERTS" ConwayExecState fn "CERTS" ConwaySpecification fn (ExecSignal fn "CERTS" Conway) Source #

classOfExecSignal fn "CERTS" ConwayMaybe String Source #

genExecContextGen (ExecContext fn "CERTS" Conway) Source #

runAgdaRuleSpecRep (ExecEnvironment fn "CERTS" Conway) → SpecRep (ExecState fn "CERTS" Conway) → SpecRep (ExecSignal fn "CERTS" Conway) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "CERTS" Conway)))) (SpecRep (ExecState fn "CERTS" Conway)) Source #

translateInputsExecEnvironment fn "CERTS" ConwayExecState fn "CERTS" ConwayExecSignal fn "CERTS" ConwayExecContext fn "CERTS" ConwayImpTestM Conway (SpecRep (ExecEnvironment fn "CERTS" Conway), SpecRep (ExecState fn "CERTS" Conway), SpecRep (ExecSignal fn "CERTS" Conway)) Source #

testConformanceExecContext fn "CERTS" ConwayExecEnvironment fn "CERTS" ConwayExecState fn "CERTS" ConwayExecSignal fn "CERTS" ConwayProperty Source #

extraInfoExecContext fn "CERTS" ConwayEnvironment (EraRule "CERTS" Conway) → State (EraRule "CERTS" Conway) → Signal (EraRule "CERTS" Conway) → Doc AnsiStyle Source #

IsConwayUniv fn ⇒ ExecSpecRule fn "DELEG" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg

Associated Types

type ExecContext fn "DELEG" Conway Source #

type ExecEnvironment fn "DELEG" Conway Source #

type ExecState fn "DELEG" Conway Source #

type ExecSignal fn "DELEG" Conway Source #

Methods

environmentSpecExecContext fn "DELEG" ConwaySpecification fn (ExecEnvironment fn "DELEG" Conway) Source #

stateSpecExecContext fn "DELEG" ConwayExecEnvironment fn "DELEG" ConwaySpecification fn (ExecState fn "DELEG" Conway) Source #

signalSpecExecContext fn "DELEG" ConwayExecEnvironment fn "DELEG" ConwayExecState fn "DELEG" ConwaySpecification fn (ExecSignal fn "DELEG" Conway) Source #

classOfExecSignal fn "DELEG" ConwayMaybe String Source #

genExecContextGen (ExecContext fn "DELEG" Conway) Source #

runAgdaRuleSpecRep (ExecEnvironment fn "DELEG" Conway) → SpecRep (ExecState fn "DELEG" Conway) → SpecRep (ExecSignal fn "DELEG" Conway) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "DELEG" Conway)))) (SpecRep (ExecState fn "DELEG" Conway)) Source #

translateInputsExecEnvironment fn "DELEG" ConwayExecState fn "DELEG" ConwayExecSignal fn "DELEG" ConwayExecContext fn "DELEG" ConwayImpTestM Conway (SpecRep (ExecEnvironment fn "DELEG" Conway), SpecRep (ExecState fn "DELEG" Conway), SpecRep (ExecSignal fn "DELEG" Conway)) Source #

testConformanceExecContext fn "DELEG" ConwayExecEnvironment fn "DELEG" ConwayExecState fn "DELEG" ConwayExecSignal fn "DELEG" ConwayProperty Source #

extraInfoExecContext fn "DELEG" ConwayEnvironment (EraRule "DELEG" Conway) → State (EraRule "DELEG" Conway) → Signal (EraRule "DELEG" Conway) → Doc AnsiStyle Source #

IsConwayUniv fn ⇒ ExecSpecRule fn "ENACT" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Associated Types

type ExecContext fn "ENACT" Conway Source #

type ExecEnvironment fn "ENACT" Conway Source #

type ExecState fn "ENACT" Conway Source #

type ExecSignal fn "ENACT" Conway Source #

Methods

environmentSpecExecContext fn "ENACT" ConwaySpecification fn (ExecEnvironment fn "ENACT" Conway) Source #

stateSpecExecContext fn "ENACT" ConwayExecEnvironment fn "ENACT" ConwaySpecification fn (ExecState fn "ENACT" Conway) Source #

signalSpecExecContext fn "ENACT" ConwayExecEnvironment fn "ENACT" ConwayExecState fn "ENACT" ConwaySpecification fn (ExecSignal fn "ENACT" Conway) Source #

classOfExecSignal fn "ENACT" ConwayMaybe String Source #

genExecContextGen (ExecContext fn "ENACT" Conway) Source #

runAgdaRuleSpecRep (ExecEnvironment fn "ENACT" Conway) → SpecRep (ExecState fn "ENACT" Conway) → SpecRep (ExecSignal fn "ENACT" Conway) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "ENACT" Conway)))) (SpecRep (ExecState fn "ENACT" Conway)) Source #

translateInputsExecEnvironment fn "ENACT" ConwayExecState fn "ENACT" ConwayExecSignal fn "ENACT" ConwayExecContext fn "ENACT" ConwayImpTestM Conway (SpecRep (ExecEnvironment fn "ENACT" Conway), SpecRep (ExecState fn "ENACT" Conway), SpecRep (ExecSignal fn "ENACT" Conway)) Source #

testConformanceExecContext fn "ENACT" ConwayExecEnvironment fn "ENACT" ConwayExecState fn "ENACT" ConwayExecSignal fn "ENACT" ConwayProperty Source #

extraInfoExecContext fn "ENACT" ConwayEnvironment (EraRule "ENACT" Conway) → State (EraRule "ENACT" Conway) → Signal (EraRule "ENACT" Conway) → Doc AnsiStyle Source #

IsConwayUniv fn ⇒ ExecSpecRule fn "EPOCH" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Associated Types

type ExecContext fn "EPOCH" Conway Source #

type ExecEnvironment fn "EPOCH" Conway Source #

type ExecState fn "EPOCH" Conway Source #

type ExecSignal fn "EPOCH" Conway Source #

Methods

environmentSpecExecContext fn "EPOCH" ConwaySpecification fn (ExecEnvironment fn "EPOCH" Conway) Source #

stateSpecExecContext fn "EPOCH" ConwayExecEnvironment fn "EPOCH" ConwaySpecification fn (ExecState fn "EPOCH" Conway) Source #

signalSpecExecContext fn "EPOCH" ConwayExecEnvironment fn "EPOCH" ConwayExecState fn "EPOCH" ConwaySpecification fn (ExecSignal fn "EPOCH" Conway) Source #

classOfExecSignal fn "EPOCH" ConwayMaybe String Source #

genExecContextGen (ExecContext fn "EPOCH" Conway) Source #

runAgdaRuleSpecRep (ExecEnvironment fn "EPOCH" Conway) → SpecRep (ExecState fn "EPOCH" Conway) → SpecRep (ExecSignal fn "EPOCH" Conway) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "EPOCH" Conway)))) (SpecRep (ExecState fn "EPOCH" Conway)) Source #

translateInputsExecEnvironment fn "EPOCH" ConwayExecState fn "EPOCH" ConwayExecSignal fn "EPOCH" ConwayExecContext fn "EPOCH" ConwayImpTestM Conway (SpecRep (ExecEnvironment fn "EPOCH" Conway), SpecRep (ExecState fn "EPOCH" Conway), SpecRep (ExecSignal fn "EPOCH" Conway)) Source #

testConformanceExecContext fn "EPOCH" ConwayExecEnvironment fn "EPOCH" ConwayExecState fn "EPOCH" ConwayExecSignal fn "EPOCH" ConwayProperty Source #

extraInfoExecContext fn "EPOCH" ConwayEnvironment (EraRule "EPOCH" Conway) → State (EraRule "EPOCH" Conway) → Signal (EraRule "EPOCH" Conway) → Doc AnsiStyle Source #

(NFData (SpecRep (ConwayGovPredFailure Conway)), IsConwayUniv fn) ⇒ ExecSpecRule fn "GOV" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov

Associated Types

type ExecContext fn "GOV" Conway Source #

type ExecEnvironment fn "GOV" Conway Source #

type ExecState fn "GOV" Conway Source #

type ExecSignal fn "GOV" Conway Source #

(IsConwayUniv fn, Inject (ConwayCertExecContext Conway) (Map (DepositPurpose StandardCrypto) Coin)) ⇒ ExecSpecRule fn "GOVCERT" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert

Associated Types

type ExecContext fn "GOVCERT" Conway Source #

type ExecEnvironment fn "GOVCERT" Conway Source #

type ExecState fn "GOVCERT" Conway Source #

type ExecSignal fn "GOVCERT" Conway Source #

Methods

environmentSpecExecContext fn "GOVCERT" ConwaySpecification fn (ExecEnvironment fn "GOVCERT" Conway) Source #

stateSpecExecContext fn "GOVCERT" ConwayExecEnvironment fn "GOVCERT" ConwaySpecification fn (ExecState fn "GOVCERT" Conway) Source #

signalSpecExecContext fn "GOVCERT" ConwayExecEnvironment fn "GOVCERT" ConwayExecState fn "GOVCERT" ConwaySpecification fn (ExecSignal fn "GOVCERT" Conway) Source #

classOfExecSignal fn "GOVCERT" ConwayMaybe String Source #

genExecContextGen (ExecContext fn "GOVCERT" Conway) Source #

runAgdaRuleSpecRep (ExecEnvironment fn "GOVCERT" Conway) → SpecRep (ExecState fn "GOVCERT" Conway) → SpecRep (ExecSignal fn "GOVCERT" Conway) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "GOVCERT" Conway)))) (SpecRep (ExecState fn "GOVCERT" Conway)) Source #

translateInputsExecEnvironment fn "GOVCERT" ConwayExecState fn "GOVCERT" ConwayExecSignal fn "GOVCERT" ConwayExecContext fn "GOVCERT" ConwayImpTestM Conway (SpecRep (ExecEnvironment fn "GOVCERT" Conway), SpecRep (ExecState fn "GOVCERT" Conway), SpecRep (ExecSignal fn "GOVCERT" Conway)) Source #

testConformanceExecContext fn "GOVCERT" ConwayExecEnvironment fn "GOVCERT" ConwayExecState fn "GOVCERT" ConwayExecSignal fn "GOVCERT" ConwayProperty Source #

extraInfoExecContext fn "GOVCERT" ConwayEnvironment (EraRule "GOVCERT" Conway) → State (EraRule "GOVCERT" Conway) → Signal (EraRule "GOVCERT" Conway) → Doc AnsiStyle Source #

IsConwayUniv fn ⇒ ExecSpecRule fn "NEWEPOCH" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Associated Types

type ExecContext fn "NEWEPOCH" Conway Source #

type ExecEnvironment fn "NEWEPOCH" Conway Source #

type ExecState fn "NEWEPOCH" Conway Source #

type ExecSignal fn "NEWEPOCH" Conway Source #

Methods

environmentSpecExecContext fn "NEWEPOCH" ConwaySpecification fn (ExecEnvironment fn "NEWEPOCH" Conway) Source #

stateSpecExecContext fn "NEWEPOCH" ConwayExecEnvironment fn "NEWEPOCH" ConwaySpecification fn (ExecState fn "NEWEPOCH" Conway) Source #

signalSpecExecContext fn "NEWEPOCH" ConwayExecEnvironment fn "NEWEPOCH" ConwayExecState fn "NEWEPOCH" ConwaySpecification fn (ExecSignal fn "NEWEPOCH" Conway) Source #

classOfExecSignal fn "NEWEPOCH" ConwayMaybe String Source #

genExecContextGen (ExecContext fn "NEWEPOCH" Conway) Source #

runAgdaRuleSpecRep (ExecEnvironment fn "NEWEPOCH" Conway) → SpecRep (ExecState fn "NEWEPOCH" Conway) → SpecRep (ExecSignal fn "NEWEPOCH" Conway) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "NEWEPOCH" Conway)))) (SpecRep (ExecState fn "NEWEPOCH" Conway)) Source #

translateInputsExecEnvironment fn "NEWEPOCH" ConwayExecState fn "NEWEPOCH" ConwayExecSignal fn "NEWEPOCH" ConwayExecContext fn "NEWEPOCH" ConwayImpTestM Conway (SpecRep (ExecEnvironment fn "NEWEPOCH" Conway), SpecRep (ExecState fn "NEWEPOCH" Conway), SpecRep (ExecSignal fn "NEWEPOCH" Conway)) Source #

testConformanceExecContext fn "NEWEPOCH" ConwayExecEnvironment fn "NEWEPOCH" ConwayExecState fn "NEWEPOCH" ConwayExecSignal fn "NEWEPOCH" ConwayProperty Source #

extraInfoExecContext fn "NEWEPOCH" ConwayEnvironment (EraRule "NEWEPOCH" Conway) → State (EraRule "NEWEPOCH" Conway) → Signal (EraRule "NEWEPOCH" Conway) → Doc AnsiStyle Source #

IsConwayUniv fn ⇒ ExecSpecRule fn "POOL" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool

Associated Types

type ExecContext fn "POOL" Conway Source #

type ExecEnvironment fn "POOL" Conway Source #

type ExecState fn "POOL" Conway Source #

type ExecSignal fn "POOL" Conway Source #

IsConwayUniv fn ⇒ ExecSpecRule fn "RATIFY" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Associated Types

type ExecContext fn "RATIFY" Conway Source #

type ExecEnvironment fn "RATIFY" Conway Source #

type ExecState fn "RATIFY" Conway Source #

type ExecSignal fn "RATIFY" Conway Source #

Methods

environmentSpecExecContext fn "RATIFY" ConwaySpecification fn (ExecEnvironment fn "RATIFY" Conway) Source #

stateSpecExecContext fn "RATIFY" ConwayExecEnvironment fn "RATIFY" ConwaySpecification fn (ExecState fn "RATIFY" Conway) Source #

signalSpecExecContext fn "RATIFY" ConwayExecEnvironment fn "RATIFY" ConwayExecState fn "RATIFY" ConwaySpecification fn (ExecSignal fn "RATIFY" Conway) Source #

classOfExecSignal fn "RATIFY" ConwayMaybe String Source #

genExecContextGen (ExecContext fn "RATIFY" Conway) Source #

runAgdaRuleSpecRep (ExecEnvironment fn "RATIFY" Conway) → SpecRep (ExecState fn "RATIFY" Conway) → SpecRep (ExecSignal fn "RATIFY" Conway) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "RATIFY" Conway)))) (SpecRep (ExecState fn "RATIFY" Conway)) Source #

translateInputsExecEnvironment fn "RATIFY" ConwayExecState fn "RATIFY" ConwayExecSignal fn "RATIFY" ConwayExecContext fn "RATIFY" ConwayImpTestM Conway (SpecRep (ExecEnvironment fn "RATIFY" Conway), SpecRep (ExecState fn "RATIFY" Conway), SpecRep (ExecSignal fn "RATIFY" Conway)) Source #

testConformanceExecContext fn "RATIFY" ConwayExecEnvironment fn "RATIFY" ConwayExecState fn "RATIFY" ConwayExecSignal fn "RATIFY" ConwayProperty Source #

extraInfoExecContext fn "RATIFY" ConwayEnvironment (EraRule "RATIFY" Conway) → State (EraRule "RATIFY" Conway) → Signal (EraRule "RATIFY" Conway) → Doc AnsiStyle Source #

IsConwayUniv fn ⇒ ExecSpecRule fn "UTXO" Conway Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Associated Types

type ExecContext fn "UTXO" Conway Source #

type ExecEnvironment fn "UTXO" Conway Source #

type ExecState fn "UTXO" Conway Source #

type ExecSignal fn "UTXO" Conway Source #

conformsToImpl ∷ ∀ (rule ∷ Symbol) fn era. (ShelleyEraImp era, ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), NFData (ExecContext fn rule era), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext fn rule era), SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Inject (State (EraRule rule era)) (ExecState fn rule era), Eq (SpecRep (ExecState fn rule era)), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (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) ⇒ Property Source #

generatesWithin ∷ ∀ a. (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → IntSpec Source #

inputsGenerateWithin ∷ ∀ (fn ∷ [Type] → TypeType) (rule ∷ Symbol) era. ExecSpecRule fn rule era ⇒ IntSpec Source #

runConformance ∷ ∀ (rule ∷ Symbol) (fn ∷ [Type] → TypeType) era. (ExecSpecRule fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ImpTestM era (Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)), Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era))) Source #

checkConformance ∷ ∀ rule era fn. (Era era, ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) → ImpTestM era () Source #

defaultTestConformance ∷ ∀ fn era rule. (ShelleyEraImp era, ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (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)), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property Source #

translateWithContextSpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a) Source #

Translate a Haskell type a whose translation context is ctx into its Agda type, in the ImpTest monad.