𝕣 : Register value. ℕ_{2^64}. GP eq (A.1).
9.1. Machine Model
def
Jar.PVM.Reg : TypeJar.PVM.Reg : Type
def
Jar.PVM.Registers : TypeJar.PVM.Registers : Type
Register file: 13 × 64-bit registers. ⟦𝕣⟧_13.
inductive type
Jar.PVM.PageAccess : TypeJar.PVM.PageAccess : Type
Page access mode. GP eq (4.17).
Constructors
writable : Jar.PVM.PageAccess
readable : Jar.PVM.PageAccess
inaccessible : Jar.PVM.PageAccess
structure
Jar.PVM.Memory : TypeJar.PVM.Memory : Type
μ : RAM state. GP eq (4.17). μ ≡ ⟨μ_v : 𝔹_{2^32}, μ_a : ⟦{W, R, ∅}⟧_p⟩ where p = 2^32 / Z_P. Uses sparse page storage: only materialized pages are stored.
Constructor
Jar.PVM.Memory.mk
Fields
pages : Dict Nat ByteArray
μ_v : Memory contents, sparse by page. Dict from page index to page data.
access : Array Jar.PVM.PageAccess
μ_a : Per-page access flags.
heapTop : Nat
Heap top pointer (byte address) for sbrk.
guardZone : Nat
Guard zone size: addresses below this return .panic on access. Z_Z (65536) for standard GP layout, 0 for contiguous linear memory.
structure
Jar.PVM.MachineState : TypeJar.PVM.MachineState : Type
Complete PVM machine state.
Constructor
Jar.PVM.MachineState.mk
Fields
registers : Jar.PVM.Registers
ω : Register file. ⟦𝕣⟧_13.
memory : Jar.PVM.Memory
μ : RAM.
gas : Jar.SignedGas
ζ : Gas remaining.
pc : Jar.PVM.Reg
ι : Program counter.
inductive type
Jar.PVM.ExitReason : TypeJar.PVM.ExitReason : Type
PVM exit reason. GP Appendix A.
Constructors
halt : Jar.PVM.ExitReason
Regular termination (halt instruction).
panic : Jar.PVM.ExitReason
Irregular termination (exceptional circumstance).
outOfGas : Jar.PVM.ExitReason
Gas exhaustion.
pageFault (address : Jar.PVM.Reg) : Jar.PVM.ExitReason
Page fault: attempt to access inaccessible address.
hostCall (id : Jar.PVM.Reg) : Jar.PVM.ExitReason
Host-call request: ecalli instruction with identifier.
structure
Jar.PVM.InvocationResult : TypeJar.PVM.InvocationResult : Type
Result of a PVM invocation.
Constructor
Jar.PVM.InvocationResult.mk
Fields
exitReason : Jar.PVM.ExitReason
Exit reason (halt/panic/oog/fault/host).
exitValue : Jar.PVM.Reg
ω_7 : Value in register 7 at exit (status/return value).
gas : Jar.SignedGas
Gas counter at exit (may be negative for OOG).
registers : Jar.PVM.Registers
Final register file.
memory : Jar.PVM.Memory
Final memory state.
nextPC : Nat
Next PC (valid after hostCall, for resumption).
lastPC : Nat
Last PC before exit.
inductive type
Jar.PVM.InstructionCategory : TypeJar.PVM.InstructionCategory : Type
PVM instruction categories (for documentation; not used in execution).
Constructors
noArgs : Jar.PVM.InstructionCategory
oneImmediate : Jar.PVM.InstructionCategory
regImm64 : Jar.PVM.InstructionCategory
twoImm : Jar.PVM.InstructionCategory
offset : Jar.PVM.InstructionCategory
regImm : Jar.PVM.InstructionCategory
twoReg : Jar.PVM.InstructionCategory
threeReg : Jar.PVM.InstructionCategory