For loops

[Chris-Hawblitzel]

Examples:

        fn test_loop() {
            let mut n: u64 = 0;
            for x in iter: 0..10
                invariant n == iter.cur * 3,
            {
                assert(x < 10);
                assert(x == iter.cur);
                n += 3;
            }
            assert(n == 30);
        }

        fn test_loop_peek() {
            let mut n: u64 = 0;
            for x in 0..10
                invariant n == x * 3,
            {
                assert(x < 10);
                n += 3;
            }
            assert(n == 30);
        }

        fn test_loop(n: u32) -> (v: Vec<u32>)
            ensures
                v.len() == n,
                forall|i: int| 0 <= i < n ==> v[i] == i,
        {
            let mut v: Vec<u32> = Vec::new();
            for i in iter: 0..n
                invariant
                    v@ =~= iter@,
            {
                v.push(i);
            }
            v
        }

Currently, this has been tested on ranges but other iterators that implement the appropriate traits could also be used:

pub trait ForLoopGhostIterator {
    type ExecIter;
    type Item;
    type Decrease;

    // Connect the ExecIter to the GhostIter
    // Always enabled
    // Always true before and after each loop iteration
    spec fn exec_invariant(&self, exec_iter: &Self::ExecIter) -> bool;

    // Additional optional invariants about the GhostIter
    // May be disabled with #[verifier::no_auto_loop_invariant]
    // If enabled, always true before and after each loop iteration
    // (When the analysis can infer a spec initial value, the analysis places the value in init)
    spec fn ghost_invariant(&self, init: Option<&Self>) -> bool;

    // Is the loop condition satisfied?
    spec fn ghost_condition(&self) -> bool;

    // Value used by default for decreases clause when no explicit decreases clause is provided
    // (the user can override this with an explicit decreases clause).
    // (If there's no appropriate decrease, this can return an arbitrary value like 0,
    // and the user will have to provide an explicit decreases clause.)
    spec fn ghost_decrease(&self) -> Self::Decrease;

    // If there will be Some next value, and we can make a useful guess as to what the next value
    // will be, return it.
    // Otherwise, return an arbitrary value.
    spec fn ghost_peek_next(&self) -> Self::Item;

    // At the end of the for loop, advance to the next position.
    spec fn ghost_advance(&self, exec_iter: &Self::ExecIter) -> Self where Self: Sized;
}

pub trait ForLoopGhostIteratorNew {
    type GhostIter;

    // Create a new ghost iterator from an exec iterator
    spec fn ghost_iter(&self) -> Self::GhostIter;
}

It is conventional, but not mandated, that ghost iterators will also implement a view method that returns a Seq of all the elements iterated over so far.

The syntax macro translates for loops into regular loops with an added ghost iterator and added invariants, so that for x in y: e invariant inv { body } is translated into:

{
    #[allow(non_snake_case)]
    let mut VERUS_exec_iter = core::iter::IntoIterator::into_iter(e);
    #[allow(non_snake_case)]
    let ghost mut y = vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter(&VERUS_exec_iter);
    loop
        invariant_ensures
            vstd::pervasive::ForLoopGhostIterator::exec_invariant(&y, &VERUS_exec_iter),
            vstd::pervasive::ForLoopGhostIterator::ghost_invariant(&y,
                builtin::infer_spec_for_loop_iter(
                    &vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter(
                        &core::iter::IntoIterator::into_iter(e)))),
            { let x = vstd::pervasive::ForLoopGhostIterator::ghost_peek_next(&y); inv },
        ensures
            !vstd::pervasive::ForLoopGhostIterator::ghost_condition(&y),
    {
        if let Some(x) = core::iter::Iterator::next(&mut y) { body } else { break }
        proof { y = vstd::pervasive::ForLoopGhostIterator::ghost_advance(&y, &VERUS_exec_iter); }
    }
}

This translation is only used for verification; when erasing spec or proofs, the translation produces the original for loop with the spec code erased. For verification, regular loops are used in order to get access to the executable iterator so that exec_invariant can be applied to it.

The ghost_invariant method takes an optional init value containing the original expression that was used to create the exec and ghost iterators. This expression is an exec expression, but if it is legal to view the expression as a spec expression (e.g. via when_used_as_spec), and the spec expression only depends on variables that are unmodified inside the loop, then Verus passes the expression as Some(expression) to init. This enables a much stronger ghost_invariant that, for example, can talk about the end of the Range without the programmer having to write an explicit invariant like iter.end == 10 or 0 <= iter.cur < 10.

[Chris-Hawblitzel]

Note: I think ghost_advance and ghost_iter should probably be proof functions rather than spec functions, but I'd like to wait to see if we can do #851 first.

[tjhance]

What does it mean 'Return Some(spec) if successful, None otherwise'? This isn't documentation for a function, so what's doing the returning?

[Chris-Hawblitzel]

I fixed it to say Evaluate to

[tjhance]

What's this comment about?

[Chris-Hawblitzel]

I fixed this to use an actual PhantomData value

[tjhance]

I'm not sure what a better way to do it is, but I think the current infer_spec_for_loop_iter_modes span map system has some weird behavior; specifically, I worry about the side effects of the AST traversals that we'd rather ignore:

• In the modes.rs traversal, we traverse the contents, then ignore any error we get
• In the ast_simplify.rs traversal, the expression will be mapped only to be thrown away (the ast_visitor map function goes bottom-up). And unless I'm mistaken, this means an error won't get thrown away

Also, in both traversals, the 'state' object is going to be updated, even though the result is going to be thrown away. This seems particularly problematic in modes.rs, where an error bubbling up would cause the 'state' to end up in an invalid state.

[Chris-Hawblitzel]

I'm not sure what a better way to do it is, but I think the current infer_spec_for_loop_iter_modes span map system has some weird behavior; specifically, I worry about the side effects of the AST traversals that we'd rather ignore:

• In the modes.rs traversal, we traverse the contents, then ignore any error we get
• In the ast_simplify.rs traversal, the expression will be mapped only to be thrown away (the ast_visitor map function goes bottom-up). And unless I'm mistaken, this means an error won't get thrown away

Also, in both traversals, the 'state' object is going to be updated, even though the result is going to be thrown away. This seems particularly problematic in modes.rs, where an error bubbling up would cause the 'state' to end up in an invalid state.

I changed this to perform the modification entirely in modes.rs, so ast_simplify.rs is no longer involved. Within modes.rs, I changed the code to restore state after processing an Err for InferSpecForLoopIter.

[tjhance]

ret_mode needs to be saved too

[jaybosamiya]

Overall, I think this is a really cool and important feature to add!

A few comments/questions:

1. Are there situations where iter.cur is necessary, and we cannot just use the iteration variable x? If so, this might be good to document with an example when explaining the feature. Overall I do believe that in some cases iter.cur might be more readable than x, so I think we should have it anyways, but yeah, if we have an example, that would motivate it even more.

2. for x in 0..10 in Rust is slightly different from C's for (int x = 0; x < 10; x++) in that the variable x is never actually set to 10 in Rust, instead the iterator just "runs out". Do we think that can be a point of confusion in the invariant for more complex iterators in the future? Specifically, consider for x in (0..10).map(|a| a * 3).filter(|b| b < 13), which doesn't have a trivial "last value", so the final value exposed to the outside might not be obvious. Fwiw, this might possibly be fixed simply through sufficient documentation in the book, and might not need a fix to the design, but is definitely something we need to pay attention to, since folks who understand how Rust iterators work can be confused by this.

3. Is the trait design restricting us to terminating iterators only? Supporting non-terminating iterators would be important btw. I believe that the current design would support them, but just bringing up a few examples that we should look into to confirm that (eventually when we add the other iterator combinators) would not require a re-design of the ForLoopGhostIterator trait: std::iter::repeat(()).take(10) is terminating, since the repeat is non-terminating (so would just have an arbitrary value in its ghost_decrease), but then the take could make it terminating (by having an actually decreasing value in ghost_decrease). Also (0..10).take_while(|a| a * a < 10) is terminating because even though take_while may or may not be terminating by itself, the 0..10 is terminating.

4. For ghost_peek_next, is there a reason that it is not returning an Option<Self::Item> and using .unwrap_or(vstd::pervasive::arbitrary()) or similar in the expansion? That might be a cleaner thing for implementers of the trait to implement. Similar for ghost_decrease. It is possible I'm missing something obvious here btw, so mostly asking for clarification (but I do think modulo a good reason, we might want to put the Options there)

5. I really love the automatic inference of 0 <= iter.cur <= 10 <3 I also appreciate that this has the machinery to support this for arbitrarily complex user-defined iterators too.

6. Can we (or indeed even should we) support things like let mut iter = (0..10); for x in iter { ... }, without needing to say for x in iter: iter or similar to be able to access the iter view and such. I don't think this is a common use case though, so it might be fine to even just say "live with the iter: iter" btw.

[tjhance]

Could we split Typing into two objects, one passed by & and one passed by &mut, to match the style of the other recursions? That would make the 'state' a lot smaller, so we could just clone it.

[Chris-Hawblitzel]

1. Are there situations where iter.cur is necessary, and we cannot just use the iteration variable x? If so, this might be good to document with an example when explaining the feature. Overall I do believe that in some cases iter.cur might be more readable than x, so I think we should have it anyways, but yeah, if we have an example, that would motivate it even more.

I think this will come up when we use iterators generated by slices and vectors. There are some unrelated technical issues to resolve in working with slices before this will work properly with the std library iterators, but in the meantime the for_loop_vec_custom_iterator test gives a preview of what a Vec iterator would look like:

            // TODO: should be able to just say:
            // for x in iter: v
            for x in iter: vec_iter_copy(v)
                invariant
                    b <==> (forall|i: int| 0 <= i < iter.cur ==> v[i] > 0),
            {

Here, x is the element from the Vec in each iteration, and x isn't nearly as useful in invariants as iter is. So I agree, when these iterators are ready, the Verus guide documentation on for loops should explain why it's necessary to use the iterator in the invariants for iterators from collection types.

2. for x in 0..10 in Rust is slightly different from C's for (int x = 0; x < 10; x++) in that the variable x is never actually set to 10 in Rust, instead the iterator just "runs out". Do we think that can be a point of confusion in the invariant for more complex iterators in the future? Specifically, consider for x in (0..10).map(|a| a * 3).filter(|b| b < 13), which doesn't have a trivial "last value", so the final value exposed to the outside might not be obvious. Fwiw, this might possibly be fixed simply through sufficient documentation in the book, and might not need a fix to the design, but is definitely something we need to pay attention to, since folks who understand how Rust iterators work can be confused by this.

The value of x in the invariant comes from the ghost_peek_next method, and I would expect this be convenient for simple ranges, but that the iterator (e.g. iter) would be more useful in the general case. In the long run, I think it would be good to emit a warning or error if someone tries to use x and x isn't provided by the iterator's ghost_peek_next (see point 4 below).

3. Is the trait design restricting us to terminating iterators only? Supporting non-terminating iterators would be important btw. I believe that the current design would support them, but just bringing up a few examples that we should look into to confirm that (eventually when we add the other iterator combinators) would not require a re-design of the ForLoopGhostIterator trait: std::iter::repeat(()).take(10) is terminating, since the repeat is non-terminating (so would just have an arbitrary value in its ghost_decrease), but then the take could make it terminating (by having an actually decreasing value in ghost_decrease). Also (0..10).take_while(|a| a * a < 10) is terminating because even though take_while may or may not be terminating by itself, the 0..10 is terminating.

In principle, the design supports nonterminating iterators, since it allows any invariant and ensures and it makes decreases optional. You could, for example, have a nonterminating iterator ensure false. You could also have iterator combinators supply their own invariants that are, in principle, built out of the iterators that they are combining, and this could, in principle, turn a nonterminating iterator into a terminating iterator. In practice, I don't know how easy it is to compose the invariants and ensures when combining iterators together.

4. For ghost_peek_next, is there a reason that it is not returning an Option<Self::Item> and using .unwrap_or(vstd::pervasive::arbitrary()) or similar in the expansion? That might be a cleaner thing for implementers of the trait to implement. Similar for ghost_decrease. It is possible I'm missing something obvious here btw, so mostly asking for clarification (but I do think modulo a good reason, we might want to put the Options there)

I like this suggestion and I just pushed it in a commit. In the short term, we will just use .unwrap_or(vstd::pervasive::arbitrary()), which just throws away the Option and doesn't really change much. But in the long term, I think we could exploit the Option to insert a check to see that if someone uses the x in for x in ... in one of the invariants, that ghost_peek_next actually returns Some(...).

6. Can we (or indeed even should we) support things like let mut iter = (0..10); for x in iter { ... }, without needing to say for x in iter: iter or similar to be able to access the iter view and such. I don't think this is a common use case though, so it might be fine to even just say "live with the iter: iter" btw.

I'm inclined to just say "live with the iter: iter" for simplicity. Under the hood, things get complicated even in this example, because Rust implicitly calls iter.into_iterator(), which in this case returns the original iterator iter, but in other cases (e.g. for x in v for a Vec v), transforms a non-iterator into an iterator.

[Chris-Hawblitzel]

Could we split Typing into two objects, one passed by & and one passed by &mut, to match the style of the other recursions? That would make the 'state' a lot smaller, so we could just clone it.

My plan is to merge #961 into this just before merging this into main, and squash it all into a single commit. But I'll wait for the remaining reviews first.

[Chris-Hawblitzel]

In principle, the design supports nonterminating iterators, since it allows any invariant and ensures and it makes decreases optional. You could, for example, have a nonterminating iterator ensure false. You could also have iterator combinators supply their own invariants that are, in principle, built out of the iterators that they are combining, and this could, in principle, turn a nonterminating iterator into a terminating iterator. In practice, I don't know how easy it is to compose the invariants and ensures when combining iterators together.

I should also add: this is all just for automatically generating some convenient default invariants and ensures in common cases. If it turns out to be too hard to compose these defaults together for complex iterator combinators, that's ok. We can just have the combinators generate defaults of invariant true, ensures true, etc. and have the user add the real invariants explicitly in the loop.

[utaal-b]

@Chris-Hawblitzel provided some context offline for the translation to loop.
It is now an exact match of the canonical translation in the rust reference (which addresses my concern of potential inconsistencies of treatment of the translation for verification and compilation). Thanks!

[jaybosamiya]

Awesome, lgtm! Looking forward to have for loops in Verus :)