11.11. ecall Dispatch🔗

The ecall instruction dispatches management operations and dynamic CALL. phi[11] selects the operation, phi[12] encodes subject (high u32) and object (low u32) with indirection.

def

Jar.JAVM.Kernel.dispatchEcall (state : KernelState) :
  KernelState × DispatchResult
Jar.JAVM.Kernel.dispatchEcall
  (state : KernelState) :
  KernelState × DispatchResult

ecall dispatch: φ[11]=op, φ[12]=subject|object.

inductive type

Jar.JAVM.Kernel.DispatchResult : Type
Jar.JAVM.Kernel.DispatchResult : Type

Internal dispatch result.

Constructors

continue_ : DispatchResult

protocolCall (slot : Nat) : DispatchResult

rootHalt (value : Nat) : DispatchResult

rootPanic : DispatchResult

rootOutOfGas : DispatchResult

rootPageFault (addr : Nat) : DispatchResult

faultHandled : DispatchResult