Fix _mm256_bsrli_epi128 shift logic and update mlkem doctest

[Arul-Sujith]

While running the full workspace test suite (cargo test --all), I encountered two isolated test failures. This PR addresses both issues to ensure the workspace builds and tests cleanly.

1. Fix _mm256_bsrli_epi128 Shift Logic in core-models

The Issue:
The core-models interpretation of the _mm256_bsrli_epi128 (AVX2 Byte Shift Right Logical Immediate) instruction was wrapping the immediate shift value (imm8) using modulo 16.

However, per the Intel Intrinsics Guide, if the byte shift value imm8 is greater than 15, the entire 128-bit lane must be zeroed out. The previous modulo logic incorrectly caused shifts of e.g., 16 to wrap around to a 0-byte shift, resulting in an assertion failure in the _mm256_bsrli_epi128 unit test:

assertion `left == right` failed
  left: [-6341777437115142865265983506360485911, -20679178649182049665911232702807607085]
 right: [0, 0]

The Fix:
Updated the implementation in crates/utils/core-models/src/core_arch/x86/interpretations.rs to explicitly check if imm8 > 15 { 0 }. The software model now accurately reflects the underlying x86 hardware behavior.

2. Update libcrux-kats Doctest for MlKemTests::load()

The Issue:
A module-level doctest in crates/testing/kats/src/wycheproof/mlkem.rs failed to compile (error[E0061]: this function takes 2 arguments but 1 argument was supplied). The function signature for MlKemTests::load() had been updated to require a second argument (group_type: TestGroupType), but the example usage in the documentation comment was left calling the function with only one argument.

The Fix:
Updated the doctest to import TestGroupType and provide TestGroupType::MlKemTest as the required second argument, restoring compilation.

Verification

Both fixes were verified locally against rustc 1.90.0:

• cargo test -p core-models _mm256_bsrli_epi128 (Passes)
• cargo test -p libcrux-kats --doc (Passes)

[karthikbhargavan]

Thank you for posting this. This was interestingly a bug in the upstream Rust core, which we caught and fixed.
https://cryspen.com/post/specify-rust-simd/

We had been waiting for the fix to land in Rust stable and you are right that we should now update the definition in our model. I believe your fix is already included in our recent intrinsics PR: #1481

Can you check whether this PR covers your bugfix? Especially see:

libcrux/crates/utils/core-models/src/core_arch/x86/interpretations.rs

Line 493 in 3ee598d

pub fn _mm256_bsrli_epi128<const IMM8: i32>(a: i128x2) -> i128x2 {

[Arul-Sujith]

I can confirm that the implementation in PR #1481 perfectly covers the bug fix I made for _mm256_bsrli_epi128

Since #1481 handles the core-models fix, should I amend this PR to remove that commit and just leave the fix for the libcrux-kats doctest compilation error?

(Also, I just opened a new PR for issue #1491 (Replacing Secret traits with inherent methods) which is ready for review!)

[jschneider-bensch]

Since #1481 handles the core-models fix, should I amend this PR to remove that commit and just leave the fix for the libcrux-kats doctest compilation error?

Thanks again for the PR! Yes, I'd like to keep the core-models related changes all in #1481, but would be happy to take your doctest fix.