11.3. Capability Dispatch Results🔗

Internal dispatch within the kernel produces a DispatchResult that determines whether execution continues, a protocol cap was invoked, or the root VM terminated.

inductive type

Jar.JAVM.Cap.DispatchResult : Type
Jar.JAVM.Cap.DispatchResult : Type

Result of CALL dispatch.

Constructors

continue_ : Jar.JAVM.Cap.DispatchResult

Continue execution of active VM.

protocolCall (slot : Nat) (regs : Jar.JAVM.Registers)
  (gas : Nat) : Jar.JAVM.Cap.DispatchResult

Protocol cap called — host should handle.

rootHalt (value : Nat) : Jar.JAVM.Cap.DispatchResult

Root VM halted normally.

rootPanic : Jar.JAVM.Cap.DispatchResult

Root VM panicked.

rootOutOfGas : Jar.JAVM.Cap.DispatchResult

Root VM out of gas.

def

Jar.JAVM.Kernel.PvmRunFn : Type
Jar.JAVM.Kernel.PvmRunFn : Type

PVM run function type (selects gas model).