I am trying to write a proof using a loop invariant for an algorithm that I wrote, where A is the array and v is the value being searched for:

bSearch(A, v) {

return binarySearch(A, 0, length(A)-1, v)

}

binarySearch(A, l, r, v) {

if l >= r:

return -1

p = l+(r-1)/2

if A[p] == v:

return p

if A[p] < v

return binarySearch(A, p-1, r, v)

else return binarySearch(A, l, p-1, v)

}

I am having trouble determining what the loop invariant is. I understand that the loop comes from the recursive nature of the algorithm, and I believe the loop invariant has something to do with the value of p, and the sequence of if statements. I also know that p is the value being returned, and that it is the index where v is found. Any insight on the specifics of the identity loop invariant/ what line it is on would be awesome. Thank you!