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

[Paul Zimmermann]

       Dear Pawel,

your conjecture is false. I wrote a small program using SageMath and found
the smallest counter-example with beta=128, d1=67 and d0=90.

Before line 14 of Algorithm reciprocal_word_3by2 one gets p=67 and t0=110.

For beta=256 I found 3 counter-examples, and 7 for beta=512.

Best regards,
Paul Zimmermann

> From: Paweł Bylica <chfast at gmail.com>
> Date: Fri, 19 Jun 2020 11:38:33 +0200
> 
> 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
> _______________________________________________
> gmp-discuss mailing list
> gmp-discuss at gmplib.org
> https://gmplib.org/mailman/listinfo/gmp-discuss