let mov_mov_elim_ph = {
  ph = (fun is ->
      if safe_mov_mov_elim is then (
        let [i1; i2] = is in
        Some [i2]
      ) else None);
  input_hint = 2;
}
let mov_mov_elim_ph =
{
  ph
  =
  (fun is ->
      if safe_mov_mov_elim is
      then
        (let [i1 ; i2] = is in
          Some [i2])
      else None);
  input_hint = 2
}
Vale.Transformers.MovMovElim.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 Vale.Def.Types_s.fst.checked Vale.Def.PossiblyMonad.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Vale.Transformers.MovMovElim.fst
Vale.Transformers.PeepHole.Mkpre_peephole Prims.list Vale.X64.Machine_Semantics_s.ins Vale.Transformers.MovMovElim.safe_mov_mov_elim FStar.Pervasives.Native.Some Prims.Cons Prims.Nil FStar.Pervasives.Native.option Prims.bool FStar.Pervasives.Native.None
module Vale.Transformers.MovMovElim

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.Def.PossiblyMonad
open Vale.Transformers.InstructionReorder
open Vale.X64.InsLemmas

open Vale.Transformers.PeepHole

(*
 * AR: this proof relies on multiple inductive type inversions to know that
 *     oprs1 is a Mov64 (resp. for oprs2)
 *    
 *     this used to go through earlier with just ifuel 1, because F* was weakening
 *       the branch VCs with discriminator expressions, thereby unintentionally
 *       triggering the inversions, this is no longer true in F*, and hence more ifuel
 *)

#push-options "--ifuel 4"
let safe_mov_mov_elim (is:list ins) : Tot bool =
  match is with
  | [Instr i1 oprs1 (AnnotateMov64 ()); Instr i2 oprs2 (AnnotateMov64 ())] ->
    let oprs1:normal (instr_operands_t [out op64] [op64]) =
      coerce_to_normal #(instr_operands_t [out op64] [op64]) oprs1 in
    let oprs2:normal (instr_operands_t [out op64] [op64]) =
      coerce_to_normal #(instr_operands_t [out op64] [op64]) oprs2 in
    let (dst1, (src1, ())) = oprs1 in
    let (dst2, (src2, ())) = oprs2 in
    dst1 = dst2 && OReg? dst1 && (
      let OReg rd = dst1 in
      match src2 with
      | OConst _ -> true
      | OReg rs2 -> not (rs2 = rd)
      | OStack (m, _) | OMem (m, _) ->
        match m with
        | MConst _ -> true
        | _ -> false // TODO: Can we relax this restriction?
    )
  | _ -> false
#pop-options
val mov_mov_elim_ph : Vale.Transformers.PeepHole.pre_peephole
Vale.Transformers.PeepHole.pre_peephole