Add RAPx tool description and CI workflow

.github/workflows/rapx.yml

@@ -0,0 +1,47 @@
+name: RAPx
+
+on:
+  workflow_dispatch:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+env:
+  RAPX_VERSION: "8864b6113c950365a74a3fa35bbfc32ad0660af5"
+  TOOLCHAIN: "nightly-2025-11-25"
+
+jobs:
+  verify-slice:
+    name: Verify core::slice with RAPx
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      - name: Set up Rust toolchain
+        run: |
+          rustup toolchain install $TOOLCHAIN
+          rustup component add rust-src --toolchain $TOOLCHAIN
+
+      - name: Clone and install RAPx
+        run: |
+          rm -rf RAPx
+          git clone --branch verify-std https://github.com/safer-rust/RAPx.git
+          cd RAPx
+          git fetch origin $RAPX_VERSION
+          git checkout $RAPX_VERSION
+          ./install.sh
+
+      - name: Run RAPx verification
+        run: |
+          export RUSTUP_TOOLCHAIN=$(rustup show active-toolchain | cut -d ' ' -f 1)
+          export RAPX_SYSROOT=$(rustc --print sysroot)
+          export LD_LIBRARY_PATH="$RAPX_SYSROOT/lib"
+          export RUSTFLAGS="--cfg=rapx -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)"
+          export __CARGO_TESTS_ONLY_SRC_ROOT="$(pwd)/library"
+          # `core` is a dependency (not a workspace member) of `library`, so RAPx
+          # only analyzes it as a primary package when invoked from library/core.
+          cd library/core
+          cargo +$RUSTUP_TOOLCHAIN rapx verify --module slice --mode targeted

library/core/Cargo.toml

@@ -44,7 +44,8 @@ check-cfg = [
     'cfg(target_has_reliable_f128_math)',
     'cfg(llvm_enzyme)',
     'cfg(kani)',
-    'cfg(flux)'
+    'cfg(flux)',
+    'cfg(rapx)',
 ]
 
 [package.metadata.flux]

library/core/src/lib.rs

@@ -412,3 +412,6 @@ include!("primitive_docs.rs");
 
 #[cfg(flux)]
 mod flux_info;
+
+#[cfg(rapx)]
+mod rapx_macro {}

library/core/src/ptr/mod.rs

@@ -525,6 +525,12 @@ mod mut_ptr;
 #[inline(always)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_diagnostic_item = "ptr_copy_nonoverlapping"]
+#[cfg_attr(rapx, rapx::requires(Align(src, T)))]
+#[cfg_attr(rapx, rapx::requires(Align(dst, T)))]
+#[cfg_attr(rapx, rapx::requires(ValidPtr(src, T, count)))]
+#[cfg_attr(rapx, rapx::requires(ValidPtr(dst, T, count)))]
+#[cfg_attr(rapx, rapx::requires(NonOverlap(dst, src, T, count)))]
+#[cfg_attr(rapx, rapx::requires(ValidNum(size_of(T) * count <= isize::MAX)))]
 pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: usize) {
     ub_checks::assert_unsafe_precondition!(
         check_language_ub,
@@ -622,6 +628,10 @@ pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: us
 #[inline(always)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_diagnostic_item = "ptr_copy"]
+#[cfg_attr(rapx, rapx::requires(ValidPtr(src, T, count)))]
+#[cfg_attr(rapx, rapx::requires(Align(src, T)))]
+#[cfg_attr(rapx, rapx::requires(ValidPtr(dst, T, count)))]
+#[cfg_attr(rapx, rapx::requires(Align(dst, T)))]
 pub const unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize) {
     // SAFETY: the safety contract for `copy` must be upheld by the caller.
     unsafe {
@@ -1360,6 +1370,9 @@ pub const unsafe fn swap<T>(x: *mut T, y: *mut T) {
 #[rustc_diagnostic_item = "ptr_swap_nonoverlapping"]
 #[rustc_allow_const_fn_unstable(const_eval_select)] // both implementations behave the same
 #[track_caller]
+#[cfg_attr(rapx, rapx::requires(ValidPtr(x, T, count)))]
+#[cfg_attr(rapx, rapx::requires(Align(x, T)))]
+#[cfg_attr(rapx, rapx::requires(NonOverlap(x, y, T, count)))]
 pub const unsafe fn swap_nonoverlapping<T>(x: *mut T, y: *mut T, count: usize) {
     ub_checks::assert_unsafe_precondition!(
         check_library_ub,
@@ -2224,6 +2237,9 @@ pub unsafe fn write_volatile<T>(dst: *mut T, src: T) {
     let new_addr = usize::wrapping_add(product, p.addr());
     *result != usize::MAX && new_addr % a == 0
 })]
+/// # Safety
+/// The alignment `a` must be a non-zero power of two.
+#[cfg_attr(rapx, rapx::requires(ValidNum(a != 0)))]
 pub(crate) unsafe fn align_offset<T: Sized>(p: *const T, a: usize) -> usize {
     // FIXME(#75598): Direct use of these intrinsics improves codegen significantly at opt-level <=
     // 1, where the method versions of these operations are not inlined.