CR fixes

Signed-off-by: Jake Massimo <[email protected]>

Author: jakemas

dev/x86_64/src/ntt.S

@@ -267,7 +267,6 @@ vmovdqa		%ymm11,256*\off+224(%rdi)
 .balign 4
 .global MLD_ASM_NAMESPACE(ntt_avx2)
 MLD_ASM_FN_SYMBOL(ntt_avx2)
-endbr64
 vmovdqa		MLD_AVX2_BACKEND_DATA_OFFSET_8XQ*4(%rsi),%ymm0
 
 levels0t1	0

proofs/hol_light/x86_64/README.md

@@ -71,6 +71,15 @@ be the code under verification as part of the precondition. For example, the fol
        MAYCHANGE [memory :> bytes(a,1024)])`
 ```
 
+## Platform Compatibility
+
+These x86_64 assembly proofs are expected to work on the following platforms:
+
+- **Linux x86_64**: Fully supported (native build and execution)
+- **Linux AArch64**: Not currently supported. Requires x86_64 cross-compilation tools (`x86_64-linux-gnu-as` and `x86_64-linux-gnu-objdump`).
+- **macOS x86_64**: Fully supported (native build and execution)
+- **macOS ARM (Apple Silicon)**: Not currently supported. Differences in assembler behavior between clang-based (macOS) and gcc-based (Linux) toolchains can cause verification mismatches, particularly with regard to argument ordering optimizations for commutative instructions.
+
 ## Reproducing the proofs
 
 To reproduce the proofs, enter the nix shell via

scripts/autogen

@@ -1630,7 +1630,7 @@ def gen_hol_light_asm():
             "ntt.S",
             "mldsa_ntt.S",
             "dev/x86_64/src",
-            "-Imldsa/src/native/x86_64/src/ -mavx2 -mbmi2 -msse4 -fcf-protection=none",
+            "-Imldsa/src/native/x86_64/src/ -mavx2 -mbmi2 -msse4 -fcf-protection=full",
         ),
     ]