Proposal:

1. Assume a series of BPF instructions have been parsed, a control flow graph has been created along with a set of pre and post conditions.
2. Assume that the BPF instructions are being executed one at a time.
3. Prior to executing any BPF instruction the concrete state of the VM should be entailed by the abstract state of the CFG at that label.
4. If the concrete state violated the pre-conditions, then either the pre-conditions or the implementation of the BPF VM are wrong.

Notes from discussion with @dthaler

something like this:
ebpf_domain_t from_inv(pre_invariants.at(label));
to get the expected set of pre-invariants
 
then create a crab::linear_constraint_t that checks register Y against value Z
 
then do
if (inv.intersect(cst)) to check it
 
where cst is the linear constraint