Iterative Fibonacci algorithm correctness proof, finding loop invariants The algorithm take in an integer $n$ and outputs the $n$th number in the Fibonacci sequence ($F_n$). The sequence starts with $F_0$. I am trying to prove the correctness assuming valid input:

int Fib(int n) {
    int i = 0;
    int j = 1;
    int k = 1;
    int m = n;
    while(m &gt;= 3){
        m = m-3;
        i = j +k;
        j = i+k;
        k = i + j;
    }
    if(m == 0 ){
        return i;
    }
    else{
        if(m == 1){
            return j;
        }
        else{
            return k;
        }
    }
}


For a reminder, a loop invariant is a claim which holds every time just before the loop condition is checked. It holds even when the loop condition is false. I've established and proven one loop invariant that $m \geq 0$. This helps me show that the algorithm terminates since when the loop exits since $m$ is either 0, 1, or 2. However, I'm stuck on finding another loop invariant that would help me show that the algorithm produces the correct Fibonacci number. 

One pattern I found is that the result of returning i, j, or k is due to the result of the initial value of $m$ $\% 3$. Depending on the remainder, either i, j, or k is returned. I tried expanding this idea further but led myself to a dead end. I'm thinking I need to find some way to express $F_n = F_{n-1} + F_{n-2}$ in terms of i, j and k in order to prove that the program outputs correctly. Am I on the right track with remainders or is there something I'm missing?
It kind of depends on what formalism you want to use for this proof.. But the core-idea which holds for pretty much any such formalism is the following:

Suppose you establish some invariant $I$ you will want to be able to make the following conclusion

$$
m &lt; 3 \land I \implies X
$$

where $X$ tells you that the values $i,j$ and $k$ have the right values.

You are on the right track with the argument $I = I' \cup \{ m = n \mod 3 \}$, however $I' = \{m \geq 0\}$  is way too weak to establish that $\texttt{Fib}(n)$ returns the $n$th Fibonacci number.



Try the following: 


Find some existential (for some value, eg. $z$) claim about the relationship of $n$ and $m$ (seems like you already did so)
Now use that value $z$ to show $\{ k = F_z, i = F_{z-2}, j = F_{z-1} \}$1


I hope this will help you!

1: Depends on your claim about $m$ and $n$, could also be shifted $\{ k = F_{z+2}, i = F_z, j = F_{z+1} \}$ as in gnasher729's answer which is simpler. The core idea is the same.