Just take the obvious approach already

Dynamically tracking which resources need to be released is only a performance issue. Lots of things affect performance, e.g. the JIT. Therefore it doesn't make sense to impose "no dynamic tracking" as a hard design requirement.

> BPF, on the other hand, essentially makes anything the verifier can't understand the programmer's problem.

This is a nightmare. Other comparable systems (CIL, JVM, WASM) carefully define what bytecode programs are valid and pretty much never change them (maybe relaxing a bit here and there), but valid bytecode is rich enough for compilers to compile any valid source program so users don't have to care.

I hope the BPF community eventually figures this out, but they're accumulating a horrendous amount of baggage in the meantime.