Revision c421c49f00116ed3f19ea07913a3fa0e75a24b1c authored by Jonathan Protzenko on 15 May 2020, 15:49:05 UTC, committed by GitHub on 15 May 2020, 15:49:05 UTC
Vale.X64.CPU_Features_s.fst
module Vale.X64.CPU_Features_s
open FStar.Mul
open Vale.X64.Machine_s
open Vale.Def.Words_s
assume val aesni_enabled : bool // CPUID.01H:ECX.AESNI[bit 25]
assume val avx_enabled : bool // CPUID.01H:ECX.AVX[bit 28]
assume val pclmulqdq_enabled : bool // CPUID.01H:ECX.PCLMULQDQ[bit 1]
assume val avx2_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 rdrand_enabled : bool // CPUID.01H.ECX.RDRAND[bit 30] = 0
let sse_enabled : bool = sse2_enabled && ssse3_enabled && sse4_1_enabled
let avx512_enabled : bool =
avx512f_enabled && avx512dq_enabled && avx512bw_enabled && avx512vl_enabled
assume val cpuid (r:reg_64) (rax:nat64) (rcx:nat64) : nat64
assume val cpuid_features (u:unit) :
Lemma ((forall rcx . {:pattern (cpuid rRcx 1 rcx)} (Vale.Def.Types_s.iand (cpuid rRcx 1 rcx) (pow2_norm 25) > 0) = aesni_enabled) /\
(forall rcx . {:pattern (cpuid rRcx 1 rcx)} (Vale.Def.Types_s.iand (cpuid rRcx 1 rcx) (pow2_norm 28) > 0) = avx_enabled) /\
(forall rcx . {:pattern (cpuid rRcx 1 rcx)} (Vale.Def.Types_s.iand (cpuid rRcx 1 rcx) (pow2_norm 1) > 0) = pclmulqdq_enabled) /\
(forall rcx . {:pattern (cpuid rRdx 1 rcx)} (Vale.Def.Types_s.iand (cpuid rRdx 1 rcx) (pow2_norm 26) > 0) = sse2_enabled) /\
(forall rcx . {:pattern (cpuid rRcx 1 rcx)} (Vale.Def.Types_s.iand (cpuid rRcx 1 rcx) (pow2_norm 9) > 0) = ssse3_enabled) /\
(forall rcx . {:pattern (cpuid rRcx 1 rcx)} (Vale.Def.Types_s.iand (cpuid rRcx 1 rcx) (pow2_norm 19) > 0) = sse4_1_enabled) /\
(forall rcx . {:pattern (cpuid rRcx 1 rcx)} (Vale.Def.Types_s.iand (cpuid rRcx 1 rcx) (pow2_norm 22) > 0) = movbe_enabled) /\
(forall rcx . {:pattern (cpuid rRcx 1 rcx)} (Vale.Def.Types_s.iand (cpuid rRcx 1 rcx) (pow2_norm 30) > 0) = rdrand_enabled) /\
(Vale.Def.Types_s.iand (cpuid rRbx 7 0) (pow2_norm 5) > 0) = avx2_enabled /\
(Vale.Def.Types_s.iand (cpuid rRbx 7 0) (pow2_norm 8) > 0) = bmi2_enabled /\
(Vale.Def.Types_s.iand (cpuid rRbx 7 0) (pow2_norm 16) > 0) = avx512f_enabled /\
(Vale.Def.Types_s.iand (cpuid rRbx 7 0) (pow2_norm 17) > 0) = avx512dq_enabled /\
(Vale.Def.Types_s.iand (cpuid rRbx 7 0) (pow2_norm 19) > 0) = adx_enabled /\
(Vale.Def.Types_s.iand (cpuid rRbx 7 0) (pow2_norm 29) > 0) = sha_enabled /\
(Vale.Def.Types_s.iand (cpuid rRbx 7 0) (pow2_norm 30) > 0) = avx512bw_enabled /\
(Vale.Def.Types_s.iand (cpuid rRbx 7 0) (pow2_norm 31) > 0) = avx512vl_enabled
)
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...