Simd Models

.gitignore

@@ -52,3 +52,4 @@ package-lock.json
 # already existing elements were commented out
 
 #/target
+testable-simd-models/target

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # standard library we currently track.
 
 [toolchain]
-channel = "nightly-2024-11-03"
+channel = "nightly-2025-06-30"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

testable-simd-models/Cargo.toml

@@ -0,0 +1,16 @@
+[package]
+name = "testable-simd-models"
+version = "0.0.2"
+authors = ["Cryspen"]
+license = "Apache-2.0"
+homepage = "https://github.com/cryspen/verify-rust-std/testable-simd-models"
+edition = "2021"
+repository = "https://github.com/cryspen/verify-rust-std/testable-simd-models"
+readme = "README.md"
+
+[dependencies]
+rand = "0.9"
+pastey = "0.1.0"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn" }

testable-simd-models/README.md

@@ -0,0 +1,2 @@
+# testable-simd-models
+Rust models for the Core Library

testable-simd-models/src/abstractions/bit.rs

@@ -0,0 +1,204 @@
+//! # Bit Manipulation and Machine Integer Utilities
+//!
+//! This module provides utilities for working with individual bits and machine integer types.
+//! It defines a [`Bit`] enum to represent a single bit (`0` or `1`) along with convenient
+//! conversion implementations between `Bit`, [`bool`], and various primitive integer types.
+//!
+//! In addition, the module introduces the [`MachineInteger`] trait which abstracts over
+//! integer types, providing associated constants:
+//!
+//! - `BITS`: The size of the integer type in bits.
+//! - `SIGNED`: A flag indicating whether the type is signed.
+//!
+//! The [`Bit`] type includes methods for extracting the value of a specific bit from an integer.
+//! For example, [`Bit::of_int`] returns the bit at a given position for a provided integer,
+//! handling both positive and negative values (assuming a two's complement representation).
+//!
+//! # Examples
+//!
+//! ```rust
+//! use testable_simd_models::abstractions::bit::{Bit, MachineInteger};
+//!
+//! // Extract the 3rd bit (0-indexed) from an integer.
+//! let bit = Bit::of_int(42, 2);
+//! println!("The extracted bit is: {:?}", bit);
+//!
+//! // Convert Bit to a primitive integer type.
+//! let num: u8 = bit.into();
+//! println!("As an integer: {}", num);
+//! ```
+//!
+//! [`bool`]: https://doc.rust-lang.org/std/primitive.bool.html
+//! [`Bit::of_int`]: enum.Bit.html#method.of_int
+
+/// Represent a bit: `0` or `1`.
+#[derive(Copy, Clone, Eq, PartialEq, Debug)]
+pub enum Bit {
+    Zero,
+    One,
+}
+impl std::ops::BitAnd for Bit {
+    type Output = Self;
+    fn bitand(self, rhs: Self) -> Self {
+        match self {
+            Bit::Zero => Bit::Zero,
+            Bit::One => rhs,
+        }
+    }
+}
+
+impl std::ops::BitOr for Bit {
+    type Output = Self;
+    fn bitor(self, rhs: Self) -> Self {
+        match self {
+            Bit::Zero => rhs,
+            Bit::One => Bit::One,
+        }
+    }
+}
+
+impl std::ops::BitXor for Bit {
+    type Output = Self;
+    fn bitxor(self, rhs: Self) -> Self {
+        match (self, rhs) {
+            (Bit::Zero, Bit::Zero) => Bit::Zero,
+            (Bit::One, Bit::One) => Bit::Zero,
+            _ => Bit::One,
+        }
+    }
+}
+
+impl std::ops::Neg for Bit {
+    type Output = Self;
+    fn neg(self) -> Self {
+        match self {
+            Bit::One => Bit::Zero,
+            Bit::Zero => Bit::One,
+        }
+    }
+}
+macro_rules! generate_from_bit_impls {
+    ($($ty:ident),*) => {
+        $(impl From<Bit> for $ty {
+            fn from(bit: Bit) -> Self {
+                bool::from(bit) as $ty
+            }
+        })*
+    };
+}
+generate_from_bit_impls!(u8, u16, u32, u64, u128, i8, i16, i32, i64, i128);
+
+impl From<Bit> for bool {
+    fn from(bit: Bit) -> Self {
+        match bit {
+            Bit::Zero => false,
+            Bit::One => true,
+        }
+    }
+}
+
+impl From<bool> for Bit {
+    fn from(b: bool) -> Bit {
+        match b {
+            false => Bit::Zero,
+            true => Bit::One,
+        }
+    }
+}
+
+/// A trait for types that represent machine integers.
+pub trait MachineInteger {
+    /// The size of this integer type in bits.
+    fn bits() -> u32;
+
+    /// The signedness of this integer type.
+    const SIGNED: bool;
+    /// Element of the integer type with every bit as 0.
+    const ZEROS: Self;
+    /// Element of the integer type with every bit as 1.
+    const ONES: Self;
+    /// Minimum value of the integer type.
+    const MIN: Self;
+    /// Maximum value of the integer type.
+    const MAX: Self;
+
+    /// Implements functionality for `simd_add` in `crate::abstractions::simd`.
+    fn wrapping_add(self, rhs: Self) -> Self;
+    /// Implements functionality for `simd_sub` in `crate::abstractions::simd`.
+    fn wrapping_sub(self, rhs: Self) -> Self;
+    /// Implements functionality for `simd_mul` in `crate::abstractions::simd`.
+    fn overflowing_mul(self, rhs: Self) -> Self;
+    /// Implements functionality for `simd_saturating_add` in `crate::abstractions::simd`.
+    fn saturating_add(self, rhs: Self) -> Self;
+    /// Implements functionality for `simd_saturating_sub` in `crate::abstractions::simd`.
+    fn saturating_sub(self, rhs: Self) -> Self;
+    /// Implements functionality for `simd_abs_diff` in `crate::abstractions::simd`.
+    fn absolute_diff(self, rhs: Self) -> Self;
+    /// Implements functionality for `simd_abs` in `crate::abstractions::simd`.
+    fn absolute_val(self) -> Self;
+}
+
+macro_rules! generate_imachine_integer_impls {
+    ($($ty:ident),*) => {
+        $(
+	    impl MachineInteger for $ty {
+		const SIGNED: bool = true;
+		const ZEROS: $ty = 0;
+		const ONES: $ty = -1;
+		const MIN: $ty = $ty::MIN;
+		const MAX: $ty = $ty::MAX;
+		fn bits() -> u32 { $ty::BITS }
+		fn wrapping_add(self, rhs: Self) -> Self { self.wrapping_add(rhs) }
+		fn wrapping_sub(self, rhs: Self) -> Self { self.wrapping_sub(rhs) }
+		fn overflowing_mul(self, rhs: Self) -> Self { self.overflowing_mul(rhs).0 }
+		fn saturating_add(self, rhs: Self) -> Self { self.saturating_add(rhs)}
+		fn saturating_sub(self, rhs: Self) -> Self { self.saturating_sub(rhs) }
+		fn absolute_diff(self, rhs: Self) -> Self {if self > rhs {$ty::wrapping_sub(self, rhs)} else {$ty::wrapping_sub(rhs, self)}}
+		fn absolute_val(self) -> Self {if self == $ty::MIN {self} else {self.abs()}}
+            })*
+    };
+}
+
+macro_rules! generate_umachine_integer_impls {
+    ($($ty:ident),*) => {
+        $(
+	    impl MachineInteger for $ty {
+		const SIGNED: bool = false;
+		const ZEROS: $ty = 0;
+		const ONES: $ty = $ty::MAX;
+		const MIN: $ty = $ty::MIN;
+		const MAX: $ty = $ty::MAX;
+
+
+		fn bits() -> u32 { $ty::BITS }
+		fn wrapping_add(self, rhs: Self) -> Self { self.wrapping_add(rhs) }
+		fn wrapping_sub(self, rhs: Self) -> Self { self.wrapping_sub(rhs) }
+		fn overflowing_mul(self, rhs: Self) -> Self { self.overflowing_mul(rhs).0 }
+		fn saturating_add(self, rhs: Self) -> Self { self.saturating_add(rhs)}
+		fn saturating_sub(self, rhs: Self) -> Self { self.saturating_sub(rhs)}
+		fn absolute_diff(self, rhs: Self) -> Self {if self > rhs {self - rhs} else {rhs - self}}
+		fn absolute_val(self) -> Self {self}
+        })*
+    };
+}
+generate_imachine_integer_impls!(i8, i16, i32, i64, i128);
+generate_umachine_integer_impls!(u8, u16, u32, u64, u128);
+
+impl Bit {
+    fn of_raw_int(x: u128, nth: u32) -> Self {
+        if x / 2u128.pow(nth) % 2 == 1 {
+            Self::One
+        } else {
+            Self::Zero
+        }
+    }
+
+    pub fn of_int<T: Into<i128> + MachineInteger>(x: T, nth: u32) -> Bit {
+        let x: i128 = x.into();
+        if x >= 0 {
+            Self::of_raw_int(x as u128, nth)
+        } else {
+            Self::of_raw_int((2i128.pow(T::bits()) + x) as u128, nth)
+        }
+    }
+}

testable-simd-models/src/abstractions/bitvec.rs

@@ -0,0 +1,155 @@
+//! This module provides a specification-friendly bit vector type.
+use super::bit::{Bit, MachineInteger};
+use super::funarr::*;
+
+use std::fmt::Formatter;
+
+/// A fixed-size bit vector type.
+///
+/// `BitVec<N>` is a specification-friendly, fixed-length bit vector that internally
+/// stores an array of [`Bit`] values, where each `Bit` represents a single binary digit (0 or 1).
+///
+/// This type provides several utility methods for constructing and converting bit vectors:
+///
+/// The [`Debug`] implementation for `BitVec` pretty-prints the bits in groups of eight,
+/// making the bit pattern more human-readable. The type also implements indexing,
+/// allowing for easy access to individual bits.
+#[derive(Copy, Clone, Eq, PartialEq)]
+pub struct BitVec<const N: u64>(FunArray<N, Bit>);
+
+/// Pretty prints a bit slice by group of 8
+fn bit_slice_to_string(bits: &[Bit]) -> String {
+    bits.iter()
+        .map(|bit| match bit {
+            Bit::Zero => '0',
+            Bit::One => '1',
+        })
+        .collect::<Vec<_>>()
+        .chunks(8)
+        .map(|bits| bits.iter().collect::<String>())
+        .map(|s| format!("{s} "))
+        .collect::<String>()
+        .trim()
+        .into()
+}
+
+impl<const N: u64> core::fmt::Debug for BitVec<N> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), std::fmt::Error> {
+        write!(f, "{}", bit_slice_to_string(&self.0.as_vec()))
+    }
+}
+
+impl<const N: u64> core::ops::Index<u64> for BitVec<N> {
+    type Output = Bit;
+    fn index(&self, index: u64) -> &Self::Output {
+        self.0.get(index)
+    }
+}
+
+/// Convert a bit slice into an unsigned number.
+
+fn u128_int_from_bit_slice(bits: &[Bit]) -> u128 {
+    bits.iter()
+        .enumerate()
+        .map(|(i, bit)| u128::from(*bit) << i)
+        .sum::<u128>()
+}
+
+/// Convert a bit slice into a machine integer of type `T`.
+fn int_from_bit_slice<T: TryFrom<i128> + MachineInteger + Copy>(bits: &[Bit]) -> T {
+    debug_assert!(bits.len() <= T::bits() as usize);
+    let result = if T::SIGNED {
+        let is_negative = matches!(bits[T::bits() as usize - 1], Bit::One);
+        let s = u128_int_from_bit_slice(&bits[0..T::bits() as usize - 1]) as i128;
+        if is_negative {
+            s + (-2i128).pow(T::bits() - 1)
+        } else {
+            s
+        }
+    } else {
+        u128_int_from_bit_slice(bits) as i128
+    };
+    let Ok(n) = result.try_into() else {
+        // Conversion must succeed as `result` is guaranteed to be in range due to the bit-length check.
+        unreachable!()
+    };
+    n
+}
+impl<const N: u64> BitVec<N> {
+    /// Constructor for BitVec. `BitVec::<N>::from_fn` constructs a bitvector out of a function that takes usizes smaller than `N` and produces bits.
+    pub fn from_fn<F: Fn(u64) -> Bit>(f: F) -> Self {
+        Self(FunArray::from_fn(f))
+    }
+    /// Convert a slice of machine integers where only the `d` least significant bits are relevant.
+    pub fn from_slice<T: Into<i128> + MachineInteger + Copy>(x: &[T], d: u64) -> Self {
+        Self::from_fn(|i| Bit::of_int::<T>(x[(i / d) as usize], (i % d) as u32))
+    }
+
+    /// Construct a BitVec out of a machine integer.
+    pub fn from_int<T: Into<i128> + MachineInteger + Copy>(n: T) -> Self {
+        Self::from_slice::<T>(&[n], T::bits() as u64)
+    }
+
+    /// Convert a BitVec into a machine integer of type `T`.
+    pub fn to_int<T: TryFrom<i128> + MachineInteger + Copy>(self) -> T {
+        int_from_bit_slice(&self.0.as_vec())
+    }
+
+    /// Convert a BitVec into a vector of machine integers of type `T`.
+    pub fn to_vec<T: TryFrom<i128> + MachineInteger + Copy>(&self) -> Vec<T> {
+        self.0
+            .as_vec()
+            .chunks(T::bits() as usize)
+            .map(int_from_bit_slice)
+            .collect()
+    }
+
+    /// Generate a random BitVec.
+    pub fn rand() -> Self {
+        use rand::prelude::*;
+        let random_source: Vec<_> = {
+            let mut rng = rand::rng();
+            (0..N).map(|_| rng.random::<bool>()).collect()
+        };
+        Self::from_fn(|i| random_source[i as usize].into())
+    }
+}
+
+impl<const N: u64> BitVec<N> {
+    pub fn chunked_shift<const CHUNK: u64, const SHIFTS: u64>(
+        self,
+        shl: FunArray<SHIFTS, i128>,
+    ) -> BitVec<N> {
+        fn chunked_shift<const N: u64, const CHUNK: u64, const SHIFTS: u64>(
+            bitvec: BitVec<N>,
+            shl: FunArray<SHIFTS, i128>,
+        ) -> BitVec<N> {
+            BitVec::from_fn(|i| {
+                let nth_bit = i % CHUNK;
+                let nth_chunk = i / CHUNK;
+                let shift: i128 = if nth_chunk < SHIFTS {
+                    shl[nth_chunk]
+                } else {
+                    0
+                };
+                let local_index = (nth_bit as i128).wrapping_sub(shift);
+                if local_index < CHUNK as i128 && local_index >= 0 {
+                    let local_index = local_index as u64;
+                    bitvec[nth_chunk * CHUNK + local_index]
+                } else {
+                    Bit::Zero
+                }
+            })
+        }
+        chunked_shift::<N, CHUNK, SHIFTS>(self, shl)
+    }
+
+    /// Folds over the array, accumulating a result.
+    ///
+    /// # Arguments
+    /// * `init` - The initial value of the accumulator.
+    /// * `f` - A function combining the accumulator and each element.
+    pub fn fold<A>(&self, init: A, f: fn(A, Bit) -> A) -> A {
+        self.0.fold(init, f)
+    }
+}