x86_64: Replace rej_uniform AVX2 intrinsics with assembly + HOL-Light proof

Replaces the intrinsics-based rej_uniform_avx2.c with a hand-written
assembly routine (mld_rej_uniform_avx2_asm) and adds HOL-Light functional
correctness and memory-safety proofs on top of s2n-bignum, plus the CBMC
contract proof.

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

Author: jakemas

.github/workflows/hol_light.yml

@@ -208,6 +208,8 @@ jobs:
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
           - name: intt_avx2_asm
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
+          - name: rej_uniform_avx2_asm
+            needs: ["mldsa_specs.ml", "mldsa_rej_uniform_table.ml"]
           - name: nttunpack_avx2_asm
             needs: ["mldsa_specs.ml", "subroutine_signatures.ml"]
           - name: pointwise_avx2_asm

BIBLIOGRAPHY.md

@@ -308,7 +308,7 @@ source code and documentation.
   - [dev/x86_64/src/poly_use_hint_88_avx2_asm.S](dev/x86_64/src/poly_use_hint_88_avx2_asm.S)
   - [dev/x86_64/src/polyz_unpack_17_avx2_asm.S](dev/x86_64/src/polyz_unpack_17_avx2_asm.S)
   - [dev/x86_64/src/polyz_unpack_19_avx2_asm.S](dev/x86_64/src/polyz_unpack_19_avx2_asm.S)
-  - [dev/x86_64/src/rej_uniform_avx2.c](dev/x86_64/src/rej_uniform_avx2.c)
+  - [dev/x86_64/src/rej_uniform_avx2_asm.S](dev/x86_64/src/rej_uniform_avx2_asm.S)
   - [dev/x86_64/src/rej_uniform_eta2_avx2.c](dev/x86_64/src/rej_uniform_eta2_avx2.c)
   - [dev/x86_64/src/rej_uniform_eta4_avx2.c](dev/x86_64/src/rej_uniform_eta4_avx2.c)
   - [mldsa/src/native/x86_64/src/intt_avx2_asm.S](mldsa/src/native/x86_64/src/intt_avx2_asm.S)
@@ -326,7 +326,7 @@ source code and documentation.
   - [mldsa/src/native/x86_64/src/poly_use_hint_88_avx2_asm.S](mldsa/src/native/x86_64/src/poly_use_hint_88_avx2_asm.S)
   - [mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S](mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S)
   - [mldsa/src/native/x86_64/src/polyz_unpack_19_avx2_asm.S](mldsa/src/native/x86_64/src/polyz_unpack_19_avx2_asm.S)
-  - [mldsa/src/native/x86_64/src/rej_uniform_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_avx2.c)
+  - [mldsa/src/native/x86_64/src/rej_uniform_avx2_asm.S](mldsa/src/native/x86_64/src/rej_uniform_avx2_asm.S)
   - [mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c)
   - [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c)
   - [proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S](proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S)
@@ -344,6 +344,7 @@ source code and documentation.
   - [proofs/hol_light/x86_64/mldsa/poly_use_hint_88_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_use_hint_88_avx2_asm.S)
   - [proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S)
   - [proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mldsa/rej_uniform_avx2_asm.S](proofs/hol_light/x86_64/mldsa/rej_uniform_avx2_asm.S)
 
 ### `Round3_Spec`
 

dev/x86_64/meta.h

@@ -80,7 +80,7 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
   }
 
   /* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
-  return (int)mld_rej_uniform_avx2(r, buf);
+  return (int)mld_rej_uniform_avx2_asm(r, buf, mld_rej_uniform_table);
 }
 
 #if !defined(MLD_CONFIG_NO_KEYPAIR_API)

dev/x86_64/src/arith_native_x86_64.h

@@ -77,10 +77,21 @@ __contract__(
     r[i] == old(*(int32_t (*)[MLDSA_N])r)[j])))
 );
 
-#define mld_rej_uniform_avx2 MLD_NAMESPACE(mld_rej_uniform_avx2)
-MLD_MUST_CHECK_RETURN_VALUE
-unsigned mld_rej_uniform_avx2(int32_t *r,
-                              const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN]);
+#define mld_rej_uniform_avx2_asm MLD_NAMESPACE(rej_uniform_avx2_asm)
+/* This contract must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/x86_64/proofs/rej_uniform_avx2_asm.ml */
+MLD_MUST_CHECK_RETURN_VALUE MLD_SYSV_ABI
+unsigned mld_rej_uniform_avx2_asm(
+    int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN],
+    const uint8_t table[256][8])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, 840))
+  requires(table == mld_rej_uniform_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  ensures(array_bound(r, 0, return_value, 0, MLDSA_Q))
+);
 
 #if !defined(MLD_CONFIG_NO_KEYPAIR_API)
 #define mld_rej_uniform_eta2_avx2 MLD_NAMESPACE(mld_rej_uniform_eta2_avx2)