9.5. Instruction Execution (Appendix A.6)🔗

inductive type

Jar.PVM.StepResult : Type
Jar.PVM.StepResult : Type

Result of executing one instruction step.

Constructors

«continue» (pc : Nat) (regs : Jar.PVM.Registers)
  (mem : Jar.PVM.Memory) : Jar.PVM.StepResult

Continue execution: new PC, updated registers, updated memory.

halt : Jar.PVM.StepResult

Halt normally.

panic : Jar.PVM.StepResult

Panic (trap or invalid).

fault (addr : UInt64) : Jar.PVM.StepResult

Page fault at address.

hostCall (id : UInt64) (regs : Jar.PVM.Registers)
  (mem : Jar.PVM.Memory) (nextPC : Nat) : Jar.PVM.StepResult

Host call with function ID and next PC for resumption.

def

Jar.PVM.executeStep (prog : Jar.PVM.ProgramBlob) (pc : Nat)
  (regs : Jar.PVM.Registers) (mem : Jar.PVM.Memory)
  (heapModel : Jar.HeapModel := Jar.HeapModel.sbrk) : Jar.PVM.StepResult
Jar.PVM.executeStep
  (prog : Jar.PVM.ProgramBlob) (pc : Nat)
  (regs : Jar.PVM.Registers)
  (mem : Jar.PVM.Memory)
  (heapModel : Jar.HeapModel :=
    Jar.HeapModel.sbrk) :
  Jar.PVM.StepResult

Execute one PVM instruction. GP Appendix A. Takes current state, returns step result.