val lemma_movbe_is_mov_bswap (dst src: operand64) (s: machine_state)
    : Lemma (requires (OReg? dst))
      (ensures
        (let movbe = make_instr_annotate ins_MovBe64 (AnnotateMovbe64 ()) dst src in
          let mov = make_instr ins_Mov64 dst src in
          let bswap = make_instr ins_Bswap64 dst in
          let s1 = machine_eval_ins movbe s in
          let s2 = machine_eval_ins bswap (machine_eval_ins mov s) in
          s1.ms_ok ==> equiv_states s1 s2))
let lemma_movbe_is_mov_bswap (dst src:operand64) (s:machine_state) :
  Lemma
    (requires (OReg? dst))
    (ensures (
        let movbe = make_instr_annotate ins_MovBe64 (AnnotateMovbe64 ()) dst src in
        let mov = make_instr ins_Mov64 dst src in
        let bswap = make_instr ins_Bswap64 dst in
        let s1 = machine_eval_ins movbe s in
        let s2 = machine_eval_ins bswap (machine_eval_ins mov s) in
        s1.ms_ok ==> equiv_states s1 s2)) =
  let movbe = make_instr_annotate ins_MovBe64 (AnnotateMovbe64 ()) dst src in
  let mov = make_instr ins_Mov64 dst src in
  let bswap = make_instr ins_Bswap64 dst in
  let s_movbe = machine_eval_ins movbe s in
  let s_mov = machine_eval_ins mov s in
  let s_bswap = machine_eval_ins bswap s_mov in
  if valid_src_operand64_and_taint src s && valid_dst_operand64 dst s then (
    let src_v = eval_operand src s in
    let dst_movbe_v = T.reverse_bytes_nat64 src_v in
    let dst_mov_v = eval_operand dst s_mov in
    let dst_bswap_v = T.reverse_bytes_nat64 dst_mov_v in
    if s_movbe.ms_ok then (
      assert (Vale.X64.CPU_Features_s.movbe_enabled);
      assert (s_movbe == update_operand64_preserve_flags'' dst dst_movbe_v s s);
      assert (s_mov == update_operand64_preserve_flags'' dst src_v s s);
      lemma_update_to_valid_destination_keeps_it_as_valid_src dst s src_v;
      assert (eval_operand dst s_mov == src_v);
      assert (valid_src_operand64_and_taint dst s_mov);
      assert (s_bswap == update_operand64_preserve_flags'' dst dst_bswap_v s_mov s_mov);
      assert (src_v == dst_mov_v);
      assert (dst_movbe_v == dst_bswap_v);
      lemma_double_update_reg dst s s_mov s_bswap s_movbe src_v dst_bswap_v
    ) else ()
  ) else (
    assert (s_movbe == {s with ms_ok = false});
    assert (s_mov == {s with ms_ok = false});
    assert (s_bswap.ms_ok == false)
  )
val lemma_movbe_is_mov_bswap (dst src: operand64) (s: machine_state)
    : Lemma (requires (OReg? dst))
      (ensures
        (let movbe = make_instr_annotate ins_MovBe64 (AnnotateMovbe64 ()) dst src in
          let mov = make_instr ins_Mov64 dst src in
          let bswap = make_instr ins_Bswap64 dst in
          let s1 = machine_eval_ins movbe s in
          let s2 = machine_eval_ins bswap (machine_eval_ins mov s) in
          s1.ms_ok ==> equiv_states s1 s2))
let lemma_movbe_is_mov_bswap (dst src: operand64) (s: machine_state)
    : Lemma (requires (OReg? dst))
      (ensures
        (let movbe = make_instr_annotate ins_MovBe64 (AnnotateMovbe64 ()) dst src in
          let mov = make_instr ins_Mov64 dst src in
          let bswap = make_instr ins_Bswap64 dst in
          let s1 = machine_eval_ins movbe s in
          let s2 = machine_eval_ins bswap (machine_eval_ins mov s) in
          s1.ms_ok ==> equiv_states s1 s2)) =
let movbe = make_instr_annotate ins_MovBe64 (AnnotateMovbe64 ()) dst src in
let mov = make_instr ins_Mov64 dst src in
let bswap = make_instr ins_Bswap64 dst in
let s_movbe = machine_eval_ins movbe s in
let s_mov = machine_eval_ins mov s in
let s_bswap = machine_eval_ins bswap s_mov in
if valid_src_operand64_and_taint src s && valid_dst_operand64 dst s
then
  (let src_v = eval_operand src s in
    let dst_movbe_v = T.reverse_bytes_nat64 src_v in
    let dst_mov_v = eval_operand dst s_mov in
    let dst_bswap_v = T.reverse_bytes_nat64 dst_mov_v in
    if s_movbe.ms_ok
    then
      (assert (Vale.X64.CPU_Features_s.movbe_enabled);
        assert (s_movbe == update_operand64_preserve_flags'' dst dst_movbe_v s s);
        assert (s_mov == update_operand64_preserve_flags'' dst src_v s s);
        lemma_update_to_valid_destination_keeps_it_as_valid_src dst s src_v;
        assert (eval_operand dst s_mov == src_v);
        assert (valid_src_operand64_and_taint dst s_mov);
        assert (s_bswap == update_operand64_preserve_flags'' dst dst_bswap_v s_mov s_mov);
        assert (src_v == dst_mov_v);
        assert (dst_movbe_v == dst_bswap_v);
        lemma_double_update_reg dst s s_mov s_bswap s_movbe src_v dst_bswap_v))
else
  (assert (s_movbe == { s with ms_ok = false });
    assert (s_mov == { s with ms_ok = false });
    assert (s_bswap.ms_ok == false))
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.X64.Machine_s.operand64 Vale.X64.Machine_Semantics_s.machine_state Prims.op_AmpAmp Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint Vale.X64.Machine_Semantics_s.valid_dst_operand64 Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok Vale.Transformers.PeepHole.lemma_double_update_reg Prims.unit Prims._assert Prims.eq2 Vale.Def.Types_s.nat64 Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags'' Prims.b2t Vale.X64.Machine_Semantics_s.eval_operand Vale.Transformers.PeepHole.lemma_update_to_valid_destination_keeps_it_as_valid_src Vale.X64.CPU_Features_s.movbe_enabled Prims.bool Vale.Def.Words_s.nat64 Vale.Def.Types_s.reverse_bytes_nat64 Vale.X64.Machine_Semantics_s.Mkmachine_state Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace Vale.X64.Machine_Semantics_s.machine_eval_ins Vale.X64.InsLemmas.make_instr_t Prims.Nil Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.instr_operand Vale.X64.InsLemmas.make_instr Prims.Cons Vale.X64.Instruction_s.inOut Vale.X64.Instruction_s.op64 Vale.X64.Instruction_s.PreserveFlags Vale.X64.Instructions_s.ins_Bswap64 Vale.X64.InsLemmas.make_instr_t_args Vale.X64.Instruction_s.out Vale.X64.Instructions_s.ins_Mov64 Vale.X64.InsLemmas.make_instr_annotate Vale.X64.Instructions_s.ins_MovBe64 Vale.X64.Machine_Semantics_s.AnnotateMovbe64 Vale.X64.Instruction_s.InstrTypeRecord Vale.X64.Machine_s.uu___is_OReg Vale.X64.Machine_s.nat64 Vale.X64.Machine_s.reg_64 Prims.squash Prims.l_imp Vale.Transformers.InstructionReorder.equiv_states FStar.Pervasives.pattern
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

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;
}

module T = Vale.Def.Types_s
module H = Vale.Arch.Heap

#push-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 0 --max_ifuel 0"
let lemma_movbe_is_mov_bswap (dst src:operand64) (s:machine_state) :
  Lemma
    (requires (OReg? dst))
    (ensures (
        let movbe = make_instr_annotate ins_MovBe64 (AnnotateMovbe64 ()) dst src in
        let mov = make_instr ins_Mov64 dst src in
        let bswap = make_instr ins_Bswap64 dst in
        let s1 = machine_eval_ins movbe s in
val lemma_movbe_is_mov_bswap (dst src: operand64) (s: machine_state)
    : Lemma (requires (OReg? dst))
      (ensures
        (let movbe = make_instr_annotate ins_MovBe64 (AnnotateMovbe64 ()) dst src in
          let mov = make_instr ins_Mov64 dst src in
          let bswap = make_instr ins_Bswap64 dst in
          let s1 = machine_eval_ins movbe s in
          let s2 = machine_eval_ins bswap (machine_eval_ins mov s) in
          s1.ms_ok ==> equiv_states s1 s2))

    dst: Vale.X64.Machine_s.operand64 ->
    src: Vale.X64.Machine_s.operand64 ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> FStar.Pervasives.Lemma (requires OReg? dst)
      (ensures
        (let movbe =
            Vale.X64.InsLemmas.make_instr_annotate Vale.X64.Instructions_s.ins_MovBe64
              (Vale.X64.Machine_Semantics_s.AnnotateMovbe64 ())
              dst
              src
          in
          let mov = Vale.X64.InsLemmas.make_instr Vale.X64.Instructions_s.ins_Mov64 dst src in
          let bswap = Vale.X64.InsLemmas.make_instr Vale.X64.Instructions_s.ins_Bswap64 dst in
          let s1 = Vale.X64.Machine_Semantics_s.machine_eval_ins movbe s in
          let s2 =
            Vale.X64.Machine_Semantics_s.machine_eval_ins bswap
              (Vale.X64.Machine_Semantics_s.machine_eval_ins mov s)
          in
          Mkmachine_state?.ms_ok s1 ==> Vale.Transformers.InstructionReorder.equiv_states s1 s2))