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

Test.Cardano.Ledger.Conformance.ExecSpecRule.Core

Documentation

class (ForAllRuleTypes (HasSpec fn) rule era, ForAllRuleTypes ToExpr rule era, ForAllRuleTypes NFData rule era, Eq (Event (EraRule rule era)), Typeable (Event (EraRule rule era)), KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext fn rule era) (PredicateFailure (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 = ()

Methods

environmentSpec ∷ ExecContext fn rule era → Specification fn (Environment (EraRule rule era)) Source #

stateSpec ∷ ExecContext fn rule era → Environment (EraRule rule era) → Specification fn (State (EraRule rule era)) Source #

signalSpec ∷ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Specification fn (Signal (EraRule rule era)) Source #

genExecContext ∷ Gen (ExecContext fn rule era) Source #

default genExecContext ∷ Arbitrary (ExecContext fn rule era) ⇒ Gen (ExecContext fn rule era) Source #

runAgdaRule ∷ SpecRep (Environment (EraRule rule era)) → SpecRep (State (EraRule rule era)) → SpecRep (Signal (EraRule rule era)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (State (EraRule rule era))) Source #

translateInputs ∷ Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → ExecContext fn rule era → ImpTestM era (SpecRep (Environment (EraRule rule era)), SpecRep (State (EraRule rule era)), SpecRep (Signal (EraRule rule era))) Source #

default translateInputs ∷ (ForAllRuleTypes (SpecTranslate (ExecContext fn rule era)) rule era, ToExpr (SpecRep (Environment (EraRule rule era))), ToExpr (SpecRep (State (EraRule rule era))), ToExpr (SpecRep (Signal (EraRule rule era)))) ⇒ Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → ExecContext fn rule era → ImpTestM era (SpecRep (Environment (EraRule rule era)), SpecRep (State (EraRule rule era)), SpecRep (Signal (EraRule rule era))) Source #

testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), NFData (SpecRep (Environment (EraRule rule era))), NFData (SpecRep (State (EraRule rule era))), NFData (SpecRep (Signal (EraRule rule era))), NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (Environment (EraRule rule era))), ToExpr (SpecRep (State (EraRule rule era))), ToExpr (SpecRep (Signal (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (State (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (State (EraRule rule era)))) ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Property Source #

Instances

Instances details
IsConwayUniv fn ⇒ ExecSpecRule fn "CERT" Conway Source # 
Instance details

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

Associated Types

type ExecContext fn "CERT" Conway Source #

Methods

environmentSpec ∷ ExecContext fn "CERT" Conway → Specification fn (Environment (EraRule "CERT" Conway)) Source #

stateSpec ∷ ExecContext fn "CERT" Conway → Environment (EraRule "CERT" Conway) → Specification fn (State (EraRule "CERT" Conway)) Source #

signalSpec ∷ ExecContext fn "CERT" Conway → Environment (EraRule "CERT" Conway) → State (EraRule "CERT" Conway) → Specification fn (Signal (EraRule "CERT" Conway)) Source #

genExecContext ∷ Gen (ExecContext fn "CERT" Conway) Source #

runAgdaRule ∷ SpecRep (Environment (EraRule "CERT" Conway)) → SpecRep (State (EraRule "CERT" Conway)) → SpecRep (Signal (EraRule "CERT" Conway)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "CERT" Conway)))) (SpecRep (State (EraRule "CERT" Conway))) Source #

translateInputs ∷ Environment (EraRule "CERT" Conway) → State (EraRule "CERT" Conway) → Signal (EraRule "CERT" Conway) → ExecContext fn "CERT" Conway → ImpTestM Conway (SpecRep (Environment (EraRule "CERT" Conway)), SpecRep (State (EraRule "CERT" Conway)), SpecRep (Signal (EraRule "CERT" Conway))) Source #

testConformance ∷ ExecContext fn "CERT" Conway → Environment (EraRule "CERT" Conway) → State (EraRule "CERT" Conway) → Signal (EraRule "CERT" Conway) → Property Source #

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

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

Associated Types

type ExecContext fn "GOV" Conway Source #

Methods

environmentSpec ∷ ExecContext fn "GOV" Conway → Specification fn (Environment (EraRule "GOV" Conway)) Source #

stateSpec ∷ ExecContext fn "GOV" Conway → Environment (EraRule "GOV" Conway) → Specification fn (State (EraRule "GOV" Conway)) Source #

signalSpec ∷ ExecContext fn "GOV" Conway → Environment (EraRule "GOV" Conway) → State (EraRule "GOV" Conway) → Specification fn (Signal (EraRule "GOV" Conway)) Source #

genExecContext ∷ Gen (ExecContext fn "GOV" Conway) Source #

runAgdaRule ∷ SpecRep (Environment (EraRule "GOV" Conway)) → SpecRep (State (EraRule "GOV" Conway)) → SpecRep (Signal (EraRule "GOV" Conway)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "GOV" Conway)))) (SpecRep (State (EraRule "GOV" Conway))) Source #

translateInputs ∷ Environment (EraRule "GOV" Conway) → State (EraRule "GOV" Conway) → Signal (EraRule "GOV" Conway) → ExecContext fn "GOV" Conway → ImpTestM Conway (SpecRep (Environment (EraRule "GOV" Conway)), SpecRep (State (EraRule "GOV" Conway)), SpecRep (Signal (EraRule "GOV" Conway))) Source #

testConformance ∷ ExecContext fn "GOV" Conway → Environment (EraRule "GOV" Conway) → State (EraRule "GOV" Conway) → Signal (EraRule "GOV" Conway) → Property Source #

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

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

Associated Types

type ExecContext fn "RATIFY" Conway Source #

Methods

environmentSpec ∷ ExecContext fn "RATIFY" Conway → Specification fn (Environment (EraRule "RATIFY" Conway)) Source #

stateSpec ∷ ExecContext fn "RATIFY" Conway → Environment (EraRule "RATIFY" Conway) → Specification fn (State (EraRule "RATIFY" Conway)) Source #

signalSpec ∷ ExecContext fn "RATIFY" Conway → Environment (EraRule "RATIFY" Conway) → State (EraRule "RATIFY" Conway) → Specification fn (Signal (EraRule "RATIFY" Conway)) Source #

genExecContext ∷ Gen (ExecContext fn "RATIFY" Conway) Source #

runAgdaRule ∷ SpecRep (Environment (EraRule "RATIFY" Conway)) → SpecRep (State (EraRule "RATIFY" Conway)) → SpecRep (Signal (EraRule "RATIFY" Conway)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "RATIFY" Conway)))) (SpecRep (State (EraRule "RATIFY" Conway))) Source #

translateInputs ∷ Environment (EraRule "RATIFY" Conway) → State (EraRule "RATIFY" Conway) → Signal (EraRule "RATIFY" Conway) → ExecContext fn "RATIFY" Conway → ImpTestM Conway (SpecRep (Environment (EraRule "RATIFY" Conway)), SpecRep (State (EraRule "RATIFY" Conway)), SpecRep (Signal (EraRule "RATIFY" Conway))) Source #

testConformance ∷ ExecContext fn "RATIFY" Conway → Environment (EraRule "RATIFY" Conway) → State (EraRule "RATIFY" Conway) → Signal (EraRule "RATIFY" Conway) → Property Source #

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

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

Associated Types

type ExecContext fn "UTXO" Conway Source #

Methods

environmentSpec ∷ ExecContext fn "UTXO" Conway → Specification fn (Environment (EraRule "UTXO" Conway)) Source #

stateSpec ∷ ExecContext fn "UTXO" Conway → Environment (EraRule "UTXO" Conway) → Specification fn (State (EraRule "UTXO" Conway)) Source #

signalSpec ∷ ExecContext fn "UTXO" Conway → Environment (EraRule "UTXO" Conway) → State (EraRule "UTXO" Conway) → Specification fn (Signal (EraRule "UTXO" Conway)) Source #

genExecContext ∷ Gen (ExecContext fn "UTXO" Conway) Source #

runAgdaRule ∷ SpecRep (Environment (EraRule "UTXO" Conway)) → SpecRep (State (EraRule "UTXO" Conway)) → SpecRep (Signal (EraRule "UTXO" Conway)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule "UTXO" Conway)))) (SpecRep (State (EraRule "UTXO" Conway))) Source #

translateInputs ∷ Environment (EraRule "UTXO" Conway) → State (EraRule "UTXO" Conway) → Signal (EraRule "UTXO" Conway) → ExecContext fn "UTXO" Conway → ImpTestM Conway (SpecRep (Environment (EraRule "UTXO" Conway)), SpecRep (State (EraRule "UTXO" Conway)), SpecRep (Signal (EraRule "UTXO" Conway))) Source #

testConformance ∷ ExecContext fn "UTXO" Conway → Environment (EraRule "UTXO" Conway) → State (EraRule "UTXO" Conway) → Signal (EraRule "UTXO" Conway) → Property Source #

conformsToImpl ∷ ∀ (rule ∷ Symbol) fn era. (ShelleyEraImp era, ExecSpecRule fn rule era, NFData (SpecRep (Environment (EraRule rule era))), NFData (SpecRep (State (EraRule rule era))), NFData (SpecRep (Signal (EraRule rule era))), NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (Environment (EraRule rule era))), ToExpr (SpecRep (State (EraRule rule era))), ToExpr (SpecRep (Signal (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext fn rule era), SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (State (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (State (EraRule rule era)))) ⇒ Property Source #

computationResultToEither ∷ ComputationResult e a → Either e a Source #

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

runConformance ∷ ∀ (rule ∷ Symbol) (fn ∷ [Type] → Type → Type) era. (ExecSpecRule fn rule era, NFData (SpecRep (Environment (EraRule rule era))), NFData (SpecRep (State (EraRule rule era))), NFData (SpecRep (Signal (EraRule rule era))), NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (Environment (EraRule rule era))), ToExpr (SpecRep (State (EraRule rule era))), ToExpr (SpecRep (Signal (EraRule rule era))), SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (State (EraRule rule era)))) ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → ImpTestM era (Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (State (EraRule rule era))), Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (State (EraRule rule era)))) Source #

checkConformance ∷ (ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (State (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (State (EraRule rule era)))) ⇒ Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (State (EraRule rule era))) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (State (EraRule rule era))) → ImpTestM era () Source #