JAR: JAM Axiomatic Reference

9.3. Memory Operations (Appendix A.4)🔗

🔗def
Jar.PVM.readU8 (m : Jar.PVM.Memory) (addr : UInt64) :
  Jar.PVM.MemResult UInt64
Jar.PVM.readU8 (m : Jar.PVM.Memory)
  (addr : UInt64) :
  Jar.PVM.MemResult UInt64

Read 1 byte unsigned.

🔗def
Jar.PVM.readU16 (m : Jar.PVM.Memory) (addr : UInt64) :
  Jar.PVM.MemResult UInt64
Jar.PVM.readU16 (m : Jar.PVM.Memory)
  (addr : UInt64) :
  Jar.PVM.MemResult UInt64

Read 2 bytes unsigned LE.

🔗def
Jar.PVM.readU32 (m : Jar.PVM.Memory) (addr : UInt64) :
  Jar.PVM.MemResult UInt64
Jar.PVM.readU32 (m : Jar.PVM.Memory)
  (addr : UInt64) :
  Jar.PVM.MemResult UInt64

Read 4 bytes unsigned LE.

🔗def
Jar.PVM.readU64 (m : Jar.PVM.Memory) (addr : UInt64) :
  Jar.PVM.MemResult UInt64
Jar.PVM.readU64 (m : Jar.PVM.Memory)
  (addr : UInt64) :
  Jar.PVM.MemResult UInt64

Read 8 bytes LE.

🔗def
Jar.PVM.writeU8 (m : Jar.PVM.Memory) (addr val : UInt64) :
  Jar.PVM.MemResult Jar.PVM.Memory
Jar.PVM.writeU8 (m : Jar.PVM.Memory)
  (addr val : UInt64) :
  Jar.PVM.MemResult Jar.PVM.Memory

Write 1 byte.

🔗def
Jar.PVM.writeU16 (m : Jar.PVM.Memory) (addr val : UInt64) :
  Jar.PVM.MemResult Jar.PVM.Memory
Jar.PVM.writeU16 (m : Jar.PVM.Memory)
  (addr val : UInt64) :
  Jar.PVM.MemResult Jar.PVM.Memory

Write 2 bytes LE.

🔗def
Jar.PVM.writeU32 (m : Jar.PVM.Memory) (addr val : UInt64) :
  Jar.PVM.MemResult Jar.PVM.Memory
Jar.PVM.writeU32 (m : Jar.PVM.Memory)
  (addr val : UInt64) :
  Jar.PVM.MemResult Jar.PVM.Memory

Write 4 bytes LE.

🔗def
Jar.PVM.writeU64 (m : Jar.PVM.Memory) (addr val : UInt64) :
  Jar.PVM.MemResult Jar.PVM.Memory
Jar.PVM.writeU64 (m : Jar.PVM.Memory)
  (addr val : UInt64) :
  Jar.PVM.MemResult Jar.PVM.Memory

Write 8 bytes LE.

🔗def
Jar.PVM.readByteArray (m : Jar.PVM.Memory) (addr : UInt64) (n : Nat) :
  Jar.PVM.MemResult ByteArray
Jar.PVM.readByteArray (m : Jar.PVM.Memory)
  (addr : UInt64) (n : Nat) :
  Jar.PVM.MemResult ByteArray

Read n raw bytes from memory starting at addr. Returns ByteArray or fault.

🔗def
Jar.PVM.writeByteArray (m : Jar.PVM.Memory) (addr : UInt64)
  (data : ByteArray) : Jar.PVM.MemResult Jar.PVM.Memory
Jar.PVM.writeByteArray
  (m : Jar.PVM.Memory) (addr : UInt64)
  (data : ByteArray) :
  Jar.PVM.MemResult Jar.PVM.Memory

Write a ByteArray into memory starting at addr. Returns updated memory or fault.

🔗def
Jar.PVM.sbrk (m : Jar.PVM.Memory) (sizeBytes : UInt64) :
  Jar.PVM.Memory × UInt64
Jar.PVM.sbrk (m : Jar.PVM.Memory)
  (sizeBytes : UInt64) :
  Jar.PVM.Memory × UInt64

sbrk(n): Grow the heap by n pages. Returns new heap base or 0 on failure. Finds the first inaccessible page after existing writable heap and marks n new pages as writable.