let prefetch_elim_ph = {
  ph = (function
      | [Instr i oprs (AnnotatePrefetchnta ())] ->
        Some []
      | _ -> None);
  input_hint = 1;
}
let prefetch_elim_ph =
{
  ph
  =
  (function
    | [Instr i oprs (AnnotatePrefetchnta ())] -> Some []
    | _ -> None);
  input_hint = 1
}
Vale.Transformers.PrefetchElim.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.Bytes_Code_s.fst.checked Vale.Transformers.PeepHole.fsti.checked Vale.Transformers.InstructionReorder.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Vale.Transformers.PrefetchElim.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 FStar.Pervasives.Native.Some Prims.Nil FStar.Pervasives.Native.None FStar.Pervasives.Native.option
module Vale.Transformers.PrefetchElim

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 prefetch_elim_ph : Vale.Transformers.PeepHole.pre_peephole
Vale.Transformers.PeepHole.pre_peephole