@@ -321,53 +321,23 @@ function exp2(uint256 x) pure returns (uint256 result) {
321321/// @return result The index of the most significant bit as a uint256.
322322/// @custom:smtchecker abstract-function-nondet
323323function msb (uint256 x ) pure returns (uint256 result ) {
324- // 2^128
325324 assembly ("memory-safe" ) {
326- let factor := shl (7 , gt (x, 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF ))
327- x := shr (factor, x)
328- result := or (result, factor)
329- }
330- // 2^64
331- assembly ("memory-safe" ) {
332- let factor := shl (6 , gt (x, 0xFFFFFFFFFFFFFFFF ))
333- x := shr (factor, x)
334- result := or (result, factor)
335- }
336- // 2^32
337- assembly ("memory-safe" ) {
338- let factor := shl (5 , gt (x, 0xFFFFFFFF ))
339- x := shr (factor, x)
340- result := or (result, factor)
341- }
342- // 2^16
343- assembly ("memory-safe" ) {
344- let factor := shl (4 , gt (x, 0xFFFF ))
345- x := shr (factor, x)
346- result := or (result, factor)
347- }
348- // 2^8
349- assembly ("memory-safe" ) {
350- let factor := shl (3 , gt (x, 0xFF ))
351- x := shr (factor, x)
352- result := or (result, factor)
353- }
354- // 2^4
355- assembly ("memory-safe" ) {
356- let factor := shl (2 , gt (x, 0xF ))
357- x := shr (factor, x)
358- result := or (result, factor)
359- }
360- // 2^2
361- assembly ("memory-safe" ) {
362- let factor := shl (1 , gt (x, 0x3 ))
363- x := shr (factor, x)
364- result := or (result, factor)
365- }
366- // 2^1
367- // No need to shift x any more.
368- assembly ("memory-safe" ) {
369- let factor := gt (x, 0x1 )
370- result := or (result, factor)
325+ // 2^128
326+ result := shl (7 , lt (0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF , x))
327+ // 2^64
328+ result := or (result, shl (6 , lt (0xFFFFFFFFFFFFFFFF , shr (result, x))))
329+ // 2^32
330+ result := or (result, shl (5 , lt (0xFFFFFFFF , shr (result, x))))
331+ // 2^16
332+ result := or (result, shl (4 , lt (0xFFFF , shr (result, x))))
333+ // 2^8
334+ result := or (result, shl (3 , lt (0xFF , shr (result, x))))
335+ // 2^4
336+ result := or (result, shl (2 , lt (0xF , shr (result, x))))
337+ // 2^2
338+ result := or (result, shl (1 , lt (0x3 , shr (result, x))))
339+ // 2^1
340+ result := or (result, lt (0x1 , shr (result, x)))
371341 }
372342}
373343
@@ -596,10 +566,6 @@ function mulDivSigned(int256 x, int256 y, int256 denominator) pure returns (int2
596566/// @return result The result as a uint256.
597567/// @custom:smtchecker abstract-function-nondet
598568function sqrt (uint256 x ) pure returns (uint256 result ) {
599- if (x == 0 ) {
600- return 0 ;
601- }
602-
603569 // For our first guess, we calculate the biggest power of 2 which is smaller than the square root of x.
604570 //
605571 // We know that the "msb" (most significant bit) of x is a power of 2 such that we have:
@@ -623,53 +589,27 @@ function sqrt(uint256 x) pure returns (uint256 result) {
623589 // $$
624590 //
625591 // Consequently, $2^{log_2(x) /2} is a good first approximation of sqrt(x) with at least one correct bit.
626- uint256 xAux = uint256 (x);
627- result = 1 ;
628- if (xAux >= 2 ** 128 ) {
629- xAux >>= 128 ;
630- result <<= 64 ;
631- }
632- if (xAux >= 2 ** 64 ) {
633- xAux >>= 64 ;
634- result <<= 32 ;
635- }
636- if (xAux >= 2 ** 32 ) {
637- xAux >>= 32 ;
638- result <<= 16 ;
639- }
640- if (xAux >= 2 ** 16 ) {
641- xAux >>= 16 ;
642- result <<= 8 ;
643- }
644- if (xAux >= 2 ** 8 ) {
645- xAux >>= 8 ;
646- result <<= 4 ;
647- }
648- if (xAux >= 2 ** 4 ) {
649- xAux >>= 4 ;
650- result <<= 2 ;
651- }
652- if (xAux >= 2 ** 2 ) {
653- result <<= 1 ;
592+ unchecked {
593+ // ideally, we should use arithmetic operators, but solc is not smart enough to optimize `2**(msb(x)/2)`
594+ /// forge-lint: disable-next-line(incorrect-shift)
595+ result = 1 << (msb (x) >> 1 );
654596 }
655597
656598 // At this point, `result` is an estimation with at least one bit of precision. We know the true value has at
657599 // most 128 bits, since it is the square root of a uint256. Newton's method converges quadratically (precision
658600 // doubles at every iteration). We thus need at most 7 iteration to turn our partial result with one bit of
659601 // precision into the expected uint128 result.
660- unchecked {
661- result = (result + x / result) >> 1 ;
662- result = (result + x / result) >> 1 ;
663- result = (result + x / result) >> 1 ;
664- result = (result + x / result) >> 1 ;
665- result = (result + x / result) >> 1 ;
666- result = (result + x / result) >> 1 ;
667- result = (result + x / result) >> 1 ;
602+ assembly ("memory-safe" ) {
603+ // note: division by zero in EVM returns zero
604+ result := shr (1 , add (result, div (x, result)))
605+ result := shr (1 , add (result, div (x, result)))
606+ result := shr (1 , add (result, div (x, result)))
607+ result := shr (1 , add (result, div (x, result)))
608+ result := shr (1 , add (result, div (x, result)))
609+ result := shr (1 , add (result, div (x, result)))
610+ result := shr (1 , add (result, div (x, result)))
668611
669612 // If x is not a perfect square, round the result toward zero.
670- uint256 roundedResult = x / result;
671- if (result >= roundedResult) {
672- result = roundedResult;
673- }
613+ result := sub (result, gt (result, div (x, result)))
674614 }
675615}
0 commit comments