val va_codegen_success_Pclmulqdq : dst:va_operand_xmm -> src:va_operand_xmm -> dstHi:bool ->
  srcHi:bool -> Tot va_pbool
let va_codegen_success_Pclmulqdq dst src dstHi srcHi =
  (va_ttrue ())
val va_codegen_success_Pclmulqdq : dst:va_operand_xmm -> src:va_operand_xmm -> dstHi:bool ->
  srcHi:bool -> Tot va_pbool
let va_codegen_success_Pclmulqdq dst src dstHi srcHi =
(va_ttrue ())
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 Prims.bool Vale.X64.Decls.va_ttrue Vale.X64.Decls.va_pbool
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"]
val va_codegen_success_Pclmulqdq : dst:va_operand_xmm -> src:va_operand_xmm -> dstHi:bool ->
  srcHi:bool -> Tot va_pbool

    dst: Vale.X64.Decls.va_operand_xmm ->
    src: Vale.X64.Decls.va_operand_xmm ->
    dstHi: Prims.bool ->
    srcHi: Prims.bool
  -> Vale.X64.Decls.va_pbool