diff --git a/dev/x86_64/src/ntt.S b/dev/x86_64/src/ntt.S index 090088148..e3af60f42 100644 --- a/dev/x86_64/src/ntt.S +++ b/dev/x86_64/src/ntt.S @@ -81,8 +81,33 @@ vpblendd $0xAA,%ymm12,%ymm\h,%ymm\h /* mulhi(h, zh) */ */ vpsubd %ymm\h,%ymm\l,%ymm12 /* l - mulhi(h, zh) * = h' - mulhi(q, mullo(h, zl)) */ -vpaddd %ymm\h,%ymm\l,%ymm\l /* l + mulhi(h, zh) +/* + * VEX Encoding Optimization for Platform-Independent Code + * + * Some assemblers (notably clang) will automatically swap operands of + * commutative instructions like VPADDD to use shorter encodings, while others + * (like gcc) may not. This causes different machine code across platforms. + * + * VEX prefixes come in two forms: + * - 2-byte VEX (0xC5): Can only be used when the ModR/M.rm operand is ymm0-7 + * - 3-byte VEX (0xC4): Required when ModR/M.rm operand is ymm8-15 + * + * When one operand is in ymm0-7 and another is in ymm8-15, we explicitly + * place the lower-numbered register (ymm0-7) as the second source operand + * to enable the 2-byte VEX encoding. Since VPADDD is commutative, this + * produces identical results while ensuring consistent machine code across + * different assemblers. + * + * Example: + * VPADDD ymm4, ymm4, ymm8 -> 3-byte VEX (0xC4 0xC1 0x5D 0xFE 0xE0) + * VPADDD ymm4, ymm8, ymm4 -> 2-byte VEX (0xC5 0xBD 0xFE 0xE4) ✓ preferred + */ +.if (\l < 8) && (\h >= 8) +vpaddd %ymm\l,%ymm\h,%ymm\l /* l + mulhi(h, zh) * = l' + mulhi(q, mullo(h, zl)) */ +.else +vpaddd %ymm\h,%ymm\l,%ymm\l +.endif vmovshdup %ymm13,%ymm13 vpblendd $0xAA,%ymm14,%ymm13,%ymm13 /* mulhi(q, mullo(h, zl)) */ diff --git a/mldsa/src/native/x86_64/src/ntt.S b/mldsa/src/native/x86_64/src/ntt.S index afecb10de..39c78f94a 100644 --- a/mldsa/src/native/x86_64/src/ntt.S +++ b/mldsa/src/native/x86_64/src/ntt.S @@ -55,7 +55,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -70,7 +70,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -85,7 +85,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -100,7 +100,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -197,7 +197,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -212,7 +212,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -227,7 +227,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -242,7 +242,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -339,7 +339,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -354,7 +354,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -369,7 +369,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -384,7 +384,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -481,7 +481,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -496,7 +496,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -511,7 +511,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -526,7 +526,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -623,7 +623,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -638,7 +638,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -653,7 +653,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -668,7 +668,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -763,7 +763,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm7, %ymm12 - vpaddd %ymm8, %ymm7, %ymm7 + vpaddd %ymm7, %ymm8, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -888,7 +888,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm6, %ymm12 - vpaddd %ymm11, %ymm6, %ymm6 + vpaddd %ymm6, %ymm11, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -956,7 +956,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm4, %ymm12 - vpaddd %ymm11, %ymm4, %ymm4 + vpaddd %ymm4, %ymm11, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1032,7 +1032,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm3, %ymm12 - vpaddd %ymm11, %ymm3, %ymm3 + vpaddd %ymm3, %ymm11, %ymm3 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1065,7 +1065,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1080,7 +1080,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -1095,7 +1095,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -1110,7 +1110,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1205,7 +1205,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm7, %ymm12 - vpaddd %ymm8, %ymm7, %ymm7 + vpaddd %ymm7, %ymm8, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1330,7 +1330,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm6, %ymm12 - vpaddd %ymm11, %ymm6, %ymm6 + vpaddd %ymm6, %ymm11, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1398,7 +1398,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm4, %ymm12 - vpaddd %ymm11, %ymm4, %ymm4 + vpaddd %ymm4, %ymm11, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1474,7 +1474,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm3, %ymm12 - vpaddd %ymm11, %ymm3, %ymm3 + vpaddd %ymm3, %ymm11, %ymm3 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1507,7 +1507,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1522,7 +1522,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -1537,7 +1537,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -1552,7 +1552,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1647,7 +1647,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm7, %ymm12 - vpaddd %ymm8, %ymm7, %ymm7 + vpaddd %ymm7, %ymm8, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1772,7 +1772,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm6, %ymm12 - vpaddd %ymm11, %ymm6, %ymm6 + vpaddd %ymm6, %ymm11, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1840,7 +1840,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm4, %ymm12 - vpaddd %ymm11, %ymm4, %ymm4 + vpaddd %ymm4, %ymm11, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1916,7 +1916,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm3, %ymm12 - vpaddd %ymm11, %ymm3, %ymm3 + vpaddd %ymm3, %ymm11, %ymm3 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1949,7 +1949,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1964,7 +1964,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -1979,7 +1979,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -1994,7 +1994,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -2089,7 +2089,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm7, %ymm12 - vpaddd %ymm8, %ymm7, %ymm7 + vpaddd %ymm7, %ymm8, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -2214,7 +2214,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm6, %ymm12 - vpaddd %ymm11, %ymm6, %ymm6 + vpaddd %ymm6, %ymm11, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -2282,7 +2282,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm4, %ymm12 - vpaddd %ymm11, %ymm4, %ymm4 + vpaddd %ymm4, %ymm11, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -2358,7 +2358,7 @@ MLD_ASM_FN_SYMBOL(ntt_avx2) vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm3, %ymm12 - vpaddd %ymm11, %ymm3, %ymm3 + vpaddd %ymm3, %ymm11, %ymm3 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 diff --git a/proofs/hol_light/x86_64/mldsa/mldsa_ntt.S b/proofs/hol_light/x86_64/mldsa/mldsa_ntt.S index 7f2862b56..d2b1cd57c 100644 --- a/proofs/hol_light/x86_64/mldsa/mldsa_ntt.S +++ b/proofs/hol_light/x86_64/mldsa/mldsa_ntt.S @@ -58,7 +58,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -73,7 +73,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -88,7 +88,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -103,7 +103,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -200,7 +200,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -215,7 +215,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -230,7 +230,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -245,7 +245,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -342,7 +342,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -357,7 +357,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -372,7 +372,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -387,7 +387,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -484,7 +484,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -499,7 +499,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -514,7 +514,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -529,7 +529,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -626,7 +626,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -641,7 +641,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -656,7 +656,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -671,7 +671,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -766,7 +766,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm7, %ymm12 - vpaddd %ymm8, %ymm7, %ymm7 + vpaddd %ymm7, %ymm8, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -891,7 +891,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm6, %ymm12 - vpaddd %ymm11, %ymm6, %ymm6 + vpaddd %ymm6, %ymm11, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -959,7 +959,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm4, %ymm12 - vpaddd %ymm11, %ymm4, %ymm4 + vpaddd %ymm4, %ymm11, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1035,7 +1035,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm3, %ymm12 - vpaddd %ymm11, %ymm3, %ymm3 + vpaddd %ymm3, %ymm11, %ymm3 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1068,7 +1068,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1083,7 +1083,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -1098,7 +1098,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -1113,7 +1113,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1208,7 +1208,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm7, %ymm12 - vpaddd %ymm8, %ymm7, %ymm7 + vpaddd %ymm7, %ymm8, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1333,7 +1333,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm6, %ymm12 - vpaddd %ymm11, %ymm6, %ymm6 + vpaddd %ymm6, %ymm11, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1401,7 +1401,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm4, %ymm12 - vpaddd %ymm11, %ymm4, %ymm4 + vpaddd %ymm4, %ymm11, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1477,7 +1477,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm3, %ymm12 - vpaddd %ymm11, %ymm3, %ymm3 + vpaddd %ymm3, %ymm11, %ymm3 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1510,7 +1510,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1525,7 +1525,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -1540,7 +1540,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -1555,7 +1555,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1650,7 +1650,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm7, %ymm12 - vpaddd %ymm8, %ymm7, %ymm7 + vpaddd %ymm7, %ymm8, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1775,7 +1775,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm6, %ymm12 - vpaddd %ymm11, %ymm6, %ymm6 + vpaddd %ymm6, %ymm11, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1843,7 +1843,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm4, %ymm12 - vpaddd %ymm11, %ymm4, %ymm4 + vpaddd %ymm4, %ymm11, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1919,7 +1919,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm3, %ymm12 - vpaddd %ymm11, %ymm3, %ymm3 + vpaddd %ymm3, %ymm11, %ymm3 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -1952,7 +1952,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm4, %ymm12 - vpaddd %ymm8, %ymm4, %ymm4 + vpaddd %ymm4, %ymm8, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -1967,7 +1967,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm9, %ymm9 # ymm9 = ymm9[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm9, %ymm9 # ymm9 = ymm9[0],ymm12[1],ymm9[2],ymm12[3],ymm9[4],ymm12[5],ymm9[6],ymm12[7] vpsubd %ymm9, %ymm5, %ymm12 - vpaddd %ymm9, %ymm5, %ymm5 + vpaddd %ymm5, %ymm9, %ymm5 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm9 @@ -1982,7 +1982,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm10, %ymm10 # ymm10 = ymm10[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm10, %ymm10 # ymm10 = ymm10[0],ymm12[1],ymm10[2],ymm12[3],ymm10[4],ymm12[5],ymm10[6],ymm12[7] vpsubd %ymm10, %ymm6, %ymm12 - vpaddd %ymm10, %ymm6, %ymm6 + vpaddd %ymm6, %ymm10, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm10 @@ -1997,7 +1997,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm7, %ymm12 - vpaddd %ymm11, %ymm7, %ymm7 + vpaddd %ymm7, %ymm11, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -2092,7 +2092,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm8, %ymm8 # ymm8 = ymm8[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm8, %ymm8 # ymm8 = ymm8[0],ymm12[1],ymm8[2],ymm12[3],ymm8[4],ymm12[5],ymm8[6],ymm12[7] vpsubd %ymm8, %ymm7, %ymm12 - vpaddd %ymm8, %ymm7, %ymm7 + vpaddd %ymm7, %ymm8, %ymm7 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm8 @@ -2217,7 +2217,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm6, %ymm12 - vpaddd %ymm11, %ymm6, %ymm6 + vpaddd %ymm6, %ymm11, %ymm6 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -2285,7 +2285,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm4, %ymm12 - vpaddd %ymm11, %ymm4, %ymm4 + vpaddd %ymm4, %ymm11, %ymm4 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 @@ -2361,7 +2361,7 @@ PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2: vmovshdup %ymm11, %ymm11 # ymm11 = ymm11[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm12, %ymm11, %ymm11 # ymm11 = ymm11[0],ymm12[1],ymm11[2],ymm12[3],ymm11[4],ymm12[5],ymm11[6],ymm12[7] vpsubd %ymm11, %ymm3, %ymm12 - vpaddd %ymm11, %ymm3, %ymm3 + vpaddd %ymm3, %ymm11, %ymm3 vmovshdup %ymm13, %ymm13 # ymm13 = ymm13[1,1,3,3,5,5,7,7] vpblendd $0xaa, %ymm14, %ymm13, %ymm13 # ymm13 = ymm13[0],ymm14[1],ymm13[2],ymm14[3],ymm13[4],ymm14[5],ymm13[6],ymm14[7] vpaddd %ymm13, %ymm12, %ymm11 diff --git a/proofs/hol_light/x86_64/proofs/mldsa_ntt.ml b/proofs/hol_light/x86_64/proofs/mldsa_ntt.ml index f5891e7de..515932354 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_ntt.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_ntt.ml @@ -58,8 +58,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm8) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe0; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm8) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -88,8 +87,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm9) (%_% ymm9) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x55; 0xfa; 0xe1; (* VPSUBD (%_% ymm12) (%_% ymm5) (%_% ymm9) *) - 0xc4; 0xc1; 0x55; 0xfe; 0xe9; - (* VPADDD (%_% ymm5) (%_% ymm5) (%_% ymm9) *) + 0xc5; 0xb5; 0xfe; 0xed; (* VPADDD (%_% ymm5) (%_% ymm9) (%_% ymm5) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -118,8 +116,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm10) (%_% ymm10) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe2; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm10) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf2; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm10) *) + 0xc5; 0xad; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm10) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -148,8 +145,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm11) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xfb; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm11) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -333,8 +329,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm8) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe0; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm8) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -363,8 +358,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm9) (%_% ymm9) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x55; 0xfa; 0xe1; (* VPSUBD (%_% ymm12) (%_% ymm5) (%_% ymm9) *) - 0xc4; 0xc1; 0x55; 0xfe; 0xe9; - (* VPADDD (%_% ymm5) (%_% ymm5) (%_% ymm9) *) + 0xc5; 0xb5; 0xfe; 0xed; (* VPADDD (%_% ymm5) (%_% ymm9) (%_% ymm5) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -393,8 +387,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm10) (%_% ymm10) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe2; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm10) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf2; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm10) *) + 0xc5; 0xad; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm10) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -423,8 +416,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm11) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xfb; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm11) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -609,8 +601,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm8) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe0; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm8) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -639,8 +630,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm9) (%_% ymm9) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x55; 0xfa; 0xe1; (* VPSUBD (%_% ymm12) (%_% ymm5) (%_% ymm9) *) - 0xc4; 0xc1; 0x55; 0xfe; 0xe9; - (* VPADDD (%_% ymm5) (%_% ymm5) (%_% ymm9) *) + 0xc5; 0xb5; 0xfe; 0xed; (* VPADDD (%_% ymm5) (%_% ymm9) (%_% ymm5) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -669,8 +659,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm10) (%_% ymm10) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe2; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm10) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf2; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm10) *) + 0xc5; 0xad; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm10) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -699,8 +688,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm11) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xfb; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm11) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -885,8 +873,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm8) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe0; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm8) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -915,8 +902,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm9) (%_% ymm9) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x55; 0xfa; 0xe1; (* VPSUBD (%_% ymm12) (%_% ymm5) (%_% ymm9) *) - 0xc4; 0xc1; 0x55; 0xfe; 0xe9; - (* VPADDD (%_% ymm5) (%_% ymm5) (%_% ymm9) *) + 0xc5; 0xb5; 0xfe; 0xed; (* VPADDD (%_% ymm5) (%_% ymm9) (%_% ymm5) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -945,8 +931,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm10) (%_% ymm10) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe2; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm10) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf2; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm10) *) + 0xc5; 0xad; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm10) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -975,8 +960,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm11) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xfb; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm11) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1160,8 +1144,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm8) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe0; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm8) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1190,8 +1173,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm9) (%_% ymm9) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x55; 0xfa; 0xe1; (* VPSUBD (%_% ymm12) (%_% ymm5) (%_% ymm9) *) - 0xc4; 0xc1; 0x55; 0xfe; 0xe9; - (* VPADDD (%_% ymm5) (%_% ymm5) (%_% ymm9) *) + 0xc5; 0xb5; 0xfe; 0xed; (* VPADDD (%_% ymm5) (%_% ymm9) (%_% ymm5) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1220,8 +1202,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm10) (%_% ymm10) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe2; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm10) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf2; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm10) *) + 0xc5; 0xad; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm10) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1250,8 +1231,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm11) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xfb; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm11) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1428,8 +1408,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm8) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xf8; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm8) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1655,8 +1634,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm11) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf3; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm11) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1777,8 +1755,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm11) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe3; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm11) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1917,8 +1894,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x65; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm3) (%_% ymm11) *) - 0xc4; 0xc1; 0x65; 0xfe; 0xdb; - (* VPADDD (%_% ymm3) (%_% ymm3) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xdb; (* VPADDD (%_% ymm3) (%_% ymm11) (%_% ymm3) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -1982,8 +1958,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm8) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe0; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm8) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2012,8 +1987,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm9) (%_% ymm9) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x55; 0xfa; 0xe1; (* VPSUBD (%_% ymm12) (%_% ymm5) (%_% ymm9) *) - 0xc4; 0xc1; 0x55; 0xfe; 0xe9; - (* VPADDD (%_% ymm5) (%_% ymm5) (%_% ymm9) *) + 0xc5; 0xb5; 0xfe; 0xed; (* VPADDD (%_% ymm5) (%_% ymm9) (%_% ymm5) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2042,8 +2016,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm10) (%_% ymm10) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe2; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm10) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf2; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm10) *) + 0xc5; 0xad; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm10) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2072,8 +2045,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm11) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xfb; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm11) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2250,8 +2222,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm8) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xf8; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm8) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2477,8 +2448,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm11) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf3; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm11) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2599,8 +2569,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm11) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe3; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm11) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2739,8 +2708,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x65; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm3) (%_% ymm11) *) - 0xc4; 0xc1; 0x65; 0xfe; 0xdb; - (* VPADDD (%_% ymm3) (%_% ymm3) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xdb; (* VPADDD (%_% ymm3) (%_% ymm11) (%_% ymm3) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2805,8 +2773,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm8) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe0; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm8) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2835,8 +2802,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm9) (%_% ymm9) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x55; 0xfa; 0xe1; (* VPSUBD (%_% ymm12) (%_% ymm5) (%_% ymm9) *) - 0xc4; 0xc1; 0x55; 0xfe; 0xe9; - (* VPADDD (%_% ymm5) (%_% ymm5) (%_% ymm9) *) + 0xc5; 0xb5; 0xfe; 0xed; (* VPADDD (%_% ymm5) (%_% ymm9) (%_% ymm5) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2865,8 +2831,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm10) (%_% ymm10) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe2; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm10) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf2; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm10) *) + 0xc5; 0xad; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm10) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -2895,8 +2860,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm11) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xfb; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm11) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3073,8 +3037,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm8) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xf8; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm8) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3300,8 +3263,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm11) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf3; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm11) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3422,8 +3384,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm11) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe3; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm11) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3562,8 +3523,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x65; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm3) (%_% ymm11) *) - 0xc4; 0xc1; 0x65; 0xfe; 0xdb; - (* VPADDD (%_% ymm3) (%_% ymm3) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xdb; (* VPADDD (%_% ymm3) (%_% ymm11) (%_% ymm3) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3628,8 +3588,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm8) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe0; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm8) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3658,8 +3617,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm9) (%_% ymm9) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x55; 0xfa; 0xe1; (* VPSUBD (%_% ymm12) (%_% ymm5) (%_% ymm9) *) - 0xc4; 0xc1; 0x55; 0xfe; 0xe9; - (* VPADDD (%_% ymm5) (%_% ymm5) (%_% ymm9) *) + 0xc5; 0xb5; 0xfe; 0xed; (* VPADDD (%_% ymm5) (%_% ymm9) (%_% ymm5) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3688,8 +3646,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm10) (%_% ymm10) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe2; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm10) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf2; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm10) *) + 0xc5; 0xad; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm10) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3718,8 +3675,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm11) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xfb; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm11) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -3896,8 +3852,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm8) (%_% ymm8) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x45; 0xfa; 0xe0; (* VPSUBD (%_% ymm12) (%_% ymm7) (%_% ymm8) *) - 0xc4; 0xc1; 0x45; 0xfe; 0xf8; - (* VPADDD (%_% ymm7) (%_% ymm7) (%_% ymm8) *) + 0xc5; 0xbd; 0xfe; 0xff; (* VPADDD (%_% ymm7) (%_% ymm8) (%_% ymm7) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -4123,8 +4078,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x4d; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm6) (%_% ymm11) *) - 0xc4; 0xc1; 0x4d; 0xfe; 0xf3; - (* VPADDD (%_% ymm6) (%_% ymm6) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xf6; (* VPADDD (%_% ymm6) (%_% ymm11) (%_% ymm6) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -4245,8 +4199,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x5d; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm4) (%_% ymm11) *) - 0xc4; 0xc1; 0x5d; 0xfe; 0xe3; - (* VPADDD (%_% ymm4) (%_% ymm4) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xe4; (* VPADDD (%_% ymm4) (%_% ymm11) (%_% ymm4) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -4385,8 +4338,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o" (* VPBLENDD (%_% ymm11) (%_% ymm11) (%_% ymm12) (Imm8 (word 170)) *) 0xc4; 0x41; 0x65; 0xfa; 0xe3; (* VPSUBD (%_% ymm12) (%_% ymm3) (%_% ymm11) *) - 0xc4; 0xc1; 0x65; 0xfe; 0xdb; - (* VPADDD (%_% ymm3) (%_% ymm3) (%_% ymm11) *) + 0xc5; 0xa5; 0xfe; 0xdb; (* VPADDD (%_% ymm3) (%_% ymm11) (%_% ymm3) *) 0xc4; 0x41; 0x7e; 0x16; 0xed; (* VMOVSHDUP (%_% ymm13) (%_% ymm13) *) 0xc4; 0x43; 0x15; 0x02; 0xee; 0xaa; @@ -4523,8 +4475,8 @@ let MLDSA_NTT_CORRECT = prove (`!a zetas (zetas_list:int32 list) x pc. aligned 32 a /\ aligned 32 zetas /\ - nonoverlapping (word pc,0x3079) (a, 1024) /\ - nonoverlapping (word pc,0x3079) (zetas, 2496) /\ + nonoverlapping (word pc,0x3049) (a, 1024) /\ + nonoverlapping (word pc,0x3049) (zetas, 2496) /\ nonoverlapping (a, 1024) (zetas, 2496) ==> ensures x86 (\s. bytes_loaded s (word pc) (BUTLAST mldsa_ntt_tmc) /\ @@ -4535,7 +4487,7 @@ let MLDSA_NTT_CORRECT = prove !i. i < 256 ==> read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) - (\s. read RIP s = word(pc + 0x3078) /\ + (\s. read RIP s = word(pc + 0x3048) /\ (!i. i < 256 ==> let zi = read(memory :> bytes32(word_add a (word(4 * i)))) s in