Import NI modules of GHASH from pnmadelaine_aes branch and adds specific proofs

[mamonet]

This PR imports NI modules of GHASH from pnmadelaine_aes branch and adds specific proofs. However, the proofs use properties and definitions from Vale modules so there's still some work left before this PR can be merged.

• Galois field 2^128 abstraction (can be cloned from Vale modules since portable and Vale implementations utilize same properties)
• Equivalence lemmas of Vale specification and spec/Spec.GF128 module.
• M32 support for GHASH (can be added in a follow-up PR)

[github-actions]

[CI] Important!
The code in dist/gcc-compatible, dist/msvc-compatible, and dist/wasm
is tested on cryspen/hacl-packages.
dist is not automatically re-generated, be sure to do it manually.
(A fresh snapshot can also be downloaded from CI by going to the "artifacts" section of your run.)
Then check the following tests before merging this PR.
Always check the latest run, it corresponds to the most recent version of this branch.
All jobs are expected to be successful.
In some cases manual intervention is needed. Please ping the hacl-packages maintainers.

• Build, Test, Benchmark: Build on Linux (x86, x64), Windows (x86, x64), MacOS (x64, arm64), s390x, Android (arm64) and test on Linux (x86, x64), Windows (x86, x64), MacOS (x64).
• Performance Regression Tests: Navigate to the terminal output in “Run benchmarks”. The comparison with the main branch will be at the bottom. The run fails if the performance regresses too much.
• OCaml bindings: Build & Tests
• JS bindings: Build & Tests
• Rust bindings: Build & Tests

[msprotz]

Can you say more about why you want to clone from Vale? If the specs are there and are ok, can we make sure there's no copy-paste?

[mamonet]

I had concerns that we need to remove the dependencies to Vale modules but it turned out it's ok so there's no need to do any abstraction.

[mamonet]

@msprotz Missing equivalent lemmas are added in Vale.Math.Poly2.Galois module, and utilized to complete GHASH proofs. M32 is still not supprted but NI version is ready for review.