// 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) = 1finalans = 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.

• 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.

• 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[0]+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][0];}