val va_lemma_Sub64Wrap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_dst_opr64 ->
  src:va_operand_opr64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Sub64Wrap dst src) va_s0 /\ va_is_dst_dst_opr64 dst
    va_s0 /\ va_is_src_opr64 src va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_dst_opr64 va_sM dst == Vale.Arch.Types.sub_wrap64 (va_eval_dst_opr64 va_s0 dst)
    (va_eval_opr64 va_s0 src) /\ Vale.X64.Decls.updated_cf (va_get_flags va_sM) (va_eval_dst_opr64
    va_s0 dst - va_eval_opr64 va_s0 src < 0) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM va_s0)))))
let va_lemma_Sub64Wrap va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Sub64Wrap) (va_code_Sub64Wrap dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Sub64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Sub64) dst src)) va_s0 in
  (va_sM, va_fM)
val va_lemma_Sub64Wrap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_dst_opr64 ->
  src:va_operand_opr64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Sub64Wrap dst src) va_s0 /\ va_is_dst_dst_opr64 dst
    va_s0 /\ va_is_src_opr64 src va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_dst_opr64 va_sM dst == Vale.Arch.Types.sub_wrap64 (va_eval_dst_opr64 va_s0 dst)
    (va_eval_opr64 va_s0 src) /\ Vale.X64.Decls.updated_cf (va_get_flags va_sM) (va_eval_dst_opr64
    va_s0 dst - va_eval_opr64 va_s0 src < 0) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM va_s0)))))
let va_lemma_Sub64Wrap va_b0 va_s0 dst src =
va_reveal_opaque (`%va_code_Sub64Wrap) (va_code_Sub64Wrap dst src);
let va_old_s:va_state = va_s0 in
va_ins_lemma (mk_ins (make_instr (I.ins_Sub64) dst src)) va_s0;
let va_sM, va_fM = va_eval_ins (mk_ins (make_instr (I.ins_Sub64) dst src)) va_s0 in
(va_sM, va_fM)
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_code Vale.X64.Decls.va_state Vale.X64.Decls.va_operand_dst_opr64 Vale.X64.Decls.va_operand_opr64 Vale.X64.State.vale_state Vale.X64.Lemmas.fuel FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_fuel FStar.Pervasives.Native.tuple2 Prims.nat Vale.X64.Decls.va_eval_ins Vale.X64.Taint_Semantics.mk_ins Vale.X64.InsLemmas.make_instr Prims.Cons Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.out Vale.X64.Instruction_s.opFlagsCf Vale.X64.Instruction_s.inOut Vale.X64.Instruction_s.op64 Prims.Nil Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.HavocFlags Vale.X64.Instructions_s.ins_Sub64 Prims.unit Vale.X64.Decls.va_ins_lemma Vale.X64.Decls.va_reveal_opaque Vale.X64.InsBasic.va_code_Sub64Wrap
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"]
let va_codegen_success_Mov64 dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Mov64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Mov64) (va_code_Mov64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (I.ins_Mov64) (S.AnnotateMov64 ()) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (I.ins_Mov64) (S.AnnotateMov64 ())
    dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Mov64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mov64 (va_code_Mov64 dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cmovc64

[@ "opaque_to_smt"]
let va_code_Cmovc64 dst src =
  (mk_ins (make_instr (I.ins_Cmovc64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Cmovc64 dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cmovc64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Cmovc64) (va_code_Cmovc64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cmovc64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cmovc64) dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cmovc64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cmovc64 (va_code_Cmovc64 dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Add64

[@ "opaque_to_smt"]
let va_code_Add64 dst src =
  (mk_ins (make_instr (I.ins_Add64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Add64 dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Add64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Add64) (va_code_Add64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Add64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Add64) dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Add64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Add64 (va_code_Add64 dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64
    dst va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Add64Wrap

[@ "opaque_to_smt"]
let va_code_Add64Wrap dst src =
  (mk_ins (make_instr (I.ins_Add64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Add64Wrap dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Add64Wrap va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Add64Wrap) (va_code_Add64Wrap dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Add64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Add64) dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Add64Wrap dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Add64Wrap (va_code_Add64Wrap dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64
    dst va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- AddLea64

[@ "opaque_to_smt"]
let va_code_AddLea64 dst src1 src2 =
  (mk_ins (make_instr (I.ins_AddLea64) dst src1 src2))

[@ "opaque_to_smt"]
let va_codegen_success_AddLea64 dst src1 src2 =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_AddLea64 va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_AddLea64) (va_code_AddLea64 dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_AddLea64) dst src1 src2)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_AddLea64) dst src1 src2)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_AddLea64 dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_AddLea64 (va_code_AddLea64 dst src1 src2) va_s0 dst src1 src2 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Adc64

[@ "opaque_to_smt"]
let va_code_Adc64 dst src =
  (mk_ins (make_instr (I.ins_AddCarry64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Adc64 dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Adc64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Adc64) (va_code_Adc64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_AddCarry64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_AddCarry64) dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Adc64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Adc64 (va_code_Adc64 dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64
    dst va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Adc64Wrap

[@ "opaque_to_smt"]
let va_code_Adc64Wrap dst src =
  (mk_ins (make_instr (I.ins_AddCarry64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Adc64Wrap dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Adc64Wrap va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Adc64Wrap) (va_code_Adc64Wrap dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_AddCarry64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_AddCarry64) dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Adc64Wrap dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Adc64Wrap (va_code_Adc64Wrap dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64
    dst va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Adcx64Wrap
#push-options "--smtencoding.nl_arith_repr boxwrap"

[@ "opaque_to_smt"]
let va_code_Adcx64Wrap dst src =
  (mk_ins (make_instr (I.ins_Adcx64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Adcx64Wrap dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Adcx64Wrap va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Adcx64Wrap) (va_code_Adcx64Wrap dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Adcx64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Adcx64) dst src)) va_s0 in
  assert (Vale.Arch.Types.add_wrap64 (Vale.Arch.Types.add_wrap64 (va_eval_dst_opr64 va_old_s dst)
    (va_eval_opr64 va_old_s src)) (if Vale.X64.Decls.cf (va_get_flags va_old_s) then 1 else 0) ==
    (va_eval_dst_opr64 va_old_s dst + va_eval_opr64 va_old_s src + (if Vale.X64.Decls.cf
    (va_get_flags va_old_s) then 1 else 0)) `op_Modulus` pow2_64);
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Adcx64Wrap dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Adcx64Wrap (va_code_Adcx64Wrap dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64
    dst va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

#pop-options
//--
//-- Adox64Wrap

[@ "opaque_to_smt"]
let va_code_Adox64Wrap dst src =
  (mk_ins (make_instr (I.ins_Adox64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Adox64Wrap dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Adox64Wrap va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Adox64Wrap) (va_code_Adox64Wrap dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Adox64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Adox64) dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Adox64Wrap dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Adox64Wrap (va_code_Adox64Wrap dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64
    dst va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Sub64

[@ "opaque_to_smt"]
let va_code_Sub64 dst src =
  (mk_ins (make_instr (I.ins_Sub64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Sub64 dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Sub64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Sub64) (va_code_Sub64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Sub64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Sub64) dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Sub64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Sub64 (va_code_Sub64 dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64
    dst va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Sub64Wrap

[@ "opaque_to_smt"]
let va_code_Sub64Wrap dst src =
  (mk_ins (make_instr (I.ins_Sub64) dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Sub64Wrap dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
val va_lemma_Sub64Wrap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_dst_opr64 ->
  src:va_operand_opr64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Sub64Wrap dst src) va_s0 /\ va_is_dst_dst_opr64 dst
    va_s0 /\ va_is_src_opr64 src va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_dst_opr64 va_sM dst == Vale.Arch.Types.sub_wrap64 (va_eval_dst_opr64 va_s0 dst)
    (va_eval_opr64 va_s0 src) /\ Vale.X64.Decls.updated_cf (va_get_flags va_sM) (va_eval_dst_opr64
    va_s0 dst - va_eval_opr64 va_s0 src < 0) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM va_s0)))))

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    dst: Vale.X64.Decls.va_operand_dst_opr64 ->
    src: Vale.X64.Decls.va_operand_opr64
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)