HOL-Light: Add x86_64 rej_uniform functional correctness proof

Port the MLDSA_REJ_UNIFORM_CORRECT proof from the s2n-bignum development
branch into a single bundled file at
proofs/hol_light/x86_64/proofs/mldsa_rej_uniform.ml.

Structure (all inlined):
- Machine code + EXEC rule (already present)
- Pre-helper arithmetic lemmas (VPSUBD_SIGN_BIT_BOUNDED, SIGN_BIT_BITVAL)
- Helper lemmas (mldsa_rej_uniform_helpers.ml)
- Post-helper definitions (REJ_SAMPLE, VAL_MOD_23_EQ_AND, ...)
- REJ_SAMPLE algebra (defs_extra.ml)
- R9 bridge + JA resolvers (defs.ml)
- PIVOT_VAL_EQ lemma
- MEMORY_CONJUNCT_CLOSURE lemma
- Case B closure helpers (VAL_RCX_ADD3, VAL_RCX_ADD3_ZX)
- SCALAR_BODY_LEMMA (per-iteration specification)
- Top-level MLDSA_REJ_UNIFORM_CORRECT

Register mldsa_rej_uniform in the x86_64 HOL-Light CI matrix so the
proof is verified on every PR that touches it or its dependencies.

Verifies in ~261s on a modern x86_64 machine, producing
MLDSA_REJ_UNIFORM_CORRECT with only the 3 standard HOL Light axioms.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Signed-off-by: Jake Massimo <jakemas@amazon.com>

Author: jakemas

.github/workflows/hol_light.yml

@@ -203,6 +203,8 @@ jobs:
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
           - name: mldsa_intt
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
+          - name: mldsa_rej_uniform
+            needs: ["mldsa_specs.ml", "mldsa_rej_uniform_table.ml"]
           - name: mldsa_nttunpack
             needs: ["mldsa_specs.ml"]
           - name: mldsa_pointwise