@@ -330,53 +330,23 @@ function exp2(uint256 x) pure returns (uint256 result) {
330330/// @return result The index of the most significant bit as a uint256.
331331/// @custom:smtchecker abstract-function-nondet
332332function msb (uint256 x ) pure returns (uint256 result ) {
333- // 2^128
334333 assembly ("memory-safe" ) {
335- let factor := shl (7 , gt (x, 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF ))
336- x := shr (factor, x)
337- result := or (result, factor)
338- }
339- // 2^64
340- assembly ("memory-safe" ) {
341- let factor := shl (6 , gt (x, 0xFFFFFFFFFFFFFFFF ))
342- x := shr (factor, x)
343- result := or (result, factor)
344- }
345- // 2^32
346- assembly ("memory-safe" ) {
347- let factor := shl (5 , gt (x, 0xFFFFFFFF ))
348- x := shr (factor, x)
349- result := or (result, factor)
350- }
351- // 2^16
352- assembly ("memory-safe" ) {
353- let factor := shl (4 , gt (x, 0xFFFF ))
354- x := shr (factor, x)
355- result := or (result, factor)
356- }
357- // 2^8
358- assembly ("memory-safe" ) {
359- let factor := shl (3 , gt (x, 0xFF ))
360- x := shr (factor, x)
361- result := or (result, factor)
362- }
363- // 2^4
364- assembly ("memory-safe" ) {
365- let factor := shl (2 , gt (x, 0xF ))
366- x := shr (factor, x)
367- result := or (result, factor)
368- }
369- // 2^2
370- assembly ("memory-safe" ) {
371- let factor := shl (1 , gt (x, 0x3 ))
372- x := shr (factor, x)
373- result := or (result, factor)
374- }
375- // 2^1
376- // No need to shift x any more.
377- assembly ("memory-safe" ) {
378- let factor := gt (x, 0x1 )
379- result := or (result, factor)
334+ // 2^128
335+ result := shl (7 , lt (0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF , x))
336+ // 2^64
337+ result := or (result, shl (6 , lt (0xFFFFFFFFFFFFFFFF , shr (result, x))))
338+ // 2^32
339+ result := or (result, shl (5 , lt (0xFFFFFFFF , shr (result, x))))
340+ // 2^16
341+ result := or (result, shl (4 , lt (0xFFFF , shr (result, x))))
342+ // 2^8
343+ result := or (result, shl (3 , lt (0xFF , shr (result, x))))
344+ // 2^4
345+ result := or (result, shl (2 , lt (0xF , shr (result, x))))
346+ // 2^2
347+ result := or (result, shl (1 , lt (0x3 , shr (result, x))))
348+ // 2^1
349+ result := or (result, lt (0x1 , shr (result, x)))
380350 }
381351}
382352
@@ -614,10 +584,6 @@ function mulDivSigned(int256 x, int256 y, int256 denominator) pure returns (int2
614584/// @return result The result as a uint256.
615585/// @custom:smtchecker abstract-function-nondet
616586function sqrt (uint256 x ) pure returns (uint256 result ) {
617- if (x == 0 ) {
618- return 0 ;
619- }
620-
621587 // For our first guess, we calculate the biggest power of 2 which is smaller than the square root of x.
622588 //
623589 // We know that the "msb" (most significant bit) of x is a power of 2 such that we have:
@@ -641,53 +607,27 @@ function sqrt(uint256 x) pure returns (uint256 result) {
641607 // $$
642608 //
643609 // Consequently, $2^{log_2(x) /2} is a good first approximation of sqrt(x) with at least one correct bit.
644- uint256 xAux = uint256 (x);
645- result = 1 ;
646- if (xAux >= 2 ** 128 ) {
647- xAux >>= 128 ;
648- result <<= 64 ;
649- }
650- if (xAux >= 2 ** 64 ) {
651- xAux >>= 64 ;
652- result <<= 32 ;
653- }
654- if (xAux >= 2 ** 32 ) {
655- xAux >>= 32 ;
656- result <<= 16 ;
657- }
658- if (xAux >= 2 ** 16 ) {
659- xAux >>= 16 ;
660- result <<= 8 ;
661- }
662- if (xAux >= 2 ** 8 ) {
663- xAux >>= 8 ;
664- result <<= 4 ;
665- }
666- if (xAux >= 2 ** 4 ) {
667- xAux >>= 4 ;
668- result <<= 2 ;
669- }
670- if (xAux >= 2 ** 2 ) {
671- result <<= 1 ;
610+ unchecked {
611+ // ideally, we should use arithmetic operators, but solc is not smart enough to optimize `2**(msb(x)/2)`
612+ /// forge-lint: disable-next-line(incorrect-shift)
613+ result = 1 << (msb (x) >> 1 );
672614 }
673615
674616 // At this point, `result` is an estimation with at least one bit of precision. We know the true value has at
675617 // most 128 bits, since it is the square root of a uint256. Newton's method converges quadratically (precision
676618 // doubles at every iteration). We thus need at most 7 iteration to turn our partial result with one bit of
677619 // precision into the expected uint128 result.
678- unchecked {
679- result = (result + x / result) >> 1 ;
680- result = (result + x / result) >> 1 ;
681- result = (result + x / result) >> 1 ;
682- result = (result + x / result) >> 1 ;
683- result = (result + x / result) >> 1 ;
684- result = (result + x / result) >> 1 ;
685- result = (result + x / result) >> 1 ;
620+ assembly ("memory-safe" ) {
621+ // note: division by zero in EVM returns zero
622+ result := shr (1 , add (result, div (x, result)))
623+ result := shr (1 , add (result, div (x, result)))
624+ result := shr (1 , add (result, div (x, result)))
625+ result := shr (1 , add (result, div (x, result)))
626+ result := shr (1 , add (result, div (x, result)))
627+ result := shr (1 , add (result, div (x, result)))
628+ result := shr (1 , add (result, div (x, result)))
686629
687630 // If x is not a perfect square, round the result toward zero.
688- uint256 roundedResult = x / result;
689- if (result >= roundedResult) {
690- result = roundedResult;
691- }
631+ result := sub (result, gt (result, div (x, result)))
692632 }
693633}
0 commit comments