10.7. Program Blob Format (JAR v2)🔗

Programs are distributed as capability manifest blobs. The blob header declares the total memory budget and which CODE/DATA caps to create at init. The kernel parses the manifest, compiles CODE caps, maps DATA caps, writes arguments into the args cap (slot 0), and invokes the program at PC=0 via CALL.

def

Jar.JAVM.Cap.jarMagic : UInt32
Jar.JAVM.Cap.jarMagic : UInt32

JAR magic: 'J','A','R', 0x02.

structure

Jar.JAVM.Cap.ProgramHeader : Type
Jar.JAVM.Cap.ProgramHeader : Type

Parsed JAR header.

Constructor

Jar.JAVM.Cap.ProgramHeader.mk

Fields

memoryPages : Nat

capCount : Nat

invokeCap : Nat

structure

Jar.JAVM.Cap.CapManifestEntry : Type
Jar.JAVM.Cap.CapManifestEntry : Type

Capability manifest entry from the blob.

Constructor

Jar.JAVM.Cap.CapManifestEntry.mk

Fields

capIndex : Nat

capType : Jar.JAVM.Cap.ManifestCapType

basePage : Nat

pageCount : Nat

initAccess : Jar.JAVM.Cap.Access

dataOffset : Nat

dataLen : Nat