Vec::eq does not satisfy it's postcondition

[dewert99]

PartialEq::eq currently has the postcondition result == (@self == @rhs) and Vec::<T>::ModelTy is Seq<T> which implies that Vec::eq should return true iff both vectors have exactly the same elements. Vec::eq is implemented by calling PartialEq::eq on all its elements so it returns true iff both vectors' elements have the same models. This can lead to panics in verified programs a shown below:

use creusot_contracts::*;
struct UnitModel(bool);

impl Model for UnitModel {
    type ModelTy = ();

    #[logic]
    fn model(self) -> Self::ModelTy {
        ()
    }
}

impl PartialEq for UnitModel {
    #[ensures(result == (@self == @other))]
    fn eq(&self, other: &Self) -> bool {
        true
    }
}

#[cfg_attr(not(feature = "contracts"), test)]
fn test() {
    let mut v1 = Vec::new();
    v1.push(UnitModel(true));
    let mut v2 = Vec::new();
    v2.push(UnitModel(false));
    if v1 == v2 {
        assert!(v1[0].0 == v2[0].0)
    }
}

There are a few possible ways to fix:

• Change PartialEq::eq's postcondition to result == (self == rhs)
  • This would make it challenging to have structs with various not identical versions that can often be treated as equivalent (eg. vectors with different capacities, btrees that are balanced differently, hashtables with elements in a different order)
• Change Vec::<T>::ModelTy to Seq<T::ModelTy>
  • This would mean that only who's elements implement Model could be used (All methods are currently specified in terms of models)
  • We would lose information (eg. pushing and popping gives back an identical element not just one with the same model)
• Change Vec::<T>::ModelTy to Seq<T::ModelTy> and intoduce a new logical (returning Seq<T> method to use instead of model)
  • The best way to do this would be to implement Vec::model() as self.new_logic_method().map(|e| e.model()) but this requires logical closures
  • This could make specification for vectors more verbose

Note this also affects slices

[xldenis]

Yea, this is a notion we have called "deep" vs "shallow" models. @jhjourdan and I have agreed that deep models (Seq<T::ModelTy>) are the proper way forward for Model, but we'll also need to introduce a to_seq function with the prior behavior.

You can note that certain types like Option are using the deep approach, but we didn't yet get around to fixing Vec.

Unfortunately, I don't have my computer for the next several weeks, so I cannot implement this fix. I can however review a PR, even from my phone.