Cannot prove 02_linear_search.rs

[southball]

This is my current proof:

// Prove the following:
// 1. If we return Some(i) it is the first index containing `tgt`
// 2. If we return None, then there are no indices containing `tgt`
#[requires(forall<a: T, b: T> a == b ==> a@ == b@)]
#[requires(forall<a: T, b: T> a != b ==> a@ != b@)]
#[requires(forall<a: T, b: T> a@ == b@ ==> a == b)]
#[requires(forall<a: T, b: T> a@ != b@ ==> a != b)]
#[ensures(result == None ==> forall<i: Int> i >= 0 && i < v@.len() ==> (v@[i])@ != (*tgt)@)]
#[ensures(forall<x: usize> result == Some(x) ==> forall<i: Int> i >= 0 && i < x@ ==> (v@[i])@ != (*tgt)@)]
#[ensures(forall<x: usize> result == Some(x) ==> (v@[x@])@ == (*tgt)@)]
fn search<T: Ord + ShallowModel<ShallowModelTy = T> + DeepModel>(v: &Vec<T>, tgt: &T) -> Option<usize>
where
    T::DeepModelTy: OrdLogic {
    let mut i = 0;

    #[invariant(forall<j: Int> j >= 0 && j < i@ ==> (v@[j])@ != (*tgt)@)]
    #[invariant(i@ >= 0 && i@ <= v@.len())]
    while i < v.len() {
        if v[i] == *tgt {
            proof_assert!(i@ >= 0 && i@ < v@.len());
            proof_assert!((v@[i@])@ == (*tgt)@);
            return Some(i);
        }

        i += 1
    }

    return None;
}

The line proof_assert!((v@[i@])@ == (*tgt)@); cannot be proved.

[xldenis]

Thanks for trying out Creusot! Unfortunately you stumbled into one of the most poorly named set of traits.

I've attached a fixed version of your specs below as a reference.

The short version of the issue: when reasoning about rust equality or orders use DeepModel ( soon to be called EqModel). The ShallowModel trait which should be called View is just a convenient shorthand for viewing types like Vec as their mathematical model. It is _unprincipled _ and it shouldn't occur in bounds.

extern crate creusot_contracts;
use creusot_contracts::*;
// Prove the following:
// 1. If we return Some(i) it is the first index containing `tgt`
// 2. If we return None, then there are no indices containing `tgt`
#[ensures(result == None ==> forall<i: Int> i >= 0 && i < v@.len() ==> v[i].deep_model() != tgt.deep_model())]
#[ensures(forall<x: usize> result == Some(x) ==> forall<i: Int> i >= 0 && i < x@ ==> v[i].deep_model() != tgt.deep_model())]
#[ensures(forall<x: usize> result == Some(x) ==> v[x@].deep_model() == tgt.deep_model())]
fn search<T: Ord + ShallowModel<ShallowModelTy = T> + DeepModel>(v: &Vec<T>, tgt: &T) -> Option<usize>
where
    T::DeepModelTy: OrdLogic {
    let mut i = 0;

    #[invariant(forall<j: Int> j >= 0 && j < i@ ==> v[j].deep_model() != tgt.deep_model())]
    #[invariant(i@ >= 0 && i@ <= v@.len())]
    while i < v.len() {
        if v[i] == *tgt {
            proof_assert!(v[i@].deep_model() == tgt.deep_model());
            return Some(i);
        }

        i += 1
    }

    return None;
}