Ψ : Core PVM execution loop. GP eq (1-3). Repeatedly executes single steps until halt, panic, OOG, fault, or host call. Gas is decremented by 1 per instruction.
9.11. Interpreter
def
Jar.JAVM.run (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResultJar.JAVM.run (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResult
def
Jar.JAVM.runBlockGasWith (costFn : ByteArray → ByteArray → Nat → Nat) (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResultJar.JAVM.runBlockGasWith (costFn : ByteArray → ByteArray → Nat → Nat) (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResult
Ψ : Core PVM execution loop with per-basic-block gas charging. GP v0.8.0. Gas is charged upfront on basic block entry using pipeline simulation cost. Instructions within a block execute without individual gas deduction.
def
Jar.JAVM.runBlockGas (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResultJar.JAVM.runBlockGas (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResult
Per-basic-block execution with full pipeline simulation gas.
def
Jar.JAVM.runBlockGasSinglePass (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResultJar.JAVM.runBlockGasSinglePass (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResult
Per-basic-block execution with single-pass gas model.
def
Jar.JAVM.skipMetadata (blob : ByteArray) (compact : Bool := true) : ByteArrayJar.JAVM.skipMetadata (blob : ByteArray) (compact : Bool := true) : ByteArray
Skip metadata prefix in a PVM program blob.
Metadata format: E(metadata_length) ‖ metadata_bytes ‖ actual_program
When compact is true, uses JAM codec natural encoding for the length prefix (gp072).
When false, uses u32 LE (jar1).
def
Jar.JAVM.initStandard (blob' args : ByteArray) (compact : Bool := true) : Option (Jar.JAVM.ProgramBlob × Jar.JAVM.Registers × Jar.JAVM.Memory)Jar.JAVM.initStandard (blob' args : ByteArray) (compact : Bool := true) : Option (Jar.JAVM.ProgramBlob × Jar.JAVM.Registers × Jar.JAVM.Memory)
Parse standard program blob and initialize PVM state. GP Appendix A §2.6. Blob format (after metadata): E₃(|o|) ‖ E₃(|w|) ‖ E₂(z) ‖ E₃(s) ‖ o ‖ w ‖ E₄(|c|) ‖ c where c is a deblob-format blob. Returns (ProgramBlob, initial registers, initial memory).
def
Jar.JAVM.initCap (blob args : ByteArray) : Option (Jar.JAVM.ProgramBlob × Jar.JAVM.Registers × Jar.JAVM.Memory)Jar.JAVM.initCap (blob args : ByteArray) : Option (Jar.JAVM.ProgramBlob × Jar.JAVM.Registers × Jar.JAVM.Memory)
Initialize PVM from a JAR capability manifest blob. Parses header + cap entries. CODE cap → ProgramBlob. DATA caps → mapped memory regions.
def
Jar.JAVM.initProgram [Jar.JarConfig] (blob args : ByteArray) : Option (Jar.JAVM.ProgramBlob × Jar.JAVM.Registers × Jar.JAVM.Memory)Jar.JAVM.initProgram [Jar.JarConfig] (blob args : ByteArray) : Option (Jar.JAVM.ProgramBlob × Jar.JAVM.Registers × Jar.JAVM.Memory)
Y(p, a) : Program initialization dispatched by capability model.
-
v2 (jar1): capability manifest blob format
-
none (gp072): segmented (GP v0.7.2) memory layout
def
Jar.JAVM.runProgram [Jar.JarConfig] (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResultJar.JAVM.runProgram [Jar.JarConfig] (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) : Jar.JAVM.InvocationResult
Ψ : Core PVM run dispatched by gas model. Uses per-instruction (v0.7.2) or per-basic-block (v0.8.0) gas charging.
def
Jar.JAVM.runWithHostCalls (ctx : Type) [Inhabited ctx] (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) (handler : Jar.JAVM.HostCallHandler ctx) (context : ctx) (runFn : Jar.JAVM.ProgramBlob → Nat → Jar.JAVM.Registers → Jar.JAVM.Memory → Int64 → Jar.JAVM.InvocationResult := Jar.JAVM.run) : Jar.JAVM.InvocationResult × ctxJar.JAVM.runWithHostCalls (ctx : Type) [Inhabited ctx] (prog : Jar.JAVM.ProgramBlob) (pc : Nat) (regs : Jar.JAVM.Registers) (mem : Jar.JAVM.Memory) (gas : Int64) (handler : Jar.JAVM.HostCallHandler ctx) (context : ctx) (runFn : Jar.JAVM.ProgramBlob → Nat → Jar.JAVM.Registers → Jar.JAVM.Memory → Int64 → Jar.JAVM.InvocationResult := Jar.JAVM.run) : Jar.JAVM.InvocationResult × ctx
Ψ_H : PVM invocation with host-call dispatch. GP eq (A.36). Repeatedly runs PVM, handling host calls via the provided handler. Stops on halt, panic, OOG, or fault.
structure
Jar.JAVM.InstrTraceEntry : TypeJar.JAVM.InstrTraceEntry : Type
Single instruction trace entry: PC, opcode number, register snapshot.
Constructor
Jar.JAVM.InstrTraceEntry.mk
Fields
pc : Nat
opcode : Nat
regs : Array UInt64
structure
Jar.JAVM.InstrTraceConfig : TypeJar.JAVM.InstrTraceConfig : Type
Configuration for instruction-level tracing in host-call loops. When enabled, traces all instructions between host calls traceAfterCall..traceBeforeCall.
Constructor
Jar.JAVM.InstrTraceConfig.mk
Fields
enabled : Bool
Enable instruction tracing.
traceAfterCall : Nat
Start tracing after this host call number (0-indexed).
traceBeforeCall : Nat
Stop tracing before this host call number (exclusive).
def
Jar.JAVM.invokeStd (blob : ByteArray) (gasLimit : Jar.Gas) (input : ByteArray) : Jar.Gas × (ByteArray ⊕ Jar.JAVM.ExitReason)Jar.JAVM.invokeStd (blob : ByteArray) (gasLimit : Jar.Gas) (input : ByteArray) : Jar.Gas × (ByteArray ⊕ Jar.JAVM.ExitReason)
Ψ_M : Standard PVM invocation. GP Appendix B. Parses blob, initializes state, runs to completion. Returns (gas_remaining, output_or_error).