Comment by Scea91

> your specification is simply "an optimized program always behaves the same as the original"

I wouldn't say it is simple, since it is undecidable for general programs.