I don’t see how you would even start to prove this in ZK in an efficient manner.
When proving something with dynamic size, you need to prove all code paths, all sizes.
Here, everything is dynamic and as gas cost increases, you would have an exponential amount of possible states to prove.
This looks also like quite tricky to get right, test and fuzz and looks like very bug prone. In regular programming, manipulating the stack is very tricky to get right, see discussions around longjmp and setjmp.
In general, opcodes that are non-deterministic are avoided in the EVM, which is why there are proposal such as EIP-3690: EOF - JUMPDEST Table (EIP-3690: EOF - JUMPDEST Table) to ease execution analysis. This precompile goes in the complete opposite direction.
Finally all the other precompiled contracts are pure functions, with very well understood results. This one looks like even more complex than feu SELFDESTRUCT.