HOL-Light: Add support for cross-compilation

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

.github/workflows/ci.yml

@@ -677,6 +677,34 @@ jobs:
       verbose: true
       cflags: "-O0"
     secrets: inherit
+  check_hol_light_bytecode:
+    strategy:
+      fail-fast: false
+      matrix:
+        target:
+          - system: macos-latest
+            nix_shell: hol_light
+            nix_cache: false
+          - system: macos-intel
+            nix_shell: hol_light
+            nix_cache: false
+          - system: ubuntu-latest
+            nix_shell: hol_light-cross-aarch64
+            nix_cache: true
+          - system: pqcp-arm64
+            nix_shell: hol_light
+            nix_cache: false
+    runs-on: ${{ matrix.target.system }}
+    name: Check HOL-Light bytecode ${{ matrix.target.system }}
+    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 --update-hol-light-bytecode
   check_autogenerated_files:
     strategy:
       fail-fast: false
@@ -693,11 +721,3 @@ jobs:
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           script: |
             python3 ./scripts/autogen --dry-run --force-cross
-      - uses: ./.github/actions/setup-shell
-        # Building the HOL-Light bytecode currently requires native compilation
-        if: ${{ matrix.system == 'pqcp-arm64' }}
-        with:
-          nix-shell: 'hol_light'
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          script: |
-            python3 ./scripts/autogen --dry-run --update-hol-light-bytecode

flake.nix

@@ -117,6 +117,15 @@
           devShells.ci-slothy = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) slothy linters toolchains_native; };
           };
+          devShells.hol_light-cross = util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum; };
+          };
+          devShells.hol_light-cross-aarch64 = util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum; };
+          };
+          devShells.hol_light-cross-x86_64 = util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64 hol_light s2n_bignum; };
+          };
           devShells.ci-cross = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) linters toolchains; };
           };

proofs/hol_light/arm/Makefile

@@ -19,53 +19,46 @@ ARCHTYPE_RESULT=$(shell uname -m)
 SRC ?= $(S2N_BIGNUM_DIR)
 SRC_ARM ?= $(SRC)/arm
 
+ARCHFLAGS=-march=armv8.4-a+sha3
+
+# If actually on an AArch64 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 ($(ARCHTYPE_RESULT)-$(OSTYPE_RESULT),x86_64-Darwin)
+ASSEMBLE=as -arch arm64
+OBJDUMP=otool -tvV
+else
+ifeq ($(filter $(ARCHTYPE_RESULT),aarch64 arm64),)
+CROSS_PREFIX=aarch64-unknown-linux-gnu-
+# Check if cross-toolchain exists
+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' nix shell via: nix develop .#hol_light)
+endif
+endif
+ASSEMBLE=$(CROSS_PREFIX)as $(ARCHFLAGS)
+OBJDUMP=$(CROSS_PREFIX)objdump -d
+endif
+
 # Add explicit language input parameter to cpp, otherwise the use of #n for
 # numeric literals in ARM code is a problem when used inside #define macros
 # since normally that means stringization.
 #
 # Some clang-based preprocessors seem to behave differently, and get confused
 # by single-quote characters in comments, so we eliminate // comments first.
 
-ARCHFLAGS=-march=armv8.4-a+sha3
 ifeq ($(OSTYPE_RESULT),Darwin)
 PREPROCESS=sed -e 's/\/\/.*//' | $(CC) -E -xassembler-with-cpp -
 else
-PREPROCESS=$(CC) $(ARCHFLAGS) -E -xassembler-with-cpp -
+PREPROCESS=$(CC) -E -xassembler-with-cpp -
 endif
 
 # Generally GNU-type assemblers are happy with multiple instructions on
 # a line, but we split them up anyway just in case.
 
 SPLIT=tr ';' '\n'
 
-# If actually on an ARM8 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 arm64" 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-aarch64-linux-gnu
-
-ifeq ($(ARCHTYPE_RESULT),aarch64)
-ASSEMBLE=as $(ARCHFLAGS)
-OBJDUMP=objdump -d
-else
-ifeq ($(ARCHTYPE_RESULT),arm64)
-ASSEMBLE=as $(ARCHFLAGS)
-OBJDUMP=objdump -d
-else
-ifeq ($(OSTYPE_RESULT),Darwin)
-ASSEMBLE=as -arch arm64
-OBJDUMP=otool -tvV
-else
-ASSEMBLE=aarch64-linux-gnu-as $(ARCHFLAGS)
-OBJDUMP=aarch64-linux-gnu-objdump -d
-endif
-endif
-endif
-
 OBJ = mlkem/mlkem_ntt.o                                   \
       mlkem/mlkem_intt.o                                  \
       mlkem/mlkem_poly_tomont.o                           \

scripts/simpasm

@@ -246,7 +246,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