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

[Paweł Bylica]

Thanks for checking this out Paul.

Are you able to generate any counter-example for beta=2^64?

On Fri, Jun 19, 2020 at 2:21 PM Paul Zimmermann <Paul.Zimmermann at inria.fr>
wrote:

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