[$] Verifying the BPF verifier's path-exploration logic

Srinivas Narayana led a remote session about extendingAgni to prove the correctness ofthe BPF verifier's handling of different execution paths as part of the Linux Storage,Filesystem, Memory Management, and BPF Summit. The problem of ensuring thecorrectness of path explorationis much more difficult than the problem ofensuring the correctness of arithmetic operations(which wasthe subject of the previous session), however. Narayana's plan totackle the problem makes use of a mixture of specialized techniques - and mayneed some assistance from the BPF developers to make it feasible at all.