Creusot experiments

lib.rs

#![cfg_attr(not(creusot),feature(stmt_expr_attributes,proc_macro_hygiene))]

use ::std::vec;

extern crate creusot_contracts;
use creusot_contracts::*;

#[requires([email protected]() == n@)]
#[ensures(result ==> exists<i0: Int> exists<j0: Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
#[ensures(!result ==> forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < n@ && i0 < j0 && j0 < n@ ==> t@[i0] != t@[j0])]
fn find_duplicate(t: &[i32], n: usize) -> bool {
    let mut b = false;
    let mut i = 0;
    #[invariant(i@ <= n@)]
    #[invariant(b ==> exists<i0 : Int> exists<j0 : Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
    #[invariant(!b ==> forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < i@ && i0 < j0 && j0 < n@ ==> t@[i0] != t@[j0])]
    while i < n {
        let v = t[i];
        let mut j = i + 1;
        #[invariant(i@ < j@ && j@ <= n@)]
        #[invariant(b ==> exists<i0 : Int> exists<j0 : Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
        #[invariant(!b ==> forall<j0 : Int> i@ < j0 && j0 < j@ ==> t@[i@] != t@[j0])]
        #[invariant(!b ==> forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < i@ && i0 < j0 && j0 < n@ ==> t@[i0] != t@[j0])]
        while j < n {
            if v == t[j] {
                b = true;
            }
            j = j + 1;
        }
        i = i + 1;
    }
    b
}

#[requires([email protected]() == n@)]
#[ensures(result == exists<i0: Int> exists<j0: Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
fn find_duplicate2(t: &[i32], n: usize) -> bool {
    let mut b = false;
    let mut i = 0;
    #[invariant(0 <= i@ && i@ <= n@)]
    #[invariant(b ==> exists<i0 : Int> exists<j0 : Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
    #[invariant(!b ==> forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < i@ && i0 < j0 && j0 < n@ ==> t@[i0] != t@[j0])]
    while i < n && !b {
        let v = t[i];
        let mut j = i + 1;
        #[invariant(0 <= i@ && i@ < j@ && j@ <= n@)]
        #[invariant(b ==> exists<i0 : Int> exists<j0 : Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
        #[invariant(!b ==> forall<j0 : Int> i@ < j0 && j0 < j@ ==> t@[i@] != t@[j0])]
        #[invariant(!b ==> forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < i@ && i0 < j0 && j0 < n@ ==> t@[i0] != t@[j0])]
        while j < n && !b {
            if v == t[j] {
                b = true;
            }
            j = j + 1;
        }
        i = i + 1;
    }
    b
}

#[requires([email protected]() == n@)]
#[requires(forall<i: Int> 0 <= i && i < n@ ==> 0 <= t@[i]@ && t@[i]@ < n@)]
#[ensures(result ==> exists<i0: Int> exists<j0: Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
#[ensures(!result ==> forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < n@ && i0 < j0 && j0 < n@ ==> t@[i0] != t@[j0])]
fn find_duplicate3(t: &[usize], n: usize) -> bool {
    let mut u = vec![false; n];
    let mut i = 0;
    #[invariant([email protected]() == n@)]
    #[invariant(0 <= i@ && i@ <= n@)]
    #[invariant(forall<w: Int> 0 <= w && w < n@ ==> u@[w] == exists<i0: Int> 0 <= i0 && i0 < i@ && t@[i0]@ == w)]
    #[invariant(forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < j0 && j0 < i@ ==> t@[i0] != t@[j0])]
    while i < n {
        let v = t[i];
        if u[v] {
            return true;
        }
        u[v] = true;
        i = i + 1;
    }
    false
}