Correct declaration and comments re size of rej-uniform lookup table

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -161,7 +161,7 @@ __contract__(
 #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
 MLK_MUST_CHECK_RETURN_VALUE
 uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf,
-                             unsigned buflen, const uint8_t table[2048])
+                             unsigned buflen, const uint8_t table[4096])
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml. */
 __contract__(

dev/aarch64_clean/src/rej_uniform_asm.S

@@ -6,7 +6,7 @@
 /*yaml
   Name: rej_uniform_asm
   Description: Run rejection sampling on uniform random bytes to generate uniform random integers mod q
-  Signature: uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf, unsigned buflen, const uint8_t table[2048])
+  Signature: uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf, unsigned buflen, const uint8_t table[4096])
   ABI:
     x0:
       type: buffer
@@ -27,9 +27,9 @@
       test_with: 504  # MLKEM_GEN_MATRIX_NBLOCKS * MLK_XOF_RATE
     x3:
       type: buffer
-      size_bytes: 2048
+      size_bytes: 4096
       permissions: read-only
-      c_parameter: const uint8_t table[2048]
+      c_parameter: const uint8_t table[4096]
       description: Lookup table
   Stack:
     bytes: 576

dev/aarch64_opt/src/arith_native_aarch64.h

@@ -161,7 +161,7 @@ __contract__(
 #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
 MLK_MUST_CHECK_RETURN_VALUE
 uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf,
-                             unsigned buflen, const uint8_t table[2048])
+                             unsigned buflen, const uint8_t table[4096])
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml. */
 __contract__(

dev/aarch64_opt/src/rej_uniform_asm.S

@@ -6,7 +6,7 @@
 /*yaml
   Name: rej_uniform_asm
   Description: Run rejection sampling on uniform random bytes to generate uniform random integers mod q
-  Signature: uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf, unsigned buflen, const uint8_t table[2048])
+  Signature: uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf, unsigned buflen, const uint8_t table[4096])
   ABI:
     x0:
       type: buffer
@@ -27,9 +27,9 @@
       test_with: 504  # MLKEM_GEN_MATRIX_NBLOCKS * MLK_XOF_RATE
     x3:
       type: buffer
-      size_bytes: 2048
+      size_bytes: 4096
       permissions: read-only
-      c_parameter: const uint8_t table[2048]
+      c_parameter: const uint8_t table[4096]
       description: Lookup table
   Stack:
     bytes: 576

mlkem/src/native/aarch64/src/arith_native_aarch64.h

@@ -161,7 +161,7 @@ __contract__(
 #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
 MLK_MUST_CHECK_RETURN_VALUE
 uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf,
-                             unsigned buflen, const uint8_t table[2048])
+                             unsigned buflen, const uint8_t table[4096])
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml. */
 __contract__(

mlkem/src/native/aarch64/src/rej_uniform_asm.S

@@ -6,7 +6,7 @@
 /*yaml
   Name: rej_uniform_asm
   Description: Run rejection sampling on uniform random bytes to generate uniform random integers mod q
-  Signature: uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf, unsigned buflen, const uint8_t table[2048])
+  Signature: uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf, unsigned buflen, const uint8_t table[4096])
   ABI:
     x0:
       type: buffer
@@ -27,9 +27,9 @@
       test_with: 504  # MLKEM_GEN_MATRIX_NBLOCKS * MLK_XOF_RATE
     x3:
       type: buffer
-      size_bytes: 2048
+      size_bytes: 4096
       permissions: read-only
-      c_parameter: const uint8_t table[2048]
+      c_parameter: const uint8_t table[4096]
       description: Lookup table
   Stack:
     bytes: 576

proofs/hol_light/aarch64/mlkem/mlkem_rej_uniform.S

@@ -6,7 +6,7 @@
 /*yaml
   Name: rej_uniform_asm
   Description: Run rejection sampling on uniform random bytes to generate uniform random integers mod q
-  Signature: uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf, unsigned buflen, const uint8_t table[2048])
+  Signature: uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf, unsigned buflen, const uint8_t table[4096])
   ABI:
     x0:
       type: buffer
@@ -27,9 +27,9 @@
       test_with: 504  # MLKEM_GEN_MATRIX_NBLOCKS * MLK_XOF_RATE
     x3:
       type: buffer
-      size_bytes: 2048
+      size_bytes: 4096
       permissions: read-only
-      c_parameter: const uint8_t table[2048]
+      c_parameter: const uint8_t table[4096]
       description: Lookup table
   Stack:
     bytes: 576