Add support for Hacl_AES_128_GCM_NI and Hacl_AES_128_GCM_M32

[mamonet]

This patch adds the following changes:

• Extracted C files of Hacl_AES_128_GCM_NI and Hacl_AES_128_GCM_M32 from Low* modules
• Support x86 and AArch64 C intrinsics for AES and CLMUL/PMULL in libintvector.h
• Detect cpu features of aes and pmull on AArch64
• Integrate functions of both NI and M32 modules with EverCrypt_AEAD_encrypt/decrypt() conditionally using cpu features
• Add BearSSL CT64 implementation of AES-GCM in third-party directory for benchmark reference
• Impalement benchmark module for AES-GCM mode that tests encrypt and AAD functions for various message sizes

[cla-bot[bot]]

We require contributors to sign our Contributor License Agreement https://github.com/cryspen/hacl/blob/main/CLA.md ensuring that the contribution can be licensed under Apache 2.0 and MIT. In order for us to review and merge your code, please mention @cryspen/core in a comment below to get yourself added.

[cla-bot[bot]]

We require contributors to sign our Contributor License Agreement https://github.com/cryspen/hacl/blob/main/CLA.md ensuring that the contribution can be licensed under Apache 2.0 and MIT. In order for us to review and merge your code, please mention @cryspen/core in a comment below to get yourself added.

[coveralls]

Pull Request Test Coverage Report for Build 5808703668

• 3051 of 7433 (41.05%) changed or added relevant lines in 12 files are covered.
• 11 unchanged lines in 1 file lost coverage.
• Overall coverage decreased (-1.4%) to 51.361%

---

Changes Missing Coverage	Covered Lines	Changed/Added Lines	%
src/Hacl_AES_128_GCM_CT64.c	105	153	68.63%
src/Hacl_AES_256_GCM_CT64.c	105	153	68.63%
src/Hacl_Gf128_CT64.c	1670	1756	95.1%
src/Hacl_AES_256_GCM_NI.c	0	129	0.0%
src/Hacl_AES_128_CTR32_BitSlice.c	698	976	71.52%
src/Hacl_Gf128_NI.c	0	297	0.0%
src/Hacl_AES_128_GCM_NI.c	0	353	0.0%
src/Hacl_AES_256_CTR32_BitSlice.c	206	570	36.14%
src/EverCrypt_AEAD.c	118	517	22.82%
src/Hacl_AES_128_CTR32_NI.c	0	1020	0.0%
<!--	Total:	3051	7433	41.05%	-->

Files with Coverage Reduction	New Missed Lines	%
src/EverCrypt_AEAD.c	11	26.49%
<!--	Total:	11		-->

Totals
Change from base Build 5655291623:	-1.4%
Covered Lines:	31975
Relevant Lines:	62256

---

💛 - Coveralls

[franziskuskiefer]

Thanks! I'll try to look at this today or tomorrow. It looks like some CI jobs are failing. Can you have a look at them?

[mamonet]

MSVC specific tests fail along with some other tests, I'm going to investigate what triggers that.

[mamonet]

I am having difficulty reproducing opam build error, opam install . --verbose --with-test --yes proceeds successfully on my setup. Do you have any suggestions?

[franziskuskiefer]

The ocaml build seems to fail.

[mamonet]

I updated the PR with the following changes

• Add AES-256 modules
• Implement GHASH CT64
• Integrate NI and CT64 functions in EverCrypt_AEAD_encrypt/decrypt_expand_aes_gcm() and EverCrypt_AEAD_encrypt/decrypt_expand_aes_gcm_no_check()

New implementations have passed Wycheproof tests successfully.

GHASH performance measured on intel i5-10300H, built with clang -O3	Low* (CT64)	BearSSL (CT64)	OpenSSL (no-asm)
12.349148 cpb	12.715595 cpb	13.449064 cpb

[mamonet]

The imported C files of AESGCM are generated from this branch https://github.com/mamonet/hacl-star/tree/pnmadelaine_aes that has the latest changes committed here. PreComp implementation of ghash is removed and replaced with CT64 which is ~2.5x faster than the former. Also, hardware-accelerated implementation and CT64 share the same algorithm of 128x128->256 multiplication phase and identical 256->128 reduction phase that increases the shared code base and remove a considerable amount of distinctive definitions, properties, lemmas, and pre-computed tables.

[franziskuskiefer]

Rust and ocaml appear to be missing the hacl CPU detection

• OCaml: EverCrypt_AEAD.c:(.text+0x12d): undefined reference tohacl_aesgcm_support'`
• Rust: Undefined symbols for architecture x86_64: "_hacl_aesgcm_support"

[mamonet]

@franziskuskiefer I discussed the issue of checking runtime cpu features inside Evercrypt module with Jonathan yesterday. For x86 architectures that support AES-NI and CLMUL, the execution flow will go down Vale route and calling NI accelerated functions from inside Evercrypt only benefits armv8-a+ architectures which IMO not worth the trade-off with simplicity as there is no easy workaround for the issue. Calling AESGCM Vale functions conditionally with the portable ones in Evercrypt.AEAD is plain and simple way to make sure the function works on all architectures while unfolds Vale power on modern x86_64 processors. Let me know if this path makes sense to you, I'm working on the changes in F* side and will update the PR once I'm able to produce the generated C code of this design.