vstd_extra/external/
iter.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Specification for owned-array iteration not yet modeled by `vstd`.
3use vstd::{prelude::*, std_specs::iter::IteratorSpec};
4
5verus! {
6
7/// Verus proxy for the standard library's array `IntoIter`.
8#[verifier::external_type_specification]
9#[verifier::external_body]
10#[verifier::reject_recursive_types(T)]
11pub struct ExArrayIntoIter<T, const N: usize>(core::array::IntoIter<T, N>);
12
13/// The array iterator yields the array view from left to right and terminates.
14/// See [`array::into_iter`](https://doc.rust-lang.org/std/primitive.array.html#method.into_iter).
15pub assume_specification<T, const N: usize>[ <[T; N] as IntoIterator>::into_iter ](
16    array: [T; N],
17) -> (iter: <[T; N] as IntoIterator>::IntoIter)
18    ensures
19        IteratorSpec::obeys_prophetic_iter_laws(&iter),
20        IteratorSpec::will_return_none(&iter),
21        IteratorSpec::remaining(&iter) == array@,
22        IteratorSpec::decrease(&iter) == Some(N as nat),
23;
24
25} // verus!
vstd_extra/external/iter.rs

vstd_extra/external/
iter.rs
