Import AES-CTR32 modules from pnmadelaine_aes branch and add NI proofs

[mamonet]

This PR imports AES-CTR32 modules from pnmadelaine_aes branch and adds proofs for NI functions.

[github-actions[bot]]

[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

[mamonet]

The fact that the arguments to the (unverified) macro glue were in the wrong order makes me... slightly nervous

The order of arguments were flipped in the implementation side of F* code, but it doesn't meet the argument order in spec. To make the order consistent, I could either change the order for impl and spec or in libintvector.h I went for the later.

[franziskuskiefer]

@msprotz @karthikbhargavan what's the state here?