include "../../../arch/x64/Vale.X64.InsBasic.vaf"
include "../../../arch/x64/Vale.X64.InsVector.vaf"
include "../../../arch/x64/Vale.X64.InsAes.vaf"
include{:fstar}{:open} "Vale.Def.Types_s"
include{:fstar}{:open} "Vale.Arch.Types"
include{:fstar}{:open} "Vale.Math.Poly2_s"
include{:fstar}{:open} "Vale.Math.Poly2"
include{:fstar}{:open} "Vale.Math.Poly2.Bits_s"
include{:fstar}{:open} "Vale.Math.Poly2.Bits"
include{:fstar}{:open} "Vale.Math.Poly2.Words"
include{:fstar}{:open} "Vale.Math.Poly2.Lemmas"
include{:fstar}{:open} "Vale.X64.Machine_s"
include{:fstar}{:open} "Vale.X64.State"
include{:fstar}{:open} "Vale.X64.Decls"
include{:fstar}{:open} "Vale.X64.QuickCode"
include{:fstar}{:open} "Vale.X64.QuickCodes"
include{:fstar}{:open} "Vale.X64.CPU_Features_s"

module Vale.AES.X64.PolyOps

#verbatim{:interface}{:implementation}
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Math.Poly2_s
open Vale.Math.Poly2
open Vale.Math.Poly2.Bits_s
open Vale.Math.Poly2.Bits
open Vale.Math.Poly2.Lemmas
open Vale.X64.Machine_s
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsVector
open Vale.X64.InsAes
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.X64.CPU_Features_s
#endverbatim

procedure VPolyAdd(out dst:xmm, in src1:xmm, in src2:opr128)
    {:public}
    {:quick exportOnly}
    lets
        a1 := of_quad32(src1);
        a2 := of_quad32(src2);
    modifies
        efl;
    requires
        avx_enabled;
    ensures
        of_quad32(dst) == add(a1, a2);
{
    lemma_add_quad32(src1, src2);
    VPxor(dst, src1, src2);
}

procedure PolyAnd(inout dst:xmm, in src:xmm)
    {:public}
    {:quick exportOnly}
    lets
        a1 := of_quad32(dst);
        a2 := of_quad32(src);
    modifies
        efl;
    requires sse_enabled;
    ensures
        of_quad32(dst) == poly_and(a1, a2);
{
    lemma_and_quad32(dst, src);
    Pand(dst, src);
}

procedure VHigh64ToLow(out dst:xmm, in src:xmm)
    {:public}
    {:quick exportOnly}
    lets
        a := of_quad32(src);
    modifies
        efl;
    requires
        avx_enabled;
    ensures
        of_quad32(dst) == shift(a, (-64));
{
    Vpsrldq8(dst, src);
    lemma_quad32_double_shift(a);
    lemma_shift_is_div(a, 64);
    lemma_of_to_quad32(shift(a, (-64)));
}

procedure VLow64ToHigh(out dst:xmm, in src:xmm)
    {:public}
    {:quick exportOnly}
    lets
        a := of_quad32(src);
    modifies
        efl;
    requires
        avx_enabled;
    ensures
        of_quad32(dst) == shift(mask(a, 64), 64);
{
    Vpslldq8(dst, src);
    lemma_quad32_double_shift(a);
    lemma_mask_is_mod(a, 64);
    lemma_shift_is_mul(mask(a, 64), 64);
    lemma_of_to_quad32(shift(mask(a, 64), 64));
}

procedure VSwap(out dst:xmm, in src:xmm)
    {:public}
    {:quick exportOnly}
    lets
        a := of_quad32(src);
    modifies
        efl;
    requires
        avx_enabled;
    ensures
        of_quad32(dst) == swap(a, 64);
{
    VPalignr8(dst, src, src);
    lemma_quad32_double_swap(a);
    lemma_of_to_quad32(swap(a, 64));
}

procedure VPolyMul(out dst:xmm, in src1:xmm, in src2:xmm, inline src1Hi:bool, inline src2Hi:bool)
    {:public}
    {:quick exportOnly}
    lets
        a1 := of_quad32(src1);
        a2 := of_quad32(src2);
    modifies
        efl;
    requires
        pclmulqdq_enabled && avx_enabled;
    ensures
        of_quad32(dst) == mul(
            if src1Hi then shift(a1, (-64)) else mask(a1, 64),
            if src2Hi then shift(a2, (-64)) else mask(a2, 64));
{
    VPclmulqdq(dst, src1, src2, src1Hi, src2Hi);
    lemma_quad32_double(a1);
    lemma_quad32_double(a2);
    lemma_shift_is_div(a1, 64);
    lemma_shift_is_div(a2, 64);
    lemma_mask_is_mod(a1, 64);
    lemma_mask_is_mod(a2, 64);
    lemma_of_to_quad32(mul(
        if src1Hi then shift(a1, (-64)) else mask(a1, 64),
        if src2Hi then shift(a2, (-64)) else mask(a2, 64)));
}