Summary

Incorrect implementation of overflow protection in MathMasters::mulWadUp dilutes the intended safety check against overflow, so that certain non-overflow multiplication operations get treated as if they were overflows (false positives).

Vulnerability Details

The following line of code

is supposed to be a safety check designed to prevent multiplication overflow when performing fixed-point arithmetic. Although the comment above it describes a correct overflow check, the assembly code implementation is incorrect.
The or operation performs a bitwise OR between div(not(0), y) and x, combining the bits of x and the safe maximum multiplier for y. This does not make logical sense in the context of assessing the risk of multiplication overflow: since or(div(not(0), y), x)) >= x, the inclusion of the OR operation effectively dilutes the intended safety check against overflow, resulting in false positives.

Example: using uint64 instead of uint256 for simplicity, mulWadUp incorrectly throws an overflow error (in uint64 context) for x = 3008292032 (0xb34ee4c0) with y = 2991730824 (0xb2523088).

Impact

The flawed logic may erroneously treat certain non-overflow multiplication operations as if they were overflows, leading to unnecessary transaction reverts.
Such false positives in overflow detection not only compromise the contract's operational integrity but also could lead to a loss of user trust and potential financial disruptions for applications depending on the contract's accurate execution of arithmetic operations.

Tools Used

Halmos, ChatGPT

Recommendations

Correct the overflow safety check, e.g.

(This correct version is being used in `mulWad˛.)