vstd: add specification to Vec::retain

[bsdinis]

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

[Chris-Hawblitzel]

This one took me a while to work through, but I think there are two challenges that make Vec::retain tricky to specify. First, the exec function f can be nondeterministic, whereas Seq::filter deals with deterministic spec functions. Consider the vector [10, 20, 10]. Suppose that f retains the first 10, retains the 20, and drops the last 10, returning [10, 20]. There's no deterministic spec function we could pass to Seq::filter that would replicate this behavior. So I think you'll need a version of Seq filter that works based on index rather than value, so that in this case it can retain index 0, retain index 1, and drop index 2.

Second, the idiom we usually use with .ensures is ensures exists|ret| f.ensures(args, ret) && ...something about ret.... Intuitively, this means "we called f and it returned some ret such that ...something about ret...". If you only talk about the true return value, as in f.ensures((&t, ), true), clients will be unable to prove some results:

fn ft(u: &u8) -> (b: bool) ensures b { true }
fn ff(u: &u8) -> (b: bool) ensures !b { false }

fn test_t() {
    reveal_with_fuel(Seq::filter, 2);

    let mut v: Vec<u8> = vec![10];
    v.retain(ff);
    assert(!ff.ensures((&10, ), true));
    assert(v@ =~= seq![]);

    let mut v: Vec<u8> = vec![10];
    v.retain(ft);
    //assume(ft.ensures((&10, ), true));
    assert(v@ =~= seq![10]); // FAILS without assume
}

So you may have to use something like:

    ensures
        exists|fs: spec_fn(int) -> bool| {
            &&& forall|i: int| 0 <= i < old(vec).len() ==> f.ensures((#[trigger] &old(vec)@[i], ), fs(i))
            &&& vec@ == ... something to filter old(vec) using fs ...
        },

if you want to use some sort of Seq filter function to calculate the new vec.

[bsdinis]

Oof, that is a great point. I wonder if it's worth it to specify it as is or whether we should find a better way to convert (deterministic) exec functions into spec functions. I presume all the work on the iterators would also want to enable the combinators that depend on closures? @parno what do you think?

[tjhance]

I think it would be really great to have like an is_pure() function on fn types. This would need a buncha design work though.

[parno]

I presume all the work on the iterators would also want to enable the combinators that depend on closures? @parno what do you think?

Yes, at the moment, there's a complicated implementation for such combinators based on prophetic sequences (see the prototype), but if we knew the closures were pure, we could potentially have a simpler "happy case" for those instances.