| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Constrained.Trace.Pipeline
Synopsis
- data Rule (i ∷ Symbol) where
- DELEG ∷ Rule "DELEG"
- DELEGS ∷ Rule "DELEGS"
- DELPL ∷ Rule "DELPL"
- EPOCH ∷ Rule "EPOCH"
- LEDGER ∷ Rule "LEDGER"
- LEDGERS ∷ Rule "LEDGERS"
- MIR ∷ Rule "MIR"
- NEWEPOCH ∷ Rule "NEWSPOCH"
- NEWPP ∷ Rule "NEWPP"
- POOL ∷ Rule "POOL"
- POOLREAP ∷ Rule "POOLREAP"
- PPUP ∷ Rule "PPUP"
- RUPD ∷ Rule "RUPD"
- SNAP ∷ Rule "SNAP"
- TICK ∷ Rule "TICK"
- TICKF ∷ Rule "TICKF"
- UPEC ∷ Rule "UPEC"
- UTXO ∷ Rule "UTXO"
- UTXOW ∷ Rule "UTXOW"
- GOVCERT ∷ Rule "GOVCERT"
- GOV ∷ Rule "GOV"
- trc ∷ Proof era → Rule tag → Environment (EraRule tag era) → State (EraRule tag era) → Signal (EraRule tag era) → TRC (EraRule tag era)
- sts ∷ ∀ era tag. (BaseM (EraRule tag era) ~ Reader Globals, STS (EraRule tag era)) ⇒ Proof era → Rule tag → Environment (EraRule tag era) → State (EraRule tag era) → Signal (EraRule tag era) → Either (NonEmpty (PredicateFailure (EraRule tag era))) (State (EraRule tag era))
- stsWithContinuations ∷ ∀ era tag ans. (BaseM (EraRule tag era) ~ Reader Globals, STS (EraRule tag era)) ⇒ Proof era → Rule tag → (NonEmpty (PredicateFailure (EraRule tag era)) → ans) → (State (EraRule tag era) → ans) → Environment (EraRule tag era) → State (EraRule tag era) → Signal (EraRule tag era) → ans
- pipeToGraph ∷ Era era ⇒ Stage era → HashSet (Name era) → TraceM era (DependGraph era)
- mergePipeline ∷ Era era ⇒ Pipeline era → HashSet (Name era) → DependGraph era → TraceM era (DependGraph era)
- solvePipeline2 ∷ Reflect era ⇒ Pipeline era → TraceM era (Env era, DependGraph era)
- main ∷ IO ()
- sts0 ∷ (Show ctx, Show state, Show sig, Testable prop) ⇒ Gen ctx → (ctx → Gen state) → (ctx → state → Gen sig) → (ctx → state → sig → state) → (state → state → prop) → Property
- sts1 ∷ (Show ctx, Show state, Show sig, Testable prop) ⇒ Gen state → (state → Gen ctx) → (state → ctx → Gen sig) → ((ctx, state, sig) → state) → (state → state → prop) → Property
- proofx ∷ Proof BabbageEra
- genLedgerState ∷ Gen (Env BabbageEra, Subst BabbageEra, LedgerState BabbageEra)
- genSig ∷ Reflect era ⇒ Proof era → (a, Subst era, b) → p → Gen (Tx era)
Documentation
data Rule (i ∷ Symbol) where Source #
Constructors
| DELEG ∷ Rule "DELEG" | |
| DELEGS ∷ Rule "DELEGS" | |
| DELPL ∷ Rule "DELPL" | |
| EPOCH ∷ Rule "EPOCH" | |
| LEDGER ∷ Rule "LEDGER" | |
| LEDGERS ∷ Rule "LEDGERS" | |
| MIR ∷ Rule "MIR" | |
| NEWEPOCH ∷ Rule "NEWSPOCH" | |
| NEWPP ∷ Rule "NEWPP" | |
| POOL ∷ Rule "POOL" | |
| POOLREAP ∷ Rule "POOLREAP" | |
| PPUP ∷ Rule "PPUP" | |
| RUPD ∷ Rule "RUPD" | |
| SNAP ∷ Rule "SNAP" | |
| TICK ∷ Rule "TICK" | |
| TICKF ∷ Rule "TICKF" | |
| UPEC ∷ Rule "UPEC" | |
| UTXO ∷ Rule "UTXO" | |
| UTXOW ∷ Rule "UTXOW" | |
| GOVCERT ∷ Rule "GOVCERT" | |
| GOV ∷ Rule "GOV" |
trc ∷ Proof era → Rule tag → Environment (EraRule tag era) → State (EraRule tag era) → Signal (EraRule tag era) → TRC (EraRule tag era) Source #
sts ∷ ∀ era tag. (BaseM (EraRule tag era) ~ Reader Globals, STS (EraRule tag era)) ⇒ Proof era → Rule tag → Environment (EraRule tag era) → State (EraRule tag era) → Signal (EraRule tag era) → Either (NonEmpty (PredicateFailure (EraRule tag era))) (State (EraRule tag era)) Source #
stsWithContinuations ∷ ∀ era tag ans. (BaseM (EraRule tag era) ~ Reader Globals, STS (EraRule tag era)) ⇒ Proof era → Rule tag → (NonEmpty (PredicateFailure (EraRule tag era)) → ans) → (State (EraRule tag era) → ans) → Environment (EraRule tag era) → State (EraRule tag era) → Signal (EraRule tag era) → ans Source #
pipeToGraph ∷ Era era ⇒ Stage era → HashSet (Name era) → TraceM era (DependGraph era) Source #
Translate a Pipe into a DependGraph, given the set of variables that have aready been solved for.
mergePipeline ∷ Era era ⇒ Pipeline era → HashSet (Name era) → DependGraph era → TraceM era (DependGraph era) Source #
Merge a Pipeline into an existing DependGraph, given the set of variables that have aready been solved for, to get a larger DependGraph
solvePipeline2 ∷ Reflect era ⇒ Pipeline era → TraceM era (Env era, DependGraph era) Source #
Solve a Pipeline to get both an Env and a DependGraph
sts0 ∷ (Show ctx, Show state, Show sig, Testable prop) ⇒ Gen ctx → (ctx → Gen state) → (ctx → state → Gen sig) → (ctx → state → sig → state) → (state → state → prop) → Property Source #
sts1 ∷ (Show ctx, Show state, Show sig, Testable prop) ⇒ Gen state → (state → Gen ctx) → (state → ctx → Gen sig) → ((ctx, state, sig) → state) → (state → state → prop) → Property Source #
When we run a STS rule, the context (env) is a subset of the state, so it makes sense to generate state, and then extract the context.