| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Constrained.Trace.TraceMonad
Synopsis
- data TraceState era = TraceState !Int !(Env era)
- newtype TraceM era x = TraceM (StateT (TraceState era) (ExceptT [String] Gen) x)
- runTraceM ∷ Int → Env era → TraceM era a → Gen (a, Int, Env era)
- fstTriple ∷ (a, b, c) → a
- toGen ∷ TraceM era a → Gen a
- failTrace ∷ [String] → TraceM era a
- liftTyped ∷ Typed a → TraceM era a
- liftGen ∷ Gen a → TraceM era a
- getEnv ∷ TraceM era (Env era)
- getCount ∷ TraceM era Int
- putEnv ∷ Env era → TraceM era (Env era)
- putCount ∷ Int → TraceM era ()
- liftCounter ∷ ((Int, a) → Gen (Int, b)) → a → TraceM era b
- getTerm ∷ Term era a → TraceM era a
- getTarget ∷ RootTarget era r a → TraceM era a
- fromMapTerm ∷ Term era (Map k a) → TraceM era (k, a)
- fromMapTermSuchThat ∷ Term era (Map k a) → ((k, a) → Bool) → TraceM era (k, a)
- fromSetTerm ∷ Term era (Set b) → TraceM era b
- update ∷ (Env era → TraceM era (Env era)) → TraceM era ()
- updateVar ∷ Term era t → (t → t) → TraceM era ()
- setVar ∷ Term era t → t → TraceM era ()
- refInputs ∷ Proof era → TxBody era → Set (TxIn (EraCrypto era))
- reqSig ∷ Proof era → TxBody era → Set (KeyHash 'Witness (EraCrypto era))
- compileTraceWithSubst ∷ Era era ⇒ OrderInfo → Subst era → [Pred era] → TraceM era (DependGraph era)
- toolChainTrace ∷ Era era ⇒ Proof era → OrderInfo → [Pred era] → Subst era → TraceM era (Subst era)
- universeTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- pparamsTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- utxoTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- pstateTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- vstateTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- dstateTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- ledgerStateTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- epochStateTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- newEpochStateTrace ∷ Reflect era ⇒ Proof era → Subst era → TraceM era (Subst era)
- makeTrace ∷ Int → TraceM era a → TraceM era [(Env era, a)]
- data TraceStep era a = TraceStep {}
- beforeAfterTrace ∷ Int → (Int → TraceM era a) → TraceM era [TraceStep era a]
- genLedgerStateEnv ∷ Reflect era ⇒ Proof era → TraceM era (Env era)
- genNewEpochStateEnv ∷ Reflect era ⇒ Proof era → TraceM era (Env era)
- data PredGen era = PredGen (Vector (StrictSeq (Tx era), SlotNo)) (Env era)
- genTraceParts ∷ Reflect era ⇒ Proof era → Int → (Proof era → TraceM era (Tx era)) → TraceM era ([TraceStep era (Tx era)], Maybe (IRC (MOCKCHAIN era) → Gen (Either a (MockChainState era))), PredGen era)
- traceStepToVector ∷ (step → Tx era) → [step] → Word64 → [([Tx era], SlotNo)] → TraceM era (Vector (StrictSeq (Tx era), SlotNo))
- newStsTrace ∷ (Reflect era, STS (MOCKCHAIN era)) ⇒ Proof era → Int → (Proof era → TraceM era (Tx era)) → Gen (Trace (MOCKCHAIN era))
- mockChainProp ∷ ∀ era. (Reflect era, STS (MOCKCHAIN era)) ⇒ Proof era → Int → (Proof era → TraceM era (Tx era)) → (Trace (MOCKCHAIN era) → Property) → Property
- stepProp ∷ (MockChainState era → MockBlock era → MockChainState era → Property) → Trace (MOCKCHAIN era) → Property
- deltaProp ∷ (MockChainState era → MockBlock era → MockChainState era → Property) → Trace (MOCKCHAIN era) → Property
- preserveProp ∷ (MockChainState era → MockChainState era → Property) → Trace (MOCKCHAIN era) → Property
- epochProp ∷ ConwayEraGov era ⇒ (MockChainState era → MockChainState era → Property) → Trace (MOCKCHAIN era) → Property
- splitEpochs ∷ [MockChainState era] → [NonEmpty (MockChainState era)]
- showPulserState ∷ ConwayEraGov era ⇒ MockChainState era → String
Documentation
data TraceState era Source #
Constructors
| TraceState !Int !(Env era) |
getTerm ∷ Term era a → TraceM era a Source #
Lookup the value of a Term in the Env internal to TraceM.
getTarget ∷ RootTarget era r a → TraceM era a Source #
fromMapTerm ∷ Term era (Map k a) → TraceM era (k, a) Source #
Pick a random (key,value) pair from a Map
fromMapTermSuchThat ∷ Term era (Map k a) → ((k, a) → Bool) → TraceM era (k, a) Source #
Pick a random (key,value) pair from a Map such that the (key,value) pair meets predicate p
update ∷ (Env era → TraceM era (Env era)) → TraceM era () Source #
Update the Env internal to TraceM.
updateVar ∷ Term era t → (t → t) → TraceM era () Source #
Update the value of one variable stored in the Env internal to TraceM.
compileTraceWithSubst ∷ Era era ⇒ OrderInfo → Subst era → [Pred era] → TraceM era (DependGraph era) Source #
Compile [Pred era] in the TraceM monad First: Apply the Rewriter Second: appy the Subst Third: Construct the DependGraph
toolChainTrace ∷ Era era ⇒ Proof era → OrderInfo → [Pred era] → Subst era → TraceM era (Subst era) Source #
Use the tool chain to generate a Subst from a list of Pred, in the TraceM monad.
makeTrace ∷ Int → TraceM era a → TraceM era [(Env era, a)] Source #
Iterate a function make to make a trace of length n. Each call to make gets the
most recent value of the Env internal to TraceM. The function make is
supposed to compute a, and (possibly) update the Env internal to TraceM.
genLedgerStateEnv ∷ Reflect era ⇒ Proof era → TraceM era (Env era) Source #
Generate an Env that contains the pieces of the LedgerState by chaining smaller pieces together.
genNewEpochStateEnv ∷ Reflect era ⇒ Proof era → TraceM era (Env era) Source #
Generate an Env that contains the pieces of the NewEpochState by chaining smaller pieces together.
How we encode a trace, when we run STS of (MOCKCHAIN era)
Instances
| Reflect era ⇒ Show (PredGen era) Source # | |
| (STS (MOCKCHAIN era), Reflect era) ⇒ HasTrace (MOCKCHAIN era) (PredGen era) Source # | |
Defined in Test.Cardano.Ledger.Constrained.Trace.TraceMonad Methods interpretSTS ∷ HasCallStack ⇒ BaseEnv (MOCKCHAIN era) → BaseM (MOCKCHAIN era) a → a Source # envGen ∷ PredGen era → Gen (Environment (MOCKCHAIN era)) Source # sigGen ∷ PredGen era → Environment (MOCKCHAIN era) → State (MOCKCHAIN era) → Gen (Signal (MOCKCHAIN era)) Source # shrinkSignal ∷ Signal (MOCKCHAIN era) → [Signal (MOCKCHAIN era)] Source # | |
genTraceParts ∷ Reflect era ⇒ Proof era → Int → (Proof era → TraceM era (Tx era)) → TraceM era ([TraceStep era (Tx era)], Maybe (IRC (MOCKCHAIN era) → Gen (Either a (MockChainState era))), PredGen era) Source #
traceStepToVector ∷ (step → Tx era) → [step] → Word64 → [([Tx era], SlotNo)] → TraceM era (Vector (StrictSeq (Tx era), SlotNo)) Source #
newStsTrace ∷ (Reflect era, STS (MOCKCHAIN era)) ⇒ Proof era → Int → (Proof era → TraceM era (Tx era)) → Gen (Trace (MOCKCHAIN era)) Source #
Generate a Control.State.Transition.Trace(Trace) from a (TraceM era (Tx era))
mockChainProp ∷ ∀ era. (Reflect era, STS (MOCKCHAIN era)) ⇒ Proof era → Int → (Proof era → TraceM era (Tx era)) → (Trace (MOCKCHAIN era) → Property) → Property Source #
Create a testable Property from two things 1) A function that generates Tx 2) A function that creates a property from a (Trace (MOCKCHAIN era))
stepProp ∷ (MockChainState era → MockBlock era → MockChainState era → Property) → Trace (MOCKCHAIN era) → Property Source #
Given trace [(sig0,state0),(sig1,state1),(sig2,state2),(sig3,state3)]
conjoin [p pstate0 sig1 state1, p state0 sig2 state2, p state0 sig3 state3]
test that p holds between state0 and stateN for all N
deltaProp ∷ (MockChainState era → MockBlock era → MockChainState era → Property) → Trace (MOCKCHAIN era) → Property Source #
Given trace [(sig0,state0),(sig1,state1),(sig2,state2),(sig3,state3)]
conjoin [p pstate0 sig1 state1, p state1 sig2 state2, p state2 sig3 state3]
test that p holds bteween (state0 stateN sig(N+1) state(N+1) for all N
preserveProp ∷ (MockChainState era → MockChainState era → Property) → Trace (MOCKCHAIN era) → Property Source #
Given trace [(sig0,state0),(sig1,state1),(sig2,state2),(sig3,state3)] test that (p state0 stateN), where stateN is the last state in the trace
epochProp ∷ ConwayEraGov era ⇒ (MockChainState era → MockChainState era → Property) → Trace (MOCKCHAIN era) → Property Source #
Apply '(preserveProp p)' to each full Epoch in a Trace. A partial epoch at the end of the trace is not tested.
splitEpochs ∷ [MockChainState era] → [NonEmpty (MockChainState era)] Source #
showPulserState ∷ ConwayEraGov era ⇒ MockChainState era → String Source #