val va_codegen_success_Mov64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> Tot va_pbool
let va_codegen_success_Mov64 dst src =
  (va_ttrue ())
val va_codegen_success_Mov64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> Tot va_pbool
let va_codegen_success_Mov64 dst src =
(va_ttrue ())
Vale.X64.InsBasic.fst.checked
Vale.X64.Taint_Semantics.fst.checked Vale.X64.StateLemmas.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.Decls.fst.checked Vale.X64.CPU_Features_s.fst.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked
Vale.X64.InsBasic.fst
Vale.X64.Decls.va_operand_dst_opr64 Vale.X64.Decls.va_operand_opr64 Vale.X64.Decls.va_ttrue Vale.X64.Decls.va_pbool
module Vale.X64.InsBasic
open Vale.X64
open Vale.X64.StateLemmas
open Vale.X64.InsLemmas
open Vale.X64.Taint_Semantics
open Vale.X64.CPU_Features_s
open Vale.X64.Memory
open Vale.X64.Stack_i
module I = Vale.X64.Instructions_s
module S = Vale.X64.Machine_Semantics_s
friend Vale.X64.Decls
#reset-options "--initial_fuel 5 --max_fuel 5 --max_ifuel 2 --z3rlimit 20"
//-- Mov64

[@ "opaque_to_smt"]
let va_code_Mov64 dst src =
  (mk_ins (make_instr_annotate (I.ins_Mov64) (S.AnnotateMov64 ()) dst src))

[@ "opaque_to_smt"]
val va_codegen_success_Mov64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> Tot va_pbool
dst: Vale.X64.Decls.va_operand_dst_opr64 -> src: Vale.X64.Decls.va_operand_opr64
  -> Vale.X64.Decls.va_pbool