What is the situation just after we discover that rb is negative (to wit -3 if M=8)?
q already holds 3 too many bits of nearly correct quotient.
if q were augmented by (÷ r Nd) it would be exactly correct.
I.e. q+(÷ r Nd) is the exact unrounded quotient to 4 too many places.
We need the left of those bits to do the required round.
The invariant ('Invar) still holds!
That is just what SchemeF computes with s recursion.
<p>
Let x be the low 4 bits of q (q&15).

I really need a hard bound on r!!!!!!!!
<h3>Notation</h3>
floor(x) is the greatest integer not greater than x.
<br>fp(x) = x − floor(x), the fractional part of x.
<br> x = floor(x) + fp(x).
<br> fp(8/3) = ⅔.
<hr>In the beginning 2<sup>52</sup> ≤ df &lt; 2<sup>53</sup> and 2<sup>52</sup> ≤ nf &lt; 2<sup>53</sup>.
For some j, 2<sup>10</sup> ≤ j &lt; 2<sup>11</sup> and j∙2<sup>42</sup> ≤ df &lt; (j+1)∙2<sup>42</sup>.
<br>Enumerating the cases <a href=CC/bnd.c>we find</a> (or <a href=bnd.scm>here</a>) that 0x3fd9200000000000 ≤ Nd &lt; 2<sup>62</sup>.
<br>r &lt; 2<sup>54</sup>.
The code “<tt>lu r = (N*nf)&lt;&lt;ad</tt>” ensures that the high order bit of the quotient appears where we need it and that we compute just enough quotient bits.
<pre>r = (r&lt;&lt;8) - Nd*(r>>54);</pre>
The value (r>>54) is named “nq” in the code.
Since Nd is near 2<sup>62</sup> we can see that this expression nearly cancels, but how closely is the vital question.
<p>The initial r is N∙nf or twice that, and we take the product of their upper bounds as an upper bound for the initial r.
Thus r ≤ 2<sup>10+1+53</sup> = 2<sup>64</sup> — close call.
<p>Here is statistical evidence for bounds we aspire to prove in this sequence of programs: <a href=CC/a2.c>2</a>, <a href=CC/a3.c>3</a> and <a href=CC/a4.c>4</a>.
They are each small textual modifications on <a href=CC/a.c>this short version</a> which works for 10<sup>8</sup> random cases.
Number 4 makes evident that M=8 is at the edge of testing this design in simple C programs on 64 bit computers.
Note the ramifications of the fact that max exceeds 2<sup>39</sup> and thus Nd*nq would require 72 bits to hold properly, were it not for the fact that 8 of those high bits cancel in the subtraction and thus nothing is lost.
<p>I note one possibility that might be considered, but not considered beyond this paragraph.
A bit or two in the table entries for N which would indicate interpreting one or more bits in r to choose nq.
Such might require only a few dozen gates whereas allowing another bit in nq would require hundreds.
Parameter z in some of the code specifies how many more bits of df to consult to choose N.
The code without z has implicitly chosen z to be 2.
Perhaps a better choice would be to set z to 1 and consult an extra bit in r while choosing nq.