vstd: add IteratorSpec for core::iter::Enumerate

[arxgy]

vstd/std_specs/iter.rs provides IteratorSpec implementations for iterator adapters such as Rev, but not for core::iter::Enumerate. A function that consumes an enumerate therefore fails to verify:

fn tag_indices(v: Vec<u32>) -> (out: Vec<(usize, u32)>)
    ensures out@ == v@.map(|k: int, x: u32| ((k as usize), x)),
{
    let mut out: Vec<(usize, u32)> = Vec::new();
    let it = v.into_iter();
    let en = it.enumerate();
    for (i, x) in en {
        out.push((i, x));
    }
    out                     // fails: `Enumerate` is not supported (Enumerate has no IteratorSpec)
}

Fix

This PR adds an IteratorSpec for core::iter::Enumerate. It contributes:

• remaining(): the items the iterator will yield. It is the inner iterator's remaining items, each paired with the index it will be reached at.
• enumerate_postcondition: a broadcast axiom giving enumerate_iter(r) == i and enumerate_count(r) == 0, the inner iterator and the counter the result starts from.
• peek(): the inner iterator's guess, paired with the same index, so that a for-loop's (i, x) pattern is usable in its invariant.
• an open decrease(), will_return_none() and obeys_prophetic_iter_laws(), each forwarding to the inner iterator.

After introducing Enumerate in this PR, we can reason the Enumerate iterator in Verus. And the problem code above can be proved as below:

 fn tag_indices(v: Vec<u32>) -> (out: Vec<(usize, u32)>)
     ensures out@ == v@.map(|k: int, x: u32| ((k as usize), x)),
 {
     let mut out: Vec<(usize, u32)> = Vec::new();
     let it = v.into_iter();
     let en = it.enumerate();
-    for (i, x) in en {
+    for (i, x) in iter: en
+        invariant out@ == iter.seq().take(iter.index()),
+    {
         out.push((i, x));
     }
     out
 }

A for-loop-over-enumerate regression test is included.

_{By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.}

[parno]

Thanks for the contribution! I added some comments/suggestions.

[parno]

In our other iterators, we have marked remaining, will_return_none, and decrease as closed, uninterp functions, and provided the necessary knowledge via the *_postcondition conditions. See, for example, the way Map is handled. For consistency, can we update this iterator accordingly?

[parno]

Is this assert necessary for the proof or is it illustrative? Either way, the comment is a bit unclear.

[parno]

I'm not sure this line or the next is needed; it seems more confusing than clarifying.

[parno]

This test seems tautological, since it's just repeating the relevant definitions in remaining_of_fresh_enumerate, and the second one seems more about collect's functionality. Let's cut the test.

[parno]

I'm not convinced this one is useful either.

[parno]

I also notice that the Rust docs say:

The method does no guarding against overflows, so enumerating more than usize::MAX elements either produces the wrong result or panics.
We might need to adjust your specs to account for that.