Formal verification of translation validators: a case study on instruction scheduling optimizations