Help with Zip iterator

[boulme]

Hello,

Still playing with my_reverse variants after your answer in this other thread, I tried with this simple version combining only range and zip iterators:

#[ensures((^slice)@.ext_eq(slice@.reverse()))]
fn my_reverse<T>(slice: &mut [T]) {
    let n = slice.len();
    let old_v: Ghost<&mut [T]> = gh! { slice };
    #[invariant(n@ == slice@.len())]
    #[invariant(equiv_range(slice@, old_v@, produced.len(), n@-produced.len()))]
    #[invariant(equiv_reverse_range(slice@, old_v@, 0, produced.len(), n@-1))]
    #[invariant(equiv_reverse_range(slice@, old_v@, n@-produced.len(), n@, n@-1))]
    for (i,j) in (0..n/2).zip(0..n/2) { slice.swap(i, n-j-1); }
}

And I get the following error message:
error[E0277]: the trait bound std::iter::Zip<std::ops::Range, std::ops::Range>: creusot_contracts::Iteratoris not satisfied

After that, I tried to copy-paste your specification of the Zip iterator in my file, but did not succeed to integrate it. Is there a simple workaround ?

[boulme]

Here are more details on my issues. I have started to rebuild iterators from scratch by copy-pasting the examples of creusot/tests.

First, my variant for (i,j) in (0..n/2) { slice.swap(i, n-i-1); } is "desugared" into the code below, which works well:

#[ensures((^slice)@.ext_eq(slice@.reverse()))]
fn my_reverse_range<T>(slice: &mut [T]) {
    let n = slice.len();
    let old_v: Ghost<&mut [T]> = gh! { slice };
    let mut it = Range { start: 0, end: n/2 }.into_iter();
    let iter_old = gh! { it };
    let mut produced = gh! { Seq::EMPTY };
    
    #[invariant(inv(it))]
    #[invariant(iter_old.produces(produced.inner(), it))]
    /* real invariant */
    #[invariant(n@ == slice@.len())]
    #[invariant(equiv_range(slice@, old_v@, produced.len(), n@-produced.len()))]
    #[invariant(equiv_reverse_range(slice@, old_v@, 0, produced.len(), n@-1))]
    #[invariant(equiv_reverse_range(slice@, old_v@, n@-produced.len(), n@, n@-1))]
    loop {
        match it.next() {
            Some(i) => {
                produced = gh! { produced.concat(Seq::singleton(i)) };
                slice.swap(i, n-i-1);
            }
            None => break,
        }
    }
}

However, I do not succeed to achieve the for (i,j) in (0..n/2).zip(0..n/2) version in the same way. I wonder if this is related with your mysterious comment in your Zip iterator, that I quote here: "Using an unzip definition doesn't work well because of issues related to datatypes and match". For the record, here is my full attempt: main.rs.gz. Any suggestion or explanation is welcome ;-)

[jhjourdan]

The main problem is that we need to specify Zip in the creusot-contract crate. For this, we need to copy-paste the specification proven in the tests, but there is an issue : in the tests, we can have access to the fields of the Zip struct, which is impossible for stdlib's zip (they are private fields). So we need to create logic function to model these fields....

All this is not fundamentally difficult, but quite a bit of boilerplate.

[boulme]

Thanks for your answer. Yes, I have an idea of how the Zip iterator could be modeled. But when I am trying to do it myself, I am struggling with an issue! Inspired by your Tacas'23 proposal to use ghost fields in data-structures that are client of iterators, I started to model Zip as:

struct Zip<I: Iterator, J: Iterator> {
    iter1: I,
    iter2: J,
    produced1: Ghost<Seq<I::Item>>, 
    produced2: Ghost<Seq<J::Item>>,
}

impl<I: Iterator, J: Iterator> Iterator for Zip<I, J> {
    type Item = (I::Item, J::Item);

   // ...
    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
        pearlite! {
           self.iter1.produces(self.produced1.inner(), tl.iter1) && self.iter2.produces(self.produced2.inner(), tl.iter2) &&
           self.produced1.inner().len() == visited.len() && self.produced2.inner().len() == visited.len() &&
           (forall<i :_> 0 <= i && i < visited.len() ==>
                visited[i] == (self.produced1.inner()[i], self.produced2.inner()[i]))
        }
    }

    //..
    fn next(&mut self) -> Option<Self::Item> {
        match (self.iter1.next(), self.iter2.next()) {
            (Some(i1), Some(i2)) => {
                self.produced1=gh! { self.produced1.inner().concat(Seq::singleton(i1)) };
                self.produced2=gh! { self.produced2.inner().concat(Seq::singleton(i2)) };
                Some((i1, i2))
            },
            _ => None,
        }
    }

Unfortunately, I get this error message from creusot:

error[creusot]: associated types are unsupported in type declarations
   --> src/main.rs:165:5
    |
165 |     produced1: Ghost<Seq<I::Item>>, 
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It is difficult to understand, because some simplistic examples with ghost field in type declarations seem well-supported. Here is my attempt: main.rs.gz

[jhjourdan]

The problem is that associated types (like I::Item in the definition of Zip) are not allowed in type declarations. This is due to the way they are translated to Why3. @xldenis has some plans to fix this issue.

But anyway, you don't need these ghost fields for the specification of Zip. The reason we add such a ghost field for Map is that it can be used for the invariant of the closure. But there is no such closure in Zip.

[xldenis]

Indeed, I need to rebase and merge #808 which would add support for associated types in fields.

[jhjourdan]

See #862 for a specification of Zip, and a session with your example. It passed on the first try !

[boulme]

Great! Thanks a lot!
I have looked at your commit, and the specification of Zip looks similar to the one of my first attempt above which failed. I have tried the ghost field approach, because I (wrongly) suspected an issue of SMT-solvers with exists quantifier. Your solution shows that the issue was more probably in my desugaring of the for-loop and its associated implicit invariants.

[xldenis]

@boulme in the root of the creusot repository we have an expand script which you can use to print the output of the desugaring.

./expand my_rust.rs will dump the rust code provided by macro expansion (including for loops). Note: you must provide an invariant (even if it is just true) for this to work as that is the actual macro call.

[boulme]

Great! I will try it !

[xldenis]

it can be rather finicky to use, but it should give a correct expansion if you previously compiled creusot_contracts with creusot (either by running ./mlcfg or cargo test --test ui. It's really a personal debugging tool :)