Testable Models for SIMD Intrinsics #423
Conversation
|
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 |
testable-simd-models/README.md
Outdated
| } | ||
| } | ||
| ``` | ||
| Thus, we then go to to `core_arch/x86/models/avx2.rs`, and add the implementation. After some modification, it ends up looking like this. |
There was a problem hiding this comment.
Can you please elaborate on what this "implementation" needs to look like, what it can do/cannot do? I am looking at the code above and your "implementation" below and am having a hard time understanding the reasons for each of the differences.
There was a problem hiding this comment.
We added more descriptions and brought the code so much closer that the diff is encapsulated in one change: the macro switches to a function (with the same arguments).
testable-simd-models/README.md
Outdated
| To contribute new models of intrinsics, we expect the author to follow | ||
| the above steps and provide comprehensive tests. It is important that | ||
| the model author look carefully at both the Intel/ARM specification | ||
| and the Rust `stdarch` implementation, because the Rust implementation | ||
| may not necessarily be correct. |
There was a problem hiding this comment.
I find "the above steps" not particularly obvious, and they do not at all mention looking at the Intel/ARM specs (which I agree is very important). Can you please work on improving the description above so that it provides a recipe that someone else could actually follow?
There was a problem hiding this comment.
We added more explanations, comments welcome.
|
Thanks for the quick comments. We will do another pass on this PR in the next few days. |
* Provided more detailed description for how to model and test intrinsics * Restored static asserts which were in the upstream code * Switched the use of u64 back to u32 to make it closer to upstream * Defined functions like `transpose` to reduce visual diffs
| To model a defined intrinsic, we essentially copy the Rust code of | ||
| the intrinsic from `core::arch` and adapt it to use our underlying abstractions. The | ||
| changes needed to the code are sometimes scriptable, and indeed most | ||
| of our models were generated from a script, but some changes are still |
There was a problem hiding this comment.
Would it be possible to make that script available, or if it already exists in some public place, link to it?
|
|
||
| Thus, we then go to `core_arch/x86/models/avx2.rs`, and add this implementation. | ||
| The only change it requires here is that the `simd_shuffle` macro is a function in our model, | ||
| and we discard all the function attributes. |
There was a problem hiding this comment.
Can you please include a unified diff in here to make entirely explicit what the changes look like?
| let mut rng = rand::rng(); | ||
| (0..N).map(|_| rng.random::<bool>()).collect() |
There was a problem hiding this comment.
May I ask you to do two things:
- Be explicit in what seed is being used to ensure reproducible results. Perhaps set the seed at start-up and print that seed to the logs.
- Do not use a fixed seed in this: each CI run should use a different seed so that, over time, we have an even broader range of tests run. Yet, since this can cause unexpected test failures, it is important that the seed be printed somewhere as in the above item.
Solution to challenge 15, resolves #173.
This PR provides testable models for
core::archintrinsics, 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_epi128and_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
libcruxcryptographic 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.