AArch64 NTT/invNTT: Drop dead flag-set in loop tail

The loop-tail `subs count, count, #1` writes NZCV, but the loop closes on
`cbnz` and the flags are never read. Replace with a plain `sub` in both the
opt and clean variants. The HOL-Light bytecode is updated to match; the
proofs are otherwise unchanged.

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

Author: hanno-becker

dev/aarch64_clean/src/intt_aarch64_asm.S

@@ -299,7 +299,7 @@ intt_layer4567_start:
         str q_data2, [inp, #(-64 + 16*2)]
         str q_data3, [inp, #(-64 + 16*3)]
 
-        subs count, count, #1
+        sub count, count, #1
         cbnz count, intt_layer4567_start
 
         // ---------------------------------------------------------------------
@@ -347,7 +347,7 @@ intt_layer123_start:
         str q_data2, [in, #(-16 + 2*(512/8))]
         str q_data3, [in, #(-16 + 3*(512/8))]
 
-        subs count, count, #1
+        sub count, count, #1
         cbnz count, intt_layer123_start
 
         pop_stack

dev/aarch64_clean/src/ntt_aarch64_asm.S

@@ -255,7 +255,7 @@ ntt_layer123_start:
         str q_data6, [in, #(-16 + 6*(512/8))]
         str q_data7, [in, #(-16 + 7*(512/8))]
 
-        subs count, count, #1
+        sub count, count, #1
         cbnz count, ntt_layer123_start
 
         mov in, inp
@@ -291,7 +291,7 @@ ntt_layer4567_start:
         str q_data2, [in, #(-16*2)]
         str q_data3, [in, #(-16*1)]
 
-        subs count, count, #1
+        sub count, count, #1
         cbnz count, ntt_layer4567_start
 
         pop_stack

dev/aarch64_opt/src/intt_aarch64_asm.S

@@ -685,7 +685,7 @@ intt_layer4567_start:
         // str q10, [x3, #(-64 + 16*2)]               // .....~.............................................................................'.....~.............................................................................'.....l.............................................................................
         // str q11, [x3, #(-64 + 16*3)]               // ................................................................~..................'................................................................~..................'................................................................l..................
 
-        subs count, count, 1
+        sub count, count, 1
         cbnz count, intt_layer4567_start
                                                  // Instructions:    71
                                                  // Expected cycles: 77
@@ -1187,7 +1187,7 @@ intt_layer123_start:
         // str q10, [x0, #(-16 + 2*(512/8))]          // ...............................................~........'..............................................................*........'..............................................................~......
         // str q11, [x0, #(-16 + 3*(512/8))]          // ........................................................'..~....................................................................'..l..................................................................
 
-        subs count, count, 1
+        sub count, count, 1
         cbnz count, intt_layer123_start
                                                 // Instructions:    81
                                                 // Expected cycles: 86

dev/aarch64_opt/src/ntt_aarch64_asm.S

@@ -527,7 +527,7 @@ ntt_layer123_start:
         // str q14, [x0, #(-16 + 6*(512/8))]          // ................................~................................'......................................~................................'......................................l.....
         // str q15, [x0, #(-16 + 7*(512/8))]          // .....................................~...........................'...........................................~...........................'...........................................l
 
-        subs count, count, 1
+        sub count, count, 1
         cbnz count, ntt_layer123_start
                                                 // Instructions:    93
                                                 // Expected cycles: 84
@@ -1070,7 +1070,7 @@ ntt_layer4567_start:
         // str q10, [x0, #(-16*2)]                    // ...........~..................................'............~..................................'............l...........................
         // str q11, [x0, #(-16*1)]                    // ......................................~.......'.......................................~.......'.......................................l
 
-        subs count, count, 1
+        sub count, count, 1
         cbnz count, ntt_layer4567_start
                                               // Instructions:    66
                                               // Expected cycles: 49

mlkem/src/native/aarch64/src/intt_aarch64_asm.S

@@ -295,7 +295,7 @@ Lintt_layer4567_start:
         sqrdmulh v31.8h, v8.8h, v11.h[5]
         sub v14.8h, v21.8h, v10.8h
         stur q0, [x3, #-0x30]
-        subs x4, x4, #0x1
+        sub x4, x4, #0x1
         cbnz x4, Lintt_layer4567_start
         mul v15.8h, v6.8h, v15.8h
         sub v22.8h, v20.8h, v25.8h
@@ -521,7 +521,7 @@ Lintt_layer123_start:
         sqrdmulh v9.8h, v13.8h, v0.h[1]
         str q17, [x0, #0x130]
         mul v17.8h, v19.8h, v0.h[0]
-        subs x4, x4, #0x1
+        sub x4, x4, #0x1
         cbnz x4, Lintt_layer123_start
         mls v23.8h, v10.8h, v7.h[0]
         ldr q11, [x0, #0x190]

mlkem/src/native/aarch64/src/ntt_aarch64_asm.S

@@ -223,7 +223,7 @@ Lntt_layer123_start:
         add v28.8h, v13.8h, v23.8h
         sub v13.8h, v13.8h, v23.8h
         mul v23.8h, v20.8h, v0.h[2]
-        subs x4, x4, #0x1
+        sub x4, x4, #0x1
         cbnz x4, Lntt_layer123_start
         sqrdmulh v3.8h, v5.8h, v1.h[1]
         mls v23.8h, v15.8h, v7.h[0]
@@ -470,7 +470,7 @@ Lntt_layer4567_start:
         sub v30.8h, v21.8h, v17.8h
         mul v0.8h, v16.8h, v1.8h
         trn1 v28.4s, v6.4s, v12.4s
-        subs x4, x4, #0x1
+        sub x4, x4, #0x1
         cbnz x4, Lntt_layer4567_start
         add v22.8h, v11.8h, v8.8h
         mul v27.8h, v27.8h, v4.h[2]

proofs/hol_light/aarch64/mlkem/intt_aarch64_asm.S

@@ -298,7 +298,7 @@ Lintt_layer4567_start:
         sqrdmulh v31.8h, v8.8h, v11.h[5]
         sub v14.8h, v21.8h, v10.8h
         stur q0, [x3, #-0x30]
-        subs x4, x4, #0x1
+        sub x4, x4, #0x1
         cbnz x4, Lintt_layer4567_start
         mul v15.8h, v6.8h, v15.8h
         sub v22.8h, v20.8h, v25.8h
@@ -524,7 +524,7 @@ Lintt_layer123_start:
         sqrdmulh v9.8h, v13.8h, v0.h[1]
         str q17, [x0, #0x130]
         mul v17.8h, v19.8h, v0.h[0]
-        subs x4, x4, #0x1
+        sub x4, x4, #0x1
         cbnz x4, Lintt_layer123_start
         mls v23.8h, v10.8h, v7.h[0]
         ldr q11, [x0, #0x190]

proofs/hol_light/aarch64/mlkem/ntt_aarch64_asm.S

@@ -226,7 +226,7 @@ Lntt_layer123_start:
         add v28.8h, v13.8h, v23.8h
         sub v13.8h, v13.8h, v23.8h
         mul v23.8h, v20.8h, v0.h[2]
-        subs x4, x4, #0x1
+        sub x4, x4, #0x1
         cbnz x4, Lntt_layer123_start
         sqrdmulh v3.8h, v5.8h, v1.h[1]
         mls v23.8h, v15.8h, v7.h[0]
@@ -473,7 +473,7 @@ Lntt_layer4567_start:
         sub v30.8h, v21.8h, v17.8h
         mul v0.8h, v16.8h, v1.8h
         trn1 v28.4s, v6.4s, v12.4s
-        subs x4, x4, #0x1
+        sub x4, x4, #0x1
         cbnz x4, Lntt_layer4567_start
         add v22.8h, v11.8h, v8.8h
         mul v27.8h, v27.8h, v4.h[2]

proofs/hol_light/aarch64/proofs/intt_aarch64_asm.ml

@@ -242,7 +242,7 @@ let mlkem_intt_mc = define_assert_from_elf
   0x4f5bd91f;       (* arm_SQRDMULH_VEC Q31 Q8 (Q11 :> LANE_H 5) 16 128 *)
   0x6e6a86ae;       (* arm_SUB_VEC Q14 Q21 Q10 16 128 *)
   0x3c9d0060;       (* arm_STR Q0 X3 (Immediate_Offset (word 18446744073709551568)) *)
-  0xf1000484;       (* arm_SUBS X4 X4 (rvalue (word 1)) *)
+  0xd1000484;       (* arm_SUB X4 X4 (rvalue (word 1)) *)
   0xb5fff464;       (* arm_CBNZ X4 (word 2096780) *)
   0x4e6f9ccf;       (* arm_MUL_VEC Q15 Q6 Q15 16 128 *)
   0x6e798696;       (* arm_SUB_VEC Q22 Q20 Q25 16 128 *)
@@ -466,7 +466,7 @@ let mlkem_intt_mc = define_assert_from_elf
   0x4f50d1a9;       (* arm_SQRDMULH_VEC Q9 Q13 (Q0 :> LANE_H 1) 16 128 *)
   0x3d804c11;       (* arm_STR Q17 X0 (Immediate_Offset (word 304)) *)
   0x4f408271;       (* arm_MUL_VEC Q17 Q19 (Q0 :> LANE_H 0) 16 128 *)
-  0xf1000484;       (* arm_SUBS X4 X4 (rvalue (word 1)) *)
+  0xd1000484;       (* arm_SUB X4 X4 (rvalue (word 1)) *)
   0xb5fff664;       (* arm_CBNZ X4 (word 2096844) *)
   0x6f474157;       (* arm_MLS_VEC Q23 Q10 (Q7 :> LANE_H 0) 16 128 *)
   0x3dc0640b;       (* arm_LDR Q11 X0 (Immediate_Offset (word 400)) *)

proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml

@@ -170,7 +170,7 @@ let mlkem_ntt_mc = define_assert_from_elf
   0x4e7785bc;       (* arm_ADD_VEC Q28 Q13 Q23 16 128 *)
   0x6e7785ad;       (* arm_SUB_VEC Q13 Q13 Q23 16 128 *)
   0x4f608297;       (* arm_MUL_VEC Q23 Q20 (Q0 :> LANE_H 2) 16 128 *)
-  0xf1000484;       (* arm_SUBS X4 X4 (rvalue (word 1)) *)
+  0xd1000484;       (* arm_SUB X4 X4 (rvalue (word 1)) *)
   0xb5fff664;       (* arm_CBNZ X4 (word 2096844) *)
   0x4f51d0a3;       (* arm_SQRDMULH_VEC Q3 Q5 (Q1 :> LANE_H 1) 16 128 *)
   0x6f4741f7;       (* arm_MLS_VEC Q23 Q15 (Q7 :> LANE_H 0) 16 128 *)
@@ -415,7 +415,7 @@ let mlkem_ntt_mc = define_assert_from_elf
   0x6e7186be;       (* arm_SUB_VEC Q30 Q21 Q17 16 128 *)
   0x4e619e00;       (* arm_MUL_VEC Q0 Q16 Q1 16 128 *)
   0x4e8c28dc;       (* arm_TRN1 Q28 Q6 Q12 32 128 *)
-  0xf1000484;       (* arm_SUBS X4 X4 (rvalue (word 1)) *)
+  0xd1000484;       (* arm_SUB X4 X4 (rvalue (word 1)) *)
   0xb5fff704;       (* arm_CBNZ X4 (word 2096864) *)
   0x4e688576;       (* arm_ADD_VEC Q22 Q11 Q8 16 128 *)
   0x4f64837b;       (* arm_MUL_VEC Q27 Q27 (Q4 :> LANE_H 2) 16 128 *)