I'm ready to move forward on this one.  Have improved the assertions, explanations, and variable names.  Hve also added references to show that the foundations are firm.  After tens of millions of trials, I haven't found a single misrounding.  I can't prove "correctly rounded" but am content with "high accuracy".  The speed is comparable to what we had in 3.7, so I think it is a net win all around.