[TEST ONLY] Introduce overflow

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

dev/aarch64_opt/src/rej_uniform_asm.S

@@ -312,7 +312,7 @@ rej_uniform_loop48_end:
     b.lo rej_uniform_memory_copy
 
         sub     buflen, buflen, #24
-        ld3     {buf0.8b, buf1.8b, buf2.8b}, [buf], #24
+        ld3     {buf0.16b, buf1.16b, buf2.16b}, [buf], #48
 
         zip1    tmp0.16b, buf0.16b, buf1.16b
         zip1    tmp1.16b, buf1.16b, buf2.16b

dev/x86_64/src/rej_uniform_asm.S

@@ -98,8 +98,7 @@ MLK_ASM_FN_SYMBOL(rej_uniform_asm)
 rej_uniform_asm_loop_start:
   // 1. Split 96 bits into eight 12-bit integers where each integer.
   //    We explain the algorithm by considering the lowest 64 bits of vals.
-  movq    (in, pos), vals        // Load low 8 bytes into bits [63:0] of vals
-  pinsrd  $2, 8(in, pos), vals   // Insert 4 bytes into bits [95:64] of vals
+  movdqu  (in, pos), vals        // Load 16 bytes, overread by 4
   //    vals: [ 63..48 | 47..32 | 31..16 | 15..0 ]
   pshufb  shuffle_in_mask, vals
   //    vals: [ 47..32 | 39..24 | 23..8 | 15..0 ]

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

@@ -158,7 +158,7 @@ Lrej_uniform_loop48_end:
         cmp x2, #0x18
         b.lo Lrej_uniform_memory_copy
         sub x2, x2, #0x18
-        ld3 { v0.8b, v1.8b, v2.8b }, [x1], #24
+        ld3 { v0.16b, v1.16b, v2.16b }, [x1], #48
         zip1 v4.16b, v0.16b, v1.16b
         zip1 v5.16b, v1.16b, v2.16b
         bic v4.8h, #0xf0, lsl #8

mlkem/src/native/x86_64/src/rej_uniform_asm.S

@@ -54,8 +54,7 @@ MLK_ASM_FN_SYMBOL(rej_uniform_asm)
         movq $0x5555, %r9            # imm = 0x5555
 
 Lrej_uniform_asm_loop_start:
-        movq (%rsi,%r8), %xmm2
-        pinsrd $0x2, 0x8(%rsi,%r8), %xmm2
+        movdqu (%rsi,%r8), %xmm2
         pshufb %xmm4, %xmm2
         movdqa %xmm2, %xmm3
         psrlw $0x4, %xmm3

proofs/hol_light/aarch64/mlkem/mlkem_rej_uniform.S

@@ -160,7 +160,7 @@ Lrej_uniform_loop48_end:
         cmp x2, #0x18
         b.lo Lrej_uniform_memory_copy
         sub x2, x2, #0x18
-        ld3 { v0.8b, v1.8b, v2.8b }, [x1], #24
+        ld3 { v0.16b, v1.16b, v2.16b }, [x1], #48
         zip1 v4.16b, v0.16b, v1.16b
         zip1 v5.16b, v1.16b, v2.16b
         bic v4.8h, #0xf0, lsl #8