def

Jar.JAVM.getReg (regs : Jar.JAVM.Registers) (r : Fin 13) : UInt64
Jar.JAVM.getReg
  (regs : Jar.JAVM.Registers)
  (r : Fin 13) : UInt64

Get register value (bounds-checked).

def

Jar.JAVM.setReg (regs : Jar.JAVM.Registers) (r : Fin 13) (v : UInt64) :
  Jar.JAVM.Registers
Jar.JAVM.setReg
  (regs : Jar.JAVM.Registers) (r : Fin 13)
  (v : UInt64) : Jar.JAVM.Registers

Set register value (bounds-checked). Returns new register file.

def

Jar.JAVM.nextPC (pc skip : Nat) : Nat
Jar.JAVM.nextPC (pc skip : Nat) : Nat

Compute next PC (default: advance past current instruction).

def

Jar.JAVM.opcodeName (op : Nat) : String
Jar.JAVM.opcodeName (op : Nat) : String

Human-readable opcode name for tracing.

inductive type

Jar.JAVM.StepResult : Type
Jar.JAVM.StepResult : Type

Result of executing one instruction step.

Constructors

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

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

halt : Jar.JAVM.StepResult

Halt normally.

trap : Jar.JAVM.StepResult

Deliberate trap (opcode 0).

panic : Jar.JAVM.StepResult

Runtime panic (bad djump, invalid opcode, etc.).

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

Page fault at address.

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

Host call with function ID and next PC for resumption (ecalli).

ecall (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory)
  (nextPC : Nat) : Jar.JAVM.StepResult

Management op / dynamic CALL (ecall opcode 3). φ[11]=op, φ[12]=subject|object.

def

Jar.JAVM.executeStep (prog : Jar.JAVM.ProgramBlob) (pc : Nat)
  (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) :
  Jar.JAVM.StepResult
Jar.JAVM.executeStep
  (prog : Jar.JAVM.ProgramBlob) (pc : Nat)
  (regs : Jar.JAVM.Registers)
  (mem : Jar.JAVM.Memory) :
  Jar.JAVM.StepResult

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

JAR: Join-Accumulate Refine

9.10. Instruction Execution (Appendix A.6)🔗

Constructors