AArch64 rej_uniform: Remove three dead instructions

Drop a dead `sub buflen, #24`, a dead `add output_tmp, ctr1, lsl #1`
(immediately overwritten), and a `b` to the next label. The deletions
shift later offsets, so the HOL-Light bytecode, PC/length constants, step
ranges and state variables are adjusted to match; the proof still passes.

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

Author: hanno-becker

dev/aarch64_opt/src/rej_uniform_aarch64_asm.S

@@ -313,7 +313,6 @@ rej_uniform_loop48_end:
     cmp buflen, #24
     b.lo rej_uniform_memory_copy
 
-        sub     buflen, buflen, #24
         ld3     {buf0.8b, buf1.8b, buf2.8b}, [buf], #24
 
         zip1    tmp0.16b, buf0.16b, buf1.16b
@@ -356,7 +355,6 @@ rej_uniform_loop48_end:
         add     output_tmp, output_tmp, ctr0, lsl #1
 
         st1     {val1.8h}, [output_tmp]
-        add     output_tmp, output_tmp, ctr1, lsl #1
 
         add     count, count, ctr0
         add     count, count, ctr1
@@ -385,7 +383,6 @@ rej_uniform_final_copy:
         b.lt rej_uniform_final_copy
 
     mov x0, count
-    b rej_uniform_return
 
 rej_uniform_return:
     pop_stack

mlkem/src/native/aarch64/src/rej_uniform_aarch64_asm.S

@@ -159,7 +159,6 @@ Lrej_uniform_loop48_end:
         b.hs Lrej_uniform_memory_copy
         cmp x2, #0x18
         b.lo Lrej_uniform_memory_copy
-        sub x2, x2, #0x18
         ld3 { v0.8b, v1.8b, v2.8b }, [x1], #24
         zip1 v4.16b, v0.16b, v1.16b
         zip1 v5.16b, v1.16b, v2.16b
@@ -188,7 +187,6 @@ Lrej_uniform_loop48_end:
         st1 { v16.8h }, [x7]
         add x7, x7, x12, lsl #1
         st1 { v17.8h }, [x7]
-        add x7, x7, x13, lsl #1
         add x9, x9, x12
         add x9, x9, x13
 
@@ -211,7 +209,6 @@ Lrej_uniform_final_copy:
         cmp x11, #0x100
         b.lt Lrej_uniform_final_copy
         mov x0, x9
-        b Lrej_uniform_return
 
 Lrej_uniform_return:
         add sp, sp, #0x240

proofs/hol_light/aarch64/mlkem/rej_uniform_aarch64_asm.S

@@ -161,7 +161,6 @@ Lrej_uniform_loop48_end:
         b.hs Lrej_uniform_memory_copy
         cmp x2, #0x18
         b.lo Lrej_uniform_memory_copy
-        sub x2, x2, #0x18
         ld3 { v0.8b, v1.8b, v2.8b }, [x1], #24
         zip1 v4.16b, v0.16b, v1.16b
         zip1 v5.16b, v1.16b, v2.16b
@@ -190,7 +189,6 @@ Lrej_uniform_loop48_end:
         st1 { v16.8h }, [x7]
         add x7, x7, x12, lsl #1
         st1 { v17.8h }, [x7]
-        add x7, x7, x13, lsl #1
         add x9, x9, x12
         add x9, x9, x13
 
@@ -213,7 +211,6 @@ Lrej_uniform_final_copy:
         cmp x11, #0x100
         b.lt Lrej_uniform_final_copy
         mov x0, x9
-        b Lrej_uniform_return
 
 Lrej_uniform_return:
         add sp, sp, #0x240