let movbe_elim_ph = {
  ph = (function
      | [Instr i oprs (AnnotateMovbe64 proof_of_movbe)] ->
        let oprs:normal (instr_operands_t [out op64] [op64]) =
          coerce_to_normal #(instr_operands_t [out op64] [op64]) oprs in
        let (dst, (src, ())) = oprs in
        if OReg? dst then (
          let mov = make_instr ins_Mov64 dst src in
          let bswap = make_instr ins_Bswap64 dst in
          Some [mov; bswap]
        ) else None
      | _ -> None);
  input_hint = 1;
}
let movbe_elim_ph =
{
  ph
  =
  (function
    | [Instr i oprs (AnnotateMovbe64 proof_of_movbe)] ->
      let oprs:normal (instr_operands_t [out op64] [op64]) =
        coerce_to_normal #(instr_operands_t [out op64] [op64]) oprs
      in
      let dst, (src, ()) = oprs in
      if OReg? dst
      then
        (let mov = make_instr ins_Mov64 dst src in
          let bswap = make_instr ins_Bswap64 dst in
          Some [mov; bswap])
      else None
    | _ -> None);
  input_hint = 1
}
Vale.Transformers.MovbeElim.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Transformers.PeepHole.fsti.checked Vale.Transformers.InstructionReorder.fst.checked Vale.Def.Types_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Vale.Transformers.MovbeElim.fst
Vale.Transformers.PeepHole.Mkpre_peephole Prims.list Vale.X64.Machine_Semantics_s.ins Vale.X64.Instruction_s.instr_t_record Vale.X64.Instruction_s.instr_operands_t Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__outs Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__args Vale.X64.Machine_Semantics_s.equals_instr Vale.X64.Instruction_s.InstrTypeRecord Prims.Cons Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.out Vale.X64.Instruction_s.op64 Prims.Nil Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.PreserveFlags Vale.X64.Instructions_s.ins_MovBe64 Vale.X64.Machine_s.operand64 Vale.X64.Machine_s.uu___is_OReg Vale.X64.Machine_s.nat64 Vale.X64.Machine_s.reg_64 FStar.Pervasives.Native.Some Vale.X64.InsLemmas.make_instr_t Vale.X64.InsLemmas.make_instr Vale.X64.Instruction_s.inOut Vale.X64.Instructions_s.ins_Bswap64 Vale.X64.InsLemmas.make_instr_t_args Vale.X64.Instructions_s.ins_Mov64 Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option FStar.Pervasives.norm FStar.Pervasives.norm_step FStar.Pervasives.zeta FStar.Pervasives.iota FStar.Pervasives.delta_attr Prims.string FStar.Pervasives.Native.Mktuple2 Vale.X64.Instruction_s.instr_operand_inout Vale.X64.Instruction_s.Out Vale.X64.Instruction_s.IOpEx Vale.X64.Instruction_s.IOp64 Vale.Transformers.PeepHole.coerce_to_normal
module Vale.Transformers.MovbeElim

open Vale.X64.Bytes_Code_s
open Vale.X64.Instruction_s
open Vale.X64.Instructions_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.X64.Print_s
open Vale.Transformers.InstructionReorder
open Vale.X64.InsLemmas

open Vale.Transformers.PeepHole
val movbe_elim_ph : Vale.Transformers.PeepHole.pre_peephole
Vale.Transformers.PeepHole.pre_peephole