Derive Arbitrary for various core_arch::x86 types

.github/workflows/goto-transcoder.yml

@@ -27,6 +27,8 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
+      - name: Apply stdarch patch
+        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Generate contracts programs
       - name: Generate contracts

.github/workflows/kani-metrics.yml

@@ -18,7 +18,9 @@ jobs:
       uses: actions/checkout@v4
       with:
         submodules: true
-
+    - name: Apply stdarch patch
+      run: cd library/stdarch && patch -p1 < ../../stdarch.patch
+
     # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
     - name: Set up Python
       uses: actions/setup-python@v4

.github/workflows/kani.yml

@@ -43,7 +43,9 @@ jobs:
         with:
           path: head
           submodules: true
-
+      - name: Apply stdarch patch
+        run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch
+
       # Step 2: Install jq
       - name: Install jq
         if: matrix.os == 'ubuntu-latest'
@@ -72,18 +74,24 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
+      - name: Apply stdarch patch
+        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run Kani autoharness on the std library for selected functions.
       # Uses "--include-pattern" to make sure we do not try to run across all
       # possible functions as that may take a lot longer than expected. Instead,
       # explicitly list all functions (or prefixes thereof) the proofs of which
       # are known to pass.
+      # Notes:
+      # - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
+      #   core_arch::x86:: functions that are known to verify successfully.
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern core_arch::x86::__m128d::as_f64x2 \
             --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
@@ -136,6 +144,8 @@ jobs:
         with:
           path: head
           submodules: true
+      - name: Apply stdarch patch
+        run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run list on the std library
       - name: Run Kani List
@@ -168,6 +178,8 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
+      - name: Apply stdarch patch
+        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run autoharness analyzer on the std library
       - name: Run Autoharness Analyzer

stdarch.patch

@@ -0,0 +1,51 @@
+--- a/crates/core_arch/src/aarch64/neon/mod.rs
++++ b/crates/core_arch/src/aarch64/neon/mod.rs
+@@ -2,6 +2,9 @@
+
+ #![allow(non_camel_case_types)]
+
++#[cfg(kani)]
++use crate::kani;
++
+ #[rustfmt::skip]
+ mod generated;
+ #[rustfmt::skip]
+--- a/crates/core_arch/src/arm_shared/neon/mod.rs
++++ b/crates/core_arch/src/arm_shared/neon/mod.rs
+@@ -1,5 +1,8 @@
+ //! ARMv7 NEON intrinsics
+
++#[cfg(kani)]
++use crate::kani;
++
+ #[rustfmt::skip]
+ mod generated;
+ #[rustfmt::skip]
+--- a/crates/core_arch/src/macros.rs
++++ b/crates/core_arch/src/macros.rs
+@@ -128,6 +128,15 @@ macro_rules! types {
+             }
+         }
+
++        #[cfg(kani)]
++        $(#[$stability])+
++        impl kani::Arbitrary for $name {
++            fn any() -> Self {
++                let data: [$elem_type; $len] = kani::any();
++                Self { 0: data }
++            }
++        }
++
+         $(#[$stability])+
+         impl crate::fmt::Debug for $name {
+             #[inline]
+--- a/crates/core_arch/src/x86/mod.rs
++++ b/crates/core_arch/src/x86/mod.rs
+@@ -1,5 +1,7 @@
+ //! `x86` and `x86_64` intrinsics.
+
++#[cfg(kani)]
++use crate::kani;
+ use crate::mem::transmute;
+
+ #[macro_use]