Simplification of "reciprocal word 3by2" (aka invert_pi1)

[Paweł Bylica]

Hello GMP,

First of all thank you for the "Improved division by invariant integers"
paper [1]. It is an excellent source of information for implementing
multi-precision division.

In the implementation of the Algorithm 6 which defines the
RECIPROCAL_WORD_3by2 procedure I noticed a condition I cannot find coverage
for. I am not capable of proving this with math, but I believe the condition

    if (<p, t0> >= <d1, d0>)
        v--;

which in invert_pi1() in gmp-impl.h is implemented as

    if (UNLIKELY (p >= d1))
      {
        if (p > d1 || t0 >= d0)
          v--;
      }

can be simplified to

    if (UNLIKELY (p > d1))
      v--;

The conjecture is that the condition (p == d1 && t0 >= d0) never holds.


I tried to find a counter-example using GMP tests, my unit tests and
fuzzing. So far unsuccessfully.
The GMP tests seem to be lacking coverage in general. I was not able to
find a sample to hit the case of (p == d1).

Bests,
Paweł

[1] https://gmplib.org/~tege/division-paper.pdf