We're talking about eBPF programs here. Those halt by design as you cannot loop (jump backwards) and have a limited number of instructions you can use per progr

We're talking about eBPF programs here. Those halt by design as you cannot loop (jump backwards) and have a limited number of instructions you can use per program. So the halting problem isn't really and issue here in this particular case. You can just run the original and rewritten code in an eBPF VM with mock inputs and compare.