11.12. Kernel Initialization and Execution🔗

def

Jar.JAVM.Kernel.initKernel (prog : Jar.JAVM.ProgramBlob)
  (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory)
  (gas memoryPages : Nat) (pvmRun : PvmRunFn := Jar.JAVM.run) :
  KernelState
Jar.JAVM.Kernel.initKernel
  (prog : Jar.JAVM.ProgramBlob)
  (regs : Jar.JAVM.Registers)
  (mem : Jar.JAVM.Memory)
  (gas memoryPages : Nat)
  (pvmRun : PvmRunFn := Jar.JAVM.run) :
  KernelState

Initialize a kernel from a parsed PVM program, arguments, and gas budget. For jar1: creates VM 0 with protocol caps 1-28, manifest caps, UNTYPED at 254. Sets φ[7]=op, φ[8]=args_base, φ[9]=args_len. PC=0.

The main kernel loop runs the active VM, dispatches ecalli/ecall results, handles CALL/REPLY/fault transitions, and exits to the host on protocol cap invocations.

def

Jar.JAVM.Kernel.runKernel (state : KernelState) (fuel : Nat) :
  KernelState × KernelResult
Jar.JAVM.Kernel.runKernel
  (state : KernelState) (fuel : Nat) :
  KernelState × KernelResult

Run the kernel until it needs host interaction or terminates. Uses fuel parameter for termination proof.