Port: use consistent architecture identifier

This commit ports the change from
pq-code-package/mlkem-native#1456
to mldsa-native.

Currently, mldsa-native already uses x86_64 as the architecture
identifier for x86 in its existing HOL-Light proofs, and no changes are
required in that regard. This commit simply aligns the surrounding
scripts and infrastructure to consistently use x86_64 as the
architecture name.

- Adds the related scripts to support dual architectures by introducing
  an explicit arch parameter in the autogen process.

- Replaces the arm_or_x86 flag with a unified arch flag in test scripts.

Signed-off-by: willieyz <[email protected]>

Author: willieyz

scripts/autogen

@@ -27,7 +27,9 @@ montgomery_factor = pow(2, 32, modulus)
 _RE_DEFINED = re.compile(r"defined\(([^)]+)\)")
 _RE_MARKDOWN_CITE = re.compile(r"\[\^(?P<id>\w+)\]")
 _RE_C_CITE = re.compile(r"@\[(?P<id>\w+)")
-_RE_BYTECODE_START = re.compile(r"=== bytecode start: mldsa/([^/\s]+?)\.o")
+_RE_BYTECODE_START = re.compile(
+    r"=== bytecode start: (?:aarch64|x86_64)/mldsa/([^/\s]+?)\.o"
+)
 _RE_FUNC_SYMBOL = re.compile(r"MLD_ASM_FN_SYMBOL\((.*)\)")
 _RE_MACRO_CHECK = re.compile(r"[^_]((?:MLD_|MLDSA_)\w+)(.*)$", re.M)
 _RE_DEFINE = re.compile(r"^\s*#define\s+(\w+)")
@@ -2124,28 +2126,30 @@ def update_via_simpasm(
 
 
 def gen_hol_light_asm_file(job):
-    infile, outfile, indir, cflags = job
+    infile, outfile, indir, cflags, arch = job
     update_via_simpasm(
         f"{indir}/{infile}",
-        "proofs/hol_light/x86_64/mldsa",
+        "proofs/hol_light/" + arch + "/mldsa",
         outfile=outfile,
         cflags=cflags,
         preserve_header=False,
     )
 
 
 def gen_hol_light_asm():
-    joblist = [
+    x86_64_flags = "-mavx2 -mbmi2 -msse4 -fcf-protection=full"
+    joblist_x86_64 = [
         (
             "ntt.S",
             "mldsa_ntt.S",
             "dev/x86_64/src",
-            "-Imldsa/src/native/x86_64/src/ -mavx2 -mbmi2 -msse4 -fcf-protection=full",
+            f"-Imldsa/src/native/x86_64/src -Imldsa/src/common.h {x86_64_flags}",
+            "x86_64",
         ),
     ]
 
     with ThreadPoolExecutor() as executor:
-        _ = list(executor.map(partial(gen_hol_light_asm_file), joblist))
+        _ = list(executor.map(partial(gen_hol_light_asm_file), joblist_x86_64))
 
 
 def update_via_copy(infile_full, outfile_full, transform=None):
@@ -2914,16 +2918,30 @@ def update_bytecode_in_proof_script(filepath, bytecode):
     update_file(filepath, updated_content)
 
 
-def update_hol_light_bytecode():
-    """Update HOL Light proof files with bytecode from make dump_bytecode."""
+def update_hol_light_bytecode_for_arch(arch, force_cross=False):
     status_update(
-        "HOL Light bytecode",
-        "Running make dump_bytecode ... (this may take a few minutes)",
+        f"HOL Light bytecode ({arch})",
+        f"Running make dump_bytecode ({arch})... (this may take a few minutes)",
     )
 
+    source_arch = arch
+    if platform.machine().lower() in ["arm64", "aarch64"]:
+        native_arch = "aarch64"
+    else:
+        native_arch = "x86_64"
+
+    if native_arch != source_arch:
+        cross_prefix = f"{source_arch}-unknown-linux-gnu-"
+        cross_gcc = cross_prefix + "gcc"
+        # Check if cross-compiler is present
+        if shutil.which(cross_gcc) is None:
+            if force_cross is False:
+                return
+            raise Exception(f"Could not find cross toolchain {cross_prefix}")
+
     # Run make to get bytecode output
     result = subprocess.run(
-        ["make", "-C", "proofs/hol_light/x86_64", "dump_bytecode"],
+        ["make", "-C", "proofs/hol_light/" + arch, "dump_bytecode"],
         capture_output=True,
         text=True,
         check=True,
@@ -2935,10 +2953,15 @@ def update_hol_light_bytecode():
 
     # Update each .ml file
     for obj_name, bytecode in bytecode_dict.items():
-        ml_file = "proofs/hol_light/x86_64/proofs/" + obj_name + ".ml"
+        ml_file = "proofs/hol_light/" + arch + "/proofs/" + obj_name + ".ml"
         update_bytecode_in_proof_script(ml_file, bytecode)
 
 
+def update_hol_light_bytecode(force_cross=False):
+    """Update HOL Light proof files with bytecode from make dump_bytecode."""
+    update_hol_light_bytecode_for_arch("x86_64", force_cross=force_cross)
+
+
 def gen_test_config(config_path, config_spec, default_config_content):
     """Generate a config file by modifying the default config."""
     status_update("test configs", config_path)

scripts/tests

@@ -1000,33 +1000,33 @@ class Tests:
 
         if platform.machine().lower() in ["arm64", "aarch64"]:
             # TODO: Skip HOL-Light proofs on arm64/aarch64 until the first proof is added
-            # arm_or_x86 = "arm"
+            # arch = "aarch64"
             return
         elif platform.machine().lower() in ["x86_64"]:
-            arm_or_x86 = "x86_64"
+            arch = "x86_64"
         else:
             return
 
-        def list_proofs(arm_or_x86):
-            cmd_str = ["./proofs/hol_light/" + arm_or_x86 + "/list_proofs.sh"]
+        def list_proofs(arch):
+            cmd_str = ["./proofs/hol_light/" + arch + "/list_proofs.sh"]
             p = subprocess.run(cmd_str, capture_output=True, universal_newlines=False)
             proofs = filter(lambda s: s.strip() != "", p.stdout.decode().split("\n"))
             return list(proofs)
 
         if self.args.list_functions:
-            for p in list_proofs(arm_or_x86):
+            for p in list_proofs(arch):
                 print(p)
             exit(0)
 
-        def run_hol_light_single_step(proofs, arm_or_x86):
+        def run_hol_light_single_step(proofs, arch):
             num_proofs = len(proofs)
             for i, func in enumerate(proofs):
                 log = logger(f"HOL_LIGHT ({i+1}/{num_proofs})", None, None, None)
                 log.info(f"Starting HOL-Light proof for {func}")
                 start = time.time()
                 proof_bin = f"mldsa/{func}.native"
                 proof_target = f"mldsa/{func}.correct"
-                proof_dir = "proofs/hol_light/" + arm_or_x86
+                proof_dir = "proofs/hol_light/" + arch
                 # Remove intermediate proof files to force-rerun
                 try:
                     os.remove(os.path.join(proof_dir, proof_bin))
@@ -1039,7 +1039,7 @@ class Tests:
                         f"mldsa/{func}.correct",
                     ]
                     + self.make_j(),
-                    cwd="proofs/hol_light/" + arm_or_x86,
+                    cwd="proofs/hol_light/" + arch,
                     env=os.environ.copy(),
                     capture_output=(self.args.verbose is False),
                 )
@@ -1054,11 +1054,11 @@ class Tests:
                 else:
                     log.info(f"   SUCCESS (after {dur}s)")
 
-        proofs = list_proofs(arm_or_x86)
+        proofs = list_proofs(arch)
         if self.args.proof is not None:
             proofs = self.args.proof
 
-        run_hol_light_single_step(proofs, arm_or_x86)
+        run_hol_light_single_step(proofs, arch)
         self.check_fail()