Emulate arm64 binary on x86_64 machine

[potsrevennil]

I added scripts/tests (should be able to be executed by simply typing tests in nix shell) for functional, kat and nistkat tests.

The script currently automatically detects the host system and decides to run natively on ARM64 machines or emulate on QEMU for x86_64 machines. We might want to add the capability to manually specify whether to run tests natively or on QEMU in the future. However, I don't think we need this functionality for now.

Usage of the script is as follow:

> tests --help
Usage: tests [OPTIONS] COMMAND [ARGS]...

Options:
  --help  Show this message and exit.

Commands:
  func     Run the functional tests for all parameter sets
  kat      Run the kat tests for all parameter sets
  nistkat  Run the nistkat tests for all parameter sets
  run      Run the specified binary file

> tests nistkat --help
Usage: tests nistkat [OPTIONS]

Options:
  -v, --verbose  Show verbose output or not
  --help         Show this message and exit.

I have also added black as the Python formatter and updated the format and lint scripts to utilize it for checking the format of Python scripts. I don't have a strong opinion on the choice of Python formatter, so if there are any better suggestions, I am open to using them.

I made CI continues even when some part of the tests failed as @hanno-becker suggested in https://github.com/pq-code-package/mlkem-c-aarch64/issues/48 (sorry about that I somehow missed the message last week).

• emulate arm64 binary on x86_64 machine
• Output binaries to bin/ directory
• add nistkat checksum back
• use black for python formatting
• add tests script for running a specify binary
• factor out the common part of compiling and running a binary
• add test command for func, nistkat and kat tests
• compare tests result to the META file
• add github step summary to tests script if the env var exists
• update ci to use the tests script
• cleanup
• only add -static if is linux x86_64
• still run kat/nistkat tests even if previous tests failed

[hanno-becker]

I understand that we want developers to use nix, but I think a bare make should work out of the box on standard environments -- just to satisfy people who are curious about the repo and want to give it a very quick try.

Can we keep make working outside of the nix environment @potsrevennil ?

[potsrevennil]

@hanno-becker I'm not sure if I understand you correctly

nix is only used for specifying dependencies here, so make can definitely work outside of the nix shell. However, users will need to install all the dependencies themselves, and how they do this is out of scope for this PR, I think. For different users and different machines, there might be many ways to install all the dependencies, and nix is provided especially for those who want to give a quick try. If someone wants to do this without nix, there's not much we can do, but as long as they have qemu and gcc pre-installed, building with make should work.

To be more clear, there are two external dependencies for make: qemu and gcc. I assumed these dependencies should be available in the user's shell environment, though the shell does not need to be a nix shell. Users can make these dependencies available in any way they like if they are not using nix, or overwrite the Makefile variables via command line arguments.

[hanno-becker]

@potsrevennil Ok, I'll have another look. When I try make outside of the nix shell, I get

% make
make: *** No rule to make target `bin/test_kyber768', needed by `mlkem'.  Stop.

Does it work for you?

[potsrevennil]

@hanno-becker Oh, this is not what I intended...

It seems like a incompatibility issue of different version of make, which version of make are you using ?

I tested on my macOS, under x86_64 environment I got GNU Make 3.81 ... built for i386-apple-darwin11.3.0, and it result in the same issue as yours

While under aarch64 environment of my macOS and nix shell, I have GNU Make 4.4.1 Built for aarch64-apple-darwin23.0.0 and GNU Make 4.4.1 Built for aarch64-apple-darwin23.4.0 respectively, which worked just fine.

I pushed a new version which should resolve this issue, but maybe we would also want to fix a version of make, or have a way to make sure that the makefile is compatible for different version of make

[hanno-becker]

@potsrevennil Can we remove the macros, even if it means a bit of repetition between the makefile targets?

[potsrevennil]

@hanno-becker Done, please have a look again, thanks

[hanno-becker]

Minor comment regarding qemu on AArch64 systems.

[hanno-becker]

Mostly LGTM, but can we keep the make output in the CI logs?

[hanno-becker]

@potsrevennil

Currently, I see the following in the CI log:

DEBUG > Emulating test/bin/gen_KAT512 with QEMU
  CC      
mlkem/poly.c: In function ‘pqcrystals_kyber512_ref_scalar_compress_q_16’:
mlkem/poly.c:27: warning: ignoring ‘#pragma CPROVER check’ [-Wunknown-pragmas]
   27 | #pragma CPROVER check push

Is there a way to show the full command line?

[potsrevennil]

Ah, yes! Let me see how to do it

[hanno-becker]

Thanks a lot @potsrevennil, LGTM