SBPF.Syntax — the sBPF instruction set

Abstract syntax of the Solana eBPF (sBPF) instruction set, ported from rBPFSyntax.thy. The headline type is Solanalib.SBPF.BpfInstruction, the 22-constructor algebraic representation of a decoded instruction, together with the register, operand, operation, condition, and version enumerations it uses.

Main definitions

• Solanalib.SBPF.BpfIReg — the eleven integer registers BR0 … BR10.
• Solanalib.SBPF.SndOp — an instruction's second operand (immediate or register).
• Solanalib.SBPF.BpfInstruction — a decoded sBPF instruction.
• Solanalib.SBPF.BpfIReg.toU4 / ofU4 — the register ↔ 4-bit-field bridge.

inductive Solanalib.SBPF.BpfIReg : Type

The eleven sBPF integer registers. BR10 is the read-only frame pointer.

• br0 : BpfIReg
• br1 : BpfIReg
• br2 : BpfIReg
• br3 : BpfIReg
• br4 : BpfIReg
• br5 : BpfIReg
• br6 : BpfIReg
• br7 : BpfIReg
• br8 : BpfIReg
• br9 : BpfIReg
• br10 : BpfIReg

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqBpfIReg : DecidableEq BpfIReg

Equations

• Solanalib.SBPF.instDecidableEqBpfIReg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Solanalib.SBPF.instReprBpfIReg : Repr BpfIReg

Equations

• Solanalib.SBPF.instReprBpfIReg = { reprPrec := Solanalib.SBPF.instReprBpfIReg.repr }

def Solanalib.SBPF.instReprBpfIReg.repr : BpfIReg → Nat → Std.Format

Equations

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

inductive Solanalib.SBPF.SndOp : Type

An instruction's second operand: an immediate or a source register.

• imm (i : U32) : SndOp
• reg (r : BpfIReg) : SndOp

def Solanalib.SBPF.instDecidableEqSndOp.decEq (x✝ x✝¹ : SndOp) : Decidable (x✝ = x✝¹)

Equations

• Solanalib.SBPF.instDecidableEqSndOp.decEq (Solanalib.SBPF.SndOp.imm a) (Solanalib.SBPF.SndOp.imm b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Solanalib.SBPF.instDecidableEqSndOp.decEq (Solanalib.SBPF.SndOp.imm i) (Solanalib.SBPF.SndOp.reg r) = isFalse ⋯
• Solanalib.SBPF.instDecidableEqSndOp.decEq (Solanalib.SBPF.SndOp.reg r) (Solanalib.SBPF.SndOp.imm i) = isFalse ⋯
• Solanalib.SBPF.instDecidableEqSndOp.decEq (Solanalib.SBPF.SndOp.reg a) (Solanalib.SBPF.SndOp.reg b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqSndOp : DecidableEq SndOp

Equations

• Solanalib.SBPF.instDecidableEqSndOp = Solanalib.SBPF.instDecidableEqSndOp.decEq

def Solanalib.SBPF.instReprSndOp.repr : SndOp → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Solanalib.SBPF.instReprSndOp : Repr SndOp

Equations

• Solanalib.SBPF.instReprSndOp = { reprPrec := Solanalib.SBPF.instReprSndOp.repr }

inductive Solanalib.SBPF.Arch : Type

Operand width selector for ALU operations.

• a32 : Arch
• a64 : Arch

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqArch : DecidableEq Arch

Equations

• Solanalib.SBPF.instDecidableEqArch x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Solanalib.SBPF.instReprArch.repr : Arch → Nat → Std.Format

Equations

• Solanalib.SBPF.instReprArch.repr Solanalib.SBPF.Arch.a32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Arch.a32")).group prec✝
• Solanalib.SBPF.instReprArch.repr Solanalib.SBPF.Arch.a64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Arch.a64")).group prec✝

@[implicit_reducible]

instance Solanalib.SBPF.instReprArch : Repr Arch

Equations

• Solanalib.SBPF.instReprArch = { reprPrec := Solanalib.SBPF.instReprArch.repr }

def Solanalib.SBPF.Arch.bits : Arch → Nat

The width, in bits, selected by an Arch.

Equations

• Solanalib.SBPF.Arch.a32.bits = 32
• Solanalib.SBPF.Arch.a64.bits = 64

inductive Solanalib.SBPF.Condition : Type

Branch condition for a conditional jump. The s-prefixed variants are the signed comparisons.

• eq : Condition
• gt : Condition
• ge : Condition
• lt : Condition
• le : Condition
• sEt : Condition
• ne : Condition
• sGt : Condition
• sGe : Condition
• sLt : Condition
• sLe : Condition

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqCondition : DecidableEq Condition

Equations

• Solanalib.SBPF.instDecidableEqCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Solanalib.SBPF.instReprCondition : Repr Condition

Equations

• Solanalib.SBPF.instReprCondition = { reprPrec := Solanalib.SBPF.instReprCondition.repr }

def Solanalib.SBPF.instReprCondition.repr : Condition → Nat → Std.Format

Equations

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

inductive Solanalib.SBPF.Binop : Type

Core ALU binary operations (shared by the 32- and 64-bit ALU classes).

• add : Binop
• sub : Binop
• mul : Binop
• div : Binop
• or : Binop
• and : Binop
• lsh : Binop
• rsh : Binop
• mod : Binop
• xor : Binop
• mov : Binop
• arsh : Binop

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqBinop : DecidableEq Binop

Equations

• Solanalib.SBPF.instDecidableEqBinop x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Solanalib.SBPF.instReprBinop : Repr Binop

Equations

• Solanalib.SBPF.instReprBinop = { reprPrec := Solanalib.SBPF.instReprBinop.repr }

def Solanalib.SBPF.instReprBinop.repr : Binop → Nat → Std.Format

Equations

• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.add prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.add")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.sub")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.mul prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.mul")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.div prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.div")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.or prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.or")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.and prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.and")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.lsh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.lsh")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.rsh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.rsh")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.mod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.mod")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.xor prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.xor")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.mov prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.mov")).group prec✝
• Solanalib.SBPF.instReprBinop.repr Solanalib.SBPF.Binop.arsh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Binop.arsh")).group prec✝

inductive Solanalib.SBPF.Pqrop : Type

Product/quotient/remainder operations (the sBPF PQR class).

• lmul : Pqrop
• udiv : Pqrop
• urem : Pqrop
• sdiv : Pqrop
• srem : Pqrop

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqPqrop : DecidableEq Pqrop

Equations

• Solanalib.SBPF.instDecidableEqPqrop x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Solanalib.SBPF.instReprPqrop : Repr Pqrop

Equations

• Solanalib.SBPF.instReprPqrop = { reprPrec := Solanalib.SBPF.instReprPqrop.repr }

def Solanalib.SBPF.instReprPqrop.repr : Pqrop → Nat → Std.Format

Equations

• Solanalib.SBPF.instReprPqrop.repr Solanalib.SBPF.Pqrop.lmul prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Pqrop.lmul")).group prec✝
• Solanalib.SBPF.instReprPqrop.repr Solanalib.SBPF.Pqrop.udiv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Pqrop.udiv")).group prec✝
• Solanalib.SBPF.instReprPqrop.repr Solanalib.SBPF.Pqrop.urem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Pqrop.urem")).group prec✝
• Solanalib.SBPF.instReprPqrop.repr Solanalib.SBPF.Pqrop.sdiv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Pqrop.sdiv")).group prec✝
• Solanalib.SBPF.instReprPqrop.repr Solanalib.SBPF.Pqrop.srem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Pqrop.srem")).group prec✝

inductive Solanalib.SBPF.Pqrop2 : Type

High-half multiply operations (the sBPF PQR2 class).

• uhmul : Pqrop2
• shmul : Pqrop2

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqPqrop2 : DecidableEq Pqrop2

Equations

• Solanalib.SBPF.instDecidableEqPqrop2 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Solanalib.SBPF.instReprPqrop2.repr : Pqrop2 → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Solanalib.SBPF.instReprPqrop2 : Repr Pqrop2

Equations

• Solanalib.SBPF.instReprPqrop2 = { reprPrec := Solanalib.SBPF.instReprPqrop2.repr }

inductive Solanalib.SBPF.Chunk : Type

Byte-swap / load width selector (the source theory's chunk).

• byte : Chunk
• halfWord : Chunk
• sWord : Chunk
• dWord : Chunk

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqChunk : DecidableEq Chunk

Equations

• Solanalib.SBPF.instDecidableEqChunk x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Solanalib.SBPF.instReprChunk : Repr Chunk

Equations

• Solanalib.SBPF.instReprChunk = { reprPrec := Solanalib.SBPF.instReprChunk.repr }

def Solanalib.SBPF.instReprChunk.repr : Chunk → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Solanalib.SBPF.instReprChunk.repr Solanalib.SBPF.Chunk.byte prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.Chunk.byte")).group prec✝

inductive Solanalib.SBPF.SBPFV : Type

sBPF bytecode version. v1 is the legacy format; v2 is current.

• v1 : SBPFV
• v2 : SBPFV

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqSBPFV : DecidableEq SBPFV

Equations

• Solanalib.SBPF.instDecidableEqSBPFV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Solanalib.SBPF.instReprSBPFV.repr : SBPFV → Nat → Std.Format

Equations

• Solanalib.SBPF.instReprSBPFV.repr Solanalib.SBPF.SBPFV.v1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.SBPFV.v1")).group prec✝
• Solanalib.SBPF.instReprSBPFV.repr Solanalib.SBPF.SBPFV.v2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solanalib.SBPF.SBPFV.v2")).group prec✝

@[implicit_reducible]

instance Solanalib.SBPF.instReprSBPFV : Repr SBPFV

Equations

• Solanalib.SBPF.instReprSBPFV = { reprPrec := Solanalib.SBPF.instReprSBPFV.repr }

inductive Solanalib.SBPF.BpfInstruction : Type

A decoded sBPF instruction. Constructors mirror rBPFSyntax.thy's bpf_instruction; immediate fields are U32, offsets U16, interpreted signed where the semantics requires it.

• ldImm (dst : BpfIReg) (immLo immHi : U32) : BpfInstruction

  Load a 64-bit immediate (assembled from two 32-bit halves).

• ldx (chunk : MemoryChunk) (dst src : BpfIReg) (off : U16) : BpfInstruction

  Load from memory: dst := mem[src + off] at width chunk.

• st (chunk : MemoryChunk) (dst : BpfIReg) (src : SndOp) (off : U16) : BpfInstruction

  Store to memory: mem[dst + off] := src at width chunk.

• addStk (imm : U32) : BpfInstruction

  Add an immediate to the stack pointer.

• alu (op : Binop) (dst : BpfIReg) (src : SndOp) : BpfInstruction

  32-bit ALU operation.

• neg32Reg (dst : BpfIReg) : BpfInstruction

  32-bit register negation.

• le (dst : BpfIReg) (imm : U32) : BpfInstruction

  Little-endian byte swap.

• be (dst : BpfIReg) (imm : U32) : BpfInstruction

  Big-endian byte swap.

• alu64 (op : Binop) (dst : BpfIReg) (src : SndOp) : BpfInstruction

  64-bit ALU operation.

• neg64Reg (dst : BpfIReg) : BpfInstruction

  64-bit register negation.

• hor64Imm (dst : BpfIReg) (imm : U32) : BpfInstruction

  OR a high-order 32-bit immediate into dst (v2 only).

• pqr (op : Pqrop) (dst : BpfIReg) (src : SndOp) : BpfInstruction

  32-bit product/quotient/remainder operation.

• pqr64 (op : Pqrop) (dst : BpfIReg) (src : SndOp) : BpfInstruction

  64-bit product/quotient/remainder operation.

• pqr2 (op : Pqrop2) (dst : BpfIReg) (src : SndOp) : BpfInstruction

  High-half multiply operation.

• ja (off : U16) : BpfInstruction

  Unconditional jump by off.

• jump (cond : Condition) (r : BpfIReg) (src : SndOp) (off : U16) : BpfInstruction

  Conditional jump by off when cond holds between r and src.

• callReg (src : BpfIReg) (imm : U32) : BpfInstruction

  Call the function whose address is held in register src.

• callImm (src : BpfIReg) (imm : U32) : BpfInstruction

  Call the function identified by immediate imm.

• exit : BpfInstruction

  Return from the current frame, or halt at call depth 0.

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqBpfInstruction : DecidableEq BpfInstruction

Equations

• Solanalib.SBPF.instDecidableEqBpfInstruction = Solanalib.SBPF.instDecidableEqBpfInstruction.decEq

def Solanalib.SBPF.instDecidableEqBpfInstruction.decEq (x✝ x✝¹ : BpfInstruction) : Decidable (x✝ = x✝¹)

Equations

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

def Solanalib.SBPF.instReprBpfInstruction.repr : BpfInstruction → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Solanalib.SBPF.instReprBpfInstruction : Repr BpfInstruction

Equations

• Solanalib.SBPF.instReprBpfInstruction = { reprPrec := Solanalib.SBPF.instReprBpfInstruction.repr }

@[reducible, inline]

abbrev Solanalib.SBPF.EbpfAsm : Type

A program in assembly form: a list of decoded instructions.

Equations

• Solanalib.SBPF.EbpfAsm = List Solanalib.SBPF.BpfInstruction

@[reducible, inline]

abbrev Solanalib.SBPF.BpfBin : Type

A program in binary form: a flat list of bytes.

Equations

• Solanalib.SBPF.BpfBin = List Solanalib.SBPF.U8

def Solanalib.SBPF.BpfIReg.toU4 : BpfIReg → U4

The 4-bit register-index field for a register.

Equations

• Solanalib.SBPF.BpfIReg.br0.toU4 = 0
• Solanalib.SBPF.BpfIReg.br1.toU4 = 1
• Solanalib.SBPF.BpfIReg.br2.toU4 = 2
• Solanalib.SBPF.BpfIReg.br3.toU4 = 3
• Solanalib.SBPF.BpfIReg.br4.toU4 = 4
• Solanalib.SBPF.BpfIReg.br5.toU4 = 5
• Solanalib.SBPF.BpfIReg.br6.toU4 = 6
• Solanalib.SBPF.BpfIReg.br7.toU4 = 7
• Solanalib.SBPF.BpfIReg.br8.toU4 = 8
• Solanalib.SBPF.BpfIReg.br9.toU4 = 9
• Solanalib.SBPF.BpfIReg.br10.toU4 = 10

def Solanalib.SBPF.BpfIReg.ofU4 (d : U4) : Option BpfIReg

Decode a 4-bit register-index field, rejecting out-of-range values.

Equations

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