Help proving implementation of kmeans

[nilehmann]

Hi, I'm trying to port this implementation of the K-means clustering algorithm to Creusot, but I'm stuck trying to prove the init_centers function. I'm trying to specify that init_centers returns k vectors of size n, I'm only interested in bounds checking and I don't want to model the f32 inside the inner vectors. I have this so far, but I can't prove the invariant A.

#[requires(k > 0usize)]
#[ensures(forall<j: Int> 0 <= j && j < (@result).len() ==> (@(@result)[j]).len() == @n)]
#[ensures((@result).len() == @k)]
fn init_centers(n: usize, k: usize) -> Vec<Vec<f32>> {
    let mut res: Vec<Vec<f32>> = Vec::new();
    let mut i = 0;
    #[invariant(A, forall<j: Int> 0 <= j && j < (@res).len() ==> (@(@res)[j]).len() == @n)]
    #[invariant(B, i <= k)]
    #[invariant(C, (@res).len() == @i)]
    while i < k {
        res.push(std::vec::from_elem(0.0, n));
        i += 1;
    }
    res
}

It may be related to using f32 because switching that to i32 makes it verify.

Any ideas on how I can verify this function or maybe a different way in which I can write it? Or maybe the specification is all wrong?

Thanks!

[xldenis]

Your function proves for me when I run Split_VC followed by Auto_level_0 (or you can just run Auto_level_3 and it'll work as well).

How are you going about actually doing the proofs?

[nilehmann]

I tried splitting the VC and then auto level 0, but I get a timeout in one of the loop invariants preservations

This is the mlcfg file https://pastebin.com/U23wJvv5

[xldenis]

I proved them using Alt-Ergo, it's generally recommended to have several provers installed. You can get alt-ergo pretty easily through opam: opam install alt-ergo

[nilehmann]

Thanks! that did the trick. I don't know much about why3 so I was alsmot just randomly pressing buttons

[xldenis]

You may be interested in my experimental WhyCode extension which lets you do proofs from vscode. Though, I should warn that it's very alpha