x86_64: Consolidate AVX2 kernel doc into the YAML header

poly_caddq, poly_chknorm and polyz_unpack_{17,19} each carried a prose
Name/Description/Arguments comment block in addition to the /*yaml*/ ABI
header, duplicating the same information. Fold the descriptive text into a
multi-line YAML Description field and drop the prose block, so the YAML
header is the single source of truth, matching the convention used by the
aarch64 kernels and the poly_decompose/poly_use_hint AVX2 routines.

Comment-only change: the generated shipped and HOL-Light proof assembly is
byte-identical (verified via objdump), so no proof bytecode changes.

Signed-off-by: Jake Massimo <jakemas@amazon.com>

Author: jakemas

dev/x86_64/src/poly_caddq_avx2_asm.S

@@ -18,18 +18,11 @@
  */
 
 
-/*************************************************
- * Name:        mld_poly_caddq_avx2_asm
- *
- * Description: For all coefficients of in/out polynomial add Q if
- *              coefficient is negative.
- *
- * Arguments:   - int32_t *r: pointer to input/output polynomial
- **************************************************/
-
 /*yaml
   Name: poly_caddq_avx2_asm
-  Description: x86_64 AVX2 conditional addition of q to each coefficient
+  Description: x86_64 AVX2 conditional addition of q to each coefficient.
+    For all coefficients of the in/out polynomial, add Q if the coefficient
+    is negative.
   Signature: void mld_poly_caddq_avx2_asm(int32_t *r)
   ABI:
     Architecture: x86_64

dev/x86_64/src/poly_chknorm_avx2_asm.S

@@ -18,22 +18,12 @@
  */
 
 
-/*************************************************
- * Name:        mld_poly_chknorm_avx2_asm
- *
- * Description: Check infinity norm of polynomial against given bound.
- *              Returns 0 if norm is strictly smaller than B; otherwise
- *              returns 1.
- *
- * Arguments:   - const int32_t *a: pointer to input polynomial
- *              - int32_t B:  bound
- *
- * Returns:     - 1 if any |coefficient| >= B, 0 otherwise.
- **************************************************/
-
 /*yaml
   Name: poly_chknorm_avx2_asm
-  Description: x86_64 AVX2 infinity-norm bound check on polynomial coefficients
+  Description: x86_64 AVX2 infinity-norm bound check on polynomial coefficients.
+    Check the infinity norm of the polynomial against the given bound B.
+    Returns 0 if the norm is strictly smaller than B; otherwise returns 1
+    (i.e. returns 1 if any |coefficient| >= B, 0 otherwise).
   Signature: int mld_poly_chknorm_avx2_asm(const int32_t *a, int32_t B)
   ABI:
     Architecture: x86_64

dev/x86_64/src/polyz_unpack_17_avx2_asm.S

@@ -18,20 +18,11 @@
  */
 
 
-/*************************************************
- * Name:        mld_polyz_unpack_17_avx2_asm
- *
- * Description: Unpack polynomial z with 18-bit packed coefficients
- *              (GAMMA1 = 2^17). Maps packed [0, 2^18-1] to signed
- *              [-(2^17-1), 2^17] via GAMMA1 - x.
- *
- * Arguments:   - int32_t *r:       pointer to output polynomial (1024 bytes)
- *              - const uint8_t *a: pointer to packed input (576 bytes)
- **************************************************/
-
 /*yaml
   Name: polyz_unpack_17_avx2_asm
-  Description: x86_64 AVX2 unpacking of 17-bit packed coefficients
+  Description: x86_64 AVX2 unpacking of 17-bit packed coefficients.
+    Unpack polynomial z with 18-bit packed coefficients (GAMMA1 = 2^17),
+    mapping packed [0, 2^18-1] to signed [-(2^17-1), 2^17] via GAMMA1 - x.
   Signature: void mld_polyz_unpack_17_avx2_asm(int32_t *r, const uint8_t *a)
   ABI:
     Architecture: x86_64

dev/x86_64/src/polyz_unpack_19_avx2_asm.S

@@ -18,20 +18,11 @@
  */
 
 
-/*************************************************
- * Name:        mld_polyz_unpack_19_avx2_asm
- *
- * Description: Unpack polynomial z with 20-bit packed coefficients
- *              (GAMMA1 = 2^19). Maps packed [0, 2^20-1] to signed
- *              [-(2^19-1), 2^19] via GAMMA1 - x.
- *
- * Arguments:   - int32_t *r:       pointer to output polynomial (1024 bytes)
- *              - const uint8_t *a: pointer to packed input (640 bytes)
- **************************************************/
-
 /*yaml
   Name: polyz_unpack_19_avx2_asm
-  Description: x86_64 AVX2 unpacking of 19-bit packed coefficients
+  Description: x86_64 AVX2 unpacking of 19-bit packed coefficients.
+    Unpack polynomial z with 20-bit packed coefficients (GAMMA1 = 2^19),
+    mapping packed [0, 2^20-1] to signed [-(2^19-1), 2^19] via GAMMA1 - x.
   Signature: void mld_polyz_unpack_19_avx2_asm(int32_t *r, const uint8_t *a)
   ABI:
     Architecture: x86_64

mldsa/src/native/x86_64/src/poly_caddq_avx2_asm.S

@@ -18,18 +18,11 @@
  */
 
 
-/*************************************************
- * Name:        mld_poly_caddq_avx2_asm
- *
- * Description: For all coefficients of in/out polynomial add Q if
- *              coefficient is negative.
- *
- * Arguments:   - int32_t *r: pointer to input/output polynomial
- **************************************************/
-
 /*yaml
   Name: poly_caddq_avx2_asm
-  Description: x86_64 AVX2 conditional addition of q to each coefficient
+  Description: x86_64 AVX2 conditional addition of q to each coefficient.
+    For all coefficients of the in/out polynomial, add Q if the coefficient
+    is negative.
   Signature: void mld_poly_caddq_avx2_asm(int32_t *r)
   ABI:
     Architecture: x86_64

mldsa/src/native/x86_64/src/poly_chknorm_avx2_asm.S

@@ -18,22 +18,12 @@
  */
 
 
-/*************************************************
- * Name:        mld_poly_chknorm_avx2_asm
- *
- * Description: Check infinity norm of polynomial against given bound.
- *              Returns 0 if norm is strictly smaller than B; otherwise
- *              returns 1.
- *
- * Arguments:   - const int32_t *a: pointer to input polynomial
- *              - int32_t B:  bound
- *
- * Returns:     - 1 if any |coefficient| >= B, 0 otherwise.
- **************************************************/
-
 /*yaml
   Name: poly_chknorm_avx2_asm
-  Description: x86_64 AVX2 infinity-norm bound check on polynomial coefficients
+  Description: x86_64 AVX2 infinity-norm bound check on polynomial coefficients.
+    Check the infinity norm of the polynomial against the given bound B.
+    Returns 0 if the norm is strictly smaller than B; otherwise returns 1
+    (i.e. returns 1 if any |coefficient| >= B, 0 otherwise).
   Signature: int mld_poly_chknorm_avx2_asm(const int32_t *a, int32_t B)
   ABI:
     Architecture: x86_64

mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S

@@ -18,20 +18,11 @@
  */
 
 
-/*************************************************
- * Name:        mld_polyz_unpack_17_avx2_asm
- *
- * Description: Unpack polynomial z with 18-bit packed coefficients
- *              (GAMMA1 = 2^17). Maps packed [0, 2^18-1] to signed
- *              [-(2^17-1), 2^17] via GAMMA1 - x.
- *
- * Arguments:   - int32_t *r:       pointer to output polynomial (1024 bytes)
- *              - const uint8_t *a: pointer to packed input (576 bytes)
- **************************************************/
-
 /*yaml
   Name: polyz_unpack_17_avx2_asm
-  Description: x86_64 AVX2 unpacking of 17-bit packed coefficients
+  Description: x86_64 AVX2 unpacking of 17-bit packed coefficients.
+    Unpack polynomial z with 18-bit packed coefficients (GAMMA1 = 2^17),
+    mapping packed [0, 2^18-1] to signed [-(2^17-1), 2^17] via GAMMA1 - x.
   Signature: void mld_polyz_unpack_17_avx2_asm(int32_t *r, const uint8_t *a)
   ABI:
     Architecture: x86_64

mldsa/src/native/x86_64/src/polyz_unpack_19_avx2_asm.S

@@ -18,20 +18,11 @@
  */
 
 
-/*************************************************
- * Name:        mld_polyz_unpack_19_avx2_asm
- *
- * Description: Unpack polynomial z with 20-bit packed coefficients
- *              (GAMMA1 = 2^19). Maps packed [0, 2^20-1] to signed
- *              [-(2^19-1), 2^19] via GAMMA1 - x.
- *
- * Arguments:   - int32_t *r:       pointer to output polynomial (1024 bytes)
- *              - const uint8_t *a: pointer to packed input (640 bytes)
- **************************************************/
-
 /*yaml
   Name: polyz_unpack_19_avx2_asm
-  Description: x86_64 AVX2 unpacking of 19-bit packed coefficients
+  Description: x86_64 AVX2 unpacking of 19-bit packed coefficients.
+    Unpack polynomial z with 20-bit packed coefficients (GAMMA1 = 2^19),
+    mapping packed [0, 2^20-1] to signed [-(2^19-1), 2^19] via GAMMA1 - x.
   Signature: void mld_polyz_unpack_19_avx2_asm(int32_t *r, const uint8_t *a)
   ABI:
     Architecture: x86_64

proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S

@@ -18,18 +18,11 @@
  */
 
 
-/*************************************************
- * Name:        mld_poly_caddq_avx2_asm
- *
- * Description: For all coefficients of in/out polynomial add Q if
- *              coefficient is negative.
- *
- * Arguments:   - int32_t *r: pointer to input/output polynomial
- **************************************************/
-
 /*yaml
   Name: poly_caddq_avx2_asm
-  Description: x86_64 AVX2 conditional addition of q to each coefficient
+  Description: x86_64 AVX2 conditional addition of q to each coefficient.
+    For all coefficients of the in/out polynomial, add Q if the coefficient
+    is negative.
   Signature: void mld_poly_caddq_avx2_asm(int32_t *r)
   ABI:
     Architecture: x86_64

proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S

@@ -18,22 +18,12 @@
  */
 
 
-/*************************************************
- * Name:        mld_poly_chknorm_avx2_asm
- *
- * Description: Check infinity norm of polynomial against given bound.
- *              Returns 0 if norm is strictly smaller than B; otherwise
- *              returns 1.
- *
- * Arguments:   - const int32_t *a: pointer to input polynomial
- *              - int32_t B:  bound
- *
- * Returns:     - 1 if any |coefficient| >= B, 0 otherwise.
- **************************************************/
-
 /*yaml
   Name: poly_chknorm_avx2_asm
-  Description: x86_64 AVX2 infinity-norm bound check on polynomial coefficients
+  Description: x86_64 AVX2 infinity-norm bound check on polynomial coefficients.
+    Check the infinity norm of the polynomial against the given bound B.
+    Returns 0 if the norm is strictly smaller than B; otherwise returns 1
+    (i.e. returns 1 if any |coefficient| >= B, 0 otherwise).
   Signature: int mld_poly_chknorm_avx2_asm(const int32_t *a, int32_t B)
   ABI:
     Architecture: x86_64