val prefetch_elim_correct (is: list ins) (s: machine_state)
    : Lemma (peephole_correct prefetch_elim_ph is s)
      [SMTPat (peephole_correct prefetch_elim_ph is s)]
let prefetch_elim_correct (is:list ins) (s:machine_state) :
  Lemma (peephole_correct prefetch_elim_ph is s)
    [SMTPat (peephole_correct prefetch_elim_ph is s)] =
  match is with
  | [Instr i oprs (AnnotatePrefetchnta ())] -> ()
  | _ -> ()
val prefetch_elim_correct (is: list ins) (s: machine_state)
    : Lemma (peephole_correct prefetch_elim_ph is s)
      [SMTPat (peephole_correct prefetch_elim_ph is s)]
let prefetch_elim_correct (is: list ins) (s: machine_state)
    : Lemma (peephole_correct prefetch_elim_ph is s)
      [SMTPat (peephole_correct prefetch_elim_ph is s)] =
match is with
| [Instr i oprs (AnnotatePrefetchnta ())] -> ()
| _ -> ()
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
Prims.list Vale.X64.Machine_Semantics_s.ins Vale.X64.Machine_Semantics_s.machine_state 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 Prims.unit Prims.l_True Prims.squash Vale.Transformers.PeepHole.peephole_correct Vale.Transformers.PrefetchElim.prefetch_elim_ph Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
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

let prefetch_elim_ph = {
  ph = (function
      | [Instr i oprs (AnnotatePrefetchnta ())] ->
        Some []
      | _ -> None);
  input_hint = 1;
}

#push-options "--fuel 2 --ifuel 3"
let prefetch_elim_correct (is:list ins) (s:machine_state) :
  Lemma (peephole_correct prefetch_elim_ph is s)
val prefetch_elim_correct (is: list ins) (s: machine_state)
    : Lemma (peephole_correct prefetch_elim_ph is s)
      [SMTPat (peephole_correct prefetch_elim_ph is s)]
is: Prims.list Vale.X64.Machine_Semantics_s.ins -> s: Vale.X64.Machine_Semantics_s.machine_state
  -> FStar.Pervasives.Lemma
      (ensures
        Vale.Transformers.PeepHole.peephole_correct Vale.Transformers.PrefetchElim.prefetch_elim_ph
          is
          s)
      [
        SMTPat (Vale.Transformers.PeepHole.peephole_correct Vale.Transformers.PrefetchElim.prefetch_elim_ph
              is
              s)
      ]