Documentation

Solanalib.SBPF.Value

SBPF.Value — the CompCert-style memory value #

The value type read from and written to memory (Val.thy's val). A memory access at a given MemoryChunk width yields one of these tagged values.

Scope note: Val.thy additionally defines a large suite of CompCert-style arithmetic on val (add32, divmod64s, bswap32, cmpu, …). Those operate on the x86-64 JIT's value-typed registers and are out of scope here — the sBPF interpreter operates on raw U64 registers directly. Only the value type, which the memory model needs, is ported.

Main definitions #

source
inductive Solanalib.SBPF.Val :
Type

A CompCert-style memory value: either undefined or a tagged machine word.

Instances For
    source
    @[implicit_reducible]
    instance Solanalib.SBPF.instDecidableEqVal :
    DecidableEq Val
    Equations
    source
    def Solanalib.SBPF.instDecidableEqVal.decEq (x✝ x✝¹ : Val) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      def Solanalib.SBPF.instReprVal.repr :
      Val → Nat → Std.Format
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Solanalib.SBPF.instReprVal :
        Repr Val
        Equations