True But Not Enough

This is the standard binary search skeleton, searching for x in a sorted array A[0..n):

int binsearch(int x, int[] A, int n) {
  int lo = 0;
  int hi = n;
  while (lo < hi) {
    int mid = lo + (hi - lo) / 2;
    if (A[mid] == x) return mid;
    else if (A[mid] < x) lo = mid + 1;
    else hi = mid;
  }
  return -1;
}

Which loop invariant is both always true and strong enough to prove that returning -1 means x is absent?