Sync ML-KEM Keccak generated wipes

Regenerate the forced-cross Keccak outputs after adding stack clearing to the shared x4 source. The aarch64 host-local autogen path skipped the x86_64 generated files, but CI regenerates them on x86_64 and with forced cross toolchains.

This expands the generated wipe-store blocks in the checked-in Armv8.1-M and x86_64 outputs so the native autogen and HOL-Light bytecode dry-run checks agree with the source.

Co-authored-by: Codex <codex@openai.com>
Signed-off-by: Joe Doyle <joseph.doyle@trailofbits.com>

Author: tob-joe

mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S

@@ -683,11 +683,14 @@ Lkeccak_f1600_x4_mve_asm_roundend_pre:
 Lkeccak_f1600_x4_mve_asm_roundend:
         movs r0, #0x0
         vdup.32 q0, r0
-        .set .Lkeccak_f1600_x4_mve_clear_stack_offset, 0
-        .rept 8
-        vstrw.32 q0, [sp, #.Lkeccak_f1600_x4_mve_clear_stack_offset]
-        .set .Lkeccak_f1600_x4_mve_clear_stack_offset, .Lkeccak_f1600_x4_mve_clear_stack_offset + 16
-        .endr
+        vstrw.32 q0, [sp]
+        vstrw.32 q0, [sp, #16]
+        vstrw.32 q0, [sp, #32]
+        vstrw.32 q0, [sp, #48]
+        vstrw.32 q0, [sp, #64]
+        vstrw.32 q0, [sp, #80]
+        vstrw.32 q0, [sp, #96]
+        vstrw.32 q0, [sp, #112]
         add sp, #0x80
         .cfi_adjust_cfa_offset -0x80
         vpop {d8, d9, d10, d11, d12, d13, d14, d15}

mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S

@@ -474,11 +474,30 @@ LLkeccak_f1600_x4_avx2:
         vmovq %xmm15, 0x250(%rdi)
         vmovhpd %xmm15, 0x318(%rdi)
         vpxor %ymm0, %ymm0, %ymm0
-        .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, 0
-        .rept 24
-        vmovdqu %ymm0, .Lkeccak_f1600_x4_avx2_clear_stack_offset(%rsp)
-        .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, .Lkeccak_f1600_x4_avx2_clear_stack_offset + 32
-        .endr
+        vmovdqu %ymm0, (%rsp)
+        vmovdqu %ymm0, 0x20(%rsp)
+        vmovdqu %ymm0, 0x40(%rsp)
+        vmovdqu %ymm0, 0x60(%rsp)
+        vmovdqu %ymm0, 0x80(%rsp)
+        vmovdqu %ymm0, 0xa0(%rsp)
+        vmovdqu %ymm0, 0xc0(%rsp)
+        vmovdqu %ymm0, 0xe0(%rsp)
+        vmovdqu %ymm0, 0x100(%rsp)
+        vmovdqu %ymm0, 0x120(%rsp)
+        vmovdqu %ymm0, 0x140(%rsp)
+        vmovdqu %ymm0, 0x160(%rsp)
+        vmovdqu %ymm0, 0x180(%rsp)
+        vmovdqu %ymm0, 0x1a0(%rsp)
+        vmovdqu %ymm0, 0x1c0(%rsp)
+        vmovdqu %ymm0, 0x1e0(%rsp)
+        vmovdqu %ymm0, 0x200(%rsp)
+        vmovdqu %ymm0, 0x220(%rsp)
+        vmovdqu %ymm0, 0x240(%rsp)
+        vmovdqu %ymm0, 0x260(%rsp)
+        vmovdqu %ymm0, 0x280(%rsp)
+        vmovdqu %ymm0, 0x2a0(%rsp)
+        vmovdqu %ymm0, 0x2c0(%rsp)
+        vmovdqu %ymm0, 0x2e0(%rsp)
         movq %r11, %rsp
         .cfi_def_cfa_register %rsp
         retq

proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S

@@ -477,11 +477,30 @@ LLkeccak_f1600_x4_avx2:
         vmovq %xmm15, 0x250(%rdi)
         vmovhpd %xmm15, 0x318(%rdi)
         vpxor %ymm0, %ymm0, %ymm0
-        .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, 0
-        .rept 24
-        vmovdqu %ymm0, .Lkeccak_f1600_x4_avx2_clear_stack_offset(%rsp)
-        .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, .Lkeccak_f1600_x4_avx2_clear_stack_offset + 32
-        .endr
+        vmovdqu %ymm0, (%rsp)
+        vmovdqu %ymm0, 0x20(%rsp)
+        vmovdqu %ymm0, 0x40(%rsp)
+        vmovdqu %ymm0, 0x60(%rsp)
+        vmovdqu %ymm0, 0x80(%rsp)
+        vmovdqu %ymm0, 0xa0(%rsp)
+        vmovdqu %ymm0, 0xc0(%rsp)
+        vmovdqu %ymm0, 0xe0(%rsp)
+        vmovdqu %ymm0, 0x100(%rsp)
+        vmovdqu %ymm0, 0x120(%rsp)
+        vmovdqu %ymm0, 0x140(%rsp)
+        vmovdqu %ymm0, 0x160(%rsp)
+        vmovdqu %ymm0, 0x180(%rsp)
+        vmovdqu %ymm0, 0x1a0(%rsp)
+        vmovdqu %ymm0, 0x1c0(%rsp)
+        vmovdqu %ymm0, 0x1e0(%rsp)
+        vmovdqu %ymm0, 0x200(%rsp)
+        vmovdqu %ymm0, 0x220(%rsp)
+        vmovdqu %ymm0, 0x240(%rsp)
+        vmovdqu %ymm0, 0x260(%rsp)
+        vmovdqu %ymm0, 0x280(%rsp)
+        vmovdqu %ymm0, 0x2a0(%rsp)
+        vmovdqu %ymm0, 0x2c0(%rsp)
+        vmovdqu %ymm0, 0x2e0(%rsp)
         movq %r11, %rsp
         .cfi_def_cfa_register %rsp
         retq