Unsound verification when cloning vector elements

[nokunish]

Verifying the properties of a vector after cloning its elements cause unsoundness.

For instance, given an element,

struct Elem<T> 
    where T: Copy        
{
    val: T,
    next: usize
}

Verifying the field next, in which we don't clone, will cause the error,

fn push<T>(init: T) 
    where T: Copy
{

    let mut vec:Vec<Elem<T>> = Vec::new();

    let mut i = 0;

    prusti_assert!( i < vec.len() ==> 
        (*SliceIndex::index(i, &vec)).next == 0
    );

    vec.push(Elem {val: init.clone(), next: 0});
}

Error message:

Details: consistency error in prusti_test::test_v1::code::debug::debug::push: Consistency error: DomainType references non-existent domain Snap$__TYPARAM__$_T$0$__. (<no position>)

However, all four of the below will get verified successfully:

1. Verifying the cloned val field instead

fn push<T>(init: T) 
    where T: Copy
{

    let mut vec:Vec<Elem<T>> = Vec::new();

    let mut i = 0;
    
    prusti_assert!( i < vec.len() ==> 
        (*SliceIndex::index(i, &vec)).val === init
    );

    vec.push(Elem {val: init.clone(), next: 0});
}

2. Verifying the cloned val field before / after verifying the next field

fn push<T>(init: T) 
    where T: Copy
{

    let mut vec:Vec<Elem<T>> = Vec::new();

    let mut i = 0;
    
    prusti_assert!( i < vec.len() ==> 
        (*SliceIndex::index(i, &vec)).val === init
    );

    prusti_assert!( i < vec.len() ==> 
        (*SliceIndex::index(i, &vec)).next == 0
    );

    vec.push(Elem {val: init.clone(), next: 0});
}

3. clone the value first, before calling push

fn push<T>(init: T) 
    where T: Copy
{

    let mut vec:Vec<Elem<T>> = Vec::new();

    let mut i = 0;
    let val = init.clone();

    prusti_assert!( i < vec.len() ==> 
        (*SliceIndex::index(i, &vec)).next == 0
    );

    vec.push(Elem {val, next: 0});
}

4. if we don't clone (which is possible in this case since we implemented Copy)

fn push<T>(init: T) 
    where T: Copy
{

    let mut vec:Vec<Elem<T>> = Vec::new();

    let mut i = 0;

    prusti_assert!( i < vec.len() ==> 
        (*SliceIndex::index(i, &vec)).next == 0
    );

    vec.push(Elem {val: init, next: 0});
}

Also, providing the post-condition,

#[ensures(
        *SliceIndex::index(&self, self.len() - 1) === value
    )]
pub fn push(&mut self, value: T);

in the external specification seems to fix the issue (but providing post-conditions that does not reference value has no effect), which I'm not sure why?

[fpoli]

Thanks for the report. Could you provide a full example with the specification of SliceIndex?