Re: [PATCH RFC] bpf: add DAG fast-path in verifier to skip redundant state pruning

[Seunghyeon Lee <hyeon3125@gmail.com>]

Alexei,

Agreed — DAG-only is the narrow case. The general case is the right direction.

On merge_verifier_state():
I've been looking at this from two angles:

Transfer-function approach (your direction): merge_verifier_state() as
the join operator in a dataflow lattice. The key question: what's the
minimal state representation that preserves safety without full state
enumeration?

Proof-carrying approach (longer-term): If a compiler can prove properties
about the transfer function before loading, the verifier only needs to
check the proof, not simulate the lattice. This is essentially PCC
(Necula 1997) applied to BPF.

These two converge at merge_verifier_state(): the join operator defines
the abstract domain. If the domain is finite and the transfer functions
are monotone, you get termination for free — proof becomes a byproduct.

Looking forward to seeing your prototype. What representation are you
using for the abstract state?

- Seunghyeon