Proving loop termination with an addition

[ROMemories]

I am trying to prove that the following function does not panic (as a helper function because hax does not currently support Iterator::position()):

fn position<const N: usize>(slice: &[u8; N], needle: u8) -> Option<usize> {
    let mut i = 0;
    while i < N && slice[i] != needle {
        i += 1;
    }
    if i < N {
        Some(i)
    } else {
        None
    }
}

view in hax playground

My understanding is that there are three things to prove in this function:

• That the array indexing does not panic (i.e., i < N).
• That the addition does not overflow.
• That the loop terminates.

Later, I could try proving that the function actually returns the correct index, but this is out of scope.

F* typechecking currently fails on the addition's rhs, but I could use a hint about whether this is because the addition cannot be proven overflow-free and how to prove this correctly (I would also be fine with assumeing things here, as I expect this to be temporary).

[maximebuyse]

Our model for while loops is not very usable at the moment. You could use an assume (for example with i < N) to show that the addition doesn't overflow. But you would not be able to prove termination anyway.

We are currently working on an improvement on this in #1375 . you can check this playground that uses this branch and adds an annotation to prove termination and an invariant for the loop.