JAR: JAM Axiomatic Reference

9.6. Interpreter🔗

🔗def
Jar.PVM.run (prog : Jar.PVM.ProgramBlob) (pc : Nat)
  (regs : Jar.PVM.Registers) (mem : Jar.PVM.Memory) (gas : Int64) :
  Jar.PVM.InvocationResult
Jar.PVM.run (prog : Jar.PVM.ProgramBlob)
  (pc : Nat) (regs : Jar.PVM.Registers)
  (mem : Jar.PVM.Memory) (gas : Int64) :
  Jar.PVM.InvocationResult

Ψ : 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.

🔗def
Jar.PVM.initStandard (blob' args : ByteArray) :
  Option (Jar.PVM.ProgramBlob × Jar.PVM.Registers × Jar.PVM.Memory)
Jar.PVM.initStandard
  (blob' args : ByteArray) :
  Option
    (Jar.PVM.ProgramBlob ×
      Jar.PVM.Registers × Jar.PVM.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.PVM.runWithHostCalls (ctx : Type) [Inhabited ctx]
  (prog : Jar.PVM.ProgramBlob) (pc : Nat) (regs : Jar.PVM.Registers)
  (mem : Jar.PVM.Memory) (gas : Int64)
  (handler : Jar.PVM.HostCallHandler ctx) (context : ctx)
  (runFn :
    Jar.PVM.ProgramBlob →
      Nat →
        Jar.PVM.Registers →
          Jar.PVM.Memory → Int64 → Jar.PVM.InvocationResult :=
    Jar.PVM.run) :
  Jar.PVM.InvocationResult × ctx
Jar.PVM.runWithHostCalls (ctx : Type)
  [Inhabited ctx]
  (prog : Jar.PVM.ProgramBlob) (pc : Nat)
  (regs : Jar.PVM.Registers)
  (mem : Jar.PVM.Memory) (gas : Int64)
  (handler : Jar.PVM.HostCallHandler ctx)
  (context : ctx)
  (runFn :
    Jar.PVM.ProgramBlob →
      Nat →
        Jar.PVM.Registers →
          Jar.PVM.Memory →
            Int64 →
              Jar.PVM.InvocationResult :=
    Jar.PVM.run) :
  Jar.PVM.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.

🔗def
Jar.PVM.invokeStd (blob : ByteArray) (gasLimit : Jar.Gas)
  (input : ByteArray) : Jar.Gas × (ByteArray ⊕ Jar.PVM.ExitReason)
Jar.PVM.invokeStd (blob : ByteArray)
  (gasLimit : Jar.Gas)
  (input : ByteArray) :
  Jar.Gas ×
    (ByteArray ⊕ Jar.PVM.ExitReason)

Ψ_M : Standard PVM invocation. GP Appendix B. Parses blob, initializes state, runs to completion. Returns (gas_remaining, output_or_error).