Add 512bits add and mult operations (#5035)

This commit is contained in:
Hadrien Croubois
2025-02-26 11:04:14 +01:00
committed by GitHub
parent 2ed8956992
commit f999ba42a1
5 changed files with 372 additions and 195 deletions

View File

@ -17,6 +17,34 @@ library Math {
Expand // Away from zero
}
/**
* @dev Return the 512-bit addition of two uint256.
*
* The result is stored in two 256 variables such that sum = high * 2²⁵⁶ + low.
*/
function add512(uint256 a, uint256 b) internal pure returns (uint256 high, uint256 low) {
assembly ("memory-safe") {
low := add(a, b)
high := lt(low, a)
}
}
/**
* @dev Return the 512-bit multiplication of two uint256.
*
* The result is stored in two 256 variables such that product = high * 2²⁵⁶ + low.
*/
function mul512(uint256 a, uint256 b) internal pure returns (uint256 high, uint256 low) {
// 512-bit multiply [high low] = x * y. Compute the product mod 2²⁵⁶ and mod 2²⁵⁶ - 1, then use
// the Chinese Remainder Theorem to reconstruct the 512 bit result. The result is stored in two 256
// variables such that product = high * 2²⁵⁶ + low.
assembly ("memory-safe") {
let mm := mulmod(a, b, not(0))
low := mul(a, b)
high := sub(sub(mm, low), lt(mm, low))
}
}
/**
* @dev Returns the addition of two unsigned integers, with an success flag (no overflow).
*/
@ -143,26 +171,18 @@ library Math {
*/
function mulDiv(uint256 x, uint256 y, uint256 denominator) internal pure returns (uint256 result) {
unchecked {
// 512-bit multiply [prod1 prod0] = x * y. Compute the product mod 2²⁵⁶ and mod 2²⁵⁶ - 1, then use
// the Chinese Remainder Theorem to reconstruct the 512 bit result. The result is stored in two 256
// variables such that product = prod1 * 2²⁵⁶ + prod0.
uint256 prod0 = x * y; // Least significant 256 bits of the product
uint256 prod1; // Most significant 256 bits of the product
assembly {
let mm := mulmod(x, y, not(0))
prod1 := sub(sub(mm, prod0), lt(mm, prod0))
}
(uint256 high, uint256 low) = mul512(x, y);
// Handle non-overflow cases, 256 by 256 division.
if (prod1 == 0) {
if (high == 0) {
// Solidity will revert if denominator == 0, unlike the div opcode on its own.
// The surrounding unchecked block does not change this fact.
// See https://docs.soliditylang.org/en/latest/control-structures.html#checked-or-unchecked-arithmetic.
return prod0 / denominator;
return low / denominator;
}
// Make sure the result is less than 2²⁵⁶. Also prevents denominator == 0.
if (denominator <= prod1) {
if (denominator <= high) {
Panic.panic(ternary(denominator == 0, Panic.DIVISION_BY_ZERO, Panic.UNDER_OVERFLOW));
}
@ -170,15 +190,15 @@ library Math {
// 512 by 256 division.
///////////////////////////////////////////////
// Make division exact by subtracting the remainder from [prod1 prod0].
// Make division exact by subtracting the remainder from [high low].
uint256 remainder;
assembly {
// Compute remainder using mulmod.
remainder := mulmod(x, y, denominator)
// Subtract 256 bit number from 512 bit number.
prod1 := sub(prod1, gt(remainder, prod0))
prod0 := sub(prod0, remainder)
high := sub(high, gt(remainder, low))
low := sub(low, remainder)
}
// Factor powers of two out of denominator and compute largest power of two divisor of denominator.
@ -189,15 +209,15 @@ library Math {
// Divide denominator by twos.
denominator := div(denominator, twos)
// Divide [prod1 prod0] by twos.
prod0 := div(prod0, twos)
// Divide [high low] by twos.
low := div(low, twos)
// Flip twos such that it is 2²⁵⁶ / twos. If twos is zero, then it becomes one.
twos := add(div(sub(0, twos), twos), 1)
}
// Shift in bits from prod1 into prod0.
prod0 |= prod1 * twos;
// Shift in bits from high into low.
low |= high * twos;
// Invert denominator mod 2²⁵⁶. Now that denominator is an odd number, it has an inverse modulo 2²⁵⁶ such
// that denominator * inv ≡ 1 mod 2²⁵⁶. Compute the inverse by starting with a seed that is correct for
@ -215,9 +235,9 @@ library Math {
// Because the division is now exact we can divide by multiplying with the modular inverse of denominator.
// This will give us the correct result modulo 2²⁵⁶. Since the preconditions guarantee that the outcome is
// less than 2²⁵⁶, this is the final result. We don't need to compute the high bits of the result and prod1
// less than 2²⁵⁶, this is the final result. We don't need to compute the high bits of the result and high
// is no longer required.
result = prod0 * inverse;
result = low * inverse;
return result;
}
}
@ -229,6 +249,26 @@ library Math {
return mulDiv(x, y, denominator) + SafeCast.toUint(unsignedRoundsUp(rounding) && mulmod(x, y, denominator) > 0);
}
/**
* @dev Calculates floor(x * y >> n) with full precision. Throws if result overflows a uint256.
*/
function mulShr(uint256 x, uint256 y, uint8 n) internal pure returns (uint256 result) {
unchecked {
(uint256 high, uint256 low) = mul512(x, y);
if (high >= 1 << n) {
Panic.panic(Panic.UNDER_OVERFLOW);
}
return (high << (256 - n)) | (low >> n);
}
}
/**
* @dev Calculates x * y >> n with full precision, following the selected rounding direction.
*/
function mulShr(uint256 x, uint256 y, uint8 n, Rounding rounding) internal pure returns (uint256) {
return mulShr(x, y, n) + SafeCast.toUint(unsignedRoundsUp(rounding) && mulmod(x, y, 1 << n) > 0);
}
/**
* @dev Calculate the modular multiplicative inverse of a number in Z/nZ.
*