Well, you could embed a machine-checked proof that instruction sequences of the targeted form will sometimes survive previous optimization passes and therefore

Well, you could embed a machine-checked proof that instruction sequences of the targeted form will sometimes survive previous optimization passes and therefore the given optimization will always be contributing something. But that's hard, so every compiler I've used leaves it to human engineering instead.