| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
UntypedPlutusCore.Evaluation.Machine.SteppableCek.Internal
Description
The CEK machine.
The CEK machine relies on variables having non-equal Uniques whenever they have non-equal
string names. I.e. Uniques are used instead of string names. This is for efficiency reasons.
The CEK machines handles name capture by design.
Synopsis
- data CekState uni fun ann
- data Context uni fun ann
- = FrameAwaitArg ann !(CekValue uni fun ann) !(Context uni fun ann)
- | FrameAwaitFunTerm ann !(CekValEnv uni fun ann) !(NTerm uni fun ann) !(Context uni fun ann)
- | FrameAwaitFunValue ann !(CekValue uni fun ann) !(Context uni fun ann)
- | FrameForce ann !(Context uni fun ann)
- | FrameConstr ann !(CekValEnv uni fun ann) !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
- | FrameCases ann !(CekValEnv uni fun ann) !(Vector (NTerm uni fun ann)) !(Context uni fun ann)
- | NoFrame
- contextAnn ∷ Context uni fun ann → Maybe ann
- liftCek ∷ (PrimMonad m, PrimState m ~ s) ⇒ CekM uni fun s a → m a
- class Monad m ⇒ PrimMonad (m ∷ Type → Type) where
- lenContext ∷ Context uni fun ann → Word
- cekStateContext ∷ Traversal' (CekState uni fun ann) (Context uni fun ann)
- cekStateAnn ∷ CekState uni fun ann → Maybe ann
- runCekDeBruijn ∷ ThrowableBuiltins uni fun ⇒ MachineParameters CekMachineCosts fun (CekValue uni fun ann) → ExBudgetMode cost uni fun → EmitterMode uni fun → NTerm uni fun ann → (Either (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ()), cost, [Text])
- computeCek ∷ ∀ uni fun ann s. (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) ⇒ Context uni fun ann → CekValEnv uni fun ann → NTerm uni fun ann → CekM uni fun s (CekState uni fun ann)
- returnCek ∷ ∀ uni fun ann s. (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) ⇒ Context uni fun ann → CekValue uni fun ann → CekM uni fun s (CekState uni fun ann)
- mkCekTrans ∷ ∀ cost uni fun ann m s. (ThrowableBuiltins uni fun, PrimMonad m, s ~ PrimState m) ⇒ MachineParameters CekMachineCosts fun (CekValue uni fun ann) → ExBudgetMode cost uni fun → EmitterMode uni fun → Slippage → m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
- type CekTrans uni fun ann s = Trans (CekM uni fun s) (CekState uni fun ann)
- nilSlippage ∷ Slippage
- data EvaluationResult a
- data EvaluationError structural operational
- = StructuralEvaluationError !structural
- | OperationalEvaluationError !operational
- data ErrorWithCause err cause = ErrorWithCause {}
- type ThrowableBuiltins uni fun = (PrettyUni uni, Pretty fun, Typeable uni, Typeable fun)
- data CekUserError
- type CekEvaluationException name uni fun = EvaluationException (MachineError fun) CekUserError (Term name uni fun ())
- data ExBudgetCategory fun
- = BStep StepKind
- | BBuiltinApp fun
- | BStartup
- newtype CekBudgetSpender uni fun s = CekBudgetSpender {
- unCekBudgetSpender ∷ ExBudgetCategory fun → ExBudget → CekM uni fun s ()
- newtype ExBudgetMode cost uni fun = ExBudgetMode {
- unExBudgetMode ∷ ∀ s. ST s (ExBudgetInfo cost uni fun s)
- data StepKind
- data CekValue uni fun ann
- newtype EmitterMode uni fun = EmitterMode {
- unEmitterMode ∷ ∀ s. ST s ExBudget → ST s (CekEmitterInfo uni fun s)
- data ArgStack uni fun ann
- = EmptyStack
- | ConsStack !(CekValue uni fun ann) !(ArgStack uni fun ann)
- data ExBudgetInfo cost uni fun s = ExBudgetInfo {
- _exBudgetModeSpender ∷ !(CekBudgetSpender uni fun s)
- _exBudgetModeGetFinal ∷ !(ST s cost)
- _exBudgetModeGetCumulative ∷ !(ST s ExBudget)
- type CekEmitter uni fun s = DList Text → CekM uni fun s ()
- data CekEmitterInfo uni fun s = CekEmitterInfo {
- _cekEmitterInfoEmit ∷ !(CekEmitter uni fun s)
- _cekEmitterInfoGetFinal ∷ !(ST s [Text])
- newtype CekM uni fun s a = CekM {}
- type CekValEnv uni fun ann = RAList (CekValue uni fun ann)
- type GivenCekReqs uni fun ann s = (GivenCekRuntime uni fun ann, GivenCekEmitter uni fun s, GivenCekSpender uni fun s, GivenCekSlippage, GivenCekStepCounter s, GivenCekCosts)
- type GivenCekSpender uni fun s = ?cekBudgetSpender ∷ CekBudgetSpender uni fun s
- data StepCounter (n ∷ Nat) s
- type NumberOfStepCounters = CountConstructorsEnum (Rep StepKind)
- type CounterSize = NumberOfStepCounters + 1
- type TotalCountIndex = NumberOfStepCounters
- type Slippage = Word8
- type NTerm uni fun = Term NamedDeBruijn uni fun
- splitStructuralOperational ∷ Either (EvaluationException structural operational term) a → Either (ErrorWithCause structural term) (EvaluationResult a)
- unsafeSplitStructuralOperational ∷ (PrettyPlc structural, PrettyPlc term, Typeable structural, Typeable term) ⇒ Either (EvaluationException structural operational term) a → EvaluationResult a
- dischargeCekValue ∷ CekValue uni fun ann → NTerm uni fun ()
- defaultSlippage ∷ Slippage
- runCekM ∷ ∀ a cost uni fun ann. ThrowableBuiltins uni fun ⇒ MachineParameters CekMachineCosts fun (CekValue uni fun ann) → ExBudgetMode cost uni fun → EmitterMode uni fun → (∀ s. GivenCekReqs uni fun ann s ⇒ CekM uni fun s a) → (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost, [Text])
Documentation
data Context uni fun ann Source #
Similar to Context, but augmented with an ann
Constructors
| FrameAwaitArg ann !(CekValue uni fun ann) !(Context uni fun ann) | [V _] |
| FrameAwaitFunTerm ann !(CekValEnv uni fun ann) !(NTerm uni fun ann) !(Context uni fun ann) | [_ N] |
| FrameAwaitFunValue ann !(CekValue uni fun ann) !(Context uni fun ann) | |
| FrameForce ann !(Context uni fun ann) | (force _) |
| FrameConstr ann !(CekValEnv uni fun ann) !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann) | |
| FrameCases ann !(CekValEnv uni fun ann) !(Vector (NTerm uni fun ann)) !(Context uni fun ann) | |
| NoFrame |
contextAnn ∷ Context uni fun ann → Maybe ann Source #
liftCek ∷ (PrimMonad m, PrimState m ~ s) ⇒ CekM uni fun s a → m a Source #
Lift a CEK computation to a primitive.PrimMonad m
class Monad m ⇒ PrimMonad (m ∷ Type → Type) where Source #
Class of monads which can perform primitive state-transformer actions.
Methods
primitive ∷ (State# (PrimState m) → (# State# (PrimState m), a #)) → m a Source #
Execute a primitive operation.
Instances
| PrimMonad IO | |
| PrimMonad (ST s) | |
| PrimMonad (ST s) | |
| PrimMonad m ⇒ PrimMonad (GenT m) | |
| PrimMonad m ⇒ PrimMonad (PropertyT m) | |
| PrimMonad m ⇒ PrimMonad (TestT m) | |
| PrimMonad m ⇒ PrimMonad (TreeT m) | |
| PrimMonad m ⇒ PrimMonad (ResourceT m) | |
| PrimMonad m ⇒ PrimMonad (MaybeT m) | |
| (Monoid w, PrimMonad m) ⇒ PrimMonad (AccumT w m) | Since: primitive-0.6.3.0 |
| PrimMonad m ⇒ PrimMonad (ExceptT e m) | |
| PrimMonad m ⇒ PrimMonad (IdentityT m) | |
| PrimMonad m ⇒ PrimMonad (ReaderT r m) | |
| PrimMonad m ⇒ PrimMonad (SelectT r m) | |
| PrimMonad m ⇒ PrimMonad (StateT s m) | |
| PrimMonad m ⇒ PrimMonad (StateT s m) | |
| (Monoid w, PrimMonad m) ⇒ PrimMonad (WriterT w m) | |
| (Monoid w, PrimMonad m) ⇒ PrimMonad (WriterT w m) | |
| (Monoid w, PrimMonad m) ⇒ PrimMonad (WriterT w m) | |
| PrimMonad (CekM uni fun s) Source # | |
| PrimMonad m ⇒ PrimMonad (ContT r m) | Since: primitive-0.6.3.0 |
| (Monoid w, PrimMonad m) ⇒ PrimMonad (RWST r w s m) | |
| (Monoid w, PrimMonad m) ⇒ PrimMonad (RWST r w s m) | |
| (Monoid w, PrimMonad m) ⇒ PrimMonad (RWST r w s m) | |
lenContext ∷ Context uni fun ann → Word Source #
cekStateContext ∷ Traversal' (CekState uni fun ann) (Context uni fun ann) Source #
cekStateAnn ∷ CekState uni fun ann → Maybe ann Source #
runCekDeBruijn ∷ ThrowableBuiltins uni fun ⇒ MachineParameters CekMachineCosts fun (CekValue uni fun ann) → ExBudgetMode cost uni fun → EmitterMode uni fun → NTerm uni fun ann → (Either (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ()), cost, [Text]) Source #
computeCek ∷ ∀ uni fun ann s. (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) ⇒ Context uni fun ann → CekValEnv uni fun ann → NTerm uni fun ann → CekM uni fun s (CekState uni fun ann) Source #
returnCek ∷ ∀ uni fun ann s. (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) ⇒ Context uni fun ann → CekValue uni fun ann → CekM uni fun s (CekState uni fun ann) Source #
mkCekTrans ∷ ∀ cost uni fun ann m s. (ThrowableBuiltins uni fun, PrimMonad m, s ~ PrimState m) ⇒ MachineParameters CekMachineCosts fun (CekValue uni fun ann) → ExBudgetMode cost uni fun → EmitterMode uni fun → Slippage → m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s) Source #
Based on the supplied arguments, initialize the CEK environment and construct a state transition function. Returns the constructed transition function paired with the methods to live access the running budget.
nilSlippage ∷ Slippage Source #
A CEK parameter that turns the slippage optimization *off*.
This is needed in the case of the debugger, where the accounting/budgeting costs must be *live* updated.
data EvaluationResult a Source #
The parameterized type of results various evaluation engines return.
On the PLC side this becomes (via makeKnown) either a call to Error or
a value of the PLC counterpart of type a.
Constructors
| EvaluationSuccess !a | |
| EvaluationFailure |
Instances
data EvaluationError structural operational Source #
The type of errors that can occur during evaluation. There are two kinds of errors:
- Structural ones -- these are errors that are indicative of the _structure_ of the program being
wrong. For example, a free variable was encountered during evaluation, a non-function was
applied to an argument or
tailListwas applied to a non-list. - Operational ones -- these are errors that are indicative of the _logic_ of the program being
wrong. For example,
errorwas executed,tailListwas applied to an empty list or evaluation ran out of gas.
On the chain both of these are just regular failures and we don't distinguish between them there: if a script fails, it fails, it doesn't matter what the reason was. However in the tests it does matter why the failure occurred: a structural error may indicate that the test was written incorrectly while an operational error may be entirely expected.
In other words, structural errors are "runtime type errors" and operational errors are regular runtime errors. Which means that evaluating an (erased) well-typed program should never produce a structural error, only an operational one. This creates a sort of "runtime type system" for UPLC and it would be great to stick to it and enforce in tests etc, but we currently don't.
Constructors
| StructuralEvaluationError !structural | |
| OperationalEvaluationError !operational |
Instances
data ErrorWithCause err cause Source #
An error and (optionally) what caused it.
Constructors
| ErrorWithCause | |
Instances
type ThrowableBuiltins uni fun = (PrettyUni uni, Pretty fun, Typeable uni, Typeable fun) Source #
The set of constraints we need to be able to throw exceptions with things with built-in types and functions in them.
data CekUserError Source #
Constructors
| CekOutOfExError !ExRestrictingBudget | The final overspent (i.e. negative) budget. |
| CekEvaluationFailure | Error has been called or a builtin application has failed |
Instances
type CekEvaluationException name uni fun = EvaluationException (MachineError fun) CekUserError (Term name uni fun ()) Source #
The CEK machine-specific EvaluationException.
data ExBudgetCategory fun Source #
Constructors
| BStep StepKind | |
| BBuiltinApp fun | |
| BStartup |
Instances
newtype CekBudgetSpender uni fun s Source #
The CEK machine is parameterized over a spendBudget function. This makes the budgeting machinery extensible
and allows us to separate budgeting logic from evaluation logic and avoid branching on the union
of all possible budgeting state types during evaluation.
Constructors
| CekBudgetSpender | |
Fields
| |
newtype ExBudgetMode cost uni fun Source #
A budgeting mode to execute the CEK machine in.
Constructors
| ExBudgetMode | |
Fields
| |
Instances
data CekValue uni fun ann Source #
Constructors
| VCon !(Some (ValueOf uni)) | |
| VDelay !(NTerm uni fun ann) !(CekValEnv uni fun ann) | |
| VLamAbs !NamedDeBruijn !(NTerm uni fun ann) !(CekValEnv uni fun ann) | |
| VBuiltin | A partial builtin application, accumulating arguments for eventual full application.
We don't need a |
Fields
| |
| VConstr !Word64 !(ArgStack uni fun ann) | |
Instances
| (PrettyUni uni, Pretty fun) ⇒ PrettyBy PrettyConfigPlc (CekValue uni fun ann) Source # | |
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods prettyBy ∷ PrettyConfigPlc → CekValue uni fun ann → Doc ann0 Source # prettyListBy ∷ PrettyConfigPlc → [CekValue uni fun ann] → Doc ann0 Source # | |
| Show (BuiltinRuntime (CekValue uni fun ann)) Source # | |
| (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni) ⇒ Show (CekValue uni fun ann) Source # | |
| HasConstant (CekValue uni fun ann) Source # | |
| (Closed uni, Everywhere uni ExMemoryUsage) ⇒ ExMemoryUsage (CekValue uni fun ann) Source # | |
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods memoryUsage ∷ CekValue uni fun ann → CostRose Source # | |
| type UniOf (CekValue uni fun ann) Source # | |
newtype EmitterMode uni fun Source #
An emitting mode to execute the CEK machine in, similar to ExBudgetMode.
Constructors
| EmitterMode | |
Fields
| |
data ArgStack uni fun ann Source #
A LIFO stack of CekValues, useful for recording multiple arguments which will need to
be pushed onto the context in reverse order.
Constructors
| EmptyStack | |
| ConsStack !(CekValue uni fun ann) !(ArgStack uni fun ann) |
data ExBudgetInfo cost uni fun s Source #
Runtime budgeting info.
Constructors
| ExBudgetInfo | |
Fields
| |
type CekEmitter uni fun s = DList Text → CekM uni fun s () Source #
The CEK machine is parameterized over an emitter function, similar to CekBudgetSpender.
data CekEmitterInfo uni fun s Source #
Runtime emitter info, similar to ExBudgetInfo.
Constructors
| CekEmitterInfo | |
Fields
| |
newtype CekM uni fun s a Source #
The monad the CEK machine runs in.
Instances
| Applicative (CekM uni fun s) Source # | |
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods pure ∷ a → CekM uni fun s a Source # (<*>) ∷ CekM uni fun s (a → b) → CekM uni fun s a → CekM uni fun s b Source # liftA2 ∷ (a → b → c) → CekM uni fun s a → CekM uni fun s b → CekM uni fun s c Source # (*>) ∷ CekM uni fun s a → CekM uni fun s b → CekM uni fun s b Source # (<*) ∷ CekM uni fun s a → CekM uni fun s b → CekM uni fun s a Source # | |
| Functor (CekM uni fun s) Source # | |
| Monad (CekM uni fun s) Source # | |
| PrimMonad (CekM uni fun s) Source # | |
| ThrowableBuiltins uni fun ⇒ MonadError (CekEvaluationException NamedDeBruijn uni fun) (CekM uni fun s) Source # | |
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods throwError ∷ CekEvaluationException NamedDeBruijn uni fun → CekM uni fun s a Source # catchError ∷ CekM uni fun s a → (CekEvaluationException NamedDeBruijn uni fun → CekM uni fun s a) → CekM uni fun s a Source # | |
| type PrimState (CekM uni fun s) Source # | |
type GivenCekReqs uni fun ann s = (GivenCekRuntime uni fun ann, GivenCekEmitter uni fun s, GivenCekSpender uni fun s, GivenCekSlippage, GivenCekStepCounter s, GivenCekCosts) Source #
Constraint requiring all of the machine's implicit parameters.
type GivenCekSpender uni fun s = ?cekBudgetSpender ∷ CekBudgetSpender uni fun s Source #
Implicit parameter for budget spender.
data StepCounter (n ∷ Nat) s Source #
A set of Word8 counters that is used in the CEK machine
to count steps.
type NumberOfStepCounters = CountConstructorsEnum (Rep StepKind) Source #
The number of step counters that we need, should be the same as the number of constructors
of StepKind.
type CounterSize = NumberOfStepCounters + 1 Source #
The total number of counters that we need, one extra for the total counter. See Note [Structure of the step counter]
type TotalCountIndex = NumberOfStepCounters Source #
The index at which the total step counter is kept. See Note [Structure of the step counter]
type NTerm uni fun = Term NamedDeBruijn uni fun Source #
The Terms that CEK can execute must have DeBruijn binders
Name is not necessary but we leave it here for simplicity and debuggability.
splitStructuralOperational ∷ Either (EvaluationException structural operational term) a → Either (ErrorWithCause structural term) (EvaluationResult a) Source #
Preserve the contents of an StructuralEvaluationError as a Left and turn an
OperationalEvaluationError into a Right EvaluationFailure (thus erasing the content of the
error in the latter case).
unsafeSplitStructuralOperational ∷ (PrettyPlc structural, PrettyPlc term, Typeable structural, Typeable term) ⇒ Either (EvaluationException structural operational term) a → EvaluationResult a Source #
Throw on a StructuralEvaluationError and turn an OperationalEvaluationError into an
EvaluationFailure (thus erasing the content of the error in the latter case).
dischargeCekValue ∷ CekValue uni fun ann → NTerm uni fun () Source #
defaultSlippage ∷ Slippage Source #
The default number of slippage (in machine steps) to allow.
runCekM ∷ ∀ a cost uni fun ann. ThrowableBuiltins uni fun ⇒ MachineParameters CekMachineCosts fun (CekValue uni fun ann) → ExBudgetMode cost uni fun → EmitterMode uni fun → (∀ s. GivenCekReqs uni fun ann s ⇒ CekM uni fun s a) → (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost, [Text]) Source #