Testable Models for SIMD Intrinsics

[karthikbhargavan]

Solution to challenge 15, resolves #173.

This PR provides testable models for core::arch intrinsics, including abstractions to streamline the process of implementing these intrinsics and their tests.

Currently there are 384 x86 intrinsics modelled, and 181 aarch64 intrinsics modelled.

The methodology for writing the models is decribed in testable-simd-models/README.md.
First, we model the SIMD types as bitvectors that can be converted to and from arrays of machine integers.
Then, we model the raw operations on these types as functions over bitvectors, while keeping as much code as possible unchanged from the Rust code in rust-lang/stdarch/crates/core_arch.
Finally, we write tests (using a generic macro) to compare the behaviour of our models with the corresponding intrinsic implementations in Rust core.

Interestingly, in the process of modeling these intrinsivcs, we found bugs in the implementation of two intrinsics, _mm256_bsrli_epi128 and _mm512_bsrli_epi128. These bugs were fixed by our PR in the 2025-06-30 version of the library. In a small way, this shows off the impact of writing testable models of the SIMD intrinsics.

The model of intrinsics defined here is also used as the basis of formal proofs of Rust programs that use intrinsics. In particular, the libcrux cryptographic library uses these models in its proofs of the post-quantum cryptographic algorithms.

As next steps, we intend to extend these testable models to a larger subset of core (beyond SIMD) and then translate these Rust models to models in F*, Rocq, and Lean, to enable proofs using our models in these backends. This work is being done as part of the hax project.

The work in this PR was primarily done by Aniket Mishra, under the supervision of Karthikeyan Bhargavan and Maxime Buyse at Cryspen.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

Thank you very much! I am yet to read the full PR, but can you please explain how the testing is actually done (as also required by the challenge spec)? I see there is a test.sh script, but I don't see it being invoked anywhere.

[karthikbhargavan]

Thanks for the quick comments. We will do another pass on this PR in the next few days.

[tautschnig]

Thank you for the documentation updates, this is really helpful. Some more comments below, but also one larger request: please include a CI job so that those tests that you created are actually run in our CI.

[feliperodri]

@karthikbhargavan could you solve the compilation failures to pass CI tests?