val va_lemma_VPclmulqdq : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src1:va_operand_xmm -> src2:va_operand_xmm -> src1Hi:bool -> src2Hi:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi) va_s0 /\
    va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src1 va_s0 /\ va_is_src_xmm src2 va_s0 /\ va_get_ok
    va_s0 /\ (pclmulqdq_enabled /\ avx_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.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2.Bits_s.of_double32 (if src1Hi then Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 src1) else Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 src1)))
    (Vale.Math.Poly2.Bits_s.of_double32 (if src2Hi then Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 src2) else Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 src2)))) /\
    va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst va_sM
    va_s0)))))
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)
val va_lemma_VPclmulqdq : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src1:va_operand_xmm -> src2:va_operand_xmm -> src1Hi:bool -> src2Hi:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi) va_s0 /\
    va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src1 va_s0 /\ va_is_src_xmm src2 va_s0 /\ va_get_ok
    va_s0 /\ (pclmulqdq_enabled /\ avx_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.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2.Bits_s.of_double32 (if src1Hi then Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 src1) else Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 src1)))
    (Vale.Math.Poly2.Bits_s.of_double32 (if src2Hi then Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 src2) else Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 src2)))) /\
    va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst va_sM
    va_s0)))))
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)
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_code Vale.X64.Decls.va_state Vale.X64.Decls.va_operand_xmm Prims.bool 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.opXmm Prims.Nil Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.PreserveFlags Vale.X64.Instructions_s.ins_VPclmulqdq Prims.op_Addition Prims.int Vale.X64.Machine_s.OReg Vale.X64.Machine_s.quad32 Vale.X64.Machine_s.reg_xmm Prims.unit Vale.X64.Decls.va_ins_lemma Vale.X64.Decls.va_reveal_opaque Vale.X64.InsAes.va_code_VPclmulqdq
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"]
val va_lemma_VPclmulqdq : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src1:va_operand_xmm -> src2:va_operand_xmm -> src1Hi:bool -> src2Hi:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi) va_s0 /\
    va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src1 va_s0 /\ va_is_src_xmm src2 va_s0 /\ va_get_ok
    va_s0 /\ (pclmulqdq_enabled /\ avx_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.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2.Bits_s.of_double32 (if src1Hi then Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 src1) else Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 src1)))
    (Vale.Math.Poly2.Bits_s.of_double32 (if src2Hi then Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 src2) else Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 src2)))) /\
    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_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    dst: Vale.X64.Decls.va_operand_xmm ->
    src1: Vale.X64.Decls.va_operand_xmm ->
    src2: Vale.X64.Decls.va_operand_xmm ->
    src1Hi: Prims.bool ->
    src2Hi: Prims.bool
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)