test

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

flake.nix

@@ -120,6 +120,12 @@
           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

@@ -26,17 +26,20 @@ ARCHFLAGS=-march=armv8.4-a+sha3
 # 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
-COMPILE=$(CROSS_PREFIX)$(CC)
+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
@@ -46,9 +49,9 @@ COMPILE=$(CROSS_PREFIX)$(CC)
 # by single-quote characters in comments, so we eliminate // comments first.
 
 ifeq ($(OSTYPE_RESULT),Darwin)
-PREPROCESS=sed -e 's/\/\/.*//' | $(COMPILE) -E -xassembler-with-cpp -
+PREPROCESS=sed -e 's/\/\/.*//' | $(CC) -E -xassembler-with-cpp -
 else
-PREPROCESS=$(COMPILE) $(ARCHFLAGS) -E -xassembler-with-cpp -
+PREPROCESS=$(CC) -E -xassembler-with-cpp -
 endif
 
 # Generally GNU-type assemblers are happy with multiple instructions on