Derive Arbitrary for various core_arch::x86 types

This enables autoharness to generate an additional 4067 harnesses (and
successfully prove 363 of them).

Using a patch instead of directly modifying the source code here for
`library/stdarch` is a git submodule. Modifying the source code directly
would require forking that other repository, tweaking our submodule
pointer, and thereby causing additional challenges for our fork update
automation.

The long-term solution should be automated derive-arbitrary support in
autoharness.

Author: tautschnig

.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 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,32 @@
+diff --git a/crates/core_arch/src/macros.rs b/crates/core_arch/src/macros.rs
+index f59e278b..f3d33636 100644
+--- 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]
+diff --git a/crates/core_arch/src/x86/mod.rs b/crates/core_arch/src/x86/mod.rs
+index 0404b194..d57d1fc8 100644
+--- 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]