HOL-Light: Add support for MacOS

The HOL-Light/s2n-bignum proofs expect ELF formatted object files,
but compilation on MacOS produces Mach-O object files.

This commit modifies the makefile for the HOL-Light proofs in mlkem-native
to explicitly convert from Mach-O to ELF using gobjcopy.

Unfortunately, there does not seem to be a way to get a version of
`objcopy` through `nix` that supports the required conversion, hence
we need to fall back to documentation and expressive error messages
to nudge the user to manually install `gobjcopy` via `brew install binutils`
when it cannot be found.

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

proofs/hol_light/arm/Makefile

@@ -69,11 +69,25 @@ OBJ = mlkem/mlkem_ntt.o mlkem/mlkem_intt.o
 # According to
 # https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms,
 # x18 should not be used for Apple platforms. Check this using grep.
+ifneq ($(OSTYPE_RESULT),Darwin)
 $(OBJ): %.o : %.S
 	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
 	cat $< | $(PREPROCESS) | $(SPLIT) | grep -v -E '^\s+.quad\s+0x[0-9a-f]+$$' | $(ASSEMBLE) -o $@ -
 	$(OBJDUMP) $@ | ( ( ! grep --ignore-case -E 'w18|[^0]x18' ) || ( rm $@ ; exit 1 ) )
 	cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ -
+else
+$(OBJ): %.o : %.S
+	@if ! (which gobjcopy >/dev/null); then \
+	  echo "gobjcopy not found. Consider installing it via 'brew install binutils', and put its parent directory (e.g. /opt/homebrew/Cellar/binutils/{VERSION}/bin) in your PATH.";\
+	  exit 1; \
+	fi
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	cat $< | $(PREPROCESS) | $(SPLIT) | grep -v -E '^\s+.quad\s+0x[0-9a-f]+$$' | $(ASSEMBLE) -o $@ -
+	$(OBJDUMP) $@ | ( ( ! grep --ignore-case -E 'w18|[^0]x18' ) || ( rm $@ ; exit 1 ) )
+	cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ -
+        # On Darwin, we need to explicitly convert Mach-O to ELF
+	gobjcopy -I mach-o-arm64 -O elf64-littleaarch64 $@ $@
+endif
 
 clean:; rm -f */*.o */*/*.o */*.correct */*.native
 

proofs/hol_light/arm/README.md

@@ -33,6 +33,18 @@ make -C proofs/hol_light/arm
 
 will build and run the proofs. Note that this make take hours even on powerful machines.
 
+### macOS (AArch64)
+
+If you want run the proofs from an AArch64 Apple machine, you need to manually install `gobjcopy` via
+
+```
+brew install binutils
+```
+
+and put its parent directory (e.g. `/opt/homebrew/Cellar/binutils/{VERSION}/bin`) into your `PATH`.
+This is needed to convert Mach-O object files to ELF (if you know a way to install a suitable version
+of `objcopy` through `nix`, please let us know!).
+
 ## What is covered?
 
 At present, this directory contains functional correctness proofs for the following functions: