## § Binary search to find rightmost index which does not possess some property

// p for predicate/property
// precondition: p(0) = false
// precondition: p(1 << NBITS) = last ix we process.
// precondition: p is monotonic;
//   once it switches to true, does not switch back to false.

if (p(1 << NBITS) == 0) { return 1 << NBITS; }
else {
assert(p(1<<NBITS) == 1);
int ans = 0;
for (int i = NBITS-1; i >= 0; i--) {
int k = 1 << i;
assert(p(ans + 2*k) == 1);
if (p(ans + k) == 0) {
ans = ans + k;
}
}
}
// postcondition:
// ans is largest index such that
// has_some_poperty(ans) = 0

• Claim 1: (Correctness) p(ans[i]) = 0. By precondition, this is true before the loop. See that it's a loop invariant, as we only update ans[i] to ans[i]+k if p(ans[i]+k) = 0. Thus, is is true after the loop.
• Claim 2: (Maximality) : At loop iteration i: p(ans[i] + 2k[i]) = 1. We cannot improve our solution by using previous jump lengths.
This implies optimality once the loop ends. At the end of the loop we have i = -1. So:
2k[-1] = 2(1/2) = 1
finalans = ans[-1]
---
p(ans[-1] + 2k[-1]) = 1
=> p(finalans+1) = 1

• Proof of Claim 2: induction on i
• Suppose claim 2 is true till index i: p(ans[i] + 2k[i]) = 1.
• To prove: induction hypothesis holds at index (i-1).
• Case analysis based on loop body at i: p(ans[i] + k[i]) = 0 or 1
• (a) p(ans[i] + k[i]) = 0. We update ans[i-1] = ans[i] + k[i].
• We wish to show that the loop invariant holds at i-1: p(ans[i-1]+2k[i-1]) == 1.
\begin{aligned} &\text{k value: } k[i] = 2^i \\ &\text{(k-1) value: } k[i-1] = 2^{i-1} = 2k[i] \\ &\text{Ind: } p(ans[i] + 2k[i]) = 0 \\ &\text{Case (a): } p(ans[i] + k[i]) = 0 \\ &\text{Update: } ans[i-1] \equiv ans[i] + k[i] \\ &p(ans[i-1] + 2k[i-1]) \\ &= p((ans[i] + k[i]) + 2k[i-1]) \\ &= p(ans[i] + k[i] + k[i])\\ &= p(ans[i] + 2k[i]) \\ &= 1 ~\text{(By Induction Hyp.)} \end{aligned}
• We've shown that the induction hypothesis hold at index $(i-1)$ in case (a) where we update the value of $ans[i]$.
• (b) If p(ans[i] + k[i]) = 1, then we update ans[i-1] = ans[i].
• We wish to show that the loop invariant holds at i-1: p(ans[i-1]+2k[i-1]) ==1.
\begin{aligned} &\text{k value: } k[i] = 2^i \\ &\text{(k-1) value: } k[i-1] = 2^{i-1} = 2k[i] \\ &\text{Ind: } p(ans[i] + 2k[i]) = 0 \\ &\text{Case (b): } p(ans[i] + k[i]) = 1 \\ &\text{Update: } ans[i-1] \equiv ans[i] \\ &p(ans[i-1] + 2k[i-1]) \\ &= p(ans[i] + 2k[i-1]) \\ &= p(ans[i] + k[i] + k[i])\\ &= p(ans[i] + 2k[i]) \\ &= 1 ~\text{(By Induction Hyp.)} \end{aligned}
• We've shown that the induction hypothesis hold at index $(i-1)$ in case (b) where we don't change the value of $ans[i]$.
• In summary, the loop invariant is held at index $(i-1)$ assuming the loop invariant is satisfied at index $(i)$, for both updates of $ans[i]$. Thus, by induction, the loop invariant holds for all iterations.
• Elaborated proof of why p(ans+1) = 1 at the end of the loop
See that we can insert a new invaraiant at the end of the loop which asserts p(ans[i]+k[i]) == 1:
if (p(1 << nbits) == 0) { return 1 << nbits; }
else {
assert(p(1<<nbits) == 1);
int ans = 0;
for (int i = nbits-1; i >= 0; i--) {
int k = 1 << i;
assert(p(ans + 2*k) == 1);
int ans2;
if (p(ans + k) == 0) {
ans2 = ans + k;
// ans2 + k
// = (ans + k) + k
// = ans + 2k
// = 1 (from assertion)
} else {
ans2 = ans;
// ans2 + k
// = ans + k
// = 1 [from else branch]
}
// ## new loop end invariant ##
// true from then, else branch.
assert(p(ans2+k) == 1)
ans = ans2;
}
}

• We've proven the correctness of the loop invariant at the end of the loop, given the prior loop invariant at the beginning of the loop.
• So, At the end of the (i=0) iteration, we have k=1, and so p(ans+1) == 1, which is the "rightmost index" condition. that we originally wanted.

#### § Fully elaborated proof

if (p(1 << nbits) == 0) { return 1 << nbits; }
else {
assert(p(1<<nbits) == 1);
int ans = 0;
// p(ans[nbits-1] + 2*(1<<nbits-1))
// = p(0 + 1 << nbits)
// = p(1 << nbits)
// = 1 [from assert]
for (int i = nbits-1; i >= 0; i--) {
int k = 1 << i;
// From previous loop iteratio (i+1):
// ---------------------------------
// p(ans[(i+1)-1] + k[i+1]) == true
// => p(ans[i] + k[i+1]) == true
// => p(ans[i] + 2k[i]) == true
assert(p(ans + 2*k) == true);

if (p(ans + k) == 0) {
ans += ans + k;
// ASSIGNMENT: ans[i-1] = ans[i] + k[i]
// p(ans[i-1] + k[i])
// = p(ans[i] + k[i] + k[i])
// = p(ans[i] + 2k[i])
// = p(ans[i] + k[i+1])
// = 1 (from induction hyp)
} else {
ans = ans; // no-op
// ASSIGNMENT: ans[i-1] = ans[i].
// p(ans[i-1] + k[i])
// = p(ans[i] + k[i])
// = 1 (from else branch)
}
// ## new loop end invariant ##
// p(ans[i-1] + k[i])== 1
assert(p(ans+k) == 1)
}
}


#### § Simplified implementation

If we are willing to suffer some performance impact, we can change the loop to become significantly easier to prove:
if (p(1 << nbits) == 0) { return 1 << nbits; }
else {
assert(p(1<<nbits) == 1);
int ans = 0;
int i = nbits-1;
while(i >= 0) {
assert (p(ans+2*k) == 1);
int k = 1 << i;
if (p(ans + k) == 0) {
ans += ans + k;
} else {
i--;
}
assert(p(ans) == 0)
}
}

In this version of the loop, we only decrement i when we are sure that p(ans+k) == 0. We don't need to prove that decrementing i monotonically per loop trip maintains the invariant; Rather, we can try "as many is as necessary" and then decrement i once it turns out to not be useful.

#### § Relationship to LCA / binary lifting

This is very similar to LCA, where we find the lowest node that is not an ancestor. The ancestor of such a node must be the ancestor.
int lca(int u, int v) {
if (is_ancestor(u, v)) return u;
if (is_ancestor(v, u)) return v;

// u is not an ancestor of v.
// find lowest parent of u that is not an ancestor of v.
for (int i = l; i >= 0; --i) {
if (!is_ancestor(up[u][i], v))
u = up[u][i];
}
return up[u];
}