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

Test.Cardano.Ledger.Conformance.ExecSpecRule.Core

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

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

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

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

genExecContextGen (ExecContext fn rule era) Source #

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

runAgdaRuleSpecRep (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 #

translateInputsExecEnvironment 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))) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property Source #

extraInfoExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → String Source #

Instances

Instances details
IsConwayUniv fn ⇒ 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 #

Methods

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

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

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

genExecContextGen (ExecContext fn "CERT" Conway) Source #

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

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

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

extraInfoExecContext fn "CERT" ConwayEnvironment (EraRule "CERT" Conway) → State (EraRule "CERT" Conway) → Signal (EraRule "CERT" Conway) → String 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 #

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) → String 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 #

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) → String 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 #

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) → String 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 #

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) → String 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 ⇒ ExecSpecRule fn "GOVCERT" Conway Source # 
Instance details

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

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 #

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) → String 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 #

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) → String 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 #

Methods

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

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

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

genExecContextGen (ExecContext fn "POOL" Conway) Source #

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

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

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

extraInfoExecContext fn "POOL" ConwayEnvironment (EraRule "POOL" Conway) → State (EraRule "POOL" Conway) → Signal (EraRule "POOL" Conway) → String 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 #

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) → String 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 #

Methods

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

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

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

genExecContextGen (ExecContext fn "UTXO" Conway) Source #

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

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

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

extraInfoExecContext fn "UTXO" ConwayEnvironment (EraRule "UTXO" Conway) → State (EraRule "UTXO" Conway) → Signal (EraRule "UTXO" Conway) → String 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))), 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))) ⇒ Property Source #

generatesWithin ∷ ∀ a. (NFData a, ToExpr a, Typeable a) ⇒ Gen a → 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)) ⇒ 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 ∷ (ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn 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 #