Remove 2 dead instruction from AArch64 back-end poly_tomont()

1. Remove 2 dead instructions.
2. These appear outside the inner-loop of poly_tomont(), so do NOT
   re-apply SLOTHY to minimize the difference in code going into production.
3. Re-autogen all files
4. Update HOL-Light bytecode for poly_tomont()
5. Re-check HOL-Light proof of this function.

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

dev/aarch64_clean/src/poly_tomont_asm.S

@@ -43,7 +43,6 @@
         factor            .req v2
         factor_t          .req v3
         modulus           .req v4
-        modulus_twisted   .req v5
 
         tmp0              .req v6
 
@@ -55,9 +54,6 @@ MLK_ASM_FN_SYMBOL(poly_tomont_asm)
         mov wtmp, #3329 // ML-KEM modulus
         dup modulus.8h, wtmp
 
-        mov wtmp, #20159 // Barrett twist of 1 wrt 2^27
-        dup modulus_twisted.8h, wtmp
-
         mov wtmp, #-1044 // 2^16 % 3329
         dup factor.8h, wtmp
 
@@ -100,7 +96,6 @@ poly_tomont_loop:
         .unreq factor
         .unreq factor_t
         .unreq modulus
-        .unreq modulus_twisted
 
         .unreq tmp0
 

dev/aarch64_opt/src/poly_tomont_asm.S

@@ -42,7 +42,6 @@
         factor            .req v2
         factor_t          .req v3
         modulus           .req v4
-        modulus_twisted   .req v5
 
         tmp0              .req v6
 
@@ -54,9 +53,6 @@ MLK_ASM_FN_SYMBOL(poly_tomont_asm)
         mov wtmp, #3329 // ML-KEM modulus
         dup modulus.8h, wtmp
 
-        mov wtmp, #20159 // Barrett twist of 1 wrt 2^27
-        dup modulus_twisted.8h, wtmp
-
         mov wtmp, #-1044 // 2^16 % 3329
         dup factor.8h, wtmp
 
@@ -217,7 +213,6 @@ poly_tomont_loop:
         .unreq factor
         .unreq factor_t
         .unreq modulus
-        .unreq modulus_twisted
 
         .unreq tmp0
 

mlkem/src/native/aarch64/src/poly_tomont_asm.S

@@ -34,8 +34,6 @@ MLK_ASM_FN_SYMBOL(poly_tomont_asm)
         .cfi_startproc
         mov w2, #0xd01              // =3329
         dup v4.8h, w2
-        mov w2, #0x4ebf             // =20159
-        dup v5.8h, w2
         mov w2, #-0x414             // =-1044
         dup v2.8h, w2
         mov w2, #-0x2824            // =-10276

proofs/hol_light/aarch64/mlkem/mlkem_poly_tomont.S

@@ -37,8 +37,6 @@ PQCP_MLKEM_NATIVE_MLKEM768_poly_tomont_asm:
         .cfi_startproc
         mov w2, #0xd01              // =3329
         dup v4.8h, w2
-        mov w2, #0x4ebf             // =20159
-        dup v5.8h, w2
         mov w2, #-0x414             // =-1044
         dup v2.8h, w2
         mov w2, #-0x2824            // =-10276

proofs/hol_light/aarch64/proofs/mlkem_poly_tomont.ml

@@ -18,8 +18,6 @@ let poly_tomont_asm_mc = define_assert_from_elf
 [
   0x5281a022;       (* arm_MOV W2 (rvalue (word 3329)) *)
   0x4e020c44;       (* arm_DUP_GEN Q4 X2 16 128 *)
-  0x5289d7e2;       (* arm_MOV W2 (rvalue (word 20159)) *)
-  0x4e020c45;       (* arm_DUP_GEN Q5 X2 16 128 *)
   0x12808262;       (* arm_MOVN W2 (word 1043) 0 *)
   0x4e020c42;       (* arm_DUP_GEN Q2 X2 16 128 *)
   0x12850462;       (* arm_MOVN W2 (word 10275) 0 *)