HOL-Light: Allow cross-generation of byte code

.github/workflows/ci.yml

@@ -725,15 +725,63 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        system: [ubuntu-latest, ubuntu-24.04-arm]
-    runs-on: ${{ matrix.system }}
+        target:
+          - system: macos-latest
+            nix_shell: 'ci-cross-x86_64'
+            nix_cache: 'true'
+            extra_args: '--force-cross'
+          # TODO: This does not yet work (#1304) <- MLKEM ISSUE, Port when fixed
+          # - system: macos-15-intel
+          #   nix_cache: 'false'
+          #   nix_shell: 'ci'
+          - system: ubuntu-latest
+            nix_shell: 'ci-cross-aarch64'
+            nix_cache: 'true'
+            extra_args: '--force-cross'
+          - system: ubuntu-24.04-arm
+            nix_shell: 'ci-cross-x86_64'
+            nix_cache: 'true'
+            extra_args: '--force-cross'
+    runs-on: ${{ matrix.target.system }}
     name: Check autogenerated files
     steps:
       - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
       - uses: ./.github/actions/setup-shell
         with:
-          nix-shell: 'ci-cross' # Need cross-compiler for ASM simplification
-          nix-cache: 'true'
+          nix-shell: ${{ matrix.target.nix_shell }}
+          nix-cache: ${{ matrix.target.nix_cache }}
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            python3 ./scripts/autogen --dry-run ${{ matrix.target.extra_args }}
+  check_hol_light_object_code:
+    strategy:
+      fail-fast: false
+      matrix:
+        target:
+          - system: macos-latest
+            nix_cache: 'true'
+            nix_shell: 'hol_light-cross-x86_64'
+            extra_args: '--force-cross'
+          # TODO: autogen does not yet work on macos15-intel (#1304)
+          # - system: macos-15-intel
+          #   nix_cache: 'false'
+          #   nix_shell: 'ci'
+          - system: ubuntu-latest
+            nix_shell: 'hol_light-cross-aarch64'
+            nix_cache: 'true'
+            extra_args: '--force-cross'
+          - system: ubuntu-24.04-arm
+            nix_shell: 'hol_light-cross-x86_64'
+            nix_cache: 'true'
+            extra_args: '--force-cross'
+    runs-on: ${{ matrix.target.system }}
+    name: Check object code in HOL-Light proofs
+    steps:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+      - uses: ./.github/actions/setup-shell
+        with:
+          nix-shell: ${{ matrix.target.nix_shell }}
+          nix-cache: ${{ matrix.target.nix_cache }}
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           script: |
-            python3 ./scripts/autogen --dry-run --force-cross
+            python3 ./scripts/autogen --dry-run --update-hol-light-bytecode ${{ matrix.target.extra_args }}

.github/workflows/nix.yml

@@ -69,10 +69,11 @@ jobs:
           devShell: ci
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           script: |
-            # NOTE: we're not running cross compilation tests on macOS currently
-            #       and building cross compilation toolchain on macOS runner took
-            #       extremely long time
-            if [[ ${{ runner.os }} != 'macOS' ]]; then
+            # We only run cross-compilation checks for x86 on macos-latest,
+            # so restrict caching to the corresponding cross shell.
+            if [[ ${{ runner.os }} == 'macOS' ]]; then
+              nix develop .#ci-cross-x86_64 --profile tmp-cross
+            else
               nix develop .#ci-cross --profile tmp-cross
               # GH ubuntu-24.04 image tend to run outof space
               if [[ ${{ matrix.runner }} == 'ubuntu-24.04' ]]; then

flake.nix

@@ -43,6 +43,10 @@
                 '')
             ];
           };
+          holLightShellHook = ''
+            export PATH=$PWD/scripts:$PATH
+            export PROOF_DIR="$PWD/proofs/hol_light"
+          '';
         in
         {
           _module.args.pkgs = import inputs.nixpkgs {
@@ -87,24 +91,28 @@
 
           # arm-none-eabi-gcc + platform files from pqmx
           packages.m55-an547 = util.m55-an547;
+          #packages.avr-toolchain = util.avr-toolchain; # TODO The AVR shell is currently unavaliable for mldsa-native
           devShells.arm-embedded = util.mkShell {
             packages = builtins.attrValues
               {
                 inherit (config.packages) m55-an547;
                 inherit (pkgs) gcc-arm-embedded qemu coreutils python3 git;
               };
           };
+
+          devShells.avr = util.mkShell (import ./nix/avr { inherit pkgs; });
           devShells.hol_light = (util.mkShell {
-            packages = builtins.attrValues {
-              inherit (config.packages) linters hol_light s2n_bignum;
-            };
-          }).overrideAttrs (old: {
-            shellHook = ''
-              export PATH=$PWD/scripts:$PATH
-              # Set proof directory for x86_64
-              export PROOF_DIR_X86_64="$PWD/proofs/hol_light/x86_64"
-            '';
-          });
+            packages = builtins.attrValues { inherit (config.packages) linters hol_light s2n_bignum; };
+          }).overrideAttrs (old: { shellHook = holLightShellHook; });
+          devShells.hol_light-cross = (util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum; };
+          }).overrideAttrs (old: { shellHook = holLightShellHook; });
+          devShells.hol_light-cross-aarch64 = (util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum; };
+          }).overrideAttrs (old: { shellHook = holLightShellHook; });
+          devShells.hol_light-cross-x86_64 = (util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64 hol_light s2n_bignum; };
+          }).overrideAttrs (old: { shellHook = holLightShellHook; });
           devShells.ci = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) linters toolchains_native; };
           };

proofs/hol_light/x86_64/Makefile

@@ -19,6 +19,19 @@ ARCHTYPE_RESULT=$(shell uname -m)
 SRC ?= $(S2N_BIGNUM_DIR)
 SRC_X86 ?= $(SRC)/x86
 
+# If actually on an x86_64 machine, just use the assembler (as). Otherwise
+# use a cross-assembling version so that the code can still be assembled
+# and the proofs checked against the object files (though you won't be able
+# to run code without additional emulation infrastructure).
+ifeq ($(filter $(ARCHTYPE_RESULT),x86_64),)
+CROSS_PREFIX=x86_64-unknown-linux-gnu-
+ifeq ($(shell command -v $(ASSEMBLE) >/dev/null 2>&1 && echo yes || echo no),no)
+$(error Cross-toolchain not found. Please run in the 'hol_light-cross-x86_64' nix shell via: nix develop .#hol_light-cross-x86_64)
+endif
+endif
+ASSEMBLE=$(CROSS_PREFIX)as $(ARCHFLAGS)
+OBJDUMP=$(CROSS_PREFIX)objdump -d
+
 # Add explicit language input parameter to cpp, otherwise the use of #n for
 # numeric literals in x86 code is a problem when used inside #define macros
 # since normally that means stringization.
@@ -37,29 +50,6 @@ endif
 
 SPLIT=tr ';' '\n'
 
-# If actually on an x86_64 machine, just use the assembler (as). Otherwise
-# use a cross-assembling version so that the code can still be assembled
-# and the proofs checked against the object files (though you won't be able
-# to run code without additional emulation infrastructure). For the clang
-# version on OS X we just add the "-arch x86_64" option. For the Linux/gcc
-# toolchain we assume the presence of the special cross-assembler. This
-# can be installed via something like:
-#
-#  sudo apt-get install binutils-x86-64-linux-gnu
-
-ifeq ($(ARCHTYPE_RESULT),x86_64)
-ASSEMBLE=as
-OBJDUMP=objdump -d
-else
-ifeq ($(OSTYPE_RESULT),Darwin)
-ASSEMBLE=as -arch x86_64
-OBJDUMP=otool -tvV
-else
-ASSEMBLE=x86_64-linux-gnu-as
-OBJDUMP=x86_64-linux-gnu-objdump -d
-endif
-endif
-
 OBJ = mldsa/mldsa_ntt.o
 
 # Build object files from assembly sources

scripts/autogen

@@ -2920,16 +2920,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,
@@ -2941,10 +2955,17 @@ 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."""
+    # NOTE: The following line is commented out until there are hol_light aarch64 proofs.
+    # update_hol_light_bytecode_for_arch("aarch64", force_cross=force_cross)
+    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)
@@ -3170,7 +3191,7 @@ def _main():
     high_level_status("Completed final backend synchronization")
 
     if args.update_hol_light_bytecode:
-        update_hol_light_bytecode()
+        update_hol_light_bytecode(args.force_cross)
         high_level_status("Updated HOL Light bytecode")
 
     gen_monolithic_source_file()

scripts/simpasm

@@ -247,7 +247,7 @@ def simplify(logger, args, asm_input, asm_output=None):
             logger.debug(f"Using raw global symbol {sym} going forward ...")
 
         cmd = [args.objdump, "--disassemble", tmp_objfile0]
-        if platform.system() == "Darwin":
+        if platform.system() == "Darwin" and args.arch == "aarch64":
             cmd += ["--triple=aarch64"]
 
         # Add syntax option if specified