verifier

verifier. Use when you need help with verifier.

SKILL.md

GitHub

Verifier Guide

Use this file for verifier failures, pointer-class reasoning, and constraint-aware program design.

When to Use This File

  • verifier rejects the program
  • the user shares a verifier log
  • loops, stack usage, packet parsing, or map value access are failing
  • the user asks how to write code that the verifier will accept

Verifier Working Style

When a verifier error appears:

  1. Identify the failing pointer class:
    • packet pointer
    • map value pointer
    • stack pointer
    • nullable helper result
    • context-derived pointer
  2. Reduce to the smallest bad path.
  3. Add the missing proof the verifier needs.
  4. Re-run with logs and inspect the exact failing register state.

Do not answer with generic folklore if the user provided a real verifier log. Explain the failing path in that log.

Common Error Patterns

Error Usual Cause Default Fix
invalid indirect read from stack uninitialized stack passed to helper zero-init local buffers
R0 invalid mem access 'scalar' nullable result used unchecked add if (!ptr) return ...
math between pkt pointer and unbounded register packet offset not proven safe bounds-check against data_end
back-edge from insn X to Y unverifiable loop unroll or use bounded loop with constant limit
register R1 type=map_value expected=fp wrong helper argument shape use the helper's expected pointer type and stage through locals
invalid stack type stack escape the verifier cannot model simplify locals and pass stable stack addresses only
too many instructions oversized program split with tail calls or subprograms

Proofs the Verifier Usually Needs

Packet Access

Every dereference needs a prior bound:

void *data = (void *)(long)ctx->data;
void *data_end = (void *)(long)ctx->data_end;
struct ethhdr *eth = data;

if ((void *)(eth + 1) > data_end)
    return XDP_DROP;

Nullable Map Lookups

u64 *val = bpf_map_lookup_elem(&my_map, &key);
if (!val)
    return 0;

__sync_fetch_and_add(val, 1);

Stack Initialization

char buf[64] = {};
bpf_get_current_comm(buf, sizeof(buf));

Bounded Loops

#pragma unroll
for (int i = 0; i < 4; i++) {
    // ...
}

Or, on newer kernels:

static long cb(u32 i, void *ctx) {
    return 0;
}

bpf_loop(128, cb, NULL, 0);

Design Rules That Avoid Verifier Pain

  • keep helpers close to the proof that justifies their arguments
  • use local temporaries when helper argument shapes are subtle
  • make bounds and NULL checks happen before branching complexity explodes
  • keep loops obviously bounded
  • prefer simpler control flow during early bring-up
  • compile with -g so source lines appear in logs

Minimal Verifier Debug Flow

mount -t bpf bpffs /sys/fs/bpf
bpftool prog load prog.bpf.o /sys/fs/bpf/test
export LIBBPF_LOG_LEVEL=debug

If the user has a libbpf log, explain:

  • which instruction failed
  • what the register type was at that point
  • what proof was missing
  • the smallest code change likely to satisfy the verifier

Related Features

  • bpf_loop reduces the need for manual unrolling on newer kernels
  • tail calls help with instruction-limit pressure
  • per-CPU maps often simplify shared-state proofs
  • object storage maps can be easier to reason about than pointer-keyed hash tables