Help with the predefined seq.reverse and seq.subsequence

[boulme]

Hello,

I succeed to prove this little example:

#[predicate]
fn equiv_range<T>(s1: Seq<T>, s2:Seq<T>, l: Int, u: Int) -> bool {
    pearlite! {
        forall<i : Int> l <= i && i < u ==> s1[i] == s2[i]
    }
}

#[predicate]
fn equiv_reverse_range<T>(s1: Seq<T>, s2:Seq<T>, l: Int, u: Int, n: Int) -> bool {
    pearlite! {
        forall<i : Int> l <= i && i < u ==> s1[i] == s2[n-i]
    }
}

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

But, if I failed to prove the following variant, using predefined operations on sequences instead of my own predicates:

#[ensures((^slice)@ == (slice@).reverse())]
fn my_reverse2<T>(slice: &mut [T]) {
    let n = slice.len();
    let old_v: Ghost<&mut [T]> = gh! { slice };
    let mut i = 0;
    #[invariant(n@ == slice@.len())]
    #[invariant(slice@.subsequence(i@, n@-i@) == old_v@.subsequence(i@, n@-i@))]
    #[invariant(slice@.subsequence(0, i@) == old_v@.reverse().subsequence(0, i@))]
    #[invariant(slice@.subsequence(n@-i@, n@) == old_v@.reverse().subsequence(n@-i@, n@))]
    while i < n/2 {
        slice.swap(i,n-i-1);
        i+=1
    }
}

It seems that invariant preservation on subsequences cannot be proved. (When, I replace the above "==" over sequences by "ext_eq", all invariant initializations are proved, but no preservation yet). Sorry, I am still not used to interactive proof debugging with why3. Thus, I do not understand what is happening here.

Another question on this example: if we use a for i in 0..n/2 { slice.swap(i, n-i-1) } instead of a while, how are we supposed to express the invariants over i at the top of the loop (since the i is now in the scope of the loop) ? (Got "cannot find value i in this scope" when I tried).

[boulme]

Actually, I would also like to play with this other variant, purely based on (mutable) iterators:

use std::mem::swap;
fn my_reverse<T>(slice: &mut [T]) {
    let (left, right) = slice.split_at_mut(slice.len()/2);
    for (l, r) in left.iter_mut().zip(right.iter_mut().rev()) {
        swap(l, r)
    }
}

Do you think possible to reason on such a combination of iterators in Creusot ?

[xldenis]

those operations are all supported, the real question will be finding the invariant which expresses the desired property.

[xldenis]

It seems that invariant preservation on subsequences cannot be proved. (When, I replace the above "==" over sequences by "ext_eq", all invariant initializations are proved, but no preservation yet). Sorry, I am still not used to interactive proof debugging with why3. Thus, I do not understand what is happening here.

Likely you are facing issues with SMT, they can be quite sensitive to formulation of properties. I'll take a look now.

[xldenis]

The first invariant can be proved with the help of the following lemma:

#[ghost]
#[requires(l + 1 <=  u -1)]
#[requires(s.len() == t.len())]
#[requires(0 <= l && l <= u && u <= s.len())]
#[requires(s.subsequence(l, u) == t.subsequence(l, u))]
#[ensures(s.subsequence(l + 1, u - 1) == t.subsequence(l + 1, u - 1))]
fn restrict_subseq<T>(s : Seq<T>, t : Seq<T>, l : Int, u : Int) {}

We have no lemmas available on reverse which makes it relatively unsurprising that we can not prove anything useful as a result.

[xldenis]

Here is a (nearly) complete proof session, I was able to prove all the invariants, though it was often pretty tricky for extensionality issues. The only missing property is the postcondition which needs a glue lemma like:

#[ghost]
#[requires(0 <= k && k < s.len())]
#[ensures(s.reverse() == s.subsequence(k, s.len()).reverse().concat(s.subsequence(0, k).reverse()))]
fn reverse_cat<T>(s : Seq<T>, k : Int) {}

unfortunately, I don't think this is general enough (need something about odd-length sequences)

Archive.zip

[boulme]

Thanks a lot. Your trick of using ghost code to make the proof progress is cute: it reminds me Coq :).
And this shows me how to prove the invariants based on subsequence with postcondition, modulo one single admitted fact:

 // admitted !
#[ghost]
#[requires(0 <= l && l <=  u && u <= s.len() && u <= t.len())]
#[requires(s.subsequence(l, u).ext_eq(t.subsequence(l, u)))]
#[ensures(equiv_range(s,t,l,u)) ]
fn subseq_equiv_range<T>(s : Seq<T>, t : Seq<T>, l : Int, u : Int) { }

But, I needed to use ext_eq instead of == on sequences. And the version with subsequence in invariants induced a lot of pain (i.e. ghost code to help the proof). See main.rs.gz

Finally, my first version above is the simplest one. Moreover, it still works without change for this nice specification:

#[ensures((^slice)@.ext_eq(slice@.reverse()))]
fn my_reverse<T>(slice: &mut [T]) 

[xldenis]

Another question on this example: if we use a for i in 0..n/2 { slice.swap(i, n-i-1) } instead of a while, how are we supposed to express the invariants over i at the top of the loop (since the i is now in the scope of the loop) ? (Got "cannot find value i in this scope" when I tried).

This is a tricky thing about for loops in rust: what if the first call returns None? What value can we give i? Our approach is instead to use produced to refer to it, indirectly.

[boulme]

Desugaring your answer, here is a simple recipe for this simple example, i.e. with an integer loop variable i.
Recipe: the loop invariant of the for simply corresponds to the invariant of the while, where i@ has been replaced by produced.len(). Hence, we get:

#[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 in 0..n/2 { slice.swap(i, n-i-1); }
}