val safe_mov_mov_elim (is: list ins) : Tot bool
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
val safe_mov_mov_elim (is: list ins) : Tot bool
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)
| _ -> false
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
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_s.operand64 Prims.op_AmpAmp Prims.op_Equality Vale.X64.Machine_s.uu___is_OReg Vale.X64.Machine_s.nat64 Vale.X64.Machine_s.reg_64 Prims.op_Negation Vale.X64.Machine_s.maddr Vale.Arch.HeapTypes_s.taint Prims.int Prims.bool FStar.Pervasives.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.zeta FStar.Pervasives.iota FStar.Pervasives.delta_attr Prims.string Prims.Nil Vale.X64.Instruction_s.instr_out FStar.Pervasives.Native.Mktuple2 Vale.X64.Instruction_s.instr_operand_inout Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.Out Vale.X64.Instruction_s.IOpEx Vale.X64.Instruction_s.IOp64 Vale.Transformers.PeepHole.coerce_to_normal Vale.X64.Instruction_s.out Vale.X64.Instruction_s.op64
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"
val safe_mov_mov_elim (is: list ins) : Tot bool
is: Prims.list Vale.X64.Machine_Semantics_s.ins -> Prims.bool