JAR: Join-Accumulate Refine

9.6. Program Blob Decoding (Appendix A.5)🔗

🔗structure
Jar.JAVM.ProgramBlob : Type
Jar.JAVM.ProgramBlob : Type

Decoded program blob components.

Constructor

Jar.JAVM.ProgramBlob.mk

Fields

code : ByteArray

Instruction code bytes.

bitmask : ByteArray

Opcode bitmask: bit i is set if byte i is an opcode position.

jumpTable : Array UInt32

Jump table: maps dynamic jump indices to code positions.

🔗def
Jar.JAVM.deblob (blob : ByteArray) (compact : Bool := true) :
  Option Jar.JAVM.ProgramBlob
Jar.JAVM.deblob (blob : ByteArray)
  (compact : Bool := true) :
  Option Jar.JAVM.ProgramBlob

Deblob: parse a program blob into (code, bitmask, jumpTable). GP Appendix A. Format: E(|j|) ‖ E₁(z) ‖ E(|c|) ‖ E_z(j) ‖ c ‖ k where z = jump table entry size (1-4), j = jump table, c = code, k = bitmask. When compact is true, E() uses JAM codec variable-length natural (gp072). When false, E() = E₄() is u32 LE (jar1).

🔗def
Jar.JAVM.validateBasicBlocks (prog : Jar.JAVM.ProgramBlob) : Bool
Jar.JAVM.validateBasicBlocks
  (prog : Jar.JAVM.ProgramBlob) : Bool

Validate a deblobbed program for v0.8.0 basic block requirements:

  1. Last instruction must be a basic block terminator

  2. All branch/jump targets must be valid instruction boundaries (bitmask set) Returns true if valid.