Consider supporting iterator combinators where the combinator chain is discharged with a for-loop and with a .collect::<Vec<_>>()

[utaal]

and without explicit calls to .next(), which are rare in practice (as noted by @jaybosamiya).

We can start by supporting iterating on Range, and then combinations of .map, .filter etc that directly map to a Seq spec transformation when the iterator combinator chain is .collected in one shot (@Chris-Hawblitzel, @utaal).

[jaybosamiya]

Just noting that the specific feature that I was mentioning earlier today as quite rare was the splitting of an iterator into two to consume parts of the iterator separately, basically using Iterator::by_ref.

Using .next() itself is somewhat common in practice, but the most common use cases for it are fairly simple (for example, to get the first element of a singleton vector, while dropping the vector itself, thereby not needing a Clone on the elements of the vector: v.into_iter().next().unwrap(), which could basically be replaced just with a v.pop_front().unwrap() or v.swap_remove(0) or ...).

I think it is perfectly fine for a first pass to ignore these manual .next() use cases (if it makes implementation easier), but if our aim is to support all of safe Rust, then at some point, we're almost definitely going to have to support manual invocations of .next(). As for by_ref, that is indeed rarer, and could be punted for longer (esp since imho seems like an even more difficult challenge than just .next()).

[bsdinis]

Hi! I'm looking into adding these specs (at least to a couple of combinators to begin with).
I'm pretty new to the codebase and something that I'm struggling with is how to structure the specs.
Apologies for the rudimentary questions.

I have two main questions.

First, how to structure the specs:

• verus/source/vstd/std_specs/core.rs

  Line 142 in 5e8a125

  pub open spec fn iter_into_iter_spec<I: Iterator>(i: I) -> I {

  has a spec for Iterator::into_iter;
• However, adding a similar Iterator::enumerate yields an error assume_specification not supported for unresolved trait functions which make sense in general, but I can't figure out how to solve per se.

The second question relates to how one would go about relating the iterator view between the original and the adapted one. Continuing the example of enumerate, something like (super pseudo-Verus)

fn enumerate(self) -> (r: Enumerate<Self>)
  ensures forall|i: int| 0 <= i ==> i == r@[i].0 && self@[i] == r@[i].1 

Where we relate the values between the original and the adapted and the position with the first element of the pair.
However, Iterator does not implement view, and it's hard to imagine how it could. Maybe I'm thinking about this wrong?

[parno]

This might get simpler once #1629 lands.