Verify iter adapter unsafe methods + safe abstractions (challenge #16)

.github/workflows/verifast-iter-adapters.yml

@@ -0,0 +1,93 @@
+name: VeriFast iterator adapters
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/verifast-iter-adapters.yml'
+      - 'verifast-proofs/core/iter/adapters/**'
+      - 'verifast-proofs/setup-verifast-home'
+      - 'verifast-proofs/verifast'
+      - 'verifast-proofs/refinement-checker'
+      - 'library/core/src/iter/adapters/map_windows.rs'
+      - 'library/core/src/iter/adapters/step_by.rs'
+  push:
+    branches: [main, 16-iter-adapters]
+    paths:
+      - '.github/workflows/verifast-iter-adapters.yml'
+      - 'verifast-proofs/core/iter/adapters/**'
+      - 'verifast-proofs/setup-verifast-home'
+      - 'verifast-proofs/verifast'
+      - 'verifast-proofs/refinement-checker'
+      - 'library/core/src/iter/adapters/map_windows.rs'
+      - 'library/core/src/iter/adapters/step_by.rs'
+
+permissions:
+  contents: read
+
+concurrency:
+  group: verifast-iter-adapters-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  verify-iter-adapters:
+    name: Verify generic iterator adapter contracts
+    runs-on: ubuntu-24.04
+    timeout-minutes: 30
+    steps:
+      - name: Check out proof inputs
+        uses: actions/checkout@v4
+        with:
+          persist-credentials: false
+
+      - name: Check sources and contract selection
+        run: |
+          bash verifast-proofs/core/iter/adapters/verify.sh --static
+          python3 -I verifast-proofs/core/iter/adapters/test_sources.py
+
+      - name: Install frontend schema compiler
+        run: |
+          sudo --non-interactive apt-get update -qq
+          sudo --non-interactive apt-get install -y --no-install-recommends capnproto
+
+      - name: Restore compiled frontend
+        id: backend-cache
+        uses: actions/cache/restore@v4
+        with:
+          path: ~/.cache/verifast-iter-adapters
+          key: ${{ runner.os }}-verifast-iter-v1-${{ hashFiles('verifast-proofs/core/iter/adapters/backend/prepare.sh', 'verifast-proofs/core/iter/adapters/backend/*.patch') }}
+
+      - name: Verify contracts and source refinement
+        run: |
+          # A service cgroup limits the entire compiler/verifier process tree.
+          # --wait propagates failure, including timeout or memory exhaustion.
+          sudo --non-interactive systemd-run \
+            --unit="verifast-iter-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}" \
+            --service-type=exec --wait --pipe --collect \
+            --uid="$(id -u)" --gid="$(id -g)" \
+            --working-directory="$PWD" \
+            --setenv="PATH=$PATH" \
+            --setenv="CARGO_HOME=${CARGO_HOME:-$HOME/.cargo}" \
+            --setenv="RUSTUP_HOME=${RUSTUP_HOME:-$HOME/.rustup}" \
+            --property=MemoryMax=4G \
+            --property=MemorySwapMax=0 \
+            --property=TasksMax=256 \
+            --property=CPUQuota=200% \
+            --property=OOMPolicy=kill \
+            --property=KillMode=control-group \
+            --property=RuntimeMaxSec=1500 \
+            --property=TimeoutStopSec=15 \
+            /usr/bin/bash verifast-proofs/core/iter/adapters/verify.sh --remote
+
+      - name: Save compiled frontend
+        if: ${{ always() && !cancelled() && steps.backend-cache.outputs.cache-hit != 'true' }}
+        uses: actions/cache/save@v4
+        with:
+          path: ~/.cache/verifast-iter-adapters
+          key: ${{ steps.backend-cache.outputs.cache-primary-key }}

library/core/src/iter/adapters/array_chunks.rs

@@ -3,6 +3,8 @@ use crate::iter::adapters::SourceIter;
 use crate::iter::{
     ByRefSized, FusedIterator, InPlaceIterable, TrustedFused, TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{ControlFlow, NeverShortCircuit, Try};
 
@@ -230,6 +232,14 @@ where
         let inner_len = self.iter.size();
         let mut i = 0;
         // Use a while loop because (0..len).step_by(N) doesn't optimize well.
+        // Kani: the loop writes only `accum` and `i`, so `inner_len` keeps
+        // its entry value `self.iter.size()`; the invariant bounds `i`, which
+        // also guards the `inner_len - i` subtraction in the loop condition
+        // against underflow. The frame is stated explicitly because the
+        // `from_fn` closure borrows `self` mutably, and the inferred frame
+        // would otherwise havoc the whole adapter, `remainder` included.
+        #[safety::loop_invariant(i <= inner_len)]
+        #[cfg_attr(kani, kani::loop_modifies(&accum, &i))]
         while inner_len - i >= N {
             let chunk = crate::array::from_fn(|local| {
                 // SAFETY: The method consumes the iterator and the loop condition ensures that
@@ -274,3 +284,68 @@ unsafe impl<I: InPlaceIterable + Iterator, const N: usize> InPlaceIterable for A
         }
     };
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // `next_back_remainder` pulls the final `len % N` elements off the back via
+    // `rev().take(rem).next_chunk()`, then reverses them in place, relying on
+    // `unwrap_err_unchecked` (sound because `rem < N`).
+    macro_rules! check_next_back_remainder {
+        ($harness:ident, $elem_ty:ty, $n:expr, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it: ArrayChunks<_, N> = ArrayChunks::new(any_slice(&array).iter());
+                it.next_back_remainder();
+                let _ = &it.remainder;
+            }
+        };
+    }
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_unit, (), 2, 8);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_u8, u8, 2, 8);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_char, char, 3, 9);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_tup, (char, u8), 2, 8);
+
+    // `fold` on a `TrustedRandomAccessNoCoerce` source builds each chunk with
+    // `array::from_fn` calling `__iterator_get_unchecked(i + local)` under an
+    // `inner_len - i >= N` guard; this proves those indexes stay in bounds.
+    // The chunking loop carries a Kani loop invariant, so no unwind bound is
+    // necessary and `MAX_LEN` mirrors the accessor harness menu: `u32::MAX`
+    // for `u8`, `isize::MAX` for the ZST, moderate bounds for the wider
+    // element types.
+    macro_rules! check_fold {
+        ($harness:ident, $elem_ty:ty, $n:expr, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let it: ArrayChunks<_, N> = ArrayChunks::new(any_slice(&array).iter());
+                // Disambiguate from the in-scope internal `SpecFold::fold`.
+                let _ = crate::iter::Iterator::fold(it, 0usize, |acc, _chunk| acc.wrapping_add(1));
+            }
+        };
+    }
+    check_fold!(check_array_chunks_fold_unit, (), 2, isize::MAX as usize);
+    check_fold!(check_array_chunks_fold_u8, u8, 2, u32::MAX as usize);
+    check_fold!(check_array_chunks_fold_char, char, 3, 10);
+    check_fold!(check_array_chunks_fold_tup, (char, u8), 2, 10);
+}

library/core/src/iter/adapters/cloned.rs

@@ -152,6 +152,7 @@ where
     I: UncheckedIterator<Item = &'a T>,
     T: Clone,
 {
+    #[requires(self.it.size_hint().0 > 0)]
     unsafe fn next_unchecked(&mut self) -> T {
         // SAFETY: `Cloned` is 1:1 with the inner iterator, so if the caller promised
         // that there's an element left, the inner iterator has one too.
@@ -193,3 +194,62 @@ unsafe impl<I: InPlaceIterable> InPlaceIterable for Cloned<I> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_cloned_iter<'a, T: Clone>(orig_slice: &'a [T]) -> Cloned<crate::slice::Iter<'a, T>> {
+        Cloned::new(any_slice(orig_slice).iter())
+    }
+
+    macro_rules! check_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_cloned_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.it.size_hint().0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+    check_get_unchecked!(check_cloned_get_unchecked_unit, (), isize::MAX as usize);
+    check_get_unchecked!(check_cloned_get_unchecked_u8, u8, u32::MAX as usize);
+    check_get_unchecked!(check_cloned_get_unchecked_char, char, 50);
+    check_get_unchecked!(check_cloned_get_unchecked_tup, (char, u8), 50);
+
+    // `next_unchecked` (UncheckedIterator): the precondition is that the iterator
+    // is non-empty; establish it by construction.
+    macro_rules! check_cloned_next_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_cloned_iter::<$elem_ty>(&array);
+                kani::assume(it.it.size_hint().0 > 0);
+                let _ = unsafe { it.next_unchecked() };
+            }
+        };
+    }
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_unit, (), isize::MAX as usize);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_u8, u8, u32::MAX as usize);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_char, char, 50);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_tup, (char, u8), 50);
+}

library/core/src/iter/adapters/copied.rs

@@ -284,3 +284,69 @@ unsafe impl<I: InPlaceIterable> InPlaceIterable for Copied<I> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_adapter_iter<'a, T>(orig_slice: &'a [T]) -> Copied<crate::slice::Iter<'a, T>> {
+        Copied::new(any_slice(orig_slice).iter())
+    }
+
+    macro_rules! check_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_adapter_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.it.size_hint().0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+    check_get_unchecked!(check_copied_get_unchecked_unit, (), isize::MAX as usize);
+    check_get_unchecked!(check_copied_get_unchecked_u8, u8, u32::MAX as usize);
+    check_get_unchecked!(check_copied_get_unchecked_char, char, 50);
+    check_get_unchecked!(check_copied_get_unchecked_tup, (char, u8), 50);
+
+    // `spec_next_chunk` on the `slice::Iter` specialization bulk-copies `N` (or
+    // `len`) elements into a `MaybeUninit<[T; N]>` and then either
+    // `array_assume_init`s the full array or returns a `0..len` `IntoIter`; this
+    // proves the `copy_nonoverlapping` lengths and the init range stay in bounds.
+    // `N` is a trait generic, so it is pinned via the result type annotation.
+    // The `MAX_LEN` menu mirrors `check_get_unchecked` above: the `u8`/ZST
+    // harnesses raise the bound very high (there is no per-iteration loop, only
+    // a bulk copy, so the cost stays flat), the wider types use a moderate one.
+    macro_rules! check_spec_next_chunk {
+        ($harness:ident, $elem_ty:ty, $n:expr, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_slice(&array).iter();
+                let _result: Result<[$elem_ty; N], crate::array::IntoIter<$elem_ty, N>> =
+                    it.spec_next_chunk();
+            }
+        };
+    }
+    check_spec_next_chunk!(check_copied_spec_next_chunk_unit, (), 2, isize::MAX as usize);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_u8, u8, 3, u32::MAX as usize);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_char, char, 2, 50);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_tup, (char, u8), 2, 50);
+}

library/core/src/iter/adapters/enumerate.rs

@@ -321,3 +321,70 @@ impl<I: Default> Default for Enumerate<I> {
         Enumerate::new(Default::default())
     }
 }
+
+/// Verification harnesses for `Enumerate`'s `unsafe`/contract-bearing methods
+/// (verify-rust-std challenge #16).
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    /// An arbitrary-length sub-slice of `orig_slice` (mirrors
+    /// `slice::iter::verify::any_slice`).  The slice handed to the iterator
+    /// has a symbolic length in `0..=MAX_LEN`, so one proof covers every
+    /// length up to the backing array's size at once.  The proof is still
+    /// bounded by `MAX_LEN`: the `u8`/ZST harnesses raise `MAX_LEN` to
+    /// `u32::MAX`/`isize::MAX`, far beyond practical slice lengths, while the
+    /// wider element types use smaller bounds.
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            // SAFETY: `ptr` is non-null and aligned; length 0 makes the slice trivially valid.
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    /// Wrap an arbitrary sub-slice in `Enumerate<slice::Iter<'_, T>>`.  We build
+    /// the inner `slice::Iter` via `(&[T]).iter()` because `slice::Iter::new` is
+    /// `pub(super)` to the `slice` module and unreachable from here.
+    fn any_enumerate_iter<'a, T>(orig_slice: &'a [T]) -> Enumerate<crate::slice::Iter<'a, T>> {
+        Enumerate::new(any_slice(orig_slice).iter())
+    }
+
+    /// One plain `#[kani::proof]` harness per concrete element type (the NOTE
+    /// below explains why this is not `proof_for_contract`).  `slice::Iter<T>`
+    /// is `TrustedRandomAccessNoCoerce` for every `T`, satisfying the method's
+    /// `Self: TrustedRandomAccessNoCoerce` bound.
+    // NOTE: `__iterator_get_unchecked` is a trait method on the *generic* impl
+    // `impl<I> Iterator for Enumerate<I>`, and Kani cannot attach a
+    // `proof_for_contract` to a generic trait method (kani#1997).  So instead of
+    // the contract machinery we use a plain `#[kani::proof]` that establishes the
+    // method's precondition by construction (`idx < self.iter.size_hint().0`) and
+    // lets Kani prove the body introduces no UB -- the same safety property the
+    // contract expresses.
+    macro_rules! check_enumerate_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut enumerate = any_enumerate_iter::<$elem_ty>(&array);
+                // The method's precondition: `idx < self.iter.size_hint().0`.
+                let idx = kani::any_where(|i: &usize| *i < enumerate.iter.size_hint().0);
+                let _ = unsafe { enumerate.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+
+    // Representative element types: ZST, byte, 4-byte-align niche type, composite.
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_unit, (), isize::MAX as usize);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_u8, u8, u32::MAX as usize);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_char, char, 50);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_tup, (char, u8), 50);
+}