SBPF.Interpreter — the small-step sBPF semantics

The operational semantics of the Solana eBPF interpreter, ported from Interpreter.thy: the per-class evaluators (evalAlu32/64, evalPqr*, evalJmp, evalLoad/Store, the call/exit frame machinery), the single-step function step, and the fuel-bounded driver bpfInterp.

Registers are raw U64; signed behaviour is expressed with BitVec's signed operations (sdiv/srem/slt/sshiftRight) and sign-extension, faithful to the source theory. Note the sBPF-specific quirk (Challenge 1 of the paper): the 32-bit ADD/SUB/MUL results are sign-extended into the 64-bit register, whereas the logical/shift results are zero-extended.

Main definitions

• Solanalib.SBPF.step — execute one instruction, yielding a BpfState.
• Solanalib.SBPF.bpfInterp — run the program under a fuel bound.

Operand evaluation

def Solanalib.SBPF.sndOp32 (sop : SndOp) (rs : RegMap) : U32

The second operand as a 32-bit value: immediate verbatim, or the low 32 bits of the source register (eval_snd_op_{i,u}32 — same bits either way).

Equations

• Solanalib.SBPF.sndOp32 (Solanalib.SBPF.SndOp.imm i) rs = i
• Solanalib.SBPF.sndOp32 (Solanalib.SBPF.SndOp.reg r) rs = BitVec.setWidth 32 (rs r)

def Solanalib.SBPF.sndOp64 (sop : SndOp) (rs : RegMap) : U64

The second operand as a 64-bit value: a sign-extended immediate, or the source register verbatim (eval_snd_op_{i,u}64 — same bits either way).

Equations

• Solanalib.SBPF.sndOp64 (Solanalib.SBPF.SndOp.imm i) rs = BitVec.signExtend 64 i
• Solanalib.SBPF.sndOp64 (Solanalib.SBPF.SndOp.reg r) rs = rs r

ALU

def Solanalib.SBPF.evalAlu32 (bop : Binop) (dst : BpfIReg) (sop : SndOp) (rs : RegMap) (isV1 : Bool) : RegOutcome

32-bit ALU (eval_alu32). Add/sub/mul sign-extend the 32-bit result; the rest zero-extend. mul/div/mod are v1-only.

Equations

• One or more equations did not get rendered due to their size.
• Solanalib.SBPF.evalAlu32 Solanalib.SBPF.Binop.mov dst sop rs isV1 = Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (BitVec.setWidth 64 (Solanalib.SBPF.sndOp32 sop rs)))

def Solanalib.SBPF.evalAlu64 (bop : Binop) (dst : BpfIReg) (sop : SndOp) (rs : RegMap) (isV1 : Bool) : RegOutcome

64-bit ALU (eval_alu64). mul/div/mod are v1-only; the shift amount is masked to 6 bits.

Equations

• One or more equations did not get rendered due to their size.
• Solanalib.SBPF.evalAlu64 Solanalib.SBPF.Binop.add dst sop rs isV1 = Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (rs dst + Solanalib.SBPF.sndOp64 sop rs))
• Solanalib.SBPF.evalAlu64 Solanalib.SBPF.Binop.or dst sop rs isV1 = Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (rs dst ||| Solanalib.SBPF.sndOp64 sop rs))
• Solanalib.SBPF.evalAlu64 Solanalib.SBPF.Binop.and dst sop rs isV1 = Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (rs dst &&& Solanalib.SBPF.sndOp64 sop rs))
• Solanalib.SBPF.evalAlu64 Solanalib.SBPF.Binop.xor dst sop rs isV1 = Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (rs dst ^^^ Solanalib.SBPF.sndOp64 sop rs))
• Solanalib.SBPF.evalAlu64 Solanalib.SBPF.Binop.mov dst sop rs isV1 = Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (Solanalib.SBPF.sndOp64 sop rs))
• Solanalib.SBPF.evalAlu64 Solanalib.SBPF.Binop.lsh dst sop rs isV1 = Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (rs dst <<< BitVec.toNat (Solanalib.SBPF.sndOp32 sop rs &&& 63)))
• Solanalib.SBPF.evalAlu64 Solanalib.SBPF.Binop.rsh dst sop rs isV1 = Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (rs dst >>> BitVec.toNat (Solanalib.SBPF.sndOp32 sop rs &&& 63)))

def Solanalib.SBPF.evalAdd64ImmR10 (i : U32) (ss : StackState) (isV1 : Bool) : Option StackState

Add a (sign-extended) immediate to the stack pointer (eval_add64_imm_R10). v2-only.

Equations

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

def Solanalib.SBPF.evalNeg32 (dst : BpfIReg) (rs : RegMap) (isV1 : Bool) : RegOutcome

32-bit negate (eval_neg32). v1-only.

Equations

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

def Solanalib.SBPF.evalNeg64 (dst : BpfIReg) (rs : RegMap) (isV1 : Bool) : RegOutcome

64-bit negate (eval_neg64). v1-only.

Equations

• Solanalib.SBPF.evalNeg64 dst rs isV1 = if isV1 = true then Solanalib.SBPF.RegOutcome.oks (Solanalib.SBPF.setReg rs dst (-rs dst)) else Solanalib.SBPF.RegOutcome.okn

def Solanalib.SBPF.evalLe (dst : BpfIReg) (imm : U32) (rs : RegMap) (isV1 : Bool) : RegOutcome

Little-endian byte swap / truncation (eval_le). v1-only.

Equations

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

def Solanalib.SBPF.evalBe (dst : BpfIReg) (imm : U32) (rs : RegMap) (isV1 : Bool) : RegOutcome

Big-endian byte swap (eval_be): reverse the bytes before reassembly. v1-only.

Equations

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

def Solanalib.SBPF.evalHor64 (dst : BpfIReg) (imm : U32) (rs : RegMap) (isV1 : Bool) : RegOutcome

OR a high-order 32-bit immediate into the top half of dst (eval_hor64). v2-only.

Equations

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

PQR (product / quotient / remainder)

def Solanalib.SBPF.pqrDivResult (sop : SndOp) (rs' : RegMap) (zero : Bool) : RegOutcome

A division/remainder guard: zero divisor faults as nok for an immediate operand (verifier should reject) and okn for a register operand.

Equations

• Solanalib.SBPF.pqrDivResult (Solanalib.SBPF.SndOp.imm i) rs' zero = if zero = true then Solanalib.SBPF.RegOutcome.nok else Solanalib.SBPF.RegOutcome.oks rs'
• Solanalib.SBPF.pqrDivResult (Solanalib.SBPF.SndOp.reg r) rs' zero = if zero = true then Solanalib.SBPF.RegOutcome.okn else Solanalib.SBPF.RegOutcome.oks rs'

def Solanalib.SBPF.evalPqr32 (pop : Pqrop) (dst : BpfIReg) (sop : SndOp) (rs : RegMap) (isV1 : Bool) : RegOutcome

32-bit PQR (eval_pqr32). v2-only.

Equations

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

def Solanalib.SBPF.evalPqr64 (pop : Pqrop) (dst : BpfIReg) (sop : SndOp) (rs : RegMap) (isV1 : Bool) : RegOutcome

64-bit PQR (eval_pqr64). v2-only.

Equations

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

def Solanalib.SBPF.evalPqr64_2 (pop : Pqrop2) (dst : BpfIReg) (sop : SndOp) (rs : RegMap) (isV1 : Bool) : RegOutcome

High-half multiply (eval_pqr64_2). v2-only.

The standard high-multiply semantics: widen both operands to 128 bits (zero- extend for uhmul, sign-extend for shmul), multiply, and take the high 64 bits. (Interpreter.thy's eval_pqr64_2 appears to mis-source its signed operand from dst; we implement the intended semantics and let differential testing against the reference VM adjudicate.)

Equations

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

Memory

def Solanalib.SBPF.evalStore (chk : MemoryChunk) (dst : BpfIReg) (sop : SndOp) (off : U16) (rs : RegMap) (m : Mem) : Option Mem

Store the second operand at dst + off (eval_store).

Equations

• Solanalib.SBPF.evalStore chk dst sop off rs m = Solanalib.SBPF.storev chk m (rs dst + BitVec.signExtend 64 off) (Solanalib.SBPF.memoryChunkValueOfU64 chk (Solanalib.SBPF.sndOp64 sop rs))

def Solanalib.SBPF.evalLoad (chk : MemoryChunk) (dst src : BpfIReg) (off : U16) (rs : RegMap) (m : Mem) : Option RegMap

Load from src + off into dst, zero-extending narrow loads (eval_load).

Equations

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

def Solanalib.SBPF.evalLoadImm (dst : BpfIReg) (imm1 imm2 : U32) (rs : RegMap) : RegMap

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

Equations

• Solanalib.SBPF.evalLoadImm dst imm1 imm2 rs = Solanalib.SBPF.setReg rs dst (BitVec.setWidth 64 imm1 &&& ↑4294967295 ||| BitVec.setWidth 64 imm2 <<< 32)

Jump

def Solanalib.SBPF.evalJmp (cond : Condition) (dst : BpfIReg) (sop : SndOp) (rs : RegMap) : Bool

Evaluate a branch condition (eval_jmp).

Equations

• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.eq dst sop rs = (rs dst == Solanalib.SBPF.sndOp64 sop rs)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.gt dst sop rs = BitVec.ult (Solanalib.SBPF.sndOp64 sop rs) (rs dst)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.ge dst sop rs = BitVec.ule (Solanalib.SBPF.sndOp64 sop rs) (rs dst)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.lt dst sop rs = BitVec.ult (rs dst) (Solanalib.SBPF.sndOp64 sop rs)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.le dst sop rs = BitVec.ule (rs dst) (Solanalib.SBPF.sndOp64 sop rs)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.sEt dst sop rs = (rs dst &&& Solanalib.SBPF.sndOp64 sop rs != 0)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.ne dst sop rs = (rs dst != Solanalib.SBPF.sndOp64 sop rs)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.sGt dst sop rs = BitVec.slt (Solanalib.SBPF.sndOp64 sop rs) (rs dst)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.sGe dst sop rs = BitVec.sle (Solanalib.SBPF.sndOp64 sop rs) (rs dst)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.sLt dst sop rs = BitVec.slt (rs dst) (Solanalib.SBPF.sndOp64 sop rs)
• Solanalib.SBPF.evalJmp Solanalib.SBPF.Condition.sLe dst sop rs = BitVec.sle (rs dst) (Solanalib.SBPF.sndOp64 sop rs)

Call / exit

def Solanalib.SBPF.pushFrame (rs : RegMap) (ss : StackState) (isV1 : Bool) (pc : U64) (gaps : Bool) : Option StackState × RegMap

Push a new call frame, saving BR6–BR9 and the frame pointer (push_frame). Returns none (with rs unchanged) when the call stack is full.

Equations

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

def Solanalib.SBPF.evalCallReg (src : BpfIReg) (imm : U32) (rs : RegMap) (ss : StackState) (isV1 : Bool) (pc : U64) (gaps : Bool) (programVmAddr : U64) : Option (U64 × RegMap × StackState)

Call the function whose address is in a register (eval_callReg).

Equations

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

def Solanalib.SBPF.evalCallImm (pc : U64) (src : BpfIReg) (imm : U32) (rs : RegMap) (ss : StackState) (isV1 : Bool) (fm : FuncMap) (gaps : Bool) : Option (U64 × RegMap × StackState)

Call the function identified by an immediate, via the registry when the source register is BR0 (eval_callImm).

Equations

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

def Solanalib.SBPF.popFrame (ss : StackState) : CallFrame

The frame to return into (pop_frame).

Equations

• Solanalib.SBPF.popFrame ss = ss.callFrames.getD (BitVec.toNat (ss.callDepth - 1)) Solanalib.SBPF.emptyFrame✝

def Solanalib.SBPF.evalExit (rs : RegMap) (ss : StackState) (isV1 : Bool) : U64 × RegMap × StackState

Return from the current frame, restoring saved registers (eval_exit).

Equations

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

Step

def Solanalib.SBPF.stepRegOutcome (o : RegOutcome) (pc : U64) (m : Mem) (ss : StackState) (sv : SBPFV) (fm : FuncMap) (curCu remainCu : U64) : BpfState

Lift an ALU-style RegOutcome into the post-state of a pc + 1 step.

Equations

• Solanalib.SBPF.stepRegOutcome Solanalib.SBPF.RegOutcome.nok pc m ss sv fm curCu remainCu = Solanalib.SBPF.BpfState.err
• Solanalib.SBPF.stepRegOutcome Solanalib.SBPF.RegOutcome.okn pc m ss sv fm curCu remainCu = Solanalib.SBPF.BpfState.eflag
• Solanalib.SBPF.stepRegOutcome (Solanalib.SBPF.RegOutcome.oks rs') pc m ss sv fm curCu remainCu = Solanalib.SBPF.BpfState.ok (pc + 1) rs' m ss sv fm (curCu + 1) remainCu

def Solanalib.SBPF.step (pc : U64) (ins : BpfInstruction) (rs : RegMap) (m : Mem) (ss : StackState) (sv : SBPFV) (fm : FuncMap) (gaps : Bool) (programVmAddr curCu remainCu : U64) : BpfState

Execute a single instruction (step).

Equations

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

def Solanalib.SBPF.bpfInterp : Nat → BpfBin → BpfState → Bool → U64 → BpfState

Run the program under a fuel bound (bpf_interp). Each step is gated on PC being in range and fuel remaining; exhaustion or an out-of-range PC yields a fault.

Equations

• One or more equations did not get rendered due to their size.
• Solanalib.SBPF.bpfInterp 0 x✝³ x✝² x✝¹ x✝ = Solanalib.SBPF.BpfState.eflag
• Solanalib.SBPF.bpfInterp n.succ x✝² Solanalib.SBPF.BpfState.eflag x✝¹ x✝ = Solanalib.SBPF.BpfState.eflag
• Solanalib.SBPF.bpfInterp n.succ x✝² Solanalib.SBPF.BpfState.err x✝¹ x✝ = Solanalib.SBPF.BpfState.err
• Solanalib.SBPF.bpfInterp n.succ x✝² (Solanalib.SBPF.BpfState.success v) x✝¹ x✝ = Solanalib.SBPF.BpfState.success v