AArch64: Use alignment-safe Neon stores in rej_uniform

The output pointer in rej_uniform_asm.S advances in multiples of 2 bytes
(sizeof(int16_t)), so it is not 16-byte aligned in general. The `str qN, [ptr]`
instruction requires 16-byte alignment, which faults on bare-metal AArch64
without an MMU (Device memory). Replace with `st1 {vN.8h}, [ptr]` which
has no alignment requirement.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Author: mkannwischer

dev/aarch64_opt/src/rej_uniform_asm.S

@@ -283,16 +283,16 @@ rej_uniform_loop48:
         tbl     val2.16b, {val2.16b}, table2.16b
         tbl     val3.16b, {val3.16b}, table3.16b
 
-        str     val0q, [output_tmp]
+        st1     {val0.8h}, [output_tmp]
         add     output_tmp, output_tmp, ctr0, lsl #1
 
-        str     val1q, [output_tmp]
+        st1     {val1.8h}, [output_tmp]
         add     output_tmp, output_tmp, ctr1, lsl #1
 
-        str     val2q, [output_tmp]
+        st1     {val2.8h}, [output_tmp]
         add     output_tmp, output_tmp, ctr2, lsl #1
 
-        str     val3q, [output_tmp]
+        st1     {val3.8h}, [output_tmp]
         add     output_tmp, output_tmp, ctr3, lsl #1
 
         add     ctr01, ctr0, ctr1
@@ -350,10 +350,10 @@ rej_uniform_loop48_end:
         tbl     val0.16b, {val0.16b}, table0.16b
         tbl     val1.16b, {val1.16b}, table1.16b
 
-        str     val0q, [output_tmp]
+        st1     {val0.8h}, [output_tmp]
         add     output_tmp, output_tmp, ctr0, lsl #1
 
-        str     val1q, [output_tmp]
+        st1     {val1.8h}, [output_tmp]
         add     output_tmp, output_tmp, ctr1, lsl #1
 
         add     count, count, ctr0

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

@@ -141,13 +141,13 @@ Lrej_uniform_loop48:
         tbl	v17.16b, { v17.16b }, v25.16b
         tbl	v18.16b, { v18.16b }, v26.16b
         tbl	v19.16b, { v19.16b }, v27.16b
-        str	q16, [x7]
+        st1	{ v16.8h }, [x7]
         add	x7, x7, x12, lsl #1
-        str	q17, [x7]
+        st1	{ v17.8h }, [x7]
         add	x7, x7, x13, lsl #1
-        str	q18, [x7]
+        st1	{ v18.8h }, [x7]
         add	x7, x7, x14, lsl #1
-        str	q19, [x7]
+        st1	{ v19.8h }, [x7]
         add	x7, x7, x15, lsl #1
         add	x12, x12, x13
         add	x14, x14, x15
@@ -187,9 +187,9 @@ Lrej_uniform_loop48_end:
         fmov	w13, s21
         tbl	v16.16b, { v16.16b }, v24.16b
         tbl	v17.16b, { v17.16b }, v25.16b
-        str	q16, [x7]
+        st1	{ v16.8h }, [x7]
         add	x7, x7, x12, lsl #1
-        str	q17, [x7]
+        st1	{ v17.8h }, [x7]
         add	x7, x7, x13, lsl #1
         add	x9, x9, x12
         add	x9, x9, x13

proofs/hol_light/aarch64/mlkem/mlkem_rej_uniform.S

@@ -143,13 +143,13 @@ Lrej_uniform_loop48:
         tbl	v17.16b, { v17.16b }, v25.16b
         tbl	v18.16b, { v18.16b }, v26.16b
         tbl	v19.16b, { v19.16b }, v27.16b
-        str	q16, [x7]
+        st1	{ v16.8h }, [x7]
         add	x7, x7, x12, lsl #1
-        str	q17, [x7]
+        st1	{ v17.8h }, [x7]
         add	x7, x7, x13, lsl #1
-        str	q18, [x7]
+        st1	{ v18.8h }, [x7]
         add	x7, x7, x14, lsl #1
-        str	q19, [x7]
+        st1	{ v19.8h }, [x7]
         add	x7, x7, x15, lsl #1
         add	x12, x12, x13
         add	x14, x14, x15
@@ -189,9 +189,9 @@ Lrej_uniform_loop48_end:
         fmov	w13, s21
         tbl	v16.16b, { v16.16b }, v24.16b
         tbl	v17.16b, { v17.16b }, v25.16b
-        str	q16, [x7]
+        st1	{ v16.8h }, [x7]
         add	x7, x7, x12, lsl #1
-        str	q17, [x7]
+        st1	{ v17.8h }, [x7]
         add	x7, x7, x13, lsl #1
         add	x9, x9, x12
         add	x9, x9, x13

proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml

@@ -102,13 +102,13 @@ let mlkem_rej_uniform_mc = define_assert_from_elf
   0x4e190231;       (* arm_TBL Q17 [Q17] Q25 128 *)
   0x4e1a0252;       (* arm_TBL Q18 [Q18] Q26 128 *)
   0x4e1b0273;       (* arm_TBL Q19 [Q19] Q27 128 *)
-  0x3d8000f0;       (* arm_STR Q16 X7 (Immediate_Offset (word 0)) *)
+  0x4c0074f0;       (* arm_STR Q16 X7 No_Offset *)
   0x8b0c04e7;       (* arm_ADD X7 X7 (Shiftedreg X12 LSL 1) *)
-  0x3d8000f1;       (* arm_STR Q17 X7 (Immediate_Offset (word 0)) *)
+  0x4c0074f1;       (* arm_STR Q17 X7 No_Offset *)
   0x8b0d04e7;       (* arm_ADD X7 X7 (Shiftedreg X13 LSL 1) *)
-  0x3d8000f2;       (* arm_STR Q18 X7 (Immediate_Offset (word 0)) *)
+  0x4c0074f2;       (* arm_STR Q18 X7 No_Offset *)
   0x8b0e04e7;       (* arm_ADD X7 X7 (Shiftedreg X14 LSL 1) *)
-  0x3d8000f3;       (* arm_STR Q19 X7 (Immediate_Offset (word 0)) *)
+  0x4c0074f3;       (* arm_STR Q19 X7 No_Offset *)
   0x8b0f04e7;       (* arm_ADD X7 X7 (Shiftedreg X15 LSL 1) *)
   0x8b0d018c;       (* arm_ADD X12 X12 X13 *)
   0x8b0f01ce;       (* arm_ADD X14 X14 X15 *)
@@ -146,9 +146,9 @@ let mlkem_rej_uniform_mc = define_assert_from_elf
   0x1e2602ad;       (* arm_FMOV_FtoI W13 Q21 0 32 *)
   0x4e180210;       (* arm_TBL Q16 [Q16] Q24 128 *)
   0x4e190231;       (* arm_TBL Q17 [Q17] Q25 128 *)
-  0x3d8000f0;       (* arm_STR Q16 X7 (Immediate_Offset (word 0)) *)
+  0x4c0074f0;       (* arm_STR Q16 X7 No_Offset *)
   0x8b0c04e7;       (* arm_ADD X7 X7 (Shiftedreg X12 LSL 1) *)
-  0x3d8000f1;       (* arm_STR Q17 X7 (Immediate_Offset (word 0)) *)
+  0x4c0074f1;       (* arm_STR Q17 X7 No_Offset *)
   0x8b0d04e7;       (* arm_ADD X7 X7 (Shiftedreg X13 LSL 1) *)
   0x8b0c0129;       (* arm_ADD X9 X9 X12 *)
   0x8b0d0129;       (* arm_ADD X9 X9 X13 *)