Coming up with loop invariants involving k?
There is a very simple way to determine whether you have the correct loop invariant:

Can you prove that it holds when entering the loop?
Can you prove that the loop maintains it?
Can you deduce correctness of the algorithm using the invariant?

I trust that you can do all these checks yourself.