SBPF.State — interpreter state

The machine state of the sBPF interpreter, ported from vm_state.thy, vm.thy, ebpf.thy, and the state section of Interpreter.thy. This module defines the register file, the call-frame stack, the function registry, the small-step result type, the VM constants, and the initial state.

Main definitions

• Solanalib.SBPF.RegMap — the eleven 64-bit registers as a function.
• Solanalib.SBPF.StackState — the call-frame stack.
• Solanalib.SBPF.BpfState — the small-step result (ok / success / eflag / err).
• Solanalib.SBPF.RegOutcome — an ALU step result (oks / okn / nok).

VM constants

def Solanalib.SBPF.scratchRegs : Nat

Number of scratch (caller-saved) registers, BR6–BR9.

Equations

• Solanalib.SBPF.scratchRegs = 4

def Solanalib.SBPF.mmStackStart : U64

Base virtual address of the VM stack region.

Equations

• Solanalib.SBPF.mmStackStart = 8589934592

def Solanalib.SBPF.mmInputStart : U64

Base virtual address of the program input region.

Equations

• Solanalib.SBPF.mmInputStart = 17179869184

def Solanalib.SBPF.maxCallDepth : U64

Maximum nested call depth.

Equations

• Solanalib.SBPF.maxCallDepth = 64

def Solanalib.SBPF.stackFrameSize : U64

Size of a single stack frame, in bytes.

Equations

• Solanalib.SBPF.stackFrameSize = 4096

Registers

@[reducible, inline]

abbrev Solanalib.SBPF.RegMap : Type

The register file: each of the eleven registers holds a 64-bit word.

Equations

• Solanalib.SBPF.RegMap = (Solanalib.SBPF.BpfIReg → Solanalib.SBPF.U64)

def Solanalib.SBPF.evalReg (dst : BpfIReg) (rs : RegMap) : U64

Read a register (eval_reg).

Equations

• Solanalib.SBPF.evalReg dst rs = rs dst

def Solanalib.SBPF.setReg (rs : RegMap) (r : BpfIReg) (v : U64) : RegMap

Functional register update: rs with r set to v.

Equations

• Solanalib.SBPF.setReg rs r v r' = if r' = r then v else rs r'

def Solanalib.SBPF.initRegMap : RegMap

The all-zero register file (init_reg_map).

Equations

• Solanalib.SBPF.initRegMap x✝ = 0

Call frames and the stack

structure Solanalib.SBPF.CallFrame : Type

A saved call frame: the caller's scratch registers, frame pointer, and the program counter to return to (vm_state.thy's CallFrame).

• callerSavedRegisters : List U64

  The caller-saved registers BR6–BR9, in order.

• framePointer : U64

  The caller's frame pointer (BR10).

• targetPc : U64

  The program counter to resume at on return.

theorem Solanalib.SBPF.CallFrame.ext_iff {x y : CallFrame} : x = y ↔ x.callerSavedRegisters = y.callerSavedRegisters ∧ x.framePointer = y.framePointer ∧ x.targetPc = y.targetPc

theorem Solanalib.SBPF.CallFrame.ext {x y : CallFrame} (callerSavedRegisters : x.callerSavedRegisters = y.callerSavedRegisters) (framePointer : x.framePointer = y.framePointer) (targetPc : x.targetPc = y.targetPc) : x = y

@[implicit_reducible]

instance Solanalib.SBPF.instReprCallFrame : Repr CallFrame

Equations

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

def Solanalib.SBPF.instReprCallFrame.repr : CallFrame → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqCallFrame : DecidableEq CallFrame

Equations

• Solanalib.SBPF.instDecidableEqCallFrame = Solanalib.SBPF.instDecidableEqCallFrame.decEq

def Solanalib.SBPF.instDecidableEqCallFrame.decEq (x✝ x✝¹ : CallFrame) : Decidable (x✝ = x✝¹)

Equations

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

structure Solanalib.SBPF.StackState : Type

The call-frame stack: current depth, stack pointer, and saved frames.

• callDepth : U64

  The current nesting depth of function calls.

• stackPointer : U64

  The current stack pointer.

• callFrames : List CallFrame

  The saved call frames, innermost last.

theorem Solanalib.SBPF.StackState.ext_iff {x y : StackState} : x = y ↔ x.callDepth = y.callDepth ∧ x.stackPointer = y.stackPointer ∧ x.callFrames = y.callFrames

theorem Solanalib.SBPF.StackState.ext {x y : StackState} (callDepth : x.callDepth = y.callDepth) (stackPointer : x.stackPointer = y.stackPointer) (callFrames : x.callFrames = y.callFrames) : x = y

def Solanalib.SBPF.instReprStackState.repr : StackState → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Solanalib.SBPF.instReprStackState : Repr StackState

Equations

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

def Solanalib.SBPF.instDecidableEqStackState.decEq (x✝ x✝¹ : StackState) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqStackState : DecidableEq StackState

Equations

• Solanalib.SBPF.instDecidableEqStackState = Solanalib.SBPF.instDecidableEqStackState.decEq

def Solanalib.SBPF.initStackState : StackState

The initial stack: depth 0, stack pointer at the top of the region, and maxCallDepth default frames preallocated (init_stack_state).

Equations

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

Function registry

@[reducible, inline]

abbrev Solanalib.SBPF.FuncMap : Type

The function registry: a partial map from a 32-bit key to a target address (ebpf.thy's func_map).

Equations

• Solanalib.SBPF.FuncMap = (Solanalib.SBPF.U32 → Option Solanalib.SBPF.U64)

def Solanalib.SBPF.initFuncMap : FuncMap

The empty function registry (init_func_map).

Equations

• Solanalib.SBPF.initFuncMap x✝ = none

def Solanalib.SBPF.getFunctionRegistry (key : U32) (fm : FuncMap) : Option U64

Look up a function address by key (get_function_registry).

Equations

• Solanalib.SBPF.getFunctionRegistry key fm = fm key

Step results

inductive Solanalib.SBPF.BpfState : Type

The small-step result (bpf_state).

• ok pc rs m ss sv fm curCu remainCu — a normal post-state.
• success v — the program returned v.
• eflag — a runtime fault (out-of-bounds, fuel exhaustion, …).
• err — a malformed instruction the verifier should have rejected.

• ok (pc : U64) (rs : RegMap) (m : Mem) (ss : StackState) (sv : SBPFV) (fm : FuncMap) (curCu remainCu : U64) : BpfState
• success (v : U64) : BpfState
• eflag : BpfState
• err : BpfState

inductive Solanalib.SBPF.RegOutcome : Type

The result of an ALU-style evaluation ('a option2, specialised to the register file): oks carries the updated registers, okn signals a runtime fault (EFlag), nok a malformed instruction (Err).

• nok : RegOutcome
• okn : RegOutcome
• oks (rs : RegMap) : RegOutcome

def Solanalib.SBPF.initBpfState (rs : RegMap) (m : Mem) (n : U64) (v : SBPFV) : BpfState

The initial machine state: PC 0, BR10 pointing at the top of the stack, memory m, version v, empty registry, and n units of fuel (init_bpf_state).

Equations

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