val va_quick_VPclmulqdq (dst src1 src2: va_operand_xmm) (src1Hi src2Hi: bool)
    : (va_quickCode unit (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi))
let va_quick_VPclmulqdq (dst:va_operand_xmm) (src1:va_operand_xmm) (src2:va_operand_xmm)
  (src1Hi:bool) (src2Hi:bool) : (va_quickCode unit (va_code_VPclmulqdq dst src1 src2 src1Hi
  src2Hi)) =
  (va_QProc (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi) ([va_Mod_flags; va_mod_xmm dst])
    (va_wp_VPclmulqdq dst src1 src2 src1Hi src2Hi) (va_wpProof_VPclmulqdq dst src1 src2 src1Hi
    src2Hi))
val va_quick_VPclmulqdq (dst src1 src2: va_operand_xmm) (src1Hi src2Hi: bool)
    : (va_quickCode unit (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi))
let va_quick_VPclmulqdq (dst src1 src2: va_operand_xmm) (src1Hi src2Hi: bool)
    : (va_quickCode unit (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi)) =
(va_QProc (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi)
    ([va_Mod_flags; va_mod_xmm dst])
    (va_wp_VPclmulqdq dst src1 src2 src1Hi src2Hi)
    (va_wpProof_VPclmulqdq dst src1 src2 src1Hi src2Hi))
Vale.X64.InsAes.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.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.fsti
Vale.X64.Decls.va_operand_xmm Prims.bool Vale.X64.QuickCode.va_QProc Prims.unit Vale.X64.InsAes.va_code_VPclmulqdq Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_flags Vale.X64.QuickCode.va_mod_xmm Prims.Nil Vale.X64.InsAes.va_wp_VPclmulqdq Vale.X64.InsAes.va_wpProof_VPclmulqdq Vale.X64.QuickCode.va_quickCode
module Vale.X64.InsAes
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.AES.AES_s
open Vale.Math.Poly2_s
open Vale.Math.Poly2.Bits_s
open Vale.X64.Machine_s
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.QuickCode
open Vale.X64.CPU_Features_s
//-- Pclmulqdq

val va_code_Pclmulqdq : dst:va_operand_xmm -> src:va_operand_xmm -> dstHi:bool -> srcHi:bool -> Tot
  va_code

val va_codegen_success_Pclmulqdq : dst:va_operand_xmm -> src:va_operand_xmm -> dstHi:bool ->
  srcHi:bool -> Tot va_pbool

val va_lemma_Pclmulqdq : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src:va_operand_xmm -> dstHi:bool -> srcHi:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Pclmulqdq dst src dstHi srcHi) va_s0 /\ va_is_dst_xmm
    dst va_s0 /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ pclmulqdq_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 dstHi then Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 dst) else Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 dst)))
    (Vale.Math.Poly2.Bits_s.of_double32 (if srcHi then Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 src) else Vale.Arch.Types.quad32_double_lo (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)))))
[@ va_qattr]
let va_wp_Pclmulqdq (dst:va_operand_xmm) (src:va_operand_xmm) (dstHi:bool) (srcHi:bool)
  (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 /\ pclmulqdq_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.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mul (Vale.Math.Poly2.Bits_s.of_double32
    (va_if dstHi (fun _ -> Vale.Arch.Types.quad32_double_hi (va_eval_xmm va_s0 dst)) (fun _ ->
    Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 dst)))) (Vale.Math.Poly2.Bits_s.of_double32
    (va_if srcHi (fun _ -> Vale.Arch.Types.quad32_double_hi (va_eval_xmm va_s0 src)) (fun _ ->
    Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 src))))) ==> va_k va_sM (())))

val va_wpProof_Pclmulqdq : dst:va_operand_xmm -> src:va_operand_xmm -> dstHi:bool -> srcHi:bool ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Pclmulqdq dst src dstHi srcHi va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Pclmulqdq dst src dstHi srcHi)
    ([va_Mod_flags; va_mod_xmm dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Pclmulqdq (dst:va_operand_xmm) (src:va_operand_xmm) (dstHi:bool) (srcHi:bool) :
  (va_quickCode unit (va_code_Pclmulqdq dst src dstHi srcHi)) =
  (va_QProc (va_code_Pclmulqdq dst src dstHi srcHi) ([va_Mod_flags; va_mod_xmm dst])
    (va_wp_Pclmulqdq dst src dstHi srcHi) (va_wpProof_Pclmulqdq dst src dstHi srcHi))
//--
//-- VPclmulqdq

val va_code_VPclmulqdq : dst:va_operand_xmm -> src1:va_operand_xmm -> src2:va_operand_xmm ->
  src1Hi:bool -> src2Hi:bool -> Tot va_code

val va_codegen_success_VPclmulqdq : dst:va_operand_xmm -> src1:va_operand_xmm ->
  src2:va_operand_xmm -> src1Hi:bool -> src2Hi:bool -> Tot va_pbool

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_qattr]
let va_wp_VPclmulqdq (dst:va_operand_xmm) (src1:va_operand_xmm) (src2:va_operand_xmm) (src1Hi:bool)
  (src2Hi:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (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) /\ (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.Math.Poly2.Bits_s.to_quad32
    (Vale.Math.Poly2_s.mul (Vale.Math.Poly2.Bits_s.of_double32 (va_if src1Hi (fun _ ->
    Vale.Arch.Types.quad32_double_hi (va_eval_xmm va_s0 src1)) (fun _ ->
    Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0 src1))))
    (Vale.Math.Poly2.Bits_s.of_double32 (va_if src2Hi (fun _ -> Vale.Arch.Types.quad32_double_hi
    (va_eval_xmm va_s0 src2)) (fun _ -> Vale.Arch.Types.quad32_double_lo (va_eval_xmm va_s0
    src2))))) ==> va_k va_sM (())))

val va_wpProof_VPclmulqdq : dst:va_operand_xmm -> src1:va_operand_xmm -> src2:va_operand_xmm ->
  src1Hi:bool -> src2Hi:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_VPclmulqdq dst src1 src2 src1Hi src2Hi va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_VPclmulqdq dst src1 src2 src1Hi
    src2Hi) ([va_Mod_flags; va_mod_xmm dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_VPclmulqdq (dst:va_operand_xmm) (src1:va_operand_xmm) (src2:va_operand_xmm)
  (src1Hi:bool) (src2Hi:bool) : (va_quickCode unit (va_code_VPclmulqdq dst src1 src2 src1Hi
val va_quick_VPclmulqdq (dst src1 src2: va_operand_xmm) (src1Hi src2Hi: bool)
    : (va_quickCode unit (va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi))

    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
  -> Vale.X64.QuickCode.va_quickCode Prims.unit
      (Vale.X64.InsAes.va_code_VPclmulqdq dst src1 src2 src1Hi src2Hi)