diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 92a392bac..4048ae518 100644 --- a/.github/workflows/ci.yml +++ b/.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 }} diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 896093879..82b53c3e3 100644 --- a/.github/workflows/nix.yml +++ b/.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 diff --git a/flake.nix b/flake.nix index 82b641b85..7da8bd268 100644 --- a/flake.nix +++ b/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,6 +91,7 @@ # arm-none-eabi-gcc + platform files from pqmx packages.m55-an547 = util.m55-an547; + packages.avr-toolchain = util.avr-toolchain; devShells.arm-embedded = util.mkShell { packages = builtins.attrValues { @@ -94,17 +99,20 @@ 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; }; }; diff --git a/proofs/hol_light/x86_64/Makefile b/proofs/hol_light/x86_64/Makefile index a045a9b58..5b201e2f7 100644 --- a/proofs/hol_light/x86_64/Makefile +++ b/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 diff --git a/scripts/autogen b/scripts/autogen index 8691e7198..2f43cd5d8 100755 --- a/scripts/autogen +++ b/scripts/autogen @@ -2914,16 +2914,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, @@ -2935,10 +2949,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) @@ -3164,7 +3185,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() diff --git a/scripts/simpasm b/scripts/simpasm index 010969d28..289eac4c1 100755 --- a/scripts/simpasm +++ b/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