JAR: JAM Axiomatic Reference

9.4. Instruction Decoding (Appendix A.5)🔗

🔗def
Jar.PVM.sext (nBytes : Nat) (x : UInt64) : UInt64
Jar.PVM.sext (nBytes : Nat) (x : UInt64) :
  UInt64

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}.

🔗def
Jar.PVM.toSigned (x : UInt64) : Int64
Jar.PVM.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.PVM.toUnsigned (x : Int64) : UInt64
Jar.PVM.toUnsigned (x : Int64) : UInt64

Convert signed back to unsigned.

🔗def
Jar.PVM.djump (jumpTable : Array UInt32) (addr : UInt64) : Option Nat
Jar.PVM.djump (jumpTable : Array UInt32)
  (addr : UInt64) : Option Nat

Dynamic jump validation. GP eq (210). Returns target PC or none (panic).