Documentation

Solanalib.SBPF.Decoder

SBPF.Decoder — sBPF bytecode decoding #

Decoding of binary sBPF into the abstract BpfInstruction syntax, ported from rBPFDecoder.thy. decode maps a single opcode + operand fields to an instruction; findInstr slices the 8- (or 16-) byte instruction out of a byte list at a given program counter and decodes it.

Main definitions #

source
def Solanalib.SBPF.insnSize :
Nat

The size of an encoded instruction slot, in bytes.

Equations
Instances For
    source
    def Solanalib.SBPF.decode (opc : U8) (dv sv : U4) (off : U16) (imm : U32) :
    Option BpfInstruction

    Decode a single sBPF instruction from its opcode and operand fields (rbpf_decoder). Both register fields must name a valid register (0–10), except the 0x07 stack-pointer form which uses the sentinel destination 11.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Solanalib.SBPF.findInstr (pc : Nat) (l : BpfBin) :
      Option BpfInstruction

      Locate and decode the instruction at program counter pc in byte list l (bpf_find_instr). Handles the 16-byte 0x18 load-immediate form.

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