JAR: Join-Accumulate Refine

9.3. Machine Model🔗

🔗def
Jar.JAVM.Reg : Type
Jar.JAVM.Reg : Type

𝕣 : Register value. ℕ_{2^64}. GP eq (A.1).

🔗def
Jar.JAVM.Registers : Type
Jar.JAVM.Registers : Type

Register file: 13 × 64-bit registers. ⟦𝕣⟧_13.

🔗inductive type
Jar.JAVM.PageAccess : Type
Jar.JAVM.PageAccess : Type

Page access mode. GP eq (4.17).

Constructors

writable : Jar.JAVM.PageAccess
readable : Jar.JAVM.PageAccess
inaccessible : Jar.JAVM.PageAccess
🔗structure
Jar.JAVM.Memory : Type
Jar.JAVM.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.JAVM.Memory.mk

Fields

pages : Dict Nat ByteArray

μ_v : Memory contents, sparse by page. Dict from page index to page data.

access : Array Jar.JAVM.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.

🔗def
Jar.JAVM.Memory.getByte (m : Jar.JAVM.Memory) (addr : Nat) : UInt8
Jar.JAVM.Memory.getByte
  (m : Jar.JAVM.Memory) (addr : Nat) :
  UInt8

Read a byte from sparse memory. Unmaterialized pages return 0.

🔗def
Jar.JAVM.Memory.setByte (m : Jar.JAVM.Memory) (addr : Nat)
  (val : UInt8) : Jar.JAVM.Memory
Jar.JAVM.Memory.setByte
  (m : Jar.JAVM.Memory) (addr : Nat)
  (val : UInt8) : Jar.JAVM.Memory

Write a byte to sparse memory. Materializes page if needed.

🔗def
Jar.JAVM.Memory.isReadable (m : Jar.JAVM.Memory) (addr : Nat) : Bool
Jar.JAVM.Memory.isReadable
  (m : Jar.JAVM.Memory) (addr : Nat) :
  Bool

R(μ) : Set of readable addresses. GP eq (4.18). i ∈ R(μ) iff μ_a[⌊i / Z_P⌋] ≠ ∅

🔗def
Jar.JAVM.Memory.isWritable (m : Jar.JAVM.Memory) (addr : Nat) : Bool
Jar.JAVM.Memory.isWritable
  (m : Jar.JAVM.Memory) (addr : Nat) :
  Bool

W(μ) : Set of writable addresses. GP eq (4.19). i ∈ W(μ) iff μ_a[⌊i / Z_P⌋] = W

🔗structure
Jar.JAVM.MachineState : Type
Jar.JAVM.MachineState : Type

Complete PVM machine state.

Constructor

Jar.JAVM.MachineState.mk

Fields

registers : Jar.JAVM.Registers

ω : Register file. ⟦𝕣⟧_13.

memory : Jar.JAVM.Memory

μ : RAM.

gas : Jar.SignedGas

ζ : Gas remaining.

pc : Jar.JAVM.Reg

ι : Program counter.

🔗inductive type
Jar.JAVM.ExitReason : Type
Jar.JAVM.ExitReason : Type

PVM exit reason. GP Appendix A.

Constructors

halt : Jar.JAVM.ExitReason

Regular termination (halt instruction).

trap : Jar.JAVM.ExitReason

Deliberate termination (trap instruction, opcode 0).

panic : Jar.JAVM.ExitReason

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

outOfGas : Jar.JAVM.ExitReason

Gas exhaustion.

pageFault (address : Jar.JAVM.Reg) : Jar.JAVM.ExitReason

Page fault: attempt to access inaccessible address.

hostCall (id : Jar.JAVM.Reg) : Jar.JAVM.ExitReason

Host-call request: ecalli instruction with identifier.

ecall : Jar.JAVM.ExitReason

Management op / dynamic CALL: ecall instruction (opcode 3).

🔗structure
Jar.JAVM.InvocationResult : Type
Jar.JAVM.InvocationResult : Type

Result of a PVM invocation.

Constructor

Jar.JAVM.InvocationResult.mk

Fields

exitReason : Jar.JAVM.ExitReason

Exit reason (halt/panic/oog/fault/host).

exitValue : Jar.JAVM.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.JAVM.Registers

Final register file.

memory : Jar.JAVM.Memory

Final memory state.

nextPC : Nat

Next PC (valid after hostCall, for resumption).

lastPC : Nat

Last PC before exit.

🔗def
Jar.JAVM.HostCallHandler (ctx : Type) : Type
Jar.JAVM.HostCallHandler (ctx : Type) :
  Type

Host-call handler type. Takes call id, gas, registers, memory, and returns updated state. The host context is parameterized.

🔗inductive type
Jar.JAVM.InstructionCategory : Type
Jar.JAVM.InstructionCategory : Type

PVM instruction categories (for documentation; not used in execution).

Constructors

noArgs : Jar.JAVM.InstructionCategory
oneImmediate : Jar.JAVM.InstructionCategory
regImm64 : Jar.JAVM.InstructionCategory
twoImm : Jar.JAVM.InstructionCategory
offset : Jar.JAVM.InstructionCategory
regImm : Jar.JAVM.InstructionCategory
twoReg : Jar.JAVM.InstructionCategory
threeReg : Jar.JAVM.InstructionCategory