Unwanted revert in WadRayMath library

[MichaelMorami]

summary

rayDiv and wadDiv revert too eagerly due to an explicit check written in assembly: LINK
Although true only for very large numbers, the functions revert in cases where mathematically a, b should be acceptable, but in practice, they aren't due to the heuristic used in the implementation.
The check can be seen in the specification written here, and the results can be seen here

Detailed explanation

wadDiv and rayDiv functions in the WadRayMath.sol library revert if and only if the following solidity functions return the value true:

function wadDivRevertingSolidity(uint256 a, uint256 b) public pure returns (bool d) {
    if (b != 0)
    {
        d =  (a > ((type(uint256).max - b/2)/WAD));
    } else {
        d = true;
    }
    return d;
  }

function wadRayRevertingSolidity(uint256 a, uint256 b) public pure returns (bool d) {
    if (b != 0)
    {
        d =  (a > ((type(uint256).max - b/2)/RAY));
    } else {
        d = true;
    }
    return d;
  }

this can be verified via the equivalence checking rules in the prover:

• specification
• result

However, this is a logic bug: if we treat a, b as uint256 and consider wadDiv for a moment, then as soon as a > MAX_UINT256/(2 *WAD) we have a*WAD>MAX_UINT256/2, so we can find a very large b <= MAX_UINT256 which would cause a "ghost overflow" in the computation. Nevertheless, it is very possible for a/b*WAD to still give a valid result. (i.e., both a and b can be very large! but their quotient can be small...).

Running an equivalence check produces the counterexample in the image (you can also see in the links of the result above).

After converting these values to decimal, we get:
104212880313584575881213886507819117067942986199076507635512000000000000000000 / 23158417847463239084714197001737581570653996933128112807891555555555555555556 = 4
so the solidity version reverts even though it shouldn't.