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

Contents

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

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

stateSpec ∷ ExecContext fn "CERT" Conway → ExecEnvironment fn "CERT" Conway → Specification fn (ExecState fn "CERT" Conway) Source #

signalSpec ∷ ExecContext fn "CERT" Conway → ExecEnvironment fn "CERT" Conway → ExecState fn "CERT" Conway → Specification fn (ExecSignal fn "CERT" Conway) Source #

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

runAgdaRule ∷ SpecRep (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 #

translateInputs ∷ ExecEnvironment fn "CERT" Conway → ExecState fn "CERT" Conway → ExecSignal fn "CERT" Conway → ExecContext fn "CERT" Conway → ImpTestM Conway (SpecRep (ExecEnvironment fn "CERT" Conway), SpecRep (ExecState fn "CERT" Conway), SpecRep (ExecSignal fn "CERT" Conway)) Source #

testConformance ∷ ExecContext fn "CERT" Conway → ExecEnvironment fn "CERT" Conway → ExecState fn "CERT" Conway → ExecSignal fn "CERT" Conway → Property Source #

extraInfo ∷ ExecContext fn "CERT" Conway → Environment (EraRule "CERT" Conway) → State (EraRule "CERT" Conway) → Signal (EraRule "CERT" Conway) → String Source #