JAR: Join-Accumulate Refine

9.5. Memory Operations (Appendix A.4)🔗

🔗inductive type
Jar.JAVM.MemResult (α : Type) : Type
Jar.JAVM.MemResult (α : Type) : Type

Result of a memory access: success or fault.

Constructors

ok {α : Type} : α → Jar.JAVM.MemResult α
panic {α : Type} : Jar.JAVM.MemResult α
fault {α : Type} : UInt64 → Jar.JAVM.MemResult α
🔗def
Jar.JAVM.pageOf (addr : UInt64) : Nat
Jar.JAVM.pageOf (addr : UInt64) : Nat

Page index for an address.

🔗def
Jar.JAVM.pageAligned (addr : UInt64) : UInt64
Jar.JAVM.pageAligned (addr : UInt64) :
  UInt64

Page-aligned address for fault reporting.

🔗def
Jar.JAVM.checkReadable (m : Jar.JAVM.Memory) (addr : UInt64) (n : Nat) :
  Jar.JAVM.MemResult Unit
Jar.JAVM.checkReadable
  (m : Jar.JAVM.Memory) (addr : UInt64)
  (n : Nat) : Jar.JAVM.MemResult Unit

Check read access for an address range [addr, addr+n).

🔗def
Jar.JAVM.checkWritable (m : Jar.JAVM.Memory) (addr : UInt64) (n : Nat) :
  Jar.JAVM.MemResult Unit
Jar.JAVM.checkWritable
  (m : Jar.JAVM.Memory) (addr : UInt64)
  (n : Nat) : Jar.JAVM.MemResult Unit

Check write access for an address range [addr, addr+n).

🔗def
Jar.JAVM.readMemBytes (m : Jar.JAVM.Memory) (addr : UInt64) (n : Nat) :
  Jar.JAVM.MemResult UInt64
Jar.JAVM.readMemBytes
  (m : Jar.JAVM.Memory) (addr : UInt64)
  (n : Nat) : Jar.JAVM.MemResult UInt64

Read n bytes from memory at address, returning LE-encoded UInt64.

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

Read 1 byte unsigned.

🔗def
Jar.JAVM.readI8 (m : Jar.JAVM.Memory) (addr : UInt64) :
  Jar.JAVM.MemResult UInt64
Jar.JAVM.readI8 (m : Jar.JAVM.Memory)
  (addr : UInt64) :
  Jar.JAVM.MemResult UInt64

Read 1 byte sign-extended.

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

Read 2 bytes unsigned LE.

🔗def
Jar.JAVM.readI16 (m : Jar.JAVM.Memory) (addr : UInt64) :
  Jar.JAVM.MemResult UInt64
Jar.JAVM.readI16 (m : Jar.JAVM.Memory)
  (addr : UInt64) :
  Jar.JAVM.MemResult UInt64

Read 2 bytes sign-extended LE.

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

Read 4 bytes unsigned LE.

🔗def
Jar.JAVM.readI32 (m : Jar.JAVM.Memory) (addr : UInt64) :
  Jar.JAVM.MemResult UInt64
Jar.JAVM.readI32 (m : Jar.JAVM.Memory)
  (addr : UInt64) :
  Jar.JAVM.MemResult UInt64

Read 4 bytes sign-extended LE.

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

Read 8 bytes LE.

🔗def
Jar.JAVM.writeMemBytes (m : Jar.JAVM.Memory) (addr val : UInt64)
  (n : Nat) : Jar.JAVM.MemResult Jar.JAVM.Memory
Jar.JAVM.writeMemBytes
  (m : Jar.JAVM.Memory)
  (addr val : UInt64) (n : Nat) :
  Jar.JAVM.MemResult Jar.JAVM.Memory

Write bytes to memory at address in LE order. Returns updated memory or fault.

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

Write 1 byte.

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

Write 2 bytes LE.

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

Write 4 bytes LE.

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

Write 8 bytes LE.

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

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

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

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

🔗def
Jar.JAVM.sbrk (m : Jar.JAVM.Memory) (sizeBytes : UInt64) :
  Jar.JAVM.Memory × UInt64
Jar.JAVM.sbrk (m : Jar.JAVM.Memory)
  (sizeBytes : UInt64) :
  Jar.JAVM.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.