diff --git a/.github/workflows/verifast-iter-adapters.yml b/.github/workflows/verifast-iter-adapters.yml new file mode 100644 index 0000000000000..a723985302579 --- /dev/null +++ b/.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 }} diff --git a/library/core/src/iter/adapters/array_chunks.rs b/library/core/src/iter/adapters/array_chunks.rs index 7c003cff10c7b..dc0a1069d20b8 100644 --- a/library/core/src/iter/adapters/array_chunks.rs +++ b/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 InPlaceIterable for A } }; } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|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); +} diff --git a/library/core/src/iter/adapters/cloned.rs b/library/core/src/iter/adapters/cloned.rs index 0f05260059880..096f7de14278c 100644 --- a/library/core/src/iter/adapters/cloned.rs +++ b/library/core/src/iter/adapters/cloned.rs @@ -152,6 +152,7 @@ where I: UncheckedIterator, 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 InPlaceIterable for Cloned { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = I::MERGE_BY; } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|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> { + 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); +} diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs index 3db6c5dafd400..4e41cf8ba2915 100644 --- a/library/core/src/iter/adapters/copied.rs +++ b/library/core/src/iter/adapters/copied.rs @@ -284,3 +284,69 @@ unsafe impl InPlaceIterable for Copied { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = I::MERGE_BY; } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|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> { + 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); +} diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs index e7e18d178031f..65e82bafef523 100644 --- a/library/core/src/iter/adapters/enumerate.rs +++ b/library/core/src/iter/adapters/enumerate.rs @@ -321,3 +321,70 @@ impl Default for Enumerate { 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(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::(|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>`. 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> { + 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` + /// 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 Iterator for Enumerate`, 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); +} diff --git a/library/core/src/iter/adapters/filter.rs b/library/core/src/iter/adapters/filter.rs index b22419ccf080a..661da9d2cee26 100644 --- a/library/core/src/iter/adapters/filter.rs +++ b/library/core/src/iter/adapters/filter.rs @@ -221,6 +221,89 @@ unsafe impl InPlaceIterable for Filter { const MERGE_BY: Option> = I::MERGE_BY; } +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|v| *v != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + // `Filter`'s predicate is `FnMut(&Self::Item)`; for `slice::Iter` that is + // `FnMut(&&T)`. A nondeterministic predicate exercises both the kept and the + // filtered branch. A named fn pointer keeps the helper return type nameable. + fn maybe_keep(_: &&T) -> bool { + kani::any() + } + + // `next_chunk_dropless` writes every element (branchlessly) into a + // `MaybeUninit<[_; N]>` and bumps `initialized` only for kept elements, + // breaking once `initialized == N`; this proves the `get_unchecked_mut(idx)` + // writes and the final `array_assume_init` / `IntoIter` range stay in bounds. + // + // Boundedness: the chunk fill iterates through the generic default + // `Iterator::try_fold` (a while-let loop that calls a generic closure in + // iterator.rs), so this adapter cannot attach a loop contract to it. A + // fixed `MAX_LEN` only proves safety for sources up to that length. A + // predicate can reject arbitrarily many elements before accepting one; + // covering every value of `initialized` does not prove preservation of + // the buffer and iterator invariants across those extra iterations. + // These harnesses do not meet the challenge's unbounded requirement. + // + // N = 0 with a nonempty source remains an upstream defect in this snapshot: + // the closure writes through + // `array.get_unchecked_mut(idx)` before it compares `initialized < N`, so + // `next_chunk::<0>()` on a source that yields at least one element writes + // out of bounds into the zero-length array. Repo rules + // (doc/src/general-rules.md) do not permit a local change to the runtime + // logic unless it has been incorporated upstream. The defect is tracked + // at https://github.com/rust-lang/rust/issues/153803, with a proposed fix + // at https://github.com/rust-lang/rust/pull/153813. + // The separate empty-source N = 0 harness below does not cover this defect. + macro_rules! check_next_chunk_dropless { + ($harness:ident, $elem_ty:ty, $n:expr) => { + #[kani::proof] + #[kani::unwind(7)] + fn $harness() { + const MAX_LEN: usize = 6; + const N: usize = $n; + let array: [$elem_ty; MAX_LEN] = kani::any(); + let mut it = Filter::new( + any_slice(&array).iter(), + maybe_keep::<$elem_ty> as fn(&&$elem_ty) -> bool, + ); + let _ = it.next_chunk_dropless::(); + } + }; + } + check_next_chunk_dropless!(check_filter_next_chunk_dropless_unit, (), 4); + check_next_chunk_dropless!(check_filter_next_chunk_dropless_u8, u8, 4); + check_next_chunk_dropless!(check_filter_next_chunk_dropless_char, char, 4); + check_next_chunk_dropless!(check_filter_next_chunk_dropless_tup, (char, u8), 4); + check_next_chunk_dropless!(check_filter_next_chunk_dropless_unit_n1, (), 1); + check_next_chunk_dropless!(check_filter_next_chunk_dropless_u8_n1, u8, 1); + check_next_chunk_dropless!(check_filter_next_chunk_dropless_char_n1, char, 1); + check_next_chunk_dropless!(check_filter_next_chunk_dropless_tup_n1, (char, u8), 1); + + // With no source elements, the faulty write is unreachable. Exercise the + // zero-capacity result and its drop without claiming nonempty-source safety. + #[kani::proof] + fn check_filter_next_chunk_dropless_empty_n0() { + let mut it = Filter::new(crate::iter::empty::(), |_: &u8| kani::any::()); + let _ = it.next_chunk_dropless::<0>(); + } +} + trait SpecAssumeCount { /// # Safety /// diff --git a/library/core/src/iter/adapters/filter_map.rs b/library/core/src/iter/adapters/filter_map.rs index 24ec6b1741ce1..d8cca33eaafe1 100644 --- a/library/core/src/iter/adapters/filter_map.rs +++ b/library/core/src/iter/adapters/filter_map.rs @@ -211,3 +211,121 @@ unsafe impl InPlaceIterable for FilterMap { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = I::MERGE_BY; } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|v| *v != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + // Maps `&T -> Option` nondeterministically to exercise both the + // "element kept" and "element filtered" paths of the chunk-fill loop, with + // a nondeterministic payload of the parameterized output type `B`. + fn maybe_map_to(_: &T) -> Option { + kani::any::().then(|| kani::any()) + } + + // A drop-requiring output type: `needs_drop::()` is true, so + // the chunk loop's `Guard` compiles real drop glue instead of a no-op and + // the payload byte-copy plus `mem::forget` handling must keep every + // initialized slot live and in bounds. Kani models a panic as a + // verification failure and has no unwinding, so the panic-during-drop + // path itself is not expressible in a passing harness; the coverage this + // type adds is the non-trivial drop-glue code path. + struct DropToken(u8); + + impl Drop for DropToken { + fn drop(&mut self) { + let _ = crate::hint::black_box(self.0); + } + } + + impl kani::Arbitrary for DropToken { + fn any() -> Self { + DropToken(kani::any()) + } + } + + // `next_chunk` fills a `MaybeUninit<[B; N]>` via a `Guard`-protected loop + // that byte-copies each mapped value's payload and bumps `initialized` only + // when the map yields `Some`; this proves the copies, the `array_assume_init`, + // and the partial-fill `IntoIter` range all stay in bounds. The output menu + // covers `usize`, a validity niche (`char`), a ZST (`()`), a padded pair + // (`(char, u8)`), and a drop-requiring type (`DropToken`). + // + // Boundedness: the chunk fill iterates through the generic default + // `Iterator::try_fold` (a while-let loop that calls a generic closure in + // iterator.rs), so this adapter cannot attach a loop contract to it. A + // fixed `MAX_LEN` only proves safety for sources up to that length. A + // mapping can return `None` arbitrarily many times before yielding `Some`; + // covering every value of `initialized` does not prove preservation of + // the buffer and iterator invariants across those extra iterations. + // These harnesses do not meet the challenge's unbounded requirement. + // + // N = 0 with a nonempty source remains an upstream defect in this snapshot: + // the closure does a one-element + // `copy_nonoverlapping` of the mapped payload into `guard.array` at + // `idx` before it compares `guard.initialized < N`, so `next_chunk::<0>()` + // on a source that yields at least one element writes out of bounds into + // the zero-capacity array. Repo rules (doc/src/general-rules.md) do not + // permit a local change to the runtime logic unless it has been + // incorporated upstream. The defect is tracked at + // https://github.com/rust-lang/rust/issues/153803, with a proposed fix at + // https://github.com/rust-lang/rust/pull/153813. + // The separate empty-source N = 0 harnesses below do not cover this defect. + macro_rules! check_next_chunk { + ($harness:ident, $elem_ty:ty, $out_ty:ty, $n:expr) => { + #[kani::proof] + #[kani::unwind(6)] + fn $harness() { + const MAX_LEN: usize = 5; + const N: usize = $n; + let array: [$elem_ty; MAX_LEN] = kani::any(); + let mut it = FilterMap::new( + any_slice(&array).iter(), + maybe_map_to::<$elem_ty, $out_ty> as fn(&$elem_ty) -> Option<$out_ty>, + ); + let _ = it.next_chunk::(); + } + }; + } + check_next_chunk!(check_filter_map_next_chunk_unit, (), usize, 3); + check_next_chunk!(check_filter_map_next_chunk_u8, u8, usize, 3); + check_next_chunk!(check_filter_map_next_chunk_char, char, usize, 3); + check_next_chunk!(check_filter_map_next_chunk_tup, (char, u8), usize, 3); + check_next_chunk!(check_filter_map_next_chunk_unit_n1, (), usize, 1); + check_next_chunk!(check_filter_map_next_chunk_u8_n1, u8, usize, 1); + check_next_chunk!(check_filter_map_next_chunk_char_n1, char, usize, 1); + check_next_chunk!(check_filter_map_next_chunk_tup_n1, (char, u8), usize, 1); + check_next_chunk!(check_filter_map_next_chunk_out_char, u8, char, 3); + check_next_chunk!(check_filter_map_next_chunk_out_unit, u8, (), 3); + check_next_chunk!(check_filter_map_next_chunk_out_tup, u8, (char, u8), 3); + check_next_chunk!(check_filter_map_next_chunk_out_drop, u8, DropToken, 3); + + // Empty sources avoid the faulty payload copy. Check both dropless and + // drop-requiring outputs at zero capacity, including dropping the result. + #[kani::proof] + fn check_filter_map_next_chunk_empty_n0() { + let mut it = FilterMap::new(crate::iter::empty::(), |_| kani::any::>()); + let _ = it.next_chunk::<0>(); + } + + #[kani::proof] + fn check_filter_map_next_chunk_empty_drop_n0() { + let mut it = + FilterMap::new(crate::iter::empty::(), |_| kani::any::>()); + let _ = it.next_chunk::<0>(); + } +} diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs index fcad6168d85cd..11d607ba466fb 100644 --- a/library/core/src/iter/adapters/fuse.rs +++ b/library/core/src/iter/adapters/fuse.rs @@ -478,3 +478,43 @@ fn and_then_or_clear(opt: &mut Option, f: impl FnOnce(&mut T) -> Option } x } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|val| *val != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + fn any_fuse_iter<'a, T>(orig_slice: &'a [T]) -> Fuse> { + Fuse::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_fuse_iter::<$elem_ty>(&array); + let idx = kani::any_where(|i: &usize| *i < it.iter.as_ref().unwrap().size_hint().0); + let _ = unsafe { it.__iterator_get_unchecked(idx) }; + } + }; + } + check_get_unchecked!(check_fuse_get_unchecked_unit, (), isize::MAX as usize); + check_get_unchecked!(check_fuse_get_unchecked_u8, u8, u32::MAX as usize); + check_get_unchecked!(check_fuse_get_unchecked_char, char, 50); + check_get_unchecked!(check_fuse_get_unchecked_tup, (char, u8), 50); +} diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs index bf9f0c48fec3b..eb77668fd620b 100644 --- a/library/core/src/iter/adapters/map.rs +++ b/library/core/src/iter/adapters/map.rs @@ -245,3 +245,69 @@ unsafe impl InPlaceIterable for Map { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = I::MERGE_BY; } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|val| *val != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + // The mapping closure is irrelevant to buffer/UB safety; a simple + // `&T -> usize` fn pointer (nameable, unlike a closure) keeps the harness + // type concrete. `slice::Iter` yields `&T`, so `F: FnMut(&T) -> usize`. + fn map_fn(_: &T) -> usize { + 0 + } + + fn any_map_iter<'a, T>(orig_slice: &'a [T]) -> Map, fn(&T) -> usize> { + Map::new(any_slice(orig_slice).iter(), map_fn:: as fn(&T) -> usize) + } + + macro_rules! check_map_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_map_iter::<$elem_ty>(&array); + let idx = kani::any_where(|i: &usize| *i < it.iter.size_hint().0); + let _ = unsafe { it.__iterator_get_unchecked(idx) }; + } + }; + } + + macro_rules! check_map_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_map_iter::<$elem_ty>(&array); + kani::assume(it.iter.size_hint().0 > 0); + let _ = unsafe { it.next_unchecked() }; + } + }; + } + + check_map_get_unchecked!(check_map_get_unchecked_unit, (), isize::MAX as usize); + check_map_get_unchecked!(check_map_get_unchecked_u8, u8, u32::MAX as usize); + check_map_get_unchecked!(check_map_get_unchecked_char, char, 50); + check_map_get_unchecked!(check_map_get_unchecked_tup, (char, u8), 50); + + check_map_next_unchecked!(check_map_next_unchecked_unit, (), isize::MAX as usize); + check_map_next_unchecked!(check_map_next_unchecked_u8, u8, u32::MAX as usize); + check_map_next_unchecked!(check_map_next_unchecked_char, char, 50); + check_map_next_unchecked!(check_map_next_unchecked_tup, (char, u8), 50); +} diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs index 3d5918a552c61..8451a02ea9da0 100644 --- a/library/core/src/iter/adapters/map_windows.rs +++ b/library/core/src/iter/adapters/map_windows.rs @@ -297,3 +297,96 @@ impl Invariant for Buffer { self.start + N <= 2 * N } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + // Build a `Buffer` in a valid state: `start` in `[0, N]` (the type + // invariant) and the live window `[start, start + N)` fully initialized with + // arbitrary values; the remaining `N` slots stay uninitialized, exactly as + // the real buffer maintains them. + fn any_buffer() -> Buffer { + let start = kani::any_where(|s: &usize| *s <= N); + let mut buffer = Buffer { + buffer: [[const { MaybeUninit::uninit() }; N], [const { MaybeUninit::uninit() }; N]], + start, + }; + let items: [T; N] = kani::any(); + let base = buffer.buffer_mut_ptr(); + items.into_iter().enumerate().for_each(|(i, item)| { + // SAFETY: `start + i < start + N <= 2 * N`, in bounds of the `2 * N` buffer. + unsafe { (*base.add(start + i)).write(item) }; + }); + buffer + } + + // `as_array_ref` / `as_uninit_array_mut` reinterpret the live window as an + // array reference; `push` rotates the window (and wraps + compacts when + // `start == N`); `drop` drops the live window. Each must respect the + // initialized-window invariant and stay in bounds of the `2 * N` storage. + macro_rules! check_buffer { + ($module:ident, $elem_ty:ty, $n:expr) => { + mod $module { + use super::*; + const N: usize = $n; + + #[kani::proof] + fn check_as_array_ref() { + let buf = any_buffer::<$elem_ty, N>(); + let _ = buf.as_array_ref(); + kani::assert(buf.is_safe(), "buffer invariant holds"); + } + + #[kani::proof] + fn check_as_uninit_array_mut() { + let mut buf = any_buffer::<$elem_ty, N>(); + let _ = buf.as_uninit_array_mut(); + kani::assert(buf.is_safe(), "buffer invariant holds"); + } + + #[kani::proof] + fn check_push() { + let mut buf = any_buffer::<$elem_ty, N>(); + buf.push(kani::any()); + kani::assert(buf.is_safe(), "buffer invariant holds after push"); + } + + #[kani::proof] + fn check_drop() { + let buf = any_buffer::<$elem_ty, N>(); + drop(buf); + } + } + }; + } + check_buffer!(verify_map_windows_unit, (), 3); + check_buffer!(verify_map_windows_u8, u8, 3); + check_buffer!(verify_map_windows_char, char, 2); + check_buffer!(verify_map_windows_tup, (char, u8), 2); + + // A drop-requiring element type: `needs_drop::()` is true, so + // `push`'s `drop_in_place` and the `Buffer` `Drop` impl execute real drop + // glue instead of compiling to no-ops, and the destructor reads the + // payload, so the dropped element must be an in-bounds, live slot. Kani + // models a panic as a verification failure and has no unwinding, so the + // panic-during-drop path itself is not expressible in a passing harness; + // the coverage this type adds is the non-trivial drop-glue code path. + struct DropToken(u8); + + impl Drop for DropToken { + fn drop(&mut self) { + let _ = crate::hint::black_box(self.0); + } + } + + impl kani::Arbitrary for DropToken { + fn any() -> Self { + DropToken(kani::any()) + } + } + + check_buffer!(verify_map_windows_drop, DropToken, 2); +} diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs index ac3cc4c4f1152..f9c8c97d5f8ec 100644 --- a/library/core/src/iter/adapters/skip.rs +++ b/library/core/src/iter/adapters/skip.rs @@ -293,3 +293,68 @@ where // I: TrustedLen would not. #[unstable(feature = "trusted_len", issue = "37572")] unsafe impl TrustedLen for Skip where I: Iterator + TrustedRandomAccess {} + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|val| *val != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + fn any_skip_iter<'a, T>(orig_slice: &'a [T]) -> Skip> { + let slice = any_slice(orig_slice); + let n = kani::any_where(|offset: &usize| *offset <= slice.len()); + Skip::new(slice.iter(), n) + } + + 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_skip_iter::<$elem_ty>(&array); + let idx = kani::any_where(|i: &usize| *i < it.iter.size_hint().0 - it.n); + let _ = unsafe { it.__iterator_get_unchecked(idx) }; + } + }; + } + check_get_unchecked!(check_skip_get_unchecked_unit, (), isize::MAX as usize); + check_get_unchecked!(check_skip_get_unchecked_u8, u8, u32::MAX as usize); + check_get_unchecked!(check_skip_get_unchecked_char, char, 50); + check_get_unchecked!(check_skip_get_unchecked_tup, (char, u8), 50); + + fn bump(x: &u8) -> u8 { + x.wrapping_add(1) + } + + // `Map` has `MAY_HAVE_SIDE_EFFECT = true` (map.rs pins + // the constant to `true` for every `Map`), so `__iterator_get_unchecked` + // compiles in the `idx == 0` prefix-dropping branch that the plain + // `slice::Iter` harnesses compile out. `idx` stays symbolic, so the + // proof covers the branch both taken (`idx == 0`, dropping the `self.n` + // skipped items) and not taken. The prefix loop runs `self.n` times, so + // this harness is bounded by `MAX_LEN`. + #[kani::proof] + #[kani::unwind(7)] + fn check_skip_get_unchecked_side_effect() { + const MAX_LEN: usize = 5; + let array: [u8; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let n = kani::any_where(|offset: &usize| *offset <= slice.len()); + let mut it = Skip::new(slice.iter().map(bump as fn(&u8) -> u8), n); + let idx = kani::any_where(|i: &usize| *i < it.iter.size_hint().0 - it.n); + let _ = unsafe { it.__iterator_get_unchecked(idx) }; + } +} diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index 32604a07ca40c..1ac22d698a43e 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -589,3 +589,46 @@ spec_int_ranges_r!(u8 u16 u32 usize); spec_int_ranges!(u8 u16 usize); #[cfg(target_pointer_width = "16")] spec_int_ranges_r!(u8 u16 usize); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|v| *v != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + // `original_step` reconstructs the configured step as `step_minus_one + 1` + // via `unchecked_add` and `NonZero::new_unchecked`. The type invariant + // (`step_minus_one < usize::MAX`) makes both operations sound; a valid + // `StepBy` is established by construction (`StepBy::new` requires `step != 0`). + macro_rules! check_original_step { + ($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 step = kani::any_where(|s: &usize| *s != 0); + let it = StepBy::new(any_slice(&array).iter(), step); + let result = it.original_step(); + kani::assert(result.get() == step, "original_step round-trips the configured step"); + } + }; + } + // `original_step` ignores the wrapped iterator, so a small backing array + // suffices; the proof is over the symbolic `step`, not the slice length. + check_original_step!(check_step_by_original_step_unit, (), 16); + check_original_step!(check_step_by_original_step_u8, u8, 16); + check_original_step!(check_step_by_original_step_char, char, 16); + check_original_step!(check_step_by_original_step_tup, (char, u8), 16); +} diff --git a/library/core/src/iter/adapters/take.rs b/library/core/src/iter/adapters/take.rs index b96335f415257..ac0f231d6dca1 100644 --- a/library/core/src/iter/adapters/take.rs +++ b/library/core/src/iter/adapters/take.rs @@ -1,6 +1,8 @@ use crate::cmp; use crate::iter::adapters::SourceIter; use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen, TrustedRandomAccess}; +#[cfg(kani)] +use crate::kani; use crate::num::NonZero; use crate::ops::{ControlFlow, Try}; @@ -299,6 +301,11 @@ impl SpecTake for Take { { let mut acc = init; let end = self.n.min(self.iter.size()); + // Kani: the loop writes only `acc` and its counter, so `end` and + // `self.iter` keep their entry values and `end <= self.iter.size()` + // stays available to the body; the invariant only has to bound the + // counter. + #[safety::loop_invariant(kani::index <= end)] for i in 0..end { // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end let val = unsafe { self.iter.__iterator_get_unchecked(i) }; @@ -310,6 +317,8 @@ impl SpecTake for Take { #[inline] fn spec_for_each(mut self, mut f: F) { let end = self.n.min(self.iter.size()); + // Kani: same frame as `spec_fold`; see the note there. + #[safety::loop_invariant(kani::index <= end)] for i in 0..end { // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end let val = unsafe { self.iter.__iterator_get_unchecked(i) }; @@ -374,3 +383,60 @@ impl A, A> ExactSizeIterator for Take> self.n } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|v| *v != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + // On a `TrustedRandomAccess` source, `SpecTake::spec_fold` / `spec_for_each` + // drive an `i < end` loop calling `__iterator_get_unchecked(i)` where + // `end = self.n.min(self.iter.size())`; this proves those unchecked indexes + // stay in bounds. The 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_spec_take { + ($fold_harness:ident, $each_harness:ident, $elem_ty:ty, $max_len:expr) => { + #[kani::proof] + fn $fold_harness() { + const MAX_LEN: usize = $max_len; + let array: [$elem_ty; MAX_LEN] = kani::any(); + let n = kani::any_where(|n: &usize| *n <= MAX_LEN); + let it = Take::new(any_slice(&array).iter(), n); + let _ = it.spec_fold(0usize, |acc, _| acc.wrapping_add(1)); + } + + #[kani::proof] + fn $each_harness() { + const MAX_LEN: usize = $max_len; + let array: [$elem_ty; MAX_LEN] = kani::any(); + let n = kani::any_where(|n: &usize| *n <= MAX_LEN); + let it = Take::new(any_slice(&array).iter(), n); + it.spec_for_each(|_| {}); + } + }; + } + check_spec_take!( + check_take_spec_fold_unit, + check_take_spec_for_each_unit, + (), + isize::MAX as usize + ); + check_spec_take!(check_take_spec_fold_u8, check_take_spec_for_each_u8, u8, u32::MAX as usize); + check_spec_take!(check_take_spec_fold_char, check_take_spec_for_each_char, char, 10); + check_spec_take!(check_take_spec_fold_tup, check_take_spec_for_each_tup, (char, u8), 10); +} diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs index e39f1535bd95d..f80e5564e4613 100644 --- a/library/core/src/iter/adapters/zip.rs +++ b/library/core/src/iter/adapters/zip.rs @@ -28,6 +28,12 @@ impl Zip { ZipImpl::new(a, b) } fn super_nth(&mut self, mut n: usize) -> Option<(A::Item, B::Item)> { + // Kani: this loop stays bounded. The blocking construct is the + // `while let` over the generic `Iterator::next`: for a general `Zip` + // no size relation is available to a loop invariant. When the + // specialized `nth` calls this function, its contracted loop has + // already consumed `delta = min(n, len - index)` items, so this loop + // runs at most one iteration for any source length. while let Some(x) = Iterator::next(self) { if n == 0 { return Some(x); @@ -270,6 +276,7 @@ where } #[inline] + #[requires(idx < Iterator::size_hint(self).0)] #[cfg_attr(kani, kani::modifies(self))] unsafe fn get_unchecked(&mut self, idx: usize) -> ::Item { let idx = self.index + idx; @@ -285,6 +292,11 @@ where { let mut accum = init; let len = ZipImpl::size_hint(&self).0; + // Kani: the loop writes only `accum` and its counter, so `len`, + // `self.index`, `self.a` and `self.b` keep their entry values and + // `self.index + len == self.len <= min(a.size(), b.size())` stays + // available to the body; the invariant only has to bound the counter. + #[safety::loop_invariant(kani::index <= len)] for i in 0..len { // SAFETY: since Self: TrustedRandomAccessNoCoerce we can trust the size-hint to // calculate the length and then use that to do unchecked iteration. @@ -334,6 +346,11 @@ where fn nth(&mut self, n: usize) -> Option { let delta = cmp::min(n, self.len - self.index); let end = self.index + delta; + // Kani: the loop writes only `self.index`, so `end`, `self.len`, + // `self.a` and `self.b` keep their entry values and + // `end <= self.len <= min(a.size(), b.size())` stays available to the + // body; the invariant only has to bound `self.index`. + #[safety::loop_invariant(self.index <= end)] while self.index < end { let i = self.index; // since get_unchecked executes code which can panic we increment the counters beforehand @@ -386,6 +403,13 @@ where // This condition can and must only be true on the first `next_back` call, // otherwise we will break the restriction on calls to `self.next_back()` // after calling `get_unchecked()`. + // Kani: the two adjust loops below stay bounded. The blocking + // construct is `next_back` on the generic inner iterators. It + // moves their private pointer state, and no public interface + // lets a loop invariant pin that state to its allocation, so + // a loop contract would havoc it into an unverifiable read. + // Harnesses that reach these loops keep a small MAX_LEN and + // an unwind bound sized to it. if sz_a != sz_b && (old_len == sz_a || old_len == sz_b) { if A::MAY_HAVE_SIDE_EFFECT && sz_a > old_len { for _ in 0..sz_a - old_len { @@ -655,6 +679,10 @@ impl SpecFold for Zip { F: FnMut(Acc, Self::Item) -> Acc, { let mut accum = init; + // Kani: this loop stays bounded. The blocking construct is the + // `while let` over the generic `ZipImpl::next`: for a general `Zip` + // no size relation is available to a loop invariant, and the generic + // `FnMut` closure state gives the havoc no expressible frame. while let Some(x) = ZipImpl::next(&mut self) { accum = f(accum, x); } @@ -669,6 +697,10 @@ impl SpecFold for Zip { F: FnMut(Acc, Self::Item) -> Acc, { let mut accum = init; + // Kani: the outer loop stays bounded. It runs one iteration for each + // `usize::MAX` chunk of a `TrustedLen` source. Every harnessed source + // reports an exact `Some` upper bound, so the loop body runs exactly + // once and a small unwind bound covers it. loop { let (upper, more) = if let Some(upper) = ZipImpl::size_hint(&self).1 { (upper, false) @@ -677,6 +709,12 @@ impl SpecFold for Zip { (usize::MAX, true) }; + // Kani: this loop stays bounded. The blocking construct is + // `next` on the generic inner iterators: it moves their private + // pointer state, and no public interface lets a loop invariant + // pin that state to its allocation, so a loop contract would + // havoc it into an unverifiable read. Harnesses that reach this + // loop keep a small MAX_LEN and an unwind bound sized to it. for _ in 0..upper { let pair = // SAFETY: TrustedLen guarantees that at least `upper` many items are available @@ -692,3 +730,297 @@ impl SpecFold for Zip { accum } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|val| *val != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + fn any_zip_iter<'a, T, U>( + orig_slice_a: &'a [T], + orig_slice_b: &'a [U], + ) -> Zip, crate::slice::Iter<'a, U>> { + Zip::new(any_slice(orig_slice_a).iter(), any_slice(orig_slice_b).iter()) + } + + macro_rules! check_zip_get_unchecked { + ($harness:ident, $elem_ty_a:ty, $elem_ty_b:ty, $max_len:expr) => { + #[kani::proof] + fn $harness() { + const MAX_LEN: usize = $max_len; + let array_a: [$elem_ty_a; MAX_LEN] = kani::any(); + let array_b: [$elem_ty_b; MAX_LEN] = kani::any(); + let mut it = any_zip_iter::<$elem_ty_a, $elem_ty_b>(&array_a, &array_b); + let idx = kani::any_where(|i: &usize| *i < crate::iter::Iterator::size_hint(&it).0); + let _ = unsafe { it.__iterator_get_unchecked(idx) }; + } + }; + } + + check_zip_get_unchecked!(check_zip_get_unchecked_unit_unit, (), (), 50); + check_zip_get_unchecked!(check_zip_get_unchecked_u8_u8, u8, u8, u32::MAX as usize); + check_zip_get_unchecked!(check_zip_get_unchecked_char_u8, char, u8, 50); + check_zip_get_unchecked!(check_zip_get_unchecked_u8_char, u8, char, 50); + check_zip_get_unchecked!(check_zip_get_unchecked_tup_tup, (char, u8), (u32, i16), 50); + + // Direct proof for the separately listed `ZipImpl::get_unchecked` target, + // over an arbitrary valid `Zip` state instead of only a freshly built one. + // The `TrustedRandomAccess` specialization establishes `index == 0` and + // `len == min(a.size(), b.size())` at construction; `next` only increments + // `index` and `next_back` only decrements `len`, so every reachable state + // satisfies `index <= len <= min(a.size(), b.size())`. The caller + // contract for `get_unchecked(idx)` is `idx < size_hint().0`, that is + // `idx < len - index`. The body then computes `self.index + idx`, which + // this proof shows stays in bounds of both sources (and cannot overflow). + macro_rules! check_zip_get_unchecked_direct { + ($harness:ident, $elem_ty_a:ty, $elem_ty_b:ty, $max_len:expr) => { + #[kani::proof] + fn $harness() { + const MAX_LEN: usize = $max_len; + let array_a: [$elem_ty_a; MAX_LEN] = kani::any(); + let array_b: [$elem_ty_b; MAX_LEN] = kani::any(); + let slice_a = any_slice(&array_a); + let slice_b = any_slice(&array_b); + let bound = cmp::min(slice_a.len(), slice_b.len()); + let len = kani::any_where(|l: &usize| *l <= bound); + let index = kani::any_where(|i: &usize| *i <= len); + let mut it = Zip { a: slice_a.iter(), b: slice_b.iter(), index, len }; + let idx = kani::any_where(|i: &usize| *i < len - index); + let _ = unsafe { ZipImpl::get_unchecked(&mut it, idx) }; + } + }; + } + + check_zip_get_unchecked_direct!(check_zip_get_unchecked_direct_unit_unit, (), (), 50); + check_zip_get_unchecked_direct!( + check_zip_get_unchecked_direct_u8_u8, + u8, + u8, + u32::MAX as usize + ); + check_zip_get_unchecked_direct!(check_zip_get_unchecked_direct_char_u8, char, u8, 50); + check_zip_get_unchecked_direct!(check_zip_get_unchecked_direct_u8_char, u8, char, 50); + check_zip_get_unchecked_direct!( + check_zip_get_unchecked_direct_tup_tup, + (char, u8), + (u32, i16), + 50 + ); + + // Safe `Zip` methods on `TrustedRandomAccess` sources drive the same + // `get_unchecked`-based machinery as `__iterator_get_unchecked`; these prove + // `next` / `nth` / `next_back` / `fold` / `spec_fold` keep their internal + // indexes in bounds. The iteration loops in the specialized `nth`, the + // specialized `fold` and the `TrustedLen` `spec_fold` carry loop + // contracts, so `MAX_LEN` follows the accessor menu above instead of a + // bound the unwind limit must cover. The remaining unwind attributes + // cover only the loops that stay bounded: `super_nth` runs at most one + // iteration after the contracted `nth` loop, and the `spec_fold` outer + // loop runs exactly once for these sources. Both counts do not depend on + // `MAX_LEN`. + macro_rules! check_zip_safe { + ($a:ty, $b:ty, $max_len:expr, $spec_max_len:expr, $nth_unwind:literal, $next:ident, + $nth:ident, $back:ident, $fold:ident, $spec:ident) => { + #[kani::proof] + fn $next() { + const MAX_LEN: usize = $max_len; + let array_a: [$a; MAX_LEN] = kani::any(); + let array_b: [$b; MAX_LEN] = kani::any(); + let mut it = any_zip_iter::<$a, $b>(&array_a, &array_b); + let _ = crate::iter::Iterator::next(&mut it); + } + // `nth` drives the contracted `while self.index < end` loop, so + // `$nth_unwind` only has to cover `super_nth` (at most one + // iteration) and the element-wise `kani::any` array construction + // of `MAX_LEN` items for the wider element types. + #[kani::proof] + #[kani::unwind($nth_unwind)] + fn $nth() { + const MAX_LEN: usize = $max_len; + let array_a: [$a; MAX_LEN] = kani::any(); + let array_b: [$b; MAX_LEN] = kani::any(); + let mut it = any_zip_iter::<$a, $b>(&array_a, &array_b); + // Requests beyond the remaining length, including usize::MAX, + // must exhaust the iterator without overflowing or reading past it. + let n: usize = kani::any(); + let _ = crate::iter::Iterator::nth(&mut it, n); + } + #[kani::proof] + fn $back() { + const MAX_LEN: usize = $max_len; + let array_a: [$a; MAX_LEN] = kani::any(); + let array_b: [$b; MAX_LEN] = kani::any(); + let mut it = any_zip_iter::<$a, $b>(&array_a, &array_b); + let _ = crate::iter::DoubleEndedIterator::next_back(&mut it); + } + #[kani::proof] + fn $fold() { + const MAX_LEN: usize = $max_len; + let array_a: [$a; MAX_LEN] = kani::any(); + let array_b: [$b; MAX_LEN] = kani::any(); + let it = any_zip_iter::<$a, $b>(&array_a, &array_b); + let _ = crate::iter::Iterator::fold(it, 0usize, |acc, _| acc.wrapping_add(1)); + } + #[kani::proof] + #[kani::unwind(7)] + fn $spec() { + const MAX_LEN: usize = $spec_max_len; + let array_a: [$a; MAX_LEN] = kani::any(); + let array_b: [$b; MAX_LEN] = kani::any(); + let it = any_zip_iter::<$a, $b>(&array_a, &array_b); + let _ = SpecFold::spec_fold(it, 0usize, |acc, _| acc.wrapping_add(1)); + } + }; + } + check_zip_safe!( + (), + (), + 50, + 5, + 3, + check_zip_next_unit, + check_zip_nth_unit, + check_zip_next_back_unit, + check_zip_fold_unit, + check_zip_spec_fold_unit + ); + check_zip_safe!( + u8, + u8, + u32::MAX as usize, + 5, + 3, + check_zip_next_u8, + check_zip_nth_u8, + check_zip_next_back_u8, + check_zip_fold_u8, + check_zip_spec_fold_u8 + ); + check_zip_safe!( + char, + u8, + 10, + 5, + 12, + check_zip_next_char_u8, + check_zip_nth_char_u8, + check_zip_next_back_char_u8, + check_zip_fold_char_u8, + check_zip_spec_fold_char_u8 + ); + check_zip_safe!( + (char, u8), + (u32, i16), + 10, + 5, + 12, + check_zip_next_tup, + check_zip_nth_tup, + check_zip_next_back_tup, + check_zip_fold_tup, + check_zip_spec_fold_tup + ); + + // `Map` is a `TrustedRandomAccess` source with + // `MAY_HAVE_SIDE_EFFECT = true` (map.rs pins the constant to `true` for + // every `Map`). Zipping one or both sides through `Map` compiles in the + // `A::MAY_HAVE_SIDE_EFFECT` / `B::MAY_HAVE_SIDE_EFFECT` branches of the + // specialized `nth` and `next_back` (including next_back's length-adjust + // loop), which the plain `slice::Iter` harnesses compile out. The two + // `any_slice` lengths are independent, so the `sz_a != sz_b` adjust path + // is reachable. + fn bump(x: &u8) -> u8 { + x.wrapping_add(1) + } + + fn side_effect_iter<'a>( + slice: &'a [u8], + ) -> crate::iter::Map, fn(&u8) -> u8> { + slice.iter().map(bump as fn(&u8) -> u8) + } + + fn plain_iter<'a>(slice: &'a [u8]) -> crate::slice::Iter<'a, u8> { + slice.iter() + } + + macro_rules! check_zip_side_effect { + ($nth:ident, $back:ident, $mk_a:ident, $mk_b:ident, $back_shape:expr) => { + // The contracted `nth` loop covers arbitrary lengths; the unwind + // bound covers only `super_nth`, which runs at most one + // iteration. + #[kani::proof] + #[kani::unwind(3)] + fn $nth() { + const MAX_LEN: usize = u32::MAX as usize; + let array_a: [u8; MAX_LEN] = kani::any(); + let array_b: [u8; MAX_LEN] = kani::any(); + let mut it = Zip::new($mk_a(any_slice(&array_a)), $mk_b(any_slice(&array_b))); + // The request can exceed either backing slice's length. + let n: usize = kani::any(); + let _ = crate::iter::Iterator::nth(&mut it, n); + } + + // `next_back` reaches the bounded adjust loops in the + // specialized `next_back`, so this harness keeps a small + // `MAX_LEN` with an unwind bound sized to it. + // + // `$back_shape` restricts the source lengths. With exactly one + // side-effect side, a plain longer side is never trimmed (the + // trim loops guard on `MAY_HAVE_SIDE_EFFECT`), so upstream's + // `debug_assert_eq!(self.a.size(), self.b.size())` after the + // trim fires with debug assertions on: a debug-only false + // assertion in std, out of scope for this PR (upstream issue + // pending). The excluded shape is "the side-effect side is + // shorter than a plain side"; the `both` variant excludes + // nothing. + #[kani::proof] + #[kani::unwind(7)] + fn $back() { + const MAX_LEN: usize = 5; + let array_a: [u8; MAX_LEN] = kani::any(); + let array_b: [u8; MAX_LEN] = kani::any(); + let slice_a = any_slice(&array_a); + let slice_b = any_slice(&array_b); + let shape: fn(usize, usize) -> bool = $back_shape; + kani::assume(shape(slice_a.len(), slice_b.len())); + let mut it = Zip::new($mk_a(slice_a), $mk_b(slice_b)); + let _ = crate::iter::DoubleEndedIterator::next_back(&mut it); + } + }; + } + + check_zip_side_effect!( + check_zip_nth_side_effect_a, + check_zip_next_back_side_effect_a, + side_effect_iter, + plain_iter, + |len_a, len_b| len_a >= len_b + ); + check_zip_side_effect!( + check_zip_nth_side_effect_b, + check_zip_next_back_side_effect_b, + plain_iter, + side_effect_iter, + |len_a, len_b| len_b >= len_a + ); + check_zip_side_effect!( + check_zip_nth_side_effect_both, + check_zip_next_back_side_effect_both, + side_effect_iter, + side_effect_iter, + |_, _| true + ); +} diff --git a/verifast-proofs/README.md b/verifast-proofs/README.md index 096d3e32e9061..3609743607d1f 100644 --- a/verifast-proofs/README.md +++ b/verifast-proofs/README.md @@ -7,6 +7,10 @@ Specifically, it currently contains the following proofs: - Partial proof of [LinkedList](alloc/collections/linked_list.rs/) - Partial proof of [RawVec](alloc/raw_vec/mod.rs/) +- Generic contracts for selected [iterator adapter methods](core/iter/adapters/), + with passing proof and source refinement checks. See its README for caller + obligations, trusted backend extensions, and remaining coverage. + See each proof's accompanying README for a tour of the proof and applicable caveats. ## Maintaining the proofs diff --git a/verifast-proofs/core/iter/adapters/README.md b/verifast-proofs/core/iter/adapters/README.md new file mode 100644 index 0000000000000..f11b6eea6b664 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/README.md @@ -0,0 +1,259 @@ +# Generic iterator adapter proof port + +This port proves generic contracts for part of Challenge 16. Hosted run +[34762580703](https://github.com/model-checking/verify-rust-std/actions/runs/34762580703) +at `6cc9cce69aac424a7fe6604165357921f26ac34d` passed the full adapter proof, +source refinement, source identity checks, and every backend regression gate. +Coverage is limited to the contracts below and depends on the documented +caller obligations and trusted backend extensions. Other Challenge 16 targets +and the complete safe abstraction remain open. + +The functions retain generic type parameters. `Buffer` also retains +symbolic `N`; there are no representative element types, fixed array sizes, +or unwind bounds. The target contracts are: + +| Target | Contract being checked | +| --- | --- | +| `StepBy::original_step` | Preserve the step field and return its nonzero successor, for any `I`. | +| `Buffer::as_array_ref` | Derive the active window's reference from its shared borrow and valid buffer bounds. | +| `Buffer::as_uninit_array_mut` | Derive a writable window from an exclusive borrow of the backing array, without requiring initialized `T` values. | +| `Buffer::push` | Consume one new `T`, drop the old front, and preserve ownership of the shifted window on normal return. | +| `Buffer::drop` | Drop exactly the initialized window and recover its storage on normal return and unwind. | + +The two raw buffer pointer helpers also have contracts. `push` and `drop` +use the standard library specification of generic drop glue. The +`drop` safety proof recovers field storage on both outcomes through one lifetime +loan frame. The `push` unwind postcondition +retains the surviving values, backing storage, and borrow token in +`push_drop_frame`, together with the old front's storage after destruction. +`finish_push_storage` proves that those resources restore `live`, including +after a panicking element destructor. + +## Ownership and bounds + +`live` separates initialized slots from ownership of their values. Only the +active window carries `.own`. Inactive storage can contain stale copied +bytes, but carries no ownership of `T`. The wraparound copy moves the +survivors' logical ownership to the destination. It does not duplicate it. +`initialized_slots` and `wrap_slots` recursively relate `MaybeUninit` +storage to initialized `T` storage, without requiring `Copy`, `Clone`, or +a particular destructor. + +The preconditions require `0 < N`, `start <= N`, representable `2 * N`, +and the allocation/layout limits of the real buffer. These follow from the +intended `MapWindows` constructor and Rust layout restrictions. They are +explicit caller obligations here. Constructor preservation and the surrounding +`MapWindows` iterator implementation are outside this projection. + +The shared accessor requires a lifetime borrow of the window. The mutable +accessor requires a borrow of the whole backing array of initialized +`MaybeUninit` wrappers because its pointer helper borrows that array. +These wrappers can contain uninitialized bytes and need no `T` ownership. +Establishing those borrows from the full safe +abstraction is outside this port. The mutable accessor accepts storage that +does not yet own initialized `T` values, as required by the clone path. + +## Source correspondence + +The annotated projection expands the three window-bound `debug_assert!` calls +into their `if cfg!(debug_assertions) { assert!(...) }` bodies. Both refinement +inputs and the full proof explicitly enable debug assertions; refinement must +establish the equivalence of these bodies. A ghost assertion proves each bounds +condition before the expansion. Line-local reachability directives account for +the disabled configuration branch and the excluded assertion failure path. + +One line-local `allow_dead_code` directive covers Rust's generated cleanup for +the `next` argument at the end of `push`. Hosted MIR inspection shows its drop +flag is cleared on both branches before the only potentially unwinding call. +An explicit `live` assertion after restoration keeps the normal completion +path subject to reachability checking. No global dead-code option is used. +A mandatory negative fixture gives a function contradictory preconditions and +permits only its generated return to be unreachable. The ghost assertion must +still be rejected, guarding the normal-path check used in `push`. + +`source/` contains complete, hashed copies of the two std source files. +`source-map.json` records the exact lines projected into `original/`: +the actual struct declarations and selected method implementations. +Private core dependencies and unrelated iterator implementations are omitted. +The projections are not alternative iterator models. + +`check_sources.py` checks snapshot hashes, equality with the current std files, +exact projection contents, matching crate roots, and the presence of a +contract on every selected method. It also rejects common proof suppression +directives. This lexical guard does not parse or validate VeriFast proofs. +Only a successful verifier run can establish the contracts. + +The annotated version keeps the original pointer helper bodies and names +returned references so ghost assertions can follow their construction. +Private proof methods are marked `unsafe` to express their explicit caller +obligations. The upstream refinement checker permits this change for private +functions; the original projection and standard library keep their original +signatures. The `Drop` trait implementation retains its safe signature and +must establish its contract from the type ownership invariant. +`refinement-checker` must establish that these changes +preserve the projected Rust behavior. It is mandatory, even if VeriFast +passes. No compiler directives are ignored during refinement. + +To deliberately refresh an original projection after reviewing a source +update, update the snapshot, its hash, and its ranges, then run: + +```sh +python3 -I check_sources.py --generate-original +``` + +Normal checks never regenerate or silently accept changed sources. + +## Validation with GitHub Actions + +The [iterator adapter workflow](../../../../.github/workflows/verifast-iter-adapters.yml) +uses a temporary GitHub-hosted Ubuntu 24.04 runner. No separately maintained +machine is needed. It runs when these proof inputs change in a pull request, +or on pushes to `16-iter-adapters` and `main`, and for merge queue checks. +Actions must be enabled in the repository. Standard public-repository jobs use +[GitHub's free hosted runners](https://docs.github.com/en/actions/reference/runners/github-hosted-runners). + +The workflow checks the source snapshots and contract selection before +running the proof and refinement stages. A systemd service limits their +entire process tree to 4 GiB RAM, no swap, two CPUs, 256 tasks, and 25 minutes. +The job has a 30-minute timeout and cancels superseded runs. Tool errors, +proof failures, and resource-limit failures fail the job. Verification and +refinement stay sequential and retain the per-process limits below. + +Run [34762580703](https://github.com/model-checking/verify-rust-std/actions/runs/34762580703) +verified 433 statements in the full adapter proof and 149 in the standalone +matrix-layout fixture on `x86_64-unknown-linux-gnu`. The full refinement checker +accepted the annotated implementations, and the source checker confirmed their +original projections against the current std snapshots. All positive and +negative backend fixtures passed, including the reachability guard. The source +checker also passed its nine tests. No compiler or verifier was run locally. + +The runner uses VeriFast 26.09 plus the narrow frontend patch in +`backend/add-unchecked.patch`. It maps `AddUnchecked` to the existing integer +addition operation, whose symbolic execution checks overflow. On inputs +where no overflow occurs, unchecked addition has the same result. Outside +that domain, unchecked addition is undefined, and the verifier must reject it. +Before checking the adapters, the runner requires a valid successor proof +and an explicit overflow diagnostic for the same operation without its +range precondition. A frontend crash does not count as the negative result. + +`backend/const-generics.patch` adds symbolic `usize` const arguments and +array lengths using the existing `typeid`/`usize_of_const` representation. +It keeps const parameters distinct from Rust types and does not add `Sized` +bounds to them. The exporter rejects other const parameter types. A positive +symbolic-length proof and an incorrect-length negative test must pass before +the adapter contracts are checked. + +The same patch routes array ownership and borrowing through VeriFast's +existing type predicates. It also removes the upstream frontend's blanket +shortcut for mutable-reference creation. Mandatory regression gates cover +valid arithmetic, symbolic width, +shared array reborrowing, and mutable array reference creation; rejection +of overflow, a wrong width, missing shared ownership, and missing mutable +storage. The mutable test converts the new reference to a raw pointer to +test creation independently of a further return reborrow. These fixtures +validate the frontend extension, not the adapter contracts. + +The `MaybeUninit` pointer `cast_init` translation is an ordinary raw-pointer +cast, matching its [Rust implementation](https://github.com/rust-lang/rust/blob/master/library/core/src/ptr/mut_ptr.rs). +It preserves the address and grants no permission to read or drop `T`. +The runner checks both address preservation and rejection of a read without +initialized storage before checking the adapters. + +The patch also preserves const operands and `ConstArgHasType` constraints +through the MIR schema and refinement checker. Constraints are compared after +generic parameter renaming; unsupported predicates still fail refinement. +The refinement fixtures require acceptance of a renamed const parameter and +rejection of a change in the returned value from `N` to `M`. + +`backend/prepare.sh` pins the source commit, source archive hash, and upstream +dependency bundle hash. It builds the MIR exporter, verifier, and refinement +checker on the hosted Linux worker. Arithmetic rules and the existing borrowing +and destruction contracts are unchanged. Mandatory source refinement still +checks the selected implementations. The workflow caches these three +binaries and the library specification, keyed by the preparation script and +patches, with checksums checked on restoration. Every regression, proof, and +refinement gate reruns after a cache hit. + +`backend/nonzero-usize.patch` adds one trusted library contract for the +`usize` instantiation of `NonZero::new_unchecked`. It requires a positive +input, preserves its value through `get()`, and cannot unwind. This matches +the [standard library implementation and its safety requirement](../../../../library/core/src/num/nonzero.rs). +The frontend routes only the `usize` instantiation to this specification. +Other instantiations remain unsupported. The constructor implementation is +not proved by this port; the new specification is part of its trusted library +boundary. A positive fixture and rejection of a missing nonzero precondition +are mandatory. + +`backend/maybeuninit-ownership.patch` extends the trusted library specification +with introduction and disposal rules for `MaybeUninit` ownership. Owning +that wrapper does not require ownership of a contained `T`; its memory remains +tracked by separate storage predicates. These rules model the wrapper's +ownership semantics and are not proved from its implementation by this port. +A positive wrapper fixture and rejection of missing ownership of an ordinary +`T` are mandatory. No new borrowing or generic drop contract is introduced. + +`backend/array-layout.patch` supplies trusted size and alignment relations for +array type IDs and `MaybeUninit`. The facts follow the +[Rust array layout guarantee](https://doc.rust-lang.org/reference/type-layout.html#array-layout) +and the wrapper's documented layout. They include zero-sized element types. +The matrix conversion and writable-window proofs remain mandatory; the layout +facts do not grant storage or ownership permissions. +The patch also removes implicit `Sized` bounds from the array length parameters +of the existing array conversion lemmas. Symbolic const parameters are +not Rust value types. The element type bounds and every storage precondition +remain in force, and the patched prelude is cached with checksum validation. + +`backend/array-subtyping.patch` models the standard covariance, fixed element +count, and `Send` conditions of arrays and `MaybeUninit`, plus representation +preservation under [Rust subtyping](https://doc.rust-lang.org/reference/subtyping.html). +The `Send` conditions follow the [array](https://doc.rust-lang.org/std/primitive.array.html#impl-Send-for-%5BT;+N%5D) +and [wrapper](https://doc.rust-lang.org/std/mem/union.MaybeUninit.html#impl-Send-for-MaybeUninit%3CT%3E) +implementations. These are trusted type-model facts. The +`Buffer` ownership proofs must still transfer every active element's ownership; +they cannot produce generic `T` ownership from those facts. Negative fixtures +require rejection when the subtype relation or `T: Send` is missing. + +## Local static checks and optional manual verification + +The static check reads small files and starts no compiler or solver: + +```sh +bash verifast-proofs/core/iter/adapters/verify.sh --static +``` + +On a separate Linux machine with at least 8 GiB currently available RAM: + +```sh +bash verifast-proofs/core/iter/adapters/verify.sh --remote +``` + +The runner uses the repository's VeriFast 26.09 wrappers and Rust +nightly 2026-02-05, with the frontend patch described above. The wrappers +can download their toolchains. The remote build needs `capnp`, `rustc-dev`, +and `llvm-tools`; the workflow installs them. Each proof process +has a 2 GiB address-space limit, each verification stage has a ten-minute +wall limit, and the stages run sequentially. Address-space limits are per +process, not a combined memory cap. Use an otherwise idle remote worker with +sufficient headroom. The runner refuses proof execution on macOS. + +The command must pass all three gates: proof verification, refinement, and +source identity. `-skip_specless_fns` skips derived trait implementations +without contracts, while the source check requires contracts on every target. +The runner does not suppress unwind paths, overflow checks, or reference +creation checks, and does not allow assumed proof obligations. + +The existing VeriFast workflow is unchanged. The separate adapter job checks +these contracts without altering the existing LinkedList and RawVec checks. + +## Remaining work + +- Prove constructor preservation and establish the accessor borrows from the + full safe abstraction, including the surrounding `MapWindows` implementation. +- Port the remaining Challenge 16 targets, including arbitrary-length filter, + filter-map, and zip iteration. This package has no proof of those loops. +- Reconcile the real nonempty-source `next_chunk::<0>()` defect in filter and + filter-map. The `MapWindows` constructor's exclusion of zero-sized windows + does not justify excluding that separate, valid filter input domain. + +Existing Kani results remain bounded where documented. The successful VeriFast +run establishes only the selected contracts, not completion of Challenge 16. diff --git a/verifast-proofs/core/iter/adapters/array_layout.rs b/verifast-proofs/core/iter/adapters/array_layout.rs new file mode 100644 index 0000000000000..c7a7ceb9b0f94 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/array_layout.rs @@ -0,0 +1,280 @@ +/*@ + +pred_ctor array_owned()(t: thread_id_t, value: [T; N]) = + foreach(Array_elems(value), own::(t)); +type_pred_def for <[T; N]>.own = array_owned::; + +lem mapped_append(f: fix(a, b), xs: list, ys: list) + req true; + ens map(f, append(xs, ys)) == append(map(f, xs), map(f, ys)); +{ + match xs { + nil => {} + cons(x, rest) => { mapped_append(f, rest, ys); } + } +} + +lem mapped_length(f: fix(a, b), xs: list) + req true; + ens length(map(f, xs)) == length(xs); +{ + match xs { + nil => {} + cons(x, rest) => { mapped_length(f, rest); } + } +} + +lem joined_window(prefix: list, window: list, suffix: list) + req true; + ens take(length(window), drop(length(prefix), append(append(prefix, window), suffix))) == window; +{ + append_assoc(prefix, window, suffix); + drop_append(length(prefix), prefix, append(window, suffix)); + take_append_l(length(window), window, suffix); +} + +lem mapped_range(f: fix(a, b), xs: list, start: usize, count: usize) + req 0 <= start &*& 0 <= count; + ens take(count, drop(start, map(f, xs))) == map(f, take(count, drop(start, xs))); +{ + match xs { + nil => {} + cons(x, rest) => { + if start > 0 { + mapped_range(f, rest, start - 1, count); + } else { + if count > 0 { mapped_range(f, rest, 0, count - 1); } + } + } + } +} + +lem owned_values_mono(t: thread_id_t, values: list) + req type_interp::() &*& type_interp::() &*& + is_subtype_of::() == true &*& foreach(values, own::(t)); + ens type_interp::() &*& type_interp::() &*& + foreach(map::(upcast, values), own::(t)); +{ + match values { + nil => { + open foreach(values, own::(t)); + close foreach(map::(upcast, values), own::(t)); + } + cons(value, rest) => { + open foreach(values, own::(t)); + open own::(t)(value); + own_mono::(t, value); + close own::(t)(upcast::(value)); + owned_values_mono::(t, rest); + close foreach(map::(upcast, values), own::(t)); + } + } +} + +lem owned_values_send(t0: thread_id_t, t1: thread_id_t, values: list) + req type_interp::() &*& is_Send(typeid(T)) == true &*& foreach(values, own::(t0)); + ens type_interp::() &*& foreach(values, own::(t1)); +{ + match values { + nil => { + open foreach(values, own::(t0)); + close foreach(values, own::(t1)); + } + cons(value, rest) => { + open foreach(values, own::(t0)); + open own::(t0)(value); + Send::send::(t0, t1, value); + close own::(t1)(value); + owned_values_send(t0, t1, rest); + close foreach(values, own::(t1)); + } + } +} + +lem mapped_uninit_upcast(values: list) + req is_subtype_of::() == true; + ens map::, std::mem::MaybeUninit>(upcast, + map(std::mem::MaybeUninit::new, values)) == + map(std::mem::MaybeUninit::new, map::(upcast, values)); +{ + match values { + nil => {} + cons(value, rest) => { + std::mem::MaybeUninit_upcast_new::(value); + mapped_uninit_upcast::(rest); + } + } +} + +fix matrix_elems(matrix: [[T; N]; 2]) -> list { + append(Array_elems(head(Array_elems(matrix))), + Array_elems(head(tail(Array_elems(matrix))))) +} + +lem matrix_upcast(matrix: [[T0; N]; 2]) + req is_subtype_of::() == true; + ens matrix_elems::(upcast::<[[T0; N]; 2], [[T1; N]; 2]>(matrix)) == + map::(upcast, matrix_elems(matrix)); +{ + std::mem::array_subtype::(); + std::mem::array_upcast::<[T0; N], [T1; N], 2>(matrix); + std::mem::array_elems_length::<[T0; N], 2>(matrix); + match Array_elems(matrix) { + nil => {} + cons(first, rest) => { + match rest { + nil => {} + cons(second, suffix) => { + std::mem::array_upcast::(first); + std::mem::array_upcast::(second); + mapped_append::(upcast, Array_elems(first), Array_elems(second)); + } + } + } + } +} + +// Keep a fraction while changing representations so precision relates the values. +pred_ctor saved_array(p: *T, count: usize, elems: list)(;) = + [1/2]array(p, count, elems); + +lem pack_array(p: *[T; N]) + req (p as *T)[..usize_of_const(typeid(N))] |-> ?elems; + ens *p |-> ?array &*& Array_elems(array) == elems; +{ + close saved_array::(p as *T, usize_of_const(typeid(N)), elems)(); + array_to_Array(p); + Array_to_array(p); + open saved_array::(p as *T, usize_of_const(typeid(N)), elems)(); + merge_fractions array(p as *T, usize_of_const(typeid(N)), _); + array_to_Array(p); +} + +lem unpack_matrix(p: *[[T; N]; 2]) + req *p |-> ?matrix; + ens (p as *T)[..2 * usize_of_const(typeid(N))] |-> matrix_elems(matrix); +{ + std::mem::array_layout::(); + Array_to_array(p); + open array(p as *[T; N], 2, _); + open array((p as *[T; N]) + 1, 1, _); + open array((p as *[T; N]) + 2, 0, _); + Array_to_array(p as *[T; N]); + Array_to_array((p as *[T; N]) + 1); + array_join(p as *T); +} + +lem pack_matrix(p: *[[T; N]; 2]) + req (p as *T)[..2 * usize_of_const(typeid(N))] |-> ?elems; + ens *p |-> ?matrix &*& matrix_elems(matrix) == elems; +{ + std::mem::array_layout::(); + array_split(p as *T, usize_of_const(typeid(N))); + pack_array(p as *[T; N]); + pack_array((p as *[T; N]) + 1); + assert *(p as *[T; N]) |-> ?first; + assert *((p as *[T; N]) + 1) |-> ?second; + close array((p as *[T; N]) + 2, 0, nil); + close array((p as *[T; N]) + 1, 1, cons(second, nil)); + close array(p as *[T; N], 2, cons(first, cons(second, nil))); + pack_array(p); +} + +// These conversions preserve writable storage. They do not claim initialized T values. +lem collapse_window(p: *std::mem::MaybeUninit) + req p[..usize_of_const(typeid(N))] |-> ?slots; + ens *(p as *std::mem::MaybeUninit<[T; N]>) |-> ?window; +{ + std::mem::array_layout::(); + std::mem::MaybeUninit_layout::(); + array_to_array_(p); + array__to_u8s_(p, usize_of_const(typeid(N))); + from_u8s_(p as *[T; N]); + std::mem::close_MaybeUninit_(p as *std::mem::MaybeUninit<[T; N]>); +} + +lem expand_window(p: *std::mem::MaybeUninit<[T; N]>) + req *p |-> ?window; + ens (p as *std::mem::MaybeUninit)[..usize_of_const(typeid(N))] |-> ?slots; +{ + std::mem::MaybeUninit_layout::(); + std::mem::open_MaybeUninit(p); + Array__to_array_(p as *[T; N]); + std::mem::array__to_array_MaybeUninit(p as *T); +} + +lem own_uninit_values(t: thread_id_t, values: list>) + req true; + ens foreach(values, own::>(t)); +{ + match values { + nil => { close foreach(values, own::>(t)); } + cons(value, rest) => { + std::mem::MaybeUninit_own_init(t, value); + close own::>(t)(value); + own_uninit_values(t, rest); + close foreach(values, own::>(t)); + } + } +} + +lem own_uninit_rows(t: thread_id_t, rows: list<[std::mem::MaybeUninit; N]>) + req true; + ens foreach(rows, own::<[std::mem::MaybeUninit; N]>(t)); +{ + match rows { + nil => { close foreach(rows, own::<[std::mem::MaybeUninit; N]>(t)); } + cons(row, rest) => { + own_uninit_values(t, Array_elems(row)); + close array_owned::, N>()(t, row); + close own::<[std::mem::MaybeUninit; N]>(t)(row); + own_uninit_rows(t, rest); + close foreach(rows, own::<[std::mem::MaybeUninit; N]>(t)); + } + } +} + +lem own_matrix_storage(t: thread_id_t, matrix: [[std::mem::MaybeUninit; N]; 2]) + req true; + ens <[[std::mem::MaybeUninit; N]; 2]>.own(t, matrix); +{ + own_uninit_rows(t, Array_elems(matrix)); + close array_owned::<[std::mem::MaybeUninit; N], 2>()(t, matrix); +} + +pred array_borrow_tokens(k: lifetime_t, p: *T, count: usize) = + pointer_within_limits(p) == true &*& + if count == 0 { true } else { + points_to_at_lft_end_token(k, p) &*& array_borrow_tokens(k, p + 1, count - 1) + }; + +lem lend_array(k: lifetime_t, p: *T, count: usize) + req p[..count] |-> ?values &*& 0 <= count; + ens array_at_lft(k, p, count, values) &*& array_borrow_tokens(k, p, count); +{ + open array(p, count, values); + if count > 0 { + borrow_points_to_at_lft(k, p); + lend_array(k, p + 1, count - 1); + } + close array_at_lft(k, p, count, values); + close array_borrow_tokens(k, p, count); +} + +lem reclaim_array(k: lifetime_t, p: *T, count: usize) + req array_borrow_tokens(k, p, count) &*& 0 <= count &*& + [_]lifetime_dead_token(k) &*& array_at_lft_(k, p, count, _); + ens p[..count] |-?-> _; +{ + open array_borrow_tokens(k, p, count); + open array_at_lft_(k, p, count, _); + if count > 0 { + borrow_points_to_at_lft_end(p); + // Discard expired lifetime bookkeeping after recovering the storage. + leak points_to_at_lft_(k, p, _); + reclaim_array(k, p + 1, count - 1); + } + close array_(p, count, _); +} + +@*/ diff --git a/verifast-proofs/core/iter/adapters/backend/add-overflow.rs b/verifast-proofs/core/iter/adapters/backend/add-overflow.rs new file mode 100644 index 0000000000000..6ea7d45d2305e --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/add-overflow.rs @@ -0,0 +1,11 @@ +#![crate_type = "lib"] +#![crate_name = "add_overflow"] +#![feature(core_intrinsics)] + +unsafe fn successor(value: usize) -> usize +//@ req true; +//@ ens true; +//@ on_unwind_ens false; +{ + unsafe { std::intrinsics::unchecked_add(value, 1) } +} diff --git a/verifast-proofs/core/iter/adapters/backend/add-unchecked.patch b/verifast-proofs/core/iter/adapters/backend/add-unchecked.patch new file mode 100644 index 0000000000000..bb2abe4b1ddde --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/add-unchecked.patch @@ -0,0 +1,12 @@ +--- a/src/rust_frontend/vf_mir_exporter/src/lib.rs ++++ b/src/rust_frontend/vf_mir_exporter/src/lib.rs +@@ -2422,6 +2422,9 @@ + fn encode_bin_op(bin_op: mir::BinOp, mut bin_op_cpn: bin_op_cpn::Builder<'_>) { + match bin_op { + mir::BinOp::Add => bin_op_cpn.set_add(()), ++ // VeriFast checks integer addition for overflow. Unchecked addition ++ // has the same result on that domain and is undefined outside it. ++ mir::BinOp::AddUnchecked => bin_op_cpn.set_add(()), + mir::BinOp::Sub => bin_op_cpn.set_sub(()), + mir::BinOp::Mul => bin_op_cpn.set_mul(()), + mir::BinOp::Div => bin_op_cpn.set_div(()), diff --git a/verifast-proofs/core/iter/adapters/backend/add-valid.rs b/verifast-proofs/core/iter/adapters/backend/add-valid.rs new file mode 100644 index 0000000000000..1c9b0a7737b46 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/add-valid.rs @@ -0,0 +1,11 @@ +#![crate_type = "lib"] +#![crate_name = "add_valid"] +#![feature(core_intrinsics)] + +unsafe fn successor(value: usize) -> usize +//@ req value < usize::MAX; +//@ ens result == value + 1; +//@ on_unwind_ens false; +{ + unsafe { std::intrinsics::unchecked_add(value, 1) } +} diff --git a/verifast-proofs/core/iter/adapters/backend/array-invalid.rs b/verifast-proofs/core/iter/adapters/backend/array-invalid.rs new file mode 100644 index 0000000000000..38cfdd121aa0f --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/array-invalid.rs @@ -0,0 +1,11 @@ +#![crate_type = "lib"] +#![crate_name = "array_invalid"] + +unsafe fn shared<'a, T, const N: usize>(p: *const [T; N]) -> &'a [T; N] +//@ req thread_token(?t) &*& [?q]lifetime_token('a) &*& [?r]ref_initialized(p); +//@ ens thread_token(t) &*& [q]lifetime_token('a) &*& result == p &*& [_](<[T; N]>.share)('a, t, result) &*& [r]ref_initialized(p); +//@ on_unwind_ens false; +{ + //@ reborrow_ref_(p); + unsafe { &*p } +} diff --git a/verifast-proofs/core/iter/adapters/backend/array-layout.patch b/verifast-proofs/core/iter/adapters/backend/array-layout.patch new file mode 100644 index 0000000000000..7e2755d544544 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/array-layout.patch @@ -0,0 +1,28 @@ +--- a/bin/rust/std/lib.rsspec ++++ b/bin/rust/std/lib.rsspec +@@ -373,0 +374,11 @@ ++ // Rust array layout and MaybeUninit transparency, including zero-sized T. ++ lem array_layout(); ++ req true; ++ ens std::mem::size_of(typeid([T; N])) == std::mem::size_of::() * usize_of_const(typeid(N)) &*& ++ std::mem::align_of::<[T; N]>() == std::mem::align_of::(); ++ ++ lem MaybeUninit_layout(); ++ req true; ++ ens std::mem::size_of::>() == std::mem::size_of::() &*& ++ std::mem::align_of::>() == std::mem::align_of::(); ++ +@@ -478 +489 @@ +- lem Array__MaybeUninit_to_Array_MaybeUninit(self: *[MaybeUninit; N]); ++ lem Array__MaybeUninit_to_Array_MaybeUninit(self: *[MaybeUninit; N]); +--- a/bin/rust/prelude_core.rsspec ++++ b/bin/rust/prelude_core.rsspec +@@ -315 +315 @@ +-lem Array__to_array_(p: *[T; N]); ++lem Array__to_array_(p: *[T; N]); +@@ -319 +319 @@ +-lem Array_to_array(p: *[T; N]); ++lem Array_to_array(p: *[T; N]); +@@ -323 +323 @@ +-lem array_to_Array(p: *[T; N]); ++lem array_to_Array(p: *[T; N]); diff --git a/verifast-proofs/core/iter/adapters/backend/array-length-invalid.rs b/verifast-proofs/core/iter/adapters/backend/array-length-invalid.rs new file mode 100644 index 0000000000000..abba535bbf91a --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/array-length-invalid.rs @@ -0,0 +1,12 @@ +#![crate_type = "lib"] +#![crate_name = "array_length_invalid"] + +unsafe fn array_len(p: *const [T; N]) -> usize +//@ req [?f]ref_initialized(p); +//@ ens [f]ref_initialized(p) &*& result == usize_of_const(typeid(N)) + 1; +//@ on_unwind_ens false; +{ + //@ reborrow_ref_(p); + let slice: &[T] = unsafe { &*p }; + slice.len() +} diff --git a/verifast-proofs/core/iter/adapters/backend/array-mut-invalid.rs b/verifast-proofs/core/iter/adapters/backend/array-mut-invalid.rs new file mode 100644 index 0000000000000..ff22a6f85f32d --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/array-mut-invalid.rs @@ -0,0 +1,10 @@ +#![crate_type = "lib"] +#![crate_name = "array_mut_invalid"] + +unsafe fn exclusive(p: *mut [T; N]) -> *mut [T; N] +//@ req true; +//@ ens true; +//@ on_unwind_ens false; +{ + unsafe { &mut *p as *mut [T; N] } +} diff --git a/verifast-proofs/core/iter/adapters/backend/array-subtyping.patch b/verifast-proofs/core/iter/adapters/backend/array-subtyping.patch new file mode 100644 index 0000000000000..58e1464023adf --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/array-subtyping.patch @@ -0,0 +1,49 @@ +--- a/bin/rust/std/lib.rsspec ++++ b/bin/rust/std/lib.rsspec +@@ -381,6 +381,46 @@ + req true; + ens std::mem::size_of::>() == std::mem::size_of::() &*& + std::mem::align_of::>() == std::mem::align_of::(); ++ ++ // Rust subtyping changes lifetime information, preserving layout and values. ++ lem upcast_identity(value: T); ++ req true; ++ ens upcast::(value) == value; ++ ++ lem subtype_layout(); ++ req is_subtype_of::() == true; ++ ens std::mem::size_of::() == std::mem::size_of::() &*& ++ std::mem::align_of::() == std::mem::align_of::(); ++ ++ lem array_subtype(); ++ req is_subtype_of::() == true; ++ ens is_subtype_of::<[T0; N], [T1; N]>() == true; ++ ++ lem array_upcast(value: [T0; N]); ++ req is_subtype_of::() == true; ++ ens Array_elems(upcast::<[T0; N], [T1; N]>(value)) == ++ map::(upcast, Array_elems(value)); ++ ++ lem array_elems_length(value: [T; N]); ++ req true; ++ ens length(Array_elems(value)) == usize_of_const(typeid(N)); ++ ++ lem MaybeUninit_subtype(); ++ req is_subtype_of::() == true; ++ ens is_subtype_of::, MaybeUninit>() == true; ++ ++ lem MaybeUninit_upcast_new(value: T0); ++ req is_subtype_of::() == true; ++ ens upcast::, MaybeUninit>(MaybeUninit::new(value)) == ++ MaybeUninit::new(upcast::(value)); ++ ++ lem array_Send(); ++ req true; ++ ens is_Send(typeid([T; N])) == is_Send(typeid(T)); ++ ++ lem MaybeUninit_Send(); ++ req true; ++ ens is_Send(typeid(MaybeUninit)) == is_Send(typeid(T)); + + fix size_of_val(x: *T) -> usize; + fix align_of_val(x: *T) -> usize; diff --git a/verifast-proofs/core/iter/adapters/backend/array-valid.rs b/verifast-proofs/core/iter/adapters/backend/array-valid.rs new file mode 100644 index 0000000000000..d65ac982d8755 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/array-valid.rs @@ -0,0 +1,52 @@ +#![crate_type = "lib"] +#![crate_name = "array_valid"] + +unsafe fn shared<'a, T, const N: usize>(p: *const [T; N]) -> &'a [T; N] +//@ req thread_token(?t) &*& [?q]lifetime_token('a) &*& [_](<[T; N]>.share)('a, t, p) &*& [?r]ref_initialized(p); +//@ ens thread_token(t) &*& [q]lifetime_token('a) &*& result == p &*& [_](<[T; N]>.share)('a, t, result) &*& [r]ref_initialized(p); +//@ on_unwind_ens false; +{ + //@ reborrow_ref_(p); + unsafe { &*p } +} + +// Return the new reference as a raw pointer to test creation independently +// of the extra lifetime reborrow inserted when returning a mutable reference. +unsafe fn exclusive(p: *mut [T; N]) -> *mut [T; N] +//@ req *p |-> ?values; +//@ ens *result |-> values &*& ref_mut_end_token(result, p); +//@ on_unwind_ens false; +{ + unsafe { &mut *p as *mut [T; N] } +} + +unsafe fn matrix_ptr( + p: *const [[std::mem::MaybeUninit; N]; 2], +) -> *const std::mem::MaybeUninit +//@ req pointer_within_limits(p) == true &*& [?f]ref_initialized(p); +//@ ens [f]ref_initialized(p) &*& result == p as *std::mem::MaybeUninit; +//@ on_unwind_ens false; +{ + //@ reborrow_ref_(p); + unsafe { (*p).as_ptr().cast() } +} + +unsafe fn matrix_mut_ptr( + p: *mut [[std::mem::MaybeUninit; N]; 2], +) -> *mut std::mem::MaybeUninit +//@ req *p |-> ?matrix; +//@ ens *(result as *[[std::mem::MaybeUninit; N]; 2]) |-> matrix &*& ref_mut_end_token(result as *[[std::mem::MaybeUninit; N]; 2], p); +//@ on_unwind_ens false; +{ + unsafe { (*p).as_mut_ptr().cast() } +} + +unsafe fn array_len(p: *const [T; N]) -> usize +//@ req [?f]ref_initialized(p); +//@ ens [f]ref_initialized(p) &*& result == usize_of_const(typeid(N)); +//@ on_unwind_ens false; +{ + //@ reborrow_ref_(p); + let slice: &[T] = unsafe { &*p }; + slice.len() +} diff --git a/verifast-proofs/core/iter/adapters/backend/cast-init-invalid.rs b/verifast-proofs/core/iter/adapters/backend/cast-init-invalid.rs new file mode 100644 index 0000000000000..97d5704eb0733 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/cast-init-invalid.rs @@ -0,0 +1,11 @@ +#![crate_type = "lib"] +#![crate_name = "cast_init_invalid"] +#![feature(cast_maybe_uninit)] + +unsafe fn read_without_storage(p: *mut std::mem::MaybeUninit) -> T +//@ req true; +//@ ens true; +//@ on_unwind_ens false; +{ + unsafe { p.cast_init().read() } +} diff --git a/verifast-proofs/core/iter/adapters/backend/cast-init-valid.rs b/verifast-proofs/core/iter/adapters/backend/cast-init-valid.rs new file mode 100644 index 0000000000000..ece9d3da93d38 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/cast-init-valid.rs @@ -0,0 +1,11 @@ +#![crate_type = "lib"] +#![crate_name = "cast_init_valid"] +#![feature(cast_maybe_uninit)] + +unsafe fn cast_pointer(p: *mut std::mem::MaybeUninit) -> *mut T +//@ req true; +//@ ens result == p as *T; +//@ on_unwind_ens false; +{ + p.cast_init() +} diff --git a/verifast-proofs/core/iter/adapters/backend/const-generics.patch b/verifast-proofs/core/iter/adapters/backend/const-generics.patch new file mode 100644 index 0000000000000..9c824b8521cfa --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/const-generics.patch @@ -0,0 +1,331 @@ +--- a/src/rust_frontend/vf_mir/vf_mir.capnp ++++ b/src/rust_frontend/vf_mir/vf_mir.capnp +@@ -422,6 +422,10 @@ + outlives @0: Outlives; + trait @2: Trait; + projection @3: Projection; ++ constArgHasType :group { ++ constant @4: TyConst; ++ ty @5: Ty; ++ } + ignored @1: Void; # A predicate that we are ignoring for now + } + } +@@ -681,6 +685,7 @@ + kind @2: CastKind; + operand @0: Operand; + ty @1: Ty; ++ sourceTy @3: Ty; + } + + struct AggregateData { +--- a/src/rust_frontend/vf_mir_exporter/src/lib.rs ++++ b/src/rust_frontend/vf_mir_exporter/src/lib.rs +@@ -1224,6 +1224,13 @@ + Self::encode_typesystem_constant(enc_ctx.tcx, enc_ctx, &const_, term_cpn.init_const()), + } + } ++ ty::ClauseKind::ConstArgHasType(constant, ty) => { ++ let mut constraint_cpn = pred_cpn.init_const_arg_has_type(); ++ Self::encode_typesystem_constant( ++ enc_ctx.tcx, enc_ctx, &constant, constraint_cpn.reborrow().init_constant(), ++ ); ++ Self::encode_ty(enc_ctx.tcx, enc_ctx, ty, constraint_cpn.init_ty()); ++ } + _ => pred_cpn.set_ignored(()), + } + } +@@ -1539,6 +1546,11 @@ + p: &hir::GenericParam, + mut p_cpn: hir_generic_param_cpn::Builder<'_>, + ) { ++ if matches!(p.kind, hir::GenericParamKind::Const { .. }) ++ && enc_ctx.tcx.type_of(p.def_id).instantiate_identity() != enc_ctx.tcx.types.usize ++ { ++ enc_ctx.tcx.dcx().span_fatal(p.span, "Only usize const parameters are supported"); ++ } + let name_cpn = p_cpn.reborrow().init_name(); + Self::encode_hir_generic_param_name(enc_ctx, p.def_id, &p.name, name_cpn); + let span_cpn = p_cpn.reborrow().init_span(); +@@ -2287,6 +2299,9 @@ + } + let operand_cpn = cast_data_cpn.reborrow().init_operand(); + Self::encode_operand(tcx, enc_ctx, operand, operand_cpn); ++ let source_ty = operand.ty(&enc_ctx.body().local_decls, tcx); ++ let source_ty_cpn = cast_data_cpn.reborrow().init_source_ty(); ++ Self::encode_ty(tcx, enc_ctx, source_ty, source_ty_cpn); + let ty_cpn = cast_data_cpn.init_ty(); + Self::encode_ty(tcx, enc_ctx, *ty, ty_cpn); + } +--- a/src/rust_frontend/vf_mir_translator/vf_mir_translator.ml ++++ b/src/rust_frontend/vf_mir_translator/vf_mir_translator.ml +@@ -801,8 +801,9 @@ + let targs = + gen_args + |> Util.flatmap @@ function +- | Mir.GenArgType arg_ty -> [ arg_ty.vf_ty ] +- | _ -> [] ++ | Mir.GenArgType arg_ty -> [ arg_ty.vf_ty ] ++ | Mir.GenArgConst const_ty -> [ const_ty ] ++ | _ -> [] + in + let lft_args = + gen_args +@@ -1247,6 +1248,7 @@ + | Const ty_const_cpn -> + let ty_expr = + match ty_const_cpn.kind with ++ | Param {name; index} -> Ast.IdentTypeExpr (loc, None, name) + | Value {ty; val_tree} -> + begin match val_tree with + | Leaf {data; size} -> +@@ -1272,7 +1274,7 @@ + match get (kind_get gen_param_cpn) with + | Type -> `Type name + | Lifetime -> `Lifetime name +- | Const -> failwith "Const generic parameters are not yet supported" ++ | Const -> `Const name + + and decode_generic_arg (gen_arg_cpn : D.generic_arg) = + let kind_cpn = gen_arg_cpn.kind in +@@ -1641,7 +1643,10 @@ + and translate_ty_const_kind (ck_cpn : D.const_kind) (loc : Ast.loc) = + let open VfMirRd.ConstKind in + match ck_cpn with +- | Param _ -> Ast.static_error loc "Todo: ConstKind::Param" None ++ | Param {name; index} -> ++ Ok (Ast.CallExpr (loc, "usize_of_const", [], [], ++ [Ast.LitPat (Ast.Typeid (loc, Ast.TypeExpr (Ast.IdentTypeExpr (loc, None, name))))], ++ Ast.Static)) + | Infer -> Ast.static_error loc "Todo: ConstKind::Infer" None + | Bound -> Ast.static_error loc "Todo: ConstKind::Bound" None + | Placeholder -> Ast.static_error loc "Todo: ConstKind::Placeholder" None +@@ -1666,20 +1671,18 @@ + let* elem_ty_info = translate_ty elem_ty_cpn loc in + let elem_ty = elem_ty_info.vf_ty in + let len_cpn = array_ty_cpn.size in +- let* (CastExpr (_, _, IntLit (_, len, _, _, _))) = +- translate_ty_const len_cpn loc +- in ++ let* Mir.GenArgConst len_ty = translate_generic_arg {kind = Const len_cpn} loc in + let vf_ty = +- Ast.StaticArrayTypeExpr +- (loc, elem_ty, LiteralConstTypeExpr (loc, Z.of_big_int len)) ++ Ast.StaticArrayTypeExpr (loc, elem_ty, len_ty) + in + let size = Ast.SizeofExpr (loc, TypeExpr vf_ty) in + let own tid vs = +- Error "Expressing ownership of an array is not yet supported" ++ Ok (Ast.ExprCallExpr (loc, Ast.TypePredExpr (loc, vf_ty, "own"), ++ [Ast.LitPat tid; Ast.LitPat vs])) + in + let full_bor_content t l = +- Error +- "Expressing the full borrow content of an array is not yet supported" ++ Ok (Ast.ExprCallExpr (loc, Ast.TypePredExpr (loc, vf_ty, "full_borrow_content"), ++ [Ast.LitPat t; Ast.LitPat l])) + in + let points_to tid l vid_op = + let* pat = RustBelt.Aux.vid_op_to_var_pat vid_op loc in +@@ -1692,9 +1695,9 @@ + own; + shr = + (fun k t l -> +- Error +- "Expressing the shared ownership of an array is not yet \ +- supported"); ++ Ok (Ast.CoefAsn (loc, Ast.DummyPat, ++ Ast.ExprCallExpr (loc, Ast.TypePredExpr (loc, vf_ty, "share"), ++ [Ast.LitPat k; Ast.LitPat t; Ast.LitPat l])))); + full_bor_content; + points_to; + pointee_fbc = None; +@@ -2433,7 +2436,22 @@ + Ok + ( tmp_rvalue_binders, + FnCallResult (CastExpr (fn_loc, PtrTypeExpr (fn_loc, ManifestTypeExpr (fn_loc, Int (Unsigned, FixedWidthRank 0))), arg)) ) +- | "std::slice::::as_ptr" -> ++ | "std::ptr::const_ptr::::cast" ++ | "std::ptr::mut_ptr::::cast" -> ( ++ match substs, args with ++ | [ Mir.GenArgType _; Mir.GenArgType target ], [ arg ] -> ++ Ok (tmp_rvalue_binders, FnCallResult ++ (Ast.CastExpr (fn_loc, PtrTypeExpr (fn_loc, target.vf_ty), arg))) ++ | inputs -> Error (`TrFnCallRExpr "Invalid generic arguments for pointer cast")) ++ | "std::ptr::mut_ptr::>::cast_init" ++ | "std::ptr::mut_ptr::>::cast_init" -> ( ++ match substs, args with ++ | [ Mir.GenArgType target ], [ arg ] -> ++ Ok (tmp_rvalue_binders, FnCallResult ++ (Ast.CastExpr (fn_loc, PtrTypeExpr (fn_loc, target.vf_ty), arg))) ++ | inputs -> Error (`TrFnCallRExpr "Invalid generic arguments for MaybeUninit pointer cast")) ++ | "std::slice::::as_ptr" ++ | "std::slice::::as_mut_ptr" -> + let [ Mir.GenArgType gen_arg_ty_info; _ ] = substs in + let [ arg ] = args in + Ok +@@ -3020,11 +3038,8 @@ + let* place_expr, place_is_mutable = translate_place place_cpn loc in + let (path, line, _), _ = Ast.lexed_loc loc in + let ignore_ref_creation = +- bor_kind = Mut +- || + not place_is_mutable && place_does_not_need_drop + || +- (* ignore &mut E for now *) + if TranslatorArgs.ignore_ref_creation then true + else + let directives = +@@ -3157,12 +3172,34 @@ + Ok (`TrRvalueExpr e) + | _ -> + let* ty_info = translate_decoded_ty cast_data.ty loc in +- let ty = ty_info.vf_ty in ++ let ty = ++ match ty_info.vf_ty with ++ | Ast.RustRefTypeExpr (_, Ast.InferredTypeExpr _, _, (Ast.SliceTypeExpr _ as slice_ty)) ++ when cast_data.kind = D.PointerCoercion -> ++ (* The borrow is checked by Rvalue::Ref; this coercion only adds slice metadata. *) ++ Ast.PtrTypeExpr (loc, slice_ty) ++ | ty -> ty ++ in ++ let cast_expr expr = ++ match cast_data.kind, cast_data.source_ty.kind, cast_data.ty.kind with ++ | D.PointerCoercion, ++ (D.Ref {ty = {kind = D.Array array_ty}} | D.RawPtr {ty = {kind = D.Array array_ty}}), ++ (D.Ref {ty = {kind = D.Slice elem_ty}} | D.RawPtr {ty = {kind = D.Slice elem_ty}}) -> ++ let* elem_ty_info = translate_decoded_ty elem_ty loc in ++ let* len = translate_ty_const array_ty.size loc in ++ (* Unsize preserves the borrowed data pointer and adds the array length. *) ++ let call = Ast.CallExpr (loc, "std::ptr::slice_from_raw_parts_mut", ++ [elem_ty_info.vf_ty], [], ++ [LitPat (Ast.CastExpr (loc, PtrTypeExpr (loc, elem_ty_info.vf_ty), expr)); ++ LitPat len], Static) in ++ Ok (`TrRvalueExpr (result_of_outcome loc call)) ++ | cast -> Ok (`TrRvalueExpr (Ast.CastExpr (loc, ty, expr))) ++ in + match operand with + | `TrOperandCopy expr + | `TrOperandMove (expr, _ (*place_is_mutable*)) + | `TrTypedConstantScalar expr -> +- Ok (`TrRvalueExpr (Ast.CastExpr (loc, ty, expr))) ++ cast_expr expr + | `TrTypedConstantRvalueBinderBuilder rvalue_binder_builder -> + failwith "Todo: Rvalue::Cast" + (*Todo @Nima: We need a better design (refactor) for passing different results of operand translation*) +@@ -5993,17 +6030,18 @@ + with + | Lifetime -> Ok (`Lifetime name) + | Type -> Ok (`Type name) +- | Const -> +- raise +- (Ast.StaticError +- ( l, +- "Structs with const parameters are not yet supported", +- None )) ++ | Const -> ++ Ok (`Const name) + in + let tparams = +- Util.flatmap (function `Type x -> [ x ] | _ -> []) generics +- in +- let tparams_with_bounds = Verifast0.tparams_with_default_bounds_exprs tparams in ++ Util.flatmap (function `Type x | `Const x -> [ x ] | `Lifetime _ -> []) generics ++ in ++ let const_params = ++ Util.flatmap (function `Const x -> [ x ] | `Type _ | `Lifetime _ -> []) generics ++ in ++ let tparams_with_bounds = ++ List.map (fun x -> (x, {Ast.sized = not (List.mem x const_params)})) tparams ++ in + let lft_params = + Util.flatmap (function `Lifetime x -> [ x ] | _ -> []) generics + in +@@ -6029,7 +6067,9 @@ + |> List.map decode_predicate + in + let sized_tparams = compute_sized_tparams preds in +- let unsized_tparams = List.filter (fun x -> not (List.mem x sized_tparams)) tparams in ++ let unsized_tparams = ++ List.filter (fun x -> not (List.mem x sized_tparams || List.mem x const_params)) tparams ++ in + let send_tparams = compute_send_tparams preds in + let tparams_targs = + List.map (fun x -> Ast.IdentTypeExpr (def_loc, None, x)) vf_tparams +--- a/src/refinement_checker/refinement_checker.ml ++++ b/src/refinement_checker/refinement_checker.ml +@@ -320,6 +320,7 @@ + | Closure of term list + | FnDef of string * gen_arg list + | ScalarInt of literal_const_expr ++| ConstParamTerm of string + | StaticPtr of string + | ConstPtr of string (* The bytes the constant pointer points to *) + | SliceConstant of ty * string +@@ -335,6 +336,7 @@ + | EnumValue (variant, ts) -> Printf.sprintf "EnumValue %s %s" variant (string_of_terms ts) + | FnDef (fn, genArgs) -> Printf.sprintf "FnDef %s [%s]" fn (String.concat "; " (List.map string_of_gen_arg genArgs)) + | ScalarInt literal -> Printf.sprintf "ScalarInt %s" (string_of_literal_const_expr literal) ++| ConstParamTerm name -> Printf.sprintf "ConstParamTerm %s" name + | ConstPtr bytes -> Printf.sprintf "ConstPtr %s" bytes + | SliceConstant (ty, bytes) -> Printf.sprintf "SliceConstant %s %s" (string_of_ty ty) bytes + | Closure ts -> Printf.sprintf "Closure %s" (string_of_terms ts) +@@ -362,7 +364,11 @@ + + let eval_mir_const genv mir_const_cpn = + match mir_const_cpn with +- Ty mir_ty_const_cpn -> failwith "Using typesystem constant expressions as MIR constant operands is not yet supported" ++ Ty mir_ty_const_cpn -> ++ begin match decode_const_expr genv mir_ty_const_cpn.const with ++ ParamConstExpr name -> ConstParamTerm name ++ | LiteralConstExpr literal -> ScalarInt literal ++ end + | Val mir_val_const_cpn -> + let ty = decode_ty genv mir_val_const_cpn.ty in + let mir_const_value_cpn = mir_val_const_cpn.const_value in +@@ -442,6 +448,7 @@ + lhs_place=local "contents_ptr"; + rhs_rvalue=Cast { + kind=PtrToPtr; ++ source_ty={kind=RawPtr {mutability=Not; ty={kind=Param "T"}}}; + operand=Copy { + local={name="self"}; + projection=[ +@@ -472,6 +479,7 @@ + lhs_place=local "contents_ptr2"; + rhs_rvalue=Cast { + kind=PtrToPtr; ++ source_ty={kind=RawPtr {mutability=Not; ty={kind=Param "T"}}}; + operand=Copy { + local={name="self"}; + projection=[ +@@ -658,6 +666,7 @@ + lhs_place=local "result"; + rhs_rvalue=Cast { + kind=PtrToPtr; ++ source_ty={kind=RawPtr {mutability=Not; ty={kind=Param "T"}}}; + operand=Copy { + local={name="b"}; + projection=[ +@@ -2336,7 +2345,20 @@ + let projection_preds1, preds1 = List.partition (function Projection _ -> true | _ -> false) preds1 in + if List.length projection_preds0 <> List.length projection_preds1 then failwith "The two functions have a different number of projection predicates"; + List.iter2 (fun pred0 pred1 -> check_predicate_refines_predicate root_genv0 pred0 root_genv1 pred1) projection_preds0 projection_preds1; +- if preds0 <> [] || preds1 <> [] then failwith "Predicate kind not supported"; ++ let is_const_predicate = function ++ | ConstArgHasType _ -> true ++ | Outlives _ | Trait _ | Projection _ | Ignored -> false ++ in ++ let decode_const_predicate genv = function ++ | ConstArgHasType pred -> Some (decode_const_expr genv pred.constant, decode_ty genv pred.ty) ++ | Outlives _ | Trait _ | Projection _ | Ignored -> None ++ in ++ let const_preds0, preds0 = List.partition is_const_predicate preds0 in ++ let const_preds1, preds1 = List.partition is_const_predicate preds1 in ++ if preds0 <> [] || preds1 <> [] || ++ List.map (decode_const_predicate root_genv0) const_preds0 <> ++ List.map (decode_const_predicate root_genv1) const_preds1 then ++ failwith "Predicate kind not supported or const parameter predicates differ"; + let inputs0 = body0.inputs in + let inputs1 = body1.inputs in + let inputs0 = List.map (decode_ty root_genv0) inputs0 in diff --git a/verifast-proofs/core/iter/adapters/backend/const-invalid.rs b/verifast-proofs/core/iter/adapters/backend/const-invalid.rs new file mode 100644 index 0000000000000..c95d465b6b173 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/const-invalid.rs @@ -0,0 +1,14 @@ +#![crate_type = "lib"] +#![crate_name = "const_invalid"] + +struct Window { + values: [T; N], +} + +fn width(_: &Window) -> usize +//@ req true; +//@ ens result == usize_of_const(typeid(N)) + 1; +//@ on_unwind_ens false; +{ + N +} diff --git a/verifast-proofs/core/iter/adapters/backend/const-valid.rs b/verifast-proofs/core/iter/adapters/backend/const-valid.rs new file mode 100644 index 0000000000000..21ccb291ee377 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/const-valid.rs @@ -0,0 +1,14 @@ +#![crate_type = "lib"] +#![crate_name = "const_valid"] + +struct Window { + values: [T; N], +} + +fn width(_: &Window) -> usize +//@ req true; +//@ ens result == usize_of_const(typeid(N)); +//@ on_unwind_ens false; +{ + N +} diff --git a/verifast-proofs/core/iter/adapters/backend/ghost-reachability-invalid.rs b/verifast-proofs/core/iter/adapters/backend/ghost-reachability-invalid.rs new file mode 100644 index 0000000000000..f450e13f22142 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/ghost-reachability-invalid.rs @@ -0,0 +1,10 @@ +#![crate_type = "lib"] +#![crate_name = "ghost_reachability_invalid"] + +unsafe fn inconsistent_input(value: bool) +//@ req value == true &*& value == false; +//@ ens true; +//@ on_unwind_ens false; +{ + //@ assert true; +} //~allow_dead_code // Allow the return only; the ghost assertion must still fail reachability. diff --git a/verifast-proofs/core/iter/adapters/backend/layout-invalid.rs b/verifast-proofs/core/iter/adapters/backend/layout-invalid.rs new file mode 100644 index 0000000000000..e105380e138fd --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/layout-invalid.rs @@ -0,0 +1,8 @@ +#![allow(dead_code)] + +unsafe fn incorrect_stride() +//@ req true; +//@ ens std::mem::size_of(typeid([T; N])) == std::mem::size_of::() * usize_of_const(typeid(N)) + 1; +{ + //@ std::mem::array_layout::(); +} diff --git a/verifast-proofs/core/iter/adapters/backend/matrix-invalid.rs b/verifast-proofs/core/iter/adapters/backend/matrix-invalid.rs new file mode 100644 index 0000000000000..559672e5dc2b9 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/matrix-invalid.rs @@ -0,0 +1,12 @@ +#![crate_type = "lib"] +#![crate_name = "matrix_invalid"] + +unsafe fn matrix_ptr( + p: *const [[std::mem::MaybeUninit; N]; 2], +) -> *const std::mem::MaybeUninit +//@ req pointer_within_limits(p) == true; +//@ ens result == p as *std::mem::MaybeUninit; +//@ on_unwind_ens false; +{ + unsafe { (*p).as_ptr().cast() } +} diff --git a/verifast-proofs/core/iter/adapters/backend/matrix-layout-valid.rs b/verifast-proofs/core/iter/adapters/backend/matrix-layout-valid.rs new file mode 100644 index 0000000000000..a9cd9861d6dea --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/matrix-layout-valid.rs @@ -0,0 +1,27 @@ +#![crate_type = "lib"] +#![crate_name = "matrix_layout_valid"] + +#[path = "../array_layout.rs"] +mod array_layout; +//@ use array_layout::{collapse_window, expand_window, matrix_elems, pack_array, pack_matrix, unpack_matrix}; + +unsafe fn round_trip(p: *mut [[T; N]; 2]) +//@ req *p |-> ?matrix; +//@ ens *p |-> ?after &*& matrix_elems(after) == matrix_elems(matrix); +//@ on_unwind_ens false; +{ + //@ unpack_matrix(p); + //@ pack_matrix(p); +} + +unsafe fn writable_window(p: *mut [std::mem::MaybeUninit; N]) +//@ req *p |-> _; +//@ ens *p |-> _; +//@ on_unwind_ens false; +{ + //@ std::mem::Array__MaybeUninit_to_Array_MaybeUninit(p); + //@ Array_to_array(p); + //@ collapse_window::(p as *std::mem::MaybeUninit); + //@ expand_window(p as *std::mem::MaybeUninit<[T; N]>); + //@ pack_array(p); +} diff --git a/verifast-proofs/core/iter/adapters/backend/maybeuninit-own-valid.rs b/verifast-proofs/core/iter/adapters/backend/maybeuninit-own-valid.rs new file mode 100644 index 0000000000000..aa1600c2f6ae3 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/maybeuninit-own-valid.rs @@ -0,0 +1,10 @@ +#![crate_type = "lib"] +#![crate_name = "maybeuninit_own_valid"] + +unsafe fn wrapper_ownership(p: *mut std::mem::MaybeUninit) +//@ req thread_token(?t) &*& *p |-> ?value; +//@ ens thread_token(t) &*& *p |-> value &*& >.own(t, value); +//@ on_unwind_ens false; +{ + //@ std::mem::MaybeUninit_own_init(t, value); +} diff --git a/verifast-proofs/core/iter/adapters/backend/maybeuninit-ownership.patch b/verifast-proofs/core/iter/adapters/backend/maybeuninit-ownership.patch new file mode 100644 index 0000000000000..31391218dd9f3 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/maybeuninit-ownership.patch @@ -0,0 +1,18 @@ +--- a/bin/rust/std/lib.rsspec ++++ b/bin/rust/std/lib.rsspec +@@ -436,6 +436,15 @@ + struct MaybeUninit; + + /*@ ++ ++ // MaybeUninit does not own or drop a contained T. Storage is tracked separately. ++ lem MaybeUninit_own_init(t: thread_id_t, value: MaybeUninit); ++ req true; ++ ens >.own(t, value); ++ ++ lem MaybeUninit_own_dispose(t: thread_id_t, value: MaybeUninit); ++ req >.own(t, value); ++ ens true; + + fix MaybeUninit::inner(v: MaybeUninit) -> option; + fix MaybeUninit::uninit() -> MaybeUninit; diff --git a/verifast-proofs/core/iter/adapters/backend/nonzero-invalid.rs b/verifast-proofs/core/iter/adapters/backend/nonzero-invalid.rs new file mode 100644 index 0000000000000..3dbb3f6da4e28 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/nonzero-invalid.rs @@ -0,0 +1,10 @@ +#![crate_type = "lib"] +#![crate_name = "nonzero_invalid"] + +unsafe fn construct(value: usize) -> std::num::NonZero +//@ req true; +//@ ens result.get() == value; +//@ on_unwind_ens false; +{ + unsafe { std::num::NonZero::new_unchecked(value) } +} diff --git a/verifast-proofs/core/iter/adapters/backend/nonzero-usize.patch b/verifast-proofs/core/iter/adapters/backend/nonzero-usize.patch new file mode 100644 index 0000000000000..10ec473a7a4d5 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/nonzero-usize.patch @@ -0,0 +1,37 @@ +--- a/src/rust_frontend/vf_mir_translator/vf_mir_translator.ml ++++ b/src/rust_frontend/vf_mir_translator/vf_mir_translator.ml +@@ -2386,6 +2386,18 @@ + (`TrFnCallRExpr + (Printf.sprintf "Invalid (generic) arg(s) for %s" + fn_name))) ++ | "std::num::NonZero::::new_unchecked" ++ when List.length substs = 1 && ++ List.for_all ++ (function ++ | Mir.GenArgType info -> ++ info.vf_ty = Ast.ManifestTypeExpr ++ (Ast.type_expr_loc info.vf_ty, Ast.Int (Ast.Unsigned, Ast.PtrRank)) ++ | Mir.GenArgLifetime _ | Mir.GenArgConst _ -> false) ++ substs -> ++ Ok (tmp_rvalue_binders, FnCallOutcome ++ (Ast.CallExpr (fn_loc, "std::num::new_nonzero_usize", [], [], ++ List.map (fun arg -> Ast.LitPat arg) args, Ast.Static))) + | "std::ptr::null_mut" -> + Ok + ( [], +--- a/bin/rust/std/lib.rsspec ++++ b/bin/rust/std/lib.rsspec +@@ -265,6 +265,13 @@ + struct NonZero; + + //@ fix NonZero::get(nz: NonZero) -> T; ++ ++ // Trusted library boundary for NonZero::::new_unchecked. ++ // The frontend routes only the usize instantiation to this specification. ++ unsafe fn new_nonzero_usize(value: usize) -> NonZero; ++ //@ req 0 < value; ++ //@ ens result.get() == value; ++ //@ on_unwind_ens false; + + /*@ + diff --git a/verifast-proofs/core/iter/adapters/backend/nonzero-valid.rs b/verifast-proofs/core/iter/adapters/backend/nonzero-valid.rs new file mode 100644 index 0000000000000..a0cb3c76e2668 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/nonzero-valid.rs @@ -0,0 +1,10 @@ +#![crate_type = "lib"] +#![crate_name = "nonzero_valid"] + +unsafe fn construct(value: usize) -> std::num::NonZero +//@ req 0 < value; +//@ ens result.get() == value; +//@ on_unwind_ens false; +{ + unsafe { std::num::NonZero::new_unchecked(value) } +} diff --git a/verifast-proofs/core/iter/adapters/backend/prepare.sh b/verifast-proofs/core/iter/adapters/backend/prepare.sh new file mode 100644 index 0000000000000..a14d91e7979d7 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/prepare.sh @@ -0,0 +1,88 @@ +#!/usr/bin/env bash +set -euo pipefail + +if [[ "$(uname -s)" != Linux || "${1:-}" != --remote ]]; then + echo 'The frontend build is restricted to the remote Linux verification job.' >&2 + exit 2 +fi + +backend_dir="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)" +# The cached exporter still needs the pinned toolchain's shared libraries. +rustup component add --toolchain nightly-2026-02-05 rustc-dev llvm-tools +cache_key="$(sha256sum "$backend_dir/prepare.sh" "$backend_dir/add-unchecked.patch" \ + "$backend_dir/const-generics.patch" "$backend_dir/nonzero-usize.patch" \ + "$backend_dir/maybeuninit-ownership.patch" "$backend_dir/array-layout.patch" \ + "$backend_dir/array-subtyping.patch" | sha256sum | cut -d ' ' -f 1)" +cache_dir="$HOME/.cache/verifast-iter-adapters/$cache_key" +if [[ -f "$cache_dir/checksums" ]]; then + (cd "$cache_dir" && sha256sum --check checksums) + install -m 755 "$cache_dir/verifast" "${VERIFAST_HOME:?}/bin/verifast" + install -m 755 "$cache_dir/vf-rust-mir-exporter" "$VERIFAST_HOME/bin/vf-rust-mir-exporter" + install -m 755 "$cache_dir/refinement-checker" "$VERIFAST_HOME/bin/refinement-checker" + install -m 644 "$cache_dir/std-lib.rsspec" "$VERIFAST_HOME/bin/rust/std/lib.rsspec" + install -m 644 "$cache_dir/prelude_core.rsspec" "$VERIFAST_HOME/bin/rust/prelude_core.rsspec" + echo 'Restored the patched frontend; all proof and regression checks will run' + exit 0 +fi +source_commit=809de4596839b739dd999f9e462242c835e3af46 +source_hash=0238aec44351c877b3c859c7252340540923c1b620f9981be176d7cea4e67a1e +build_dir="$(mktemp -d "${TMPDIR:-/tmp}/verifast-iter-backend.XXXXXXXX")" +trap 'rm -rf -- "$build_dir"' EXIT + +command -v capnp >/dev/null +curl --fail --location --retry 2 --max-time 120 --max-filesize 67108864 \ + --output "$build_dir/source.tar.gz" \ + "https://codeload.github.com/verifast/verifast/tar.gz/$source_commit" +printf '%s %s\n' "$source_hash" "$build_dir/source.tar.gz" | sha256sum --check +tar -xzf "$build_dir/source.tar.gz" --strip-components=1 -C "$build_dir" \ + "verifast-$source_commit/src" "verifast-$source_commit/bin" +patch --batch --fuzz=0 --directory="$build_dir" -p1 < "$backend_dir/add-unchecked.patch" +patch --batch --fuzz=0 --directory="$build_dir" -p1 < "$backend_dir/const-generics.patch" +patch --batch --fuzz=0 --directory="$build_dir" -p1 < "$backend_dir/nonzero-usize.patch" +patch --batch --fuzz=0 --directory="$build_dir" -p1 < "$backend_dir/maybeuninit-ownership.patch" +patch --batch --fuzz=0 --directory="$build_dir" -p1 < "$backend_dir/array-layout.patch" +patch --batch --fuzz=0 --directory="$build_dir" -p1 < "$backend_dir/array-subtyping.patch" + +# Use the dependency bundle pinned by upstream's setup-build.sh. Its compiler +# and package paths are built for /tmp/vfdeps-adf88dc on Linux. +curl --fail --location --retry 2 --max-time 180 --max-filesize 536870912 \ + --output "$build_dir/deps.txz" \ + https://github.com/verifast/vfdeps/releases/download/25.01/vfdeps-adf88dc-linux.txz +printf '%s %s\n' \ + 8d022c93d51a1d13ec1e782d767c60462405f6865d5ee416f82d6234e93ee580 \ + "$build_dir/deps.txz" | sha256sum --check +tar -xjf "$build_dir/deps.txz" --directory=/tmp +export PATH="/tmp/vfdeps-adf88dc/bin:$PATH" +export CAPNP_INCLUDE=/tmp/vfdeps-adf88dc/include +export CAPNP_INC_DIR="$CAPNP_INCLUDE" +# The dynamic linker expands this token after the executable is installed. +# shellcheck disable=SC2016 +export OCAMLOPT_CCLIB_FLAGS='-Wl,-rpath=$ORIGIN' +export Z3_DLL_DIR=/tmp/vfdeps-adf88dc/lib + +CARGO_BUILD_JOBS=1 cargo +nightly-2026-02-05 install --locked --jobs 1 \ + --git https://github.com/btj/capnpc-ocaml-decoder \ + --rev 2d6606d9b59cd0c88a66729f3f076c10c0c8e0b2 --root "$build_dir/decoder" +export PATH="$build_dir/decoder/bin:$PATH" +CARGO_BUILD_JOBS=1 CARGO_PROFILE_DEV_DEBUG=0 RUSTFLAGS='-C rpath=yes' \ + cargo +nightly-2026-02-05 build --locked --jobs 1 \ + --manifest-path "$build_dir/src/rust_frontend/vf_mir_exporter/Cargo.toml" +install -m 755 "$build_dir/src/rust_frontend/vf_mir_exporter/target/debug/vf_mir_exporter" \ + "${VERIFAST_HOME:?}/bin/vf-rust-mir-exporter" +( + cd "$build_dir/src" + dune build -j 1 vfconsole/vfconsole.exe refinement_checker/main.exe +) +install -m 755 "$build_dir/src/_build/default/vfconsole/vfconsole.exe" "$VERIFAST_HOME/bin/verifast" +install -m 755 "$build_dir/src/_build/default/refinement_checker/main.exe" \ + "$VERIFAST_HOME/bin/refinement-checker" +install -m 644 "$build_dir/bin/rust/std/lib.rsspec" "$VERIFAST_HOME/bin/rust/std/lib.rsspec" +install -m 644 "$build_dir/bin/rust/prelude_core.rsspec" "$VERIFAST_HOME/bin/rust/prelude_core.rsspec" +mkdir -p "$cache_dir" +install -m 755 "$VERIFAST_HOME/bin/verifast" "$cache_dir/verifast" +install -m 755 "$VERIFAST_HOME/bin/vf-rust-mir-exporter" "$cache_dir/vf-rust-mir-exporter" +install -m 755 "$VERIFAST_HOME/bin/refinement-checker" "$cache_dir/refinement-checker" +install -m 644 "$VERIFAST_HOME/bin/rust/std/lib.rsspec" "$cache_dir/std-lib.rsspec" +install -m 644 "$VERIFAST_HOME/bin/rust/prelude_core.rsspec" "$cache_dir/prelude_core.rsspec" +(cd "$cache_dir" && sha256sum verifast vf-rust-mir-exporter refinement-checker std-lib.rsspec prelude_core.rsspec > checksums) +echo 'Prepared VeriFast 26.09 with checked addition and symbolic usize const parameters' diff --git a/verifast-proofs/core/iter/adapters/backend/refinement-invalid.rs b/verifast-proofs/core/iter/adapters/backend/refinement-invalid.rs new file mode 100644 index 0000000000000..f9ba5e07db0da --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/refinement-invalid.rs @@ -0,0 +1,6 @@ +#![crate_type = "lib"] +#![crate_name = "const_refinement"] + +pub fn width() -> usize { + M +} diff --git a/verifast-proofs/core/iter/adapters/backend/refinement-original.rs b/verifast-proofs/core/iter/adapters/backend/refinement-original.rs new file mode 100644 index 0000000000000..560363376c188 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/refinement-original.rs @@ -0,0 +1,6 @@ +#![crate_type = "lib"] +#![crate_name = "const_refinement"] + +pub fn width() -> usize { + N +} diff --git a/verifast-proofs/core/iter/adapters/backend/refinement-valid.rs b/verifast-proofs/core/iter/adapters/backend/refinement-valid.rs new file mode 100644 index 0000000000000..45896f2db6565 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/refinement-valid.rs @@ -0,0 +1,6 @@ +#![crate_type = "lib"] +#![crate_name = "const_refinement"] + +pub fn width() -> usize { + A +} diff --git a/verifast-proofs/core/iter/adapters/backend/subtype-invalid.rs b/verifast-proofs/core/iter/adapters/backend/subtype-invalid.rs new file mode 100644 index 0000000000000..99ebb62ec7898 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/subtype-invalid.rs @@ -0,0 +1,8 @@ +#![allow(dead_code)] + +unsafe fn missing_subtype() +//@ req true; +//@ ens true; +{ + //@ std::mem::array_subtype::(); +} diff --git a/verifast-proofs/core/iter/adapters/backend/value-own-invalid.rs b/verifast-proofs/core/iter/adapters/backend/value-own-invalid.rs new file mode 100644 index 0000000000000..b42825bc8938d --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/value-own-invalid.rs @@ -0,0 +1,9 @@ +#![crate_type = "lib"] +#![crate_name = "value_own_invalid"] + +unsafe fn missing_value_ownership(p: *mut T) +//@ req thread_token(?t) &*& *p |-> ?value; +//@ ens thread_token(t) &*& *p |-> value &*& .own(t, value); +//@ on_unwind_ens false; +{ +} diff --git a/verifast-proofs/core/iter/adapters/backend/value-send-invalid.rs b/verifast-proofs/core/iter/adapters/backend/value-send-invalid.rs new file mode 100644 index 0000000000000..e235cf8a884d3 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/backend/value-send-invalid.rs @@ -0,0 +1,9 @@ +#![allow(dead_code)] + +unsafe fn missing_send() +//@ req type_interp::() &*& .own(?t0, ?value) &*& exists::(?t1); +//@ ens type_interp::() &*& .own(t1, value); +{ + //@ open exists::(t1); + //@ Send::send::(t0, t1, value); +} diff --git a/verifast-proofs/core/iter/adapters/check_sources.py b/verifast-proofs/core/iter/adapters/check_sources.py new file mode 100644 index 0000000000000..809ac82b6a1fa --- /dev/null +++ b/verifast-proofs/core/iter/adapters/check_sources.py @@ -0,0 +1,164 @@ +#!/usr/bin/env python3 +"""Check proof inputs without invoking Rust, VeriFast, or a solver.""" + +import argparse +import hashlib +import json +from pathlib import Path +import re +import sys + + +PACKAGE = Path(__file__).resolve().parent +LIMIT = 1024 * 1024 +PROJECTION_HEADER = "// Source projection checked by check_sources.py. Do not edit manually.\n\n" + + +def read_file(path): + with path.open("rb") as source: + data = source.read(LIMIT + 1) + if len(data) > LIMIT: + raise ValueError(f"input exceeds {LIMIT} bytes: {path}") + return data + + +def inside(root, relative): + path = (root / relative).resolve() + if not path.is_relative_to(root.resolve()): + raise ValueError(f"path escapes its input directory: {relative}") + return path + + +def project(data, ranges): + lines = data.decode("utf-8").splitlines(keepends=True) + parts = [] + previous = 0 + for start, end in ranges: + if not 1 <= start <= end <= len(lines) or start <= previous: + raise ValueError(f"invalid or overlapping source range: {start}:{end}") + parts.append("".join(lines[start - 1:end])) + previous = end + return (PROJECTION_HEADER + "\n".join(parts)).encode("utf-8") + + +def mask_comments(text, annotations_only=False): + """Select Rust text or VeriFast comments, preserving source offsets.""" + masked = ["\n" if char == "\n" else " " for char in text] if annotations_only else list(text) + position = 0 + while position < len(text): + if text.startswith("//", position): + end = text.find("\n", position) + end = len(text) if end == -1 else end + elif text.startswith("/*", position): + end = position + 2 + depth = 1 + while depth and end < len(text): + if text.startswith("/*", end): + depth += 1 + end += 2 + elif text.startswith("*/", end): + depth -= 1 + end += 2 + else: + end += 1 + if depth: + raise ValueError("unterminated Rust block comment") + elif text[position] == '"': + position += 1 + while position < len(text) and text[position] != '"': + position += 2 if text[position] == "\\" else 1 + position += 1 + continue + else: + position += 1 + continue + annotation = text.startswith(("//@", "/*@"), position) + for offset in range(position, end): + if annotations_only and annotation: + masked[offset] = text[offset] + elif not annotations_only and text[offset] != "\n": + masked[offset] = " " + position = end + return "".join(masked) + + +def check_contracts(path, names): + text = read_file(path).decode("utf-8") + forbidden = ( + r"\bassume\s*\(", + r"\breq\s+false\s*;", + r"\b(?:allow_assume|ignore_unwind_paths|ignore_ref_creation|disable_overflow_check)\b", + r"#\s*\[\s*cfg(?:_attr)?\s*\(", + ) + if any(re.search(pattern, text) for pattern in forbidden): + raise ValueError(f"verification bypass in {path}") + rust = mask_comments(text) + annotations = mask_comments(text, annotations_only=True) + for name in names: + matches = list(re.finditer(r"\bfn\s+" + re.escape(name) + r"\b", rust)) + if len(matches) != 1: + raise ValueError(f"expected exactly one body for {name} in {path}") + begin = matches[0].end() + nesting = 0 + end = begin + while end < len(rust): + character = rust[end] + if character in "([": + nesting += 1 + elif character in ")]": + nesting -= 1 + elif nesting == 0 and character in "{;": + break + end += 1 + if end == len(rust) or rust[end] != "{": + raise ValueError(f"missing implementation for {name} in {path}") + clauses = annotations[begin:end] + for clause in ("req", "ens", "on_unwind_ens"): + if not re.search(r"\b" + clause + r"\s", clauses): + raise ValueError(f"missing {clause} for {name} in {path}") + + +def check(package=PACKAGE, repo=None, generate=False): + repo = package.parents[3] if repo is None else repo + manifest = json.loads(read_file(package / "source-map.json")) + if manifest.get("version") != 1 or len(manifest.get("sources", [])) != 2: + raise ValueError("unexpected source manifest") + for entry in manifest["sources"]: + snapshot = read_file(inside(package, entry["snapshot"])) + if hashlib.sha256(snapshot).hexdigest() != entry["sha256"]: + raise ValueError(f"snapshot hash changed: {entry['snapshot']}") + if snapshot != read_file(inside(repo, entry["upstream"])): + raise ValueError(f"std source differs from proof snapshot: {entry['upstream']}") + expected = project(snapshot, entry["ranges"]) + original = inside(package, entry["projection"]) + if generate: + original.parent.mkdir(parents=True, exist_ok=True) + original.write_bytes(expected) + elif read_file(original) != expected: + raise ValueError(f"original projection differs from selected std source: {original}") + if not generate: + check_contracts(package / "verified" / original.name, entry["contracts"]) + if not generate: + original_root = read_file(package / "original/lib.rs") + if original_root != read_file(package / "verified/lib.rs"): + raise ValueError("original and verified crate roots must match") + return len(manifest["sources"]) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--generate-original", action="store_true", + help="regenerate projections from unchanged, hash-checked snapshots") + args = parser.parse_args() + try: + count = check(generate=args.generate_original) + except (OSError, UnicodeError, ValueError, KeyError, TypeError) as error: + print(f"source check failed: {error}", file=sys.stderr) + return 1 + action = "generated" if args.generate_original else "checked" + print(f"{action} {count} source projections; no compiler or verifier was invoked") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/verifast-proofs/core/iter/adapters/original/lib.rs b/verifast-proofs/core/iter/adapters/original/lib.rs new file mode 100644 index 0000000000000..506672c09b373 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/original/lib.rs @@ -0,0 +1,15 @@ +#![no_std] +#![crate_type = "lib"] +#![allow(dead_code, unused_imports, internal_features)] +#![feature(cast_maybe_uninit, core_intrinsics, staged_api, stmt_expr_attributes)] +#![stable(feature = "rust1", since = "1.0.0")] + +extern crate core as std; + +#[stable(feature = "rust1", since = "1.0.0")] +pub use std::{fmt, intrinsics, mem, num, ptr}; + +#[path = "../array_layout.rs"] +mod array_layout; +mod map_windows; +mod step_by; diff --git a/verifast-proofs/core/iter/adapters/original/map_windows.rs b/verifast-proofs/core/iter/adapters/original/map_windows.rs new file mode 100644 index 0000000000000..57d96be3cb0cc --- /dev/null +++ b/verifast-proofs/core/iter/adapters/original/map_windows.rs @@ -0,0 +1,116 @@ +// Source projection checked by check_sources.py. Do not edit manually. + +use crate::mem::MaybeUninit; + +use crate::{fmt, ptr}; + +struct Buffer { + // Invariant: `self.buffer[self.start..self.start + N]` is initialized, + // with all other elements being uninitialized. This also + // implies that `self.start <= N`. + buffer: [[MaybeUninit; N]; 2], + start: usize, +} + +impl Buffer { + + #[inline] + fn buffer_ptr(&self) -> *const MaybeUninit { + self.buffer.as_ptr().cast() + } + + #[inline] + fn buffer_mut_ptr(&mut self) -> *mut MaybeUninit { + self.buffer.as_mut_ptr().cast() + } + + #[inline] + fn as_array_ref(&self) -> &[T; N] { + debug_assert!(self.start + N <= 2 * N); + + // SAFETY: our invariant guarantees these elements are initialized. + unsafe { &*self.buffer_ptr().add(self.start).cast() } + } + + #[inline] + fn as_uninit_array_mut(&mut self) -> &mut MaybeUninit<[T; N]> { + debug_assert!(self.start + N <= 2 * N); + + // SAFETY: our invariant guarantees these elements are in bounds. + unsafe { &mut *self.buffer_mut_ptr().add(self.start).cast() } + } + + /// Pushes a new item `next` to the back, and pops the front-most one. + /// + /// All the elements will be shifted to the front end when pushing reaches + /// the back end. + fn push(&mut self, next: T) { + let buffer_mut_ptr = self.buffer_mut_ptr(); + debug_assert!(self.start + N <= 2 * N); + + let to_drop = if self.start == N { + // We have reached the end of our buffer and have to copy + // everything to the start. Example layout for N = 3. + // + // 0 1 2 3 4 5 0 1 2 3 4 5 + // ┌───┬───┬───┬───┬───┬───┐ ┌───┬───┬───┬───┬───┬───┐ + // │ - │ - │ - │ a │ b │ c │ -> │ b │ c │ n │ - │ - │ - │ + // └───┴───┴───┴───┴───┴───┘ └───┴───┴───┴───┴───┴───┘ + // ↑ ↑ + // start start + + // SAFETY: the two pointers are valid for reads/writes of N -1 + // elements because our array's size is semantically 2 * N. The + // regions also don't overlap for the same reason. + // + // We leave the old elements in place. As soon as `start` is set + // to 0, we treat them as uninitialized and treat their copies + // as initialized. + let to_drop = unsafe { + ptr::copy_nonoverlapping(buffer_mut_ptr.add(self.start + 1), buffer_mut_ptr, N - 1); + (*buffer_mut_ptr.add(N - 1)).write(next); + buffer_mut_ptr.add(self.start) + }; + self.start = 0; + to_drop + } else { + // SAFETY: `self.start` is < N as guaranteed by the invariant + // plus the check above. Even if the drop at the end panics, + // the invariant is upheld. + // + // Example layout for N = 3: + // + // 0 1 2 3 4 5 0 1 2 3 4 5 + // ┌───┬───┬───┬───┬───┬───┐ ┌───┬───┬───┬───┬───┬───┐ + // │ - │ a │ b │ c │ - │ - │ -> │ - │ - │ b │ c │ n │ - │ + // └───┴───┴───┴───┴───┴───┘ └───┴───┴───┴───┴───┴───┘ + // ↑ ↑ + // start start + // + let to_drop = unsafe { + (*buffer_mut_ptr.add(self.start + N)).write(next); + buffer_mut_ptr.add(self.start) + }; + self.start += 1; + to_drop + }; + + // SAFETY: the index is valid and this is element `a` in the + // diagram above and has not been dropped yet. + unsafe { ptr::drop_in_place(to_drop.cast_init()) }; + } +} + +impl Drop for Buffer { + fn drop(&mut self) { + // SAFETY: our invariant guarantees that N elements starting from + // `self.start` are initialized. We drop them here. + unsafe { + let initialized_part: *mut [T] = crate::ptr::slice_from_raw_parts_mut( + self.buffer_mut_ptr().add(self.start).cast(), + N, + ); + ptr::drop_in_place(initialized_part); + } + } +} diff --git a/verifast-proofs/core/iter/adapters/original/step_by.rs b/verifast-proofs/core/iter/adapters/original/step_by.rs new file mode 100644 index 0000000000000..17e69e16e4040 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/original/step_by.rs @@ -0,0 +1,36 @@ +// Source projection checked by check_sources.py. Do not edit manually. + +use crate::intrinsics; + +use crate::num::NonZero; + +#[must_use = "iterators are lazy and do nothing unless consumed"] +#[stable(feature = "iterator_step_by", since = "1.28.0")] +#[derive(Clone, Debug)] +pub struct StepBy { + /// This field is guaranteed to be preprocessed by the specialized `SpecRangeSetup::setup` + /// in the constructor. + /// For most iterators that processing is a no-op, but for Range<{integer}> types it is lossy + /// which means the inner iterator cannot be returned to user code. + /// Additionally this type-dependent preprocessing means specialized implementations + /// cannot be used interchangeably. + iter: I, + /// This field is `step - 1`, aka the correct amount to pass to `nth` when iterating. + /// It MUST NOT be `usize::MAX`, as `unsafe` code depends on being able to add one + /// without the risk of overflow. (This is important so that length calculations + /// don't need to check for division-by-zero, for example.) + step_minus_one: usize, + first_take: bool, +} + +impl StepBy { + + /// The `step` that was originally passed to `Iterator::step_by(step)`, + /// aka `self.step_minus_one + 1`. + #[inline] + fn original_step(&self) -> NonZero { + // SAFETY: By type invariant, `step_minus_one` cannot be `MAX`, which + // means the addition cannot overflow and the result cannot be zero. + unsafe { NonZero::new_unchecked(intrinsics::unchecked_add(self.step_minus_one, 1)) } + } +} diff --git a/verifast-proofs/core/iter/adapters/source-map.json b/verifast-proofs/core/iter/adapters/source-map.json new file mode 100644 index 0000000000000..596a67ec7a20d --- /dev/null +++ b/verifast-proofs/core/iter/adapters/source-map.json @@ -0,0 +1,21 @@ +{ + "version": 1, + "sources": [ + { + "upstream": "library/core/src/iter/adapters/map_windows.rs", + "snapshot": "source/map_windows.rs", + "sha256": "f82419679445fa307ffc7d869f5e8e75578925a82ea51005ef7dddf46a8e1d61", + "projection": "original/map_windows.rs", + "ranges": [[2, 2], [4, 4], [41, 47], [108, 108], [116, 201], [224, 236]], + "contracts": ["buffer_ptr", "buffer_mut_ptr", "as_array_ref", "as_uninit_array_mut", "push", "drop"] + }, + { + "upstream": "library/core/src/iter/adapters/step_by.rs", + "snapshot": "source/step_by.rs", + "sha256": "5de19bd52fe39caf378b1d64e72d14220c67dab3f79ff485ade9b559be337e49", + "projection": "original/step_by.rs", + "ranges": [[1, 1], [5, 5], [16, 33], [42, 42], [50, 58]], + "contracts": ["original_step"] + } + ] +} diff --git a/verifast-proofs/core/iter/adapters/source/map_windows.rs b/verifast-proofs/core/iter/adapters/source/map_windows.rs new file mode 100644 index 0000000000000..8451a02ea9da0 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/source/map_windows.rs @@ -0,0 +1,392 @@ +use crate::iter::FusedIterator; +use crate::mem::MaybeUninit; +use crate::ub_checks::Invariant; +use crate::{fmt, ptr}; + +/// An iterator over the mapped windows of another iterator. +/// +/// This `struct` is created by the [`Iterator::map_windows`]. See its +/// documentation for more information. +#[must_use = "iterators are lazy and do nothing unless consumed"] +#[unstable(feature = "iter_map_windows", issue = "87155")] +pub struct MapWindows { + f: F, + inner: MapWindowsInner, +} + +struct MapWindowsInner { + // We fuse the inner iterator because there shouldn't be "holes" in + // the sliding window. Once the iterator returns a `None`, we make + // our `MapWindows` iterator return `None` forever. + iter: Option, + // Since iterators are assumed lazy, i.e. it only yields an item when + // `Iterator::next()` is called, and `MapWindows` is not an exception. + // + // Before the first iteration, we keep the buffer `None`. When the user + // first call `next` or other methods that makes the iterator advance, + // we collect the first `N` items yielded from the inner iterator and + // put it into the buffer. + // + // When the inner iterator has returned a `None` (i.e. fused), we take + // away this `buffer` and leave it `None` to reclaim its resources. + // + // FIXME: should we shrink the size of `buffer` using niche optimization? + buffer: Option>, +} + +// `Buffer` uses two times of space to reduce moves among the iterations. +// `Buffer` is semantically `[MaybeUninit; 2 * N]`. However, due +// to limitations of const generics, we use this different type. Note that +// it has the same underlying memory layout. +struct Buffer { + // Invariant: `self.buffer[self.start..self.start + N]` is initialized, + // with all other elements being uninitialized. This also + // implies that `self.start <= N`. + buffer: [[MaybeUninit; N]; 2], + start: usize, +} + +impl MapWindows { + pub(in crate::iter) fn new(iter: I, f: F) -> Self { + assert!(N != 0, "array in `Iterator::map_windows` must contain more than 0 elements"); + + // Only ZST arrays' length can be so large. + if size_of::() == 0 { + assert!( + N.checked_mul(2).is_some(), + "array size of `Iterator::map_windows` is too large" + ); + } + + Self { inner: MapWindowsInner::new(iter), f } + } +} + +impl MapWindowsInner { + #[inline] + fn new(iter: I) -> Self { + Self { iter: Some(iter), buffer: None } + } + + fn next_window(&mut self) -> Option<&[I::Item; N]> { + let iter = self.iter.as_mut()?; + match self.buffer { + // It is the first time to advance. We collect + // the first `N` items from `self.iter` to initialize `self.buffer`. + None => self.buffer = Buffer::try_from_iter(iter), + Some(ref mut buffer) => match iter.next() { + None => { + // Fuse the inner iterator since it yields a `None`. + self.iter.take(); + self.buffer.take(); + } + // Advance the iterator. We first call `next` before changing our buffer + // at all. This means that if `next` panics, our invariant is upheld and + // our `Drop` impl drops the correct elements. + Some(item) => buffer.push(item), + }, + } + self.buffer.as_ref().map(Buffer::as_array_ref) + } + + fn size_hint(&self) -> (usize, Option) { + let Some(ref iter) = self.iter else { return (0, Some(0)) }; + let (lo, hi) = iter.size_hint(); + if self.buffer.is_some() { + // If the first `N` items are already yielded by the inner iterator, + // the size hint is then equal to the that of the inner iterator's. + (lo, hi) + } else { + // If the first `N` items are not yet yielded by the inner iterator, + // the first `N` elements should be counted as one window, so both bounds + // should subtract `N - 1`. + (lo.saturating_sub(N - 1), hi.map(|hi| hi.saturating_sub(N - 1))) + } + } +} + +impl Buffer { + fn try_from_iter(iter: &mut impl Iterator) -> Option { + let first_half = crate::array::iter_next_chunk(iter).ok()?; + let buffer = + [MaybeUninit::new(first_half).transpose(), [const { MaybeUninit::uninit() }; N]]; + Some(Self { buffer, start: 0 }) + } + + #[inline] + fn buffer_ptr(&self) -> *const MaybeUninit { + self.buffer.as_ptr().cast() + } + + #[inline] + fn buffer_mut_ptr(&mut self) -> *mut MaybeUninit { + self.buffer.as_mut_ptr().cast() + } + + #[inline] + fn as_array_ref(&self) -> &[T; N] { + debug_assert!(self.start + N <= 2 * N); + + // SAFETY: our invariant guarantees these elements are initialized. + unsafe { &*self.buffer_ptr().add(self.start).cast() } + } + + #[inline] + fn as_uninit_array_mut(&mut self) -> &mut MaybeUninit<[T; N]> { + debug_assert!(self.start + N <= 2 * N); + + // SAFETY: our invariant guarantees these elements are in bounds. + unsafe { &mut *self.buffer_mut_ptr().add(self.start).cast() } + } + + /// Pushes a new item `next` to the back, and pops the front-most one. + /// + /// All the elements will be shifted to the front end when pushing reaches + /// the back end. + fn push(&mut self, next: T) { + let buffer_mut_ptr = self.buffer_mut_ptr(); + debug_assert!(self.start + N <= 2 * N); + + let to_drop = if self.start == N { + // We have reached the end of our buffer and have to copy + // everything to the start. Example layout for N = 3. + // + // 0 1 2 3 4 5 0 1 2 3 4 5 + // ┌───┬───┬───┬───┬───┬───┐ ┌───┬───┬───┬───┬───┬───┐ + // │ - │ - │ - │ a │ b │ c │ -> │ b │ c │ n │ - │ - │ - │ + // └───┴───┴───┴───┴───┴───┘ └───┴───┴───┴───┴───┴───┘ + // ↑ ↑ + // start start + + // SAFETY: the two pointers are valid for reads/writes of N -1 + // elements because our array's size is semantically 2 * N. The + // regions also don't overlap for the same reason. + // + // We leave the old elements in place. As soon as `start` is set + // to 0, we treat them as uninitialized and treat their copies + // as initialized. + let to_drop = unsafe { + ptr::copy_nonoverlapping(buffer_mut_ptr.add(self.start + 1), buffer_mut_ptr, N - 1); + (*buffer_mut_ptr.add(N - 1)).write(next); + buffer_mut_ptr.add(self.start) + }; + self.start = 0; + to_drop + } else { + // SAFETY: `self.start` is < N as guaranteed by the invariant + // plus the check above. Even if the drop at the end panics, + // the invariant is upheld. + // + // Example layout for N = 3: + // + // 0 1 2 3 4 5 0 1 2 3 4 5 + // ┌───┬───┬───┬───┬───┬───┐ ┌───┬───┬───┬───┬───┬───┐ + // │ - │ a │ b │ c │ - │ - │ -> │ - │ - │ b │ c │ n │ - │ + // └───┴───┴───┴───┴───┴───┘ └───┴───┴───┴───┴───┴───┘ + // ↑ ↑ + // start start + // + let to_drop = unsafe { + (*buffer_mut_ptr.add(self.start + N)).write(next); + buffer_mut_ptr.add(self.start) + }; + self.start += 1; + to_drop + }; + + // SAFETY: the index is valid and this is element `a` in the + // diagram above and has not been dropped yet. + unsafe { ptr::drop_in_place(to_drop.cast_init()) }; + } +} + +impl Clone for Buffer { + fn clone(&self) -> Self { + let mut buffer = Buffer { + buffer: [[const { MaybeUninit::uninit() }; N], [const { MaybeUninit::uninit() }; N]], + start: self.start, + }; + buffer.as_uninit_array_mut().write(self.as_array_ref().clone()); + buffer + } +} + +impl Clone for MapWindowsInner +where + I: Iterator + Clone, + I::Item: Clone, +{ + fn clone(&self) -> Self { + Self { iter: self.iter.clone(), buffer: self.buffer.clone() } + } +} + +impl Drop for Buffer { + fn drop(&mut self) { + // SAFETY: our invariant guarantees that N elements starting from + // `self.start` are initialized. We drop them here. + unsafe { + let initialized_part: *mut [T] = crate::ptr::slice_from_raw_parts_mut( + self.buffer_mut_ptr().add(self.start).cast(), + N, + ); + ptr::drop_in_place(initialized_part); + } + } +} + +#[unstable(feature = "iter_map_windows", issue = "87155")] +impl Iterator for MapWindows +where + I: Iterator, + F: FnMut(&[I::Item; N]) -> R, +{ + type Item = R; + + fn next(&mut self) -> Option { + let window = self.inner.next_window()?; + let out = (self.f)(window); + Some(out) + } + + fn size_hint(&self) -> (usize, Option) { + self.inner.size_hint() + } +} + +// Note that even if the inner iterator not fused, the `MapWindows` is still fused, +// because we don't allow "holes" in the mapping window. +#[unstable(feature = "iter_map_windows", issue = "87155")] +impl FusedIterator for MapWindows +where + I: Iterator, + F: FnMut(&[I::Item; N]) -> R, +{ +} + +#[unstable(feature = "iter_map_windows", issue = "87155")] +impl ExactSizeIterator for MapWindows +where + I: ExactSizeIterator, + F: FnMut(&[I::Item; N]) -> R, +{ +} + +#[unstable(feature = "iter_map_windows", issue = "87155")] +impl fmt::Debug for MapWindows { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("MapWindows").field("iter", &self.inner.iter).finish() + } +} + +#[unstable(feature = "iter_map_windows", issue = "87155")] +impl Clone for MapWindows +where + I: Iterator + Clone, + F: Clone, + I::Item: Clone, +{ + fn clone(&self) -> Self { + Self { f: self.f.clone(), inner: self.inner.clone() } + } +} + +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for Buffer { + fn is_safe(&self) -> bool { + self.start + N <= 2 * N + } +} + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + // Build a `Buffer` in a valid state: `start` in `[0, N]` (the type + // invariant) and the live window `[start, start + N)` fully initialized with + // arbitrary values; the remaining `N` slots stay uninitialized, exactly as + // the real buffer maintains them. + fn any_buffer() -> Buffer { + let start = kani::any_where(|s: &usize| *s <= N); + let mut buffer = Buffer { + buffer: [[const { MaybeUninit::uninit() }; N], [const { MaybeUninit::uninit() }; N]], + start, + }; + let items: [T; N] = kani::any(); + let base = buffer.buffer_mut_ptr(); + items.into_iter().enumerate().for_each(|(i, item)| { + // SAFETY: `start + i < start + N <= 2 * N`, in bounds of the `2 * N` buffer. + unsafe { (*base.add(start + i)).write(item) }; + }); + buffer + } + + // `as_array_ref` / `as_uninit_array_mut` reinterpret the live window as an + // array reference; `push` rotates the window (and wraps + compacts when + // `start == N`); `drop` drops the live window. Each must respect the + // initialized-window invariant and stay in bounds of the `2 * N` storage. + macro_rules! check_buffer { + ($module:ident, $elem_ty:ty, $n:expr) => { + mod $module { + use super::*; + const N: usize = $n; + + #[kani::proof] + fn check_as_array_ref() { + let buf = any_buffer::<$elem_ty, N>(); + let _ = buf.as_array_ref(); + kani::assert(buf.is_safe(), "buffer invariant holds"); + } + + #[kani::proof] + fn check_as_uninit_array_mut() { + let mut buf = any_buffer::<$elem_ty, N>(); + let _ = buf.as_uninit_array_mut(); + kani::assert(buf.is_safe(), "buffer invariant holds"); + } + + #[kani::proof] + fn check_push() { + let mut buf = any_buffer::<$elem_ty, N>(); + buf.push(kani::any()); + kani::assert(buf.is_safe(), "buffer invariant holds after push"); + } + + #[kani::proof] + fn check_drop() { + let buf = any_buffer::<$elem_ty, N>(); + drop(buf); + } + } + }; + } + check_buffer!(verify_map_windows_unit, (), 3); + check_buffer!(verify_map_windows_u8, u8, 3); + check_buffer!(verify_map_windows_char, char, 2); + check_buffer!(verify_map_windows_tup, (char, u8), 2); + + // A drop-requiring element type: `needs_drop::()` is true, so + // `push`'s `drop_in_place` and the `Buffer` `Drop` impl execute real drop + // glue instead of compiling to no-ops, and the destructor reads the + // payload, so the dropped element must be an in-bounds, live slot. Kani + // models a panic as a verification failure and has no unwinding, so the + // panic-during-drop path itself is not expressible in a passing harness; + // the coverage this type adds is the non-trivial drop-glue code path. + struct DropToken(u8); + + impl Drop for DropToken { + fn drop(&mut self) { + let _ = crate::hint::black_box(self.0); + } + } + + impl kani::Arbitrary for DropToken { + fn any() -> Self { + DropToken(kani::any()) + } + } + + check_buffer!(verify_map_windows_drop, DropToken, 2); +} diff --git a/verifast-proofs/core/iter/adapters/source/step_by.rs b/verifast-proofs/core/iter/adapters/source/step_by.rs new file mode 100644 index 0000000000000..1ac22d698a43e --- /dev/null +++ b/verifast-proofs/core/iter/adapters/source/step_by.rs @@ -0,0 +1,634 @@ +use crate::intrinsics; +use crate::iter::{TrustedLen, TrustedRandomAccess, from_fn}; +#[cfg(kani)] +use crate::kani; +use crate::num::NonZero; +use crate::ops::{Range, Try}; +use crate::ub_checks::Invariant; + +/// An iterator for stepping iterators by a custom amount. +/// +/// This `struct` is created by the [`step_by`] method on [`Iterator`]. See +/// its documentation for more. +/// +/// [`step_by`]: Iterator::step_by +/// [`Iterator`]: trait.Iterator.html +#[must_use = "iterators are lazy and do nothing unless consumed"] +#[stable(feature = "iterator_step_by", since = "1.28.0")] +#[derive(Clone, Debug)] +pub struct StepBy { + /// This field is guaranteed to be preprocessed by the specialized `SpecRangeSetup::setup` + /// in the constructor. + /// For most iterators that processing is a no-op, but for Range<{integer}> types it is lossy + /// which means the inner iterator cannot be returned to user code. + /// Additionally this type-dependent preprocessing means specialized implementations + /// cannot be used interchangeably. + iter: I, + /// This field is `step - 1`, aka the correct amount to pass to `nth` when iterating. + /// It MUST NOT be `usize::MAX`, as `unsafe` code depends on being able to add one + /// without the risk of overflow. (This is important so that length calculations + /// don't need to check for division-by-zero, for example.) + step_minus_one: usize, + first_take: bool, +} + +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for StepBy { + fn is_safe(&self) -> bool { + self.step_minus_one < usize::MAX + } +} + +impl StepBy { + #[inline] + pub(in crate::iter) fn new(iter: I, step: usize) -> StepBy { + assert!(step != 0); + let iter = >::setup(iter, step); + StepBy { iter, step_minus_one: step - 1, first_take: true } + } + + /// The `step` that was originally passed to `Iterator::step_by(step)`, + /// aka `self.step_minus_one + 1`. + #[inline] + fn original_step(&self) -> NonZero { + // SAFETY: By type invariant, `step_minus_one` cannot be `MAX`, which + // means the addition cannot overflow and the result cannot be zero. + unsafe { NonZero::new_unchecked(intrinsics::unchecked_add(self.step_minus_one, 1)) } + } +} + +#[stable(feature = "iterator_step_by", since = "1.28.0")] +impl Iterator for StepBy +where + I: Iterator, +{ + type Item = I::Item; + + #[inline] + fn next(&mut self) -> Option { + self.spec_next() + } + + #[inline] + fn size_hint(&self) -> (usize, Option) { + self.spec_size_hint() + } + + #[inline] + fn nth(&mut self, n: usize) -> Option { + self.spec_nth(n) + } + + fn try_fold(&mut self, acc: Acc, f: F) -> R + where + F: FnMut(Acc, Self::Item) -> R, + R: Try, + { + self.spec_try_fold(acc, f) + } + + #[inline] + fn fold(self, acc: Acc, f: F) -> Acc + where + F: FnMut(Acc, Self::Item) -> Acc, + { + self.spec_fold(acc, f) + } +} + +impl StepBy +where + I: ExactSizeIterator, +{ + // The zero-based index starting from the end of the iterator of the + // last element. Used in the `DoubleEndedIterator` implementation. + fn next_back_index(&self) -> usize { + let rem = self.iter.len() % self.original_step(); + if self.first_take { if rem == 0 { self.step_minus_one } else { rem - 1 } } else { rem } + } +} + +#[stable(feature = "double_ended_step_by_iterator", since = "1.38.0")] +impl DoubleEndedIterator for StepBy +where + I: DoubleEndedIterator + ExactSizeIterator, +{ + #[inline] + fn next_back(&mut self) -> Option { + self.spec_next_back() + } + + #[inline] + fn nth_back(&mut self, n: usize) -> Option { + self.spec_nth_back(n) + } + + fn try_rfold(&mut self, init: Acc, f: F) -> R + where + F: FnMut(Acc, Self::Item) -> R, + R: Try, + { + self.spec_try_rfold(init, f) + } + + #[inline] + fn rfold(self, init: Acc, f: F) -> Acc + where + Self: Sized, + F: FnMut(Acc, Self::Item) -> Acc, + { + self.spec_rfold(init, f) + } +} + +// StepBy can only make the iterator shorter, so the len will still fit. +#[stable(feature = "iterator_step_by", since = "1.28.0")] +impl ExactSizeIterator for StepBy where I: ExactSizeIterator {} + +// SAFETY: This adapter is shortening. TrustedLen requires the upper bound to be calculated correctly. +// These requirements can only be satisfied when the upper bound of the inner iterator's upper +// bound is never `None`. I: TrustedRandomAccess happens to provide this guarantee while +// I: TrustedLen would not. +// This also covers the Range specializations since the ranges also implement TRA +#[unstable(feature = "trusted_len", issue = "37572")] +unsafe impl TrustedLen for StepBy where I: Iterator + TrustedRandomAccess {} + +trait SpecRangeSetup { + fn setup(inner: T, step: usize) -> T; +} + +impl SpecRangeSetup for T { + #[inline] + default fn setup(inner: T, _step: usize) -> T { + inner + } +} + +/// Specialization trait to optimize `StepBy>` iteration. +/// +/// # Safety +/// +/// Technically this is safe to implement (look ma, no unsafe!), but in reality +/// a lot of unsafe code relies on ranges over integers being correct. +/// +/// For correctness *all* public StepBy methods must be specialized +/// because `setup` drastically alters the meaning of the struct fields so that mixing +/// different implementations would lead to incorrect results. +unsafe trait StepByImpl { + type Item; + + fn spec_next(&mut self) -> Option; + + fn spec_size_hint(&self) -> (usize, Option); + + fn spec_nth(&mut self, n: usize) -> Option; + + fn spec_try_fold(&mut self, acc: Acc, f: F) -> R + where + F: FnMut(Acc, Self::Item) -> R, + R: Try; + + fn spec_fold(self, acc: Acc, f: F) -> Acc + where + F: FnMut(Acc, Self::Item) -> Acc; +} + +/// Specialization trait for double-ended iteration. +/// +/// See also: `StepByImpl` +/// +/// # Safety +/// +/// The specializations must be implemented together with `StepByImpl` +/// where applicable. I.e. if `StepBy` does support backwards iteration +/// for a given iterator and that is specialized for forward iteration then +/// it must also be specialized for backwards iteration. +unsafe trait StepByBackImpl { + type Item; + + fn spec_next_back(&mut self) -> Option + where + I: DoubleEndedIterator + ExactSizeIterator; + + fn spec_nth_back(&mut self, n: usize) -> Option + where + I: DoubleEndedIterator + ExactSizeIterator; + + fn spec_try_rfold(&mut self, init: Acc, f: F) -> R + where + I: DoubleEndedIterator + ExactSizeIterator, + F: FnMut(Acc, Self::Item) -> R, + R: Try; + + fn spec_rfold(self, init: Acc, f: F) -> Acc + where + I: DoubleEndedIterator + ExactSizeIterator, + F: FnMut(Acc, Self::Item) -> Acc; +} + +unsafe impl StepByImpl for StepBy { + type Item = I::Item; + + #[inline] + default fn spec_next(&mut self) -> Option { + let step_size = if self.first_take { 0 } else { self.step_minus_one }; + self.first_take = false; + self.iter.nth(step_size) + } + + #[inline] + default fn spec_size_hint(&self) -> (usize, Option) { + #[inline] + fn first_size(step: NonZero) -> impl Fn(usize) -> usize { + move |n| if n == 0 { 0 } else { 1 + (n - 1) / step } + } + + #[inline] + fn other_size(step: NonZero) -> impl Fn(usize) -> usize { + move |n| n / step + } + + let (low, high) = self.iter.size_hint(); + + if self.first_take { + let f = first_size(self.original_step()); + (f(low), high.map(f)) + } else { + let f = other_size(self.original_step()); + (f(low), high.map(f)) + } + } + + #[inline] + default fn spec_nth(&mut self, mut n: usize) -> Option { + if self.first_take { + self.first_take = false; + let first = self.iter.next(); + if n == 0 { + return first; + } + n -= 1; + } + // n and self.step_minus_one are indices, we need to add 1 to get the amount of elements + // When calling `.nth`, we need to subtract 1 again to convert back to an index + let mut step = self.original_step().get(); + // n + 1 could overflow + // thus, if n is usize::MAX, instead of adding one, we call .nth(step) + if n == usize::MAX { + self.iter.nth(step - 1); + } else { + n += 1; + } + + // overflow handling + loop { + let mul = n.checked_mul(step); + { + if intrinsics::likely(mul.is_some()) { + return self.iter.nth(mul.unwrap() - 1); + } + } + let div_n = usize::MAX / n; + let div_step = usize::MAX / step; + let nth_n = div_n * n; + let nth_step = div_step * step; + let nth = if nth_n > nth_step { + step -= div_n; + nth_n + } else { + n -= div_step; + nth_step + }; + self.iter.nth(nth - 1); + } + } + + default fn spec_try_fold(&mut self, mut acc: Acc, mut f: F) -> R + where + F: FnMut(Acc, Self::Item) -> R, + R: Try, + { + #[inline] + fn nth( + iter: &mut I, + step_minus_one: usize, + ) -> impl FnMut() -> Option + '_ { + move || iter.nth(step_minus_one) + } + + if self.first_take { + self.first_take = false; + match self.iter.next() { + None => return try { acc }, + Some(x) => acc = f(acc, x)?, + } + } + from_fn(nth(&mut self.iter, self.step_minus_one)).try_fold(acc, f) + } + + default fn spec_fold(mut self, mut acc: Acc, mut f: F) -> Acc + where + F: FnMut(Acc, Self::Item) -> Acc, + { + #[inline] + fn nth( + iter: &mut I, + step_minus_one: usize, + ) -> impl FnMut() -> Option + '_ { + move || iter.nth(step_minus_one) + } + + if self.first_take { + self.first_take = false; + match self.iter.next() { + None => return acc, + Some(x) => acc = f(acc, x), + } + } + from_fn(nth(&mut self.iter, self.step_minus_one)).fold(acc, f) + } +} + +unsafe impl StepByBackImpl for StepBy { + type Item = I::Item; + + #[inline] + default fn spec_next_back(&mut self) -> Option { + self.iter.nth_back(self.next_back_index()) + } + + #[inline] + default fn spec_nth_back(&mut self, n: usize) -> Option { + // `self.iter.nth_back(usize::MAX)` does the right thing here when `n` + // is out of bounds because the length of `self.iter` does not exceed + // `usize::MAX` (because `I: ExactSizeIterator`) and `nth_back` is + // zero-indexed + let n = n.saturating_mul(self.original_step().get()).saturating_add(self.next_back_index()); + self.iter.nth_back(n) + } + + default fn spec_try_rfold(&mut self, init: Acc, mut f: F) -> R + where + F: FnMut(Acc, Self::Item) -> R, + R: Try, + { + #[inline] + fn nth_back( + iter: &mut I, + step_minus_one: usize, + ) -> impl FnMut() -> Option + '_ { + move || iter.nth_back(step_minus_one) + } + + match self.next_back() { + None => try { init }, + Some(x) => { + let acc = f(init, x)?; + from_fn(nth_back(&mut self.iter, self.step_minus_one)).try_fold(acc, f) + } + } + } + + #[inline] + default fn spec_rfold(mut self, init: Acc, mut f: F) -> Acc + where + Self: Sized, + F: FnMut(Acc, I::Item) -> Acc, + { + #[inline] + fn nth_back( + iter: &mut I, + step_minus_one: usize, + ) -> impl FnMut() -> Option + '_ { + move || iter.nth_back(step_minus_one) + } + + match self.next_back() { + None => init, + Some(x) => { + let acc = f(init, x); + from_fn(nth_back(&mut self.iter, self.step_minus_one)).fold(acc, f) + } + } + } +} + +/// For these implementations, `SpecRangeSetup` calculates the number +/// of iterations that will be needed and stores that in `iter.end`. +/// +/// The various iterator implementations then rely on that to not need +/// overflow checking, letting loops just be counted instead. +/// +/// These only work for unsigned types, and will need to be reworked +/// if you want to use it to specialize on signed types. +/// +/// Currently these are only implemented for integers up to `usize` due to +/// correctness issues around `ExactSizeIterator` impls on 16bit platforms. +/// And since `ExactSizeIterator` is a prerequisite for backwards iteration +/// and we must consistently specialize backwards and forwards iteration +/// that makes the situation complicated enough that it's not covered +/// for now. +macro_rules! spec_int_ranges { + ($($t:ty)*) => ($( + + const _: () = assert!(usize::BITS >= <$t>::BITS); + + impl SpecRangeSetup> for Range<$t> { + #[inline] + fn setup(mut r: Range<$t>, step: usize) -> Range<$t> { + let inner_len = r.size_hint().0; + // If step exceeds $t::MAX, then the count will be at most 1 and + // thus always fit into $t. + let yield_count = inner_len.div_ceil(step); + // Turn the range end into an iteration counter + r.end = yield_count as $t; + r + } + } + + unsafe impl StepByImpl> for StepBy> { + #[inline] + fn spec_next(&mut self) -> Option<$t> { + // if a step size larger than the type has been specified fall back to + // t::MAX, in which case remaining will be at most 1. + let step = <$t>::try_from(self.original_step().get()).unwrap_or(<$t>::MAX); + let remaining = self.iter.end; + if remaining > 0 { + let val = self.iter.start; + // this can only overflow during the last step, after which the value + // will not be used + self.iter.start = val.wrapping_add(step); + self.iter.end = remaining - 1; + Some(val) + } else { + None + } + } + + #[inline] + fn spec_size_hint(&self) -> (usize, Option) { + let remaining = self.iter.end as usize; + (remaining, Some(remaining)) + } + + // The methods below are all copied from the Iterator trait default impls. + // We have to repeat them here so that the specialization overrides the StepByImpl defaults + + #[inline] + fn spec_nth(&mut self, n: usize) -> Option { + self.advance_by(n).ok()?; + self.next() + } + + #[inline] + fn spec_try_fold(&mut self, init: Acc, mut f: F) -> R + where + F: FnMut(Acc, Self::Item) -> R, + R: Try + { + let mut accum = init; + while let Some(x) = self.next() { + accum = f(accum, x)?; + } + try { accum } + } + + #[inline] + fn spec_fold(self, init: Acc, mut f: F) -> Acc + where + F: FnMut(Acc, Self::Item) -> Acc + { + // if a step size larger than the type has been specified fall back to + // t::MAX, in which case remaining will be at most 1. + let step = <$t>::try_from(self.original_step().get()).unwrap_or(<$t>::MAX); + let remaining = self.iter.end; + let mut acc = init; + let mut val = self.iter.start; + for _ in 0..remaining { + acc = f(acc, val); + // this can only overflow during the last step, after which the value + // will no longer be used + val = val.wrapping_add(step); + } + acc + } + } + )*) +} + +macro_rules! spec_int_ranges_r { + ($($t:ty)*) => ($( + const _: () = assert!(usize::BITS >= <$t>::BITS); + + unsafe impl StepByBackImpl> for StepBy> { + + #[inline] + fn spec_next_back(&mut self) -> Option { + let step = self.original_step().get() as $t; + let remaining = self.iter.end; + if remaining > 0 { + let start = self.iter.start; + self.iter.end = remaining - 1; + Some(start + step * (remaining - 1)) + } else { + None + } + } + + // The methods below are all copied from the Iterator trait default impls. + // We have to repeat them here so that the specialization overrides the StepByImplBack defaults + + #[inline] + fn spec_nth_back(&mut self, n: usize) -> Option { + if self.advance_back_by(n).is_err() { + return None; + } + self.next_back() + } + + #[inline] + fn spec_try_rfold(&mut self, init: Acc, mut f: F) -> R + where + F: FnMut(Acc, Self::Item) -> R, + R: Try + { + let mut accum = init; + while let Some(x) = self.next_back() { + accum = f(accum, x)?; + } + try { accum } + } + + #[inline] + fn spec_rfold(mut self, init: Acc, mut f: F) -> Acc + where + F: FnMut(Acc, Self::Item) -> Acc + { + let mut accum = init; + while let Some(x) = self.next_back() { + accum = f(accum, x); + } + accum + } + } + )*) +} + +#[cfg(target_pointer_width = "64")] +spec_int_ranges!(u8 u16 u32 u64 usize); +// DoubleEndedIterator requires ExactSizeIterator, which isn't implemented for Range +#[cfg(target_pointer_width = "64")] +spec_int_ranges_r!(u8 u16 u32 usize); + +#[cfg(target_pointer_width = "32")] +spec_int_ranges!(u8 u16 u32 usize); +#[cfg(target_pointer_width = "32")] +spec_int_ranges_r!(u8 u16 u32 usize); + +#[cfg(target_pointer_width = "16")] +spec_int_ranges!(u8 u16 usize); +#[cfg(target_pointer_width = "16")] +spec_int_ranges_r!(u8 u16 usize); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + fn any_slice(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::(|v| *v != 0) as *const T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts(ptr, 0) } + } + } + + // `original_step` reconstructs the configured step as `step_minus_one + 1` + // via `unchecked_add` and `NonZero::new_unchecked`. The type invariant + // (`step_minus_one < usize::MAX`) makes both operations sound; a valid + // `StepBy` is established by construction (`StepBy::new` requires `step != 0`). + macro_rules! check_original_step { + ($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 step = kani::any_where(|s: &usize| *s != 0); + let it = StepBy::new(any_slice(&array).iter(), step); + let result = it.original_step(); + kani::assert(result.get() == step, "original_step round-trips the configured step"); + } + }; + } + // `original_step` ignores the wrapped iterator, so a small backing array + // suffices; the proof is over the symbolic `step`, not the slice length. + check_original_step!(check_step_by_original_step_unit, (), 16); + check_original_step!(check_step_by_original_step_u8, u8, 16); + check_original_step!(check_step_by_original_step_char, char, 16); + check_original_step!(check_step_by_original_step_tup, (char, u8), 16); +} diff --git a/verifast-proofs/core/iter/adapters/test_sources.py b/verifast-proofs/core/iter/adapters/test_sources.py new file mode 100644 index 0000000000000..7c270009ef498 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/test_sources.py @@ -0,0 +1,95 @@ +#!/usr/bin/env python3 +"""Exercise stale-source and omitted-contract failures without a compiler.""" + +import importlib.util +import json +from pathlib import Path +import sys +import tempfile +import unittest + + +PACKAGE = Path(__file__).resolve().parent +sys.dont_write_bytecode = True +SPEC = importlib.util.spec_from_file_location("check_sources", PACKAGE / "check_sources.py") +CHECKER = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(CHECKER) + + +class SourceGateTests(unittest.TestCase): + def setUp(self): + self.temporary = tempfile.TemporaryDirectory(prefix="vrs602-source-check-") + self.addCleanup(self.temporary.cleanup) + self.repo = Path(self.temporary.name) + self.package = self.repo / "verifast-proofs/core/iter/adapters" + self.manifest = json.loads(CHECKER.read_file(PACKAGE / "source-map.json")) + paths = ["source-map.json", "original/lib.rs", "verified/lib.rs"] + for entry in self.manifest["sources"]: + paths.extend((entry["snapshot"], entry["projection"], + "verified/" + Path(entry["projection"]).name)) + upstream = self.repo / entry["upstream"] + upstream.parent.mkdir(parents=True, exist_ok=True) + upstream.write_bytes(CHECKER.read_file(PACKAGE / entry["snapshot"])) + for relative in paths: + destination = self.package / relative + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes(CHECKER.read_file(PACKAGE / relative)) + + def check(self): + return CHECKER.check(package=self.package, repo=self.repo) + + def alter(self, relative, before, after): + path = self.package / relative + text = path.read_text() + self.assertIn(before, text) + path.write_text(text.replace(before, after, 1)) + + def test_current_inputs_and_array_return_signatures(self): + self.assertEqual(self.check(), 2) + + def test_upstream_drift(self): + path = self.repo / self.manifest["sources"][0]["upstream"] + path.write_bytes(path.read_bytes() + b"\n") + with self.assertRaisesRegex(ValueError, "std source differs"): + self.check() + + def test_snapshot_drift(self): + path = self.package / self.manifest["sources"][0]["snapshot"] + path.write_bytes(path.read_bytes() + b"\n") + with self.assertRaisesRegex(ValueError, "snapshot hash changed"): + self.check() + + def test_projection_drift(self): + self.alter("original/step_by.rs", "self.step_minus_one, 1", "self.step_minus_one, 2") + with self.assertRaisesRegex(ValueError, "original projection differs"): + self.check() + + def test_ordinary_comment_does_not_count_as_contract(self): + self.alter("verified/step_by.rs", "//@ req", "// req") + with self.assertRaisesRegex(ValueError, "missing req for original_step"): + self.check() + + def test_missing_unwind_clause(self): + self.alter("verified/step_by.rs", "//@ on_unwind_ens false;", "") + with self.assertRaisesRegex(ValueError, "missing on_unwind_ens"): + self.check() + + def test_suppressed_method(self): + self.alter("verified/step_by.rs", " #[inline]", " #[cfg(any())]\n #[inline]") + with self.assertRaisesRegex(ValueError, "verification bypass"): + self.check() + + def test_assumption(self): + self.alter("verified/step_by.rs", "//@ on_unwind_ens false;", + "//@ on_unwind_ens false;\n //@ assume(false);") + with self.assertRaisesRegex(ValueError, "verification bypass"): + self.check() + + def test_changed_crate_root(self): + self.alter("verified/lib.rs", "mod step_by;", "") + with self.assertRaisesRegex(ValueError, "crate roots must match"): + self.check() + + +if __name__ == "__main__": + unittest.main() diff --git a/verifast-proofs/core/iter/adapters/verified/lib.rs b/verifast-proofs/core/iter/adapters/verified/lib.rs new file mode 100644 index 0000000000000..506672c09b373 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/verified/lib.rs @@ -0,0 +1,15 @@ +#![no_std] +#![crate_type = "lib"] +#![allow(dead_code, unused_imports, internal_features)] +#![feature(cast_maybe_uninit, core_intrinsics, staged_api, stmt_expr_attributes)] +#![stable(feature = "rust1", since = "1.0.0")] + +extern crate core as std; + +#[stable(feature = "rust1", since = "1.0.0")] +pub use std::{fmt, intrinsics, mem, num, ptr}; + +#[path = "../array_layout.rs"] +mod array_layout; +mod map_windows; +mod step_by; diff --git a/verifast-proofs/core/iter/adapters/verified/map_windows.rs b/verifast-proofs/core/iter/adapters/verified/map_windows.rs new file mode 100644 index 0000000000000..9b992de59336b --- /dev/null +++ b/verifast-proofs/core/iter/adapters/verified/map_windows.rs @@ -0,0 +1,527 @@ +// Generic contract proof. See ../README.md for validation evidence and scope. + +use crate::mem::MaybeUninit; +use crate::{fmt, ptr}; + +//@ use array_layout::{array_borrow_tokens, collapse_window, expand_window, lend_array, matrix_elems, own_matrix_storage, pack_matrix, reclaim_array, unpack_matrix}; +//@ use array_layout::{joined_window, mapped_append, mapped_length, mapped_range, mapped_uninit_upcast, matrix_upcast, owned_values_mono, owned_values_send}; + +struct Buffer { + // Invariant: `self.buffer[self.start..self.start + N]` is initialized, + // with all other elements being uninitialized. This also + // implies that `self.start <= N`. + buffer: [[MaybeUninit; N]; 2], + start: usize, +} + +/*@ + +fix width() -> usize { usize_of_const(typeid(N)) } + +fix base(b: *Buffer) -> *std::mem::MaybeUninit { + &(*b).buffer as *std::mem::MaybeUninit +} + +// These are constructor/layout restrictions, not a finite proof bound. +pred bounds(b: *Buffer; start: usize) = + (*b).start |-> start &*& 0 < width::() &*& + width::() <= usize::MAX / 2 &*& start <= width::() &*& + 2 * width::() * std::mem::size_of::() <= isize::MAX &*& + pointer_within_limits(base(b)) == true &*& + pointer_within_limits(base(b) + start) == true &*& + pointer_within_limits(base(b) + 2 * width::()) == true; + +// Inactive slots may retain copied bytes. They carry no ownership of T. +pred live(t: thread_id_t, b: *Buffer, start: usize, values: list) = + bounds(b, start) &*& length(values) == width::() &*& + base(b)[..start] |-> ?prefix &*& + (base(b) + start)[..width::()] |-> map(std::mem::MaybeUninit::new, values) &*& + (base(b) + start + width::())[..width::() - start] |-> ?suffix &*& + foreach(values, own::(t)); + +pred storage(b: *Buffer; start: usize) = + bounds(b, start) &*& base(b)[..2 * width::()] |-> ?slots; + +pred_ctor writable_matrix(b: *Buffer)(;) = (*b).buffer |-> ?matrix; + +pred >.own(t, buffer) = + exists::>(?values) &*& + 0 < width::() &*& width::() <= usize::MAX / 2 &*& + 0 <= buffer.start &*& buffer.start <= width::() &*& + 2 * width::() * std::mem::size_of::() <= isize::MAX &*& + length(values) == width::() &*& + take(width::(), drop(buffer.start, matrix_elems(buffer.buffer))) == + map(std::mem::MaybeUninit::new, values) &*& + foreach(values, own::(t)); + +lem Buffer_own_mono() + req type_interp::() &*& type_interp::() &*& type_interp::() &*& + Buffer_own::(?t, ?buffer) &*& is_subtype_of::() == true; + ens type_interp::() &*& type_interp::() &*& type_interp::() &*& + Buffer_own::(t, Buffer:: { + buffer: upcast(buffer.buffer), start: upcast(buffer.start) }); +{ + open Buffer_own::(t, buffer); + open exists::>(?values); + std::mem::subtype_layout::(); + std::mem::upcast_identity(buffer.start); + std::mem::MaybeUninit_subtype::(); + matrix_upcast::, std::mem::MaybeUninit, N>(buffer.buffer); + mapped_range::, std::mem::MaybeUninit>(upcast, + matrix_elems(buffer.buffer), buffer.start, width::()); + mapped_uninit_upcast::(values); + mapped_length::(upcast, values); + owned_values_mono::(t, values); + close exists(map::(upcast, values)); + close Buffer_own::(t, Buffer:: { + buffer: upcast(buffer.buffer), start: upcast(buffer.start) }); +} + +lem Buffer_send(t1: thread_id_t) + req type_interp::() &*& type_interp::() &*& Buffer_own::(?t0, ?buffer) &*& + is_Send(typeid(Buffer)) == true; + ens type_interp::() &*& type_interp::() &*& Buffer_own::(t1, buffer); +{ + open Buffer_own::(t0, buffer); + open exists::>(?values); + std::mem::array_Send::<[std::mem::MaybeUninit; N], 2>(); + std::mem::array_Send::, N>(); + std::mem::MaybeUninit_Send::(); + owned_values_send(t0, t1, values); + close exists(values); + close Buffer_own::(t1, buffer); +} + +// A destructor cannot consume ownership of the surviving window. +pred push_drop_frame(t: thread_id_t, b: *Buffer, start: usize, + values: list, matrix: *[[std::mem::MaybeUninit; N]; 2]) = + bounds(b, if start == width::() { 0 } else { start + 1 }) &*& + 0 <= start &*& start <= width::() &*& length(values) == width::() &*& + ref_mut_end_token(matrix, &(*b).buffer) &*& foreach(values, own::(t)) &*& + if start == width::() { + (matrix as *std::mem::MaybeUninit)[..width::()] |-> map(std::mem::MaybeUninit::new, values) &*& + ((matrix as *std::mem::MaybeUninit) + start + 1)[..width::() - 1] |-> ?stale + } else { + (matrix as *std::mem::MaybeUninit)[..start] |-> ?prefix &*& + ((matrix as *std::mem::MaybeUninit) + start + 1)[..width::()] |-> map(std::mem::MaybeUninit::new, values) &*& + ((matrix as *std::mem::MaybeUninit) + start + width::() + 1)[..width::() - start - 1] |-> ?suffix + }; + +// This ghost restoration is valid after either outcome of dropping the old front. +lem finish_push_storage(t: thread_id_t, b: *Buffer, start: usize, + values: list, matrix: *[[std::mem::MaybeUninit; N]; 2]) + req push_drop_frame(t, b, start, values, matrix) &*& + *(((matrix as *std::mem::MaybeUninit) + start) as *T) |-> _; + ens live(t, b, if start == width::() { 0 } else { start + 1 }, values); +{ + open push_drop_frame(t, b, start, values, matrix); + open bounds(b, if start == width::() { 0 } else { start + 1 }); + let p = matrix as *std::mem::MaybeUninit; + std::mem::close_MaybeUninit_(p + start); + if start == width::() { + close array(p + start, width::(), _); + assert (p + start)[..width::()] |-> ?suffix; + joined_window(nil, map(std::mem::MaybeUninit::new, values), suffix); + array_join(p); + } else { + close array(p + start + 1, 0, nil); + close array(p + start, 1, _); + array_join(p); + assert p[..start + 1] |-> ?prefix; + assert (p + start + width::() + 1)[..width::() - start - 1] |-> ?suffix; + joined_window(prefix, map(std::mem::MaybeUninit::new, values), suffix); + array_join(p); + array_join(p); + } + pack_matrix(matrix); + end_ref_mut(matrix); + unpack_matrix(&(*b).buffer); + array_split(base(b), if start == width::() { 0 } else { start + 1 }); + array_split(base(b) + (if start == width::() { 0 } else { start + 1 }), width::()); + close bounds(b, if start == width::() { 0 } else { start + 1 }); + close live(t, b, if start == width::() { 0 } else { start + 1 }, values); +} + +// The same frame survives normal and unwinding generic drop glue. +pred drop_frame(b: *Buffer, start: usize, + matrix: *[[std::mem::MaybeUninit; N]; 2], k: lifetime_t, slice: *[T]) = + bounds(b, start) &*& ref_mut_end_token(matrix, &(*b).buffer) &*& + (matrix as *std::mem::MaybeUninit)[..start] |-> ?prefix &*& + ((matrix as *std::mem::MaybeUninit) + start + width::())[..width::() - start] |-> ?suffix &*& + array_borrow_tokens(k, ((matrix as *std::mem::MaybeUninit) + start) as *T, width::()) &*& + close_points_to_at_lft_token(1, k, slice, 1) &*& + slice as *T == ((matrix as *std::mem::MaybeUninit) + start) as *T &*& + ptr_len(slice) == width::(); + +lem finish_drop_storage(b: *Buffer, start: usize, + matrix: *[[std::mem::MaybeUninit; N]; 2], k: lifetime_t, slice: *[T]) + nonghost_callers_only + req drop_frame(b, start, matrix, k, slice) &*& *slice |-> _; + ens storage(b, start); +{ + open drop_frame(b, start, matrix, k, slice); + open bounds(b, start); + close_points_to_at_lft_(slice); + open_points_to_slice_at_lft_(slice); + end_lifetime(k); + let p = matrix as *std::mem::MaybeUninit; + reclaim_array(k, (p + start) as *T, width::()); + std::mem::array__to_array_MaybeUninit((p + start) as *T); + array_join(p); + array_join(p); + pack_matrix(matrix); + end_ref_mut(matrix); + unpack_matrix(&(*b).buffer); + close bounds(b, start); + close storage(b, start); +} + +// Unwrap initialized slots without requiring T: Copy or duplicating T.own. +lem initialized_slots(p: *std::mem::MaybeUninit, values: list) + req p[..length(values)] |-> map(std::mem::MaybeUninit::new, values); + ens (p as *T)[..length(values)] |-> values; +{ + std::mem::MaybeUninit_layout::(); + open array(p, length(values), _); + match values { + nil => { + close array(p as *T, 0, nil); + } + cons(value, tail) => { + std::mem::open_MaybeUninit(p); + close points_to(p as *T, value); + initialized_slots(p + 1, tail); + close array(p as *T, length(values), values); + } + } +} + +lem wrap_slots(p: *T, values: list) + req p[..length(values)] |-> values; + ens (p as *std::mem::MaybeUninit)[..length(values)] |-> map(std::mem::MaybeUninit::new, values); +{ + std::mem::MaybeUninit_layout::(); + open array(p, length(values), values); + match values { + nil => { + close array(p as *std::mem::MaybeUninit, 0, nil); + } + cons(value, tail) => { + std::mem::close_MaybeUninit(p as *std::mem::MaybeUninit); + wrap_slots(p + 1, tail); + close array(p as *std::mem::MaybeUninit, length(values), _); + } + } +} + +// The caller supplies a borrow of the window. It can originate from a live +// initialized array (as_array_ref), or writable storage (as_uninit_array_mut). +// Proving the surrounding safe abstraction and its constructors is separate. + +@*/ + +impl Buffer { + #[inline] + unsafe fn buffer_ptr(&self) -> *const MaybeUninit +//@ req pointer_within_limits(base(self)) == true &*& [?f]ref_initialized(&(*self).buffer); + //@ ens [f]ref_initialized(&(*self).buffer) &*& result == base(self); + //@ on_unwind_ens false; + { + //@ reborrow_ref_(&(*self).buffer); + self.buffer.as_ptr().cast() + } + + #[inline] + unsafe fn buffer_mut_ptr(&mut self) -> *mut MaybeUninit +//@ req (*self).buffer |-> ?matrix; + //@ ens *(result as *[[std::mem::MaybeUninit; N]; 2]) |-> matrix &*& ref_mut_end_token(result as *[[std::mem::MaybeUninit; N]; 2], &(*self).buffer); + //@ on_unwind_ens false; + { + self.buffer.as_mut_ptr().cast() + } + + #[inline] + unsafe fn as_array_ref<'a>(&'a self) -> &'a [T; N] +/*@ + req [?f]bounds(self, ?start) &*& [?q]lifetime_token('a) &*& + [_]frac_borrow('a, ref_initialized_(self)) &*& + [?bf]ref_initialized(&(*self).buffer) &*& + type_interp::<[T; N]>() &*& + [_](<[T; N]>.share)('a, ?t, (base(self) + start) as *[T; N]); + @*/ + /*@ + ens [f]bounds(self, start) &*& [q]lifetime_token('a) &*& + [bf]ref_initialized(&(*self).buffer) &*& + type_interp::<[T; N]>() &*& + ref_origin(result) == ref_origin((base(self) + start) as *[T; N]) &*& + [_](<[T; N]>.share)('a, t, result); + @*/ + //@ on_unwind_ens false; + { + //@ open [f]bounds(self, start); + //@ assert start + width::() <= 2 * width::(); + #[rustfmt::skip] + if cfg!(debug_assertions) { //~allow_dead_code // The disabled configuration branch is unreachable. + assert!(self.start + N <= 2 * N); //~allow_dead_code // The proven bounds exclude assertion failure. + } + + // SAFETY: our invariant guarantees these elements are initialized. + let buffer_ptr = unsafe { self.buffer_ptr() }; + //@ let window = (base(self) + start) as *[T; N]; + //@ let reference = precreate_ref(window); + //@ init_ref_share('a, t, reference); + //@ let r = open_frac_borrow('a, ref_initialized_(reference), q); + //@ open [r]ref_initialized_::<[T; N]>(reference)(); + let result = unsafe { &*buffer_ptr.add(self.start).cast() }; + //@ close [r]ref_initialized_::<[T; N]>(reference)(); + //@ close_frac_borrow(r, ref_initialized_(reference)); + //@ close [f]bounds(self, start); + result + } + + #[inline] + unsafe fn as_uninit_array_mut<'a>(&'a mut self) -> &'a mut MaybeUninit<[T; N]> +/*@ + req thread_token(?t) &*& bounds(self, ?start) &*& [?q]lifetime_token('a) &*& + full_borrow('a, writable_matrix(self)); + @*/ + /*@ + ens thread_token(t) &*& bounds(self, start) &*& [q]lifetime_token('a) &*& + full_borrow('a, >.full_borrow_content(t, result)); + @*/ + //@ on_unwind_ens false; + { + //@ open bounds(self, start); + //@ assert start + width::() <= 2 * width::(); + #[rustfmt::skip] + if cfg!(debug_assertions) { //~allow_dead_code // The disabled configuration branch is unreachable. + assert!(self.start + N <= 2 * N); //~allow_dead_code // The proven bounds exclude assertion failure. + } + + // SAFETY: our invariant guarantees these elements are in bounds. + //@ open_full_borrow_strong_('a, writable_matrix(self)); + //@ open writable_matrix::(self)(); + let buffer_mut_ptr = unsafe { self.buffer_mut_ptr() }; + //@ unpack_matrix(buffer_mut_ptr as *[[std::mem::MaybeUninit; N]; 2]); + //@ array_split(buffer_mut_ptr, start); + //@ array_split(buffer_mut_ptr + start, width::()); + //@ collapse_window::(buffer_mut_ptr + start); + unsafe { + let result = &mut *buffer_mut_ptr.add(self.start).cast(); + //@ let window = (buffer_mut_ptr + start) as *std::mem::MaybeUninit<[T; N]>; + /*@ + { + pred ctx() = + ref_mut_end_token(result, window) &*& + ref_mut_end_token(buffer_mut_ptr as *[[std::mem::MaybeUninit; N]; 2], &(*self).buffer) &*& + buffer_mut_ptr[..start] |-> ?prefix &*& + (buffer_mut_ptr + start + width::())[..width::() - start] |-> ?suffix; + produce_lem_ptr_chunk restore_full_borrow_(ctx, + >.full_borrow_content(t, result), + writable_matrix(self))() { + open ctx(); + open_full_borrow_content::>(t, result); + assert *result |-> ?borrowed_contents; + std::mem::MaybeUninit_own_dispose::<[T; N]>(t, borrowed_contents); + end_ref_mut_::>(); + expand_window(window); + array_join(buffer_mut_ptr); + array_join(buffer_mut_ptr); + pack_matrix(buffer_mut_ptr as *[[std::mem::MaybeUninit; N]; 2]); + end_ref_mut_::<[[std::mem::MaybeUninit; N]; 2]>(); + close writable_matrix::(self)(); + } { + assert *result |-> ?contents; + std::mem::MaybeUninit_own_init::<[T; N]>(t, contents); + close_full_borrow_content::>(t, result); + close ctx(); + close_full_borrow_strong_(); + } + } + @*/ + //@ close bounds(self, start); + result + } + } + + /// Pushes a new item `next` to the back, and pops the front-most one. + /// + /// All the elements will be shifted to the front end when pushing reaches + /// the back end. + unsafe fn push(&mut self, next: T) + /*@ + req thread_token(?t) &*& live(t, self, ?start, ?values) &*& .own(t, next); + @*/ + /*@ + ens thread_token(t) &*& live(t, self, if start == width::() { 0 } else { start + 1 }, + append(tail(values), cons(next, nil))); + @*/ + /*@ + on_unwind_ens thread_token(t) &*& + push_drop_frame(t, self, start, append(tail(values), cons(next, nil)), ?matrix) &*& + *(((matrix as *std::mem::MaybeUninit) + start) as *T) |-> _; + @*/ + { + //@ open live(t, self, start, values); + //@ open bounds(self, start); + //@ let next_value = next; + //@ open array(base(self) + start, width::(), map(std::mem::MaybeUninit::new, values)); + //@ assert pointer_within_limits(base(self) + start + 1) == true; + //@ close array(base(self) + start, width::(), map(std::mem::MaybeUninit::new, values)); + //@ assert base(self)[..start] |-> ?prefix_slots; + //@ assert (base(self) + start + width::())[..width::() - start] |-> ?suffix_slots; + //@ joined_window(prefix_slots, map(std::mem::MaybeUninit::new, values), suffix_slots); + //@ array_join(base(self)); + //@ array_join(base(self)); + //@ pack_matrix(&(*self).buffer); + let buffer_mut_ptr = unsafe { self.buffer_mut_ptr() }; + //@ unpack_matrix(buffer_mut_ptr as *[[std::mem::MaybeUninit; N]; 2]); + //@ array_split(buffer_mut_ptr, start); + //@ array_split(buffer_mut_ptr + start, width::()); + //@ open foreach(values, own::(t)); + //@ open array(buffer_mut_ptr + start, width::(), _); + //@ assert start + width::() <= 2 * width::(); + #[rustfmt::skip] + if cfg!(debug_assertions) { //~allow_dead_code // The disabled configuration branch is unreachable. + assert!(self.start + N <= 2 * N); //~allow_dead_code // The proven bounds exclude assertion failure. + } + + let to_drop = if self.start == N { + // We have reached the end of our buffer and have to copy + // everything to the start. Example layout for N = 3. + // + // 0 1 2 3 4 5 0 1 2 3 4 5 + // ┌───┬───┬───┬───┬───┬───┐ ┌───┬───┬───┬───┬───┬───┐ + // │ - │ - │ - │ a │ b │ c │ -> │ b │ c │ n │ - │ - │ - │ + // └───┴───┴───┴───┴───┴───┘ └───┴───┴───┴───┴───┴───┘ + // ↑ ↑ + // start start + + // SAFETY: the two pointers are valid for reads/writes of N -1 + // elements because our array's size is semantically 2 * N. The + // regions also don't overlap for the same reason. + // + // We leave the old elements in place. As soon as `start` is set + // to 0, we treat them as uninitialized and treat their copies + // as initialized. + let to_drop = unsafe { + //@ array_split(buffer_mut_ptr, width::() - 1); + //@ open array(buffer_mut_ptr + width::() - 1, 1, _); + //@ array_to_array_(buffer_mut_ptr); + ptr::copy_nonoverlapping(buffer_mut_ptr.add(self.start + 1), buffer_mut_ptr, N - 1); + (*buffer_mut_ptr.add(N - 1)).write(next); + //@ end_ref_mut_::>(); + //@ open array(buffer_mut_ptr + width::(), 0, _); + //@ close array(buffer_mut_ptr + width::(), 0, nil); + //@ close array(buffer_mut_ptr + width::() - 1, 1, cons(std::mem::MaybeUninit::new(next), nil)); + //@ array_join(buffer_mut_ptr); + buffer_mut_ptr.add(self.start) + }; + self.start = 0; + to_drop + } else { + // SAFETY: `self.start` is < N as guaranteed by the invariant + // plus the check above. Even if the drop at the end panics, + // the invariant is upheld. + // + // Example layout for N = 3: + // + // 0 1 2 3 4 5 0 1 2 3 4 5 + // ┌───┬───┬───┬───┬───┬───┐ ┌───┬───┬───┬───┬───┬───┐ + // │ - │ a │ b │ c │ - │ - │ -> │ - │ - │ b │ c │ n │ - │ + // └───┴───┴───┴───┴───┴───┘ └───┴───┴───┴───┴───┴───┘ + // ↑ ↑ + // start start + // + let to_drop = unsafe { + //@ open array(buffer_mut_ptr + start + width::(), width::() - start, _); + (*buffer_mut_ptr.add(self.start + N)).write(next); + //@ end_ref_mut_::>(); + //@ close array(buffer_mut_ptr + start + width::() + 1, 0, nil); + //@ close array(buffer_mut_ptr + start + width::(), 1, cons(std::mem::MaybeUninit::new(next), nil)); + //@ array_join(buffer_mut_ptr + start + 1); + buffer_mut_ptr.add(self.start) + }; + self.start += 1; + to_drop + }; + + // SAFETY: the index is valid and this is element `a` in the + // diagram above and has not been dropped yet. + //@ close foreach(nil, own::(t)); + //@ close own::(t)(next); + //@ close foreach(cons(next, nil), own::(t)); + //@ foreach_append(tail(values), cons(next, nil)); + //@ mapped_append::>(std::mem::MaybeUninit::new, tail(values), cons(next, nil)); + //@ close bounds(self, if start == width::() { 0 } else { start + 1 }); + //@ close push_drop_frame(t, self, start, append(tail(values), cons(next, nil)), buffer_mut_ptr as *[[std::mem::MaybeUninit; N]; 2]); + //@ std::mem::open_MaybeUninit(to_drop); + //@ close points_to(to_drop as *T, head(values)); + //@ open own::(t)(head(values)); + unsafe { ptr::drop_in_place(to_drop.cast_init()) }; + //@ finish_push_storage(t, self, start, append(tail(values), cons(next, nil)), buffer_mut_ptr as *[[std::mem::MaybeUninit; N]; 2]); + //@ assert live(t, self, if start == width::() { 0 } else { start + 1 }, append(tail(values), cons(next_value, nil))); + } //~allow_dead_code // Rust emits cleanup for the already moved next argument. +} + +impl Drop for Buffer { + fn drop(&mut self) + /*@ + req thread_token(?t) &*& live(t, self, ?start, ?values); + @*/ + /*@ + ens thread_token(t) &*& drop_frame(self, start, ?matrix, ?k, ?slice) &*& *slice |-> _; + @*/ + //@ on_unwind_ens thread_token(t) &*& drop_frame(self, start, ?matrix, ?k, ?slice) &*& *slice |-> _; + /*@ + safety_proof { + open Buffer_full_borrow_content::(_t, self)(); + open >.own(_t, ?buffer); + open exists::>(?values); + let start = buffer.start; + unpack_matrix(&(*self).buffer); + array_split(base(self), start); + array_split(base(self) + start, width::()); + close bounds(self, start); + close live(_t, self, start, values); + call(); + assert drop_frame(self, start, ?matrix, ?k, ?slice); + finish_drop_storage(self, start, matrix, k, slice); + open storage(self, start); + open bounds(self, start); + pack_matrix(&(*self).buffer); + assert (*self).buffer |-> ?after; + own_matrix_storage(_t, after); + } + @*/ + { + //@ open live(t, self, start, values); + //@ open bounds(self, start); + //@ assert base(self)[..start] |-> ?prefix_slots; + //@ assert (base(self) + start + width::())[..width::() - start] |-> ?suffix_slots; + //@ joined_window(prefix_slots, map(std::mem::MaybeUninit::new, values), suffix_slots); + //@ array_join(base(self)); + //@ array_join(base(self)); + //@ pack_matrix(&(*self).buffer); + // SAFETY: our invariant guarantees that N elements starting from + // `self.start` are initialized. We drop them here. + unsafe { + let buffer_mut_ptr = self.buffer_mut_ptr(); + //@ let matrix = buffer_mut_ptr as *[[std::mem::MaybeUninit; N]; 2]; + //@ unpack_matrix(matrix); + //@ array_split(buffer_mut_ptr, start); + //@ array_split(buffer_mut_ptr + start, width::()); + let initialized_part: *mut [T] = + crate::ptr::slice_from_raw_parts_mut(buffer_mut_ptr.add(self.start).cast(), N); + //@ initialized_slots(buffer_mut_ptr + start, values); + //@ let k = begin_lifetime(); + //@ lend_array(k, (buffer_mut_ptr + start) as *T, width::()); + //@ close_points_to_slice_at_lft(initialized_part); + //@ open_points_to_at_lft(initialized_part, 1); + //@ close <[T]>.own(t, slice_of_elems(values)); + //@ close bounds(self, start); + //@ close drop_frame(self, start, matrix, k, initialized_part); + ptr::drop_in_place(initialized_part); + } + } +} diff --git a/verifast-proofs/core/iter/adapters/verified/step_by.rs b/verifast-proofs/core/iter/adapters/verified/step_by.rs new file mode 100644 index 0000000000000..bfbf327ddc227 --- /dev/null +++ b/verifast-proofs/core/iter/adapters/verified/step_by.rs @@ -0,0 +1,38 @@ +// Generic contract proof. See ../README.md for validation evidence and scope. + +use crate::intrinsics; +use crate::num::NonZero; + +#[must_use = "iterators are lazy and do nothing unless consumed"] +#[stable(feature = "iterator_step_by", since = "1.28.0")] +#[derive(Clone, Debug)] +pub struct StepBy { + /// This field is guaranteed to be preprocessed by the specialized `SpecRangeSetup::setup` + /// in the constructor. + /// For most iterators that processing is a no-op, but for Range<{integer}> types it is lossy + /// which means the inner iterator cannot be returned to user code. + /// Additionally this type-dependent preprocessing means specialized implementations + /// cannot be used interchangeably. + iter: I, + /// This field is `step - 1`, aka the correct amount to pass to `nth` when iterating. + /// It MUST NOT be `usize::MAX`, as `unsafe` code depends on being able to add one + /// without the risk of overflow. (This is important so that length calculations + /// don't need to check for division-by-zero, for example.) + step_minus_one: usize, + first_take: bool, +} + +impl StepBy { + /// The `step` that was originally passed to `Iterator::step_by(step)`, + /// aka `self.step_minus_one + 1`. + #[inline] + unsafe fn original_step(&self) -> NonZero +//@ req [?f](*self).step_minus_one |-> ?step &*& step < usize::MAX; + //@ ens [f](*self).step_minus_one |-> step &*& result.get() == step + 1 &*& 0 < result.get(); + //@ on_unwind_ens false; + { + // SAFETY: By type invariant, `step_minus_one` cannot be `MAX`, which + // means the addition cannot overflow and the result cannot be zero. + unsafe { NonZero::new_unchecked(intrinsics::unchecked_add(self.step_minus_one, 1)) } + } +} diff --git a/verifast-proofs/core/iter/adapters/verify.sh b/verifast-proofs/core/iter/adapters/verify.sh new file mode 100644 index 0000000000000..b4ff0f1e58fba --- /dev/null +++ b/verifast-proofs/core/iter/adapters/verify.sh @@ -0,0 +1,377 @@ +#!/usr/bin/env bash +set -euo pipefail + +proof_dir="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)" +cd "$proof_dir" + +case "${1:-}" in + --static) + exec python3 -I check_sources.py + ;; + --remote) + ;; + *) + echo 'Usage: bash verify.sh --static | --remote' >&2 + echo '--remote runs compilers and solvers on a prepared Linux machine.' >&2 + exit 2 + ;; +esac + +# Do not invoke the repository wrappers on the memory-constrained Mac. +# The wrappers may install VeriFast and its pinned Rust toolchain. +if [[ "$(uname -s)" != Linux ]]; then + echo 'Proof execution requires a separate Linux machine. Use --static here.' >&2 + exit 2 +fi + +python3 -I check_sources.py + +# This is a per-process address-space limit, not an aggregate process-tree cap. +# Require headroom for the verifier, Rust frontend, solver, and operating system. +python3 -I - <<'PY' +from pathlib import Path +import sys + +fields = dict(line.split(":", 1) for line in Path("/proc/meminfo").read_text().splitlines()) +available_kib = int(fields["MemAvailable"].split()[0]) +if available_kib < 8 * 1024 * 1024: + sys.exit("Proof execution requires at least 8 GiB currently available RAM.") +print(f"Remote preflight: {available_kib // 1024} MiB available RAM") +PY + +command -v timeout >/dev/null +ulimit -c 0 +ulimit -t 600 +export VFVERSION=26.09 +export CARGO_BUILD_JOBS=1 +export RAYON_NUM_THREADS=1 +export PATH="$proof_dir/../../..:$PATH" + +# Install the pinned release and build its patched Rust frontend remotely. +# The workflow's cgroup also covers this build. Proof processes get the tighter +# per-process address-space limit after the compiler has finished. +export VFPLATFORM=linux +# shellcheck source=/dev/null +source "$proof_dir/../../../setup-verifast-home" +export VERIFAST_HOME +timeout --signal=TERM --kill-after=10s 900s bash backend/prepare.sh --remote +ulimit -v 2097152 + +# Check both the defined-input case and rejection of a potentially overflowing +# input before trusting the frontend mapping for the adapter proof. +timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/add-valid.rs +timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/const-valid.rs +if ! timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/array-valid.rs; then + # The regression already failed. Emit heap context without changing that verdict. + diagnostic_status=0 + timeout --signal=TERM --kill-after=5s 30s \ + verifast -json -rustc_args '--edition 2024' backend/array-valid.rs || diagnostic_status=$? + printf 'Array regression diagnostic status: %s\n' "$diagnostic_status" + exit 1 +fi +negative_log="$(mktemp)" +trap 'rm -f -- "$negative_log"' EXIT +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/array-length-invalid.rs >"$negative_log" 2>&1; then + cat "$negative_log" + echo 'The array-to-slice coercion accepted an incorrect length.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "Cannot prove" not in diagnostics or "Rust frontend failed" in diagnostics: + raise SystemExit("The array length check did not report the expected proof failure") +PY +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/add-overflow.rs >"$negative_log" 2>&1; then + cat "$negative_log" + echo 'The frontend accepted unchecked addition without an overflow precondition.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "Potential arithmetic overflow." not in diagnostics or "Rust frontend failed" in diagnostics: + sys.exit("The negative check did not produce the required overflow diagnostic.") +PY +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/const-invalid.rs >"$negative_log" 2>&1; then + cat "$negative_log" + echo 'The frontend accepted an incorrect symbolic array length.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "Cannot prove" not in diagnostics or "Rust frontend failed" in diagnostics: + sys.exit("The const-parameter negative check did not reach a proof failure.") +PY +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/array-invalid.rs >"$negative_log" 2>&1; then + cat "$negative_log" + echo 'The frontend accepted an array reference without a shared borrow.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "No matching heap chunks" not in diagnostics or "Rust frontend failed" in diagnostics: + sys.exit("The array-reference negative check did not reach a borrow proof failure.") +PY +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/array-mut-invalid.rs >"$negative_log" 2>&1; then + cat "$negative_log" + echo 'The frontend accepted a mutable array reference without owning its storage.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "No matching heap chunks" not in diagnostics or "Rust frontend failed" in diagnostics: + sys.exit("The mutable-array negative check did not reach a storage proof failure.") +PY +timeout --signal=TERM --kill-after=10s 60s \ + refinement-checker --rustc-args '--edition 2024' \ + backend/refinement-original.rs backend/refinement-valid.rs +if timeout --signal=TERM --kill-after=10s 60s \ + refinement-checker --rustc-args '--edition 2024' \ + backend/refinement-original.rs backend/refinement-invalid.rs >"$negative_log" 2>&1; then + cat "$negative_log" + echo 'The refinement checker equated distinct symbolic const parameters.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if not all(s in diagnostics for s in ("ConstParamTerm N", "ConstParamTerm M", "not equal")): + sys.exit("The refinement negative check did not distinguish the two const parameters.") +PY + +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/matrix-invalid.rs >"$negative_log" 2>&1; then + echo 'The array-to-slice negative check unexpectedly passed.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "No matching heap chunks" not in diagnostics or "Rust frontend failed" in diagnostics: + sys.exit("The array-to-slice negative check did not reject missing reference permissions.") +PY + +timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/nonzero-valid.rs +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/nonzero-invalid.rs >"$negative_log" 2>&1; then + echo 'The NonZero negative check unexpectedly passed.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "Cannot prove" not in diagnostics or "Rust frontend failed" in diagnostics: + sys.exit("The NonZero negative check did not reject the missing nonzero precondition.") +PY + +timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/maybeuninit-own-valid.rs +timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/cast-init-valid.rs +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/cast-init-invalid.rs >"$negative_log" 2>&1; then + echo 'The pointer cast granted access to missing initialized storage.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "No matching heap chunks" not in diagnostics or "Rust frontend failed" in diagnostics: + raise SystemExit("The cast negative check did not reject a read without storage") +PY +if timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/value-own-invalid.rs >"$negative_log" 2>&1; then + echo 'The ownership model created ownership of an arbitrary T.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "No matching heap chunks" not in diagnostics or "Rust frontend failed" in diagnostics: + raise SystemExit("The negative ownership check did not reject missing T ownership") +PY + +# Keep every stage sequential and require both proof and refinement to succeed. +# Collect their independent diagnostics even when the first stage fails. +# No assumption, unwind, reference-creation, or overflow suppression flags. +if timeout --signal=TERM --kill-after=5s 30s \ + verifast -rustc_args '--edition 2024' backend/layout-invalid.rs >"$negative_log" 2>&1; then + echo 'The incorrect array stride unexpectedly verified' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "Cannot prove condition" not in diagnostics or "Rust frontend failed" in diagnostics: + raise SystemExit("The negative layout check did not reject the incorrect stride") +PY + +for negative_fixture in backend/subtype-invalid.rs backend/value-send-invalid.rs; do + if timeout --signal=TERM --kill-after=5s 30s \ + verifast -rustc_args '--edition 2024' "$negative_fixture" >"$negative_log" 2>&1; then + printf 'Invalid generic conversion unexpectedly verified: %s\n' "$negative_fixture" >&2 + exit 1 + fi + cat "$negative_log" + python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if "Cannot prove condition" not in diagnostics or "Rust frontend failed" in diagnostics: + raise SystemExit("The negative conversion check did not reject its missing precondition") +PY +done + +if timeout --signal=TERM --kill-after=5s 30s \ + verifast -rustc_args '--edition 2024' backend/ghost-reachability-invalid.rs >"$negative_log" 2>&1; then + echo 'An unreachable normal-path ghost assertion unexpectedly verified.' >&2 + exit 1 +fi +cat "$negative_log" +python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +diagnostics = Path(sys.argv[1]).read_text() +if not any("ghost-reachability-invalid.rs(9," in line and line.endswith(": dead code") + for line in diagnostics.splitlines()): + raise SystemExit("The reachability negative check did not reject the ghost assertion") +PY + +layout_status=0 +timeout --signal=TERM --kill-after=10s 60s \ + verifast -rustc_args '--edition 2024' backend/matrix-layout-valid.rs || layout_status=$? +proof_status=0 +timeout --signal=TERM --kill-after=10s 600s \ + verifast -rustc_args '--edition 2024 -C debug-assertions=yes' -skip_specless_fns verified/lib.rs || proof_status=$? +refinement_status=0 +timeout --signal=TERM --kill-after=10s 600s \ + refinement-checker --rustc-args '--edition 2024 -C debug-assertions=yes' original/lib.rs verified/lib.rs || refinement_status=$? +python3 -I check_sources.py +if (( proof_status != 0 || layout_status != 0 )); then + # Inspect compiler-generated cleanup when reachability diagnostics remain. + diagnostic_status=0 + timeout --signal=TERM --kill-after=5s 60s \ + rustup run nightly-2026-02-05 rustc --edition 2024 --crate-type lib \ + --emit=mir -Zmir-include-spans=yes -o "$negative_log" verified/lib.rs || diagnostic_status=$? + printf 'MIR diagnostic process status: %s\n' "$diagnostic_status" + if (( diagnostic_status == 0 )); then + python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import sys + +path = Path(sys.argv[1]) +if path.stat().st_size > 8 * 1024 * 1024: + raise SystemExit("MIR diagnostic exceeded the 8 MiB parsing limit") +printing = False +budget = 24000 +for line in path.read_text().splitlines(): + if line.startswith("fn "): + printing = "::push(" in line + if printing and budget > 0: + print(line[:budget]) + budget -= len(line) + 1 +PY + fi + diagnostic_status=0 + timeout --signal=TERM --kill-after=5s 60s \ + verifast -rustc_args '--edition 2024 -C debug-assertions=no' \ + -skip_specless_fns verified/lib.rs || diagnostic_status=$? + printf 'Debug-assertions-disabled diagnostic status: %s\n' "$diagnostic_status" + # These bounded, sequential diagnostics cannot replace the full proof verdict. + while IFS= read -r proof_location; do + diagnostic_status=0 + timeout --signal=TERM --kill-after=5s 30s \ + verifast -json -rustc_args '--edition 2024' -skip_specless_fns \ + -focus "$proof_location" verified/lib.rs >"$negative_log" 2>&1 || diagnostic_status=$? + printf 'Diagnostic %s: process status %s\n' "$proof_location" "$diagnostic_status" + python3 -I - "$negative_log" <<'PY' +from pathlib import Path +import json +import sys + +path = Path(sys.argv[1]) +if path.stat().st_size > 8 * 1024 * 1024: + raise SystemExit("Diagnostic exceeded the 8 MiB parsing limit") +lines = path.read_text().splitlines() +for line in reversed(lines): + if line.startswith('["VeriFast-Json",'): + result = json.loads(line)[3]["result"] + if result[0] == "SymbolicExecutionError": + print(json.dumps(result[2:4])) + for frame in result[1]: + if frame[0] == "Executing": + print(json.dumps(frame)[:7000]) + break + else: + print(json.dumps(result)[:7000]) + break +else: + print("No JSON verdict; last diagnostic lines:") + print("\n".join(lines[-15:])[:7000]) +PY + done < <(python3 -I - <<'PY' +from pathlib import Path +import re + +for path in (Path("array_layout.rs"), Path("verified/map_windows.rs"), Path("verified/step_by.rs")): + for line_number, line in enumerate(path.read_text().splitlines(), 1): + if re.match(r"\s*(?:unsafe\s+)?(?:fn|lem)\s+\w+", line): + location_path = "verified/../array_layout.rs" if path.name == "array_layout.rs" else str(path) + print(f"{location_path}:{line_number}") +PY + ) +fi +if (( proof_status != 0 || refinement_status != 0 || layout_status != 0 )); then + printf 'FAIL: proof status %s; refinement status %s; layout status %s\n' \ + "$proof_status" "$refinement_status" "$layout_status" >&2 + exit 1 +fi +echo 'PASS: generic adapter contracts, source refinement, and source identity'