9.9. JAR Blob Format🔗

jar1 uses a custom blob format with a magic header, capability entries, and sub-blobs for CODE caps.

def

Jar.JAVM.jarMagic : Nat
Jar.JAVM.jarMagic : Nat

JAR magic value: 'J'=0x4A, 'A'=0x41, 'R'=0x52, 0x02.

structure

Jar.JAVM.JarHeader : Type
Jar.JAVM.JarHeader : Type

JAR header (10 bytes).

Constructor

Jar.JAVM.JarHeader.mk

Fields

memoryPages : Nat

capCount : Nat

invokeCap : Nat

structure

Jar.JAVM.JarCapEntry : Type
Jar.JAVM.JarCapEntry : Type

JAR capability entry (19 bytes).

Constructor

Jar.JAVM.JarCapEntry.mk

Fields

capIndex : Nat

isCode : Bool

basePage : Nat

pageCount : Nat

isRW : Bool

dataOffset : Nat

dataLen : Nat

def

Jar.JAVM.parseJarHeader (blob : ByteArray) :
  Option (Jar.JAVM.JarHeader × Nat)
Jar.JAVM.parseJarHeader
  (blob : ByteArray) :
  Option (Jar.JAVM.JarHeader × Nat)

Parse a JAR header (11 bytes). Returns header + offset after header.

def

Jar.JAVM.parseJarCapEntry (blob : ByteArray) (offset : Nat) :
  Option (Jar.JAVM.JarCapEntry × Nat)
Jar.JAVM.parseJarCapEntry
  (blob : ByteArray) (offset : Nat) :
  Option (Jar.JAVM.JarCapEntry × Nat)

Parse a JAR capability entry (19 bytes) at the given offset.

def

Jar.JAVM.parseCodeSubBlob (blob : ByteArray)
  (dataOffset dataLen : Nat) : Option Jar.JAVM.ProgramBlob
Jar.JAVM.parseCodeSubBlob
  (blob : ByteArray)
  (dataOffset dataLen : Nat) :
  Option Jar.JAVM.ProgramBlob

Parse a CODE cap's sub-blob into a ProgramBlob. Format: jump_len(4) + entry_size(1) + code_len(4) + jt + code + bitmask.