SBPF.CommType — machine words for the sBPF ISA

Fixed-width machine words underpinning the Solana eBPF (sBPF) semantics, ported from the OOPSLA 2025 Isabelle/HOL formalisation (rBPFCommType.thy, Yuan et al., A Complete Formal Semantics of eBPF ISA for Solana).

Every width is modelled as BitVec n: a bit container with no inherent signedness. Signed vs. unsigned behaviour is a property of the operation (BitVec.sdiv / .smod / .sshiftRight vs / / % / >>>), exactly as on real hardware — so a single representation serves both the word and sword roles of the source theory.

Main definitions

• Solanalib.SBPF.U4 … U128 — the machine-word widths.
• Solanalib.SBPF.u8ListOfU64 and friends — little-endian byte serialisation.
• Solanalib.SBPF.u64OfU8List and friends — the parsing inverse.

@[reducible, inline]

abbrev Solanalib.SBPF.U4 : Type

4-bit word — the register-index field of an encoded instruction.

Equations

• Solanalib.SBPF.U4 = BitVec 4

@[reducible, inline]

abbrev Solanalib.SBPF.U8 : Type

8-bit word — a byte.

Equations

• Solanalib.SBPF.U8 = BitVec 8

@[reducible, inline]

abbrev Solanalib.SBPF.U16 : Type

16-bit word — the instruction offset field.

Equations

• Solanalib.SBPF.U16 = BitVec 16

@[reducible, inline]

abbrev Solanalib.SBPF.U32 : Type

32-bit word — the instruction immediate field.

Equations

• Solanalib.SBPF.U32 = BitVec 32

@[reducible, inline]

abbrev Solanalib.SBPF.U64 : Type

64-bit word — the register width.

Equations

• Solanalib.SBPF.U64 = BitVec 64

@[reducible, inline]

abbrev Solanalib.SBPF.U128 : Type

128-bit word — wide-multiply results.

Equations

• Solanalib.SBPF.U128 = BitVec 128

def Solanalib.SBPF.i8Min : U8

Smallest signed 8-bit value (-128), as raw bits.

Equations

• Solanalib.SBPF.i8Min = 128

def Solanalib.SBPF.i8Max : U8

Largest signed 8-bit value (127).

Equations

• Solanalib.SBPF.i8Max = 127

def Solanalib.SBPF.u8Max : U8

Largest unsigned 8-bit value (255).

Equations

• Solanalib.SBPF.u8Max = 255

def Solanalib.SBPF.i32Min : U32

Smallest signed 32-bit value, as raw bits.

Equations

• Solanalib.SBPF.i32Min = 2147483648

def Solanalib.SBPF.i32Max : U32

Largest signed 32-bit value.

Equations

• Solanalib.SBPF.i32Max = 2147483647

def Solanalib.SBPF.u32Max : U32

Largest unsigned 32-bit value.

Equations

• Solanalib.SBPF.u32Max = 4294967295

def Solanalib.SBPF.i64Min : U64

Smallest signed 64-bit value, as raw bits.

Equations

• Solanalib.SBPF.i64Min = 9223372036854775808

def Solanalib.SBPF.i64Max : U64

Largest signed 64-bit value.

Equations

• Solanalib.SBPF.i64Max = 9223372036854775807

def Solanalib.SBPF.u64Max : U64

Largest unsigned 64-bit value.

Equations

• Solanalib.SBPF.u64Max = 18446744073709551615

def Solanalib.SBPF.u8OfBool (b : Bool) : U8

A byte encoding of a boolean: 1 for true, 0 for false.

Equations

• Solanalib.SBPF.u8OfBool b = if b = true then 1 else 0

def Solanalib.SBPF.u8ListOfU16 (i : U16) : List U8

Little-endian bytes of a 16-bit word.

Equations

• Solanalib.SBPF.u8ListOfU16 i = [BitVec.setWidth 8 i, BitVec.setWidth 8 (i >>> 8)]

def Solanalib.SBPF.u8ListOfU32 (i : U32) : List U8

Little-endian bytes of a 32-bit word.

Equations

• Solanalib.SBPF.u8ListOfU32 i = [BitVec.setWidth 8 i, BitVec.setWidth 8 (i >>> 8), BitVec.setWidth 8 (i >>> 16), BitVec.setWidth 8 (i >>> 24)]

def Solanalib.SBPF.u8ListOfU64 (i : U64) : List U8

Little-endian bytes of a 64-bit word.

Equations

• One or more equations did not get rendered due to their size.

def Solanalib.SBPF.u16OfU8List : List U8 → Option U16

Reassemble a little-endian 2-byte list into a 16-bit word.

Equations

• Solanalib.SBPF.u16OfU8List [b0, b1] = some (BitVec.setWidth 16 b0 ||| BitVec.setWidth 16 b1 <<< 8)
• Solanalib.SBPF.u16OfU8List x✝ = none

def Solanalib.SBPF.u32OfU8List : List U8 → Option U32

Reassemble a little-endian 4-byte list into a 32-bit word.

Equations

• Solanalib.SBPF.u32OfU8List [b0, b1, b2, b3] = some (BitVec.setWidth 32 b0 ||| BitVec.setWidth 32 b1 <<< 8 ||| BitVec.setWidth 32 b2 <<< 16 ||| BitVec.setWidth 32 b3 <<< 24)
• Solanalib.SBPF.u32OfU8List x✝ = none

def Solanalib.SBPF.u64OfU8List : List U8 → Option U64

Reassemble a little-endian 8-byte list into a 64-bit word.

Equations

• One or more equations did not get rendered due to their size.
• Solanalib.SBPF.u64OfU8List x✝ = none