Range refinement after conditional branches

This week we landed range refinement after conditional branches in the verifier (PR #101). The short version: when control flow forks on a comparison like r1 < 256, the true branch should know r1 ∈ [0, 255] and the false branch should know r1 ∈ [256, u64::MAX]. Before this change, both branches inherited the parent’s range and a lot of safe code was rejected.

Why this matters

Many real eBPF programs look like:

if (event->line < NUM_GPIO) {
    metrics[event->line]++;   // index now provably in-bounds
}

Without refinement, the verifier sees the array access in the true branch with the original range of event->line — which may not be tight enough to prove the index is safe. With refinement, the comparison itself becomes a fact the abstract state carries forward.

What we changed

Two pieces:

1. Branch-aware state propagation in the CFG walker — each outgoing edge of a conditional carries a state with the relevant register refined.
2. A small lattice of comparisons — lt, le, gt, ge, eq, ne — each with rules for both the true and false continuations, in both signed and unsigned interpretations.

The trickiest part was the interaction with our existing tnum tracking. A tnum says “these bits are known and these are unknown”; a range says “the value lives between min and max”. After refinement, both must agree, and the simplest way to enforce that is to recompute tnum from the refined range and vice versa until both stop changing. We capped this at one iteration; in practice the fixpoint converges immediately.

What we got back

The internal fuzz harness (#97) now finds zero false positives in a corpus of ~12 000 generated programs that exercise array indexing patterns. Verification time is unchanged within noise.

Next: per-instruction liveness has landed (PR #100); state pruning scaffolding is in place (PR #99). Both should compose to keep the verifier cheap as we add more domains.