Add functional correctness proofs for AArch64-optimized NTT and invNTT in HOL Light

[potsrevennil]

Summary:

• Resolves Add HOL-Light & s2n-bignum infrastructure to nix environment #603

Steps:

• The makefile in s2n-bignum/arm/ is copied to proofs/hol_light and adjusted to be compatible with nix.
• The nix patches for hol_light and s2n-bignum mainly fix the path issue (e.g. using relative paths) of the 2 projects.

Performed local tests:

• lint passing
• tests all passing
• tests bench passing
• tests cbmc passing

Do you expect this change to impact performance: Yes/No

If yes, please provide local benchmarking results.

[hanno-becker]

Something is still fishy in the Makefile target for object files -- see comments.

Also, the following fails:

make -j8 p256/bignum_montmul_p256.native
$S2N_BIGNUM_DIR/tools/run-proof.sh ./p256/bignum_montmul_p256.native ./p256_output
> Fatal error: exception Failure("dest_cons4: 4-byte inst code 2839547939 != first 4 bytes of []")

Could you also add a brief README that explains what one should do to fully compile + run a proof, and refer to the nix environment for setup? Is it feasible to run at least one proof in CI to confirm that the setup is functional? (e.g. a "hol-light sanity check" job or similar)

[hanno-becker]

Thank you @potsrevennil for fixing the Makefile issue.

Something is still not right, though:

make -j8 p256/bignum_montmul_p256.correct

continues to fail with

Fatal error: exception Failure("dest_cons4: 4-byte inst code 2839547939 != first 4 bytes of []")
make: *** [Makefile:440: p256/bignum_montmul_p256.correct] Error 2

[rod-chapman]

I have tried to reproduce proof results on macOS. In short:

1. pulled and checked out this branch.
2. Re-started NIX
3. cd proofs/hol_light/arm
4. make
   terminates with

Fatal error: exception Failure("not an ELF file")
mlkem/mlkem_ntt.native had errors!
make: *** [Makefile:112: mlkem/mlkem_ntt.correct] Error 1

[rod-chapman]

I note that

$ file mlkem/mlkem_ntt.o
mlkem/mlkem_ntt.o: Mach-O 64-bit arm64 object

which is obviously "not an ELF file". Is this the problem?

[hanno-becker]

Yes, s2n-bignum/HOL-Light's object file parser only supports ELF

[rod-chapman]

To confirm this PR is working OK, we need a testcase which is much smaller and faster than either NTT or INTT. What's the smallest, simplest, fastest proof that we can add?

[hanno-becker]

We've tested small examples before. Now the PR is targeting the actual ML-KEM proofs.

[rod-chapman]

I have reproduced the proofs successfully on an EC2 Graviton 3 (c7g) machine, running Ubuntu 24.04.

[hanno-becker]

Thanks @potsrevennil for the work!