Sign-extend a value from n bytes to 64-bit. GP eq (191). sext(n, x) = x + ⌊x / 2^(8n-1)⌋ · (2^64 - 2^(8n)). For n ∈ {1,2,4,8}.
9.7. Instruction Operand Decoding
def
Jar.JAVM.sext (nBytes : Nat) (x : UInt64) : UInt64Jar.JAVM.sext (nBytes : Nat) (x : UInt64) : UInt64
def
Jar.JAVM.sext32 (x : UInt64) : UInt64Jar.JAVM.sext32 (x : UInt64) : UInt64
Sign-extend from 4 bytes (32-bit) to 64-bit.
def
Jar.JAVM.toSigned (x : UInt64) : Int64Jar.JAVM.toSigned (x : UInt64) : Int64
Convert unsigned 64-bit to signed interpretation. GP eq (158). sign(x) = x if x < 2^63, else x - 2^64.
def
Jar.JAVM.toUnsigned (x : Int64) : UInt64Jar.JAVM.toUnsigned (x : Int64) : UInt64
Convert signed back to unsigned.
def
Jar.JAVM.djump (jumpTable : Array UInt32) (addr : UInt64) : Option NatJar.JAVM.djump (jumpTable : Array UInt32) (addr : UInt64) : Option Nat
Dynamic jump validation. GP eq (210). Returns target PC or none (panic).
9.7.1. Register Extraction
def
Jar.JAVM.regA (instrBytes : ByteArray) (pc : Nat) : Fin 13Jar.JAVM.regA (instrBytes : ByteArray) (pc : Nat) : Fin 13
Decode register A from instruction byte 1 (lower 4 bits), capped at 12.
def
Jar.JAVM.regB (instrBytes : ByteArray) (pc : Nat) : Fin 13Jar.JAVM.regB (instrBytes : ByteArray) (pc : Nat) : Fin 13
Decode register B from instruction byte 1 (upper 4 bits), capped at 12.
def
Jar.JAVM.regD (instrBytes : ByteArray) (pc : Nat) : Fin 13Jar.JAVM.regD (instrBytes : ByteArray) (pc : Nat) : Fin 13
Decode register D from instruction byte 2 (lower 4 bits), capped at 12. Used in 3-register format.
9.7.2. Immediate Extraction
def
Jar.JAVM.readImmBytes (code : ByteArray) (offset n : Nat) : UInt64Jar.JAVM.readImmBytes (code : ByteArray) (offset n : Nat) : UInt64
Read n bytes starting at offset from instruction stream, returning LE value.
def
Jar.JAVM.readSignedAt (code : ByteArray) (offset n : Nat) : UInt64Jar.JAVM.readSignedAt (code : ByteArray) (offset n : Nat) : UInt64
Read n bytes and sign-extend (matching Rust read_signed_at).
def
Jar.JAVM.extractImm (code : ByteArray) (pc skip startByte : Nat) : UInt64Jar.JAVM.extractImm (code : ByteArray) (pc skip startByte : Nat) : UInt64
Generic immediate extraction: read sign-extended imm starting at byte startByte.
Available bytes = max(0, ℓ + 1 - startByte), capped at 4.
def
Jar.JAVM.extractImm64 (code : ByteArray) (pc _skip : Nat) : UInt64Jar.JAVM.extractImm64 (code : ByteArray) (pc _skip : Nat) : UInt64
A.5.3: OneRegExtImm — register + 8-byte immediate (load_imm_64).
def
Jar.JAVM.extractOffset (code : ByteArray) (pc skip : Nat) : UInt64Jar.JAVM.extractOffset (code : ByteArray) (pc skip : Nat) : UInt64
A.5.5: OneOffset — jump target. lX = min(4, ℓ), target = ı + Z_lX(...).
9.7.3. Operand Format Decoders
def
Jar.JAVM.extractOneImm (code : ByteArray) (pc skip : Nat) : UInt64Jar.JAVM.extractOneImm (code : ByteArray) (pc skip : Nat) : UInt64
A.5.2: OneImm — one immediate (ecalli). lX = min(4, ℓ), νX = X_lX(E_lX⁻¹(ζ[ı+1..+lX])). Sign-extended per GP. Valid range for jar1: 0-127. Values ≥128 fault the VM.
def
Jar.JAVM.extractRegImm (code : ByteArray) (pc skip : Nat) : Fin 13 × UInt64Jar.JAVM.extractRegImm (code : ByteArray) (pc skip : Nat) : Fin 13 × UInt64
A.5.6: OneRegOneImm — register + one immediate. rA = min(12, ζ[ı+1] mod 16), lX = min(4, max(0, ℓ-1)).
def
Jar.JAVM.extractRegImmOffset (code : ByteArray) (pc skip : Nat) : Fin 13 × UInt64 × UInt64Jar.JAVM.extractRegImmOffset (code : ByteArray) (pc skip : Nat) : Fin 13 × UInt64 × UInt64
A.5.8: OneRegImmOffset — register + immediate + offset (load_imm_jump, branches). Same encoding as OneRegTwoImm but second value is pc-relative offset. Returns (reg, imm, target).
def
Jar.JAVM.extractRegTwoImm (code : ByteArray) (pc skip : Nat) : Fin 13 × UInt64 × UInt64Jar.JAVM.extractRegTwoImm (code : ByteArray) (pc skip : Nat) : Fin 13 × UInt64 × UInt64
A.5.7: OneRegTwoImm — register + two immediates (branch_eq_imm etc). Byte 1: low 4 = reg, bits 4-6 = lX encoding.
def
Jar.JAVM.extractTwoImm (code : ByteArray) (pc skip : Nat) : UInt64 × UInt64Jar.JAVM.extractTwoImm (code : ByteArray) (pc skip : Nat) : UInt64 × UInt64
A.5.4: TwoImm — two immediates (store_imm_*). lX = min(4, ζ[ı+1] mod 8).
def
Jar.JAVM.extractTwoRegImm (code : ByteArray) (pc skip : Nat) : Fin 13 × Fin 13 × UInt64Jar.JAVM.extractTwoRegImm (code : ByteArray) (pc skip : Nat) : Fin 13 × Fin 13 × UInt64
A.5.10: TwoRegOneImm — two registers + one immediate. lX = min(4, max(0, ℓ-1)). Used for ALU ops, loads, stores.
def
Jar.JAVM.extractTwoRegOffset (code : ByteArray) (pc skip : Nat) : Fin 13 × Fin 13 × UInt64Jar.JAVM.extractTwoRegOffset (code : ByteArray) (pc skip : Nat) : Fin 13 × Fin 13 × UInt64
A.5.11: TwoRegOneOffset — two registers + offset. Same as TwoRegOneImm but value is pc-relative. Returns (rA, rB, target).
def
Jar.JAVM.extractTwoRegTwoImm (code : ByteArray) (pc skip : Nat) : Fin 13 × Fin 13 × UInt64 × UInt64Jar.JAVM.extractTwoRegTwoImm (code : ByteArray) (pc skip : Nat) : Fin 13 × Fin 13 × UInt64 × UInt64
A.5.12: TwoRegTwoImm — two registers + two immediates. lX from ζ[ı+2], uses separate encoding byte.
9.7.4. Decode Utilities
def
Jar.JAVM.skipDistance (bm : ByteArray) (i : Nat) : NatJar.JAVM.skipDistance (bm : ByteArray) (i : Nat) : Nat
Skip distance: number of bytes until the next opcode position. GP eq (77). F_skip(i) = min(24, j ∈ ℕ : bitmask[i+1+j] = 1).
def
Jar.JAVM.isTerminator (opcode : Nat) : BoolJar.JAVM.isTerminator (opcode : Nat) : Bool
Check if opcode is a basic block terminator (v0.8.0).
def
Jar.JAVM.zeta (code : ByteArray) (i : Nat) : NatJar.JAVM.zeta (code : ByteArray) (i : Nat) : Nat
Zero-extended code read (ζ, eq A.4).
def
Jar.JAVM.bitmaskGet (bm : ByteArray) (i : Nat) : BoolJar.JAVM.bitmaskGet (bm : ByteArray) (i : Nat) : Bool
Check if bit at position i is set in the (unpacked) bitmask.
After deblob, the bitmask has one byte per code byte (0 or 1).
def
Jar.JAVM.decodeLEn (data : ByteArray) (offset n : Nat) : NatJar.JAVM.decodeLEn (data : ByteArray) (offset n : Nat) : Nat
Decode a fixed-width natural from n LE bytes starting at offset.
def
Jar.JAVM.decodeJamNatural (data : ByteArray) (offset : Nat) : Option (Nat × Nat)Jar.JAVM.decodeJamNatural (data : ByteArray) (offset : Nat) : Option (Nat × Nat)
Decode a JAM codec variable-length natural number. GP Appendix C. Returns (value, bytes_consumed) or none.
def
Jar.JAVM.decodeDeBlobNat (blob : ByteArray) (offset : Nat) (compact : Bool) : Option (Nat × Nat)Jar.JAVM.decodeDeBlobNat (blob : ByteArray) (offset : Nat) (compact : Bool) : Option (Nat × Nat)
Decode a natural from the deblob header. In compact mode (gp072) uses JAM variable-length encoding; in fixed mode (jar1) uses u32 LE.
def
Jar.JAVM.gasPerPage : NatJar.JAVM.gasPerPage : Nat
Gas cost per page for memory allocation.
def
Jar.JAVM.computeMemCycles (totalPages : Nat) : NatJar.JAVM.computeMemCycles (totalPages : Nat) : Nat
Compute memory tier load/store cycles based on total accessible pages.