val va_wp_AESNI_imc (dst src: va_operand_xmm) (va_s0: va_state) (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_AESNI_imc (dst:va_operand_xmm) (src:va_operand_xmm) (va_s0:va_state) (va_k:(va_state ->
  unit -> Type0)) : Type0 =
  (va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ aesni_enabled /\
    (forall (va_x_dst:va_value_xmm) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl
    (va_upd_operand_xmm dst va_x_dst va_s0) in va_get_ok va_sM /\ va_eval_xmm va_sM dst ==
    Vale.AES.AES_s.inv_mix_columns_LE (va_eval_xmm va_s0 src) ==> va_k va_sM (())))
val va_wp_AESNI_imc (dst src: va_operand_xmm) (va_s0: va_state) (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_AESNI_imc (dst src: va_operand_xmm) (va_s0: va_state) (va_k: (va_state -> unit -> Type0))
    : Type0 =
(va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ aesni_enabled /\
  (forall (va_x_dst: va_value_xmm) (va_x_efl: Vale.X64.Flags.t).
      let va_sM = va_upd_flags va_x_efl (va_upd_operand_xmm dst va_x_dst va_s0) in
      va_get_ok va_sM /\
      va_eval_xmm va_sM dst == Vale.AES.AES_s.inv_mix_columns_LE (va_eval_xmm va_s0 src) ==>
      va_k va_sM (())))
Vale.X64.InsAes.fst.checked
Vale.X64.Taint_Semantics.fst.checked Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.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.InsLemmas.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fst.checked Vale.X64.Decls.fst.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Types_s.fst.checked Vale.AES.AES_s.fst.checked Vale.AES.AES_common_s.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.X64.InsAes.fst
Vale.X64.Decls.va_operand_xmm Vale.X64.Decls.va_state Prims.unit Prims.l_and Vale.X64.Decls.va_is_dst_xmm Vale.X64.Decls.va_is_src_xmm Prims.b2t Vale.X64.Decls.va_get_ok Vale.X64.CPU_Features_s.aesni_enabled Prims.l_Forall Vale.X64.Decls.va_value_xmm Vale.X64.Flags.t Prims.l_imp Prims.eq2 Vale.Def.Types_s.quad32 Vale.X64.Decls.va_eval_xmm Vale.AES.AES_s.inv_mix_columns_LE Vale.X64.State.vale_state Vale.X64.Decls.va_upd_flags Vale.X64.Decls.va_upd_operand_xmm
module Vale.X64.InsAes
open Vale.Def.Types_s
open Vale.X64.Machine_s
open Vale.X64
open Vale.X64.State
open Vale.X64.StateLemmas
open Vale.X64.InsLemmas
open Vale.X64.Taint_Semantics
open Vale.X64.Decls
open Vale.X64.CPU_Features_s
module I = Vale.X64.Instructions_s
module S = Vale.X64.Machine_Semantics_s
module P = Vale.X64.Print_s

friend Vale.X64.Decls
#reset-options "--initial_fuel 4 --max_fuel 4 --z3rlimit 20"
//-- Pclmulqdq

[@ "opaque_to_smt"]
let va_code_Pclmulqdq dst src dstHi srcHi =
  (mk_ins (make_instr (I.ins_Pclmulqdq ((if dstHi then 1 else 0) + (if srcHi then 16 else 0)))
    (OReg dst) (OReg src)))

[@ "opaque_to_smt"]
let va_codegen_success_Pclmulqdq dst src dstHi srcHi =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Pclmulqdq va_b0 va_s0 dst src dstHi srcHi =
  va_reveal_opaque (`%va_code_Pclmulqdq) (va_code_Pclmulqdq dst src dstHi srcHi);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_Pclmulqdq ((if dstHi then 1 else 0) + (if srcHi then 16
    else 0))) (OReg dst) (OReg src))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_Pclmulqdq ((if dstHi then 1 else 0) +
    (if srcHi then 16 else 0))) (OReg dst) (OReg src))) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Pclmulqdq dst src dstHi srcHi va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Pclmulqdq (va_code_Pclmulqdq dst src dstHi srcHi) va_s0 dst src
    dstHi srcHi 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_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- VPclmulqdq

[@ "opaque_to_smt"]
let va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi =
  (mk_ins (make_instr (I.ins_VPclmulqdq ((if src1Hi then 1 else 0) + (if src2Hi then 16 else 0)))
    (OReg dst) (OReg src1) (OReg src2)))

[@ "opaque_to_smt"]
let va_codegen_success_VPclmulqdq dst src1 src2 src1Hi src2Hi =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_VPclmulqdq va_b0 va_s0 dst src1 src2 src1Hi src2Hi =
  va_reveal_opaque (`%va_code_VPclmulqdq) (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_VPclmulqdq ((if src1Hi then 1 else 0) + (if src2Hi then
    16 else 0))) (OReg dst) (OReg src1) (OReg src2))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_VPclmulqdq ((if src1Hi then 1 else 0)
    + (if src2Hi then 16 else 0))) (OReg dst) (OReg src1) (OReg src2))) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_VPclmulqdq dst src1 src2 src1Hi src2Hi va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VPclmulqdq (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi) va_s0
    dst src1 src2 src1Hi src2Hi 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_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- AESNI_enc

[@ "opaque_to_smt"]
let va_code_AESNI_enc dst src =
  (mk_ins (make_instr (I.ins_AESNI_enc) (OReg dst) (OReg src)))

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

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


[@"opaque_to_smt"]
let va_wpProof_AESNI_enc dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_AESNI_enc (va_code_AESNI_enc 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_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- VAESNI_enc

[@ "opaque_to_smt"]
let va_code_VAESNI_enc dst src1 src2 =
  (mk_ins (make_instr (I.ins_VAESNI_enc) (OReg dst) (OReg src1) (OReg src2)))

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

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


[@"opaque_to_smt"]
let va_wpProof_VAESNI_enc dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VAESNI_enc (va_code_VAESNI_enc dst src1 src2) va_s0 dst src1 src2 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_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- AESNI_enc_last

[@ "opaque_to_smt"]
let va_code_AESNI_enc_last dst src =
  (mk_ins (make_instr (I.ins_AESNI_enc_last) (OReg dst) (OReg src)))

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

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


[@"opaque_to_smt"]
let va_wpProof_AESNI_enc_last dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_AESNI_enc_last (va_code_AESNI_enc_last 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_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- VAESNI_enc_last

[@ "opaque_to_smt"]
let va_code_VAESNI_enc_last dst src1 src2 =
  (mk_ins (make_instr (I.ins_VAESNI_enc_last) (OReg dst) (OReg src1) (OReg src2)))

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

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


[@"opaque_to_smt"]
let va_wpProof_VAESNI_enc_last dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VAESNI_enc_last (va_code_VAESNI_enc_last dst src1 src2) va_s0 dst
    src1 src2 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_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- AESNI_dec

val va_code_AESNI_dec : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_code
[@ "opaque_to_smt"]
let va_code_AESNI_dec dst src =
  (mk_ins (make_instr (I.ins_AESNI_dec) (OReg dst) (OReg src)))

val va_codegen_success_AESNI_dec : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_AESNI_dec dst src =
  (va_ttrue ())


val va_lemma_AESNI_dec : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm -> src:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AESNI_dec dst src) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ aesni_enabled))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_xmm va_sM dst == Vale.Def.Types_s.quad32_xor (Vale.AES.AES_s.inv_mix_columns_LE
    (Vale.AES.AES_common_s.inv_sub_bytes (Vale.AES.AES_s.inv_shift_rows_LE (va_eval_xmm va_s0
    dst)))) (va_eval_xmm va_s0 src) /\ va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM
    (va_update_operand_xmm dst va_sM va_s0)))))
[@"opaque_to_smt"]
let va_lemma_AESNI_dec va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_AESNI_dec) (va_code_AESNI_dec dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_AESNI_dec) (OReg dst) (OReg src))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_AESNI_dec) (OReg dst) (OReg src)))
    va_s0 in
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_AESNI_dec (dst:va_operand_xmm) (src:va_operand_xmm) (va_s0:va_state) (va_k:(va_state ->
  unit -> Type0)) : Type0 =
  (va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ aesni_enabled /\
    (forall (va_x_dst:va_value_xmm) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl
    (va_upd_operand_xmm dst va_x_dst va_s0) in va_get_ok va_sM /\ va_eval_xmm va_sM dst ==
    Vale.Def.Types_s.quad32_xor (Vale.AES.AES_s.inv_mix_columns_LE
    (Vale.AES.AES_common_s.inv_sub_bytes (Vale.AES.AES_s.inv_shift_rows_LE (va_eval_xmm va_s0
    dst)))) (va_eval_xmm va_s0 src) ==> va_k va_sM (())))


val va_wpProof_AESNI_dec : dst:va_operand_xmm -> src:va_operand_xmm -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AESNI_dec dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AESNI_dec dst src) ([va_Mod_flags;
    va_mod_xmm dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_AESNI_dec dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_AESNI_dec (va_code_AESNI_dec 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_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_AESNI_dec (dst:va_operand_xmm) (src:va_operand_xmm) : (va_quickCode unit
  (va_code_AESNI_dec dst src)) =
  (va_QProc (va_code_AESNI_dec dst src) ([va_Mod_flags; va_mod_xmm dst]) (va_wp_AESNI_dec dst src)
    (va_wpProof_AESNI_dec dst src))
//--
//-- AESNI_dec_last

val va_code_AESNI_dec_last : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_code
[@ "opaque_to_smt"]
let va_code_AESNI_dec_last dst src =
  (mk_ins (make_instr (I.ins_AESNI_dec_last) (OReg dst) (OReg src)))

val va_codegen_success_AESNI_dec_last : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_AESNI_dec_last dst src =
  (va_ttrue ())


val va_lemma_AESNI_dec_last : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AESNI_dec_last dst src) va_s0 /\ va_is_dst_xmm dst
    va_s0 /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ aesni_enabled))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_xmm va_sM dst == Vale.Def.Types_s.quad32_xor (Vale.AES.AES_common_s.inv_sub_bytes
    (Vale.AES.AES_s.inv_shift_rows_LE (va_eval_xmm va_s0 dst))) (va_eval_xmm va_s0 src) /\
    va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst va_sM
    va_s0)))))
[@"opaque_to_smt"]
let va_lemma_AESNI_dec_last va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_AESNI_dec_last) (va_code_AESNI_dec_last dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_AESNI_dec_last) (OReg dst) (OReg src))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_AESNI_dec_last) (OReg dst) (OReg
    src))) va_s0 in
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_AESNI_dec_last (dst:va_operand_xmm) (src:va_operand_xmm) (va_s0:va_state) (va_k:(va_state
  -> unit -> Type0)) : Type0 =
  (va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ aesni_enabled /\
    (forall (va_x_dst:va_value_xmm) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl
    (va_upd_operand_xmm dst va_x_dst va_s0) in va_get_ok va_sM /\ va_eval_xmm va_sM dst ==
    Vale.Def.Types_s.quad32_xor (Vale.AES.AES_common_s.inv_sub_bytes
    (Vale.AES.AES_s.inv_shift_rows_LE (va_eval_xmm va_s0 dst))) (va_eval_xmm va_s0 src) ==> va_k
    va_sM (())))


val va_wpProof_AESNI_dec_last : dst:va_operand_xmm -> src:va_operand_xmm -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AESNI_dec_last dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AESNI_dec_last dst src)
    ([va_Mod_flags; va_mod_xmm dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_AESNI_dec_last dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_AESNI_dec_last (va_code_AESNI_dec_last 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_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_AESNI_dec_last (dst:va_operand_xmm) (src:va_operand_xmm) : (va_quickCode unit
  (va_code_AESNI_dec_last dst src)) =
  (va_QProc (va_code_AESNI_dec_last dst src) ([va_Mod_flags; va_mod_xmm dst]) (va_wp_AESNI_dec_last
    dst src) (va_wpProof_AESNI_dec_last dst src))
//--
//-- AESNI_imc

val va_code_AESNI_imc : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_code
[@ "opaque_to_smt"]
let va_code_AESNI_imc dst src =
  (mk_ins (make_instr (I.ins_AESNI_imc) (OReg dst) (OReg src)))

val va_codegen_success_AESNI_imc : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_AESNI_imc dst src =
  (va_ttrue ())


val va_lemma_AESNI_imc : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm -> src:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AESNI_imc dst src) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ aesni_enabled))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_xmm va_sM dst == Vale.AES.AES_s.inv_mix_columns_LE (va_eval_xmm va_s0 src) /\
    va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst va_sM
    va_s0)))))
[@"opaque_to_smt"]
let va_lemma_AESNI_imc va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_AESNI_imc) (va_code_AESNI_imc dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_AESNI_imc) (OReg dst) (OReg src))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_AESNI_imc) (OReg dst) (OReg src)))
    va_s0 in
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_AESNI_imc (dst:va_operand_xmm) (src:va_operand_xmm) (va_s0:va_state) (va_k:(va_state ->
val va_wp_AESNI_imc (dst src: va_operand_xmm) (va_s0: va_state) (va_k: (va_state -> unit -> Type0))
    : Type0

    dst: Vale.X64.Decls.va_operand_xmm ->
    src: Vale.X64.Decls.va_operand_xmm ->
    va_s0: Vale.X64.Decls.va_state ->
    va_k: (_: Vale.X64.Decls.va_state -> _: Prims.unit -> Type0)
  -> Type0