HOL-Light: Add support for cross-compilation

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

Author: hanno-becker

.github/workflows/ci.yml

@@ -688,16 +688,8 @@ jobs:
       - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
       - uses: ./.github/actions/setup-shell
         with:
-          nix-shell: 'ci-cross' # Need cross-compiler for ASM simplification
+          nix-shell: 'hol_light-cross' # Need cross-compiler for ASM simplification
           nix-cache: 'true'
           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
+            python3 ./scripts/autogen --dry-run --force-cross --update-hol-light-bytecode

flake.nix

@@ -117,6 +117,9 @@
           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.ci-cross = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) linters toolchains; };
           };

proofs/hol_light/arm/Makefile

@@ -19,53 +19,43 @@ 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 ($(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
+COMPILE=$(CROSS_PREFIX)$(CC)
+
 # 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 -
+PREPROCESS=sed -e 's/\/\/.*//' | $(COMPILE) -E -xassembler-with-cpp -
 else
-PREPROCESS=$(CC) $(ARCHFLAGS) -E -xassembler-with-cpp -
+PREPROCESS=$(COMPILE) $(ARCHFLAGS) -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