include "../../../../arch/x64/Vale.X64.InsBasic.vaf"
include "../../../../arch/x64/Vale.X64.InsMem.vaf"
include "../../../../arch/x64/Vale.X64.InsVector.vaf"
include{:fstar}{:open} "Vale.Arch.TypesNative"
include{:fstar}{:open} "Vale.Lib.Meta"
include "../Vale.Lib.X64.Cpuid.vaf"

module Vale.Lib.X64.Cpuidstdcall

#verbatim{:interface}{:implementation}
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.X64.CPU_Features_s

#endverbatim

#verbatim{:implementation}
open Vale.Lib.Meta
open Vale.Lib.X64.Cpuid
#endverbatim

procedure Check_aesni_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    reads
        mem; heap0;
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> aesni_enabled && pclmulqdq_enabled;
        rbx == old(rbx);
{
    Check_aesni_support();
}


procedure Check_sha_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> sha_enabled;
        rbx == old(rbx);
{
    Check_sha_support();
}

procedure Check_adx_bmi2_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> adx_enabled && bmi2_enabled;
        rbx == old(rbx);
{
    Check_adx_bmi2_support();
}

procedure Check_avx_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> avx_cpuid_enabled;
        rbx == old(rbx);
{
    Check_avx_support();
}

procedure Check_avx2_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> avx2_cpuid_enabled;
        rbx == old(rbx);
{
    Check_avx2_support();
}

procedure Check_movbe_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> movbe_enabled;
        rbx == old(rbx);
{
    Check_movbe_support();
}

procedure Check_sse_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> sse_enabled;
        rbx == old(rbx);
{
    Check_sse_support();
}

procedure Check_rdrand_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> rdrand_enabled;
        rbx == old(rbx);
{
    Check_rdrand_support();
}

procedure Check_avx512_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; r10; r11; efl;
    ensures
        rax != 0 ==> avx512_cpuid_enabled;
        rbx == old(rbx);
{
    Check_avx512_support();
}

procedure Check_osxsave_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rbx; rcx; rdx; r9; efl;
    ensures
        rax != 0 ==> osxsave_enabled;
        rbx == old(rbx);
{
    Check_osxsave_support();
}

procedure Check_avx_xcr0_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rcx; rdx; efl;
    requires
        osxsave_enabled;
    ensures
        rax != 0 ==> avx_xcr0;
{
    Check_avx_xcr0_support();
}

procedure Check_avx512_xcr0_stdcall(inline win:bool)
    {:public}
    {:quick}
    {:exportSpecs}
    modifies
        rax; rcx; rdx; efl;
    requires
        osxsave_enabled;
        avx_xcr0;
    ensures
        rax != 0 ==> avx512_xcr0;
{
    Check_avx512_xcr0_support();
}