testing: HOL-Light: add support for cross-proofing

This commit introduces two new flags to the hol_light command of the
tests script. The first allows user specification of which architecture to
run/list the proofs for and the second allows for entering the nix
cross-compilation devshell for that architecture. If either are not
passed, the behavior is unchanged.

Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>

Author: L-series

scripts/tests

@@ -1017,7 +1017,9 @@ class Tests:
 
     def hol_light(self):
 
-        if platform.machine().lower() in ["arm64", "aarch64"]:
+        if self.args.arch:
+            arch = self.args.arch
+        elif platform.machine().lower() in ["arm64", "aarch64"]:
             arch = "aarch64"
         elif platform.machine().lower() in ["x86_64"]:
             arch = "x86_64"
@@ -1050,12 +1052,14 @@ class Tests:
                     os.remove(os.path.join(proof_dir, proof_target))
                 except FileNotFoundError:
                     pass
+
+                make_cmd = [
+                    "make",
+                    f"mlkem/{func}.correct",
+                ]
+
                 p = subprocess.run(
-                    [
-                        "make",
-                        f"mlkem/{func}.correct",
-                    ]
-                    + self.make_j(),
+                    make_cmd,
                     cwd="proofs/hol_light/" + arch,
                     env=os.environ.copy(),
                     capture_output=(self.args.verbose is False),
@@ -1481,6 +1485,14 @@ def cli():
         default=False,
     )
 
+    hol_light_parser.add_argument(
+        "-a",
+        "--arch",
+        help="Architecture for which to list/run HOL_LIGHT proofs (aarch64 or x86_64).",
+        choices=["aarch64", "x86_64"],
+        default=None,
+    )
+
     # func arguments
     func_parser = cmd_subparsers.add_parser(
         "func",