SBPF.Memory — the sBPF memory model #

Byte-addressable memory, access widths, and the load / store operations of the sBPF semantics, ported from Mem.thy. Memory is a partial map from 64-bit address to byte; loads and stores are little-endian and operate at one of four access widths.

Main definitions #

Solanalib.SBPF.MemoryChunk — access width (m8 … m64).
Solanalib.SBPF.Mem — the byte-addressable address space.
Solanalib.SBPF.loadv — read a Val of a given width (none if unmapped).
Solanalib.SBPF.storev — write a Val, returning the updated memory.

source

inductive Solanalib.SBPF.MemoryChunk :

Type

Access width for a memory operation (the source theory's memory_chunk).

Instances For

source

@[implicit_reducible]

instance Solanalib.SBPF.instDecidableEqMemoryChunk :

DecidableEq MemoryChunk

Equations

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

source

def Solanalib.SBPF.instReprMemoryChunk.repr :

MemoryChunk → Nat → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance Solanalib.SBPF.instReprMemoryChunk :

Repr MemoryChunk

Equations

Solanalib.SBPF.instReprMemoryChunk = { reprPrec := Solanalib.SBPF.instReprMemoryChunk.repr }

source

@[reducible, inline]

abbrev Solanalib.SBPF.Mem :

Type

Byte-addressable memory: a partial map from 64-bit address to byte.

Modelled as a total function into Option U8 (none = unmapped), matching the source theory's (u64, u8) map.

Equations

Solanalib.SBPF.Mem = (Solanalib.SBPF.U64 → Option Solanalib.SBPF.U8)

Instances For

source

def Solanalib.SBPF.initMem :

Mem

The empty address space — every byte unmapped.

Equations

Solanalib.SBPF.initMem x✝ = none

Instances For

source

def Solanalib.SBPF.vlongOfMemoryChunk :

MemoryChunk → Val

The width of a chunk, as a 64-bit value (vlong_of_memory_chunk).

Equations

Instances For

source

def Solanalib.SBPF.memoryChunkValueOfU64 (mc : MemoryChunk) (v : U64) :

Val

Tag a 64-bit word as the value of the given access width, truncating to the width (memory_chunk_value_of_u64).

Equations

Instances For

source

def Solanalib.SBPF.loadv (mc : MemoryChunk) (m : Mem) (addr : U64) :

Option Val

Read a value of the given width at addr, little-endian. Yields none if any byte in the accessed range is unmapped.

Equations

One or more equations did not get rendered due to their size.
Solanalib.SBPF.loadv Solanalib.SBPF.MemoryChunk.m8 m addr = Option.map (fun (b0 : Solanalib.SBPF.U8) => Solanalib.SBPF.Val.vbyte b0) (m addr)
Solanalib.SBPF.loadv Solanalib.SBPF.MemoryChunk.m16 m addr = do let b0 ← m addr let b1 ← m (addr + 1) pure (Solanalib.SBPF.Val.vshort (BitVec.setWidth 16 b0 ||| BitVec.setWidth 16 b1 <<< 8))

Instances For

source

def Solanalib.SBPF.storev (mc : MemoryChunk) (m : Mem) (addr : U64) (v : Val) :

Option Mem

Write a value of the given width at addr, little-endian. Yields none if the value's tag does not match the access width.

Equations

One or more equations did not get rendered due to their size.
Solanalib.SBPF.storev Solanalib.SBPF.MemoryChunk.m8 m addr (Solanalib.SBPF.Val.vbyte n) = some fun (i : Solanalib.SBPF.U64) => if i = addr then some n else m i
Solanalib.SBPF.storev mc m addr v = none

Instances For