val va_wpProof_Comment : c:string -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Comment c va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Comment c) ([]) va_s0 va_k ((va_sM,
    va_f0, va_g))))
let va_wpProof_Comment c va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Comment (va_code_Comment c) va_s0 c in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM va_s0));
  va_lemma_norm_mods ([]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)
val va_wpProof_Comment : c:string -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Comment c va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Comment c) ([]) va_s0 va_k ((va_sM,
    va_f0, va_g))))
let va_wpProof_Comment c va_s0 va_k =
let va_sM, va_f0 = va_lemma_Comment (va_code_Comment c) va_s0 c in
va_lemma_upd_update va_sM;
assert (va_state_eq va_sM (va_update_ok va_sM va_s0));
va_lemma_norm_mods ([]) va_sM va_s0;
let va_g = () in
(va_sM, va_f0, va_g)
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
Prims.string Vale.X64.Decls.va_state Prims.unit Vale.X64.Decls.va_fuel FStar.Pervasives.Native.Mktuple3 Vale.X64.QuickCode.va_lemma_norm_mods Prims.Nil Vale.X64.QuickCode.mod_t Prims._assert Vale.X64.Decls.va_state_eq Vale.X64.Decls.va_update_ok Vale.X64.Decls.va_lemma_upd_update FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.tuple2 Vale.X64.State.vale_state Vale.X64.InsBasic.va_lemma_Comment Vale.X64.InsBasic.va_code_Comment
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"]
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)


[@"opaque_to_smt"]
let va_wpProof_Sub64Wrap dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Sub64Wrap (va_code_Sub64Wrap 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)

//--
//-- Sbb64

[@ "opaque_to_smt"]
let va_code_Sbb64 dst src =
  (mk_ins (make_instr (I.ins_Sbb64) dst src))

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

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


[@"opaque_to_smt"]
let va_wpProof_Sbb64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Sbb64 (va_code_Sbb64 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)

//--
#restart-solver
#push-options "--max_fuel 0 --max_ifuel 0 --using_facts_from 'Prims FStar.UInt'"
let lemma_fundamental_div_mod (a b:nat64) :
  Lemma (pow2_64 * (FStar.UInt.mul_div #64 a b) + (FStar.UInt.mul_mod #64 a b) == a * b)
  =
  FStar.Math.Lemmas.lemma_div_mod (a * b) pow2_64
#pop-options
//-- lemma_fundamental_div_mod
//--
//-- Mul64Wrap

[@ "opaque_to_smt"]
let va_code_Mul64Wrap src =
  (mk_ins (make_instr (I.ins_Mul64) src))

[@ "opaque_to_smt"]
let va_codegen_success_Mul64Wrap src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Mul64Wrap va_b0 va_s0 src =
  va_reveal_opaque (`%va_code_Mul64Wrap) (va_code_Mul64Wrap src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Mul64) src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Mul64) src)) va_s0 in
  lemma_fundamental_div_mod (va_get_reg64 rRax va_old_s) (va_eval_opr64 va_old_s src);
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Mul64Wrap src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mul64Wrap (va_code_Mul64Wrap src) va_s0 src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM
    (va_update_flags va_sM (va_update_ok va_sM va_s0)))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_flags]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Mulx64

[@ "opaque_to_smt"]
let va_code_Mulx64 dst_hi dst_lo src =
  (mk_ins (make_instr (I.ins_Mulx64) dst_hi dst_lo src))

[@ "opaque_to_smt"]
let va_codegen_success_Mulx64 dst_hi dst_lo src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Mulx64 va_b0 va_s0 dst_hi dst_lo src =
  va_reveal_opaque (`%va_code_Mulx64) (va_code_Mulx64 dst_hi dst_lo src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Mulx64) dst_hi dst_lo src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Mulx64) dst_hi dst_lo src)) va_s0 in
  lemma_fundamental_div_mod (va_get_reg64 rRdx va_old_s) (va_eval_opr64 va_old_s src);
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Mulx64 dst_hi dst_lo src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mulx64 (va_code_Mulx64 dst_hi dst_lo src) va_s0 dst_hi dst_lo 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_lo va_sM
    (va_update_operand_dst_opr64 dst_hi va_sM va_s0))));
  va_lemma_norm_mods ([va_mod_dst_opr64 dst_lo; va_mod_dst_opr64 dst_hi]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- lemma_mul_nat
//--
//-- lemma_mul_in_bounds
//--
//-- IMul64

[@ "opaque_to_smt"]
let va_code_IMul64 dst src =
  (mk_ins (make_instr (I.ins_IMul64) dst src))

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

[@"opaque_to_smt"]
let va_lemma_IMul64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_IMul64) (va_code_IMul64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_IMul64) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_IMul64) dst src)) va_s0 in
  lemma_mul_nat (va_eval_dst_opr64 va_old_s dst) (va_eval_opr64 va_old_s src);
  lemma_mul_in_bounds (va_eval_dst_opr64 va_old_s dst) (va_eval_opr64 va_old_s src);
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_IMul64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_IMul64 (va_code_IMul64 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)

//--
//-- Xor64

[@ "opaque_to_smt"]
let va_code_Xor64 dst src =
  (mk_ins (make_instr_annotate (I.ins_Xor64) (S.AnnotateXor64 ()) dst src))

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

[@"opaque_to_smt"]
let va_lemma_Xor64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Xor64) (va_code_Xor64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (I.ins_Xor64) (S.AnnotateXor64 ()) dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (I.ins_Xor64) (S.AnnotateXor64 ())
    dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Xor64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Xor64 (va_code_Xor64 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)

//--
//-- And64

[@ "opaque_to_smt"]
let va_code_And64 dst src =
  (mk_ins (make_instr (I.ins_And64) dst src))

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

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


[@"opaque_to_smt"]
let va_wpProof_And64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_And64 (va_code_And64 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)

//--
//-- Shl64

[@ "opaque_to_smt"]
let va_code_Shl64 dst amt =
  (mk_ins (make_instr (I.ins_Shl64) dst amt))

[@ "opaque_to_smt"]
let va_codegen_success_Shl64 dst amt =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Shl64 va_b0 va_s0 dst amt =
  va_reveal_opaque (`%va_code_Shl64) (va_code_Shl64 dst amt);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Shl64) dst amt)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Shl64) dst amt)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Shl64 dst amt va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Shl64 (va_code_Shl64 dst amt) va_s0 dst amt 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)

//--
//-- Shr64

[@ "opaque_to_smt"]
let va_code_Shr64 dst amt =
  (mk_ins (make_instr (I.ins_Shr64) dst amt))

[@ "opaque_to_smt"]
let va_codegen_success_Shr64 dst amt =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Shr64 va_b0 va_s0 dst amt =
  va_reveal_opaque (`%va_code_Shr64) (va_code_Shr64 dst amt);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Shr64) dst amt)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Shr64) dst amt)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Shr64 dst amt va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Shr64 (va_code_Shr64 dst amt) va_s0 dst amt 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)

//--
//-- Cpuid_AES

[@ "opaque_to_smt"]
let va_code_Cpuid_AES () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_AES () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_AES va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_AES) (va_code_Cpuid_AES ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_AES va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_AES (va_code_Cpuid_AES ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Sha

[@ "opaque_to_smt"]
let va_code_Cpuid_Sha () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Sha () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Sha va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Sha) (va_code_Cpuid_Sha ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Sha va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Sha (va_code_Cpuid_Sha ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Adx_Bmi2

[@ "opaque_to_smt"]
let va_code_Cpuid_Adx_Bmi2 () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Adx_Bmi2 () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Adx_Bmi2 va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Adx_Bmi2) (va_code_Cpuid_Adx_Bmi2 ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Adx_Bmi2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Adx_Bmi2 (va_code_Cpuid_Adx_Bmi2 ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Avx

[@ "opaque_to_smt"]
let va_code_Cpuid_Avx () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Avx () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Avx va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Avx) (va_code_Cpuid_Avx ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Avx va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Avx (va_code_Cpuid_Avx ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Avx2

[@ "opaque_to_smt"]
let va_code_Cpuid_Avx2 () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Avx2 () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Avx2 va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Avx2) (va_code_Cpuid_Avx2 ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Avx2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Avx2 (va_code_Cpuid_Avx2 ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Sse

[@ "opaque_to_smt"]
let va_code_Cpuid_Sse () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Sse () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Sse va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Sse) (va_code_Cpuid_Sse ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Sse va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Sse (va_code_Cpuid_Sse ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Movbe

[@ "opaque_to_smt"]
let va_code_Cpuid_Movbe () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Movbe () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Movbe va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Movbe) (va_code_Cpuid_Movbe ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Movbe va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Movbe (va_code_Cpuid_Movbe ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Rdrand

[@ "opaque_to_smt"]
let va_code_Cpuid_Rdrand () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Rdrand () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Rdrand va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Rdrand) (va_code_Cpuid_Rdrand ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Rdrand va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Rdrand (va_code_Cpuid_Rdrand ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Avx512

[@ "opaque_to_smt"]
let va_code_Cpuid_Avx512 () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Avx512 () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Avx512 va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Avx512) (va_code_Cpuid_Avx512 ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Avx512 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Avx512 (va_code_Cpuid_Avx512 ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Cpuid_Osxsave

[@ "opaque_to_smt"]
let va_code_Cpuid_Osxsave () =
  (mk_ins (make_instr (I.ins_Cpuid)))

[@ "opaque_to_smt"]
let va_codegen_success_Cpuid_Osxsave () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Cpuid_Osxsave va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Cpuid_Osxsave) (va_code_Cpuid_Osxsave ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Cpuid))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Cpuid))) va_s0 in
  Vale.X64.CPU_Features_s.cpuid_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Cpuid_Osxsave va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cpuid_Osxsave (va_code_Cpuid_Osxsave ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Xgetbv_Avx

[@ "opaque_to_smt"]
let va_code_Xgetbv_Avx () =
  (mk_ins (make_instr (I.ins_Xgetbv)))

[@ "opaque_to_smt"]
let va_codegen_success_Xgetbv_Avx () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Xgetbv_Avx va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Xgetbv_Avx) (va_code_Xgetbv_Avx ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Xgetbv))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Xgetbv))) va_s0 in
  Vale.X64.CPU_Features_s.xgetbv_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Xgetbv_Avx va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Xgetbv_Avx (va_code_Xgetbv_Avx ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM (va_update_ok
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRax]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Xgetbv_Avx512

[@ "opaque_to_smt"]
let va_code_Xgetbv_Avx512 () =
  (mk_ins (make_instr (I.ins_Xgetbv)))

[@ "opaque_to_smt"]
let va_codegen_success_Xgetbv_Avx512 () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Xgetbv_Avx512 va_b0 va_s0 =
  va_reveal_opaque (`%va_code_Xgetbv_Avx512) (va_code_Xgetbv_Avx512 ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Xgetbv))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Xgetbv))) va_s0 in
  Vale.X64.CPU_Features_s.xgetbv_features ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Xgetbv_Avx512 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Xgetbv_Avx512 (va_code_Xgetbv_Avx512 ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM (va_update_ok
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_reg64 rRdx; va_Mod_reg64 rRax]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Nat64Equal

[@ "opaque_to_smt"]
let va_code_Nat64Equal dst src =
  (va_Block (va_CCons (va_code_Sub64Wrap (va_coerce_reg_opr64_to_dst_opr64 src) (va_const_opr64
    18446744073709551615)) (va_CCons (va_code_Mov64 (va_coerce_reg_opr64_to_dst_opr64 dst)
    (va_const_opr64 0)) (va_CCons (va_code_Adc64 (va_coerce_reg_opr64_to_dst_opr64 dst)
    (va_const_opr64 0)) (va_CNil ())))))

[@ "opaque_to_smt"]
let va_codegen_success_Nat64Equal dst src =
  (va_pbool_and (va_codegen_success_Sub64Wrap (va_coerce_reg_opr64_to_dst_opr64 src)
    (va_const_opr64 18446744073709551615)) (va_pbool_and (va_codegen_success_Mov64
    (va_coerce_reg_opr64_to_dst_opr64 dst) (va_const_opr64 0)) (va_pbool_and
    (va_codegen_success_Adc64 (va_coerce_reg_opr64_to_dst_opr64 dst) (va_const_opr64 0)) (va_ttrue
    ()))))

[@"opaque_to_smt"]
let va_lemma_Nat64Equal va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Nat64Equal) (va_code_Nat64Equal dst src);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (va_s2, va_fc2) = va_lemma_Sub64Wrap (va_hd va_b1) va_s0 (va_coerce_reg_opr64_to_dst_opr64
    src) (va_const_opr64 18446744073709551615) in
  let va_b2 = va_tl va_b1 in
  let (va_s3, va_fc3) = va_lemma_Mov64 (va_hd va_b2) va_s2 (va_coerce_reg_opr64_to_dst_opr64 dst)
    (va_const_opr64 0) in
  let va_b3 = va_tl va_b2 in
  let (va_s4, va_fc4) = va_lemma_Adc64 (va_hd va_b3) va_s3 (va_coerce_reg_opr64_to_dst_opr64 dst)
    (va_const_opr64 0) in
  let va_b4 = va_tl va_b3 in
  let (va_sM, va_f4) = va_lemma_empty_total va_s4 va_b4 in
  let va_f3 = va_lemma_merge_total va_b3 va_s3 va_fc4 va_s4 va_f4 va_sM in
  let va_f2 = va_lemma_merge_total va_b2 va_s2 va_fc3 va_s3 va_f3 va_sM in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc2 va_s2 va_f2 va_sM in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Nat64Equal dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Nat64Equal (va_code_Nat64Equal 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_reg_opr64
    src va_sM (va_update_operand_reg_opr64 dst va_sM va_s0)))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_reg_opr64 src; va_mod_reg_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Comment

[@ "opaque_to_smt"]
let va_code_Comment c =
  (mk_ins (make_instr_annotate (I.ins_Comment c) (S.AnnotateComment c)))

[@ "opaque_to_smt"]
let va_codegen_success_Comment c =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Comment va_b0 va_s0 c =
  va_reveal_opaque (`%va_code_Comment) (va_code_Comment c);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (I.ins_Comment c) (S.AnnotateComment c))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (I.ins_Comment c)
    (S.AnnotateComment c))) va_s0 in
  (va_sM, va_fM)
val va_wpProof_Comment : c:string -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Comment c va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Comment c) ([]) va_s0 va_k ((va_sM,
    va_f0, va_g))))

    c: Prims.string ->
    va_s0: Vale.X64.Decls.va_state ->
    va_k: (_: Vale.X64.Decls.va_state -> _: Prims.unit -> Type0)
  -> Prims.Ghost ((Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel) * Prims.unit)