val sse_enabled:bool
let sse_enabled : bool = sse2_enabled && ssse3_enabled && sse4_1_enabled
val sse_enabled:bool
let sse_enabled:bool =
sse2_enabled && ssse3_enabled && sse4_1_enabled
Vale.X64.CPU_Features_s.fst.checked
Vale.X64.Machine_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.CPU_Features_s.fst
Prims.op_AmpAmp Vale.X64.CPU_Features_s.sse2_enabled Vale.X64.CPU_Features_s.ssse3_enabled Vale.X64.CPU_Features_s.sse4_1_enabled
module Vale.X64.CPU_Features_s

open FStar.Mul
open Vale.X64.Machine_s
open Vale.Def.Words_s

(* CPUID *)

assume val aesni_enabled : bool      // CPUID.01H:ECX.AESNI[bit 25]
assume val avx_cpuid_enabled : bool        // CPUID.01H:ECX.AVX[bit 28]
assume val pclmulqdq_enabled : bool  // CPUID.01H:ECX.PCLMULQDQ[bit 1]
assume val avx2_cpuid_enabled : bool       // CPUID.7.0.EBX[5]
assume val bmi2_enabled : bool       // CPUID.7.0.EBX[8]
assume val avx512f_enabled : bool    // CPUID.7.0.EBX[16]
assume val avx512dq_enabled : bool   // CPUID.7.0.EBX[17]
assume val adx_enabled : bool        // CPUID.7.0.EBX[19]
assume val sha_enabled : bool        // CPUID.7.0.EBX[29]
assume val avx512bw_enabled : bool   // CPUID.7.0.EBX[30]
assume val avx512vl_enabled : bool   // CPUID.7.0.EBX[31]
assume val sse2_enabled : bool       // CPUID.01H:EDX.SSE2[bit 26]
assume val ssse3_enabled : bool      // CPUID.01H:ECX.SSSE3[bit 9]
assume val sse4_1_enabled : bool     // CPUID.01H:ECX.SSE4.1[bit 19]
assume val movbe_enabled : bool      // CPUID.01H.ECX.MOVBE[bit 22]
assume val osxsave_enabled : bool    // CPUID.01H.ECX.OSXSAVE[bit 27]
assume val rdrand_enabled : bool     // CPUID.01H.ECX.RDRAND[bit 30] = 0
val sse_enabled:bool
Prims.bool